diff options
| -rw-r--r-- | examples/api/CMakeLists.txt | 9 | ||||
| -rw-r--r-- | examples/api/bitvectors-new.cpp | 127 | ||||
| -rw-r--r-- | examples/api/bitvectors.cpp | 93 | ||||
| -rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 96 | ||||
| -rw-r--r-- | examples/api/bitvectors_and_arrays.cpp | 65 | ||||
| -rw-r--r-- | examples/api/combination-new.cpp | 139 | ||||
| -rw-r--r-- | examples/api/combination.cpp | 160 | ||||
| -rw-r--r-- | examples/api/datatypes-new.cpp | 179 | ||||
| -rw-r--r-- | examples/api/datatypes.cpp | 187 | ||||
| -rw-r--r-- | examples/api/extract-new.cpp | 55 | ||||
| -rw-r--r-- | examples/api/extract.cpp | 46 | ||||
| -rw-r--r-- | examples/api/helloworld-new.cpp | 30 | ||||
| -rw-r--r-- | examples/api/helloworld.cpp | 17 | ||||
| -rw-r--r-- | examples/api/linear_arith-new.cpp | 84 | ||||
| -rw-r--r-- | examples/api/linear_arith.cpp | 68 | ||||
| -rw-r--r-- | examples/api/sets-new.cpp | 95 | ||||
| -rw-r--r-- | examples/api/sets.cpp | 82 | ||||
| -rw-r--r-- | examples/api/strings-new.cpp | 95 | ||||
| -rw-r--r-- | examples/api/strings.cpp | 86 |
19 files changed, 432 insertions, 1281 deletions
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 3ced5681c..6421a3263 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -1,22 +1,13 @@ set(CVC4_EXAMPLES_API bitvectors - bitvectors-new bitvectors_and_arrays - bitvectors_and_arrays-new combination - combination-new datatypes - datatypes-new extract - extract-new helloworld - helloworld-new linear_arith - linear_arith-new sets - sets-new strings - strings-new sygus-fun sygus-grammar sygus-inv diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp deleted file mode 100644 index e5b99d783..000000000 --- a/examples/api/bitvectors-new.cpp +++ /dev/null @@ -1,127 +0,0 @@ -/********************* */ -/*! \file bitvectors-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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); - - // Variables - Term x = slv.mkConst(bitvector32, "x"); - Term a = slv.mkConst(bitvector32, "a"); - Term b = slv.mkConst(bitvector32, "b"); - - // 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.mkConst(bitvector32, "new_x"); // x after executing code (0) - Term new_x_ = - slv.mkConst(bitvector32, "new_x_"); // 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 entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(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 entailment assuming: " << new_x_eq_new_x_ << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(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 entailment assuming: " << v << endl; - cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(v) << endl; - - // Assert that a is odd - Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 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.cpp b/examples/api/bitvectors.cpp index ea0cda3e9..ab1e8ce07 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -2,7 +2,7 @@ /*! \file bitvectors.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Aina Niemetz, Morgan Deters + ** Aina Niemetz, Makai Mann ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,15 +16,15 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_BV"); // Set the logic +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. @@ -46,81 +46,82 @@ int main() { // equivalent by encoding the problem in the bit-vector theory. // Creating a bit-vector type of width 32 - Type bitvector32 = em.mkBitVectorType(32); + Sort bitvector32 = slv.mkBitVectorSort(32); // Variables - Expr x = em.mkVar("x", bitvector32); - Expr a = em.mkVar("a", bitvector32); - Expr b = em.mkVar("b", bitvector32); + Term x = slv.mkConst(bitvector32, "x"); + Term a = slv.mkConst(bitvector32, "a"); + Term b = slv.mkConst(bitvector32, "b"); // First encode the assumption that x must be equal to a or b - Expr x_eq_a = em.mkExpr(kind::EQUAL, x, a); - Expr x_eq_b = em.mkExpr(kind::EQUAL, x, b); - Expr assumption = em.mkExpr(kind::OR, x_eq_a, x_eq_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 - smt.assertFormula(assumption); + slv.assertFormula(assumption); // Introduce a new variable for the new value of x after assignment. - Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) - Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0) + Term new_x_ = + slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; - Expr ite = em.mkExpr(kind::ITE, x_eq_a, b, a); - Expr assignment0 = em.mkExpr(kind::EQUAL, new_x, ite); + 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; - smt.assertFormula(assignment0); + slv.assertFormula(assignment0); cout << "Pushing a new context." << endl; - smt.push(); + slv.push(); // Encoding code (1) // new_x_ = a xor b xor x - Expr a_xor_b_xor_x = em.mkExpr(kind::BITVECTOR_XOR, a, b, x); - Expr assignment1 = em.mkExpr(kind::EQUAL, 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; - smt.assertFormula(assignment1); - Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_); + slv.assertFormula(assignment1); + Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); - cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect entailed. " << endl; - cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; - smt.pop(); + slv.pop(); // Encoding code (2) // new_x_ = a + b - x - Expr a_plus_b = em.mkExpr(kind::BITVECTOR_PLUS, a, b); - Expr a_plus_b_minus_x = em.mkExpr(kind::BITVECTOR_SUB, a_plus_b, x); - Expr assignment2 = em.mkExpr(kind::EQUAL, new_x_, a_plus_b_minus_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; - smt.assertFormula(assignment2); + slv.assertFormula(assignment2); - cout << " Querying: " << new_x_eq_new_x_ << endl; + cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << smt.checkEntailed(new_x_eq_new_x_) << endl; + cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; - Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr(); - std::vector<Expr> v{new_x_eq_new_x_, x_neq_x}; - cout << " Querying: " << v << 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 entailment assuming: " << v << endl; cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << smt.checkEntailed(v) << endl; + cout << " CVC4: " << slv.checkEntailed(v) << endl; - // Assert that a is odd - Expr extract_op = em.mkConst(BitVectorExtract(0, 0)); - Expr lsb_of_a = em.mkExpr(extract_op, a); - cout << "Type of " << lsb_of_a << " is " << lsb_of_a.getType() << endl; - Expr a_odd = em.mkExpr(kind::EQUAL, lsb_of_a, em.mkConst(BitVector(1u, 1u))); + // Assert that a is odd + Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 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; - smt.assertFormula(a_odd); + slv.assertFormula(a_odd); cout << " Expect sat. " << endl; - cout << " CVC4: " << smt.checkSat() << 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 deleted file mode 100644 index 34356f565..000000000 --- a/examples/api/bitvectors_and_arrays-new.cpp +++ /dev/null @@ -1,96 +0,0 @@ -/********************* */ -/*! \file bitvectors_and_arrays-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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.mkConst(arraySort, "current_array"); - - // 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/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index a701e80df..2c98d4f8a 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -2,7 +2,7 @@ /*! \file bitvectors_and_arrays.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -17,17 +17,17 @@ #include <iostream> #include <cmath> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setOption("produce-models", true); // Produce Models - smt.setOption("output-language", "smtlib"); // output-language - smt.setLogic("QF_AUFBV"); // Set the logic +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): // @@ -46,50 +46,51 @@ int main() { unsigned index_size = log2(k); // size of the index - // Types - Type elementType = em.mkBitVectorType(32); - Type indexType = em.mkBitVectorType(index_size); - Type arrayType = em.mkArrayType(indexType, elementType); + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); // Variables - Expr current_array = em.mkVar("current_array", arrayType); + Term current_array = slv.mkConst(arraySort, "current_array"); // Making a bit-vector constant - Expr zero = em.mkConst(BitVector(index_size, 0u)); + Term zero = slv.mkBitVector(index_size, 0u); // Asserting that current_array[0] > 0 - Expr current_array0 = em.mkExpr(kind::SELECT, current_array, zero); - Expr current_array0_gt_0 = em.mkExpr(kind::BITVECTOR_SGT, current_array0, em.mkConst(BitVector(32, 0u))); - smt.assertFormula(current_array0_gt_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 - Expr index = em.mkConst(BitVector(index_size, 0u)); - Expr old_current = em.mkExpr(kind::SELECT, current_array, index); - Expr two = em.mkConst(BitVector(32, 2u)); + Term index = slv.mkBitVector(index_size, 0u); + Term old_current = slv.mkTerm(SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2u); - std::vector<Expr> assertions; + std::vector<Term> assertions; for (unsigned i = 1; i < k; ++i) { - index = em.mkConst(BitVector(index_size, Integer(i))); - Expr new_current = em.mkExpr(kind::BITVECTOR_MULT, two, old_current); + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); // current[i] = 2 * current[i-1] - current_array = em.mkExpr(kind::STORE, current_array, index, new_current); + current_array = slv.mkTerm(STORE, current_array, index, new_current); // current[i-1] < current [i] - Expr current_slt_new_current = em.mkExpr(kind::BITVECTOR_SLT, old_current, new_current); + Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); assertions.push_back(current_slt_new_current); - old_current = em.mkExpr(kind::SELECT, current_array, index); + old_current = slv.mkTerm(SELECT, current_array, index); } - Expr query = em.mkExpr(kind::NOT, em.mkExpr(kind::AND, assertions)); + Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); cout << "Asserting " << query << " to CVC4 " << endl; - smt.assertFormula(query); + slv.assertFormula(query); cout << "Expect sat. " << endl; - cout << "CVC4: " << smt.checkSat(em.mkConst(true)) << endl; + cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; // Getting the model cout << "The satisfying model is: " << endl; - cout << " current_array = " << smt.getValue(current_array) << endl; - cout << " current_array[0] = " << smt.getValue(current_array0) << 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 deleted file mode 100644 index ab3d80d10..000000000 --- a/examples/api/combination-new.cpp +++ /dev/null @@ -1,139 +0,0 @@ -/********************* */ -/*! \file combination-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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("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.mkReal(0); - Term one = slv.mkReal(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 - << "CVC4: " << slv.checkEntailed(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/combination.cpp b/examples/api/combination.cpp index 4e29b5a8d..817ed6f65 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -2,7 +2,7 @@ /*! \file combination.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz, Makai Mann + ** Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -18,86 +18,122 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -void prefixPrintGetValue(SmtEngine& smt, Expr e, int level = 0){ - for(int i = 0; i < level; ++i){ cout << '-'; } - cout << "smt.getValue(" << e << ") -> " << smt.getValue(e) << endl; +void prefixPrintGetValue(Solver& slv, Term t, int level = 0) +{ + cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl; - if(e.hasOperator() && e.getOperator().getKind() != kind::BUILTIN){ - prefixPrintGetValue(smt, e.getOperator(), level + 1); - } - - for(Expr::const_iterator term_i = e.begin(), term_end = e.end(); - term_i != term_end; ++term_i) + for (const Term& c : t) { - Expr curr = *term_i; - prefixPrintGetValue(smt, curr, level + 1); + prefixPrintGetValue(slv, c, level + 1); } } - -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setOption("produce-models", true); // Produce Models - smt.setOption("output-language", "cvc4"); // Set the output-language to CVC's - smt.setOption("dag-thresh", 0); //Disable dagifying the output - smt.setLogic(string("QF_UFLIRA")); +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("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 - SortType u = em.mkSort("u"); - Type integer = em.integerType(); - Type boolean = em.booleanType(); - Type uToInt = em.mkFunctionType(u, integer); - Type intPred = em.mkFunctionType(integer, boolean); + 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 - Expr x = em.mkVar("x", u); - Expr y = em.mkVar("y", u); + Term x = slv.mkConst(u, "x"); + Term y = slv.mkConst(u, "y"); // Functions - Expr f = em.mkVar("f", uToInt); - Expr p = em.mkVar("p", intPred); + Term f = slv.mkConst(uToInt, "f"); + Term p = slv.mkConst(intPred, "p"); // Constants - Expr zero = em.mkConst(Rational(0)); - Expr one = em.mkConst(Rational(1)); + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); // Terms - Expr f_x = em.mkExpr(kind::APPLY_UF, f, x); - Expr f_y = em.mkExpr(kind::APPLY_UF, f, y); - Expr sum = em.mkExpr(kind::PLUS, f_x, f_y); - Expr p_0 = em.mkExpr(kind::APPLY_UF, p, zero); - Expr p_f_y = em.mkExpr(kind::APPLY_UF, p, f_y); - - // Construct the assumptions - Expr assumptions = - em.mkExpr(kind::AND, - em.mkExpr(kind::LEQ, zero, f_x), // 0 <= f(x) - em.mkExpr(kind::LEQ, zero, f_y), // 0 <= f(y) - em.mkExpr(kind::LEQ, sum, one), // f(x) + f(y) <= 1 - p_0.notExpr(), // not p(0) - p_f_y); // p(f(y)) - smt.assertFormula(assumptions); - - cout << "Given the following assumptions:" << endl - << assumptions << endl - << "Prove x /= y is entailed. " - << "CVC4 says: " << smt.checkEntailed(em.mkExpr(kind::DISTINCT, x, y)) - << "." << endl; - - cout << "Now we call checksat on a trivial query to show that" << endl - << "the assumptions are satisfiable: " - << smt.checkSat(em.mkConst(true)) << "."<< endl; - - cout << "Finally, after a SAT call, we recursively call smt.getValue(...) on " - << "all of the assumptions to see what the satisfying model looks like." + 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 + << "CVC4: " << slv.checkEntailed(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(smt, assumptions); + 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 deleted file mode 100644 index d8061318a..000000000 --- a/examples/api/datatypes-new.cpp +++ /dev/null @@ -1,179 +0,0 @@ -/********************* */ -/*! \file datatypes-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/api/cvc4cpp.h> - -using namespace CVC4::api; - -void test(Solver& slv, Sort& consListSort) -{ - // 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. - - const 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.mkReal(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 = - slv.mkDatatypeDecl("paramlist", - sort); // give the datatype a name - DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); - DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); - paramCons.addSelector("head", sort); - paramCons.addSelectorSelf("tail"); - paramConsListSpec.addConstructor(paramCons); - paramConsListSpec.addConstructor(paramNil); - - Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); - Sort paramConsIntListSort = - paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - - const 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.mkConst(paramConsIntListSort, "a"); - 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.mkReal(50)); - std::cout << "Assert " << assertion << std::endl; - slv.assertFormula(assertion); - std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << slv.checkSat() << std::endl; -} - -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 = - slv.mkDatatypeDecl("list"); // give the datatype a name - DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", slv.getIntegerSort()); - cons.addSelectorSelf("tail"); - consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("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); - - test(slv, consListSort); - - std::cout << std::endl - << ">>> Alternatively, use declareDatatype" << std::endl; - std::cout << std::endl; - - DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); - cons2.addSelector("head", slv.getIntegerSort()); - cons2.addSelectorSelf("tail"); - DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); - std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; - Sort consListSort2 = slv.declareDatatype("list2", ctors); - test(slv, consListSort2); - - return 0; -} diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index eb156c54c..dd2c2695d 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -2,7 +2,7 @@ /*! \file datatypes.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Makai Mann ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,135 +16,164 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; - -int main() { - ExprManager em; - SmtEngine smt(&em); - - // 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"---at which point function - // symbols are assigned to its constructors, selectors, and testers. - - Datatype consListSpec(&em, "list"); // give the datatype a name - DatatypeConstructor cons("cons"); - cons.addArg("head", em.integerType()); - cons.addArg("tail", DatatypeSelfType()); // a list - consListSpec.addConstructor(cons); - DatatypeConstructor nil("nil"); - consListSpec.addConstructor(nil); - - std::cout << "spec is:" << std::endl - << consListSpec << std::endl; - - // Keep in mind that "Datatype" is the specification class for - // datatypes---"Datatype" is not itself a CVC4 Type. Now that - // our Datatype is fully specified, we can get a Type for it. - // This step resolves the "SelfType" reference and creates - // symbols for all the constructors, etc. - - DatatypeType consListType = em.mkDatatypeType(consListSpec); +using namespace CVC4::api; +void test(Solver& slv, Sort& consListSort) +{ // 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 DatatypeType, and + // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - const Datatype& consList = consListType.getDatatype(); + const Datatype& consList = consListSort.getDatatype(); - // e = cons 0 nil + // 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. - Expr e = em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("cons"), - em.mkConst(Rational(0)), - em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("nil"))); - - std::cout << "e is " << e << std::endl - << "type of cons is " << consList.getConstructor("cons").getType() - << std::endl - << "type of nil is " << consList.getConstructor("nil").getType() + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkReal(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; - // e2 = head(cons 0 nil), and of course this can be evaluated + // 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. - Expr e2 = em.mkExpr(kind::APPLY_SELECTOR, - consList["cons"].getSelector("head"), - e); + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); - std::cout << "e2 is " << e2 << std::endl - << "simplify(e2) is " << smt.simplify(e2) - << std::endl << std::endl; + 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::iterator i = consList.begin(); i != consList.end(); ++i) { + for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i) + { std::cout << "ctor: " << *i << std::endl; - for(DatatypeConstructor::iterator j = (*i).begin(); j != (*i).end(); ++j) { + 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". - Type sort = em.mkSort("T", ExprManager::SORT_FLAG_PLACEHOLDER); - Datatype paramConsListSpec(&em, "list", std::vector<Type>{sort}); - DatatypeConstructor paramCons("cons"); - DatatypeConstructor paramNil("nil"); - paramCons.addArg("head", sort); - paramCons.addArg("tail", DatatypeSelfType()); + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec = + slv.mkDatatypeDecl("paramlist", + sort); // give the datatype a name + DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); + paramCons.addSelector("head", sort); + paramCons.addSelectorSelf("tail"); paramConsListSpec.addConstructor(paramCons); paramConsListSpec.addConstructor(paramNil); - DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec); - Type paramConsIntListType = paramConsListType.instantiate(std::vector<Type>{em.integerType()}); + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = + paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - const Datatype& paramConsList = paramConsListType.getDatatype(); + const 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 DatatypeConstructorArg& stor : ctor) + for (const DatatypeSelector& stor : ctor) { std::cout << " + arg: " << stor << std::endl; } } - Expr a = em.mkVar("a", paramConsIntListType); - std::cout << "Expr " << a << " is of type " << a.getType() << std::endl; + Term a = slv.mkConst(paramConsIntListSort, "a"); + std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Expr head_a = em.mkExpr( - kind::APPLY_SELECTOR, - paramConsList["cons"].getSelector("head"), - a); - std::cout << "head_a is " << head_a << " of type " << head_a.getType() + 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 - << "type of cons is " - << paramConsList.getConstructor("cons").getType() << std::endl + << "sort of cons is " + << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - - Expr assertion = em.mkExpr(kind::GT, head_a, em.mkConst(Rational(50))); + Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); std::cout << "Assert " << assertion << std::endl; - smt.assertFormula(assertion); - + slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << smt.checkSat()<< std::endl; + std::cout << "CVC4: " << slv.checkSat() << std::endl; +} + +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 = + slv.mkDatatypeDecl("list"); // give the datatype a name + DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", slv.getIntegerSort()); + cons.addSelectorSelf("tail"); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("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); + + test(slv, consListSort); + + std::cout << std::endl + << ">>> Alternatively, use declareDatatype" << std::endl; + std::cout << std::endl; + + DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); + cons2.addSelector("head", slv.getIntegerSort()); + cons2.addSelectorSelf("tail"); + DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); + std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); return 0; } diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp deleted file mode 100644 index 3f8f974f2..000000000 --- a/examples/api/extract-new.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file extract-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Makai Mann - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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.mkConst(bitvector32, "a"); - - Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); - Term x_31_1 = slv.mkTerm(ext_31_1, x); - - Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); - Term x_30_0 = slv.mkTerm(ext_30_0, x); - - Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); - Term x_31_31 = slv.mkTerm(ext_31_31, x); - - Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 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 entailment assuming: " << eq2 << endl; - cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(eq2) << endl; - - return 0; -} diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index b63c40d82..6ff0db10d 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -2,7 +2,7 @@ /*! \file extract.cpp ** \verbatim ** Top contributors (to current version): - ** Clark Barrett, Aina Niemetz + ** Aina Niemetz, Makai Mann ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,40 +16,40 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_BV"); // Set the logic +int main() +{ + Solver slv; + slv.setLogic("QF_BV"); // Set the logic - Type bitvector32 = em.mkBitVectorType(32); + Sort bitvector32 = slv.mkBitVectorSort(32); - Expr x = em.mkVar("a", bitvector32); + Term x = slv.mkConst(bitvector32, "a"); - Expr ext_31_1 = em.mkConst(CVC4::BitVectorExtract(31,1)); - Expr x_31_1 = em.mkExpr(ext_31_1, x); + Op ext_31_1 = slv.mkOp(BITVECTOR_EXTRACT, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); - Expr ext_30_0 = em.mkConst(CVC4::BitVectorExtract(30,0)); - Expr x_30_0 = em.mkExpr(ext_30_0, x); + Op ext_30_0 = slv.mkOp(BITVECTOR_EXTRACT, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); - Expr ext_31_31 = em.mkConst(CVC4::BitVectorExtract(31,31)); - Expr x_31_31 = em.mkExpr(ext_31_31, x); + Op ext_31_31 = slv.mkOp(BITVECTOR_EXTRACT, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); - Expr ext_0_0 = em.mkConst(CVC4::BitVectorExtract(0,0)); - Expr x_0_0 = em.mkExpr(ext_0_0, x); + Op ext_0_0 = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); - Expr eq = em.mkExpr(kind::EQUAL, x_31_1, x_30_0); + Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; - smt.assertFormula(eq); + slv.assertFormula(eq); - Expr eq2 = em.mkExpr(kind::EQUAL, x_31_31, x_0_0); - cout << " Querying: " << eq2 << endl; - cout << " Expect entailed. " << endl; - cout << " CVC4: " << smt.checkEntailed(eq2) << endl; + Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); + cout << " Check entailment assuming: " << eq2 << endl; + cout << " Expect ENTAILED. " << endl; + cout << " CVC4: " << slv.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp deleted file mode 100644 index 0f98b5dcb..000000000 --- a/examples/api/helloworld-new.cpp +++ /dev/null @@ -1,30 +0,0 @@ -/********************* */ -/*! \file helloworld-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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 <cvc4/api/cvc4cpp.h> - -using namespace CVC4::api; - -int main() -{ - Solver slv; - Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); - std::cout << helloworld << " is " << slv.checkEntailed(helloworld) - << std::endl; - return 0; -} diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 5718dc230..873947522 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -2,7 +2,7 @@ /*! \file helloworld.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,14 +16,15 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; -int main() { - ExprManager em; - Expr helloworld = em.mkVar("Hello World!", em.booleanType()); - SmtEngine smt(&em); - std::cout << helloworld << " is " << smt.checkEntailed(helloworld) +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); + std::cout << helloworld << " is " << slv.checkEntailed(helloworld) << std::endl; return 0; } diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp deleted file mode 100644 index 42fe39bfb..000000000 --- a/examples/api/linear_arith-new.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \file linear_arith-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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.mkConst(integer, "x"); - Term y = slv.mkConst(real, "y"); - - // Constants - Term three = slv.mkReal(3); - Term neg2 = slv.mkReal(-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 ENTAILED." << endl; - cout << "Result from CVC4 is: " << slv.checkEntailed(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/linear_arith.cpp b/examples/api/linear_arith.cpp index 83c3109d4..c60e17f85 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -2,7 +2,7 @@ /*! \file linear_arith.cpp ** \verbatim ** Top contributors (to current version): - ** Tim King, Aina Niemetz + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -17,66 +17,66 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include "cvc4/api/cvc4cpp.h" using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); - smt.setLogic("QF_LIRA"); // Set the logic +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 - // Types - Type real = em.realType(); - Type integer = em.integerType(); + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); // Variables - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", real); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(real, "y"); // Constants - Expr three = em.mkConst(Rational(3)); - Expr neg2 = em.mkConst(Rational(-2)); - Expr two_thirds = em.mkConst(Rational(2,3)); + Term three = slv.mkReal(3); + Term neg2 = slv.mkReal(-2); + Term two_thirds = slv.mkReal(2, 3); // Terms - Expr three_y = em.mkExpr(kind::MULT, three, y); - Expr diff = em.mkExpr(kind::MINUS, y, x); + Term three_y = slv.mkTerm(MULT, three, y); + Term diff = slv.mkTerm(MINUS, y, x); // Formulas - Expr x_geq_3y = em.mkExpr(kind::GEQ, x, three_y); - Expr x_leq_y = em.mkExpr(kind::LEQ, x, y); - Expr neg2_lt_x = em.mkExpr(kind::LT, neg2, x); + 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); - Expr assumptions = - em.mkExpr(kind::AND, x_geq_3y, x_leq_y, neg2_lt_x); + Term assertions = + slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); - cout << "Given the assumptions " << assumptions << endl; - smt.assertFormula(assumptions); + cout << "Given the assertions " << assertions << endl; + slv.assertFormula(assertions); - smt.push(); - Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds); + 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 ENTAILED." << endl; - cout << "Result from CVC4 is: " << smt.checkEntailed(diff_leq_two_thirds) + cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) << endl; - smt.pop(); + slv.pop(); cout << endl; - smt.push(); - Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds); - smt.assertFormula(diff_is_two_thirds); - cout << "Show that the asserts are consistent with " << 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: " << smt.checkSat(em.mkConst(true)) << endl; - smt.pop(); + cout << "Result from CVC4 is: " << slv.checkSat() << endl; + slv.pop(); cout << "Thus the maximum value of (y - x) is 2/3."<< endl; diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp deleted file mode 100644 index 0ff3ad932..000000000 --- a/examples/api/sets-new.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/********************* */ -/*! \file sets-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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.mkConst(set, "A"); - Term B = slv.mkConst(set, "B"); - Term C = slv.mkConst(set, "C"); - - 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.checkEntailed(theorem) - << "." << endl; - } - - // Verify emptset is a subset of any set - { - Term A = slv.mkConst(set, "A"); - Term emptyset = slv.mkEmptySet(set); - - Term theorem = slv.mkTerm(SUBSET, emptyset, A); - - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) - << "." << endl; - } - - // Find me an element in {1, 2} intersection {2, 3}, if there is one. - { - Term one = slv.mkReal(1); - Term two = slv.mkReal(2); - Term three = slv.mkReal(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.mkConst(integer, "x"); - - 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/sets.cpp b/examples/api/sets.cpp index 4e4fb4cd4..aa70b4ee4 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -2,7 +2,7 @@ /*! \file sets.cpp ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Aina Niemetz, Tim King + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,82 +16,80 @@ #include <iostream> -#include <cvc4/cvc4.h> -#include <cvc4/options/set_language.h> +#include <cvc4/api/cvc4cpp.h> using namespace std; -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); +int main() +{ + Solver slv; // Optionally, set the logic. We need at least UF for equality predicate, // integers (LIA) and sets (FS). - smt.setLogic("QF_UFLIAFS"); + slv.setLogic("QF_UFLIAFS"); // Produce models - smt.setOption("produce-models", true); + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); - // Set output language to SMTLIB2 - cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); - - Type integer = em.integerType(); - Type set = em.mkSetType(integer); + 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) { - Expr A = em.mkVar("A", set); - Expr B = em.mkVar("B", set); - Expr C = em.mkVar("C", set); + Term A = slv.mkConst(set, "A"); + Term B = slv.mkConst(set, "B"); + Term C = slv.mkConst(set, "C"); - Expr unionAB = em.mkExpr(kind::UNION, A, B); - Expr lhs = em.mkExpr(kind::INTERSECTION, unionAB, C); + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); - Expr intersectionAC = em.mkExpr(kind::INTERSECTION, A, C); - Expr intersectionBC = em.mkExpr(kind::INTERSECTION, B, C); - Expr rhs = em.mkExpr(kind::UNION, intersectionAC, intersectionBC); + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); - Expr theorem = em.mkExpr(kind::EQUAL, lhs, rhs); + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } // Verify emptset is a subset of any set { - Expr A = em.mkVar("A", set); - Expr emptyset = em.mkConst(EmptySet(set)); + Term A = slv.mkConst(set, "A"); + Term emptyset = slv.mkEmptySet(set); - Expr theorem = em.mkExpr(kind::SUBSET, emptyset, A); + Term theorem = slv.mkTerm(SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " << smt.checkEntailed(theorem) + cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } // Find me an element in {1, 2} intersection {2, 3}, if there is one. { - Expr one = em.mkConst(Rational(1)); - Expr two = em.mkConst(Rational(2)); - Expr three = em.mkConst(Rational(3)); + Term one = slv.mkReal(1); + Term two = slv.mkReal(2); + Term three = slv.mkReal(3); - Expr singleton_one = em.mkExpr(kind::SINGLETON, one); - Expr singleton_two = em.mkExpr(kind::SINGLETON, two); - Expr singleton_three = em.mkExpr(kind::SINGLETON, three); - Expr one_two = em.mkExpr(kind::UNION, singleton_one, singleton_two); - Expr two_three = em.mkExpr(kind::UNION, singleton_two, singleton_three); - Expr intersection = em.mkExpr(kind::INTERSECTION, one_two, two_three); + 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); - Expr x = em.mkVar("x", integer); + Term x = slv.mkConst(integer, "x"); - Expr e = em.mkExpr(kind::MEMBER, x, intersection); + Term e = slv.mkTerm(MEMBER, x, intersection); - Result result = smt.checkSat(e); + Result result = slv.checkSatAssuming(e); cout << "CVC4 reports: " << e << " is " << result << "." << endl; - if(result == Result::SAT) { - cout << "For instance, " << smt.getValue(x) << " is a member." << 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 deleted file mode 100644 index 4d2c45d52..000000000 --- a/examples/api/strings-new.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/********************* */ -/*! \file strings-new.cpp - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 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/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.mkConst(string, "x"); - Term y = slv.mkConst(string, "y"); - Term z = slv.mkConst(string, "z"); - - // 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.mkReal(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.mkConst(string, "s1"); - Term s2 = slv.mkConst(string, "s2"); - // 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; - } -} diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index f114ef7f3..6a0e10918 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -2,7 +2,7 @@ /*! \file strings.cpp ** \verbatim ** Top contributors (to current version): - ** Tianyi Liang, Tim King + ** Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -16,86 +16,80 @@ #include <iostream> -#include <cvc4/cvc4.h> -#include <cvc4/options/set_language.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; +using namespace CVC4::api; -int main() { - ExprManager em; - SmtEngine smt(&em); +int main() +{ + Solver slv; // Set the logic - smt.setLogic("S"); - + slv.setLogic("S"); // Produce models - smt.setOption("produce-models", true); - + slv.setOption("produce-models", "true"); // The option strings-exp is needed - smt.setOption("strings-exp", true); - + slv.setOption("strings-exp", "true"); // Set output language to SMTLIB2 - std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + slv.setOption("output-language", "smt2"); // String type - Type string = em.stringType(); + Sort string = slv.getStringSort(); // std::string - std::string std_str_ab("ab"); - // CVC4::String - CVC4::String cvc4_str_ab(std_str_ab); - CVC4::String cvc4_str_abc("abc"); + std::string str_ab("ab"); // String constants - Expr ab = em.mkConst(cvc4_str_ab); - Expr abc = em.mkConst(CVC4::String("abc")); + Term ab = slv.mkString(str_ab); + Term abc = slv.mkString("abc"); // String variables - Expr x = em.mkVar("x", string); - Expr y = em.mkVar("y", string); - Expr z = em.mkVar("z", string); + Term x = slv.mkConst(string, "x"); + Term y = slv.mkConst(string, "y"); + Term z = slv.mkConst(string, "z"); // String concatenation: x.ab.y - Expr lhs = em.mkExpr(kind::STRING_CONCAT, x, ab, y); + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); // String concatenation: abc.z - Expr rhs = em.mkExpr(kind::STRING_CONCAT, abc, z); + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); // x.ab.y = abc.z - Expr formula1 = em.mkExpr(kind::EQUAL, lhs, rhs); + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); // Length of y: |y| - Expr leny = em.mkExpr(kind::STRING_LENGTH, y); + Term leny = slv.mkTerm(STRING_LENGTH, y); // |y| >= 0 - Expr formula2 = em.mkExpr(kind::GEQ, leny, em.mkConst(Rational(0))); + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0)); // Regular expression: (ab[c-e]*f)|g|h - Expr r = em.mkExpr(kind::REGEXP_UNION, - em.mkExpr(kind::REGEXP_CONCAT, - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("ab"))), - em.mkExpr(kind::REGEXP_STAR, - em.mkExpr(kind::REGEXP_RANGE, em.mkConst(String("c")), em.mkConst(String("e")))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("f")))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("g"))), - em.mkExpr(kind::STRING_TO_REGEXP, em.mkConst(String("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 - Expr s1 = em.mkVar("s1", string); - Expr s2 = em.mkVar("s2", string); + Term s1 = slv.mkConst(string, "s1"); + Term s2 = slv.mkConst(string, "s2"); // String concatenation: s1.s2 - Expr s = em.mkExpr(kind::STRING_CONCAT, s1, s2); + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); // s1.s2 in (ab[c-e]*f)|g|h - Expr formula3 = em.mkExpr(kind::STRING_IN_REGEXP, s, r); + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); // Make a query - Expr q = em.mkExpr(kind::AND, + Term q = slv.mkTerm(AND, formula1, formula2, formula3); // check sat - Result result = smt.checkSat(q); + Result result = slv.checkSatAssuming(q); std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; - if(result == Result::SAT) { - std::cout << " x = " << smt.getValue(x) << std::endl; - std::cout << " s1.s2 = " << smt.getValue(s) << std::endl; + if(result.isSat()) + { + std::cout << " x = " << slv.getValue(x) << std::endl; + std::cout << " s1.s2 = " << slv.getValue(s) << std::endl; } } |