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