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