Add missing API checks to getValue (#7475)

Fixes cvc5/cvc5-projects#307.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5e38096c830ca938afd12c3d88323ffe1f99b28b..a342cea53ec9efdf526c56a51a54663e32e43fbf 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7214,7 +7214,7 @@ std::map<Term, Term> Solver::getDifficulty() const
   CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT
                              || d_slv->getSmtMode() == SmtMode::SAT
                              || d_slv->getSmtMode() == SmtMode::SAT_UNKNOWN)
-      << "Cannot get difficulty unless after a UNSAT, SAT or unknown response.";
+      << "Cannot get difficulty unless after a UNSAT, SAT or UNKNOWN response.";
   //////// all checks before this line
   std::map<Term, Term> res;
   std::map<Node, Node> dmap;
@@ -7242,7 +7242,14 @@ std::string Solver::getProof(void) const
 Term Solver::getValue(const Term& term) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_RECOVERABLE_CHECK(d_slv->getOptions().smt.produceModels)
+      << "Cannot get value unless model generation is enabled "
+         "(try --produce-models)";
+  CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
+      << "Cannot get value unless after a SAT or UNKNOWN response.";
   CVC5_API_SOLVER_CHECK_TERM(term);
+  CVC5_API_RECOVERABLE_CHECK(term.getSort().isFirstClass())
+      << "Cannot get value of a term that is not first class.";
   //////// all checks before this line
   return getValueHelper(term);
   ////////
@@ -7256,7 +7263,12 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Cannot get value unless after a SAT or unknown response.";
+      << "Cannot get value unless after a SAT or UNKNOWN response.";
+  for (const Term& t : terms)
+  {
+    CVC5_API_RECOVERABLE_CHECK(t.getSort().isFirstClass())
+        << "Cannot get value of a term that is not first class.";
+  }
   CVC5_API_SOLVER_CHECK_TERMS(terms);
   //////// all checks before this line
 
@@ -7278,7 +7290,7 @@ std::vector<Term> Solver::getModelDomainElements(const Sort& s) const
       << "Cannot get domain elements unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Cannot get domain elements unless after a SAT or unknown response.";
+      << "Cannot get domain elements unless after a SAT or UNKNOWN response.";
   CVC5_API_SOLVER_CHECK_SORT(s);
   CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort())
       << "Expecting an uninterpreted sort as argument to "
@@ -7302,7 +7314,7 @@ bool Solver::isModelCoreSymbol(const Term& v) const
       << "Cannot check if model core symbol unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Cannot check if model core symbol unless after a SAT or unknown "
+      << "Cannot check if model core symbol unless after a SAT or UNKNOWN "
          "response.";
   CVC5_API_SOLVER_CHECK_TERM(v);
   CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT)
@@ -7321,7 +7333,7 @@ std::string Solver::getModel(const std::vector<Sort>& sorts,
       << "Cannot get model unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Cannot get model unless after a SAT or unknown response.";
+      << "Cannot get model unless after a SAT or UNKNOWN response.";
   CVC5_API_SOLVER_CHECK_SORTS(sorts);
   for (const Sort& s : sorts)
   {
@@ -7387,7 +7399,7 @@ Term Solver::getSeparationHeap() const
       << "Cannot get separation heap term unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Can only get separtion heap term after sat or unknown response.";
+      << "Can only get separtion heap term after SAT or UNKNOWN response.";
   //////// all checks before this line
   return Term(this, d_slv->getSepHeapExpr());
   ////////
@@ -7404,7 +7416,7 @@ Term Solver::getSeparationNilTerm() const
       << "Cannot get separation nil term unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Can only get separtion nil term after sat or unknown response.";
+      << "Can only get separtion nil term after SAT or UNKNOWN response.";
   //////// all checks before this line
   return Term(this, d_slv->getSepNilExpr());
   ////////
@@ -7523,7 +7535,7 @@ void Solver::blockModel() const
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Can only block model after sat or unknown response.";
+      << "Can only block model after SAT or UNKNOWN response.";
   //////// all checks before this line
   d_slv->blockModel();
   ////////
@@ -7537,7 +7549,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat())
-      << "Can only block model values after sat or unknown response.";
+      << "Can only block model values after SAT or UNKNOWN response.";
   CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
       << "a non-empty set of terms";
   CVC5_API_SOLVER_CHECK_TERMS(terms);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a3fd70683bf58cfbeb479fc515ef2273cbc5b12c..2529a862291ee5017ee8f75f490405c6fb8983ac 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -856,6 +856,7 @@ set(regress_0_tests
   regress0/printer/let_shadowing.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc.smt2
+  regress0/proj-issue307-get-value-re.smt2
   regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/lfsc-test-1.smt2

diff --git a/test/regress/regress0/cvc-rerror-print.cvc.smt2 b/test/regress/regress0/cvc-rerror-print.cvc.smt2
index 03ba7c91ce9bd37b55169e38dce23d15254642c3..d3ffb7a7ea7e3c3d441c3e459d8c4ddcffe8ec0b 100644 (file)
--- a/test/regress/regress0/cvc-rerror-print.cvc.smt2
+++ b/test/regress/regress0/cvc-rerror-print.cvc.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; EXPECT: (error "Cannot get model unless after a SAT or unknown response.")
+; EXPECT: (error "Cannot get model unless after a SAT or UNKNOWN response.")
 (set-option :incremental false)
 (set-logic ALL)
 (set-option :produce-models true)

diff --git a/test/regress/regress0/proj-issue307-get-value-re.smt2 b/test/regress/regress0/proj-issue307-get-value-re.smt2
new file mode 100644 (file)
index 0000000..c52e476
--- /dev/null
+++ b/test/regress/regress0/proj-issue307-get-value-re.smt2
@@ -0,0 +1,7 @@
+; SCRUBBER: grep -v -E '\(error'
+; EXPECT: sat
+(reset)
+(set-logic ALL)
+(set-option :produce-models true)
+(check-sat)
+(get-value ((re.opt re.allchar)))