New C++ Api: Second and last batch of API guards. (#4563)

This adds the remaining API guards in the Solver object (incl. unit tests).

1 files changed, 207 insertions, 87 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index f225da333..734fcddae 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4194,8 +4194,10 @@ Term Solver::declareFun(const std::string& symbol,
  */
 Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
   return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4206,26 +4208,28 @@ Term Solver::defineFun(const std::string& symbol,
                        Sort sort,
                        Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
-  // CHECK: not recursive
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as codomain sort for function sort";
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Type> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4::Type t = bound_vars[i].d_expr->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_CHECK(sort == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
@@ -4238,17 +4242,14 @@ Term Solver::defineFun(const std::string& symbol,
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr);
   return Term(this, fun);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFun(Term fun,
                        const std::vector<Term>& bound_vars,
                        Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
   std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
   size_t size = bound_vars.size();
@@ -4257,6 +4258,15 @@ Term Solver::defineFun(Term fun,
   for (size_t i = 0; i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         domain_sorts[i] == bound_vars[i].getSort(),
         "sort of parameter",
         bound_vars[i],
@@ -4264,16 +4274,15 @@ Term Solver::defineFun(Term fun,
         << "'" << domain_sorts[i] << "'";
   }
   Sort codomain = fun.getSort().getFunctionCodomainSort();
+  CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_CHECK(codomain == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '"
       << codomain << "'";
 
-  // CHECK: not recursive
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr);
   return fun;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4284,29 +4293,33 @@ Term Solver::defineFunRec(const std::string& symbol,
                           Sort sort,
                           Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
       << "first-class sort as function codomain sort";
   Assert(!sort.isFunction()); /* A function sort is not first-class. */
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Type> domain_types;
   for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
     CVC4::Type t = bound_vars[i].d_expr->getType();
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         t.isFirstClass(), "sort of parameter", bound_vars[i], i)
         << "first-class sort of parameter of defined function";
     domain_types.push_back(t);
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
   CVC4_API_CHECK(sort == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '" << sort
       << "'";
+  CVC4_API_SOLVER_CHECK_TERM(term);
   Type type = *sort.d_type;
   if (!domain_types.empty())
   {
@@ -4316,18 +4329,14 @@ Term Solver::defineFunRec(const std::string& symbol,
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr);
   return Term(this, fun);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::defineFunRec(Term fun,
                           const std::vector<Term>& bound_vars,
                           Term term) const
 {
-  // CHECK:
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
   std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
   size_t size = bound_vars.size();
@@ -4336,21 +4345,30 @@ Term Solver::defineFunRec(Term fun,
   for (size_t i = 0; i < size; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        bound_vars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        bound_vars[i],
+        i)
+        << "a bound variable";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         domain_sorts[i] == bound_vars[i].getSort(),
         "sort of parameter",
         bound_vars[i],
         i)
         << "'" << domain_sorts[i] << "'";
   }
+  CVC4_API_SOLVER_CHECK_TERM(term);
   Sort codomain = fun.getSort().getFunctionCodomainSort();
   CVC4_API_CHECK(codomain == term.getSort())
       << "Invalid sort of function body '" << term << "', expected '"
       << codomain << "'";
-  // CHECK:
-  // for v in bound_vars: is bound var
   std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars);
   d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr);
   return fun;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4360,15 +4378,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
                            const std::vector<std::vector<Term>>& bound_vars,
                            const std::vector<Term>& terms) const
 {
-  // CHECK:
-  // for f in funs:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(f.getExprManager())
-  // for bv in bound_vars:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(bv.getExprManager())
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   size_t funs_size = funs.size();
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars)
       << "'" << funs_size << "'";
@@ -4378,13 +4388,30 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
     const std::vector<Term>& bvars = bound_vars[j];
     const Term& term = terms[j];
 
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == fun.d_solver, "function", fun, j)
+        << "function associated to this solver object";
     CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function";
+    CVC4_API_SOLVER_CHECK_TERM(term);
+
     std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
     size_t size = bvars.size();
     CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
         << "'" << domain_sorts.size() << "'";
     for (size_t i = 0; i < size; ++i)
     {
+      for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k)
+      {
+        CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+            this == bvars[k].d_solver, "bound variable", bvars[k], k)
+            << "bound variable associated to this solver object";
+        CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+            bvars[k].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+            "bound variable",
+            bvars[k],
+            k)
+            << "a bound variable";
+      }
       CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
           domain_sorts[i] == bvars[i].getSort(),
           "sort of parameter",
@@ -4397,8 +4424,6 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
         codomain == term.getSort(), "sort of function body", term, j)
         << "'" << codomain << "'";
   }
-  // CHECK:
-  // for bv in bound_vars (for v in bv): is bound var
   std::vector<Expr> efuns = termVectorToExprs(funs);
   std::vector<std::vector<Expr>> ebound_vars;
   for (const auto& v : bound_vars)
@@ -4407,6 +4432,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs,
   }
   std::vector<Expr> exprs = termVectorToExprs(terms);
   d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4422,6 +4448,7 @@ void Solver::echo(std::ostream& out, const std::string& str) const
  */
 std::vector<Term> Solver::getAssertions(void) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   std::vector<Expr> assertions = d_smtEngine->getAssertions();
   /* Can not use
    *   return std::vector<Term>(assertions.begin(), assertions.end());
@@ -4432,6 +4459,7 @@ std::vector<Term> Solver::getAssertions(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4439,8 +4467,11 @@ std::vector<Term> Solver::getAssertions(void) const
  */
 std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
 {
-  // CHECK: produce-models set
-  // CHECK: result sat
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceAssignments())
+      << "Cannot get assignment unless assignment generation is enabled "
+         "(try --produce-assignments)";
   std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment();
   std::vector<std::pair<Term, Term>> res;
   for (const auto& p : assignment)
