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

2 files changed, 86 insertions, 11 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.