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.setOption("output-language", "smt2"); // use smt-lib v2 as output language
44 slv.setLogic(string("QF_UFLIRA"));
45
46 // Sorts
47 Sort u = tm.mkUninterpretedSort("u");
48 Sort integer = tm.getIntegerSort();
49 Sort boolean = tm.getBooleanSort();
50 Sort uToInt = tm.mkFunctionSort({u}, integer);
51 Sort intPred = tm.mkFunctionSort({integer}, boolean);
52
53 // Variables
54 Term x = tm.mkConst(u, "x");
55 Term y = tm.mkConst(u, "y");
56
57 // Functions
58 Term f = tm.mkConst(uToInt, "f");
59 Term p = tm.mkConst(intPred, "p");
60
61 // Constants
62 Term zero = tm.mkInteger(0);
63 Term one = tm.mkInteger(1);
64
65 // Terms
66 Term f_x = tm.mkTerm(Kind::APPLY_UF, {f, x});
67 Term f_y = tm.mkTerm(Kind::APPLY_UF, {f, y});
68 Term sum = tm.mkTerm(Kind::ADD, {f_x, f_y});
69 Term p_0 = tm.mkTerm(Kind::APPLY_UF, {p, zero});
70 Term p_f_y = tm.mkTerm(Kind::APPLY_UF, {p, f_y});
71
72 // Construct the assertions
73 Term assertions =
74 tm.mkTerm(Kind::AND,
75 {
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 cout << "Given the following assertions:" << endl
85 << assertions << endl << endl;
86
87 cout << "Prove x /= y is entailed. " << endl
88 << "cvc5: " << slv.checkSatAssuming(tm.mkTerm(Kind::EQUAL, {x, y}))
89 << "." << endl
90 << endl;
91
92 cout << "Call checkSat to show that the assertions are satisfiable. "
93 << endl
94 << "cvc5: "
95 << slv.checkSat() << "."<< endl << endl;
96
97 cout << "Call slv.getValue(...) on terms of interest."
98 << endl;
99 cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl;
100 cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl;
101 cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl;
102 cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl;
103 cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y)
104 << endl << endl;
105
106 cout << "Alternatively, iterate over assertions and call slv.getValue(...) "
107 << "on all terms."
108 << endl;
109 prefixPrintGetValue(slv, assertions);
110
111 cout << endl;
112 cout << "You can also use nested loops to iterate over terms." << endl;
113 for (Term::const_iterator it = assertions.begin();
114 it != assertions.end();
115 ++it)
116 {
117 cout << "term: " << *it << endl;
118 for (Term::const_iterator it2 = (*it).begin();
119 it2 != (*it).end();
120 ++it2)
121 {
122 cout << " + child: " << *it2 << std::endl;
123 }
124 }
125 cout << endl;
126 cout << "Alternatively, you can also use for-each loops." << endl;
127 for (const Term& t : assertions)
128 {
129 cout << "term: " << t << endl;
130 for (const Term& c : t)
131 {
132 cout << " + child: " << c << endl;
133 }
134 }
135
136 return 0;
137}
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))))