c++ api: Expose TermManager to the API.

docs/api/cpp/cpp.rst

@@ -31,6 +31,7 @@ For most applications, the :cpp:class:`Solver <cvc5::Solver>` class is the main
     statistics
     synthresult
     term
+    termmanager
     unknownexplanation
 
 
@@ -53,14 +54,15 @@ Class hierarchy
   * class :ref:`api/cpp/datatypedecl:datatypedecl`
   * class :ref:`api/cpp/datatypeselector:datatypeselector`
   * class :ref:`api/cpp/driveroptions:driveroptions`
-  * class :ref:`api/cpp/grammar:grammar`  
+  * class :ref:`api/cpp/grammar:grammar`
   * class :ref:`api/cpp/op:op`
   * class :ref:`api/cpp/optioninfo:optioninfo`
   * class :ref:`api/cpp/result:result`
+  * class :ref:`api/cpp/termmanager:termmanager`
   * class :ref:`api/cpp/solver:solver`
   * class :ref:`api/cpp/sort:sort`
   * class :cpp:class:`Stat <cvc5::Stat>`
-  * class :cpp:class:`Statistics <cvc5::Statistics>`  
+  * class :cpp:class:`Statistics <cvc5::Statistics>`
   * class :ref:`api/cpp/synthresult:synthresult`
   * class :ref:`api/cpp/term:term`
 

docs/api/cpp/quickstart.rst

@@ -1,7 +1,15 @@
 Quickstart Guide
 ================
 
-First, create a cvc5 :cpp:class:`Solver <cvc5::Solver>` instance:
+First, create a cvc5 :cpp:class:`TermManager <cvc5::TermManager>` instance:
+
+.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
+   :language: cpp
+   :dedent: 2
+   :start-after: docs-cpp-quickstart-0 start
+   :end-before: docs-cpp-quickstart-0 end
+
+Then, create a cvc5 :cpp:class:`Solver <cvc5::Solver>` instance:
 
 .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp
    :language: cpp

docs/api/cpp/solver.rst

@@ -5,9 +5,8 @@ This class represents a cvc5 solver instance.
 
 :cpp:class:`Terms <cvc5::Term>`, :cpp:class:`Sorts <cvc5::Sort>` and
 :cpp:class:`Ops <cvc5::Op>` are not tied to a :cpp:class:`cvc5::Solver`
-instance and can be shared between instances.
-Term kinds are defined via enum class :doc:`cvc5::Kind <kind>`, and sort kinds
-via enum class :doc:`cvc5::SortKind <sortkind>`.
+but associated with a :cpp:class:`cvc5::TermManager` instance, which can be
+shared between solver instances.
 
 Solver options are configured via :cpp:func:`cvc5::Solver::setOption()`
 and queried via :cpp:func:`cvc5::Solver::getOption()`

docs/api/cpp/termmanager.rst

@@ -0,0 +1,27 @@
+TermManager
+===========
+
+This class represents a cvc5 term manager instance.
+
+:cpp:class:`Terms <cvc5::Term>`, :cpp:class:`Sorts <cvc5::Sort>` and
+:cpp:class:`Ops <cvc5::Op>` are not tied to a :cpp:class:`cvc5::Solver`
+but associated with a :cpp:class:`cvc5::TermManager` instance, which can be
+shared between solver instances (and thus allows sharing of terms and sorts
+between solver instances).
+
+Term kinds are defined via enum class :doc:`cvc5::Kind <kind>`, and sort kinds
+via enum class :doc:`cvc5::SortKind <sortkind>`.
+
+Solver options are configured via :cpp:func:`cvc5::Solver::setOption()`
+and queried via :cpp:func:`cvc5::Solver::getOption()`
+(for more information on configuration options, see :doc:`../../options`).
+Information about a specific option can be retrieved via
+:cpp:func:`cvc5::getOptionInfo()` (see :doc:`optioninfo`).
+
+----
+
+.. doxygenclass:: cvc5::TermManager
+    :project: cvc5
+    :members:
+    :undoc-members:
+