@@ -4448,6 +4479,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
     res.emplace_back(Term(this, p.first), Term(this, p.second));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4455,8 +4487,12 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const
  */
 std::string Solver::getInfo(const std::string& flag) const
 {
-  // CHECK: flag valid?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
+      << "Unrecognized flag for getInfo.";
+
   return d_smtEngine->getInfo(flag).toString();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4464,9 +4500,10 @@ std::string Solver::getInfo(const std::string& flag) const
  */
 std::string Solver::getOption(const std::string& option) const
 {
-  // CHECK: option exists?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   SExpr res = d_smtEngine->getOption(option);
   return res.toString();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4474,9 +4511,18 @@ std::string Solver::getOption(const std::string& option) const
  */
 std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
-  // CHECK: incremental?
-  // CHECK: option produce-unsat-assumptions set?
-  // CHECK: last check sat/valid result is unsat/invalid
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::incrementalSolving())
+      << "Cannot get unsat assumptions unless incremental solving is enabled "
+         "(try --incremental)";
+  CVC4_API_CHECK(CVC4::options::unsatAssumptions())
+      << "Cannot get unsat assumptions unless explicitly enabled "
+         "(try --produce-unsat-assumptions)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get unsat assumptions unless in unsat mode.";
+
   std::vector<Expr> uassumptions = d_smtEngine->getUnsatAssumptions();
   /* Can not use
    *   return std::vector<Term>(uassumptions.begin(), uassumptions.end());
@@ -4487,6 +4533,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4494,7 +4541,14 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
  */
 std::vector<Term> Solver::getUnsatCore(void) const
 {
-  // CHECK: result unsat?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::unsatCores())
+      << "Cannot get unsat core unless explicitly enabled "
+         "(try --produce-unsat-cores)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 == SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get unsat core unless in unsat mode.";
   UnsatCore core = d_smtEngine->getUnsatCore();
   /* Can not use
    *   return std::vector<Term>(core.begin(), core.end());
@@ -4505,6 +4559,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
     res.push_back(Term(this, e));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4512,10 +4567,10 @@ std::vector<Term> Solver::getUnsatCore(void) const
  */
 Term Solver::getValue(Term term) const
 {
-  // CHECK:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(expr.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_SOLVER_CHECK_TERM(term);
   return Term(this, d_smtEngine->getValue(*term.d_expr));
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4523,17 +4578,25 @@ Term Solver::getValue(Term term) const
  */
 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
-  // CHECK:
-  // for e in exprs:
-  // NodeManager::fromExprManager(d_exprMgr)
-  // == NodeManager::fromExprManager(e.getExprManager())
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get value unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get value when in unsat mode.";
   std::vector<Term> res;
-  for (const Term& t : terms)
+  for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "term", terms[i], i)
+        << "term associated to this solver object";
     /* Can not use emplace_back here since constructor is private. */
-    res.push_back(Term(this, d_smtEngine->getValue(*t.d_expr)));
+    res.push_back(Term(this, d_smtEngine->getValue(*terms[i].d_expr)));
   }
   return res;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4558,8 +4621,16 @@ void Solver::pop(uint32_t nscopes) const
 
 void Solver::printModel(std::ostream& out) const
 {
-  // CHECK: produce-models?
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
+  CVC4_API_CHECK(CVC4::options::produceModels())
+      << "Cannot get value unless model generation is enabled "
+         "(try --produce-models)";
+  CVC4_API_CHECK(d_smtEngine->getSmtMode()
+                 != SmtEngine::SmtMode::SMT_MODE_UNSAT)
+      << "Cannot get value when in unsat mode.";
   out << *d_smtEngine->getModel();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4583,22 +4654,11 @@ void Solver::push(uint32_t nscopes) const
 /**
  *  ( reset-assertions )
  */
-void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); }
-
-// TODO: issue #2781
-void Solver::setLogicHelper(const std::string& logic) const
+void Solver::resetAssertions(void) const
 {
-  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
-      << "Invalid call to 'setLogic', solver is already fully initialized";
-  try
-  {
-    CVC4::LogicInfo logic_info(logic);
-    d_smtEngine->setLogic(logic_info);
-  }
-  catch (CVC4::IllegalArgumentException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  d_smtEngine->resetAssertions();
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
@@ -4606,6 +4666,7 @@ void Solver::setLogicHelper(const std::string& logic) const
  */
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_EXPECTED(
       keyword == "source" || keyword == "category" || keyword == "difficulty"
           || keyword == "filename" || keyword == "license" || keyword == "name"
@@ -4625,12 +4686,21 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
       << "'sat', 'unsat' or 'unknown'";
 
   d_smtEngine->setInfo(keyword, value);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**
  *  ( set-logic <symbol> )
  */
-void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
+void Solver::setLogic(const std::string& logic) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_CHECK(!d_smtEngine->isFullyInited())
+      << "Invalid call to 'setLogic', solver is already fully initialized";
+  CVC4::LogicInfo logic_info(logic);
+  d_smtEngine->setLogic(logic_info);
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
 
 /**
  *  ( set-option <option> )
@@ -4638,16 +4708,11 @@ void Solver::setLogic(const std::string& logic) const { setLogicHelper(logic); }
 void Solver::setOption(const std::string& option,
                        const std::string& value) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_CHECK(!d_smtEngine->isFullyInited())
       << "Invalid call to 'setOption', solver is already fully initialized";
-  try
-  {
-    d_smtEngine->setOption(option, value);
-  }
-  catch (CVC4::OptionException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
+  d_smtEngine->setOption(option, value);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
@@ -4684,6 +4749,7 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(sort);
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
   (void)res.getType(true); /* kick off type checking */
@@ -4698,12 +4764,22 @@ Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
 Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
                                const std::vector<Term>& ntSymbols) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)
       << "non-empty vector";
 
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        boundVars[i],
+        i)
+        << "a bound variable";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !boundVars[i].isNull(), "parameter term", boundVars[i], i)
         << "non-null term";
   }
