SyGuS: Functions
examples/api/cpp/sygus-fun.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Abdalrhman Mohamed, Mathias Preiner, Andrew Reynolds
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 * A simple demonstration of the Sygus API.
14 *
15 * A simple demonstration of how to use the Sygus API to synthesize max and min
16 * functions.
17 */
18
19 #include <cvc5/cvc5.h>
20
21 #include <iostream>
22
23 #include "utils.h"
24
25 using namespace cvc5;
26
27 int main()
28 {
29 Solver slv;
30
31 // required options
32 slv.setOption("sygus", "true");
33 slv.setOption("incremental", "false");
34
35 // set the logic
36 slv.setLogic("LIA");
37
38 Sort integer = slv.getIntegerSort();
39 Sort boolean = slv.getBooleanSort();
40
41 // declare input variables for the functions-to-synthesize
42 Term x = slv.mkVar(integer, "x");
43 Term y = slv.mkVar(integer, "y");
44
45 // declare the grammar non-terminals
46 Term start = slv.mkVar(integer, "Start");
47 Term start_bool = slv.mkVar(boolean, "StartBool");
48
49 // define the rules
50 Term zero = slv.mkInteger(0);
51 Term one = slv.mkInteger(1);
52
53 Term plus = slv.mkTerm(ADD, {start, start});
54 Term minus = slv.mkTerm(SUB, {start, start});
55 Term ite = slv.mkTerm(ITE, {start_bool, start, start});
56
57 Term And = slv.mkTerm(AND, {start_bool, start_bool});
58 Term Not = slv.mkTerm(NOT, {start_bool});
59 Term leq = slv.mkTerm(LEQ, {start, start});
60
61 // create the grammar object
62 Grammar g = slv.mkGrammar({x, y}, {start, start_bool});
63
64 // bind each non-terminal to its rules
65 g.addRules(start, {zero, one, x, y, plus, minus, ite});
66 g.addRules(start_bool, {And, Not, leq});
67
68 // declare the functions-to-synthesize. Optionally, provide the grammar
69 // constraints
70 Term max = slv.synthFun("max", {x, y}, integer, g);
71 Term min = slv.synthFun("min", {x, y}, integer);
72
73 // declare universal variables.
74 Term varX = slv.declareSygusVar("x", integer);
75 Term varY = slv.declareSygusVar("y", integer);
76
77 Term max_x_y = slv.mkTerm(APPLY_UF, {max, varX, varY});
78 Term min_x_y = slv.mkTerm(APPLY_UF, {min, varX, varY});
79
80 // add semantic constraints
81 // (constraint (>= (max x y) x))
82 slv.addSygusConstraint(slv.mkTerm(GEQ, {max_x_y, varX}));
83
84 // (constraint (>= (max x y) y))
85 slv.addSygusConstraint(slv.mkTerm(GEQ, {max_x_y, varY}));
86
87 // (constraint (or (= x (max x y))
88 // (= y (max x y))))
89 slv.addSygusConstraint(slv.mkTerm(OR,
90 {slv.mkTerm(EQUAL, {max_x_y, varX}),
91 slv.mkTerm(EQUAL, {max_x_y, varY})}));
92
93 // (constraint (= (+ (max x y) (min x y))
94 // (+ x y)))
95 slv.addSygusConstraint(slv.mkTerm(
96 EQUAL,
97 {slv.mkTerm(ADD, {max_x_y, min_x_y}), slv.mkTerm(ADD, {varX, varY})}));
98
99 // print solutions if available
100 if (slv.checkSynth().hasSolution())
101 {
102 // Output should be equivalent to:
103 // (
104 // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
105 // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
106 // )
107 std::vector<Term> terms = {max, min};
108 utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
109 }
110
111 return 0;
112 }
examples/api/java/SygusFun.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Andrew Reynolds, Aina Niemetz
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 * A simple demonstration of the Sygus API.
14 *
15 * A simple demonstration of how to use the Sygus API to synthesize max and min
16 * functions. This is a direct translation of sygus-fun.cpp.
17 */
18
19 import static io.github.cvc5.Kind.*;
20
21 import io.github.cvc5.*;
22
23 public class SygusFun
24 {
25 public static void main(String args[]) throws CVC5ApiException
26 {
27 try (Solver slv = new Solver())
28 {
29 // required options
30 slv.setOption("sygus", "true");
31 slv.setOption("incremental", "false");
32
33 // set the logic
34 slv.setLogic("LIA");
35
36 Sort integer = slv.getIntegerSort();
37 Sort bool = slv.getBooleanSort();
38
39 // declare input variables for the functions-to-synthesize
40 Term x = slv.mkVar(integer, "x");
41 Term y = slv.mkVar(integer, "y");
42
43 // declare the grammar non-terminals
44 Term start = slv.mkVar(integer, "Start");
45 Term start_bool = slv.mkVar(bool, "StartBool");
46
47 // define the rules
48 Term zero = slv.mkInteger(0);
49 Term one = slv.mkInteger(1);
50
51 Term plus = slv.mkTerm(ADD, start, start);
52 Term minus = slv.mkTerm(SUB, start, start);
53 Term ite = slv.mkTerm(ITE, start_bool, start, start);
54
55 Term And = slv.mkTerm(AND, start_bool, start_bool);
56 Term Not = slv.mkTerm(NOT, start_bool);
57 Term leq = slv.mkTerm(LEQ, start, start);
58
59 // create the grammar object
60 Grammar g =
61 slv.mkGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
62
63 // bind each non-terminal to its rules
64 g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite});
65 g.addRules(start_bool, new Term[] {And, Not, leq});
66
67 // declare the functions-to-synthesize. Optionally, provide the grammar
68 // constraints
69 Term max = slv.synthFun("max", new Term[] {x, y}, integer, g);
70 Term min = slv.synthFun("min", new Term[] {x, y}, integer);
71
72 // declare universal variables.
73 Term varX = slv.declareSygusVar("x", integer);
74 Term varY = slv.declareSygusVar("y", integer);
75
76 Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
77 Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);
78
79 // add semantic constraints
80 // (constraint (>= (max x y) x))
81 slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX));
82
83 // (constraint (>= (max x y) y))
84 slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY));
85
86 // (constraint (or (= x (max x y))
87 // (= y (max x y))))
88 slv.addSygusConstraint(
89 slv.mkTerm(OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY)));
90
91 // (constraint (= (+ (max x y) (min x y))
92 // (+ x y)))
93 slv.addSygusConstraint(
94 slv.mkTerm(EQUAL, slv.mkTerm(ADD, max_x_y, min_x_y), slv.mkTerm(ADD, varX, varY)));
95
96 // print solutions if available
97 if (slv.checkSynth().hasSolution())
98 {
99 // Output should be equivalent to:
100 // (
101 // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
102 // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
103 // )
104 Term[] terms = new Term[] {max, min};
105 Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
106 }
107 }
108 }
109 }
examples/api/python/sygus-fun.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Yoni Zohar, Aina Niemetz, Andrew Reynolds
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 # A simple demonstration of the solving capabilities of the cvc5 sygus solver
15 # through the Python API. This is a direct translation of sygus-fun.cpp.
16 ##
17
18 import copy
19 import cvc5
20 import utils
21 from cvc5 import Kind
22
23 if __name__ == "__main__":
24 slv = cvc5.Solver()
25
26 # required options
27 slv.setOption("sygus", "true")
28 slv.setOption("incremental", "false")
29
30 # set the logic
31 slv.setLogic("LIA")
32
33 integer = slv.getIntegerSort()
34 boolean = slv.getBooleanSort()
35
36 # declare input variables for the functions-to-synthesize
37 x = slv.mkVar(integer, "x")
38 y = slv.mkVar(integer, "y")
39
40 # declare the grammar non-terminals
41 start = slv.mkVar(integer, "Start")
42 start_bool = slv.mkVar(boolean, "StartBool")
43
44 # define the rules
45 zero = slv.mkInteger(0)
46 one = slv.mkInteger(1)
47
48 plus = slv.mkTerm(Kind.ADD, start, start)
49 minus = slv.mkTerm(Kind.SUB, start, start)
50 ite = slv.mkTerm(Kind.ITE, start_bool, start, start)
51
52 And = slv.mkTerm(Kind.AND, start_bool, start_bool)
53 Not = slv.mkTerm(Kind.NOT, start_bool)
54 leq = slv.mkTerm(Kind.LEQ, start, start)
55
56 # create the grammar object
57 g = slv.mkGrammar([x, y], [start, start_bool])
58
59 # bind each non-terminal to its rules
60 g.addRules(start, {zero, one, x, y, plus, minus, ite})
61 g.addRules(start_bool, {And, Not, leq})
62
63 # declare the functions-to-synthesize. Optionally, provide the grammar
64 # constraints
65 max = slv.synthFun("max", [x, y], integer, g)
66 min = slv.synthFun("min", [x, y], integer)
67
68 # declare universal variables.
69 varX = slv.declareSygusVar("x", integer)
70 varY = slv.declareSygusVar("y", integer)
71
72 max_x_y = slv.mkTerm(Kind.APPLY_UF, max, varX, varY)
73 min_x_y = slv.mkTerm(Kind.APPLY_UF, min, varX, varY)
74
75 # add semantic constraints
76 # (constraint (>= (max x y) x))
77 slv.addSygusConstraint(slv.mkTerm(Kind.GEQ, max_x_y, varX))
78
79 # (constraint (>= (max x y) y))
80 slv.addSygusConstraint(slv.mkTerm(Kind.GEQ, max_x_y, varY))
81
82 # (constraint (or (= x (max x y))
83 # (= y (max x y))))
84 slv.addSygusConstraint(slv.mkTerm(
85 Kind.OR,
86 slv.mkTerm(Kind.EQUAL, max_x_y, varX),
87 slv.mkTerm(Kind.EQUAL, max_x_y, varY)))
88
89 # (constraint (= (+ (max x y) (min x y))
90 # (+ x y)))
91 slv.addSygusConstraint(slv.mkTerm(
92 Kind.EQUAL,
93 slv.mkTerm(Kind.ADD, max_x_y, min_x_y),
94 slv.mkTerm(Kind.ADD, varX, varY)))
95
96 # print solutions if available
97 if (slv.checkSynth().hasSolution()):
98 # Output should be equivalent to:
99 # (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
100 # (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
101 terms = [max, min]
102 utils.print_synth_solutions(terms, slv.getSynthSolutions(terms))
examples/api/smtlib/sygus-fun.sy
1 ; The printed output for this example should be equivalent to:
2 ; (
3 ; (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
4 ; (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
5 ; )
6
7 (set-logic LIA)
8 (synth-fun max ((x Int) (y Int)) Int
9 ((Start Int) (StartBool Bool))
10 ((Start Int (0 1 x y
11 (+ Start Start)
12 (- Start Start)
13 (ite StartBool Start Start)))
14 (StartBool Bool ((and StartBool StartBool)
15 (not StartBool)
16 (<= Start Start)))))
17 (synth-fun min ((x Int) (y Int)) Int)
18 (declare-var x Int)
19 (declare-var y Int)
20 (constraint (>= (max x y) x))
21 (constraint (>= (max x y) y))
22 (constraint (or (= x (max x y)) (= y (max x y))))
23 (constraint (= (+ (max x y) (min x y)) (+ x y)))
24 (check-synth)
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
21 namespace 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 */
28 void 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
20 namespace utils {
21
22 using 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 */
31 std::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
54 void 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
16 import io.github.cvc5.CVC5ApiException;
17 import io.github.cvc5.Kind;
18 import io.github.cvc5.Sort;
19 import io.github.cvc5.Term;
20 import java.util.ArrayList;
21 import java.util.List;
22
23 public 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
17 import cvc5
18 from 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
27 def 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
45 def 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)