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

diff --git a/NEWS b/NEWS
index 038b02026129d372fc35eca853481a94001f374d..0cc8cab446dc824197cdfbc8e07211226190f233 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -1,5 +1,16 @@
 This file contains a summary of important user-visible changes. 
 
+Changes since 1.6
+=================
+
+New Features:
+
+Improvements:
+
+Changes:
+* API change: Expr::iffExpr() is renamed to Expr::eqExpr() to reflect its
+              actual behavior.
+
 Changes since 1.5
 =================
 

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 68b0301ec682341ee333aef3dbe73d1af28797f3..cd604a25c4c01cd4b857d8803a73455a75efe6a2 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1007,27 +1007,102 @@ bool Term::operator==(const Term& t) const { return *d_expr == *t.d_expr; }
 
 bool Term::operator!=(const Term& t) const { return *d_expr != *t.d_expr; }
 
-Kind Term::getKind() const { return intToExtKind(d_expr->getKind()); }
+Kind Term::getKind() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return intToExtKind(d_expr->getKind());
+}
 
-Sort Term::getSort() const { return Sort(d_expr->getType()); }
+Sort Term::getSort() const
+{
+  CVC4_API_CHECK_NOT_NULL;
+  return Sort(d_expr->getType());
+}
 
 bool Term::isNull() const { return d_expr->isNull(); }
 
-Term Term::notTerm() const { return d_expr->notExpr(); }
+Term Term::notTerm() const
+{
+  try
+  {
+    return d_expr->notExpr();
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
-Term Term::andTerm(const Term& t) const { return d_expr->andExpr(*t.d_expr); }
+Term Term::andTerm(const Term& t) const
+{
+  try
+  {
+    return d_expr->andExpr(*t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
-Term Term::orTerm(const Term& t) const { return d_expr->orExpr(*t.d_expr); }
+Term Term::orTerm(const Term& t) const
+{
+  try
+  {
+    return d_expr->orExpr(*t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
-Term Term::xorTerm(const Term& t) const { return d_expr->xorExpr(*t.d_expr); }
+Term Term::xorTerm(const Term& t) const
+{
+  try
+  {
+    return d_expr->xorExpr(*t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
-Term Term::iffTerm(const Term& t) const { return d_expr->iffExpr(*t.d_expr); }
+Term Term::eqTerm(const Term& t) const
+{
+  try
+  {
+    return d_expr->eqExpr(*t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
-Term Term::impTerm(const Term& t) const { return d_expr->impExpr(*t.d_expr); }
+Term Term::impTerm(const Term& t) const
+{
+  try
+  {
+    return d_expr->impExpr(*t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
+}
 
 Term Term::iteTerm(const Term& then_t, const Term& else_t) const
 {
-  return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+  try
+  {
+    return d_expr->iteExpr(*then_t.d_expr, *else_t.d_expr);
+  }
+  catch (TypeCheckingException& e)
+  {
+    throw CVC4ApiException(e.getMessage());
+  }
 }
 
 std::string Term::toString() const { return d_expr->toString(); }

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index aebeffb0df545d986802c801acc5612f0e56f194..d06955a05ed20556b1c5d89cf67bad8fdae80a25 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -607,11 +607,11 @@ class CVC4_PUBLIC Term
   Term xorTerm(const Term& t) const;
 
   /**
-   * Boolean if-and-only-if.
+   * Equality.
    * @param t a Boolean term
    * @return the Boolean equivalence of this term and the given term
    */
-  Term iffTerm(const Term& t) const;
+  Term eqTerm(const Term& t) const;
 
   /**
    * Boolean implication.

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 61568e411d8d4e5968bbec3d6c47e1f023b78ae9..96bdb2d046b1ec10638189e6e2f5b66836520431 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -595,7 +595,8 @@ Expr Expr::xorExpr(const Expr& e) const {
   return d_exprManager->mkExpr(XOR, *this, e);
 }
 
-Expr Expr::iffExpr(const Expr& e) const {
+Expr Expr::eqExpr(const Expr& e) const
+{
   Assert(d_exprManager != NULL,
          "Don't have an expression manager for this expression!");
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 324915b1da773ee2457ef10bb9d8e43aa9ecbe55..da9d22389fee50a653ed6702c96875f8a4e915b2 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -391,7 +391,7 @@ public:
    * Returns the Boolean equivalence of this expression and
    * the given expression.
    */
-  Expr iffExpr(const Expr& e) const;
+  Expr eqExpr(const Expr& e) const;
 
   /**
    * Returns the implication of this expression and

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 9eb39e2e2a60df8e79a753969da9eef030212b94..ba3533cc3b8381654bc29b85fb12647d8df48540 100644 (file)
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -68,7 +68,7 @@ void BitVectorProof::registerAtomBB(Expr atom, Expr atom_bb) {
   Debug("pf::bv") << "BitVectorProof::registerAtomBB( " << atom
                   << ", " << atom_bb << " )" << std::endl;
 
-  Expr def = atom.iffExpr(atom_bb);
+  Expr def = atom.eqExpr(atom_bb);
   d_bbAtoms.insert(std::make_pair(atom, def));
   registerTerm(atom);
 

diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index c2ca1cb08ccadcadc649998f4164457128b80c2e..ae1dfe7bad54222e10f4fcb5596eff440924d6a6 100644 (file)
--- 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));
+}