Theory Combination
examples/api/cpp/combination.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 capabilities of cvc5
11 *
12 * A simple demonstration of how to use uninterpreted functions, combining this
13 * with arithmetic, and extracting a model at the end of a satisfiable query.
14 * The model is displayed using getValue().
15 */
16
17#include <cvc5/cvc5.h>
18
19#include <iostream>
20
21using namespace std;
22using namespace cvc5;
23
24void prefixPrintGetValue(Solver& slv, Term t, int level = 0)
25{
26 cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl;
27
28 for (const Term& c : t)
29 {
30 prefixPrintGetValue(slv, c, level + 1);
31 }
32}
33
34int main()
35{
36 TermManager tm;
37 Solver slv(tm);
38 slv.setOption("produce-models", "true"); // Produce Models
39 slv.setOption("dag-thresh", "0"); // Disable dagifying the output
40 slv.setLogic("QF_UFLIRA");
41
42 // Sorts
43 Sort u = tm.mkUninterpretedSort("u");
44 Sort integer = tm.getIntegerSort();
45 Sort boolean = tm.getBooleanSort();
46 Sort uToInt = tm.mkFunctionSort({u}, integer);
47 Sort intPred = tm.mkFunctionSort({integer}, boolean);
48
49 // Variables
50 Term x = tm.mkConst(u, "x");
51 Term y = tm.mkConst(u, "y");
52
53 // Functions
54 Term f = tm.mkConst(uToInt, "f");
55 Term p = tm.mkConst(intPred, "p");
56
57 // Constants
58 Term zero = tm.mkInteger(0);
59 Term one = tm.mkInteger(1);
60
61 // Terms
62 Term f_x = tm.mkTerm(Kind::APPLY_UF, {f, x});
63 Term f_y = tm.mkTerm(Kind::APPLY_UF, {f, y});
64 Term sum = tm.mkTerm(Kind::ADD, {f_x, f_y});
65 Term p_0 = tm.mkTerm(Kind::APPLY_UF, {p, zero});
66 Term p_f_y = tm.mkTerm(Kind::APPLY_UF, {p, f_y});
67
68 // Construct the assertions
69 Term assertions =
70 tm.mkTerm(Kind::AND,
71 {
72 tm.mkTerm(Kind::LEQ, {zero, f_x}), // 0 <= f(x)
73 tm.mkTerm(Kind::LEQ, {zero, f_y}), // 0 <= f(y)
74 tm.mkTerm(Kind::LEQ, {sum, one}), // f(x) + f(y) <= 1
75 p_0.notTerm(), // not p(0)
76 p_f_y // p(f(y))
77 });
78 slv.assertFormula(assertions);
79
80 cout << "Given the following assertions:" << endl
81 << assertions << endl << endl;
82
83 cout << "Prove x /= y is entailed." << endl
84 << "cvc5: " << slv.checkSatAssuming(tm.mkTerm(Kind::EQUAL, {x, y}))
85 << "." << endl
86 << endl;
87
88 cout << "Call checkSat to show that the assertions are satisfiable." << endl
89 << "cvc5: " << slv.checkSat() << "." << endl
90 << endl;
91
92 cout << "Call slv.getValue(...) on terms of interest."
93 << endl;
94 cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl;
95 cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl;
96 cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl;
97 cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl;
98 cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y)
99 << endl << endl;
100
101 cout << "Alternatively, iterate over assertions and call slv.getValue(...) "
102 << "on all terms."
103 << endl;
104 prefixPrintGetValue(slv, assertions);
105
106 cout << endl;
107 cout << "You can also use nested loops to iterate over terms." << endl;
108 for (Term::const_iterator it = assertions.begin();
109 it != assertions.end();
110 ++it)
111 {
112 cout << "term: " << *it << endl;
113 for (Term::const_iterator it2 = (*it).begin();
114 it2 != (*it).end();
115 ++it2)
116 {
117 cout << " + child: " << *it2 << std::endl;
118 }
119 }
120 cout << endl;
121 cout << "Alternatively, you can also use for-each loops." << endl;
122 for (const Term& t : assertions)
123 {
124 cout << "term: " << t << endl;
125 for (const Term& c : t)
126 {
127 cout << " + child: " << c << endl;
128 }
129 }
130
131 return 0;
132}
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 capabilities of cvc5
11 *
12 * A simple demonstration of how to use uninterpreted functions, combining this
13 * with arithmetic, and extracting a model at the end of a satisfiable query.
14 * The model is displayed using getValue().
15 */
16
17#include <cvc5/c/cvc5.h>
18#include <stdio.h>
19
20void prefix_print_get_value(Cvc5* slv, Cvc5Term t, int32_t level)
21{
22 // Note: The const char* returned by cvc5_term_to_string is only valid
23 // until the next call to cvc5_term_to_string. Thus, we cannot
24 // chain calls to this function in a single printf statement.
25 printf("slv.getValue(%s): ", cvc5_term_to_string(t));
26 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, t)));
27
28 for (size_t i = 0, n = cvc5_term_get_num_children(t); i < n; ++i)
29 {
30 prefix_print_get_value(slv, cvc5_term_get_child(t, i), level + 1);
31 }
32}
33
34int main()
35{
36 Cvc5TermManager* tm = cvc5_term_manager_new();
37 Cvc5* slv = cvc5_new(tm);
38 cvc5_set_option(slv, "produce-models", "true");
39 cvc5_set_option(slv, "dag-thresh", "0");
40 cvc5_set_logic(slv, "QF_UFLIRA");
41
42 // Sorts
43 Cvc5Sort un_sort = cvc5_mk_uninterpreted_sort(tm, "u");
44 Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
45 Cvc5Sort bool_sort = cvc5_get_boolean_sort(tm);
46 Cvc5Sort domain[1] = {un_sort};
47 Cvc5Sort un_to_int_sort = cvc5_mk_fun_sort(tm, 1, domain, int_sort);
48 domain[0] = int_sort;
49 Cvc5Sort int_pred_sort = cvc5_mk_fun_sort(tm, 1, domain, bool_sort);
50
51 // Variables
52 Cvc5Term x = cvc5_mk_const(tm, un_sort, "x");
53 Cvc5Term y = cvc5_mk_const(tm, un_sort, "y");
54
55 // Functions
56 Cvc5Term f = cvc5_mk_const(tm, un_to_int_sort, "f");
57 Cvc5Term p = cvc5_mk_const(tm, int_pred_sort, "p");
58
59 // Constants
60 Cvc5Term zero = cvc5_mk_integer_int64(tm, 0);
61 Cvc5Term one = cvc5_mk_integer_int64(tm, 1);
62
63 // Terms
64 Cvc5Term args[2] = {f, x};
65 Cvc5Term f_x = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args);
66 args[1] = y;
67 Cvc5Term f_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args);
68 args[0] = f_x;
69 args[1] = f_y;
70 Cvc5Term sum = cvc5_mk_term(tm, CVC5_KIND_ADD, 2, args);
71 args[0] = p;
72 args[1] = zero;
73 Cvc5Term p_0 = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args);
74 args[0] = p;
75 args[1] = f_y;
76 Cvc5Term p_f_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args);
77
78 // Construct the assertions
79 Cvc5Term args0[2] = {zero, f_x};
80 Cvc5Term args1[2] = {zero, f_y};
81 Cvc5Term args2[2] = {sum, one};
82 Cvc5Term args3[1] = {p_0};
83
84 Cvc5Term aargs[5] = {
85 cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args0), // 0 <= f(x)
86 cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args1), // 0 <= f(y)
87 cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2), // f(x) + f(y) <= 1
88 cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args3), // not p(0)
89 p_f_y};
90 Cvc5Term assertions = cvc5_mk_term(tm, CVC5_KIND_AND, 5, aargs);
91 cvc5_assert_formula(slv, assertions);
92
93 printf("Given the following assertions:\n");
94 printf("%s\n\n", cvc5_term_to_string(assertions));
95
96 printf("Prove x /= y is entailed.\n");
97 args[0] = x;
98 args[1] = y;
99 Cvc5Term assumptions[1] = {cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args)};
100 printf("cvc5: %s.\n\n",
101 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
102
103 printf("Call checkSat to show that the assertions are satisfiable.\n");
104 printf("cvc5: %s.\n\n", cvc5_result_to_string(cvc5_check_sat(slv)));
105
106 printf("Call slv.getValue(...) on terms of interest.\n");
107 printf("cvc5_get_value(slv, %s): ", cvc5_term_to_string(f_x));
108 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, f_x)));
109 printf("cvc5_get_value(slv, %s): ", cvc5_term_to_string(f_y));
110 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, f_y)));
111 printf("cvc5_get_value(slv, %s): ", cvc5_term_to_string(sum));
112 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, sum)));
113 printf("cvc5_get_value(slv, %s): ", cvc5_term_to_string(p_0));
114 printf("%s\n", cvc5_term_to_string(cvc5_get_value(slv, p_0)));
115 printf("cvc5_get_value(slv, %s): ", cvc5_term_to_string(p_f_y));
116 printf("%s\n\n", cvc5_term_to_string(cvc5_get_value(slv, p_f_y)));
117
118 printf(
119 "Alternatively, iterate over assertions and call slv.getValue(...) on "
120 "all terms.\n");
121 prefix_print_get_value(slv, assertions, 0);
122 printf("\n");
123
124 printf("You can also use nested loops to iterate over terms.\n");
125 for (size_t i = 0, n = cvc5_term_get_num_children(assertions); i < n; ++i)
126 {
127 Cvc5Term child = cvc5_term_get_child(assertions, i);
128 printf("term: %s\n", cvc5_term_to_string(child));
129 for (size_t j = 0, m = cvc5_term_get_num_children(child); j < m; ++j)
130 {
131 printf(" + child: %s\n",
132 cvc5_term_to_string(cvc5_term_get_child(child, j)));
133 }
134 }
135
136 cvc5_delete(slv);
137 cvc5_term_manager_delete(tm);
138 return 0;
139}
examples/api/java/Combination.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 capabilities of cvc5
11 *
12 * A simple demonstration of how to use uninterpreted functions, combining this
13 * with arithmetic, and extracting a model at the end of a satisfiable query.
14 * The model is displayed using getValue().
15 */
16
17import io.github.cvc5.*;
18import java.util.Iterator;
19
20public class Combination
21{
22 private static void prefixPrintGetValue(Solver slv, Term t)
23 {
24 prefixPrintGetValue(slv, t, 0);
25 }
26
27 private static void prefixPrintGetValue(Solver slv, Term t, int level)
28 {
29 System.out.println("slv.getValue(" + t + "): " + slv.getValue(t));
30
31 for (Term c : t)
32 {
33 prefixPrintGetValue(slv, c, level + 1);
34 }
35 }
36
37 public static void main(String[] args) throws CVC5ApiException
38 {
39 TermManager tm = new TermManager();
40 Solver slv = new Solver(tm);
41 {
42 slv.setOption("produce-models", "true"); // Produce Models
43 slv.setOption("dag-thresh", "0"); // Disable dagifying the output
44 slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
45 slv.setLogic("QF_UFLIRA");
46
47 // Sorts
48 Sort u = tm.mkUninterpretedSort("u");
49 Sort integer = tm.getIntegerSort();
50 Sort bool = tm.getBooleanSort();
51 Sort uToInt = tm.mkFunctionSort(u, integer);
52 Sort intPred = tm.mkFunctionSort(integer, bool);
53
54 // Variables
55 Term x = tm.mkConst(u, "x");
56 Term y = tm.mkConst(u, "y");
57
58 // Functions
59 Term f = tm.mkConst(uToInt, "f");
60 Term p = tm.mkConst(intPred, "p");
61
62 // Constants
63 Term zero = tm.mkInteger(0);
64 Term one = tm.mkInteger(1);
65
66 // Terms
67 Term f_x = tm.mkTerm(Kind.APPLY_UF, f, x);
68 Term f_y = tm.mkTerm(Kind.APPLY_UF, f, y);
69 Term sum = tm.mkTerm(Kind.ADD, f_x, f_y);
70 Term p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero);
71 Term p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y);
72
73 // Construct the assertions
74 Term assertions = tm.mkTerm(Kind.AND,
75 new Term[] {
76 tm.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x)
77 tm.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y)
78 tm.mkTerm(Kind.LEQ, sum, one), // f(x) + f(y) <= 1
79 p_0.notTerm(), // not p(0)
80 p_f_y // p(f(y))
81 });
82 slv.assertFormula(assertions);
83
84 System.out.println("Given the following assertions:\n" + assertions + "\n");
85
86 System.out.println("Prove x /= y is entailed. \n"
87 + "cvc5: " + slv.checkSatAssuming(tm.mkTerm(Kind.EQUAL, x, y)) + ".\n");
88
89 System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
90 + "cvc5: " + slv.checkSat() + ".\n");
91
92 System.out.println("Call slv.getValue(...) on terms of interest.");
93 System.out.println("slv.getValue(" + f_x + "): " + slv.getValue(f_x));
94 System.out.println("slv.getValue(" + f_y + "): " + slv.getValue(f_y));
95 System.out.println("slv.getValue(" + sum + "): " + slv.getValue(sum));
96 System.out.println("slv.getValue(" + p_0 + "): " + slv.getValue(p_0));
97 System.out.println("slv.getValue(" + p_f_y + "): " + slv.getValue(p_f_y) + "\n");
98
99 System.out.println("Alternatively, iterate over assertions and call slv.getValue(...) "
100 + "on all terms.");
101 prefixPrintGetValue(slv, assertions);
102
103 System.out.println();
104 System.out.println("You can also use nested loops to iterate over terms.");
105 Iterator<Term> it1 = assertions.iterator();
106 while (it1.hasNext())
107 {
108 Term t = it1.next();
109 System.out.println("term: " + t);
110 Iterator<Term> it2 = t.iterator();
111 while (it2.hasNext())
112 {
113 System.out.println(" + child: " + it2.next());
114 }
115 }
116 System.out.println();
117 System.out.println("Alternatively, you can also use for-each loops.");
118 for (Term t : assertions)
119 {
120 System.out.println("term: " + t);
121 for (Term c : t)
122 {
123 System.out.println(" + child: " + c);
124 }
125 }
126 }
127 Context.deletePointers();
128 }
129}
examples/api/python/pythonic/combination.py
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 capabilities of cvc5
11#
12# A simple demonstration of how to use uninterpreted functions, combining this
13# with arithmetic, and extracting a model at the end of a satisfiable query.
14# The model is displayed using getValue().
15##
16from cvc5.pythonic import *
17
18if __name__ == "__main__":
19
20 U = DeclareSort("U")
21 x, y = Consts("x y", U)
22
23 f = Function("f", U, IntSort())
24 p = Function("p", IntSort(), BoolSort())
25
26 assumptions = [f(x) >= 0, f(y) >= 0, f(x) + f(y) <= 1, Not(p(0)), p(f(y))]
27
28 prove(Implies(And(assumptions), x != y))
29
30 s = Solver()
31 s.add(assumptions)
32 assert sat == s.check()
33 m = s.model()
34
35 def print_val(t):
36 print("{}: {}".format(t, m[t]))
37
38 # print the of some terms
39 print_val(f(x))
40 print_val(f(y))
41 print_val(f(x) + f(y))
42 print_val(p(0))
43 print_val(p(f(y)))
44
45 # print value of *all* terms
46 def print_all_subterms(t):
47 print_val(t)
48 for c in t.children():
49 print_all_subterms(c)
50 print_all_subterms(And(assumptions))
examples/api/python/combination.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 combination
12# solver through the Python API. This is a direct translation of
13# combination-new.cpp.
14##
15
16import cvc5
17from cvc5 import Kind
18
19def prefixPrintGetValue(slv, t, level=0):
20 print("slv.getValue({}): {}".format(t, slv.getValue(t)))
21 for c in t:
22 prefixPrintGetValue(slv, c, level + 1)
23
24if __name__ == "__main__":
25 tm = cvc5.TermManager()
26 slv = cvc5.Solver(tm)
27 slv.setOption("produce-models", "true") # Produce Models
28 slv.setOption("dag-thresh", "0") # Disable dagifying the output
29 slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
30 slv.setLogic("QF_UFLIRA")
31
32 # Sorts
33 u = tm.mkUninterpretedSort("u")
34 integer = tm.getIntegerSort()
35 boolean = tm.getBooleanSort()
36 uToInt = tm.mkFunctionSort(u, integer)
37 intPred = tm.mkFunctionSort(integer, boolean)
38
39 # Variables
40 x = tm.mkConst(u, "x")
41 y = tm.mkConst(u, "y")
42
43 # Functions
44 f = tm.mkConst(uToInt, "f")
45 p = tm.mkConst(intPred, "p")
46
47 # Constants
48 zero = tm.mkInteger(0)
49 one = tm.mkInteger(1)
50
51 # Terms
52 f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
53 f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
54 sum_ = tm.mkTerm(Kind.ADD, f_x, f_y)
55 p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero)
56 p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
57
58 # Construct the assertions
59 assertions = tm.mkTerm(Kind.AND,
60 tm.mkTerm(Kind.LEQ, zero, f_x), # 0 <= f(x)
61 tm.mkTerm(Kind.LEQ, zero, f_y), # 0 <= f(y)
62 tm.mkTerm(Kind.LEQ, sum_, one), # f(x) + f(y) <= 1
63 p_0.notTerm(), # not p(0)
64 p_f_y # p(f(y))
65 )
66
67 slv.assertFormula(assertions)
68
69 print("Given the following assertions:", assertions, "\n")
70 print("Prove x /= y is entailed.\ncvc5: ",
71 slv.checkSatAssuming(tm.mkTerm(Kind.EQUAL, x, y)), "\n")
72
73 print("Call checkSat to show that the assertions are satisfiable")
74 print("cvc5:", slv.checkSat(), "\n")
75
76 print("Call slv.getValue(...) on terms of interest")
77 print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x)))
78 print("slv.getValue({}): {}".format(f_y, slv.getValue(f_y)))
79 print("slv.getValue({}): {}".format(sum_, slv.getValue(sum_)))
80 print("slv.getValue({}): {}".format(p_0, slv.getValue(p_0)))
81 print("slv.getValue({}): {}".format(p_f_y, slv.getValue(p_f_y)), "\n")
82
83 print("Alternatively, iterate over assertions and call"
84 " slv.getValue(...) on all terms")
85 prefixPrintGetValue(slv, assertions)
86
87 print()
88 print("You can also use nested loops to iterate over terms")
89 for a in assertions:
90 print("term:", a)
91 for t in a:
92 print(" + child: ", t)
93
94 print()
examples/api/smtlib/combination.smt2
1(set-logic QF_UFLIRA)
2(set-option :produce-models true)
3(set-option :incremental true)
4
5(declare-sort U 0)
6
7(declare-const x U)
8(declare-const y U)
9
10(declare-fun f (U) Int)
11(declare-fun p (Int) Bool)
12
13; 0 <= f(x)
14(assert (<= 0 (f x)))
15; 0 <= f(y)
16(assert (<= 0 (f y)))
17; f(x) + f(y) <= 1
18(assert (<= (+ (f x) (f y)) 1))
19; not p(0)
20(assert (not (p 0)))
21; p(f(y))
22(assert (p (f y)))
23
24(echo "Prove x != y is entailed. UNSAT (of negation) == ENTAILED")
25(check-sat-assuming ((not (distinct x y))))
26
27(echo "Call checkSat to show that the assertions are satisfiable")
28(check-sat)
29
30(echo "Call (getValue (...)) on terms of interest")
31(get-value ((f x) (f y) (+ (f x) (f y)) (p 0) (p (f y))))