diff options
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors-new.cpp | 130 | ||||
-rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 96 | ||||
-rw-r--r-- | examples/api/combination-new.cpp | 139 | ||||
-rw-r--r-- | examples/api/datatypes-new.cpp | 165 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 56 | ||||
-rw-r--r-- | examples/api/helloworld-new.cpp | 30 | ||||
-rw-r--r-- | examples/api/linear_arith-new.cpp | 85 | ||||
-rw-r--r-- | examples/api/sets-new.cpp | 96 | ||||
-rw-r--r-- | examples/api/strings-new.cpp | 96 |
9 files changed, 893 insertions, 0 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp new file mode 100644 index 000000000..596d0b515 --- /dev/null +++ b/examples/api/bitvectors-new.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file bitvectors.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Liana Hadarean, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector solver. + ** + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + + Solver slv; + slv.setLogic("QF_BV"); // Set the logic + + // The following example has been adapted from the book A Hacker's Delight by + // Henry S. Warren. + // + // Given a variable x that can only have two values, a or b. We want to + // assign to x a value other than the current one. The straightforward code + // to do that is: + // + //(0) if (x == a ) x = b; + // else x = a; + // + // Two more efficient yet equivalent methods are: + // + //(1) x = a ⊕ b ⊕ x; + // + //(2) x = a + b - x; + // + // We will use CVC4 to prove that the three pieces of code above are all + // equivalent by encoding the problem in the bit-vector theory. + + // Creating a bit-vector type of width 32 + Sort bitvector32 = slv.mkBitVectorSort(32); + + std::cout << "bitvector32 " << bitvector32 << std::endl; + // Variables + Term x = slv.mkVar("x", bitvector32); + std::cout << "bitvector32 " << bitvector32 << std::endl; + Term a = slv.mkVar("a", bitvector32); + Term b = slv.mkVar("b", bitvector32); + + // First encode the assumption that x must be equal to a or b + Term x_eq_a = slv.mkTerm(EQUAL, x, a); + Term x_eq_b = slv.mkTerm(EQUAL, x, b); + Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b); + + // Assert the assumption + slv.assertFormula(assumption); + + // Introduce a new variable for the new value of x after assignment. + Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0) + Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + + // Encoding code (0) + // new_x = x == a ? b : a; + Term ite = slv.mkTerm(ITE, x_eq_a, b, a); + Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); + + // Assert the encoding of code (0) + cout << "Asserting " << assignment0 << " to CVC4 " << endl; + slv.assertFormula(assignment0); + cout << "Pushing a new context." << endl; + slv.push(); + + // Encoding code (1) + // new_x_ = a xor b xor x + Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); + Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); + + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment1 << " to CVC4 " << endl; + slv.assertFormula(assignment1); + Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); + + cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + cout << " Popping context. " << endl; + slv.pop(); + + // Encoding code (2) + // new_x_ = a + b - x + Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b); + Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); + Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); + + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment2 << " to CVC4 " << endl; + slv.assertFormula(assignment2); + + cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + + Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); + std::vector<Term> v{new_x_eq_new_x_, x_neq_x}; + cout << " Check Validity Assuming: " << v << endl; + cout << " Expect invalid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(v) << endl; + + // Assert that a is odd + OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); + cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; + Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); + cout << "Assert " << a_odd << endl; + cout << "Check satisfiability." << endl; + slv.assertFormula(a_odd); + cout << " Expect sat. " << endl; + cout << " CVC4: " << slv.checkSat() << endl; + return 0; +} diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp new file mode 100644 index 000000000..3d4e6bca0 --- /dev/null +++ b/examples/api/bitvectors_and_arrays-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file bitvectors_and_arrays.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Aina Niemetz, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector and array solvers. + ** + **/ + +#include <iostream> +#include <cmath> +// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "smtlib"); // output-language + slv.setLogic("QF_AUFBV"); // Set the logic + + // Consider the following code (where size is some previously defined constant): + // + // + // Assert (current_array[0] > 0); + // for (unsigned i = 1; i < k; ++i) { + // current_array[i] = 2 * current_array[i - 1]; + // Assert (current_array[i-1] < current_array[i]); + // } + // + // We want to check whether the assertion in the body of the for loop holds + // throughout the loop. + + // Setting up the problem parameters + unsigned k = 4; // number of unrollings (should be a power of 2) + unsigned index_size = log2(k); // size of the index + + + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); + + // Variables + Term current_array = slv.mkVar("current_array", arraySort); + + // Making a bit-vector constant + Term zero = slv.mkBitVector(index_size, 0u); + + // Asserting that current_array[0] > 0 + Term current_array0 = slv.mkTerm(SELECT, current_array, zero); + Term current_array0_gt_0 = slv.mkTerm( + BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u)); + slv.assertFormula(current_array0_gt_0); + + // Building the assertions in the loop unrolling + Term index = slv.mkBitVector(index_size, 0u); + Term old_current = slv.mkTerm(SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2u); + + std::vector<Term> assertions; + for (unsigned i = 1; i < k; ++i) { + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); + // current[i] = 2 * current[i-1] + current_array = slv.mkTerm(STORE, current_array, index, new_current); + // current[i-1] < current [i] + Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); + assertions.push_back(current_slt_new_current); + + old_current = slv.mkTerm(SELECT, current_array, index); + } + + Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); + + cout << "Asserting " << query << " to CVC4 " << endl; + slv.assertFormula(query); + cout << "Expect sat. " << endl; + cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; + + // Getting the model + cout << "The satisfying model is: " << endl; + cout << " current_array = " << slv.getValue(current_array) << endl; + cout << " current_array[0] = " << slv.getValue(current_array0) << endl; + return 0; +} diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp new file mode 100644 index 000000000..2956d76e6 --- /dev/null +++ b/examples/api/combination-new.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file combination.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the capabilities of CVC4 + ** + ** 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 <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::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", "cvc4"); // Set the output-language to CVC's + slv.setOption("default-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.mkVar("x", u); + Term y = slv.mkVar("y", u); + + // Functions + Term f = slv.mkVar("f", uToInt); + Term p = slv.mkVar("p", intPred); + + // 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 valid. " << endl + << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y)) + << "." << endl << endl; + + cout << "Call checkSat to show that the assertions are satisfiable. " + << endl + << "CVC4: " + << 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 << endl << "Alternatively, print the model." << endl << endl; + + slv.printModel(cout); + + 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; +} diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp new file mode 100644 index 000000000..9ec679f8e --- /dev/null +++ b/examples/api/datatypes-new.cpp @@ -0,0 +1,165 @@ +/********************* */ +/*! \file datatypes.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief An example of using inductive datatypes in CVC4 + ** + ** An example of using inductive datatypes in CVC4. + **/ + +#include <iostream> +//#include <cvc4/cvc4.h> // To follow the wiki + +#include "api/cvc4cpp.h" +using namespace CVC4::api; + +int main() +{ + Solver slv; + // This example builds a simple "cons list" of integers, with + // two constructors, "cons" and "nil." + + // Building a datatype consists of two steps. + // First, the datatype is specified. + // Second, it is "resolved" to an actual sort, at which point function + // symbols are assigned to its constructors, selectors, and testers. + + DatatypeDecl consListSpec("list"); // give the datatype a name + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", slv.getIntegerSort()); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + consListSpec.addConstructor(nil); + + std::cout << "spec is:" << std::endl + << consListSpec << std::endl; + + // Keep in mind that "DatatypeDecl" is the specification class for + // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + // Now that our Datatype is fully specified, we can get a Sort for it. + // This step resolves the "SelfSort" reference and creates + // symbols for all the constructors, etc. + + Sort consListSort = slv.mkDatatypeSort(consListSpec); + + // Now our old "consListSpec" is useless--the relevant information + // has been copied out, so we can throw that spec away. We can get + // the complete spec for the datatype from the DatatypeSort, and + // this Datatype object has constructor symbols (and others) filled in. + + Datatype consList = consListSort.getDatatype(); + + // t = cons 0 nil + // + // Here, consList["cons"] gives you the DatatypeConstructor. To get + // the constructor symbol for application, use .getConstructor("cons"), + // which is equivalent to consList["cons"].getConstructor(). Note that + // "nil" is a constructor too, so it needs to be applied with + // APPLY_CONSTRUCTOR, even though it has no arguments. + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkInteger(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + + std::cout << "t is " << t << std::endl + << "sort of cons is " + << consList.getConstructorTerm("cons").getSort() << std::endl + << "sort of nil is " << consList.getConstructorTerm("nil").getSort() + << std::endl; + + // t2 = head(cons 0 nil), and of course this can be evaluated + // + // Here we first get the DatatypeConstructor for cons (with + // consList["cons"]) in order to get the "head" selector symbol + // to apply. + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); + + std::cout << "t2 is " << t2 << std::endl + << "simplify(t2) is " << slv.simplify(t2) + << std::endl << std::endl; + + // You can also iterate over a Datatype to get all its constructors, + // and over a DatatypeConstructor to get all its "args" (selectors) + for (Datatype::const_iterator i = consList.begin(); + i != consList.end(); + ++i) + { + std::cout << "ctor: " << *i << std::endl; + for (DatatypeConstructor::const_iterator j = (*i).begin(); + j != (*i).end(); + ++j) + { + std::cout << " + arg: " << *j << std::endl; + } + } + std::cout << std::endl; + + // Alternatively, you can use for each loops. + for (const auto& c : consList) + { + std::cout << "ctor: " << c << std::endl; + for (const auto& s : c) + { + std::cout << " + arg: " << s << std::endl; + } + } + std::cout << std::endl; + + // You can also define parameterized datatypes. + // This example builds a simple parameterized list of sort T, with one + // constructor "cons". + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name + DatatypeConstructorDecl paramCons("cons"); + DatatypeSelectorDecl paramHead("head", sort); + DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort()); + paramCons.addSelector(paramHead); + paramCons.addSelector(paramTail); + paramConsListSpec.addConstructor(paramCons); + + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = + paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); + + Datatype paramConsList = paramConsListSort.getDatatype(); + + std::cout << "parameterized datatype sort is " << std::endl; + for (const DatatypeConstructor& ctor : paramConsList) + { + std::cout << "ctor: " << ctor << std::endl; + for (const DatatypeSelector& stor : ctor) + { + std::cout << " + arg: " << stor << std::endl; + } + } + + Term a = slv.declareFun("a", paramConsIntListSort); + std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; + + Term head_a = slv.mkTerm( + APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() + << std::endl + << "sort of cons is " + << paramConsList.getConstructorTerm("cons").getSort() << std::endl + << std::endl; + Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50)); + std::cout << "Assert " << assertion << std::endl; + slv.assertFormula(assertion); + std::cout << "Expect sat." << std::endl; + std::cout << "CVC4: " << slv.checkSat() << std::endl; + + return 0; +} diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp new file mode 100644 index 000000000..8d31c1b12 --- /dev/null +++ b/examples/api/extract-new.cpp @@ -0,0 +1,56 @@ +/********************* */ +/*! \file extract.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector solver. + ** + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setLogic("QF_BV"); // Set the logic + + Sort bitvector32 = slv.mkBitVectorSort(32); + + Term x = slv.mkVar("a", bitvector32); + + OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); + + OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); + + OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); + + OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); + + Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); + cout << " Asserting: " << eq << endl; + slv.assertFormula(eq); + + Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); + cout << " Check validity assuming: " << eq2 << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl; + + return 0; +} diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp new file mode 100644 index 000000000..7957741e5 --- /dev/null +++ b/examples/api/helloworld-new.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file helloworld.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A very simple CVC4 example + ** + ** A very simple CVC4 tutorial example. + **/ + +#include <iostream> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort()); + std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld) + << std::endl; + return 0; +} diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp new file mode 100644 index 000000000..ef8faade9 --- /dev/null +++ b/examples/api/linear_arith-new.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file linear_arith.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 + ** + ** A simple demonstration of the linear arithmetic solving capabilities and + ** the push pop of CVC4. This also gives an example option. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setLogic("QF_LIRA"); // Set the logic + + // Prove that if given x (Integer) and y (Real) then + // the maximum value of y - x is 2/3 + + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); + + // Variables + Term x = slv.mkVar("x", integer); + Term y = slv.mkVar("y", real); + + // Constants + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); + Term two_thirds = slv.mkReal(2, 3); + + // Terms + Term three_y = slv.mkTerm(MULT, three, y); + Term diff = slv.mkTerm(MINUS, y, x); + + // Formulas + Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); + Term x_leq_y = slv.mkTerm(LEQ, x, y); + Term neg2_lt_x = slv.mkTerm(LT, neg2, x); + + Term assertions = + slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); + + cout << "Given the assertions " << assertions << endl; + slv.assertFormula(assertions); + + + slv.push(); + Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); + cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " + << slv.checkValidAssuming(diff_leq_two_thirds) << endl; + slv.pop(); + + cout << endl; + + slv.push(); + Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); + slv.assertFormula(diff_is_two_thirds); + cout << "Show that the assertions are consistent with " << endl; + cout << diff_is_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report SAT." << endl; + cout << "Result from CVC4 is: " << slv.checkSat() << endl; + slv.pop(); + + cout << "Thus the maximum value of (y - x) is 2/3."<< endl; + + return 0; +} diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp new file mode 100644 index 000000000..be35bcc21 --- /dev/null +++ b/examples/api/sets-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file sets.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief Reasoning about sets with CVC4. + ** + ** A simple demonstration of reasoning about sets with CVC4. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS"); + + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); + + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); + + // Verify union distributions over intersection + // (A union B) intersection C = (A intersection C) union (B intersection C) + { + Term A = slv.mkVar("A", set); + Term B = slv.mkVar("B", set); + Term C = slv.mkVar("C", set); + + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Verify emptset is a subset of any set + { + Term A = slv.mkVar("A", set); + Term emptyset = slv.mkEmptySet(set); + + Term theorem = slv.mkTerm(SUBSET, emptyset, A); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Find me an element in {1, 2} intersection {2, 3}, if there is one. + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + + Term x = slv.mkVar("x", integer); + + Term e = slv.mkTerm(MEMBER, x, intersection); + + Result result = slv.checkSatAssuming(e); + cout << "CVC4 reports: " << e << " is " << result << "." << endl; + + if (result.isSat()) + { + cout << "For instance, " << slv.getValue(x) << " is a member." << endl; + } + } +} diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp new file mode 100644 index 000000000..2010c6909 --- /dev/null +++ b/examples/api/strings-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file strings.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Paul Meng, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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.\endverbatim + ** + ** \brief Reasoning about strings with CVC4 via C++ API. + ** + ** A simple demonstration of reasoning about strings with CVC4 via C++ API. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // Set the logic + slv.setLogic("S"); + // Produce models + slv.setOption("produce-models", "true"); + // The option strings-exp is needed + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); + + // String type + Sort string = slv.getStringSort(); + + // std::string + std::string str_ab("ab"); + // String constants + Term ab = slv.mkString(str_ab); + Term abc = slv.mkString("abc"); + // String variables + Term x = slv.mkVar("x", string); + Term y = slv.mkVar("y", string); + Term z = slv.mkVar("z", string); + + // String concatenation: x.ab.y + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); + + // Length of y: |y| + Term leny = slv.mkTerm(STRING_LENGTH, y); + // |y| >= 0 + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); + + // Regular expression: (ab[c-e]*f)|g|h + Term r = slv.mkTerm(REGEXP_UNION, + slv.mkTerm(REGEXP_CONCAT, + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")), + slv.mkTerm(REGEXP_STAR, + slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); + + // String variables + Term s1 = slv.mkVar("s1", string); + Term s2 = slv.mkVar("s2", string); + // String concatenation: s1.s2 + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); + + // s1.s2 in (ab[c-e]*f)|g|h + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); + + // Make a query + Term q = slv.mkTerm(AND, + formula1, + formula2, + formula3); + + // check sat + Result result = slv.checkSatAssuming(q); + std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + + if(result.isSat()) + { + std::cout << " x = " << slv.getValue(x) << std::endl; + std::cout << " s1.s2 = " << slv.getValue(s) << std::endl; + } +} |