diff options
Diffstat (limited to 'examples/api/cpp/combination.cpp')
-rw-r--r-- | examples/api/cpp/combination.cpp | 136 |
1 files changed, 136 insertions, 0 deletions
diff --git a/examples/api/cpp/combination.cpp b/examples/api/cpp/combination.cpp new file mode 100644 index 000000000..d47897a7c --- /dev/null +++ b/examples/api/cpp/combination.cpp @@ -0,0 +1,136 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Tim King, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A simple demonstration of the capabilities of cvc5 + * + * A simple demonstration of how to use uninterpreted functions, combining this + * with arithmetic, and extracting a model at the end of a satisfiable query. + * The model is displayed using getValue(). + */ + +#include <cvc5/cvc5.h> + +#include <iostream> + +using namespace std; +using namespace cvc5::api; + +void prefixPrintGetValue(Solver& slv, Term t, int level = 0) +{ + cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl; + + for (const Term& c : t) + { + prefixPrintGetValue(slv, c, level + 1); + } +} + +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "cvc"); // Set the output-language to CVC's + slv.setOption("dag-thresh", "0"); // Disable dagifying the output + slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language + slv.setLogic(string("QF_UFLIRA")); + + // Sorts + Sort u = slv.mkUninterpretedSort("u"); + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort uToInt = slv.mkFunctionSort(u, integer); + Sort intPred = slv.mkFunctionSort(integer, boolean); + + // Variables + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); + + // Functions + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); + + // Constants + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + // Terms + Term f_x = slv.mkTerm(APPLY_UF, f, x); + Term f_y = slv.mkTerm(APPLY_UF, f, y); + Term sum = slv.mkTerm(PLUS, f_x, f_y); + Term p_0 = slv.mkTerm(APPLY_UF, p, zero); + Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); + + // Construct the assertions + Term assertions = slv.mkTerm(AND, + vector<Term>{ + slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x) + slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y) + slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); + slv.assertFormula(assertions); + + cout << "Given the following assertions:" << endl + << assertions << endl << endl; + + cout << "Prove x /= y is entailed. " << endl + << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << endl + << endl; + + cout << "Call checkSat to show that the assertions are satisfiable. " + << endl + << "cvc5: " + << slv.checkSat() << "."<< endl << endl; + + cout << "Call slv.getValue(...) on terms of interest." + << endl; + cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl; + cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl; + cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl; + cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl; + cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y) + << endl << endl; + + cout << "Alternatively, iterate over assertions and call slv.getValue(...) " + << "on all terms." + << endl; + prefixPrintGetValue(slv, assertions); + + cout << endl; + cout << "You can also use nested loops to iterate over terms." << endl; + for (Term::const_iterator it = assertions.begin(); + it != assertions.end(); + ++it) + { + cout << "term: " << *it << endl; + for (Term::const_iterator it2 = (*it).begin(); + it2 != (*it).end(); + ++it2) + { + cout << " + child: " << *it2 << std::endl; + } + } + cout << endl; + cout << "Alternatively, you can also use for-each loops." << endl; + for (const Term& t : assertions) + { + cout << "term: " << t << endl; + for (const Term& c : t) + { + cout << " + child: " << c << endl; + } + } + + return 0; +} |