examples/api/cpp/bags.cpp

@@ -22,28 +22,29 @@ using namespace cvc5;
 
 int main()
 {
-  Solver slv;
+  TermManager tm;
+  Solver slv(tm);
   slv.setLogic("ALL");
   // Produce models
   slv.setOption("produce-models", "true");
   slv.setOption("incremental", "true");
 
-  Sort bag = slv.mkBagSort(slv.getStringSort());
-  Term A = slv.mkConst(bag, "A");
-  Term B = slv.mkConst(bag, "B");
-  Term C = slv.mkConst(bag, "C");
-  Term x = slv.mkConst(slv.getStringSort(), "x");
+  Sort bag = tm.mkBagSort(tm.getStringSort());
+  Term A = tm.mkConst(bag, "A");
+  Term B = tm.mkConst(bag, "B");
+  Term C = tm.mkConst(bag, "C");
+  Term x = tm.mkConst(tm.getStringSort(), "x");
 
-  Term intersectionAC = slv.mkTerm(Kind::BAG_INTER_MIN, {A, C});
-  Term intersectionBC = slv.mkTerm(Kind::BAG_INTER_MIN, {B, C});
+  Term intersectionAC = tm.mkTerm(Kind::BAG_INTER_MIN, {A, C});
+  Term intersectionBC = tm.mkTerm(Kind::BAG_INTER_MIN, {B, C});
 
   // union disjoint does not distribute over intersection
   {
-    Term unionDisjointAB = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {A, B});
-    Term lhs = slv.mkTerm(Kind::BAG_INTER_MIN, {unionDisjointAB, C});
+    Term unionDisjointAB = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {A, B});
+    Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionDisjointAB, C});
     Term rhs =
-        slv.mkTerm(Kind::BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
-    Term guess = slv.mkTerm(Kind::EQUAL, {lhs, rhs});
+        tm.mkTerm(Kind::BAG_UNION_DISJOINT, {intersectionAC, intersectionBC});
+    Term guess = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
     cout << "cvc5 reports: " << guess.notTerm() << " is "
          << slv.checkSatAssuming(guess.notTerm()) << "." << endl;
 
@@ -56,19 +57,18 @@ int main()
 
   // union max distributes over intersection
   {
-    Term unionMaxAB = slv.mkTerm(Kind::BAG_UNION_MAX, {A, B});
-    Term lhs = slv.mkTerm(Kind::BAG_INTER_MIN, {unionMaxAB, C});
-    Term rhs =
-        slv.mkTerm(Kind::BAG_UNION_MAX, {intersectionAC, intersectionBC});
-    Term theorem = slv.mkTerm(Kind::EQUAL, {lhs, rhs});
+    Term unionMaxAB = tm.mkTerm(Kind::BAG_UNION_MAX, {A, B});
+    Term lhs = tm.mkTerm(Kind::BAG_INTER_MIN, {unionMaxAB, C});
+    Term rhs = tm.mkTerm(Kind::BAG_UNION_MAX, {intersectionAC, intersectionBC});
+    Term theorem = tm.mkTerm(Kind::EQUAL, {lhs, rhs});
     cout << "cvc5 reports: " << theorem.notTerm() << " is "
          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
   }
 
   // Verify emptbag is a subbag of any bag
   {
-    Term emptybag = slv.mkEmptyBag(bag);
-    Term theorem = slv.mkTerm(Kind::BAG_SUBBAG, {emptybag, A});
+    Term emptybag = tm.mkEmptyBag(bag);
+    Term theorem = tm.mkTerm(Kind::BAG_SUBBAG, {emptybag, A});
 
     cout << "cvc5 reports: " << theorem.notTerm() << " is "
          << slv.checkSatAssuming(theorem.notTerm()) << "." << endl;
@@ -78,25 +78,25 @@ int main()
   // ; {|"a", "a", "b", "b", "b"|} and {|"b", "c", "c"|}
 
   {
-    Term one = slv.mkInteger(1);
-    Term two = slv.mkInteger(2);
-    Term three = slv.mkInteger(3);
-    Term four = slv.mkInteger(4);
-    Term a = slv.mkString("a");
-    Term b = slv.mkString("b");
-    Term c = slv.mkString("c");
-
-    Term bag_a_2 = slv.mkTerm(Kind::BAG_MAKE, {a, two});
-    Term bag_b_3 = slv.mkTerm(Kind::BAG_MAKE, {b, three});
-    Term bag_b_1 = slv.mkTerm(Kind::BAG_MAKE, {b, one});
-    Term bag_c_2 = slv.mkTerm(Kind::BAG_MAKE, {c, two});
-    Term bag_a_2_b_3 = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
-    Term bag_b_1_c_2 = slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
+    Term one = tm.mkInteger(1);
+    Term two = tm.mkInteger(2);
+    Term three = tm.mkInteger(3);
+    Term four = tm.mkInteger(4);
+    Term a = tm.mkString("a");
+    Term b = tm.mkString("b");
+    Term c = tm.mkString("c");
+
+    Term bag_a_2 = tm.mkTerm(Kind::BAG_MAKE, {a, two});
+    Term bag_b_3 = tm.mkTerm(Kind::BAG_MAKE, {b, three});
+    Term bag_b_1 = tm.mkTerm(Kind::BAG_MAKE, {b, one});
+    Term bag_c_2 = tm.mkTerm(Kind::BAG_MAKE, {c, two});
+    Term bag_a_2_b_3 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2, bag_b_3});
+    Term bag_b_1_c_2 = tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_b_1, bag_c_2});
     Term union_disjoint =
