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

5 files changed, 90 insertions, 14 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 68b0301ec..cd604a25c 100644
--- 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 aebeffb0d..d06955a05 100644
--- 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 61568e411..96bdb2d04 100644
--- 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 324915b1d..da9d22389 100644
--- 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 9eb39e2e2..ba3533cc3 100644
--- 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);