Add well formed term check to solver engine (#8056)

Fixes cvc5/cvc5-projects#413.

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 546fdc34f22b1002edda6c081c2bc9c71882536b..e67877fad0459f93b814ba92dc9bde15f2ff7ec3 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -22,6 +22,7 @@
 #include "decision/decision_engine.h"
 #include "expr/bound_var_manager.h"
 #include "expr/node.h"
+#include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/language.h"
@@ -869,6 +870,8 @@ Result SolverEngine::assertFormula(const Node& formula)
   finishInit();
   d_state->doPendingPops();
 
+  // as an optimization we do not check whether formula is well-formed here, and
+  // defer this check for certain cases within the assertions module.
   Trace("smt") << "SolverEngine::assertFormula(" << formula << ")" << endl;
 
   // Substitute out any abstract values in ex
@@ -980,6 +983,7 @@ Node SolverEngine::getValue(const Node& ex) const
 {
   SolverEngineScope smts(this);
 
+  ensureWellFormedTerm(ex, "get value");
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   TypeNode expectedType = ex.getType();
 
@@ -1152,6 +1156,11 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
 
   finishInit();
 
+  for (const Node& e : exprs)
+  {
+    ensureWellFormedTerm(e, "block model values");
+  }
+
   TheoryModel* m = getAvailableModel("block model values");
 
   // get expanded assertions
@@ -1199,6 +1208,20 @@ std::vector<Node> SolverEngine::getAssertionsInternal()
 
 const Options& SolverEngine::options() const { return d_env->getOptions(); }
 
+void SolverEngine::ensureWellFormedTerm(const Node& n,
+                                        const std::string& src) const
+{
+  bool wasShadow = false;
+  if (expr::hasFreeOrShadowedVar(n, wasShadow))
+  {
+    std::string varType(wasShadow ? "shadowed" : "free");
+    std::stringstream se;
+    se << "Cannot process term with " << varType << " variable in " << src
+       << ".";
+    throw ModalException(se.str().c_str());
+  }
+}
+
 std::vector<Node> SolverEngine::getExpandedAssertions()
 {
   std::vector<Node> easserts = getAssertions();

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index dd98c674ee421106b1f05a34b3be865958eaa3b8..3d7dd5be738e6658086747f98f7e3400fd92de46 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -1048,6 +1048,16 @@ class CVC5_EXPORT SolverEngine
    */
   const Options& options() const;
 
+  /**
+   * Check that the given term is a valid closed term, which can be used as an
+   * argument to, e.g., assert, get-value, block-model-values, etc.
+   *
+   * @param n The node to check
+   * @param src The source of the check, which is printed in the exception if
+   * this check fails.
+   */
+  void ensureWellFormedTerm(const Node& n, const std::string& src) const;
+
   /* Members -------------------------------------------------------------- */
 
   /** Solver instance that owns this SolverEngine instance. */

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 3cb5155ab950e9bff36ced0b0598ec63a225fbe7..f8ace3570fc87919a8ff709851b4e2aabe84906f 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3003,5 +3003,21 @@ TEST_F(TestApiBlackSolver, proj_issue414)
   ASSERT_NO_THROW(slv.simplify(t54));
 }
 
+TEST_F(TestApiBlackSolver, proj_issue431)
+{
+  Solver slv;
+  slv.setOption("produce-models", "true");
+  slv.setOption("produce-unsat-assumptions", "true");
+  slv.setOption("produce-assertions", "true");
+  Sort s1 = slv.getStringSort();
+  Sort s3 = slv.getIntegerSort();
+  Sort s7 = slv.mkArraySort(s1, s3);
+  Term t3 = slv.mkConst(s1, "_x2");
+  Term t57 = slv.mkVar(s7, "_x38");
+  Term t103 = slv.mkTerm(Kind::SELECT, {t57, t3});
+  slv.checkSat();
+  ASSERT_THROW(slv.blockModelValues({t103}), CVC5ApiException);
+}
+
 }  // namespace test
 }  // namespace cvc5