New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

4 files changed, 298 insertions, 51 deletions

diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index b404dfb13..c9eaf103e 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -43,10 +43,10 @@ void DatatypeBlack::tearDown() {}
 void DatatypeBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort listSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype d = listSort.getDatatype();
@@ -75,22 +75,22 @@ void DatatypeBlack::testMkDatatypeSorts()
   unresTypes.insert(unresList);
 
   DatatypeDecl tree = d_solver.mkDatatypeDecl("tree");
-  DatatypeConstructorDecl node("node");
+  DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node");
   node.addSelector("left", unresTree);
   node.addSelector("right", unresTree);
   tree.addConstructor(node);
 
-  DatatypeConstructorDecl leaf("leaf");
+  DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf");
   leaf.addSelector("data", unresList);
   tree.addConstructor(leaf);
 
   DatatypeDecl list = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("car", unresTree);
   cons.addSelector("cdr", unresTree);
   list.addConstructor(cons);
 
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   list.addConstructor(nil);
 
   std::vector<DatatypeDecl> dtdecls;
@@ -130,13 +130,13 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
   TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
@@ -152,11 +152,11 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
-  DatatypeConstructorDecl ca("A");
+  DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A");
   dtypeSpecEnum.addConstructor(ca);
-  DatatypeConstructorDecl cb("B");
+  DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B");
   dtypeSpecEnum.addConstructor(cb);
-  DatatypeConstructorDecl cc("C");
+  DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C");
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
@@ -165,7 +165,8 @@ void DatatypeBlack::testDatatypeStructs()
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
-  DatatypeConstructorDecl consStream("cons");
+  DatatypeConstructorDecl consStream =
+      d_solver.mkDatatypeConstructorDecl("cons");
   consStream.addSelector("head", intSort);
   consStream.addSelectorSelf("tail");
   dtypeSpecStream.addConstructor(consStream);
@@ -204,11 +205,11 @@ void DatatypeBlack::testDatatypeNames()
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
   TS_ASSERT(dtypeSpec.getName() == std::string("list"));
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 90d4c10c1..7e925df54 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -39,6 +39,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkBitVectorSort();
   void testMkFloatingPointSort();
   void testMkDatatypeSort();
+  void testMkDatatypeSorts();
   void testMkFunctionSort();
   void testMkOp();
   void testMkParamSort();
@@ -96,9 +97,15 @@ class SolverBlack : public CxxTest::TestSuite
   void testPop3();
 
   void testSimplify();
+
+  void testAssertFormula();
   void testCheckEntailed();
   void testCheckEntailed1();
   void testCheckEntailed2();
+  void testCheckSat();
+  void testCheckSatAssuming();
+  void testCheckSatAssuming1();
+  void testCheckSatAssuming2();
 
   void testSetInfo();
   void testSetLogic();
@@ -173,6 +180,8 @@ void SolverBlack::testMkArraySort()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(boolSort, intSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(realSort, bvSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkArraySort(bvSort, fpSort));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkArraySort(boolSort, boolSort), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBitVectorSort()
@@ -191,17 +200,64 @@ void SolverBlack::testMkFloatingPointSort()
 void SolverBlack::testMkDatatypeSort()
 {
   DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec));
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkDatatypeSort(dtypeSpec), CVC4ApiException&);
+
   DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
   TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec),
                    CVC4ApiException&);
 }
 
