diff options
| -rw-r--r-- | examples/api/bitvectors-new.cpp | 130 | ||||
| -rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 96 | ||||
| -rw-r--r-- | examples/api/combination-new.cpp | 139 | ||||
| -rw-r--r-- | examples/api/datatypes-new.cpp | 165 | ||||
| -rw-r--r-- | examples/api/extract-new.cpp | 56 | ||||
| -rw-r--r-- | examples/api/helloworld-new.cpp | 30 | ||||
| -rw-r--r-- | examples/api/linear_arith-new.cpp | 85 | ||||
| -rw-r--r-- | examples/api/sets-new.cpp | 96 | ||||
| -rw-r--r-- | examples/api/strings-new.cpp | 96 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 2359 | ||||
| -rw-r--r-- | src/api/cvc4cppkind.h | 2334 |
11 files changed, 5586 insertions, 0 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp new file mode 100644 index 000000000..596d0b515 --- /dev/null +++ b/examples/api/bitvectors-new.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file bitvectors.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Liana Hadarean, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector solver. + ** + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + + Solver slv; + slv.setLogic("QF_BV"); // Set the logic + + // The following example has been adapted from the book A Hacker's Delight by + // Henry S. Warren. + // + // Given a variable x that can only have two values, a or b. We want to + // assign to x a value other than the current one. The straightforward code + // to do that is: + // + //(0) if (x == a ) x = b; + // else x = a; + // + // Two more efficient yet equivalent methods are: + // + //(1) x = a ⊕ b ⊕ x; + // + //(2) x = a + b - x; + // + // We will use CVC4 to prove that the three pieces of code above are all + // equivalent by encoding the problem in the bit-vector theory. + + // Creating a bit-vector type of width 32 + Sort bitvector32 = slv.mkBitVectorSort(32); + + std::cout << "bitvector32 " << bitvector32 << std::endl; + // Variables + Term x = slv.mkVar("x", bitvector32); + std::cout << "bitvector32 " << bitvector32 << std::endl; + Term a = slv.mkVar("a", bitvector32); + Term b = slv.mkVar("b", bitvector32); + + // First encode the assumption that x must be equal to a or b + Term x_eq_a = slv.mkTerm(EQUAL, x, a); + Term x_eq_b = slv.mkTerm(EQUAL, x, b); + Term assumption = slv.mkTerm(OR, x_eq_a, x_eq_b); + + // Assert the assumption + slv.assertFormula(assumption); + + // Introduce a new variable for the new value of x after assignment. + Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0) + Term new_x_ = slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) + + // Encoding code (0) + // new_x = x == a ? b : a; + Term ite = slv.mkTerm(ITE, x_eq_a, b, a); + Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); + + // Assert the encoding of code (0) + cout << "Asserting " << assignment0 << " to CVC4 " << endl; + slv.assertFormula(assignment0); + cout << "Pushing a new context." << endl; + slv.push(); + + // Encoding code (1) + // new_x_ = a xor b xor x + Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); + Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); + + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment1 << " to CVC4 " << endl; + slv.assertFormula(assignment1); + Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); + + cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + cout << " Popping context. " << endl; + slv.pop(); + + // Encoding code (2) + // new_x_ = a + b - x + Term a_plus_b = slv.mkTerm(BITVECTOR_PLUS, a, b); + Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); + Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); + + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment2 << " to CVC4 " << endl; + slv.assertFormula(assignment2); + + cout << " Check validity assuming: " << new_x_eq_new_x_ << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(new_x_eq_new_x_) << endl; + + Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); + std::vector<Term> v{new_x_eq_new_x_, x_neq_x}; + cout << " Check Validity Assuming: " << v << endl; + cout << " Expect invalid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(v) << endl; + + // Assert that a is odd + OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); + Term lsb_of_a = slv.mkTerm(extract_op, a); + cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; + Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); + cout << "Assert " << a_odd << endl; + cout << "Check satisfiability." << endl; + slv.assertFormula(a_odd); + cout << " Expect sat. " << endl; + cout << " CVC4: " << slv.checkSat() << endl; + return 0; +} diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp new file mode 100644 index 000000000..3d4e6bca0 --- /dev/null +++ b/examples/api/bitvectors_and_arrays-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file bitvectors_and_arrays.cpp + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Aina Niemetz, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector and array solvers. + ** + **/ + +#include <iostream> +#include <cmath> +// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "smtlib"); // output-language + slv.setLogic("QF_AUFBV"); // Set the logic + + // Consider the following code (where size is some previously defined constant): + // + // + // Assert (current_array[0] > 0); + // for (unsigned i = 1; i < k; ++i) { + // current_array[i] = 2 * current_array[i - 1]; + // Assert (current_array[i-1] < current_array[i]); + // } + // + // We want to check whether the assertion in the body of the for loop holds + // throughout the loop. + + // Setting up the problem parameters + unsigned k = 4; // number of unrollings (should be a power of 2) + unsigned index_size = log2(k); // size of the index + + + // Sorts + Sort elementSort = slv.mkBitVectorSort(32); + Sort indexSort = slv.mkBitVectorSort(index_size); + Sort arraySort = slv.mkArraySort(indexSort, elementSort); + + // Variables + Term current_array = slv.mkVar("current_array", arraySort); + + // Making a bit-vector constant + Term zero = slv.mkBitVector(index_size, 0u); + + // Asserting that current_array[0] > 0 + Term current_array0 = slv.mkTerm(SELECT, current_array, zero); + Term current_array0_gt_0 = slv.mkTerm( + BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0u)); + slv.assertFormula(current_array0_gt_0); + + // Building the assertions in the loop unrolling + Term index = slv.mkBitVector(index_size, 0u); + Term old_current = slv.mkTerm(SELECT, current_array, index); + Term two = slv.mkBitVector(32, 2u); + + std::vector<Term> assertions; + for (unsigned i = 1; i < k; ++i) { + index = slv.mkBitVector(index_size, i); + Term new_current = slv.mkTerm(BITVECTOR_MULT, two, old_current); + // current[i] = 2 * current[i-1] + current_array = slv.mkTerm(STORE, current_array, index, new_current); + // current[i-1] < current [i] + Term current_slt_new_current = slv.mkTerm(BITVECTOR_SLT, old_current, new_current); + assertions.push_back(current_slt_new_current); + + old_current = slv.mkTerm(SELECT, current_array, index); + } + + Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); + + cout << "Asserting " << query << " to CVC4 " << endl; + slv.assertFormula(query); + cout << "Expect sat. " << endl; + cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; + + // Getting the model + cout << "The satisfying model is: " << endl; + cout << " current_array = " << slv.getValue(current_array) << endl; + cout << " current_array[0] = " << slv.getValue(current_array0) << endl; + return 0; +} diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp new file mode 100644 index 000000000..2956d76e6 --- /dev/null +++ b/examples/api/combination-new.cpp @@ -0,0 +1,139 @@ +/********************* */ +/*! \file combination.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the capabilities of CVC4 + ** + ** A simple demonstration of how to use uninterpreted functions, combining this + ** with arithmetic, and extracting a model at the end of a satisfiable query. + ** The model is displayed using getValue(). + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +void prefixPrintGetValue(Solver& slv, Term t, int level = 0) +{ + cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl; + + for (const Term& c : t) + { + prefixPrintGetValue(slv, c, level + 1); + } +} + +int main() +{ + Solver slv; + slv.setOption("produce-models", "true"); // Produce Models + slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's + slv.setOption("default-dag-thresh", "0"); // Disable dagifying the output + slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language + slv.setLogic(string("QF_UFLIRA")); + + // Sorts + Sort u = slv.mkUninterpretedSort("u"); + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort uToInt = slv.mkFunctionSort(u, integer); + Sort intPred = slv.mkFunctionSort(integer, boolean); + + // Variables + Term x = slv.mkVar("x", u); + Term y = slv.mkVar("y", u); + + // Functions + Term f = slv.mkVar("f", uToInt); + Term p = slv.mkVar("p", intPred); + + // Constants + Term zero = slv.mkInteger(0); + Term one = slv.mkInteger(1); + + // Terms + Term f_x = slv.mkTerm(APPLY_UF, f, x); + Term f_y = slv.mkTerm(APPLY_UF, f, y); + Term sum = slv.mkTerm(PLUS, f_x, f_y); + Term p_0 = slv.mkTerm(APPLY_UF, p, zero); + Term p_f_y = slv.mkTerm(APPLY_UF, p, f_y); + + // Construct the assertions + Term assertions = slv.mkTerm(AND, + vector<Term>{ + slv.mkTerm(LEQ, zero, f_x), // 0 <= f(x) + slv.mkTerm(LEQ, zero, f_y), // 0 <= f(y) + slv.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1 + p_0.notTerm(), // not p(0) + p_f_y // p(f(y)) + }); + slv.assertFormula(assertions); + + cout << "Given the following assertions:" << endl + << assertions << endl << endl; + + cout << "Prove x /= y is valid. " << endl + << "CVC4: " << slv.checkValidAssuming(slv.mkTerm(DISTINCT, x, y)) + << "." << endl << endl; + + cout << "Call checkSat to show that the assertions are satisfiable. " + << endl + << "CVC4: " + << slv.checkSat() << "."<< endl << endl; + + cout << "Call slv.getValue(...) on terms of interest." + << endl; + cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl; + cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl; + cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl; + cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl; + cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y) + << endl << endl; + + cout << "Alternatively, iterate over assertions and call slv.getValue(...) " + << "on all terms." + << endl; + prefixPrintGetValue(slv, assertions); + + cout << endl << endl << "Alternatively, print the model." << endl << endl; + + slv.printModel(cout); + + cout << endl; + cout << "You can also use nested loops to iterate over terms." << endl; + for (Term::const_iterator it = assertions.begin(); + it != assertions.end(); + ++it) + { + cout << "term: " << *it << endl; + for (Term::const_iterator it2 = (*it).begin(); + it2 != (*it).end(); + ++it2) + { + cout << " + child: " << *it2 << std::endl; + } + } + cout << endl; + cout << "Alternatively, you can also use for-each loops." << endl; + for (const Term& t : assertions) + { + cout << "term: " << t << endl; + for (const Term& c : t) + { + cout << " + child: " << c << endl; + } + } + + return 0; +} diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp new file mode 100644 index 000000000..9ec679f8e --- /dev/null +++ b/examples/api/datatypes-new.cpp @@ -0,0 +1,165 @@ +/********************* */ +/*! \file datatypes.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief An example of using inductive datatypes in CVC4 + ** + ** An example of using inductive datatypes in CVC4. + **/ + +#include <iostream> +//#include <cvc4/cvc4.h> // To follow the wiki + +#include "api/cvc4cpp.h" +using namespace CVC4::api; + +int main() +{ + Solver slv; + // This example builds a simple "cons list" of integers, with + // two constructors, "cons" and "nil." + + // Building a datatype consists of two steps. + // First, the datatype is specified. + // Second, it is "resolved" to an actual sort, at which point function + // symbols are assigned to its constructors, selectors, and testers. + + DatatypeDecl consListSpec("list"); // give the datatype a name + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", slv.getIntegerSort()); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + consListSpec.addConstructor(nil); + + std::cout << "spec is:" << std::endl + << consListSpec << std::endl; + + // Keep in mind that "DatatypeDecl" is the specification class for + // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + // Now that our Datatype is fully specified, we can get a Sort for it. + // This step resolves the "SelfSort" reference and creates + // symbols for all the constructors, etc. + + Sort consListSort = slv.mkDatatypeSort(consListSpec); + + // Now our old "consListSpec" is useless--the relevant information + // has been copied out, so we can throw that spec away. We can get + // the complete spec for the datatype from the DatatypeSort, and + // this Datatype object has constructor symbols (and others) filled in. + + Datatype consList = consListSort.getDatatype(); + + // t = cons 0 nil + // + // Here, consList["cons"] gives you the DatatypeConstructor. To get + // the constructor symbol for application, use .getConstructor("cons"), + // which is equivalent to consList["cons"].getConstructor(). Note that + // "nil" is a constructor too, so it needs to be applied with + // APPLY_CONSTRUCTOR, even though it has no arguments. + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkInteger(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + + std::cout << "t is " << t << std::endl + << "sort of cons is " + << consList.getConstructorTerm("cons").getSort() << std::endl + << "sort of nil is " << consList.getConstructorTerm("nil").getSort() + << std::endl; + + // t2 = head(cons 0 nil), and of course this can be evaluated + // + // Here we first get the DatatypeConstructor for cons (with + // consList["cons"]) in order to get the "head" selector symbol + // to apply. + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); + + std::cout << "t2 is " << t2 << std::endl + << "simplify(t2) is " << slv.simplify(t2) + << std::endl << std::endl; + + // You can also iterate over a Datatype to get all its constructors, + // and over a DatatypeConstructor to get all its "args" (selectors) + for (Datatype::const_iterator i = consList.begin(); + i != consList.end(); + ++i) + { + std::cout << "ctor: " << *i << std::endl; + for (DatatypeConstructor::const_iterator j = (*i).begin(); + j != (*i).end(); + ++j) + { + std::cout << " + arg: " << *j << std::endl; + } + } + std::cout << std::endl; + + // Alternatively, you can use for each loops. + for (const auto& c : consList) + { + std::cout << "ctor: " << c << std::endl; + for (const auto& s : c) + { + std::cout << " + arg: " << s << std::endl; + } + } + std::cout << std::endl; + + // You can also define parameterized datatypes. + // This example builds a simple parameterized list of sort T, with one + // constructor "cons". + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name + DatatypeConstructorDecl paramCons("cons"); + DatatypeSelectorDecl paramHead("head", sort); + DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort()); + paramCons.addSelector(paramHead); + paramCons.addSelector(paramTail); + paramConsListSpec.addConstructor(paramCons); + + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = + paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); + + Datatype paramConsList = paramConsListSort.getDatatype(); + + std::cout << "parameterized datatype sort is " << std::endl; + for (const DatatypeConstructor& ctor : paramConsList) + { + std::cout << "ctor: " << ctor << std::endl; + for (const DatatypeSelector& stor : ctor) + { + std::cout << " + arg: " << stor << std::endl; + } + } + + Term a = slv.declareFun("a", paramConsIntListSort); + std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; + + Term head_a = slv.mkTerm( + APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() + << std::endl + << "sort of cons is " + << paramConsList.getConstructorTerm("cons").getSort() << std::endl + << std::endl; + Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50)); + std::cout << "Assert " << assertion << std::endl; + slv.assertFormula(assertion); + std::cout << "Expect sat." << std::endl; + std::cout << "CVC4: " << slv.checkSat() << std::endl; + + return 0; +} diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp new file mode 100644 index 000000000..8d31c1b12 --- /dev/null +++ b/examples/api/extract-new.cpp @@ -0,0 +1,56 @@ +/********************* */ +/*! \file extract.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the solving capabilities of the CVC4 + ** bit-vector solver. + ** + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setLogic("QF_BV"); // Set the logic + + Sort bitvector32 = slv.mkBitVectorSort(32); + + Term x = slv.mkVar("a", bitvector32); + + OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + Term x_31_1 = slv.mkTerm(ext_31_1, x); + + OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); + Term x_30_0 = slv.mkTerm(ext_30_0, x); + + OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); + Term x_31_31 = slv.mkTerm(ext_31_31, x); + + OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); + Term x_0_0 = slv.mkTerm(ext_0_0, x); + + Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); + cout << " Asserting: " << eq << endl; + slv.assertFormula(eq); + + Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); + cout << " Check validity assuming: " << eq2 << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << slv.checkValidAssuming(eq2) << endl; + + return 0; +} diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp new file mode 100644 index 000000000..7957741e5 --- /dev/null +++ b/examples/api/helloworld-new.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file helloworld.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Tim King, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A very simple CVC4 example + ** + ** A very simple CVC4 tutorial example. + **/ + +#include <iostream> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort()); + std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld) + << std::endl; + return 0; +} diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp new file mode 100644 index 000000000..ef8faade9 --- /dev/null +++ b/examples/api/linear_arith-new.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file linear_arith.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 + ** + ** A simple demonstration of the linear arithmetic solving capabilities and + ** the push pop of CVC4. This also gives an example option. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setLogic("QF_LIRA"); // Set the logic + + // Prove that if given x (Integer) and y (Real) then + // the maximum value of y - x is 2/3 + + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); + + // Variables + Term x = slv.mkVar("x", integer); + Term y = slv.mkVar("y", real); + + // Constants + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); + Term two_thirds = slv.mkReal(2, 3); + + // Terms + Term three_y = slv.mkTerm(MULT, three, y); + Term diff = slv.mkTerm(MINUS, y, x); + + // Formulas + Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); + Term x_leq_y = slv.mkTerm(LEQ, x, y); + Term neg2_lt_x = slv.mkTerm(LT, neg2, x); + + Term assertions = + slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); + + cout << "Given the assertions " << assertions << endl; + slv.assertFormula(assertions); + + + slv.push(); + Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); + cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " + << slv.checkValidAssuming(diff_leq_two_thirds) << endl; + slv.pop(); + + cout << endl; + + slv.push(); + Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); + slv.assertFormula(diff_is_two_thirds); + cout << "Show that the assertions are consistent with " << endl; + cout << diff_is_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report SAT." << endl; + cout << "Result from CVC4 is: " << slv.checkSat() << endl; + slv.pop(); + + cout << "Thus the maximum value of (y - x) is 2/3."<< endl; + + return 0; +} diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp new file mode 100644 index 000000000..be35bcc21 --- /dev/null +++ b/examples/api/sets-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file sets.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Reasoning about sets with CVC4. + ** + ** A simple demonstration of reasoning about sets with CVC4. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS"); + + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); + + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); + + // Verify union distributions over intersection + // (A union B) intersection C = (A intersection C) union (B intersection C) + { + Term A = slv.mkVar("A", set); + Term B = slv.mkVar("B", set); + Term C = slv.mkVar("C", set); + + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Verify emptset is a subset of any set + { + Term A = slv.mkVar("A", set); + Term emptyset = slv.mkEmptySet(set); + + Term theorem = slv.mkTerm(SUBSET, emptyset, A); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Find me an element in {1, 2} intersection {2, 3}, if there is one. + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + + Term x = slv.mkVar("x", integer); + + Term e = slv.mkTerm(MEMBER, x, intersection); + + Result result = slv.checkSatAssuming(e); + cout << "CVC4 reports: " << e << " is " << result << "." << endl; + + if (result.isSat()) + { + cout << "For instance, " << slv.getValue(x) << " is a member." << endl; + } + } +} diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp new file mode 100644 index 000000000..2010c6909 --- /dev/null +++ b/examples/api/strings-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file strings.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Paul Meng, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Reasoning about strings with CVC4 via C++ API. + ** + ** A simple demonstration of reasoning about strings with CVC4 via C++ API. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // Set the logic + slv.setLogic("S"); + // Produce models + slv.setOption("produce-models", "true"); + // The option strings-exp is needed + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); + + // String type + Sort string = slv.getStringSort(); + + // std::string + std::string str_ab("ab"); + // String constants + Term ab = slv.mkString(str_ab); + Term abc = slv.mkString("abc"); + // String variables + Term x = slv.mkVar("x", string); + Term y = slv.mkVar("y", string); + Term z = slv.mkVar("z", string); + + // String concatenation: x.ab.y + Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y); + // String concatenation: abc.z + Term rhs = slv.mkTerm(STRING_CONCAT, abc, z); + // x.ab.y = abc.z + Term formula1 = slv.mkTerm(EQUAL, lhs, rhs); + + // Length of y: |y| + Term leny = slv.mkTerm(STRING_LENGTH, y); + // |y| >= 0 + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); + + // Regular expression: (ab[c-e]*f)|g|h + Term r = slv.mkTerm(REGEXP_UNION, + slv.mkTerm(REGEXP_CONCAT, + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")), + slv.mkTerm(REGEXP_STAR, + slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")), + slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h"))); + + // String variables + Term s1 = slv.mkVar("s1", string); + Term s2 = slv.mkVar("s2", string); + // String concatenation: s1.s2 + Term s = slv.mkTerm(STRING_CONCAT, s1, s2); + + // s1.s2 in (ab[c-e]*f)|g|h + Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r); + + // Make a query + Term q = slv.mkTerm(AND, + formula1, + formula2, + formula3); + + // check sat + Result result = slv.checkSatAssuming(q); + std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + + if(result.isSat()) + { + std::cout << " x = " << slv.getValue(x) << std::endl; + std::cout << " s1.s2 = " << slv.getValue(s) << std::endl; + } +} diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h new file mode 100644 index 000000000..643246b62 --- /dev/null +++ b/src/api/cvc4cpp.h @@ -0,0 +1,2359 @@ +/********************* */ +/*! \file cvc4cpp.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The CVC4 C++ API. + ** + ** The CVC4 C++ API. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__API__CVC4CPP_H +#define __CVC4__API__CVC4CPP_H + +#include "cvc4cppkind.h" + +#include <map> +#include <memory> +#include <set> +#include <string> +#include <unordered_map> +#include <unordered_set> +#include <vector> + +namespace CVC4 { + +class Expr; +class Datatype; +class DatatypeConstructor; +class DatatypeConstructorArg; +class ExprManager; +class SmtEngine; +class Type; +class Options; +class Random; +class Result; + +namespace api { + +/* -------------------------------------------------------------------------- */ +/* Result */ +/* -------------------------------------------------------------------------- */ + +/** + * Encapsulation of a three-valued solver result, with explanations. + */ +class CVC4_PUBLIC Result +{ + friend class Solver; + + public: + /** + * Return true if query was a satisfiable checkSat() or checkSatAssuming() + * query. + */ + bool isSat() const; + + /** + * Return true if query was an unsatisfiable checkSat() or + * checkSatAssuming() query. + */ + bool isUnsat() const; + + /** + * Return true if query was a checkSat() or checkSatAssuming() query and + * CVC4 was not able to determine (un)satisfiability. + */ + bool isSatUnknown() const; + + /** + * Return true if corresponding query was a valid checkValid() or + * checkValidAssuming() query. + */ + bool isValid() const; + + /** + * Return true if corresponding query was an invalid checkValid() or + * checkValidAssuming() query. + */ + bool isInvalid() const; + + /** + * Return true if query was a checkValid() or checkValidAssuming() query + * and CVC4 was not able to determine (in)validity. + */ + bool isValidUnknown() const; + + /** + * Operator overloading for equality of two results. + * @param r the result to compare to for equality + * @return true if the results are equal + */ + bool operator==(const Result& r) const; + + /** + * Operator overloading for disequality of two results. + * @param r the result to compare to for disequality + * @return true if the results are disequal + */ + bool operator!=(const Result& r) const; + + /** + * @return an explanation for an unknown query result. + */ + std::string getUnknownExplanation() const; + + /** + * @return a string representation of this result. + */ + std::string toString() const; + + private: + /** + * Constructor. + * @param r the internal result that is to be wrapped by this result + * @return the Result + */ + Result(const CVC4::Result& r); + + /** + * The interal result wrapped by this result. + * This is a shared_ptr rather than a unique_ptr since CVC4::Result is + * not ref counted. + */ + std::shared_ptr<CVC4::Result> d_result; +}; + +/** + * Serialize a result to given stream. + * @param out the output stream + * @param r the result to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; + +/* -------------------------------------------------------------------------- */ +/* Sort */ +/* -------------------------------------------------------------------------- */ + +class Datatype; + +/** + * The sort of a CVC4 term. + */ +class CVC4_PUBLIC Sort +{ + friend class DatatypeConstructorDecl; + friend class DatatypeDecl; + friend class DatatypeSelectorDecl; + friend class OpTerm; + friend class Solver; + friend struct SortHashFunction; + friend class Term; + + public: + /** + * Destructor. + */ + ~Sort(); + + /** + * Assignment operator. + * @param s the sort to assign to this sort + * @return this sort after assignment + */ + Sort& operator=(const Sort& s); + + /** + * Comparison for structural equality. + * @param s the sort to compare to + * @return true if the sorts are equal + */ + bool operator==(const Sort& s) const; + + /** + * Comparison for structural disequality. + * @param s the sort to compare to + * @return true if the sorts are not equal + */ + bool operator!=(const Sort& s) const; + + /** + * Is this a Boolean sort? + * @return true if the sort is a Boolean sort + */ + bool isBoolean() const; + + /** + * Is this a integer sort? + * @return true if the sort is a integer sort + */ + bool isInteger() const; + + /** + * Is this a real sort? + * @return true if the sort is a real sort + */ + bool isReal() const; + + /** + * Is this a string sort? + * @return true if the sort is the string sort + */ + bool isString() const; + + /** + * Is this a regexp sort? + * @return true if the sort is the regexp sort + */ + bool isRegExp() const; + + /** + * Is this a rounding mode sort? + * @return true if the sort is the rounding mode sort + */ + bool isRoundingMode() const; + + /** + * Is this a bit-vector sort? + * @return true if the sort is a bit-vector sort + */ + bool isBitVector() const; + + /** + * Is this a floating-point sort? + * @return true if the sort is a floating-point sort + */ + bool isFloatingPoint() const; + + /** + * Is this a datatype sort? + * @return true if the sort is a datatype sort + */ + bool isDatatype() const; + + /** + * Is this a function sort? + * @return true if the sort is a function sort + */ + bool isFunction() const; + + /** + * Is this a predicate sort? + * That is, is this a function sort mapping to Boolean? All predicate + * sorts are also function sorts. + * @return true if the sort is a predicate sort + */ + bool isPredicate() const; + + /** + * Is this a tuple sort? + * @return true if the sort is a tuple sort + */ + bool isTuple() const; + + /** + * Is this a record sort? + * @return true if the sort is a record sort + */ + bool isRecord() const; + + /** + * Is this an array sort? + * @return true if the sort is a array sort + */ + bool isArray() const; + + /** + * Is this a Set sort? + * @return true if the sort is a Set sort + */ + bool isSet() const; + + /** + * Is this a sort kind? + * @return true if this is a sort kind + */ + bool isUninterpretedSort() const; + + /** + * Is this a sort constructor kind? + * @return true if this is a sort constructor kind + */ + bool isSortConstructor() const; + + /** + * @return the underlying datatype of a datatype sort + */ + Datatype getDatatype() const; + + /** + * Instantiate a parameterized datatype/sort sort. + * Create sorts parameter with Solver::mkParamSort(). + * @param params the list of sort parameters to instantiate with + */ + Sort instantiate(const std::vector<Sort>& params) const; + + /** + * Output a string representation of this sort to a given stream. + * @param out the output stream + */ + void toStream(std::ostream& out) const; + + /** + * @return a string representation of this sort + */ + std::string toString() const; + + private: + /** + * Constructor. + * @param t the internal type that is to be wrapped by this sort + * @return the Sort + */ + Sort(const CVC4::Type& t); + + /** + * The interal type wrapped by this sort. + * This is a shared_ptr rather than a unique_ptr to avoid overhead due to + * memory allocation (CVC4::Type is already ref counted, so this could be + * a unique_ptr instead). + */ + std::shared_ptr<CVC4::Type> d_type; +}; + +/** + * Serialize a sort to given stream. + * @param out the output stream + * @param s the sort to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_PUBLIC; + +/** + * Hash function for Sorts. + */ +struct CVC4_PUBLIC SortHashFunction +{ + size_t operator()(const Sort& s) const; +}; + +/* -------------------------------------------------------------------------- */ +/* Term */ +/* -------------------------------------------------------------------------- */ + +/** + * A CVC4 Term. + */ +class CVC4_PUBLIC Term +{ + friend class Datatype; + friend class DatatypeConstructor; + friend class Solver; + friend struct TermHashFunction; + + public: + /** + * Constructor. + */ + Term(); + + /** + * Destructor. + */ + ~Term(); + + /** + * Assignment operator, makes a copy of the given term. + * Both terms must belong to the same solver object. + * @param t the term to assign + * @return the reference to this term after assignment + */ + Term& operator=(const Term& t); + + /** + * Syntactic equality operator. + * Return true if both terms are syntactically identical. + * Both terms must belong to the same solver object. + * @param t the term to compare to for equality + * @return true if the terms are equal + */ + bool operator==(const Term& t) const; + + /** + * Syntactic disequality operator. + * Return true if both terms differ syntactically. + * Both terms must belong to the same solver object. + * @param t the term to compare to for disequality + * @return true if terms are disequal + */ + bool operator!=(const Term& t) const; + + /** + * @return the kind of this term + */ + Kind getKind() const; + + /** + * @return the sort of this term + */ + Sort getSort() const; + + /** + * @return true if this Term is a null term + */ + bool isNull() const; + + /** + * Boolean negation. + * @return the Boolean negation of this term + */ + Term notTerm() const; + + /** + * Boolean and. + * @param t a Boolean term + * @return the conjunction of this term and the given term + */ + Term andTerm(const Term& t) const; + + /** + * Boolean or. + * @param t a Boolean term + * @return the disjunction of this term and the given term + */ + Term orTerm(const Term& t) const; + + /** + * Boolean exclusive or. + * @param t a Boolean term + * @return the exclusive disjunction of this term and the given term + */ + Term xorTerm(const Term& t) const; + + /** + * Boolean if-and-only-if. + * @param t a Boolean term + * @return the Boolean equivalence of this term and the given term + */ + Term iffTerm(const Term& t) const; + + /** + * Boolean implication. + * @param t a Boolean term + * @return the implication of this term and the given term + */ + Term impTerm(const Term& t) const; + + /** + * If-then-else with this term as the Boolean condition. + * @param then_t the 'then' term + * @param else_t the 'else' term + * @return the if-then-else term with this term as the Boolean condition + */ + Term iteTerm(const Term& then_t, const Term& else_t) const; + + /** + * @return a string representation of this term + */ + std::string toString() const; + + /** + * Iterator for the children of a Term. + */ + class const_iterator : public std::iterator<std::input_iterator_tag, Term> + { + friend class Term; + + public: + /** + * Constructor. + */ + const_iterator(); + + /** + * Copy constructor. + */ + const_iterator(const const_iterator& it); + + /** + * Destructor. + */ + ~const_iterator(); + + /** + * Assignment operator. + * @param it the iterator to assign to + * @return the reference to the iterator after assignment + */ + const_iterator& operator=(const const_iterator& it); + + /** + * Equality operator. + * @param it the iterator to compare to for equality + * @return true if the iterators are equal + */ + bool operator==(const const_iterator& it) const; + + /** + * Disequality operator. + * @param it the iterator to compare to for disequality + * @return true if the iterators are disequal + */ + bool operator!=(const const_iterator& it) const; + + /** + * Increment operator (prefix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator& operator++(); + + /** + * Increment operator (postfix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator operator++(int); + + /** + * Dereference operator. + * @return the term this iterator points to + */ + Term operator*() const; + + private: + /* The internal expression iterator wrapped by this iterator. */ + void* d_iterator; + /* Constructor. */ + explicit const_iterator(void*); + }; + + /** + * @return an iterator to the first child of this Term + */ + const_iterator begin() const; + + /** + * @return an iterator to one-off-the-last child of this Term + */ + const_iterator end() const; + + private: + /** + * Constructor. + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + Term(const CVC4::Expr& e); + + /** + * The internal expression wrapped by this term. + * This is a shared_ptr rather than a unique_ptr to avoid overhead due to + * memory allocation (CVC4::Expr is already ref counted, so this could be + * a unique_ptr instead). + */ + std::shared_ptr<CVC4::Expr> d_expr; +}; + +/** + * Hash function for Terms. + */ +struct CVC4_PUBLIC TermHashFunction +{ + size_t operator()(const Term& t) const; +}; + +/** + * Serialize a term to given stream. + * @param out the output stream + * @param t the term to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_PUBLIC; + +/** + * Serialize a vector of terms to given stream. + * @param out the output stream + * @param vector the vector of terms to be serialized to the given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const std::vector<Term>& vector) CVC4_PUBLIC; + +/** + * Serialize a set of terms to the given stream. + * @param out the output stream + * @param set the set of terms to be serialized to the given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const std::set<Term>& set) CVC4_PUBLIC; + +/** + * Serialize an unordered_set of terms to the given stream. + * + * @param out the output stream + * @param unordered_set the set of terms to be serialized to the given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const std::unordered_set<Term, TermHashFunction>& + unordered_set) CVC4_PUBLIC; + +/** + * Serialize a map of terms to the given stream. + * + * @param out the output stream + * @param map the map of terms to be serialized to the given stream + * @return the output stream + */ +template <typename V> +std::ostream& operator<<(std::ostream& out, + const std::map<Term, V>& map) CVC4_PUBLIC; + +/** + * Serialize an unordered_map of terms to the given stream. + * + * @param out the output stream + * @param unordered_map the map of terms to be serialized to the given stream + * @return the output stream + */ +template <typename V> +std::ostream& operator<<(std::ostream& out, + const std::unordered_map<Term, V, TermHashFunction>& + unordered_map) CVC4_PUBLIC; + +/* -------------------------------------------------------------------------- */ +/* OpTerm */ +/* -------------------------------------------------------------------------- */ + +/** + * A CVC4 operator term. + * An operator term is a term that represents certain operators, instantiated + * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. + */ +class CVC4_PUBLIC OpTerm +{ + friend class Solver; + friend struct OpTermHashFunction; + + public: + /** + * Constructor. + */ + OpTerm(); + + /** + * Destructor. + */ + ~OpTerm(); + + /** + * Assignment operator, makes a copy of the given operator term. + * Both terms must belong to the same solver object. + * @param t the term to assign + * @return the reference to this operator term after assignment + */ + OpTerm& operator=(const OpTerm& t); + + /** + * Syntactic equality operator. + * Return true if both operator terms are syntactically identical. + * Both operator terms must belong to the same solver object. + * @param t the operator term to compare to for equality + * @return true if the operator terms are equal + */ + bool operator==(const OpTerm& t) const; + + /** + * Syntactic disequality operator. + * Return true if both operator terms differ syntactically. + * Both terms must belong to the same solver object. + * @param t the operator term to compare to for disequality + * @return true if operator terms are disequal + */ + bool operator!=(const OpTerm& t) const; + + /** + * @return the kind of this operator term + */ + Kind getKind() const; + + /** + * @return the sort of this operator term + */ + Sort getSort() const; + + /** + * @return true if this operator term is a null term + */ + bool isNull() const; + + /** + * @return a string representation of this operator term + */ + std::string toString() const; + + private: + /** + * Constructor. + * @param e the internal expression that is to be wrapped by this term + * @return the Term + */ + OpTerm(const CVC4::Expr& e); + + /** + * The internal expression wrapped by this operator term. + * This is a shared_ptr rather than a unique_ptr to avoid overhead due to + * memory allocation (CVC4::Expr is already ref counted, so this could be + * a unique_ptr instead). + */ + std::shared_ptr<CVC4::Expr> d_expr; +}; + +/** + * Serialize an operator term to given stream. + * @param out the output stream + * @param t the operator term to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const OpTerm& t) CVC4_PUBLIC; + +/** + * Hash function for OpTerms. + */ +struct CVC4_PUBLIC OpTermHashFunction +{ + size_t operator()(const OpTerm& t) const; +}; + +/* -------------------------------------------------------------------------- */ +/* Datatypes */ +/* -------------------------------------------------------------------------- */ + +class DatatypeConstructorIterator; +class DatatypeIterator; + +/** + * A place-holder sort to allow a DatatypeDecl to refer to itself. + * Self-sorted fields of DatatypeDecls will be properly sorted when a Sort is + * created for the DatatypeDecl. + */ +class CVC4_PUBLIC DatatypeDeclSelfSort +{ +}; + +/** + * A CVC4 datatype selector declaration. + */ +class CVC4_PUBLIC DatatypeSelectorDecl +{ + friend class DatatypeConstructorDecl; + + public: + /** + * Constructor. + * @param name the name of the datatype selector + * @param sort the sort of the datatype selector + * @return the DatatypeSelectorDecl + */ + DatatypeSelectorDecl(const std::string& name, Sort sort); + + /** + * Constructor. + * @param name the name of the datatype selector + * @param sort the sort of the datatype selector + * @return the DAtatypeSelectorDecl + */ + DatatypeSelectorDecl(const std::string& name, DatatypeDeclSelfSort sort); + + /** + * @return a string representation of this datatype selector + */ + std::string toString() const; + + private: + /* The name of the datatype selector. */ + std::string d_name; + /* The sort of the datatype selector. */ + Sort d_sort; +}; + +/** + * A CVC4 datatype constructor declaration. + */ +class CVC4_PUBLIC DatatypeConstructorDecl +{ + friend class DatatypeDecl; + + public: + /** + * Constructor. + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ + DatatypeConstructorDecl(const std::string& name); + + /** + * Add datatype selector declaration. + * @param stor the datatype selector declaration to add + */ + void addSelector(const DatatypeSelectorDecl& stor); + + /** + * @return a string representation of this datatype constructor declaration + */ + std::string toString() const; + + private: + /** + * The internal (intermediate) datatype constructor wrapped by this + * datatype constructor declaration. + * This is a shared_ptr rather than a unique_ptr since + * CVC4::DatatypeConstructor is not ref counted. + */ + std::shared_ptr<CVC4::DatatypeConstructor> d_ctor; +}; + +/** + * A CVC4 datatype declaration. + */ +class CVC4_PUBLIC DatatypeDecl +{ + friend class DatatypeConstructorArg; + friend class Solver; + + public: + /** + * Constructor. + * @param name the name of the datatype + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + DatatypeDecl(const std::string& name, bool isCoDatatype = false); + + /** + * Constructor for parameterized datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param param the sort parameter + * @param isCoDatatype true if a codatatype is to be constructed + */ + DatatypeDecl(const std::string& name, Sort param, bool isCoDatatype = false); + + /** + * Constructor for parameterized datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param params a list of sort parameters + * @param isCoDatatype true if a codatatype is to be constructed + */ + DatatypeDecl(const std::string& name, + const std::vector<Sort>& params, + bool isCoDatatype = false); + + /** + * Destructor. + */ + ~DatatypeDecl(); + + /** + * Add datatype constructor declaration. + * @param ctor the datatype constructor declaration to add + */ + void addConstructor(const DatatypeConstructorDecl& ctor); + + /** + * @return a string representation of this datatype declaration + */ + std::string toString() const; + + private: + /* The internal (intermediate) datatype wrapped by this datatype + * declaration + * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * not ref counted. + */ + std::shared_ptr<CVC4::Datatype> d_dtype; +}; + +/** + * A CVC4 datatype selector. + */ +class CVC4_PUBLIC DatatypeSelector +{ + friend class DatatypeConstructor; + friend class Solver; + + public: + /** + * Constructor. + */ + DatatypeSelector(); + + /** + * Destructor. + */ + ~DatatypeSelector(); + + /** + * @return a string representation of this datatype selector + */ + std::string toString() const; + + private: + /** + * Constructor. + * @param stor the internal datatype selector to be wrapped + * @return the DatatypeSelector + */ + DatatypeSelector(const CVC4::DatatypeConstructorArg& stor); + + /** + * The internal datatype selector wrapped by this datatype selector. + * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * not ref counted. + */ + std::shared_ptr<CVC4::DatatypeConstructorArg> d_stor; +}; + +/** + * A CVC4 datatype constructor. + */ +class CVC4_PUBLIC DatatypeConstructor +{ + friend class Datatype; + friend class Solver; + + public: + /** + * Constructor. + */ + DatatypeConstructor(); + + /** + * Destructor. + */ + ~DatatypeConstructor(); + + /** + * Get the datatype selector with the given name. + * This is a linear search through the selectors, so in case of + * multiple, similarly-named selectors, the first is returned. + * @param name the name of the datatype selector + * @return the first datatype selector with the given name + */ + DatatypeSelector operator[](const std::string& name) const; + DatatypeSelector getSelector(const std::string& name) const; + + /** + * Get the term representation of the datatype selector with the given name. + * This is a linear search through the arguments, so in case of multiple, + * similarly-named arguments, the selector for the first is returned. + * @param name the name of the datatype selector + * @return a term representing the datatype selector with the given name + */ + Term getSelectorTerm(const std::string& name) const; + + /** + * @return a string representation of this datatype constructor + */ + std::string toString() const; + + /** + * Iterator for the selectors of a datatype constructor. + */ + class const_iterator + : public std::iterator<std::input_iterator_tag, DatatypeConstructor> + { + friend class DatatypeConstructor; // to access constructor + + public: + /** + * Assignment operator. + * @param it the iterator to assign to + * @return the reference to the iterator after assignment + */ + const_iterator& operator=(const const_iterator& it); + + /** + * Equality operator. + * @param it the iterator to compare to for equality + * @return true if the iterators are equal + */ + bool operator==(const const_iterator& it) const; + + /** + * Disequality operator. + * @param it the iterator to compare to for disequality + * @return true if the iterators are disequal + */ + bool operator!=(const const_iterator& it) const; + + /** + * Increment operator (prefix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator& operator++(); + + /** + * Increment operator (postfix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator operator++(int); + + /** + * Dereference operator. + * @return a reference to the selector this iterator points to + */ + const DatatypeSelector& operator*() const; + + /** + * Dereference operator. + * @return a pointer to the selector this iterator points to + */ + const DatatypeSelector* operator->() const; + + private: + /** + * Constructor. + * @param ctor the internal datatype constructor to iterate over + * @param true if this is a begin() iterator + */ + const_iterator(const CVC4::DatatypeConstructor& ctor, bool begin); + /* A pointer to the list of selectors of the internal datatype + * constructor to iterate over. + * This pointer is maintained for operators == and != only. */ + const void* d_int_stors; + /* The list of datatype selector (wrappers) to iterate over. */ + std::vector<DatatypeSelector> d_stors; + /* The current index of the iterator. */ + size_t d_idx; + }; + + /** + * @return an iterator to the first selector of this constructor + */ + const_iterator begin() const; + + /** + * @return an iterator to one-off-the-last selector of this constructor + */ + const_iterator end() const; + + private: + /** + * Constructor. + * @param ctor the internal datatype constructor to be wrapped + * @return thte DatatypeConstructor + */ + DatatypeConstructor(const CVC4::DatatypeConstructor& ctor); + + /** + * The internal datatype constructor wrapped by this datatype constructor. + * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * not ref counted. + */ + std::shared_ptr<CVC4::DatatypeConstructor> d_ctor; +}; + +/* + * A CVC4 datatype. + */ +class CVC4_PUBLIC Datatype +{ + friend class Solver; + friend class Sort; + + public: + /** + * Destructor. + */ + ~Datatype(); + + /** + * Get the datatype constructor with the given name. + * This is a linear search through the constructors, so in case of multiple, + * similarly-named constructors, the first is returned. + * @param name the name of the datatype constructor + * @return the datatype constructor with the given name + */ + DatatypeConstructor operator[](const std::string& name) const; + DatatypeConstructor getConstructor(const std::string& name) const; + + /** + * Get a term representing the datatype constructor with the given name. + * This is a linear search through the constructors, so in case of multiple, + * similarly-named constructors, the + * first is returned. + */ + Term getConstructorTerm(const std::string& name) const; + + /** + * @return a string representation of this datatype + */ + std::string toString() const; + + /** + * Iterator for the constructors of a datatype. + */ + class const_iterator : public std::iterator<std::input_iterator_tag, Datatype> + { + friend class Datatype; // to access constructor + + public: + /** + * Assignment operator. + * @param it the iterator to assign to + * @return the reference to the iterator after assignment + */ + const_iterator& operator=(const const_iterator& it); + + /** + * Equality operator. + * @param it the iterator to compare to for equality + * @return true if the iterators are equal + */ + bool operator==(const const_iterator& it) const; + + /** + * Disequality operator. + * @param it the iterator to compare to for disequality + * @return true if the iterators are disequal + */ + bool operator!=(const const_iterator& it) const; + + /** + * Increment operator (prefix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator& operator++(); + + /** + * Increment operator (postfix). + * @return a reference to the iterator after incrementing by one + */ + const_iterator operator++(int); + + /** + * Dereference operator. + * @return a reference to the constructor this iterator points to + */ + const DatatypeConstructor& operator*() const; + + /** + * Dereference operator. + * @return a pointer to the constructor this iterator points to + */ + const DatatypeConstructor* operator->() const; + + private: + /** + * Constructor. + * @param dtype the internal datatype to iterate over + * @param true if this is a begin() iterator + */ + const_iterator(const CVC4::Datatype& dtype, bool begin); + /* A pointer to the list of constructors of the internal datatype + * to iterate over. + * This pointer is maintained for operators == and != only. */ + const void* d_int_ctors; + /* The list of datatype constructor (wrappers) to iterate over. */ + std::vector<DatatypeConstructor> d_ctors; + /* The current index of the iterator. */ + size_t d_idx; + }; + + /** + * @return an iterator to the first constructor of this datatype + */ + const_iterator begin() const; + + /** + * @return an iterator to one-off-the-last constructor of this datatype + */ + const_iterator end() const; + + private: + /** + * Constructor. + * @param dtype the internal datatype to be wrapped + * @return the Datatype + */ + Datatype(const CVC4::Datatype& dtype); + + /** + * The internal datatype wrapped by this datatype. + * This is a shared_ptr rather than a unique_ptr since CVC4::Datatype is + * not ref counted. + */ + std::shared_ptr<CVC4::Datatype> d_dtype; +}; + +/** + * Serialize a datatype declaration to given stream. + * @param out the output stream + * @param dtdecl the datatype declaration to be serialized to the given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const DatatypeDecl& dtdecl) CVC4_PUBLIC; + +/** + * Serialize a datatype constructor declaration to given stream. + * @param out the output stream + * @param ctordecl the datatype constructor declaration to be serialized + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const DatatypeConstructorDecl& ctordecl) CVC4_PUBLIC; + +/** + * Serialize a datatype selector declaration to given stream. + * @param out the output stream + * @param stordecl the datatype selector declaration to be serialized + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const DatatypeSelectorDecl& stordecl) CVC4_PUBLIC; + +/** + * Serialize a datatype to given stream. + * @param out the output stream + * @param dtdecl the datatype to be serialized to given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_PUBLIC; + +/** + * Serialize a datatype constructor to given stream. + * @param out the output stream + * @param ctor the datatype constructor to be serialized to given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const DatatypeConstructor& ctor) CVC4_PUBLIC; + +/** + * Serialize a datatype selector to given stream. + * @param out the output stream + * @param ctor the datatype selector to be serialized to given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const DatatypeSelector& stor) CVC4_PUBLIC; + +/* -------------------------------------------------------------------------- */ +/* Rounding Mode for Floating Points */ +/* -------------------------------------------------------------------------- */ + +/** + * A CVC4 floating point rounding mode. + */ +enum CVC4_PUBLIC RoundingMode +{ + ROUND_NEAREST_TIES_TO_EVEN, + ROUND_TOWARD_POSITIVE, + ROUND_TOWARD_NEGATIVE, + ROUND_TOWARD_ZERO, + ROUND_NEAREST_TIES_TO_AWAY, +}; + +/** + * Hash function for RoundingModes. + */ +struct CVC4_PUBLIC RoundingModeHashFunction +{ + inline size_t operator()(const RoundingMode& rm) const; +}; + +/* -------------------------------------------------------------------------- */ +/* Solver */ +/* -------------------------------------------------------------------------- */ + +/* + * A CVC4 solver. + */ +class CVC4_PUBLIC Solver +{ + public: + /* .................................................................... */ + /* Constructors/Destructors */ + /* .................................................................... */ + + /** + * Constructor. + * @param opts a pointer to a solver options object (for parser only) + * @return the Solver + */ + Solver(Options* opts = nullptr); + + /** + * Destructor. + */ + ~Solver(); + + /** + * Disallow copy/assignment. + */ + Solver(const Solver&) CVC4_UNDEFINED; + Solver& operator=(const Solver&) CVC4_UNDEFINED; + + /* .................................................................... */ + /* Sorts Handling */ + /* .................................................................... */ + + /** + * @return sort Boolean + */ + Sort getBooleanSort() const; + + /** + * @return sort Integer (in CVC4, Integer is a subtype of Real) + */ + Sort getIntegerSort() const; + + /** + * @return sort Real + */ + Sort getRealSort() const; + + /** + * @return sort RegExp + */ + Sort getRegExpSort() const; + + /** + * @return sort RoundingMode + */ + Sort getRoundingmodeSort() const; + + /** + * @return sort String + */ + Sort getStringSort() const; + + /** + * Create an array sort. + * @param indexSort the array index sort + * @param elemSort the array element sort + * @return the array sort + */ + Sort mkArraySort(Sort indexSort, Sort elemSort) const; + + /** + * Create a bit-vector sort. + * @param size the bit-width of the bit-vector sort + * @return the bit-vector sort + */ + Sort mkBitVectorSort(uint32_t size) const; + + /** + * Create a datatype sort. + * @param dtypedecl the datatype declaration from which the sort is created + * @return the datatype sort + */ + Sort mkDatatypeSort(DatatypeDecl dtypedecl) const; + + /** + * Create function sort. + * @param domain the sort of the fuction argument + * @param range the sort of the function return value + * @return the function sort + */ + Sort mkFunctionSort(Sort domain, Sort range) const; + + /** + * Create function sort. + * @param argSorts the sort of the function arguments + * @param range the sort of the function return value + * @return the function sort + */ + Sort mkFunctionSort(const std::vector<Sort>& argSorts, Sort range) const; + + /** + * Create a sort parameter. + * @param symbol the name of the sort + * @return the sort parameter + */ + Sort mkParamSort(const std::string& symbol) const; + + /** + * Create a predicate sort. + * @param sorts the list of sorts of the predicate + * @return the predicate sort + */ + Sort mkPredicateSort(const std::vector<Sort>& sorts) const; + + /** + * Create a record sort + * @param fields the list of fields of the record + * @return the record sort + */ + Sort mkRecordSort( + const std::vector<std::pair<std::string, Sort>>& fields) const; + + /** + * Create a set sort. + * @param elemSort the sort of the set elements + * @return the set sort + */ + Sort mkSetSort(Sort elemSort) const; + + /** + * Create an uninterpreted sort. + * @param symbol the name of the sort + * @return the uninterpreted sort + */ + Sort mkUninterpretedSort(const std::string& symbol) const; + + /** + * Create a tuple sort. + * @param sorts of the elements of the tuple + * @return the tuple sort + */ + Sort mkTupleSort(const std::vector<Sort>& sorts) const; + + /* .................................................................... */ + /* Create Terms */ + /* .................................................................... */ + + /** + * Create 0-ary term of given kind. + * @param kind the kind of the term + * @return the Term + */ + Term mkTerm(Kind kind) const; + + /** + * Create 0-ary term of given kind and sort. + * @param kind the kind of the term + * @param sort the sort argument to this kind + * @return the Term + */ + Term mkTerm(Kind kind, Sort sort) const; + + /** + * Create a unary term of given kind. + * @param kind the kind of the term + * @param child the child of the term + * @return the Term + */ + Term mkTerm(Kind kind, Term child) const; + + /** + * Create binary term of given kind. + * @param kind the kind of the term + * @param child1 the first child of the term + * @param child2 the second child of the term + * @return the Term + */ + Term mkTerm(Kind kind, Term child1, Term child2) const; + + /** + * Create ternary term of given kind. + * @param kind the kind of the term + * @param child1 the first child of the term + * @param child2 the second child of the term + * @param child3 the third child of the term + * @return the Term + */ + Term mkTerm(Kind kind, Term child1, Term child2, Term child3) const; + + /** + * Create n-ary term of given kind. + * @param kind the kind of the term + * @param children the children of the term + * @return the Term + */ + Term mkTerm(Kind kind, const std::vector<Term>& children) const; + + /** + * Create term with no children from a given operator term. + * Create operator terms with mkOpTerm(). + * @param the operator term + * @return the Term + */ + Term mkTerm(OpTerm opTerm) const; + + /** + * Create unary term from a given operator term. + * Create operator terms with mkOpTerm(). + * @param the operator term + * @child the child of the term + * @return the Term + */ + Term mkTerm(OpTerm opTerm, Term child) const; + + /** + * Create binary term from a given operator term. + * Create operator terms with mkOpTerm(). + * @param the operator term + * @child1 the first child of the term + * @child2 the second child of the term + * @return the Term + */ + Term mkTerm(OpTerm opTerm, Term child1, Term child2) const; + + /** + * Create ternary term from a given operator term. + * Create operator terms with mkOpTerm(). + * @param the operator term + * @child1 the first child of the term + * @child2 the second child of the term + * @child3 the third child of the term + * @return the Term + */ + Term mkTerm(OpTerm opTerm, Term child1, Term child2, Term child3) const; + + /** + * Create n-ary term from a given operator term. + * Create operator terms with mkOpTerm(). + * @param the operator term + * @children the children of the term + * @return the Term + */ + Term mkTerm(OpTerm opTerm, const std::vector<Term>& children) const; + + /* .................................................................... */ + /* Create Operator Terms */ + /* .................................................................... */ + + /** + * Create operator term of kind: + * - CHAIN_OP + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param k the kind argument to this operator + */ + OpTerm mkOpTerm(Kind kind, Kind k); + + /** + * Create operator of kind: + * - RECORD_UPDATE_OP + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg the string argument to this operator + */ + OpTerm mkOpTerm(Kind kind, const std::string& arg); + + /** + * Create operator of kind: + * - DIVISIBLE_OP + * - BITVECTOR_REPEAT_OP + * - BITVECTOR_ZERO_EXTEND_OP + * - BITVECTOR_SIGN_EXTEND_OP + * - BITVECTOR_ROTATE_LEFT_OP + * - BITVECTOR_ROTATE_RIGHT_OP + * - INT_TO_BITVECTOR_OP + * - FLOATINGPOINT_TO_UBV_OP + * - FLOATINGPOINT_TO_UBV_TOTAL_OP + * - FLOATINGPOINT_TO_SBV_OP + * - FLOATINGPOINT_TO_SBV_TOTAL_OP + * - TUPLE_UPDATE_OP + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg the uint32_t argument to this operator + */ + OpTerm mkOpTerm(Kind kind, uint32_t arg); + + /** + * Create operator of Kind: + * - BITVECTOR_EXTRACT_OP + * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP + * - FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP + * - FLOATINGPOINT_TO_FP_REAL_OP + * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP + * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP + * - FLOATINGPOINT_TO_FP_GENERIC_OP + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg1 the first uint32_t argument to this operator + * @param arg2 the second uint32_t argument to this operator + */ + OpTerm mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2); + + /* .................................................................... */ + /* Create Constants */ + /* .................................................................... */ + + /** + * Create a Boolean true constant. + * @return the true constant + */ + Term mkTrue() const; + + /** + * Create a Boolean false constant. + * @return the false constant + */ + Term mkFalse() const; + + /** + * Create a Boolean constant. + * @return the Boolean constant + * @param val the value of the constant + */ + Term mkBoolean(bool val) const; + + /** + * Create an Integer constant. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the Integer constant + */ + Term mkInteger(const char* s, uint32_t base = 10) const; + + /** + * Create an Integer constant. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the Integer constant + */ + Term mkInteger(const std::string& s, uint32_t base = 10) const; + + /** + * Create an Integer constant. + * @param val the value of the constant + * @return the Integer constant + */ + Term mkInteger(int32_t val) const; + + /** + * Create an Integer constant. + * @param val the value of the constant + * @return the Integer constant + */ + Term mkInteger(uint32_t val) const; + + /** + * Create an Integer constant. + * @param val the value of the constant + * @return the Integer constant + */ + Term mkInteger(int64_t val) const; + + /** + * Create an Integer constant. + * @param val the value of the constant + * @return the Integer constant + */ + Term mkInteger(uint64_t val) const; + + /** + * Create a constant representing the number Pi. + * @return a constant representing Pi + */ + Term mkPi() const; + + /** + * Create an Real constant. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the Real constant + */ + Term mkReal(const char* s, uint32_t base = 10) const; + + /** + * Create an Real constant. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the Real constant + */ + Term mkReal(const std::string& s, uint32_t base = 10) const; + + /** + * Create an Real constant. + * @param val the value of the constant + * @return the Real constant + */ + Term mkReal(int32_t val) const; + + /** + * Create an Real constant. + * @param val the value of the constant + * @return the Real constant + */ + Term mkReal(int64_t val) const; + + /** + * Create an Real constant. + * @param val the value of the constant + * @return the Real constant + */ + Term mkReal(uint32_t val) const; + + /** + * Create an Real constant. + * @param val the value of the constant + * @return the Real constant + */ + Term mkReal(uint64_t val) const; + + /** + * Create an Rational constant. + * @param num the value of the numerator + * @param den the value of the denominator + * @return the Rational constant + */ + Term mkReal(int32_t num, int32_t den) const; + + /** + * Create an Rational constant. + * @param num the value of the numerator + * @param den the value of the denominator + * @return the Rational constant + */ + Term mkReal(int64_t num, int64_t den) const; + + /** + * Create an Rational constant. + * @param num the value of the numerator + * @param den the value of the denominator + * @return the Rational constant + */ + Term mkReal(uint32_t num, uint32_t den) const; + + /** + * Create an Rational constant. + * @param num the value of the numerator + * @param den the value of the denominator + * @return the Rational constant + */ + Term mkReal(uint64_t num, uint64_t den) const; + + /** + * Create a regular expression empty term. + * @return the empty term + */ + Term mkRegexpEmpty() const; + + /** + * Create a regular expression sigma term. + * @return the sigma term + */ + Term mkRegexpSigma() const; + + /** + * Create a constant representing an empty set of the given sort. + * @param s the sort of the set elements. + * @return the empty set constant + */ + Term mkEmptySet(Sort s) const; + + /** + * Create a separation logic nil term. + * @param sort the sort of the nil term + * @return the separation logic nil term + */ + Term mkSepNil(Sort sort) const; + + /** + * Create a String constant. + * @param s the string this constant represents + * @return the String constant + */ + Term mkString(const char* s) const; + + /** + * Create a String constant. + * @param s the string this constant represents + * @return the String constant + */ + Term mkString(const std::string& s) const; + + /** + * Create a String constant. + * @param c the character this constant represents + * @return the String constant + */ + Term mkString(const unsigned char c) const; + + /** + * Create a String constant. + * @param s a list of unsigned values this constant represents as string + * @return the String constant + */ + Term mkString(const std::vector<unsigned>& s) const; + + /** + * Create a universe set of the given sort. + * @param sort the sort of the set elements + * @return the universe set constant + */ + Term mkUniverseSet(Sort sort) const; + + /** + * Create a bit-vector constant of given size with value 0. + * @param size the bit-width of the bit-vector sort + * @return the bit-vector constant + */ + Term mkBitVector(uint32_t size) const; + + /** + * Create a bit-vector constant of given size and value. + * @param size the bit-width of the bit-vector sort + * @param val the value of the constant + * @return the bit-vector constant + */ + Term mkBitVector(uint32_t size, uint32_t val) const; + + /** + * Create a bit-vector constant of given size and value. + * @param size the bit-width of the bit-vector sort + * @param val the value of the constant + * @return the bit-vector constant + */ + Term mkBitVector(uint32_t size, uint64_t val) const; + + /** + * Create a bit-vector constant from a given string. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the bit-vector constant + */ + Term mkBitVector(const char* s, uint32_t base = 2) const; + + /** + * Create a bit-vector constant from a given string. + * @param s the string represetntation of the constant + * @param base the base of the string representation + * @return the bit-vector constant + */ + Term mkBitVector(std::string& s, uint32_t base = 2) const; + + /** + * Create constant of kind: + * - CONST_ROUNDINGMODE + * @param rm the floating point rounding mode this constant represents + */ + Term mkConst(RoundingMode rm) const; + + /* + * Create constant of kind: + * - EMPTYSET + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, Sort arg) const; + + /** + * Create constant of kind: + * - UNINTERPRETED_CONSTANT + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, Sort arg1, int32_t arg2) const; + + /** + * Create constant of kind: + * - BOOLEAN + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, bool arg) const; + + /** + * Create constant of kind: + * - CONST_STRING + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, const char* arg) const; + + /** + * Create constant of kind: + * - CONST_STRING + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, const std::string& arg) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * - CONST_BITVECTOR + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, const char* arg1, uint32_t arg2 = 10) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * - CONST_BITVECTOR + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, const std::string& arg1, uint32_t arg2 = 10) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * - CONST_BITVECTOR + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, uint32_t arg) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, int32_t arg) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, int64_t arg) const; + + /** + * Create constant of kind: + * - ABSTRACT_VALUE + * - CONST_RATIONAL (for integers, reals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg the argument to this kind + */ + Term mkConst(Kind kind, uint64_t arg) const; + + /** + * Create constant of kind: + * - CONST_RATIONAL (for rationals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, int32_t arg1, int32_t arg2) const; + + /** + * Create constant of kind: + * - CONST_RATIONAL (for rationals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, int64_t arg1, int64_t arg2) const; + + /** + * Create constant of kind: + * - CONST_RATIONAL (for rationals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2) const; + + /** + * Create constant of kind: + * - CONST_RATIONAL (for rationals) + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, uint64_t arg1, uint64_t arg2) const; + + /** + * Create constant of kind: + * - CONST_BITVECTOR + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + */ + Term mkConst(Kind kind, uint32_t arg1, uint64_t arg2) const; + + /** + * Create constant of kind: + * - CONST_FLOATINGPOINT + * See enum Kind for a description of the parameters. + * @param kind the kind of the constant + * @param arg1 the first argument to this kind + * @param arg2 the second argument to this kind + * @param arg3 the third argument to this kind + */ + Term mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) const; + + /* .................................................................... */ + /* Create Variables */ + /* .................................................................... */ + + /** + * Create variable. + * @param symbol the name of the variable + * @param sort the sort of the variable + * @return the variable + */ + Term mkVar(const std::string& symbol, Sort sort) const; + + /** + * Create variable. + * @param sort the sort of the variable + * @return the variable + */ + Term mkVar(Sort sort) const; + + /** + * Create bound variable. + * @param symbol the name of the variable + * @param sort the sort of the variable + * @return the variable + */ + Term mkBoundVar(const std::string& symbol, Sort sort) const; + + /** + * Create bound variable. + * @param sort the sort of the variable + * @return the variable + */ + Term mkBoundVar(Sort sort) const; + + /* .................................................................... */ + /* Formula Handling */ + /* .................................................................... */ + + /** + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. + * @param t the formula to simplify + * @return the simplified formula + */ + Term simplify(const Term& t); + + /** + * Assert a formula. + * SMT-LIB: ( assert <term> ) + * @param term the formula to assert + */ + void assertFormula(Term term) const; + + /** + * Check satisfiability. + * SMT-LIB: ( check-sat ) + * @return the result of the satisfiability check. + */ + Result checkSat() const; + + /** + * Check satisfiability assuming the given formula. + * SMT-LIB: ( check-sat-assuming ( <prop_literal> ) ) + * @param assumption the formula to assume + * @return the result of the satisfiability check. + */ + Result checkSatAssuming(Term assumption) const; + + /** + * Check satisfiability assuming the given formulas. + * SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) ) + * @param assumptions the formulas to assume + * @return the result of the satisfiability check. + */ + Result checkSatAssuming(const std::vector<Term>& assumptions) const; + + /** + * Check validity. + * @return the result of the validity check. + */ + Result checkValid() const; + + /** + * Check validity assuming the given formula. + * @param assumption the formula to assume + * @return the result of the validity check. + */ + Result checkValidAssuming(Term assumption) const; + + /** + * Check validity assuming the given formulas. + * @param assumptions the formulas to assume + * @return the result of the validity check. + */ + Result checkValidAssuming(const std::vector<Term>& assumptions) const; + + /** + * Declare first-order constant (0-arity function symbol). + * SMT-LIB: ( declare-const <symbol> <sort> ) + * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) + * This command corresponds to mkVar(). + * @param symbol the name of the first-order constant + * @param sort the sort of the first-order constant + * @return the first-order constant + */ + Term declareConst(const std::string& symbol, Sort sort) const; + + /** + * Declare 0-arity function symbol. + * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) + * @param symbol the name of the function + * @param sort the sort of the return value of this function + * @return the function + */ + Term declareFun(const std::string& symbol, Sort sort) const; + + /** + * Declare n-ary function symbol. + * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> ) + * @param symbol the name of the function + * @param sorts the sorts of the parameters to this function + * @param sort the sort of the return value of this function + * @return the function + */ + Term declareFun(const std::string& symbol, + const std::vector<Sort>& sorts, + Sort sort) const; + + /** + * Declare uninterpreted sort. + * SMT-LIB: ( declare-sort <symbol> <numeral> ) + * @param symbol the name of the sort + * @param arity the arity of the sort + * @return the sort + */ + Sort declareSort(const std::string& symbol, uint32_t arity) const; + + /** + * Define n-ary function. + * SMT-LIB: ( define-fun <function_def> ) + * @param symbol the name of the function + * @param bound_vars the parameters to this function + * @param sort the sort of the return value of this function + * @param term the function body + * @return the function + */ + Term defineFun(const std::string& symbol, + const std::vector<Term>& bound_vars, + Sort sort, + Term term) const; + /** + * Define n-ary function. + * SMT-LIB: ( define-fun <function_def> ) + * Create parameter 'fun' with mkVar(). + * @param fun the sorted function + * @param bound_vars the parameters to this function + * @param term the function body + * @return the function + */ + Term defineFun(Term fun, + const std::vector<Term>& bound_vars, + Term term) const; + + /** + * Define recursive function. + * SMT-LIB: ( define-fun-rec <function_def> ) + * @param symbol the name of the function + * @param bound_vars the parameters to this function + * @param sort the sort of the return value of this function + * @param term the function body + * @return the function + */ + Term defineFunRec(const std::string& symbol, + const std::vector<Term>& bound_vars, + Sort sort, + Term term) const; + + /** + * Define recursive function. + * SMT-LIB: ( define-fun-rec <function_def> ) + * Create parameter 'fun' with mkVar(). + * @param fun the sorted function + * @param bound_vars the parameters to this function + * @param term the function body + * @return the function + */ + Term defineFunRec(Term fun, + const std::vector<Term>& bound_vars, + Term term) const; + + /** + * Define recursive functions. + * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) + * Create elements of parameter 'funs' with mkVar(). + * @param funs the sorted functions + * @param bound_vars the list of parameters to the functions + * @param term the list of function bodies of the functions + * @return the function + */ + void defineFunsRec(const std::vector<Term>& funs, + const std::vector<std::vector<Term>>& bound_vars, + const std::vector<Term>& terms) const; + + /** + * Echo a given string to the given output stream. + * SMT-LIB: ( echo <std::string> ) + * @param out the output stream + * @param str the string to echo + */ + void echo(std::ostream& out, const std::string& str) const; + + /** + * Get the list of asserted formulas. + * SMT-LIB: ( get-assertions ) + * @return the list of asserted formulas + */ + std::vector<Term> getAssertions() const; + + /** + * Get the assignment of asserted formulas. + * SMT-LIB: ( get-assignment ) + * Requires to enable option 'produce-assignments'. + * @return a list of formula-assignment pairs + */ + std::vector<std::pair<Term, Term>> getAssignment() const; + + /** + * Get info from the solver. + * SMT-LIB: ( get-info <info_flag> ) + * @return the info + */ + std::string getInfo(const std::string& flag) const; + + /** + * Get the value of a given option. + * SMT-LIB: ( get-option <keyword> ) + * @param option the option for which the value is queried + * @return a string representation of the option value + */ + std::string getOption(const std::string& option) const; + + /** + * Get the set of unsat ("failed") assumptions. + * SMT-LIB: ( get-unsat-assumptions ) + * Requires to enable option 'produce-unsat-assumptions'. + * @return the set of unsat assumptions. + */ + std::vector<Term> getUnsatAssumptions() const; + + /** + * Get the unsatisfiable core. + * SMT-LIB: ( get-unsat-core ) + * Requires to enable option 'produce-unsat-cores'. + * @return a set of terms representing the unsatisfiable core + */ + std::vector<Term> getUnsatCore() const; + + /** + * Get the value of the given term. + * SMT-LIB: ( get-value ( <term> ) ) + * @param term the term for which the value is queried + * @return the value of the given term + */ + Term getValue(Term term) const; + /** + * Get the values of the given terms. + * SMT-LIB: ( get-value ( <term>+ ) ) + * @param terms the terms for which the value is queried + * @return the values of the given terms + */ + std::vector<Term> getValue(const std::vector<Term>& terms) const; + + /** + * Pop (a) level(s) from the assertion stack. + * SMT-LIB: ( pop <numeral> ) + * @param nscopes the number of levels to pop + */ + void pop(uint32_t nscopes = 1) const; + + /** + * Print the model of a satisfiable query to the given output stream. + * Requires to enable option 'produce-models'. + * @param out the output stream + */ + void printModel(std::ostream& out) const; + + /** + * Push (a) level(s) to the assertion stack. + * SMT-LIB: ( push <numeral> ) + * @param nscopes the number of levels to push + */ + void push(uint32_t nscopes = 1) const; + + /** + * Reset the solver. + * SMT-LIB: ( reset ) + */ + void reset() const; + + /** + * Remove all assertions. + * SMT-LIB: ( reset-assertions ) + */ + void resetAssertions() const; + + /** + * Set info. + * SMT-LIB: ( set-info <attribute> ) + * @param keyword the info flag + * @param value the value of the info flag + */ + void setInfo(const std::string& keyword, const std::string& value) const; + + /** + * Set logic. + * SMT-LIB: ( set-logic <symbol> ) + * @param logic the logic to set + */ + void setLogic(const std::string& logic) const; + + /** + * Set option. + * SMT-LIB: ( set-option <option> ) + * @param option the option name + * @param value the option value + */ + void setOption(const std::string& option, const std::string& value) const; + + private: + /* Helper to convert a vector of internal types to sorts. */ + std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; + /* Helper to convert a vector of sorts to internal types. */ + std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const; + + /* The expression manager of this solver. */ + std::unique_ptr<ExprManager> d_exprMgr; + /* The SMT engine of this solver. */ + std::unique_ptr<SmtEngine> d_smtEngine; + /* The options of this solver. */ + std::unique_ptr<Options> d_opts; + /* The random number generator of this solver. */ + std::unique_ptr<Random> d_rng; +}; + +} // namespace api +} // namespace CVC4 +#endif diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h new file mode 100644 index 000000000..afa1e29f9 --- /dev/null +++ b/src/api/cvc4cppkind.h @@ -0,0 +1,2334 @@ +/********************* */ +/*! \file cvc4cpp.h + ** \verbatim + ** Top authors (to current version): Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The term kinds of the CVC4 C++ API. + ** + ** The term kinds of the CVC4 C++ API. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__API__CVC4CPPKIND_H +#define __CVC4__API__CVC4CPPKIND_H + +#include <ostream> + +namespace CVC4 { +namespace api { + +/* -------------------------------------------------------------------------- */ +/* Kind */ +/* -------------------------------------------------------------------------- */ + +/** + * The kind of a CVC4 term. + */ +enum CVC4_PUBLIC Kind +{ + /** + * Internal kind. + * Should never be exposed or created via the API. + */ + INTERNAL_KIND = -2, + /** + * Undefined kind. + * Should never be exposed or created via the API. + */ + UNDEFINED_KIND = -1, + /** + * Null kind (kind of null term Term()). + * Do not explicitly create via API functions other than Term(). + */ + NULL_EXPR, + + /* Builtin --------------------------------------------------------------- */ + + /** + * Uninterpreted constant. + * Parameters: 2 + * -[1]: Sort of the constant + * -[2]: Index of the constant + * Create with: + * mkConst(Kind, Sort, int32_t) + */ + UNINTERPRETED_CONSTANT, + /** + * Abstract value (other than uninterpreted sort constants). + * Parameters: 1 + * -[1]: Index of the abstract value + * Create with: + * mkConst(Kind kind, const char* s, uint32_t base = 10) + * mkConst(Kind kind, const std::string& s, uint32_t base = 10) + * mkConst(Kind kind, uint32_t arg) + * mkConst(Kind kind, int32_t arg) + * mkConst(Kind kind, int64_t arg) + * mkConst(Kind kind, uint64_t arg) + */ + ABSTRACT_VALUE, +#if 0 + /* Built-in operator */ + BUILTIN, +#endif + /** + * Defined function. + * Parameters: 3 (4) + * See defineFun(). + * Create with: + * defineFun(const std::string& symbol, + * const std::vector<Term>& bound_vars, + * Sort sort, + * Term term) + * defineFun(Term fun, + * const std::vector<Term>& bound_vars, + * Term term) + */ + FUNCTION, + /** + * Application of a defined function. + * Parameters: n > 1 + * -[1]..[n]: Function argument instantiation Terms + * Create with: + * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + APPLY, + /** + * Equality. + * Parameters: 2 + * -[1]..[2]: Terms with same sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + EQUAL, + /** + * Disequality. + * Parameters: n > 1 + * -[1]..[n]: Terms with same sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + DISTINCT, + /** + * Variable. + * Not permitted in bindings (forall, exists, ...). + * Parameters: + * See mkVar(). + * Create with: + * mkVar(const std::string& symbol, Sort sort) + * mkVar(Sort sort) + */ + VARIABLE, + /** + * Bound variable. + * Permitted in bindings and in the lambda and quantifier bodies only. + * Parameters: + * See mkBoundVar(). + * Create with: + * mkBoundVar(const std::string& symbol, Sort sort) + * mkBoundVar(Sort sort) + */ + BOUND_VARIABLE, +#if 0 + /* Skolem variable (internal only) */ + SKOLEM, + /* Symbolic expression (any arity) */ + SEXPR, +#endif + /** + * Lambda expression. + * Parameters: 2 + * -[1]: BOUND_VAR_LIST + * -[2]: Lambda body + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + LAMBDA, + /** + * Hilbert choice (epsilon) expression. + * Parameters: 2 + * -[1]: BOUND_VAR_LIST + * -[2]: Hilbert choice body + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + CHOICE, + /** + * Chained operation. + * Parameters: n > 1 + * -[1]: Term of kind CHAIN_OP (represents a binary op) + * -[2]..[n]: Arguments to that operator + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + * Turned into a conjunction of binary applications of the operator on + * adjoining parameters. + */ + CHAIN, + /** + * Chained operator. + * Parameters: 1 + * -[1]: Kind of the binary operation + * Create with: + * mkOpTerm(Kind opkind, Kind kind) + */ + CHAIN_OP, + + /* Boolean --------------------------------------------------------------- */ + + /** + * Boolean constant. + * Parameters: 1 + * -[1]: Boolean value of the constant + * Create with: + * mkTrue() + * mkFalse() + * mkBoolean(bool val) + * mkConst(Kind kind, bool arg) + */ + CONST_BOOLEAN, + /* Logical not. + * Parameters: 1 + * -[1]: Boolean Term to negate + * Create with: + * mkTerm(Kind kind, Term child) + */ + NOT, + /* Logical and. + * Parameters: n > 1 + * -[1]..[n]: Boolean Term of the conjunction + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + AND, + /** + * Logical implication. + * Parameters: 2 + * -[1]..[2]: Boolean Terms, [1] implies [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + IMPLIES, + /* Logical or. + * Parameters: n > 1 + * -[1]..[n]: Boolean Term of the disjunction + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + OR, + /* Logical exclusive or. + * Parameters: 2 + * -[1]..[2]: Boolean Terms, [1] xor [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + XOR, + /* If-then-else. + * Parameters: 3 + * -[1] is a Boolean condition Term + * -[2] the 'then' Term + * -[3] the 'else' Term + * 'then' and 'else' term must have same base sort. + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + ITE, + + /* UF -------------------------------------------------------------------- */ + + /* Application of an uninterpreted function. + * Parameters: n > 1 + * -[1]: Function Term + * -[2]..[n]: Function argument instantiation Terms + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + APPLY_UF, +#if 0 + /* Boolean term variable */ + BOOLEAN_TERM_VARIABLE, +#endif + /** + * Cardinality constraint on sort S. + * Parameters: 2 + * -[1]: Term of sort S + * -[2]: Positive integer constant that bounds the cardinality of sort S + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + CARDINALITY_CONSTRAINT, +#if 0 + /* Combined cardinality constraint. */ + COMBINED_CARDINALITY_CONSTRAINT, + /* Partial uninterpreted function application. */ + PARTIAL_APPLY_UF, + /* cardinality value of sort S: + * first parameter is (any) term of sort S */ + CARDINALITY_VALUE, +#endif + /** + * Higher-order applicative encoding of function application. + * Parameters: 2 + * -[1]: Function to apply + * -[2]: Argument of the function + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + HO_APPLY, + + /* Arithmetic ------------------------------------------------------------ */ + + /** + * Arithmetic addition. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + PLUS, + /** + * Arithmetic multiplication. + * Parameters: n > 1 + * -[1]..[n]: Terms of sort Integer, Real (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + MULT, +#if 0 + /* Synonym for MULT. */ + NONLINEAR_MULT, +#endif + /** + * Arithmetic subtraction. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + MINUS, + /** + * Arithmetic negation. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + UMINUS, + /** + * Real division, division by 0 undefined + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + DIVISION, + /** + * Real division with interpreted division by 0 + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + DIVISION_TOTAL, + /** + * Integer division, division by 0 undefined. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INTS_DIVISION, + /** + * Integer division with interpreted division by 0. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INTS_DIVISION_TOTAL, + /** + * Integer modulus, division by 0 undefined. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INTS_MODULUS, + /** + * Integer modulus with interpreted division by 0. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INTS_MODULUS_TOTAL, + /** + * Absolute value. + * Parameters: 1 + * -[1]: Term of sort Integer + * Create with: + * mkTerm(Kind kind, Term child) + */ + ABS, + /** + * Divisibility-by-k predicate. + * Parameters: 2 + * -[1]: DIVISIBLE_OP Term + * -[2]: Integer Term + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + DIVISIBLE, + /** + * Arithmetic power. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + POW, + /** + * Exponential. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + EXPONENTIAL, + /** + * Sine. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + SINE, + /** + * Cosine. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + COSINE, + /** + * Tangent. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + TANGENT, + /** + * Cosecant. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + COSECANT, + /** + * Secant. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + SECANT, + /** + * Cotangent. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + COTANGENT, + /** + * Arc sine. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCSINE, + /** + * Arc cosine. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCCOSINE, + /** + * Arc tangent. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCTANGENT, + /** + * Arc cosecant. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCCOSECANT, + /** + * Arc secant. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCSECANT, + /** + * Arc cotangent. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + ARCCOTANGENT, + /** + * Square root. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + SQRT, + /** + * Operator for the divisibility-by-k predicate. + * Parameter: 1 + * -[1]: The k to divide by (sort Integer) + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + DIVISIBLE_OP, + /** + * Multiple-precision rational constant. + * Parameters: + * See mkInteger(), mkReal(), mkRational() + * Create with: + * mkInteger(const char* s, uint32_t base = 10) + * mkInteger(const std::string& s, uint32_t base = 10) + * mkInteger(int32_t val) + * mkInteger(uint32_t val) + * mkInteger(int64_t val) + * mkInteger(uint64_t val) + * mkReal(const char* s, uint32_t base = 10) + * mkReal(const std::string& s, uint32_t base = 10) + * mkReal(int32_t val) + * mkReal(int64_t val) + * mkReal(uint32_t val) + * mkReal(uint64_t val) + * mkRational(int32_t num, int32_t den) + * mkRational(int64_t num, int64_t den) + * mkRational(uint32_t num, uint32_t den) + * mkRational(uint64_t num, uint64_t den) + * mkConst(Kind kind, const char* s, uint32_t base = 10) + * mkConst(Kind kind, const std::string& s, uint32_t base = 10) + * mkConst(Kind kind, uint32_t arg) + * mkConst(Kind kind, int64_t arg) + * mkConst(Kind kind, uint64_t arg) + * mkConst(Kind kind, int32_t arg) + * mkConst(Kind kind, int32_t arg1, int32_t arg2) + * mkConst(Kind kind, int64_t arg1, int64_t arg2) + * mkConst(Kind kind, uint32_t arg1, uint32_t arg2) + * mkConst(Kind kind, uint64_t arg1, uint64_t arg2) + */ + CONST_RATIONAL, + /** + * Less than. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real; [1] < [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + LT, + /** + * Less than or equal. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real; [1] <= [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + LEQ, + /** + * Greater than. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real, [1] > [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + GT, + /** + * Greater than or equal. + * Parameters: 2 + * -[1]..[2]: Terms of sort Integer, Real; [1] >= [2] + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + GEQ, + /** + * Is-integer predicate. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + IS_INTEGER, + /** + * Convert Term to Integer by the floor function. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * Create with: + * mkTerm(Kind kind, Term child) + */ + TO_INTEGER, + /** + * Convert Term to Real. + * Parameters: 1 + * -[1]: Term of sort Integer, Real + * This is a no-op in CVC4, as Integer is a subtype of Real. + */ + TO_REAL, + /** + * Pi constant. + * Create with: + * mkPi() + * mkTerm(Kind kind) + */ + PI, + + /* BV -------------------------------------------------------------------- */ + + /** + * Fixed-size bit-vector constant. + * Parameters: + * See mkBitVector(). + * Create with: + * mkBitVector(uint32_t size) + * mkBitVector(uint32_t size, uint32_t val) + * mkBitVector(uint32_t size, uint64_t val) + * mkBitVector(const char* s, uint32_t base = 2) + * mkBitVector(std::string& s, uint32_t base = 2) + * mkConst(Kind kind, const char* s, uint32_t base = 10) + * mkConst(Kind kind, const std::string& s, uint32_t base = 10) + * mkConst(Kind kind, uint32_t arg) + * mkConst(Kind kind, uint32_t arg1, uint64_t arg2) + */ + CONST_BITVECTOR, + /** + * Concatenation of two or more bit-vectors. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_CONCAT, + /** + * Bit-wise and. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_AND, + /** + * Bit-wise or. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_OR, + /** + * Bit-wise xor. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_XOR, + /** + * Bit-wise negation. + * Parameters: 1 + * -[1]: Term of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BITVECTOR_NOT, + /** + * Bit-wise nand. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_NAND, + /** + * Bit-wise nor. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_NOR, + /** + * Bit-wise xnor. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_XNOR, + /** + * Equality comparison (returns bit-vector of size 1). + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_COMP, + /** + * Multiplication of two or more bit-vectors. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_MULT, + /** + * Addition of two or more bit-vectors. + * Parameters: n > 1 + * -[1]..[n]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_PLUS, + /** + * Subtraction of two bit-vectors. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SUB, + /** + * Negation of a bit-vector (two's complement). + * Parameters: 1 + * -[1]: Term of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BITVECTOR_NEG, + /** + * Unsigned division of two bit-vectors, truncating towards 0. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UDIV, + /** + * Unsigned remainder from truncating division of two bit-vectors. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UREM, + /** + * Two's complement signed division of two bit-vectors. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SDIV, + /** + * Two's complement signed remainder of two bit-vectors + * (sign follows dividend). + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SREM, + /** + * Two's complement signed remainder + * (sign follows divisor). + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SMOD, + /** + * Unsigned division of two bit-vectors, truncating towards 0 + * (defined to be the all-ones bit pattern, if divisor is 0). + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UDIV_TOTAL, + /** + * Unsigned remainder from truncating division of two bit-vectors + * (defined to be equal to the dividend, if divisor is 0). + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UREM_TOTAL, + /** + * Bit-vector shift left. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SHL, + /** + * Bit-vector logical shift right. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_LSHR, + /** + * Bit-vector arithmetic shift right. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_ASHR, + /** + * Bit-vector unsigned less than. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_ULT, + /** + * Bit-vector unsigned less than or equal. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_ULE, + /** + * Bit-vector unsigned greater than. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UGT, + /** + * Bit-vector unsigned greater than or equal. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_UGE, + /* Bit-vector signed less than. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SLT, + /** + * Bit-vector signed less than or equal. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SLE, + /** + * Bit-vector signed greater than. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SGT, + /** + * Bit-vector signed greater than or equal. + * The two bit-vector parameters must have same width. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SGE, + /** + * Bit-vector unsigned less than, returns bit-vector of size 1. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_ULTBV, + /** + * Bit-vector signed less than. returns bit-vector of size 1. + * Parameters: 2 + * -[1]..[2]: Terms of bit-vector sort (sorts must match) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_SLTBV, + /** + * Same semantics as regular ITE, but condition is bit-vector of size 1. + * Parameters: 3 + * -[1]: Term of bit-vector sort of size 1, representing the condition + * -[2]: Term reprsenting the 'then' branch + * -[3]: Term representing the 'else' branch + * 'then' and 'else' term must have same base sort. + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + BITVECTOR_ITE, + /** + * Bit-vector redor. + * Parameters: 1 + * -[1]: Term of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BITVECTOR_REDOR, + /** + * Bit-vector redand. + * Parameters: 1 + * -[1]: Term of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BITVECTOR_REDAND, +#if 0 + /* formula to be treated as a bv atom via eager bit-blasting + * (internal-only symbol) */ + BITVECTOR_EAGER_ATOM, + /* term to be treated as a variable. used for eager bit-blasting Ackermann + * expansion of bvudiv (internal-only symbol) */ + BITVECTOR_ACKERMANIZE_UDIV, + /* term to be treated as a variable. used for eager bit-blasting Ackermann + * expansion of bvurem (internal-only symbol) */ + BITVECTOR_ACKERMANIZE_UREM, + /* operator for the bit-vector boolean bit extract. + * One parameter, parameter is the index of the bit to extract */ + BITVECTOR_BITOF_OP, +#endif + /** + * Operator for bit-vector extract (from index 'high' to 'low'). + * Parameters: 2 + * -[1]: The 'high' index + * -[2]: The 'low' index + * Create with: + * mkOpTerm(Kind kind, uint32_t param, uint32_t param) + */ + BITVECTOR_EXTRACT_OP, + /** + * Operator for bit-vector repeat. + * Parameter 1: + * -[1]: Number of times to repeat a given bit-vector + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + BITVECTOR_REPEAT_OP, + /** + * Operator for bit-vector zero-extend. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be extended + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + BITVECTOR_ZERO_EXTEND_OP, + /** + * Operator for bit-vector sign-extend. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be extended + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + BITVECTOR_SIGN_EXTEND_OP, + /** + * Operator for bit-vector rotate left. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be rotated + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + BITVECTOR_ROTATE_LEFT_OP, + /** + * Operator for bit-vector rotate right. + * Parameter 1: + * -[1]: Number of bits by which a given bit-vector is to be rotated + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + BITVECTOR_ROTATE_RIGHT_OP, +#if 0 + /* bit-vector boolean bit extract. + * first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term */ + BITVECTOR_BITOF, +#endif + /* Bit-vector extract. + * Parameters: 2 + * -[1]: BITVECTOR_EXTRACT_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_EXTRACT, + /* Bit-vector repeat. + * Parameters: 2 + * -[1]: BITVECTOR_REPEAT_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_REPEAT, + /* Bit-vector zero-extend. + * Parameters: 2 + * -[1]: BITVECTOR_ZERO_EXTEND_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_ZERO_EXTEND, + /* Bit-vector sign-extend. + * Parameters: 2 + * -[1]: BITVECTOR_SIGN_EXTEND_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_SIGN_EXTEND, + /* Bit-vector rotate left. + * Parameters: 2 + * -[1]: BITVECTOR_ROTATE_LEFT_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_ROTATE_LEFT, + /** + * Bit-vector rotate right. + * Parameters: 2 + * -[1]: BITVECTOR_ROTATE_RIGHT_OP Term + * -[2]: Term of bit-vector sort + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + BITVECTOR_ROTATE_RIGHT, + /** + * Operator for the conversion from Integer to bit-vector. + * Parameter: 1 + * -[1]: Size of the bit-vector to convert to + * Create with: + * mkOpTerm(Kind kind, uint32_t param). + */ + INT_TO_BITVECTOR_OP, + /** + * Integer conversion to bit-vector. + * Parameters: 2 + * -[1]: INT_TO_BITVECTOR_OP Term + * -[2]: Integer term + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INT_TO_BITVECTOR, + /** + * Bit-vector conversion to (nonnegative) integer. + * Parameter: 1 + * -[1]: Term of bit-vector sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + BITVECTOR_TO_NAT, + + /* FP -------------------------------------------------------------------- */ + + /** + * Floating-point constant, constructed from a double or string. + * Parameters: 3 + * -[1]: Size of the exponent + * -[2]: Size of the significand + * -[3]: Value of the floating-point constant as a bit-vector term + * Create with: + * mkConst(Kind kind, uint32_t arg1, uint32_t arg2, Term arg3) + */ + CONST_FLOATINGPOINT, + /** + * Floating-point rounding mode term. + * Create with: + * mkConst(RoundingMode rm) + */ + CONST_ROUNDINGMODE, + /** + * Create floating-point literal from bit-vector triple. + * Parameters: 3 + * -[1]: Sign bit as a bit-vector term + * -[2]: Exponent bits as a bit-vector term + * -[3]: Significand bits as a bit-vector term (without hidden bit) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_FP, + /** + * Floating-point equality. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_EQ, + /** + * Floating-point absolute value. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ABS, + /** + * Floating-point negation. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_NEG, + /** + * Floating-point addition. + * Parameters: 3 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * -[3]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_PLUS, + /** + * Floating-point sutraction. + * Parameters: 3 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * -[3]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_SUB, + /** + * Floating-point multiply. + * Parameters: 3 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * -[3]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_MULT, + /** + * Floating-point division. + * Parameters: 3 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * -[3]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_DIV, + /** + * Floating-point fused multiply and add. + * Parameters: 4 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * -[3]: Term of sort FloatingPoint + * -[4]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_FMA, + /** + * Floating-point square root. + * Parameters: 2 + * -[1]: CONST_ROUNDINGMODE + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_SQRT, + /** + * Floating-point remainder. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_REM, + /** + * Floating-point round to integral. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_RTI, + /** + * Floating-point minimum. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_MIN, + /** + * Floating-point maximum. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_MAX, +#if 0 + /* floating-point minimum (defined for all inputs) */ + FLOATINGPOINT_MIN_TOTAL, + /* floating-point maximum (defined for all inputs) */ + FLOATINGPOINT_MAX_TOTAL, +#endif + /** + * Floating-point less than or equal. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_LEQ, + /** + * Floating-point less than. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_LT, + /** + * Floating-point greater than or equal. + * Parameters: 2 + * -[1]..[2]: Terms of floating point sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_GEQ, + /** + * Floating-point greater than. + * Parameters: 2 + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FLOATINGPOINT_GT, + /** + * Floating-point is normal. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISN, + /** + * Floating-point is sub-normal. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISSN, + /** + * Floating-point is zero. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISZ, + /** + * Floating-point is infinite. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISINF, + /** + * Floating-point is NaN. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISNAN, + /** + * Floating-point is negative. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISNEG, + /** + * Floating-point is positive. + * Parameters: 1 + * -[1]: Term of floating point sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_ISPOS, + /** + * Operator for to_fp from bit vector. + * Parameters: 2 + * -[1]: Exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, + /** + * Conversion from an IEEE-754 bit vector to floating-point. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + /** + * Operator for to_fp from floating point. + * Parameters: 2 + * -[1]: Exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, + /** + * Conversion between floating-point sorts. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_FLOATINGPOINT, + /** + * Operator for to_fp from real. + * Parameters: 2 + * -[1]: Exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_REAL_OP, + /** + * Conversion from a real to floating-point. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_REAL_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_REAL, + /* + * Operator for to_fp from signed bit vector. + * Parameters: 2 + * -[1]: Exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, + /** + * Conversion from a signed bit vector to floating-point. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + /** + * Operator for to_fp from unsigned bit vector. + * Parameters: 2 + * -[1]: Exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, + /** + * Operator for converting an unsigned bit vector to floating-point. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + /** + * Operator for a generic to_fp. + * Parameters: 2 + * -[1]: exponent size + * -[2]: Significand size + * Create with: + * mkOpTerm(Kind kind, uint32_t param1, uint32_t param2) + */ + FLOATINGPOINT_TO_FP_GENERIC_OP, + /** + * Generic conversion to floating-point, used in parsing only. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_GENERIC_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_FP_GENERIC, + /** + * Operator for to_ubv. + * Parameters: 1 + * -[1]: Size of the bit-vector to convert to + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + FLOATINGPOINT_TO_UBV_OP, + /** + * Conversion from a floating-point value to an unsigned bit vector. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_UBV, + /** + * Operator for to_ubv_total. + * Parameters: 1 + * -[1]: Size of the bit-vector to convert to + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + FLOATINGPOINT_TO_UBV_TOTAL_OP, + /** + * Conversion from a floating-point value to an unsigned bit vector + * (defined for all inputs). + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_TO_UBV_TOTAL_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_UBV_TOTAL, + /** + * Operator for to_sbv. + * Parameters: 1 + * -[1]: Size of the bit-vector to convert to + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + FLOATINGPOINT_TO_SBV_OP, + /** + * Conversion from a floating-point value to a signed bit vector. + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_SBV, + /** + * Operator for to_sbv_total. + * Parameters: 1 + * -[1]: Size of the bit-vector to convert to + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + FLOATINGPOINT_TO_SBV_TOTAL_OP, + /** + * Conversion from a floating-point value to a signed bit vector + * (defined for all inputs). + * Parameters: 2 + * -[1]: FLOATINGPOINT_TO_FP_TO_SBV_TOTAL_OP Term + * -[2]: Term of sort FloatingPoint + * Create with: + * mkTerm(Term opTerm, Term child) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + FLOATINGPOINT_TO_SBV_TOTAL, + /** + * Floating-point to real. + * Parameters: 1 + * -[1]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_TO_REAL, + /** + * Floating-point to real (defined for all inputs). + * Parameters: 1 + * -[1]: Term of sort FloatingPoint + * Create with: + * mkTerm(Kind kind, Term child) + */ + FLOATINGPOINT_TO_REAL_TOTAL, + + /* Arrays ---------------------------------------------------------------- */ + + /** + * Aarray select. + * Parameters: 2 + * -[1]: Term of array sort + * -[2]: Selection index + * Create with: + * mkTerm(Term opTerm, Term child1, Term child2) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + SELECT, + /** + * Array store. + * Parameters: 3 + * -[1]: Term of array sort + * -[2]: Store index + * -[3]: Term to store at the index + * Create with: + * mkTerm(Term opTerm, Term child1, Term child2, Term child3) + * mkTerm(Term opTerm, const std::vector<Term>& children) + */ + STORE, + /** + * Constant array. + * Parameters: 2 + * -[1]: Array sort + * -[2]: Term representing a constant + * Create with: + * mkTerm(Term opTerm, Term child1, Term child2) + * mkTerm(Term opTerm, const std::vector<Term>& children) + * + * Note: We currently support the creation of constant arrays, but under some + * conditions when there is a chain of equalities connecting two constant + * arrays, the solver doesn't know what to do and aborts (Issue #1667). + */ + STORE_ALL, +#if 0 + /* array table function (internal-only symbol) */ + ARR_TABLE_FUN, + /* array lambda (internal-only symbol) */ + ARRAY_LAMBDA, + /* partial array select, for internal use only */ + PARTIAL_SELECT_0, + /* partial array select, for internal use only */ + PARTIAL_SELECT_1, +#endif + + /* Datatypes ------------------------------------------------------------- */ + + /** + * Constructor application. + * Paramters: n > 0 + * -[1]: Constructor + * -[2]..[n]: Parameters to the constructor + * Create with: + * mkTerm(Kind kind) + * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + APPLY_SELECTOR, + /** + * Datatype selector application. + * Parameters: 1 + * -[1]: Datatype term (undefined if mis-applied) + * Create with: + * mkTerm(Kind kind, Term child) + */ + APPLY_CONSTRUCTOR, + /** + * Datatype selector application. + * Parameters: 1 + * -[1]: Datatype term (defined rigidly if mis-applied) + * Create with: + * mkTerm(Kind kind, Term child) + */ + APPLY_SELECTOR_TOTAL, + /** + * Datatype tester application. + * Parameters: 2 + * -[1]: Tester term + * -[2]: Datatype term + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + APPLY_TESTER, +#if 0 + /* Parametric datatype term. */ + PARAMETRIC_DATATYPE, + /* type ascription, for datatype constructor applications; + * first parameter is an ASCRIPTION_TYPE, second is the datatype constructor + * application being ascribed */ + APPLY_TYPE_ASCRIPTION, +#endif + /** + * Operator for a tuple update. + * Parameters: 1 + * -[1]: Index of the tuple to be updated + * Create with: + * mkOpTerm(Kind kind, uint32_t param) + */ + TUPLE_UPDATE_OP, + /** + * Tuple update. + * Parameters: 3 + * -[1]: TUPLE_UPDATE_OP (which references an index) + * -[2]: Tuple + * -[3]: Element to store in the tuple at the given index + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + TUPLE_UPDATE, + /** + * Operator for a record update. + * Parameters: 1 + * -[1]: Name of the field to be updated + * Create with: + * mkOpTerm(Kind kind, const std::string& param) + */ + RECORD_UPDATE_OP, + /** + * Record update. + * Parameters: 3 + * -[1]: RECORD_UPDATE_OP Term (which references a field) + * -[2]: Record term to update + * -[3]: Element to store in the record in the given field + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + RECORD_UPDATE, +#if 0 + /* datatypes size */ + DT_SIZE, + /* datatypes height bound */ + DT_HEIGHT_BOUND, + /* datatypes height bound */ + DT_SIZE_BOUND, + /* datatypes sygus bound */ + DT_SYGUS_BOUND, + /* datatypes sygus term order */ + DT_SYGUS_TERM_ORDER, + /* datatypes sygus is constant */ + DT_SYGUS_IS_CONST, +#endif + + /* Separation Logic ------------------------------------------------------ */ + + /** + * Separation logic nil term. + * Parameters: 0 + * Create with: + * mkSepNil(Sort sort) + * mkTerm(Kind kind, Sort sort) + */ + SEP_NIL, + /** + * Separation logic empty heap. + * Parameters: 2 + * -[1]: Term of the same sort as the sort of the location of the heap + * that is constrained to be empty + * -[2]: Term of the same sort as the data sort of the heap that is + * that is constrained to be empty + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SEP_EMP, + /** + * Separation logic points-to relation. + * Parameters: 2 + * -[1]: Location of the points-to constraint + * -[2]: Data of the points-to constraint + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SEP_PTO, + /** + * Separation logic star. + * Parameters: n >= 2 + * -[1]..[n]: Child constraints that hold in disjoint (separated) heaps + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SEP_STAR, + /** + * Separation logic magic wand. + * Parameters: 2 + * -[1]: Antecendant of the magic wand constraint + * -[2]: Conclusion of the magic wand constraint, which is asserted to + * hold in all heaps that are disjoint extensions of the antecedent. + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SEP_WAND, +#if 0 + /* separation label (internal use only) */ + SEP_LABEL, +#endif + + /* Sets ------------------------------------------------------------------ */ + + /** + * Empty set constant. + * Parameters: 1 + * -[1]: Sort of the set elements + * Create with: + * mkEmptySet(Sort sort) + * mkConst(Sort sort) + */ + EMPTYSET, + /** + * Set union. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + UNION, + /** + * Set intersection. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INTERSECTION, + /** + * Set subtraction. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SETMINUS, + /** + * Subset predicate. + * Parameters: 2 + * -[1]..[2]: Terms of set sort, [1] a subset of set [2]? + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + SUBSET, + /** + * Set membership predicate. + * Parameters: 2 + * -[1]..[2]: Terms of set sort, [1] a member of set [2]? + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + MEMBER, + /** + * The set of the single element given as a parameter. + * Parameters: 1 + * -[1]: Single element + * Create with: + * mkTerm(Kind kind, Term child) + */ + SINGLETON, + /** + * The set obtained by inserting elements; + * Parameters: n > 0 + * -[1]..[n-1]: Elements inserted into set [n] + * -[n]: Set Term + * Create with: + * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + INSERT, + /** + * Set cardinality. + * Parameters: 1 + * -[1]: Set to determine the cardinality of + * Create with: + * mkTerm(Kind kind, Term child) + */ + CARD, + /** + * Set complement with respect to finite universe. + * Parameters: 1 + * -[1]: Set to complement + * Create with: + * mkTerm(Kind kind, Term child) + */ + COMPLEMENT, + /** + * Finite universe set. + * All set variables must be interpreted as subsets of it. + * Create with: + * mkUniverseSet(Sort sort) + * mkTerm(Kind kind, Sort sort) + */ + UNIVERSE_SET, + /** + * Set join. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + JOIN, + /** + * Set cartesian product. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + PRODUCT, + /** + * Set transpose. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + TRANSPOSE, + /** + * Set transitive closure. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + TCLOSURE, + /** + * Set join image. + * Parameters: 2 + * -[1]..[2]: Terms of set sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + JOIN_IMAGE, + /** + * Set identity. + * Parameters: 1 + * -[1]: Term of set sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + IDEN, + + /* Strings --------------------------------------------------------------- */ + + /** + * String concat. + * Parameters: n > 1 + * -[1]..[n]: Terms of String sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_CONCAT, + /** + * String membership. + * Parameters: 2 + * -[1]..[2]: Terms of String sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_IN_REGEXP, + /** + * String length. + * Parameters: 1 + * -[1]: Term of String sort + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_LENGTH, + /** + * String substring. + * Extracts a substring, starting at index i and of length l, from a string + * s. If the start index is negative, the start index is greater than the + * length of the string, or the length is negative, the result is the empty + * string. + * Parameters: 3 + * -[1]: Term of sort String + * -[2]: Term of sort Integer (index i) + * -[3]: Term of sort Integer (length l) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_SUBSTR, + /** + * String character at. + * Returns the character at index i from a string s. If the index is negative + * or the index is greater than the length of the string, the result is the + * empty string. Otherwise the result is a string of length 1. + * Parameters: 2 + * -[1]: Term of sort String (string s) + * -[2]: Term of sort Integer (index i) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_CHARAT, + /** + * String contains. + * Checks whether a string s1 contains another string s2. If s2 is empty, the + * result is always true. + * Parameters: 2 + * -[1]: Term of sort String (the string s1) + * -[2]: Term of sort String (the string s2) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_STRCTN, + /** + * String index-of. + * Returns the index of a substring s2 in a string s1 starting at index i. If + * the index is negative or greater than the length of string s1 or the + * substring s2 does not appear in string s1 after index i, the result is -1. + * Parameters: 3 + * -[1]: Term of sort String (substring s1) + * -[2]: Term of sort String (substring s2) + * -[3]: Term of sort Integer (index i) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_STRIDOF, + /** + * String replace. + * Replaces a string s2 in a string s1 with string s3. If s2 does not appear + * in s1, s1 is returned unmodified. + * Parameters: 3 + * -[1]: Term of sort String (string s1) + * -[2]: Term of sort String (string s2) + * -[3]: Term of sort String (string s3) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_STRREPL, + /** + * String prefix-of. + * Checks whether a string s1 is a prefix of string s2. If string s1 is + * empty, this operator returns true. + * Parameters: 2 + * -[1]: Term of sort String (string s1) + * -[2]: Term of sort String (string s2) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_PREFIX, + /** + * String suffix-of. + * Checks whether a string s1 is a suffix of string 2. If string s1 is empty, + * this operator returns true. + * Parameters: 2 + * -[1]: Term of sort String (string s1) + * -[2]: Term of sort String (string s2) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + STRING_SUFFIX, + /** + * Integer to string. + * If the integer is negative this operator returns the empty string. + * Parameters: 1 + * -[1]: Term of sort Integer + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_ITOS, + /** + * String to integer (total function). + * If the string does not contain an integer or the integer is negative, the + * operator returns -1. + * Parameters: 1 + * -[1]: Term of sort String + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_STOI, + /** + * Constant string. + * Parameters: + * See mkString() + * Create with: + * mkString(const char* s) + * mkString(const std::string& s) + * mkString(const unsigned char c) + * mkString(const std::vector<unsigned>& s) + * mkConst(Kind kind, const char* s) + * mkConst(Kind kind, const std::string& s) + */ + CONST_STRING, + /** + * Conversion from string to regexp. + * Parameters: 1 + * -[1]: Term of sort String + * Create with: + * mkTerm(Kind kind, Term child) + */ + STRING_TO_REGEXP, + /** + * Regexp Concatenation . + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_CONCAT, + /** + * Regexp union. + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_UNION, + /** + * Regexp intersection. + * Parameters: 2 + * -[1]..[2]: Terms of Regexp sort + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_INTER, + /** + * Regexp *. + * Parameters: 1 + * -[1]: Term of sort Regexp + * Create with: + * mkTerm(Kind kind, Term child) + */ + REGEXP_STAR, + /** + * Regexp +. + * Parameters: 1 + * -[1]: Term of sort Regexp + * Create with: + * mkTerm(Kind kind, Term child) + */ + REGEXP_PLUS, + /** + * Regexp ?. + * Parameters: 1 + * -[1]: Term of sort Regexp + * Create with: + * mkTerm(Kind kind, Term child) + */ + REGEXP_OPT, + /** + * Regexp range. + * Parameters: 2 + * -[1]: Lower bound character for the range + * -[2]: Upper bound character for the range + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_RANGE, + /** + * Regexp loop. + * Parameters: 2 (3) + * -[1]: Term of sort RegExp + * -[2]: Lower bound for the number of repetitions of the first argument + * -[3]: Upper bound for the number of repetitions of the first argument + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + REGEXP_LOOP, + /** + * Regexp empty. + * Parameters: 0 + * Create with: + * mkRegexpEmpty() + * mkTerm(Kind kind) + */ + REGEXP_EMPTY, + /** + * Regexp all characters. + * Parameters: 0 + * Create with: + * mkRegexpSigma() + * mkTerm(Kind kind) + */ + REGEXP_SIGMA, +#if 0 + /* regexp rv (internal use only) */ + REGEXP_RV, +#endif + + /* Quantifiers ----------------------------------------------------------- */ + + /** + * Universally quantified formula. + * Parameters: 2 (3) + * -[1]: BOUND_VAR_LIST Term + * -[2]: Quantifier body + * -[3]: (optional) INST_PATTERN_LIST Term + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + FORALL, + /** + * Existentially quantified formula. + * Parameters: 2 (3) + * -[1]: BOUND_VAR_LIST Term + * -[2]: Quantifier body + * -[3]: (optional) INST_PATTERN_LIST Term + * Create with: + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector<Term>& children) + */ + EXISTS, +#if 0 + /* instantiation constant */ + INST_CONSTANT, + /* instantiation pattern */ + INST_PATTERN, + /* a list of bound variables (used to bind variables under a quantifier) */ + BOUND_VAR_LIST, + /* instantiation no-pattern */ + INST_NO_PATTERN, + /* instantiation attribute */ + INST_ATTRIBUTE, + /* a list of instantiation patterns */ + INST_PATTERN_LIST, + /* predicate for specifying term in instantiation closure. */ + INST_CLOSURE, + /* general rewrite rule (for rewrite-rules theory) */ + REWRITE_RULE, + /* actual rewrite rule (for rewrite-rules theory) */ + RR_REWRITE, + /* actual reduction rule (for rewrite-rules theory) */ + RR_REDUCTION, + /* actual deduction rule (for rewrite-rules theory) */ + RR_DEDUCTION, + + /* Sort Kinds ------------------------------------------------------------ */ + + /* array type */ + ARRAY_TYPE, + /* a type parameter for type ascription */ + ASCRIPTION_TYPE, + /* constructor */ + CONSTRUCTOR_TYPE, + /* a datatype type index */ + DATATYPE_TYPE, + /* selector */ + SELECTOR_TYPE, + /* set type, takes as parameter the type of the elements */ + SET_TYPE, + /* sort tag */ + SORT_TAG, + /* specifies types of user-declared 'uninterpreted' sorts */ + SORT_TYPE, + /* tester */ + TESTER_TYPE, + /* a representation for basic types */ + TYPE_CONSTANT, + /* a function type */ + FUNCTION_TYPE, + /* the type of a symbolic expression */ + SEXPR_TYPE, + /* bit-vector type */ + BITVECTOR_TYPE, + /* floating-point type */ + FLOATINGPOINT_TYPE, +#endif + + /* ----------------------------------------------------------------------- */ + /* marks the upper-bound of this enumeration */ + LAST_KIND +}; + +/** + * Serialize a kind to given stream. + * @param out the output stream + * @param k the kind to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, Kind k) CVC4_PUBLIC; + +/** + * Hash function for Kinds. + */ +struct CVC4_PUBLIC KindHashFunction +{ + size_t operator()(Kind k) const; +}; + +} // namespace api +} // namespace CVC4 + +#endif |