SyGuS: Functions
examples/api/cpp/sygus-fun.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the Sygus API.
11 *
12 * A simple demonstration of how to use the Sygus API to synthesize max and min
13 * functions.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20#include "utils.h"
21
22using namespace cvc5;
23
24int main()
25{
26 TermManager tm;
27 Solver slv(tm);
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 = tm.getIntegerSort();
37 Sort boolean = tm.getBooleanSort();
38
39 // declare input variables for the functions-to-synthesize
40 Term x = tm.mkVar(integer, "x");
41 Term y = tm.mkVar(integer, "y");
42
43 // declare the grammar non-terminals
44 Term start = tm.mkVar(integer, "Start");
45 Term start_bool = tm.mkVar(boolean, "StartBool");
46
47 // define the rules
48 Term zero = tm.mkInteger(0);
49 Term one = tm.mkInteger(1);
50
51 Term plus = tm.mkTerm(Kind::ADD, {start, start});
52 Term minus = tm.mkTerm(Kind::SUB, {start, start});
53 Term ite = tm.mkTerm(Kind::ITE, {start_bool, start, start});
54
55 Term And = tm.mkTerm(Kind::AND, {start_bool, start_bool});
56 Term Not = tm.mkTerm(Kind::NOT, {start_bool});
57 Term leq = tm.mkTerm(Kind::LEQ, {start, start});
58
59 // create the grammar object
60 Grammar g = slv.mkGrammar({x, y}, {start, start_bool});
61
62 // bind each non-terminal to its rules
63 g.addRules(start, {zero, one, x, y, plus, minus, ite});
64 g.addRules(start_bool, {And, Not, leq});
65
66 // declare the functions-to-synthesize. Optionally, provide the grammar
67 // constraints
68 Term max = slv.synthFun("max", {x, y}, integer, g);
69 Term min = slv.synthFun("min", {x, y}, integer);
70
71 // declare universal variables.
72 Term varX = slv.declareSygusVar("x", integer);
73 Term varY = slv.declareSygusVar("y", integer);
74
75 Term max_x_y = tm.mkTerm(Kind::APPLY_UF, {max, varX, varY});
76 Term min_x_y = tm.mkTerm(Kind::APPLY_UF, {min, varX, varY});
77
78 // add semantic constraints
79 // (constraint (>= (max x y) x))
80 slv.addSygusConstraint(tm.mkTerm(Kind::GEQ, {max_x_y, varX}));
81
82 // (constraint (>= (max x y) y))
83 slv.addSygusConstraint(tm.mkTerm(Kind::GEQ, {max_x_y, varY}));
84
85 // (constraint (or (= x (max x y))
86 // (= y (max x y))))
87 slv.addSygusConstraint(tm.mkTerm(Kind::OR,
88 {tm.mkTerm(Kind::EQUAL, {max_x_y, varX}),
89 tm.mkTerm(Kind::EQUAL, {max_x_y, varY})}));
90
91 // (constraint (= (+ (max x y) (min x y))
92 // (+ x y)))
93 slv.addSygusConstraint(tm.mkTerm(Kind::EQUAL,
94 {tm.mkTerm(Kind::ADD, {max_x_y, min_x_y}),
95 tm.mkTerm(Kind::ADD, {varX, varY})}));
96
97 // print solutions if available
98 if (slv.checkSynth().hasSolution())
99 {
100 // Output should be equivalent to:
101 // (
102 // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
103 // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
104 // )
105 std::vector<Term> terms = {max, min};
106 utils::printSynthSolutions(terms, slv.getSynthSolutions(terms));
107 }
108
109 return 0;
110}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the Sygus API.
11 *
12 * A simple demonstration of how to use the Sygus API to synthesize max and min
13 * functions.
14 */
15
16#include <cvc5/c/cvc5.h>
17#include <stdio.h>
18
19#include "utils.h"
20
21int main()
22{
23 Cvc5TermManager* tm = cvc5_term_manager_new();
24 Cvc5* slv = cvc5_new(tm);
25
26 // required options
27 cvc5_set_option(slv, "sygus", "true");
28 cvc5_set_option(slv, "incremental", "false");
29
30 // set the logic
31 cvc5_set_logic(slv, "LIA");
32
33 Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
34 Cvc5Sort bool_sort = cvc5_get_boolean_sort(tm);
35
36 // declare input variables for the functions-to-synthesize
37 Cvc5Term x = cvc5_mk_var(tm, int_sort, "x");
38 Cvc5Term y = cvc5_mk_var(tm, int_sort, "y");
39
40 // declare the grammar non-terminals
41 Cvc5Term start = cvc5_mk_var(tm, int_sort, "Start");
42 Cvc5Term start_bool = cvc5_mk_var(tm, bool_sort, "StartBool");
43
44 // define the rules
45 Cvc5Term zero = cvc5_mk_integer_int64(tm, 0);
46 Cvc5Term one = cvc5_mk_integer_int64(tm, 1);
47
48 Cvc5Term args2[2] = {start, start};
49 Cvc5Term plus = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
50 Cvc5Term minus = cvc5_mk_term(tm, CVC5_KIND_SUB, 2, args2);
51 Cvc5Term args3[3] = {start_bool, start, start};
52 Cvc5Term ite = cvc5_mk_term(tm, CVC5_KIND_ITE, 3, args3);
53
54 args2[0] = start_bool;
55 args2[1] = start_bool;
56 Cvc5Term And = cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2);
57 Cvc5Term args1[1] = {start_bool};
58 Cvc5Term Not = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1);
59 args2[0] = start;
60 args2[1] = start;
61 Cvc5Term leq = cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2);
62
63 // create the grammar object
64 Cvc5Term b[2] = {x, y};
65 Cvc5Term s[2] = {start, start_bool};
66 Cvc5Grammar g = cvc5_mk_grammar(slv, 2, b, 2, s);
67
68 // bind each non-terminal to its rules
69 Cvc5Term rules7[7] = {zero, one, x, y, plus, minus, ite};
70 cvc5_grammar_add_rules(g, start, 7, rules7);
71 Cvc5Term rules3[3] = {And, Not, leq};
72 cvc5_grammar_add_rules(g, start_bool, 3, rules3);
73
74 // declare the functions-to-synthesize. Optionally, provide the grammar
75 // constraints
76 Cvc5Term max = cvc5_synth_fun_with_grammar(slv, "max", 2, b, int_sort, g);
77 Cvc5Term min = cvc5_synth_fun(slv, "min", 2, b, int_sort);
78
79 // declare universal variables.
80 Cvc5Term var_x = cvc5_declare_sygus_var(slv, "x", int_sort);
81 Cvc5Term var_y = cvc5_declare_sygus_var(slv, "y", int_sort);
82
83 args3[0] = max;
84 args3[1] = var_x;
85 args3[2] = var_y;
86 Cvc5Term max_x_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 3, args3);
87 args3[0] = min;
88 Cvc5Term min_x_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 3, args3);
89
90 // add semantic constraints
91 // (constraint (>= (max x y) x))
92 args2[0] = max_x_y;
93 args2[1] = var_x;
94 cvc5_add_sygus_constraint(slv, cvc5_mk_term(tm, CVC5_KIND_GEQ, 2, args2));
95
96 // (constraint (>= (max x y) y))
97 args2[1] = var_y;
98 cvc5_add_sygus_constraint(slv, cvc5_mk_term(tm, CVC5_KIND_GEQ, 2, args2));
99
100 // (constraint (or (= x (max x y))
101 // (= y (max x y))))
102 args2[0] = max_x_y;
103 args2[1] = var_x;
104 Cvc5Term lhs = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
105 args2[0] = max_x_y;
106 args2[1] = var_y;
107 Cvc5Term rhs = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
108 args2[0] = lhs;
109 args2[1] = rhs;
110 cvc5_add_sygus_constraint(slv, cvc5_mk_term(tm, CVC5_KIND_OR, 2, args2));
111
112 // (constraint (= (+ (max x y) (min x y))
113 // (+ x y)))
114 args2[0] = max_x_y;
115 args2[1] = min_x_y;
116 cvc5_term_release(lhs); // optional, not needed anymore so we can release
117 lhs = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
118 args2[0] = var_x;
119 args2[1] = var_y;
120 cvc5_term_release(rhs); // optional, not needed anymore so we can release
121 rhs = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args2);
122 args2[0] = lhs;
123 args2[1] = rhs;
124 cvc5_add_sygus_constraint(slv, cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2));
125
126 // print solutions if available
127 if (cvc5_synth_result_has_solution(cvc5_check_synth(slv)))
128 {
129 // Output should be equivalent to:
130 // (
131 // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
132 // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
133 // )
134 args2[0] = max;
135 args2[1] = min;
136 const Cvc5Term* sols = cvc5_get_synth_solutions(slv, 2, args2);
137 print_synth_solutions(2, args2, sols);
138 }
139
140 cvc5_delete(slv);
141 cvc5_term_manager_delete(tm);
142 return 0;
143}
examples/api/java/SygusFun.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * A simple demonstration of the Sygus API.
11 *
12 * A simple demonstration of how to use the Sygus API to synthesize max and min
13 * functions. This is a direct translation of sygus-fun.cpp.
14 */
15
16import static io.github.cvc5.Kind.*;
17
18import io.github.cvc5.*;
19
20public class SygusFun
21{
22 public static void main(String args[]) throws CVC5ApiException
23 {
24 TermManager tm = new TermManager();
25 Solver slv = new Solver(tm);
26 {
27 // required options
28 slv.setOption("sygus", "true");
29 slv.setOption("incremental", "false");
30
31 // set the logic
32 slv.setLogic("LIA");
33
34 Sort integer = tm.getIntegerSort();
35 Sort bool = tm.getBooleanSort();
36
37 // declare input variables for the functions-to-synthesize
38 Term x = tm.mkVar(integer, "x");
39 Term y = tm.mkVar(integer, "y");
40
41 // declare the grammar non-terminals
42 Term start = tm.mkVar(integer, "Start");
43 Term start_bool = tm.mkVar(bool, "StartBool");
44
45 // define the rules
46 Term zero = tm.mkInteger(0);
47 Term one = tm.mkInteger(1);
48
49 Term plus = tm.mkTerm(ADD, start, start);
50 Term minus = tm.mkTerm(SUB, start, start);
51 Term ite = tm.mkTerm(ITE, start_bool, start, start);
52
53 Term And = tm.mkTerm(AND, start_bool, start_bool);
54 Term Not = tm.mkTerm(NOT, start_bool);
55 Term leq = tm.mkTerm(LEQ, start, start);
56
57 // create the grammar object
58 Grammar g = slv.mkGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
59
60 // bind each non-terminal to its rules
61 g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite});
62 g.addRules(start_bool, new Term[] {And, Not, leq});
63
64 // declare the functions-to-synthesize. Optionally, provide the grammar
65 // constraints
66 Term max = slv.synthFun("max", new Term[] {x, y}, integer, g);
67 Term min = slv.synthFun("min", new Term[] {x, y}, integer);
68
69 // declare universal variables.
70 Term varX = slv.declareSygusVar("x", integer);
71 Term varY = slv.declareSygusVar("y", integer);
72
73 Term max_x_y = tm.mkTerm(APPLY_UF, max, varX, varY);
74 Term min_x_y = tm.mkTerm(APPLY_UF, min, varX, varY);
75
76 // add semantic constraints
77 // (constraint (>= (max x y) x))
78 slv.addSygusConstraint(tm.mkTerm(GEQ, max_x_y, varX));
79
80 // (constraint (>= (max x y) y))
81 slv.addSygusConstraint(tm.mkTerm(GEQ, max_x_y, varY));
82
83 // (constraint (or (= x (max x y))
84 // (= y (max x y))))
85 slv.addSygusConstraint(
86 tm.mkTerm(OR, tm.mkTerm(EQUAL, max_x_y, varX), tm.mkTerm(EQUAL, max_x_y, varY)));
87
88 // (constraint (= (+ (max x y) (min x y))
89 // (+ x y)))
90 slv.addSygusConstraint(
91 tm.mkTerm(EQUAL, tm.mkTerm(ADD, max_x_y, min_x_y), tm.mkTerm(ADD, varX, varY)));
92
93 // print solutions if available
94 if (slv.checkSynth().hasSolution())
95 {
96 // Output should be equivalent to:
97 // (
98 // (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
99 // (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
100 // )
101 Term[] terms = new Term[] {max, min};
102 Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
103 }
104 }
105 Context.deletePointers();
106 }
107}
examples/api/python/sygus-fun.py
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# A simple demonstration of the solving capabilities of the cvc5 sygus solver
12# through the Python API. This is a direct translation of sygus-fun.cpp.
13##
14
15import copy
16import cvc5
17import utils
18from cvc5 import Kind
19
20if __name__ == "__main__":
21 tm = cvc5.TermManager()
22 slv = cvc5.Solver(tm)
23
24 # required options
25 slv.setOption("sygus", "true")
26 slv.setOption("incremental", "false")
27
28 # set the logic
29 slv.setLogic("LIA")
30
31 integer = tm.getIntegerSort()
32 boolean = tm.getBooleanSort()
33
34 # declare input variables for the functions-to-synthesize
35 x = tm.mkVar(integer, "x")
36 y = tm.mkVar(integer, "y")
37
38 # declare the grammar non-terminals
39 start = tm.mkVar(integer, "Start")
40 start_bool = tm.mkVar(boolean, "StartBool")
41
42 # define the rules
43 zero = tm.mkInteger(0)
44 one = tm.mkInteger(1)
45
46 plus = tm.mkTerm(Kind.ADD, start, start)
47 minus = tm.mkTerm(Kind.SUB, start, start)
48 ite = tm.mkTerm(Kind.ITE, start_bool, start, start)
49
50 And = tm.mkTerm(Kind.AND, start_bool, start_bool)
51 Not = tm.mkTerm(Kind.NOT, start_bool)
52 leq = tm.mkTerm(Kind.LEQ, start, start)
53
54 # create the grammar object
55 g = slv.mkGrammar([x, y], [start, start_bool])
56
57 # bind each non-terminal to its rules
58 g.addRules(start, [zero, one, x, y, plus, minus, ite])
59 g.addRules(start_bool, [And, Not, leq])
60
61 # declare the functions-to-synthesize. Optionally, provide the grammar
62 # constraints
63 max = slv.synthFun("max", [x, y], integer, g)
64 min = slv.synthFun("min", [x, y], integer)
65
66 # declare universal variables.
67 varX = slv.declareSygusVar("x", integer)
68 varY = slv.declareSygusVar("y", integer)
69
70 max_x_y = tm.mkTerm(Kind.APPLY_UF, max, varX, varY)
71 min_x_y = tm.mkTerm(Kind.APPLY_UF, min, varX, varY)
72
73 # add semantic constraints
74 # (constraint (>= (max x y) x))
75 slv.addSygusConstraint(tm.mkTerm(Kind.GEQ, max_x_y, varX))
76
77 # (constraint (>= (max x y) y))
78 slv.addSygusConstraint(tm.mkTerm(Kind.GEQ, max_x_y, varY))
79
80 # (constraint (or (= x (max x y))
81 # (= y (max x y))))
82 slv.addSygusConstraint(tm.mkTerm(
83 Kind.OR,
84 tm.mkTerm(Kind.EQUAL, max_x_y, varX),
85 tm.mkTerm(Kind.EQUAL, max_x_y, varY)))
86
87 # (constraint (= (+ (max x y) (min x y))
88 # (+ x y)))
89 slv.addSygusConstraint(tm.mkTerm(
90 Kind.EQUAL,
91 tm.mkTerm(Kind.ADD, max_x_y, min_x_y),
92 tm.mkTerm(Kind.ADD, varX, varY)))
93
94 # print solutions if available
95 if (slv.checkSynth().hasSolution()):
96 # Output should be equivalent to:
97 # (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
98 # (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
99 terms = [max, min]
100 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 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Utility methods.
11 */
12
13#ifndef CVC5__UTILS_H
14#define CVC5__UTILS_H
15
16#include <cvc5/cvc5.h>
17
18namespace utils {
19
20/**
21 * Print solutions for synthesis conjecture to the standard output stream.
22 * @param terms the terms for which the synthesis solutions were retrieved
23 * @param sols the synthesis solutions of the given terms
24 */
25void printSynthSolutions(const std::vector<cvc5::Term>& terms,
26 const std::vector<cvc5::Term>& sols);
27
28} // namespace utils
29
30#endif // CVC5__UTILS_H
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Implementations of utility methods.
11 */
12
13#include "utils.h"
14
15#include <iostream>
16
17namespace utils {
18
19using namespace cvc5;
20
21/**
22 * Get the string version of define-fun command.
23 * @param f the function to print
24 * @param params the function parameters
25 * @param body the function body
26 * @return a string version of define-fun
27 */
28std::string defineFunToString(const cvc5::Term& f,
29 const std::vector<cvc5::Term>& params,
30 const cvc5::Term& body)
31{
32 cvc5::Sort sort = f.getSort();
33 if (sort.isFunction())
34 {
35 sort = sort.getFunctionCodomainSort();
36 }
37 std::stringstream ss;
38 ss << "(define-fun " << f << " (";
39 for (size_t i = 0, n = params.size(); i < n; ++i)
40 {
41 if (i > 0)
42 {
43 ss << ' ';
44 }
45 ss << '(' << params[i] << ' ' << params[i].getSort() << ')';
46 }
47 ss << ") " << sort << ' ' << body << ')';
48 return ss.str();
49}
50
51void printSynthSolutions(const std::vector<cvc5::Term>& terms,
52 const std::vector<cvc5::Term>& sols)
53{
54 std::cout << '(' << std::endl;
55 for (size_t i = 0, n = terms.size(); i < n; ++i)
56 {
57 std::vector<cvc5::Term> params;
58 cvc5::Term body = sols[i];
59 if (sols[i].getKind() == cvc5::Kind::LAMBDA)
60 {
61 params.insert(params.end(), sols[i][0].begin(), sols[i][0].end());
62 body = sols[i][1];
63 }
64 std::cout << " " << defineFunToString(terms[i], params, body) << std::endl;
65 }
66 std::cout << ')' << std::endl;
67}
68
69} // namespace utils
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Utility methods.
11 */
12
13#ifndef CVC5__C_UTILS_H
14#define CVC5__C_UTILS_H
15
16#include <cvc5/c/cvc5.h>
17
18/**
19 * Print solutions for synthesis conjecture to the stdout.
20 * @param nterms The number of terms.
21 * @param terms The terms for which the synthesis solutions were retrieved.
22 * @param sols The synthesis solutions of the given terms.
23 */
24void print_synth_solutions(size_t nterms,
25 const Cvc5Term terms[],
26 const Cvc5Term sols[]);
27
28#endif
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Implementations of utility methods.
11 */
12
13#include "utils.h"
14
15#include <stdio.h>
16#include <stdlib.h>
17
18/**
19 * Get the string version of define-fun command.
20 * @param f The function to print.
21 * @param nparams The number of function parameters.
22 * @param params The function parameters.
23 * @param body The function body.
24 * @return A string version of define-fun.
25 */
26void print_define_fun(const Cvc5Term f,
27 size_t nparams,
28 const Cvc5Term params[],
29 const Cvc5Term body)
30{
31 Cvc5Sort sort = cvc5_term_get_sort(f);
32 if (cvc5_sort_is_fun(sort))
33 {
34 sort = cvc5_sort_fun_get_codomain(sort);
35 }
36 printf("(define-fun %s (", cvc5_term_to_string(f));
37 for (size_t i = 0; i < nparams; i++)
38 {
39 printf("%s", i > 0 ? " " : "");
40 printf("(%s %s)",
41 cvc5_term_to_string(params[i]),
42 cvc5_sort_to_string(cvc5_term_get_sort(params[i])));
43 }
44 printf(") %s %s)", cvc5_sort_to_string(sort), cvc5_term_to_string(body));
45}
46
47void print_synth_solutions(size_t nterms,
48 const Cvc5Term terms[],
49 const Cvc5Term sols[])
50{
51 printf("(\n");
52 for (size_t i = 0; i < nterms; i++)
53 {
54 size_t nparams = 0;
55 Cvc5Term* params = NULL;
56 Cvc5Term body = sols[i];
57 if (cvc5_term_get_kind(sols[i]) == CVC5_KIND_LAMBDA)
58 {
59 Cvc5Term psols = cvc5_term_get_child(sols[i], 0);
60 nparams = cvc5_term_get_num_children(psols);
61 params = (Cvc5Term*)malloc(nparams * sizeof(Cvc5Term));
62 for (size_t k = 0; k < nparams; k++)
63 {
64 params[k] = cvc5_term_get_child(psols, k);
65 }
66 body = cvc5_term_get_child(sols[i], 1);
67 }
68 printf(" ");
69 print_define_fun(terms[i], nterms, params, body);
70 if (params)
71 {
72 free(params);
73 }
74 printf("\n");
75 }
76 printf(")\n");
77}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * Utility methods.
11 */
12
13import io.github.cvc5.CVC5ApiException;
14import io.github.cvc5.Kind;
15import io.github.cvc5.Sort;
16import io.github.cvc5.Term;
17import java.util.ArrayList;
18import java.util.List;
19
20public class Utils
21{
22 /**
23 * Get the string version of define-fun command.
24 *
25 * @param f the function to print
26 * @param params the function parameters
27 * @param body the function body
28 * @return a string version of define-fun
29 */
30 private static String defineFunToString(Term f, Term[] params, Term body)
31 {
32 Sort sort = f.getSort();
33 if (sort.isFunction())
34 {
35 sort = sort.getFunctionCodomainSort();
36 }
37 StringBuilder ss = new StringBuilder();
38 ss.append("(define-fun ").append(f).append(" (");
39 for (int i = 0; i < params.length; ++i)
40 {
41 if (i > 0)
42 {
43 ss.append(' ');
44 }
45 ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')');
46 }
47 ss.append(") ").append(sort).append(' ').append(body).append(')');
48 return ss.toString();
49 }
50
51 /**
52 * Print solutions for synthesis conjecture to the standard output stream.
53 *
54 * @param terms the terms for which the synthesis solutions were retrieved
55 * @param sols the synthesis solutions of the given terms
56 */
57 public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException
58 {
59 System.out.println('(');
60 for (int i = 0; i < terms.length; ++i)
61 {
62 List<Term> params = new ArrayList<>();
63 Term body = sols[i];
64 if (sols[i].getKind() == Kind.LAMBDA)
65 {
66 for (Term t : sols[i].getChild(0))
67 {
68 params.add(t);
69 }
70 body = sols[i].getChild(1);
71 }
72 System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body));
73 }
74 System.out.println(')');
75 }
76}
1#!/usr/bin/env python
2###############################################################################
3# This file is part of the cvc5 project.
4#
5# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
6# in the top-level source directory and their institutional affiliations.
7# All rights reserved. See the file COPYING in the top-level source
8# directory for licensing information.
9# #############################################################################
10#
11# Utility Methods, translated from examples/api/utils.h
12##
13
14import cvc5
15from cvc5 import Kind
16
17# Get the string version of define-fun command.
18# @param f the function to print
19# @param params the function parameters
20# @param body the function body
21# @return a string version of define-fun
22
23
24def define_fun_to_string(f, params, body):
25 sort = f.getSort()
26 if sort.isFunction():
27 sort = f.getSort().getFunctionCodomainSort()
28 result = "(define-fun " + str(f) + " ("
29 for i in range(0, len(params)):
30 if i > 0:
31 result += " "
32 result += "(" + str(params[i]) + " " + str(params[i].getSort()) + ")"
33 result += ") " + str(sort) + " " + str(body) + ")"
34 return result
35
36
37# Print solutions for synthesis conjecture to the standard output stream.
38# @param terms the terms for which the synthesis solutions were retrieved
39# @param sols the synthesis solutions of the given terms
40
41
42def print_synth_solutions(terms, sols):
43 result = "(\n"
44 for i in range(0, len(terms)):
45 params = []
46 body = sols[i]
47 if sols[i].getKind() == Kind.LAMBDA:
48 params += sols[i][0]
49 body = sols[i][1]
50 result += " " + define_fun_to_string(terms[i], params, body) + "\n"
51 result += ")"
52 print(result)