+void SolverBlack::testMkDatatypeSorts()
+{
+  Solver slv;
+
+  DatatypeDecl dtypeSpec1 = d_solver->mkDatatypeDecl("list1");
+  DatatypeConstructorDecl cons1 = d_solver->mkDatatypeConstructorDecl("cons1");
+  cons1.addSelector("head1", d_solver->getIntegerSort());
+  dtypeSpec1.addConstructor(cons1);
+  DatatypeConstructorDecl nil1 = d_solver->mkDatatypeConstructorDecl("nil1");
+  dtypeSpec1.addConstructor(nil1);
+  DatatypeDecl dtypeSpec2 = d_solver->mkDatatypeDecl("list2");
+  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons2");
+  cons2.addSelector("head2", d_solver->getIntegerSort());
+  dtypeSpec2.addConstructor(cons2);
+  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil2");
+  dtypeSpec2.addConstructor(nil2);
+  std::vector<DatatypeDecl> decls = {dtypeSpec1, dtypeSpec2};
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(decls));
+
+  TS_ASSERT_THROWS(slv.mkDatatypeSorts(decls), CVC4ApiException&);
+
+  DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list");
+  std::vector<DatatypeDecl> throwsDecls = {throwsDtypeSpec};
+  TS_ASSERT_THROWS(d_solver->mkDatatypeSorts(throwsDecls), CVC4ApiException&);
+
+  /* with unresolved sorts */
+  Sort unresList = d_solver->mkUninterpretedSort("ulist");
+  std::set<Sort> unresSorts = {unresList};
+  DatatypeDecl ulist = d_solver->mkDatatypeDecl("ulist");
+  DatatypeConstructorDecl ucons = d_solver->mkDatatypeConstructorDecl("ucons");
+  ucons.addSelector("car", unresList);
+  ucons.addSelector("cdr", unresList);
+  ulist.addConstructor(ucons);
+  DatatypeConstructorDecl unil = d_solver->mkDatatypeConstructorDecl("unil");
+  ulist.addConstructor(unil);
+  std::vector<DatatypeDecl> udecls = {ulist};
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSorts(udecls, unresSorts));
+
+  TS_ASSERT_THROWS(slv.mkDatatypeSorts(udecls, unresSorts), CVC4ApiException&);
+
+  /* Note: More tests are in datatype_api_black. */
+}
+
 void SolverBlack::testMkFunctionSort()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkFunctionSort(
@@ -228,6 +284,23 @@ void SolverBlack::testMkFunctionSort()
           {d_solver->getIntegerSort(), d_solver->mkUninterpretedSort("u")},
           funSort2),
       CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkFunctionSort(d_solver->mkUninterpretedSort("u"),
+                                      d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkFunctionSort(slv.mkUninterpretedSort("u"),
+                                      d_solver->getIntegerSort()),
+                   CVC4ApiException&);
+  std::vector<Sort> sorts1 = {d_solver->getBooleanSort(),
+                              slv.getIntegerSort(),
+                              d_solver->getIntegerSort()};
+  std::vector<Sort> sorts2 = {slv.getBooleanSort(), slv.getIntegerSort()};
+  TS_ASSERT_THROWS_NOTHING(slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
+  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts1, slv.getIntegerSort()),
+                   CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkFunctionSort(sorts2, d_solver->getIntegerSort()),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkParamSort()
@@ -246,6 +319,10 @@ void SolverBlack::testMkPredicateSort()
   TS_ASSERT_THROWS(
       d_solver->mkPredicateSort({d_solver->getIntegerSort(), funSort}),
       CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkPredicateSort({d_solver->getIntegerSort()}),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkRecordSort()
@@ -259,6 +336,9 @@ void SolverBlack::testMkRecordSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
   Sort recSort = d_solver->mkRecordSort(fields);
   TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkRecordSort(fields), CVC4ApiException&);
 }
 
 void SolverBlack::testMkSetSort()
