SyGuS: Grammars
The utility method used for printing the synthesis solutions in the examples
above is defined separately in the
utils
module:
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Utility methods.
14 */
15
16#ifndef CVC5__UTILS_H
17#define CVC5__UTILS_H
18
19#include <cvc5/cvc5.h>
20
21namespace utils {
22
23/**
24 * Print solutions for synthesis conjecture to the standard output stream.
25 * @param terms the terms for which the synthesis solutions were retrieved
26 * @param sols the synthesis solutions of the given terms
27 */
28void printSynthSolutions(const std::vector<cvc5::Term>& terms,
29 const std::vector<cvc5::Term>& sols);
30
31} // namespace utils
32
33#endif // CVC5__UTILS_H
1/******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner, Yoni Zohar
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Implementations of utility methods.
14 */
15
16#include "utils.h"
17
18#include <iostream>
19
20namespace utils {
21
22using namespace cvc5;
23
24/**
25 * Get the string version of define-fun command.
26 * @param f the function to print
27 * @param params the function parameters
28 * @param body the function body
29 * @return a string version of define-fun
30 */
31std::string defineFunToString(const cvc5::Term& f,
32 const std::vector<cvc5::Term>& params,
33 const cvc5::Term& body)
34{
35 cvc5::Sort sort = f.getSort();
36 if (sort.isFunction())
37 {
38 sort = sort.getFunctionCodomainSort();
39 }
40 std::stringstream ss;
41 ss << "(define-fun " << f << " (";
42 for (size_t i = 0, n = params.size(); i < n; ++i)
43 {
44 if (i > 0)
45 {
46 ss << ' ';
47 }
48 ss << '(' << params[i] << ' ' << params[i].getSort() << ')';
49 }
50 ss << ") " << sort << ' ' << body << ')';
51 return ss.str();
52}
53
54void printSynthSolutions(const std::vector<cvc5::Term>& terms,
55 const std::vector<cvc5::Term>& sols)
56{
57 std::cout << '(' << std::endl;
58 for (size_t i = 0, n = terms.size(); i < n; ++i)
59 {
60 std::vector<cvc5::Term> params;
61 cvc5::Term body = sols[i];
62 if (sols[i].getKind() == cvc5::LAMBDA)
63 {
64 params.insert(params.end(), sols[i][0].begin(), sols[i][0].end());
65 body = sols[i][1];
66 }
67 std::cout << " " << defineFunToString(terms[i], params, body) << std::endl;
68 }
69 std::cout << ')' << std::endl;
70}
71
72} // namespace utils
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Abdalrhman Mohamed, Andres Noetzli
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * Utility methods.
14 */
15
16import io.github.cvc5.CVC5ApiException;
17import io.github.cvc5.Kind;
18import io.github.cvc5.Sort;
19import io.github.cvc5.Term;
20import java.util.ArrayList;
21import java.util.List;
22
23public class Utils
24{
25 /**
26 * Get the string version of define-fun command.
27 *
28 * @param f the function to print
29 * @param params the function parameters
30 * @param body the function body
31 * @return a string version of define-fun
32 */
33 private static String defineFunToString(Term f, Term[] params, Term body)
34 {
35 Sort sort = f.getSort();
36 if (sort.isFunction())
37 {
38 sort = sort.getFunctionCodomainSort();
39 }
40 StringBuilder ss = new StringBuilder();
41 ss.append("(define-fun ").append(f).append(" (");
42 for (int i = 0; i < params.length; ++i)
43 {
44 if (i > 0)
45 {
46 ss.append(' ');
47 }
48 ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')');
49 }
50 ss.append(") ").append(sort).append(' ').append(body).append(')');
51 return ss.toString();
52 }
53
54 /**
55 * Print solutions for synthesis conjecture to the standard output stream.
56 *
57 * @param terms the terms for which the synthesis solutions were retrieved
58 * @param sols the synthesis solutions of the given terms
59 */
60 public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException
61 {
62 System.out.println('(');
63 for (int i = 0; i < terms.length; ++i)
64 {
65 List<Term> params = new ArrayList<>();
66 Term body = sols[i];
67 if (sols[i].getKind() == Kind.LAMBDA)
68 {
69 for (Term t : sols[i].getChild(0))
70 {
71 params.add(t);
72 }
73 body = sols[i].getChild(1);
74 }
75 System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body));
76 }
77 System.out.println(')');
78 }
79}
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Yoni Zohar, Abdalrhman Mohamed, Alex Ozdemir
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# Utility Methods, translated from examples/api/utils.h
15##
16
17import cvc5
18from cvc5 import Kind
19
20# Get the string version of define-fun command.
21# @param f the function to print
22# @param params the function parameters
23# @param body the function body
24# @return a string version of define-fun
25
26
27def define_fun_to_string(f, params, body):
28 sort = f.getSort()
29 if sort.isFunction():
30 sort = f.getSort().getFunctionCodomainSort()
31 result = "(define-fun " + str(f) + " ("
32 for i in range(0, len(params)):
33 if i > 0:
34 result += " "
35 result += "(" + str(params[i]) + " " + str(params[i].getSort()) + ")"
36 result += ") " + str(sort) + " " + str(body) + ")"
37 return result
38
39
40# Print solutions for synthesis conjecture to the standard output stream.
41# @param terms the terms for which the synthesis solutions were retrieved
42# @param sols the synthesis solutions of the given terms
43
44
45def print_synth_solutions(terms, sols):
46 result = "(\n"
47 for i in range(0, len(terms)):
48 params = []
49 body = sols[i]
50 if sols[i].getKind() == Kind.LAMBDA:
51 params += sols[i][0]
52 body = sols[i][1]
53 result += " " + define_fun_to_string(terms[i], params, body) + "\n"
54 result += ")"
55 print(result)