@@ -4711,11 +4787,21 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
   for (size_t i = 0, n = ntSymbols.size(); i < n; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == ntSymbols[i].d_solver, "term", ntSymbols[i], i)
+        << "term associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        ntSymbols[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        ntSymbols[i],
+        i)
+        << "a bound variable";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i)
         << "non-null term";
   }
 
   return Grammar(this, boundVars, ntSymbols);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 Term Solver::synthFun(const std::string& symbol,
@@ -4764,10 +4850,20 @@ Term Solver::synthFunHelper(const std::string& symbol,
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
+        << "bound variable associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        boundVars[i].d_expr->getKind() == CVC4::Kind::BOUND_VARIABLE,
+        "bound variable",
+        boundVars[i],
+        i)
+        << "a bound variable";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !boundVars[i].isNull(), "parameter term", boundVars[i], i)
         << "non-null term";
     varTypes.push_back(boundVars[i].d_expr->getType());
   }
+  CVC4_API_SOLVER_CHECK_SORT(sort);
 
   if (g != nullptr)
   {
@@ -4796,12 +4892,15 @@ Term Solver::synthFunHelper(const std::string& symbol,
 
 void Solver::addSygusConstraint(Term term) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
   CVC4_API_ARG_CHECK_EXPECTED(
       term.d_expr->getType() == d_exprMgr->booleanType(), term)
       << "boolean term";
 
   d_smtEngine->assertSygusConstraint(*term.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 void Solver::addSygusInvConstraint(Term inv,
@@ -4809,10 +4908,15 @@ void Solver::addSygusInvConstraint(Term inv,
                                    Term trans,
                                    Term post) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(inv);
+  CVC4_API_SOLVER_CHECK_TERM(inv);
   CVC4_API_ARG_CHECK_NOT_NULL(pre);
+  CVC4_API_SOLVER_CHECK_TERM(pre);
   CVC4_API_ARG_CHECK_NOT_NULL(trans);
+  CVC4_API_SOLVER_CHECK_TERM(trans);
   CVC4_API_ARG_CHECK_NOT_NULL(post);
+  CVC4_API_SOLVER_CHECK_TERM(post);
 
   CVC4_API_ARG_CHECK_EXPECTED(inv.d_expr->getType().isFunction(), inv)
       << "a function";
@@ -4847,13 +4951,21 @@ void Solver::addSygusInvConstraint(Term inv,
 
   d_smtEngine->assertSygusInvConstraint(
       *inv.d_expr, *pre.d_expr, *trans.d_expr, *post.d_expr);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Result Solver::checkSynth() const { return d_smtEngine->checkSynth(); }
+Result Solver::checkSynth() const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  return d_smtEngine->checkSynth();
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
 
 Term Solver::getSynthSolution(Term term) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_CHECK_NOT_NULL(term);
+  CVC4_API_SOLVER_CHECK_TERM(term);
 
   std::map<CVC4::Expr, CVC4::Expr> map;
   CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
@@ -4865,16 +4977,21 @@ Term Solver::getSynthSolution(Term term) const
   CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
 
   return Term(this, it->second);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 std::vector<Term> Solver::getSynthSolutions(
     const std::vector<Term>& terms) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector";
 
   for (size_t i = 0, n = terms.size(); i < n; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        this == terms[i].d_solver, "parameter term", terms[i], i)
+        << "parameter term associated to this solver object";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         !terms[i].isNull(), "parameter term", terms[i], i)
         << "non-null term";
   }
@@ -4899,11 +5016,14 @@ std::vector<Term> Solver::getSynthSolutions(
   }
 
   return synthSolution;
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 void Solver::printSynthSolution(std::ostream& out) const
 {
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   d_smtEngine->printSynthSolution(out);
+  CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
 /**