@@ -266,6 +346,9 @@ void SolverBlack::testMkSetSort()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getBooleanSort()));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->getIntegerSort()));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSetSort(d_solver->mkBitVectorSort(4)));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSetSort(d_solver->mkBitVectorSort(4)),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkUninterpretedSort()
@@ -288,6 +371,10 @@ void SolverBlack::testMkTupleSort()
                                           d_solver->getIntegerSort());
   TS_ASSERT_THROWS(d_solver->mkTupleSort({d_solver->getIntegerSort(), funSort}),
                    CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkTupleSort({d_solver->getIntegerSort()}),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkBitVector()
@@ -332,6 +419,8 @@ void SolverBlack::testMkVar()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
   TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkVar(boolSort, "x"), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBoolean()
@@ -352,6 +441,9 @@ void SolverBlack::testMkUninterpretedConst()
       d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1));
   TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkUninterpretedConst(d_solver->getBooleanSort(), 1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkAbstractValue()
@@ -393,13 +485,23 @@ void SolverBlack::testMkFloatingPoint()
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 0, t1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkFloatingPoint(3, 5, t2), CVC4ApiException&);
+
+  if (CVC4::Configuration::isBuiltWithSymFPU())
+  {
+    Solver slv;
+    TS_ASSERT_THROWS(slv.mkFloatingPoint(3, 5, t1), CVC4ApiException&);
+  }
 }
 
 void SolverBlack::testMkEmptySet()
 {
+  Solver slv;
+  Sort s = d_solver->mkSetSort(d_solver->getBooleanSort());
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(s));
   TS_ASSERT_THROWS(d_solver->mkEmptySet(d_solver->getBooleanSort()),
                    CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkEmptySet(Sort()));
+  TS_ASSERT_THROWS(slv.mkEmptySet(s), CVC4ApiException&);
 }
 
 void SolverBlack::testMkFalse()
@@ -558,6 +660,8 @@ void SolverBlack::testMkSepNil()
 {
   TS_ASSERT_THROWS_NOTHING(d_solver->mkSepNil(d_solver->getBooleanSort()));
   TS_ASSERT_THROWS(d_solver->mkSepNil(Sort()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkSepNil(d_solver->getIntegerSort()), CVC4ApiException&);
 }
 
 void SolverBlack::testMkString()
@@ -592,6 +696,7 @@ void SolverBlack::testMkTerm()
   std::vector<Term> v4 = {d_solver->mkReal(1), d_solver->mkReal(2)};
   std::vector<Term> v5 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v6 = {};
+  Solver slv;
 
   // mkTerm(Kind kind) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(PI));
@@ -603,6 +708,7 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(NOT, d_solver->mkTrue()));
   TS_ASSERT_THROWS(d_solver->mkTerm(NOT, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(NOT, a), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(NOT, d_solver->mkTrue()), CVC4ApiException&);
 
   // mkTerm(Kind kind, Term child1, Term child2) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, a, b));
@@ -610,6 +716,7 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(EQUAL, a, d_solver->mkTrue()),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(EQUAL, a, b), CVC4ApiException&);
 
   // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(
@@ -626,6 +733,10 @@ void SolverBlack::testMkTerm()
   TS_ASSERT_THROWS(
       d_solver->mkTerm(ITE, d_solver->mkTrue(), d_solver->mkTrue(), b),
       CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.mkTerm(
+          ITE, d_solver->mkTrue(), d_solver->mkTrue(), d_solver->mkTrue()),
+      CVC4ApiException&);
 
   // mkTerm(Kind kind, const std::vector<Term>& children) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(EQUAL, v1));
@@ -643,15 +754,17 @@ void SolverBlack::testMkTermFromOp()
   std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v3 = {};
   std::vector<Term> v4 = {d_solver->mkReal(5)};
+  Solver slv;
+
   // simple operator terms
   Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1);
   Op opterm2 = d_solver->mkOp(DIVISIBLE, 1);
-  // list datatype
 
+  // list datatype
   Sort sort = d_solver->mkParamSort("T");
   DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);
   cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);
@@ -661,6 +774,7 @@ void SolverBlack::testMkTermFromOp()
       listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
   Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
+
   // list datatype constructor and selector operator terms
   Term consTerm1 = list.getConstructorTerm("cons");
   Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
@@ -684,6 +798,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1), CVC4ApiException&);
 
   // mkTerm(Op op, Term child) const
   TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a));
@@ -695,24 +810,29 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(
       d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)),
       CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(opterm1, a), CVC4ApiException&);
 
   // mkTerm(Op op, Term child1, Term child2) const
