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
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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.
// 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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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):
//
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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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;
}
+++ /dev/null
-/********************* */
-/*! \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;
-}
/*! \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.
#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;
+++ /dev/null
-/********************* */
-/*! \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;
- }
- }
-}
/*! \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.
#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;
}
}
}
+++ /dev/null
-/********************* */
-/*! \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;
- }
-}
/*! \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.
#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;
}
}
projects / cvc5.git / commitdiff