From: Andrew Reynolds Date: Tue, 8 Feb 2022 03:55:07 +0000 (-0600) Subject: Always produce assertions (#8041) X-Git-Tag: cvc5-1.0.0~439 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18cf7ab96a810c0c599de7bc005db1b8b2c2146a;p=cvc5.git Always produce assertions (#8041) There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b246b7547..99fec60b4 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7639,9 +7639,6 @@ void Solver::blockModelValues(const std::vector& terms) const CVC5_API_CHECK(d_slv->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; - CVC5_API_CHECK(d_slv->getOptions().smt.produceAssertions) - << "Cannot block model value unless produce-assertions is enabled " - "(try --produce-assertions)"; CVC5_API_RECOVERABLE_CHECK(d_slv->isSmtModeSat()) << "Can only block model values after SAT or UNKNOWN response."; CVC5_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5c2659190..0256f0e61 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4566,9 +4566,7 @@ class CVC5_EXPORT Solver * * Requires enabling option * :ref:`produce-models `. - * 'produce-models' and setting option - * :ref:`block-models `. - * to a mode other than ``none``. + * 'produce-models'. * \endverbatim */ void blockModelValues(const std::vector& terms) const; diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 2b32f18ce..43493f784 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -2292,8 +2292,7 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( block-model-values ( + ) ) * } - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". + * Requires enabling 'produce-models' option. */ public void blockModelValues(Term[] terms) { diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 2ae6fbd31..0af1d703b 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -245,7 +245,8 @@ name = "SMT Layer" long = "produce-assertions" type = "bool" alias = ["interactive-mode"] - help = "keep an assertions list (enables get-assertions command)" + default = "true" + help = "keep an assertions list. Note this option is always enabled." [[option]] name = "doITESimp" diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 136cdaf8c..188c5046b 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -37,7 +37,6 @@ namespace smt { Assertions::Assertions(Env& env, AbstractValues& absv) : EnvObj(env), d_absValues(absv), - d_produceAssertions(false), d_assertionList(userContext()), d_assertionListDefs(userContext()), d_globalDefineFunLemmasIndex(userContext(), 0), @@ -52,33 +51,15 @@ Assertions::~Assertions() void Assertions::refresh() { - if (d_globalDefineFunLemmas != nullptr) + // Global definitions are asserted now to ensure they always exist. This is + // done at the beginning of preprocessing, to ensure that definitions take + // priority over, e.g. solving during preprocessing. See issue #7479. + size_t numGlobalDefs = d_globalDefineFunLemmas.size(); + for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++) { - // Global definitions are asserted now to ensure they always exist. This is - // done at the beginning of preprocessing, to ensure that definitions take - // priority over, e.g. solving during preprocessing. See issue #7479. - size_t numGlobalDefs = d_globalDefineFunLemmas->size(); - for (size_t i = d_globalDefineFunLemmasIndex.get(); i < numGlobalDefs; i++) - { - addFormula((*d_globalDefineFunLemmas)[i], false, true, false); - } - d_globalDefineFunLemmasIndex = numGlobalDefs; - } -} - -void Assertions::finishInit() -{ - // [MGD 10/20/2011] keep around in incremental mode, due to a - // cleanup ordering issue and Nodes/TNodes. If SAT is popped - // first, some user-context-dependent TNodes might still exist - // with rc == 0. - if (options().smt.produceAssertions || options().base.incrementalSolving) - { - // In the case of incremental solving, we appear to need these to - // ensure the relevant Nodes remain live. - d_produceAssertions = true; - d_globalDefineFunLemmas.reset(new std::vector()); + addFormula(d_globalDefineFunLemmas[i], false, true, false); } + d_globalDefineFunLemmasIndex = numGlobalDefs; } void Assertions::clearCurrent() @@ -157,14 +138,11 @@ void Assertions::addFormula(TNode n, bool isFunDef, bool maybeHasFv) { - // add to assertion list if it exists - if (d_produceAssertions) + // add to assertion list + d_assertionList.push_back(n); + if (isFunDef) { - d_assertionList.push_back(n); - if (isFunDef) - { - d_assertionListDefs.push_back(n); - } + d_assertionListDefs.push_back(n); } if (n.isConst() && n.getConst()) { @@ -221,12 +199,12 @@ void Assertions::addFormula(TNode n, void Assertions::addDefineFunDefinition(Node n, bool global) { n = d_absValues.substituteAbstractValues(n); - if (global && d_globalDefineFunLemmas != nullptr) + if (global) { // Global definitions are asserted at check-sat-time because we have to // make sure that they are always present Assert(!language::isLangSygus(options().base.inputLanguage)); - d_globalDefineFunLemmas->emplace_back(n); + d_globalDefineFunLemmas.emplace_back(n); } else { diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 96e5712a4..acc5f2a4c 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -46,11 +46,6 @@ class Assertions : protected EnvObj public: Assertions(Env& env, AbstractValues& absv); ~Assertions(); - /** - * Finish initialization, called once after options are finalized. Sets up - * the required bookkeeping based on the options. - */ - void finishInit(); /** * Clears out the non-context-dependent data in this class. Necessary to * clear out our assertion vectors in case someone does a push-assert-pop @@ -167,8 +162,6 @@ class Assertions : protected EnvObj bool maybeHasFv); /** Reference to the abstract values utility */ AbstractValues& d_absValues; - /** Whether we are producing assertions */ - bool d_produceAssertions; /** * The assertion list (before any conversion) for supporting getAssertions(). */ @@ -179,7 +172,7 @@ class Assertions : protected EnvObj * List of lemmas generated for global (recursive) function definitions. We * assert this list of definitions in each check-sat call. */ - std::unique_ptr> d_globalDefineFunLemmas; + std::vector d_globalDefineFunLemmas; /** The index of the above list that we have processed */ context::CDO d_globalDefineFunLemmasIndex; /** diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 01d616305..58c83074f 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -457,16 +457,6 @@ void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as) void ProcessAssertions::dumpAssertionsToStream(std::ostream& os, Assertions& as) { - // Cannot print unless produce assertions is enabled. Otherwise, the printing - // is misleading, since it does not capture what symbols were provided - // as definitions. - if (!options().smt.produceAssertions) - { - warning() - << "Assertions not available for dumping (use --produce-assertions)." - << std::endl; - return; - } PrintBenchmark pb(&d_env.getPrinter()); std::vector assertions; // Notice that the following list covers define-fun and define-fun-rec diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 9a459a0d7..8da98e399 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -304,9 +304,8 @@ std::shared_ptr PfManager::getFinalProof( void PfManager::getAssertions(Assertions& as, std::vector& assertions) { + // note that the assertion list is always available const context::CDList& al = as.getAssertionList(); - Assert(options().smt.produceAssertions) - << "Expected produce assertions to be true when checking proof"; for (const Node& a : al) { assertions.push_back(a); diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 387fd8927..8e993d376 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -347,15 +347,9 @@ void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const { - if ((opts.smt.checkModels || opts.smt.checkSynthSol || opts.smt.produceAbducts - || opts.smt.produceInterpols != options::ProduceInterpols::NONE - || opts.smt.modelCoresMode != options::ModelCoresMode::NONE - || opts.smt.blockModelsMode != options::BlockModelsMode::NONE - || opts.smt.produceProofs || isSygus(opts)) - && !opts.smt.produceAssertions) - { - verbose(1) << "SolverEngine: turning on produce-assertions to support " - << "option requiring assertions." << std::endl; + if (!opts.smt.produceAssertions) + { + verbose(1) << "SolverEngine: turning on produce-assertions." << std::endl; opts.smt.produceAssertions = true; } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index ef25d7819..9e8d4703a 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -214,9 +214,6 @@ void SolverEngine::finishInit() // of context-dependent data structures d_state->setup(); - Trace("smt-debug") << "Set up assertions..." << std::endl; - d_asserts->finishInit(); - // subsolvers if (d_env->getOptions().smt.produceAbducts) { @@ -1433,10 +1430,7 @@ void SolverEngine::checkUnsatCore() void SolverEngine::checkModel(bool hardFailure) { const context::CDList& al = d_asserts->getAssertionList(); - // --check-model implies --produce-assertions, which enables the - // assertion list, so we should be ok. - Assert(d_env->getOptions().smt.produceAssertions) - << "don't have an assertion list to check in SolverEngine::checkModel()"; + // we always enable the assertion list, so it is able to be checked TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); @@ -1714,13 +1708,7 @@ std::vector SolverEngine::getAssertions() finishInit(); d_state->doPendingPops(); Trace("smt") << "SMT getAssertions()" << endl; - if (!d_env->getOptions().smt.produceAssertions) - { - const char* msg = - "Cannot query the current assertion list when not in " - "produce-assertions mode."; - throw ModalException(msg); - } + // note we always enable assertions, so it is available here return getAssertionsInternal(); } diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 09f0e18ea..3cb5155ab 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -2102,7 +2102,7 @@ TEST_F(TestApiBlackSolver, blockModelValues2) Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - ASSERT_THROW(d_solver.blockModelValues({x}), CVC5ApiException); + ASSERT_NO_THROW(d_solver.blockModelValues({x})); } TEST_F(TestApiBlackSolver, blockModelValues3) diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 908fed6e5..80921481a 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -2079,7 +2079,7 @@ class SolverTest Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); d_solver.assertFormula(x.eqTerm(x)); d_solver.checkSat(); - assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x})); + assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x})); } @Test void blockModelValues3() throws CVC5ApiException