-  TS_ASSERT_THROWS(
-      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
-      CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(APPLY_CONSTRUCTOR,
                        consTerm1,
                        d_solver->mkReal(0),
                        d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+  TS_ASSERT_THROWS(
+      d_solver->mkTerm(opterm2, d_solver->mkReal(1), d_solver->mkReal(2)),
+      CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, d_solver->mkReal(1), Term()),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, Term(), d_solver->mkReal(1)),
                    CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(APPLY_CONSTRUCTOR,
+                              consTerm1,
+                              d_solver->mkReal(0),
+                              d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)),
+                   CVC4ApiException&);
 
-  // mkTerm(Op op, Term child1, Term child2, Term child3)
-  // const
+  // mkTerm(Op op, Term child1, Term child2, Term child3) const
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&);
   TS_ASSERT_THROWS(
       d_solver->mkTerm(
@@ -724,6 +844,7 @@ void SolverBlack::testMkTermFromOp()
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v1), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v2), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, v3), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkTerm(opterm2, v4), CVC4ApiException&);
 }
 
 void SolverBlack::testMkTrue()
@@ -747,12 +868,22 @@ void SolverBlack::testMkTuple()
   TS_ASSERT_THROWS(d_solver->mkTuple({d_solver->getIntegerSort()},
                                      {d_solver->mkReal("5.3")}),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(
+      slv.mkTuple({d_solver->mkBitVectorSort(3)}, {slv.mkBitVector("101", 2)}),
+      CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      slv.mkTuple({slv.mkBitVectorSort(3)}, {d_solver->mkBitVector("101", 2)}),
+      CVC4ApiException&);
 }
 
 void SolverBlack::testMkUniverseSet()
 {
-  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkUniverseSet(d_solver->getBooleanSort()));
+  TS_ASSERT_THROWS(d_solver->mkUniverseSet(Sort()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkUniverseSet(d_solver->getBooleanSort()),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testMkConst()
@@ -768,6 +899,9 @@ void SolverBlack::testMkConst()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
   TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
+
+  Solver slv;
+  TS_ASSERT_THROWS(slv.mkConst(boolSort), CVC4ApiException&);
 }
 
 void SolverBlack::testMkConstArray()
@@ -778,23 +912,29 @@ void SolverBlack::testMkConstArray()
   Term constArr = d_solver->mkConstArray(arrSort, zero);
 
   TS_ASSERT_THROWS_NOTHING(d_solver->mkConstArray(arrSort, zero));
+  TS_ASSERT_THROWS(d_solver->mkConstArray(Sort(), zero), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, Term()), CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(arrSort, d_solver->mkBitVector(1, 1)),
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->mkConstArray(intSort, zero), CVC4ApiException&);
+  Solver slv;
+  Term zero2 = slv.mkReal(0);
+  Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
+  TS_ASSERT_THROWS(slv.mkConstArray(arrSort2, zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(slv.mkConstArray(arrSort, zero2), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareDatatype()
 {
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors1 = {nil};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1));
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil2("nil");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil2 = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2));
-  DatatypeConstructorDecl cons2("cons");
-  DatatypeConstructorDecl nil3("nil");
+  DatatypeConstructorDecl cons2 = d_solver->mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil3 = d_solver->mkDatatypeConstructorDecl("nil");
   std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3};
   TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3));
   std::vector<DatatypeConstructorDecl> ctors4;
