From: Andrew Reynolds Date: Thu, 24 Feb 2022 18:28:58 +0000 (-0600) Subject: Check for free variables in several SolverEngine calls (#8130) X-Git-Tag: cvc5-1.0.0~387 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4972960da74afd20fdae8fbb2ca49412866bd9c0;p=cvc5.git Check for free variables in several SolverEngine calls (#8130) Fixes the nightlies due to ensuring that a unit test fails in production (it was failing only in debug). Fixes #8127. --- diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp index 3d11d1bd0..d8c9327b8 100644 --- a/examples/api/cpp/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp @@ -22,7 +22,7 @@ using namespace cvc5::api; int main() { Solver slv; - Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); + Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!"); std::cout << helloworld << " is " << slv.checkEntailed(helloworld) << std::endl; return 0; diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 7535430e3..3c2de1e2d 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -21,7 +21,7 @@ public class HelloWorld { try (Solver slv = new Solver()) { - Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!"); + Term helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!"); System.out.println(helloworld + " is " + slv.checkEntailed(helloworld)); } diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 99fec60b4..51f8b911d 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -57,6 +57,7 @@ #include "expr/sequence.h" #include "expr/type_node.h" #include "options/base_options.h" +#include "options/expr_options.h" #include "options/main_options.h" #include "options/option_exception.h" #include "options/options.h" @@ -5435,6 +5436,34 @@ bool Solver::isValidInteger(const std::string& s) const return true; } +void Solver::ensureWellFormedTerm(const Term& t) const +{ + // only check if option is set + if (d_slv->getOptions().expr.wellFormedChecking) + { + bool wasShadow = false; + if (expr::hasFreeOrShadowedVar(*t.d_node, wasShadow)) + { + std::stringstream se; + se << "Cannot process term with " << (wasShadow ? "shadowed" : "free") + << " variable"; + throw CVC5ApiException(se.str().c_str()); + } + } +} + +void Solver::ensureWellFormedTerms(const std::vector& ts) const +{ + // only check if option is set + if (d_slv->getOptions().expr.wellFormedChecking) + { + for (const Term& t : ts) + { + ensureWellFormedTerm(t); + } + } +} + void Solver::resetStatistics() { if constexpr (configuration::isStatisticsBuild()) @@ -6631,6 +6660,7 @@ Result Solver::checkEntailed(const Term& term) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); + ensureWellFormedTerm(term); //////// all checks before this line return d_slv->checkEntailed(*term.d_node); //////// @@ -6645,6 +6675,7 @@ Result Solver::checkEntailed(const std::vector& terms) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line return d_slv->checkEntailed(Term::termVectorToNodes(terms)); //////// @@ -6659,6 +6690,7 @@ void Solver::assertFormula(const Term& term) const CVC5_API_TRY_CATCH_BEGIN; CVC5_API_SOLVER_CHECK_TERM(term); CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, getBooleanSort()); + ensureWellFormedTerm(term); //////// all checks before this line d_slv->assertFormula(*term.d_node); //////// @@ -6686,6 +6718,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); + ensureWellFormedTerm(assumption); //////// all checks before this line return d_slv->checkSat(*assumption.d_node); //////// @@ -6700,6 +6733,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); + ensureWellFormedTerms(assumptions); //////// all checks before this line for (const Term& term : assumptions) { @@ -7286,6 +7320,7 @@ Term Solver::getValue(const Term& term) const CVC5_API_RECOVERABLE_CHECK(!term.getSort().isDatatype() || term.getSort().getDatatype().isWellFounded()) << "Cannot get value of a term of non-well-founded datatype sort."; + ensureWellFormedTerm(term); //////// all checks before this line return getValueHelper(term); //////// @@ -7309,6 +7344,7 @@ std::vector Solver::getValue(const std::vector& terms) const << "Cannot get value of a term of non-well-founded datatype sort."; } CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line std::vector res; @@ -7644,6 +7680,7 @@ void Solver::blockModelValues(const std::vector& terms) const CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "a non-empty set of terms"; CVC5_API_SOLVER_CHECK_TERMS(terms); + ensureWellFormedTerms(terms); //////// all checks before this line d_slv->blockModelValues(Term::termVectorToNodes(terms)); //////// diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 0256f0e61..e75bef293 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -5001,6 +5001,16 @@ class CVC5_EXPORT Solver /** Check whether string s is a valid decimal integer. */ bool isValidInteger(const std::string& s) 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 t The term to check + */ + void ensureWellFormedTerm(const Term& t) const; + /** Vector version of above. */ + void ensureWellFormedTerms(const std::vector& ts) const; + /** Increment the term stats counter. */ void increment_term_stats(Kind kind) const; /** Increment the vars stats (if 'is_var') or consts stats counter. */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 73aa3ae7d..1b33f5ac6 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -197,6 +197,12 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) { solver->setOption("incremental", "false"); } + // we don't need to check that terms passed to API methods are well + // formed, since this should be an invariant of the parser + if (!solver->getOptionInfo("wf-checking").setByUser) + { + solver->setOption("wf-checking", "false"); + } ParserBuilder parserBuilder( pExecutor->getSolver(), pExecutor->getSymbolManager(), true); diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 79bbc9f19..6f2174a4f 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -28,3 +28,11 @@ name = "Expression" type = "bool" default = "DO_SEMANTIC_CHECKS_BY_DEFAULT" help = "type check expressions" + +[[option]] + name = "wellFormedChecking" + category = "regular" + long = "wf-checking" + type = "bool" + default = "true" + help = "check that terms passed to API methods are well formed (default false for text interface)" diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 39ee661a0..1223e9875 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -740,6 +740,7 @@ Result SolverEngine::checkSat() Result SolverEngine::checkSat(const Node& assumption) { + ensureWellFormedTerm(assumption, "checkSat"); std::vector assump; if (!assumption.isNull()) { @@ -750,11 +751,13 @@ Result SolverEngine::checkSat(const Node& assumption) Result SolverEngine::checkSat(const std::vector& assumptions) { + ensureWellFormedTerms(assumptions, "checkSat"); return checkSatInternal(assumptions, false); } Result SolverEngine::checkEntailed(const Node& node) { + ensureWellFormedTerm(node, "checkEntailed"); return checkSatInternal( node.isNull() ? std::vector() : std::vector{node}, true) @@ -763,6 +766,7 @@ Result SolverEngine::checkEntailed(const Node& node) Result SolverEngine::checkEntailed(const std::vector& nodes) { + ensureWellFormedTerms(nodes, "checkEntailed"); return checkSatInternal(nodes, true).asEntailmentResult(); } @@ -853,7 +857,12 @@ Result SolverEngine::assertFormula(const Node& formula) SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); + ensureWellFormedTerm(formula, "assertFormula"); + return assertFormulaInternal(formula); +} +Result SolverEngine::assertFormulaInternal(const Node& formula) +{ // 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; @@ -863,7 +872,7 @@ Result SolverEngine::assertFormula(const Node& formula) d_asserts->assertFormula(n); return quickCheck().asEntailmentResult(); -} /* SolverEngine::assertFormula() */ +} /* -------------------------------------------------------------------------- @@ -1130,7 +1139,7 @@ Result SolverEngine::blockModel() Node eblocker = mb.getModelBlocker( eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; - return assertFormula(eblocker); + return assertFormulaInternal(eblocker); } Result SolverEngine::blockModelValues(const std::vector& exprs) @@ -1153,7 +1162,7 @@ Result SolverEngine::blockModelValues(const std::vector& exprs) ModelBlocker mb(*d_env.get()); Node eblocker = mb.getModelBlocker( eassertsProc, m, options::BlockModelsMode::VALUES, exprs); - return assertFormula(eblocker); + return assertFormulaInternal(eblocker); } std::pair SolverEngine::getSepHeapAndNilExpr(void) @@ -1195,14 +1204,29 @@ 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)) + if (Configuration::isAssertionBuild()) + { + 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()); + } + } +} + +void SolverEngine::ensureWellFormedTerms(const std::vector& ns, + const std::string& src) const +{ + if (Configuration::isAssertionBuild()) { - std::string varType(wasShadow ? "shadowed" : "free"); - std::stringstream se; - se << "Cannot process term with " << varType << " variable in " << src - << "."; - throw ModalException(se.str().c_str()); + for (const Node& n : ns) + { + ensureWellFormedTerm(n, src); + } } } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index a0c81f5fa..fd1057f3d 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -903,6 +903,9 @@ class CVC5_EXPORT SolverEngine */ UnsatCore getUnsatCoreInternal(); + /** Internal version of assertFormula */ + Result assertFormulaInternal(const Node& formula); + /** * Check that a generated proof checks. This method is the same as printProof, * but does not print the proof. Like that method, it should be called @@ -1056,6 +1059,9 @@ class CVC5_EXPORT SolverEngine * this check fails. */ void ensureWellFormedTerm(const Node& n, const std::string& src) const; + /** Vector version of above. */ + void ensureWellFormedTerms(const std::vector& ns, + const std::string& src) const; /* Members -------------------------------------------------------------- */ diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 9bf6b8491..23f48caa2 100644 --- a/test/unit/api/cpp/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp @@ -36,7 +36,7 @@ TEST_F(TestApiBlackResult, isNull) ASSERT_FALSE(res_null.isNotEntailed()); ASSERT_FALSE(res_null.isEntailmentUnknown()); Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); cvc5::api::Result res = d_solver.checkSat(); ASSERT_FALSE(res.isNull()); @@ -45,7 +45,7 @@ TEST_F(TestApiBlackResult, isNull) TEST_F(TestApiBlackResult, eq) { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); cvc5::api::Result res; cvc5::api::Result res2 = d_solver.checkSat(); @@ -58,7 +58,7 @@ TEST_F(TestApiBlackResult, eq) TEST_F(TestApiBlackResult, isSat) { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); cvc5::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isSat()); @@ -68,7 +68,7 @@ TEST_F(TestApiBlackResult, isSat) TEST_F(TestApiBlackResult, isUnsat) { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); cvc5::api::Result res = d_solver.checkSat(); ASSERT_TRUE(res.isUnsat()); @@ -81,7 +81,7 @@ TEST_F(TestApiBlackResult, isSatUnknown) d_solver.setOption("incremental", "false"); d_solver.setOption("solve-int-as-bv", "32"); Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkVar(int_sort, "x"); + Term x = d_solver.mkConst(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); cvc5::api::Result res = d_solver.checkSat(); ASSERT_FALSE(res.isSat()); @@ -111,7 +111,7 @@ TEST_F(TestApiBlackResult, isEntailmentUnknown) d_solver.setOption("incremental", "false"); d_solver.setOption("solve-int-as-bv", "32"); Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkVar(int_sort, "x"); + Term x = d_solver.mkConst(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); cvc5::api::Result res = d_solver.checkEntailed(x.eqTerm(x)); ASSERT_FALSE(res.isEntailed()); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index c6a303c8f..7234dc796 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3052,7 +3052,8 @@ TEST_F(TestApiBlackSolver, proj_issue434) Term t1040 = slv.defineFun("_f45", {t1014}, t1039.getSort(), t1039); Term t1072 = slv.mkTerm(Kind::APPLY_UF, {t1040, t510}); Term t1073 = slv.mkTerm(Kind::APPLY_UF, {t73, t1072}); - ASSERT_NO_THROW(slv.checkSatAssuming({t1073, t510})); + // the query has free variables, and should throw an exception + ASSERT_THROW(slv.checkSatAssuming({t1073, t510}), CVC5ApiException); } TEST_F(TestApiBlackSolver, proj_issue436) diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index 59bd752ca..96266bce9 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -47,7 +47,7 @@ class ResultTest assertFalse(res_null.isNotEntailed()); assertFalse(res_null.isEntailmentUnknown()); Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); Result res = d_solver.checkSat(); assertFalse(res.isNull()); @@ -56,7 +56,7 @@ class ResultTest @Test void eq() { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); Result res; Result res2 = d_solver.checkSat(); @@ -69,7 +69,7 @@ class ResultTest @Test void isSat() { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); Result res = d_solver.checkSat(); assertTrue(res.isSat()); @@ -79,7 +79,7 @@ class ResultTest @Test void isUnsat() { Sort u_sort = d_solver.mkUninterpretedSort("u"); - Term x = d_solver.mkVar(u_sort, "x"); + Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); Result res = d_solver.checkSat(); assertTrue(res.isUnsat()); @@ -92,7 +92,7 @@ class ResultTest d_solver.setOption("incremental", "false"); d_solver.setOption("solve-int-as-bv", "32"); Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkVar(int_sort, "x"); + Term x = d_solver.mkConst(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); Result res = d_solver.checkSat(); assertFalse(res.isSat()); @@ -122,7 +122,7 @@ class ResultTest d_solver.setOption("incremental", "false"); d_solver.setOption("solve-int-as-bv", "32"); Sort int_sort = d_solver.getIntegerSort(); - Term x = d_solver.mkVar(int_sort, "x"); + Term x = d_solver.mkConst(int_sort, "x"); d_solver.assertFormula(x.eqTerm(x).notTerm()); Result res = d_solver.checkEntailed(x.eqTerm(x)); assertFalse(res.isEntailed()); diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index 27160f543..247451756 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -36,7 +36,7 @@ def test_is_null(solver): assert not res_null.isNotEntailed() assert not res_null.isEntailmentUnknown() u_sort = solver.mkUninterpretedSort("u") - x = solver.mkVar(u_sort, "x") + x = solver.mkConst(u_sort, "x") solver.assertFormula(x.eqTerm(x)) res = solver.checkSat() assert not res.isNull() @@ -44,7 +44,7 @@ def test_is_null(solver): def test_eq(solver): u_sort = solver.mkUninterpretedSort("u") - x = solver.mkVar(u_sort, "x") + x = solver.mkConst(u_sort, "x") solver.assertFormula(x.eqTerm(x)) res2 = solver.checkSat() res3 = solver.checkSat() @@ -55,7 +55,7 @@ def test_eq(solver): def test_is_sat(solver): u_sort = solver.mkUninterpretedSort("u") - x = solver.mkVar(u_sort, "x") + x = solver.mkConst(u_sort, "x") solver.assertFormula(x.eqTerm(x)) res = solver.checkSat() assert res.isSat() @@ -64,7 +64,7 @@ def test_is_sat(solver): def test_is_unsat(solver): u_sort = solver.mkUninterpretedSort("u") - x = solver.mkVar(u_sort, "x") + x = solver.mkConst(u_sort, "x") solver.assertFormula(x.eqTerm(x).notTerm()) res = solver.checkSat() assert res.isUnsat() @@ -76,7 +76,7 @@ def test_is_sat_unknown(solver): solver.setOption("incremental", "false") solver.setOption("solve-int-as-bv", "32") int_sort = solver.getIntegerSort() - x = solver.mkVar(int_sort, "x") + x = solver.mkConst(int_sort, "x") solver.assertFormula(x.eqTerm(x).notTerm()) res = solver.checkSat() assert not res.isSat() @@ -104,7 +104,7 @@ def test_is_entailment_unknown(solver): solver.setOption("incremental", "false") solver.setOption("solve-int-as-bv", "32") int_sort = solver.getIntegerSort() - x = solver.mkVar(int_sort, "x") + x = solver.mkConst(int_sort, "x") solver.assertFormula(x.eqTerm(x).notTerm()) res = solver.checkEntailed(x.eqTerm(x)) assert not res.isEntailed()