-        slv.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
+        tm.mkTerm(Kind::BAG_UNION_DISJOINT, {bag_a_2_b_3, bag_b_1_c_2});
 
-    Term count_x = slv.mkTerm(Kind::BAG_COUNT, {x, union_disjoint});
-    Term e = slv.mkTerm(Kind::EQUAL, {four, count_x});
+    Term count_x = tm.mkTerm(Kind::BAG_COUNT, {x, union_disjoint});
+    Term e = tm.mkTerm(Kind::EQUAL, {four, count_x});
     Result result = slv.checkSatAssuming(e);
 
     cout << "cvc5 reports: " << e << " is " << result << "." << endl;

examples/api/cpp/bitvectors.cpp

@@ -24,7 +24,8 @@ using namespace cvc5;
 
 int main()
 {
-  Solver slv;
+  TermManager tm;
+  Solver slv(tm);
   slv.setLogic("QF_BV");  // Set the logic
 
   // The following example has been adapted from the book A Hacker's Delight by
@@ -47,30 +48,30 @@ int main()
   // equivalent by encoding the problem in the bit-vector theory.
 
   // Creating a bit-vector type of width 32
-  Sort bitvector32 = slv.mkBitVectorSort(32);
+  Sort bitvector32 = tm.mkBitVectorSort(32);
 
   // Variables
-  Term x = slv.mkConst(bitvector32, "x");
-  Term a = slv.mkConst(bitvector32, "a");
-  Term b = slv.mkConst(bitvector32, "b");
+  Term x = tm.mkConst(bitvector32, "x");
+  Term a = tm.mkConst(bitvector32, "a");
+  Term b = tm.mkConst(bitvector32, "b");
 
   // First encode the assumption that x must be equal to a or b
-  Term x_eq_a = slv.mkTerm(Kind::EQUAL, {x, a});
-  Term x_eq_b = slv.mkTerm(Kind::EQUAL, {x, b});
-  Term assumption = slv.mkTerm(Kind::OR, {x_eq_a, x_eq_b});
+  Term x_eq_a = tm.mkTerm(Kind::EQUAL, {x, a});
+  Term x_eq_b = tm.mkTerm(Kind::EQUAL, {x, b});
+  Term assumption = tm.mkTerm(Kind::OR, {x_eq_a, x_eq_b});
 
   // Assert the assumption
   slv.assertFormula(assumption);
 
   // Introduce a new variable for the new value of x after assignment.
-  Term new_x = slv.mkConst(bitvector32, "new_x");  // x after executing code (0)
+  Term new_x = tm.mkConst(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkConst(bitvector32, "new_x_");  // x after executing code (1) or (2)
+      tm.mkConst(bitvector32, "new_x_");  // x after executing code (1) or (2)
 
   // Encoding code (0)
   // new_x = x == a ? b : a;
-  Term ite = slv.mkTerm(Kind::ITE, {x_eq_a, b, a});
-  Term assignment0 = slv.mkTerm(Kind::EQUAL, {new_x, ite});
+  Term ite = tm.mkTerm(Kind::ITE, {x_eq_a, b, a});
+  Term assignment0 = tm.mkTerm(Kind::EQUAL, {new_x, ite});
 
   // Assert the encoding of code (0)
   cout << "Asserting " << assignment0 << " to cvc5 " << endl;
@@ -80,13 +81,13 @@ int main()
 
   // Encoding code (1)
   // new_x_ = a xor b xor x
-  Term a_xor_b_xor_x = slv.mkTerm(Kind::BITVECTOR_XOR, {a, b, x});
-  Term assignment1 = slv.mkTerm(Kind::EQUAL, {new_x_, a_xor_b_xor_x});
+  Term a_xor_b_xor_x = tm.mkTerm(Kind::BITVECTOR_XOR, {a, b, x});
+  Term assignment1 = tm.mkTerm(Kind::EQUAL, {new_x_, a_xor_b_xor_x});
 
   // Assert encoding to cvc5 in current context;
   cout << "Asserting " << assignment1 << " to cvc5 " << endl;
   slv.assertFormula(assignment1);
-  Term new_x_eq_new_x_ = slv.mkTerm(Kind::EQUAL, {new_x, new_x_});
+  Term new_x_eq_new_x_ = tm.mkTerm(Kind::EQUAL, {new_x, new_x_});
 
   cout << " Check sat assuming: " << new_x_eq_new_x_.notTerm() << endl;
   cout << " Expect UNSAT. " << endl;
@@ -96,9 +97,9 @@ int main()
 
   // Encoding code (2)
   // new_x_ = a + b - x
-  Term a_plus_b = slv.mkTerm(Kind::BITVECTOR_ADD, {a, b});
-  Term a_plus_b_minus_x = slv.mkTerm(Kind::BITVECTOR_SUB, {a_plus_b, x});
-  Term assignment2 = slv.mkTerm(Kind::EQUAL, {new_x_, a_plus_b_minus_x});
+  Term a_plus_b = tm.mkTerm(Kind::BITVECTOR_ADD, {a, b});
+  Term a_plus_b_minus_x = tm.mkTerm(Kind::BITVECTOR_SUB, {a_plus_b, x});
+  Term assignment2 = tm.mkTerm(Kind::EQUAL, {new_x_, a_plus_b_minus_x});
 
   // Assert encoding to cvc5 in current context;
   cout << "Asserting " << assignment2 << " to cvc5 " << endl;
@@ -108,18 +109,18 @@ int main()
   cout << " Expect UNSAT. " << endl;
   cout << " cvc5: " << slv.checkSatAssuming(new_x_eq_new_x_.notTerm()) << endl;
 
-  Term x_neq_x = slv.mkTerm(Kind::EQUAL, {x, x}).notTerm();
+  Term x_neq_x = tm.mkTerm(Kind::EQUAL, {x, x}).notTerm();
   std::vector<Term> v{new_x_eq_new_x_, x_neq_x};
-  Term query = slv.mkTerm(Kind::AND, {v});
+  Term query = tm.mkTerm(Kind::AND, {v});
   cout << " Check sat assuming: " << query.notTerm() << endl;
   cout << " Expect SAT. " << endl;
   cout << " cvc5: " << slv.checkSatAssuming(query.notTerm()) << endl;
 
   // Assert that a is odd
-  Op extract_op = slv.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
-  Term lsb_of_a = slv.mkTerm(extract_op, {a});
+  Op extract_op = tm.mkOp(Kind::BITVECTOR_EXTRACT, {0, 0});
+  Term lsb_of_a = tm.mkTerm(extract_op, {a});
   cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl;
-  Term a_odd = slv.mkTerm(Kind::EQUAL, {lsb_of_a, slv.mkBitVector(1u, 1u)});
+  Term a_odd = tm.mkTerm(Kind::EQUAL, {lsb_of_a, tm.mkBitVector(1u, 1u)});
   cout << "Assert " << a_odd << endl;
   cout << "Check satisfiability." << endl;
   slv.assertFormula(a_odd);

examples/api/cpp/bitvectors_and_arrays.cpp

@@ -25,7 +25,8 @@ using namespace cvc5;
 
 int main()
 {
-  Solver slv;
+  TermManager tm;
+  Solver slv(tm);
   slv.setOption("produce-models", "true");      // Produce Models
   slv.setOption("output-language", "smtlib"); // output-language
   slv.setLogic("QF_AUFBV");                   // Set the logic
@@ -48,48 +49,48 @@ int main()
 
 
   // Sorts
-  Sort elementSort = slv.mkBitVectorSort(32);
-  Sort indexSort = slv.mkBitVectorSort(index_size);
-  Sort arraySort = slv.mkArraySort(indexSort, elementSort);
+  Sort elementSort = tm.mkBitVectorSort(32);
+  Sort indexSort = tm.mkBitVectorSort(index_size);
+  Sort arraySort = tm.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkConst(arraySort, "current_array");
+  Term current_array = tm.mkConst(arraySort, "current_array");
 
   // Making a bit-vector constant
-  Term zero = slv.mkBitVector(index_size, 0u);
+  Term zero = tm.mkBitVector(index_size, 0u);
 
   // Asserting that current_array[0] > 0
-  Term current_array0 = slv.mkTerm(Kind::SELECT, {current_array, zero});
-  Term current_array0_gt_0 = slv.mkTerm(
-      Kind::BITVECTOR_SGT, {current_array0, slv.mkBitVector(32, 0u)});
+  Term current_array0 = tm.mkTerm(Kind::SELECT, {current_array, zero});
+  Term current_array0_gt_0 = tm.mkTerm(
+      Kind::BITVECTOR_SGT, {current_array0, tm.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(Kind::SELECT, {current_array, index});
-  Term two = slv.mkBitVector(32, 2u);
+  Term index = tm.mkBitVector(index_size, 0u);
+  Term old_current = tm.mkTerm(Kind::SELECT, {current_array, index});
+  Term two = tm.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(Kind::BITVECTOR_MULT, {two, old_current});
+    index = tm.mkBitVector(index_size, i);
+    Term new_current = tm.mkTerm(Kind::BITVECTOR_MULT, {two, old_current});
     // current[i] = 2 * current[i-1]
     current_array =
-        slv.mkTerm(Kind::STORE, {current_array, index, new_current});
+        tm.mkTerm(Kind::STORE, {current_array, index, new_current});
     // current[i-1] < current [i]
     Term current_slt_new_current =
-        slv.mkTerm(Kind::BITVECTOR_SLT, {old_current, new_current});
+        tm.mkTerm(Kind::BITVECTOR_SLT, {old_current, new_current});
     assertions.push_back(current_slt_new_current);
 
-    old_current = slv.mkTerm(Kind::SELECT, {current_array, index});
+    old_current = tm.mkTerm(Kind::SELECT, {current_array, index});
   }
 
-  Term query = slv.mkTerm(Kind::NOT, {slv.mkTerm(Kind::AND, assertions)});
+  Term query = tm.mkTerm(Kind::NOT, {tm.mkTerm(Kind::AND, assertions)});
 
   cout << "Asserting " << query << " to cvc5 " << endl;
   slv.assertFormula(query);
   cout << "Expect sat. " << endl;
-  cout << "cvc5: " << slv.checkSatAssuming(slv.mkTrue()) << endl;
+  cout << "cvc5: " << slv.checkSatAssuming(tm.mkTrue()) << endl;
 
   // Getting the model
   cout << "The satisfying model is: " << endl;