New C++ API: Add tests for term object. (#2755)

1 files changed, 514 insertions, 8 deletions

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index c2ca1cb08..ae1dfe7ba 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -2,7 +2,7 @@
 /*! \file term_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Aina Niemetz, Andres Noetzli
  ** 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.
@@ -24,14 +24,520 @@ class TermBlack : public CxxTest::TestSuite
   void setUp() override {}
   void tearDown() override {}
 
-  void testTermAssignment()
-  {
-    Term t1 = d_solver.mkReal(1);
-    Term t2 = t1;
-    t2 = d_solver.mkReal(2);
-    TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
-  }
+  void testEq();
+  void testGetKind();
+  void testGetSort();
+  void testIsNull();
+  void testNotTerm();
+  void testAndTerm();
+  void testOrTerm();
+  void testXorTerm();
+  void testEqTerm();
+  void testImpTerm();
+  void testIteTerm();
+
+  void testTermAssignment();
 
  private:
   Solver d_solver;
 };
+
+void TermBlack::testEq()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar("x", uSort);
+  Term y = d_solver.mkVar("y", uSort);
+  Term z;
+
+  TS_ASSERT(x == x);
+  TS_ASSERT(!(x != x));
+  TS_ASSERT(!(x == y));
+  TS_ASSERT(x != y);
+  TS_ASSERT(!(x == z));
+  TS_ASSERT(x != z);
+}
+
+void TermBlack::testGetKind()
+{
+  Sort uSort = d_solver.mkUninterpretedSort("u");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(uSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n;
+  TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
+  Term x = d_solver.mkVar("x", uSort);
+  TS_ASSERT_THROWS_NOTHING(x.getKind());
+  Term y = d_solver.mkVar("y", uSort);
+  TS_ASSERT_THROWS_NOTHING(y.getKind());
+
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS_NOTHING(f.getKind());
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS_NOTHING(p.getKind());
+
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS_NOTHING(zero.getKind());
+
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS_NOTHING(f_x.getKind());
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  TS_ASSERT_THROWS_NOTHING(f_y.getKind());
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  TS_ASSERT_THROWS_NOTHING(sum.getKind());
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.getKind());
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  TS_ASSERT_THROWS_NOTHING(p_f_y.getKind());
+}
+
+void TermBlack::testGetSort()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term n;
+  TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
+  Term x = d_solver.mkVar("x", bvSort);
+  TS_ASSERT_THROWS_NOTHING(x.getSort());
+  TS_ASSERT(x.getSort() == bvSort);
+  Term y = d_solver.mkVar("y", bvSort);
+  TS_ASSERT_THROWS_NOTHING(y.getSort());
+  TS_ASSERT(y.getSort() == bvSort);
+
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS_NOTHING(f.getSort());
+  TS_ASSERT(f.getSort() == funSort1);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS_NOTHING(p.getSort());
+  TS_ASSERT(p.getSort() == funSort2);
+
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS_NOTHING(zero.getSort());
+  TS_ASSERT(zero.getSort() == intSort);
+
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS_NOTHING(f_x.getSort());
+  TS_ASSERT(f_x.getSort() == intSort);
+  Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+  TS_ASSERT_THROWS_NOTHING(f_y.getSort());
+  TS_ASSERT(f_y.getSort() == intSort);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+  TS_ASSERT_THROWS_NOTHING(sum.getSort());
+  TS_ASSERT(sum.getSort() == intSort);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.getSort());
+  TS_ASSERT(p_0.getSort() == boolSort);
+  Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+  TS_ASSERT_THROWS_NOTHING(p_f_y.getSort());
+  TS_ASSERT(p_f_y.getSort() == boolSort);
+}
+
+void TermBlack::testIsNull()
+{
+  Term x;
+  TS_ASSERT(x.isNull());
+  x = d_solver.mkVar("x", d_solver.mkBitVectorSort(4));
+  TS_ASSERT(!x.isNull());
+}
+
+void TermBlack::testNotTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.notTerm());
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.notTerm(), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.notTerm(), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.notTerm());
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.notTerm());
+}
+
+void TermBlack::testAndTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.andTerm(p), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.andTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.andTerm(zero), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.andTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.andTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.andTerm(f_x), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.andTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.andTerm(sum), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.andTerm(b));
+  TS_ASSERT_THROWS(p_0.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.andTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.andTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.andTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.andTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_0.andTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(b));
+  TS_ASSERT_THROWS(p_f_x.andTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.andTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.andTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.andTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.andTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.andTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_0));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.andTerm(p_f_x));
+}
+
+void TermBlack::testOrTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.orTerm(p), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.orTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.orTerm(zero), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.orTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.orTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.orTerm(f_x), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.orTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.orTerm(sum), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.orTerm(b));
+  TS_ASSERT_THROWS(p_0.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.orTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.orTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.orTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.orTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_0.orTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(b));
+  TS_ASSERT_THROWS(p_f_x.orTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.orTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.orTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.orTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.orTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.orTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_0));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.orTerm(p_f_x));
+}
+
+void TermBlack::testXorTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.xorTerm(p), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.xorTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.xorTerm(zero), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.xorTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.xorTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.xorTerm(f_x), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.xorTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.xorTerm(sum), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(b));
+  TS_ASSERT_THROWS(p_0.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.xorTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.xorTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.xorTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.xorTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_0.xorTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(b));
+  TS_ASSERT_THROWS(p_f_x.xorTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.xorTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.xorTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.xorTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.xorTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.xorTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_0));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.xorTerm(p_f_x));
+}
+
+void TermBlack::testEqTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p.eqTerm(p));
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.eqTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(zero.eqTerm(zero));
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.eqTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(zero));
+  TS_ASSERT_THROWS_NOTHING(f_x.eqTerm(f_x));
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.eqTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.eqTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(zero));
+  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(f_x));
+  TS_ASSERT_THROWS_NOTHING(sum.eqTerm(sum));
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(b));
+  TS_ASSERT_THROWS(p_0.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.eqTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.eqTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.eqTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.eqTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_0.eqTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(b));
+  TS_ASSERT_THROWS(p_f_x.eqTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.eqTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.eqTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.eqTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.eqTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.eqTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_0));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.eqTerm(p_f_x));
+}
+
+void TermBlack::testImpTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.impTerm(p), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.impTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.impTerm(zero), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.impTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.impTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.impTerm(f_x), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.impTerm(b), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.impTerm(sum), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.impTerm(b));
+  TS_ASSERT_THROWS(p_0.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.impTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.impTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.impTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_0.impTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_0.impTerm(p_0));
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(b));
+  TS_ASSERT_THROWS(p_f_x.impTerm(x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.impTerm(f), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.impTerm(p), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.impTerm(zero), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.impTerm(f_x), CVC4ApiException&);
+  TS_ASSERT_THROWS(p_f_x.impTerm(sum), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_0));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.impTerm(p_f_x));
+}
+
+void TermBlack::testIteTerm()
+{
+  Sort bvSort = d_solver.mkBitVectorSort(8);
+  Sort intSort = d_solver.getIntegerSort();
+  Sort boolSort = d_solver.getBooleanSort();
+  Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
+  Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
+
+  Term b = d_solver.mkTrue();
+  TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
+  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
+  TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
+  TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
+  Term f = d_solver.mkVar("f", funSort1);
+  TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
+  Term p = d_solver.mkVar("p", funSort2);
+  TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
+  Term zero = d_solver.mkInteger(0);
+  TS_ASSERT_THROWS(zero.iteTerm(x, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(zero.iteTerm(x, b), CVC4ApiException&);
+  Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+  TS_ASSERT_THROWS(f_x.iteTerm(b, b), CVC4ApiException&);
+  TS_ASSERT_THROWS(f_x.iteTerm(b, x), CVC4ApiException&);
+  Term sum = d_solver.mkTerm(PLUS, f_x, f_x);
+  TS_ASSERT_THROWS(sum.iteTerm(x, x), CVC4ApiException&);
+  TS_ASSERT_THROWS(sum.iteTerm(b, x), CVC4ApiException&);
+  Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+  TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(b, b));
+  TS_ASSERT_THROWS_NOTHING(p_0.iteTerm(x, x));
+  TS_ASSERT_THROWS(p_0.iteTerm(x, b), CVC4ApiException&);
+  Term p_f_x = d_solver.mkTerm(APPLY_UF, p, f_x);
+  TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(b, b));
+  TS_ASSERT_THROWS_NOTHING(p_f_x.iteTerm(x, x));
+  TS_ASSERT_THROWS(p_f_x.iteTerm(x, b), CVC4ApiException&);
+}
+
+void TermBlack::testTermAssignment()
+{
+  Term t1 = d_solver.mkReal(1);
+  Term t2 = t1;
+  t2 = d_solver.mkReal(2);
+  TS_ASSERT_EQUALS(t1, d_solver.mkReal(1));
+}