@@ -802,6 +942,9 @@ void SolverBlack::testDeclareDatatype()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.declareDatatype(std::string("a"), ctors1),
+                   CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareFun()
@@ -817,6 +960,8 @@ void SolverBlack::testDeclareFun()
                    CVC4ApiException&);
   TS_ASSERT_THROWS(d_solver->declareFun("f5", {bvSort, bvSort}, funSort),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.declareFun("f1", {}, bvSort), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareSort()
@@ -959,11 +1104,11 @@ void SolverBlack::testGetOp()
 
   // Test Datatypes -- more complicated
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
   Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
   Datatype consList = consListSort.getDatatype();
@@ -1059,11 +1204,11 @@ void SolverBlack::testSimplify()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
   DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver->mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver->getIntegerSort());
   cons.addSelectorSelf("tail");
   consListSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver->mkDatatypeConstructorDecl("nil");
   consListSpec.addConstructor(nil);
   Sort consListSort = d_solver->mkDatatypeSort(consListSpec);
 
@@ -1081,6 +1226,8 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(x_eq_b));
   TS_ASSERT(d_solver->mkTrue() != x_eq_b);
   TS_ASSERT(d_solver->mkTrue() != d_solver->simplify(x_eq_b));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.simplify(x), CVC4ApiException&);
 
   Term i1 = d_solver->mkConst(d_solver->getIntegerSort(), "i1");
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(i1));
@@ -1123,12 +1270,22 @@ void SolverBlack::testSimplify()
   TS_ASSERT_THROWS_NOTHING(d_solver->simplify(f2));
 }
 
