Theory Combination
examples/api/cpp/combination.cpp
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Mathias Preiner, Tim King
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 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 Solver slv;
40 slv.setOption("produce-models", "true"); // Produce Models
41 slv.setOption("dag-thresh", "0"); // Disable dagifying the output
42 slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
43 slv.setLogic(string("QF_UFLIRA"));
44
45 // Sorts
46 Sort u = slv.mkUninterpretedSort("u");
47 Sort integer = slv.getIntegerSort();
48 Sort boolean = slv.getBooleanSort();
49 Sort uToInt = slv.mkFunctionSort({u}, integer);
50 Sort intPred = slv.mkFunctionSort({integer}, boolean);
51
52 // Variables
53 Term x = slv.mkConst(u, "x");
54 Term y = slv.mkConst(u, "y");
55
56 // Functions
57 Term f = slv.mkConst(uToInt, "f");
58 Term p = slv.mkConst(intPred, "p");
59
60 // Constants
61 Term zero = slv.mkInteger(0);
62 Term one = slv.mkInteger(1);
63
64 // Terms
65 Term f_x = slv.mkTerm(Kind::APPLY_UF, {f, x});
66 Term f_y = slv.mkTerm(Kind::APPLY_UF, {f, y});
67 Term sum = slv.mkTerm(Kind::ADD, {f_x, f_y});
68 Term p_0 = slv.mkTerm(Kind::APPLY_UF, {p, zero});
69 Term p_f_y = slv.mkTerm(Kind::APPLY_UF, {p, f_y});
70
71 // Construct the assertions
72 Term assertions =
73 slv.mkTerm(Kind::AND,
74 {
75 slv.mkTerm(Kind::LEQ, {zero, f_x}), // 0 <= f(x)
76 slv.mkTerm(Kind::LEQ, {zero, f_y}), // 0 <= f(y)
77 slv.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(slv.mkTerm(Kind::EQUAL, {x, y}))
88 << "." << endl
89 << endl;
90
91 cout << "Call checkSat to show that the assertions are satisfiable. "
92 << endl
93 << "cvc5: "
94 << slv.checkSat() << "."<< endl << endl;
95
96 cout << "Call slv.getValue(...) on terms of interest."
97 << endl;
98 cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl;
99 cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl;
100 cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl;
101 cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl;
102 cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y)
103 << endl << endl;
104
105 cout << "Alternatively, iterate over assertions and call slv.getValue(...) "
106 << "on all terms."
107 << endl;
108 prefixPrintGetValue(slv, assertions);
109
110 cout << endl;
111 cout << "You can also use nested loops to iterate over terms." << endl;
112 for (Term::const_iterator it = assertions.begin();
113 it != assertions.end();
114 ++it)
115 {
116 cout << "term: " << *it << endl;
117 for (Term::const_iterator it2 = (*it).begin();
118 it2 != (*it).end();
119 ++it2)
120 {
121 cout << " + child: " << *it2 << std::endl;
122 }
123 }
124 cout << endl;
125 cout << "Alternatively, you can also use for-each loops." << endl;
126 for (const Term& t : assertions)
127 {
128 cout << "term: " << t << endl;
129 for (const Term& c : t)
130 {
131 cout << " + child: " << c << endl;
132 }
133 }
134
135 return 0;
136}
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-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 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 }
130}
examples/api/python/pythonic/combination.py
1from cvc5.pythonic import *
2
3if __name__ == "__main__":
4
5 U = DeclareSort("U")
6 x, y = Consts("x y", U)
7
8 f = Function("f", U, IntSort())
9 p = Function("p", IntSort(), BoolSort())
10
11 assumptions = [f(x) >= 0, f(y) >= 0, f(x) + f(y) <= 1, Not(p(0)), p(f(y))]
12
13 prove(Implies(And(assumptions), x != y))
14
15 s = Solver()
16 s.add(assumptions)
17 assert sat == s.check()
18 m = s.model()
19
20 def print_val(t):
21 print("{}: {}".format(t, m[t]))
22
23 # print the of some terms
24 print_val(f(x))
25 print_val(f(y))
26 print_val(f(x) + f(y))
27 print_val(p(0))
28 print_val(p(f(y)))
29
30 # print value of *all* terms
31 def print_all_subterms(t):
32 print_val(t)
33 for c in t.children():
34 print_all_subterms(c)
35 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-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 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 slv = cvc5.Solver()
29 slv.setOption("produce-models", "true") # Produce Models
30 slv.setOption("dag-thresh", "0") # Disable dagifying the output
31 slv.setOption("output-language", "smt2") # use smt-lib v2 as output language
32 slv.setLogic("QF_UFLIRA")
33
34 # Sorts
35 u = slv.mkUninterpretedSort("u")
36 integer = slv.getIntegerSort()
37 boolean = slv.getBooleanSort()
38 uToInt = slv.mkFunctionSort(u, integer)
39 intPred = slv.mkFunctionSort(integer, boolean)
40
41 # Variables
42 x = slv.mkConst(u, "x")
43 y = slv.mkConst(u, "y")
44
45 # Functions
46 f = slv.mkConst(uToInt, "f")
47 p = slv.mkConst(intPred, "p")
48
49 # Constants
50 zero = slv.mkInteger(0)
51 one = slv.mkInteger(1)
52
53 # Terms
54 f_x = slv.mkTerm(Kind.APPLY_UF, f, x)
55 f_y = slv.mkTerm(Kind.APPLY_UF, f, y)
56 sum_ = slv.mkTerm(Kind.ADD, f_x, f_y)
57 p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero)
58 p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y)
59
60 # Construct the assertions
61 assertions = slv.mkTerm(Kind.AND,
62 slv.mkTerm(Kind.LEQ, zero, f_x), # 0 <= f(x)
63 slv.mkTerm(Kind.LEQ, zero, f_y), # 0 <= f(y)
64 slv.mkTerm(Kind.LEQ, sum_, one), # f(x) + f(y) <= 1
65 p_0.notTerm(), # not p(0)
66 p_f_y # p(f(y))
67 )
68
69 slv.assertFormula(assertions)
70
71 print("Given the following assertions:", assertions, "\n")
72 print("Prove x /= y is entailed.\ncvc5: ",
73 slv.checkSatAssuming(slv.mkTerm(Kind.EQUAL, x, y)), "\n")
74
75 print("Call checkSat to show that the assertions are satisfiable")
76 print("cvc5:", slv.checkSat(), "\n")
77
78 print("Call slv.getValue(...) on terms of interest")
79 print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x)))
80 print("slv.getValue({}): {}".format(f_y, slv.getValue(f_y)))
81 print("slv.getValue({}): {}".format(sum_, slv.getValue(sum_)))
82 print("slv.getValue({}): {}".format(p_0, slv.getValue(p_0)))
83 print("slv.getValue({}): {}".format(p_f_y, slv.getValue(p_f_y)), "\n")
84
85 print("Alternatively, iterate over assertions and call"
86 " slv.getValue(...) on all terms")
87 prefixPrintGetValue(slv, assertions)
88
89 print()
90 print("You can also use nested loops to iterate over terms")
91 for a in assertions:
92 print("term:", a)
93 for t in a:
94 print(" + child: ", t)
95
96 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))))