From 61321e583c889ca097b1ac008899a43467cabc21 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 27 Oct 2021 18:52:44 -0500 Subject: [PATCH] Add missing API checks to getValue (#7475) Fixes cvc5/cvc5-projects#307. --- src/api/cpp/cvc5.cpp | 30 +++++++++++++------ test/regress/CMakeLists.txt | 1 + .../regress0/cvc-rerror-print.cvc.smt2 | 2 +- .../regress0/proj-issue307-get-value-re.smt2 | 7 +++++ 4 files changed, 30 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/proj-issue307-get-value-re.smt2 diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 5e38096c8..a342cea53 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7214,7 +7214,7 @@ std::map 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 res; std::map 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 Solver::getValue(const std::vector& 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 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& 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& 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 a3fd70683..2529a8622 100644 --- 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 03ba7c91c..d3ffb7a7e 100644 --- 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 index 000000000..c52e476e0 --- /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))) -- 2.30.2