+void SolverBlack::testAssertFormula()
+{
+  TS_ASSERT_THROWS_NOTHING(d_solver->assertFormula(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->assertFormula(Term()), CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.assertFormula(d_solver->mkTrue()), CVC4ApiException&);
+}
+
 void SolverBlack::testCheckEntailed()
 {
   d_solver->setOption("incremental", "false");
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   TS_ASSERT_THROWS(d_solver->checkEntailed(d_solver->mkTrue()),
                    CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testCheckEntailed1()
@@ -1142,6 +1299,8 @@ void SolverBlack::testCheckEntailed1()
   TS_ASSERT_THROWS(d_solver->checkEntailed(Term()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(d_solver->mkTrue()));
   TS_ASSERT_THROWS_NOTHING(d_solver->checkEntailed(z));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testCheckEntailed2()
@@ -1191,6 +1350,91 @@ void SolverBlack::testCheckEntailed2()
   TS_ASSERT_THROWS(
       d_solver->checkEntailed({n, d_solver->mkTerm(DISTINCT, x, y)}),
       CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkEntailed(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSat()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSat());
+  TS_ASSERT_THROWS(d_solver->checkSat(), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming()
+{
+  d_solver->setOption("incremental", "false");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(d_solver->mkTrue()),
+                   CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming1()
+{
+  Sort boolSort = d_solver->getBooleanSort();
+  Term x = d_solver->mkConst(boolSort, "x");
+  Term y = d_solver->mkConst(boolSort, "y");
+  Term z = d_solver->mkTerm(AND, x, y);
+  d_solver->setOption("incremental", "true");
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(Term()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(z));
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
+}
+
+void SolverBlack::testCheckSatAssuming2()
+{
+  d_solver->setOption("incremental", "true");
+
+  Sort uSort = d_solver->mkUninterpretedSort("u");
+  Sort intSort = d_solver->getIntegerSort();
+  Sort boolSort = d_solver->getBooleanSort();
+  Sort uToIntSort = d_solver->mkFunctionSort(uSort, intSort);
+  Sort intPredSort = d_solver->mkFunctionSort(intSort, boolSort);
+
+  Term n = Term();
+  // Constants
+  Term x = d_solver->mkConst(uSort, "x");
+  Term y = d_solver->mkConst(uSort, "y");
+  // Functions
+  Term f = d_solver->mkConst(uToIntSort, "f");
+  Term p = d_solver->mkConst(intPredSort, "p");
+  // Values
+  Term zero = d_solver->mkReal(0);
+  Term one = d_solver->mkReal(1);
+  // Terms
+  Term f_x = d_solver->mkTerm(APPLY_UF, f, x);
+  Term f_y = d_solver->mkTerm(APPLY_UF, f, y);
+  Term sum = d_solver->mkTerm(PLUS, f_x, f_y);
+  Term p_0 = d_solver->mkTerm(APPLY_UF, p, zero);
+  Term p_f_y = d_solver->mkTerm(APPLY_UF, p, f_y);
+  // Assertions
+  Term assertions =
+      d_solver->mkTerm(AND,
+                       std::vector<Term>{
+                           d_solver->mkTerm(LEQ, zero, f_x),  // 0 <= f(x)
+                           d_solver->mkTerm(LEQ, zero, f_y),  // 0 <= f(y)
+                           d_solver->mkTerm(LEQ, sum, one),  // f(x) + f(y) <= 1
+                           p_0.notTerm(),                    // not p(0)
+                           p_f_y                             // p(f(y))
+                       });
+
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(d_solver->mkTrue()));
+  d_solver->assertFormula(assertions);
+  TS_ASSERT_THROWS_NOTHING(
+      d_solver->checkSatAssuming(d_solver->mkTerm(DISTINCT, x, y)));
+  TS_ASSERT_THROWS_NOTHING(d_solver->checkSatAssuming(
+      {d_solver->mkFalse(), d_solver->mkTerm(DISTINCT, x, y)}));
+  TS_ASSERT_THROWS(d_solver->checkSatAssuming(n), CVC4ApiException&);
+  TS_ASSERT_THROWS(
+      d_solver->checkSatAssuming({n, d_solver->mkTerm(DISTINCT, x, y)}),
+      CVC4ApiException&);
+  Solver slv;
+  TS_ASSERT_THROWS(slv.checkSatAssuming(d_solver->mkTrue()), CVC4ApiException&);
 }
 
 void SolverBlack::testSetLogic()
diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index 42d2dcb25..437b5cf26 100644
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -63,10 +63,10 @@ void SortBlack::testGetDatatype()
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatype());
@@ -80,11 +80,11 @@ void SortBlack::testDatatypeSorts()
   Sort intSort = d_solver.getIntegerSort();
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
@@ -121,8 +121,9 @@ void SortBlack::testInstantiate()
   // instantiate parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons =
+      d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
@@ -131,10 +132,10 @@ void SortBlack::testInstantiate()
       paramDtypeSort.instantiate(std::vector<Sort>{d_solver.getIntegerSort()}));
   // instantiate non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS(
@@ -265,8 +266,9 @@ void SortBlack::testGetDatatypeParamSorts()
   // create parametric datatype, check should not fail
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl paramCons("cons");
-  DatatypeConstructorDecl paramNil("nil");
+  DatatypeConstructorDecl paramCons =
+      d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl paramNil = d_solver.mkDatatypeConstructorDecl("nil");
   paramCons.addSelector("head", sort);
   paramDtypeSpec.addConstructor(paramCons);
   paramDtypeSpec.addConstructor(paramNil);
@@ -274,10 +276,10 @@ void SortBlack::testGetDatatypeParamSorts()
   TS_ASSERT_THROWS_NOTHING(paramDtypeSort.getDatatypeParamSorts());
   // create non-parametric datatype sort, check should fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS(dtypeSort.getDatatypeParamSorts(), CVC4ApiException&);
@@ -287,10 +289,10 @@ void SortBlack::testGetDatatypeArity()
 {
   // create datatype sort, check should not fail
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  DatatypeConstructorDecl cons("cons");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", d_solver.getIntegerSort());
   dtypeSpec.addConstructor(cons);
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   TS_ASSERT_THROWS_NOTHING(dtypeSort.getDatatypeArity());
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index d8f022201..a3cbd028f 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -197,8 +197,8 @@ void TermBlack::testGetOp()
   // Test Datatypes Ops
   Sort sort = d_solver.mkParamSort("T");
   DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
-  DatatypeConstructorDecl cons("cons");
-  DatatypeConstructorDecl nil("nil");
+  DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+  DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   cons.addSelector("head", sort);
   cons.addSelectorSelf("tail");
   listDecl.addConstructor(cons);