1 /********************* */
2 /*! \file combination-new.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Makai Mann
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief A simple demonstration of the capabilities of CVC4
13 **
14 ** A simple demonstration of how to use uninterpreted functions, combining this
15 ** with arithmetic, and extracting a model at the end of a satisfiable query.
16 ** The model is displayed using getValue().
17 **/
18
19 #include <iostream>
20
21 // #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
22 #include "api/cvc4cpp.h"
23
24 using namespace std;
25 using namespace CVC4::api;
26
prefixPrintGetValue(Solver & slv,Term t,int level=0)27 void 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
main()37 int main()
38 {
39 Solver slv;
40 slv.setOption("produce-models", "true"); // Produce Models
41 slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's
42 slv.setOption("default-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 = slv.mkUninterpretedSort("u");
48 Sort integer = slv.getIntegerSort();
49 Sort boolean = slv.getBooleanSort();
50 Sort uToInt = slv.mkFunctionSort(u, integer);
51 Sort intPred = slv.mkFunctionSort(integer, boolean);
52
53 // Variables
54 Term x = slv.mkVar(u, "x");
55 Term y = slv.mkVar(u, "y");
56
57 // Functions
58 Term f = slv.mkVar(uToInt, "f");
59 Term p = slv.mkVar(intPred, "p");
60
61 // Constants
62 Term zero = slv.mkReal(0);
63 Term one = slv.mkReal(1);
64
65 // Terms
66 Term f_x = slv.mkTerm(APPLY_UF, f, x);
67 Term f_y = slv.mkTerm(APPLY_UF, f, y);
68 Term sum = slv.mkTerm(PLUS, f_x, f_y);
69 Term p_0 = slv.mkTerm(APPLY_UF, p, zero);
70 Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y);
71
72 // Construct the assertions
73 Term assertions = slv.mkTerm(AND,
74 vector<Term>{
75 slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
76 slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
77 slv.mkTerm(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 valid. " << endl
87 << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y))
88 << "." << endl << endl;
89
90 cout << "Call checkSat to show that the assertions are satisfiable. "
91 << endl
92 << "CVC4: "
93 << slv.checkSat() << "."<< endl << 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 << endl << "Alternatively, print the model." << endl << endl;
110
111 slv.printModel(cout);
112
113 cout << endl;
114 cout << "You can also use nested loops to iterate over terms." << endl;
115 for (Term::const_iterator it = assertions.begin();
116 it != assertions.end();
117 ++it)
118 {
119 cout << "term: " << *it << endl;
120 for (Term::const_iterator it2 = (*it).begin();
121 it2 != (*it).end();
122 ++it2)
123 {
124 cout << " + child: " << *it2 << std::endl;
125 }
126 }
127 cout << endl;
128 cout << "Alternatively, you can also use for-each loops." << endl;
129 for (const Term& t : assertions)
130 {
131 cout << "term: " << t << endl;
132 for (const Term& c : t)
133 {
134 cout << " + child: " << c << endl;
135 }
136 }
137
138 return 0;
139 }
140