From 838a04edc3a41c98ee3a8121d4687e987f559fd1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Oct 2021 20:16:20 -0500 Subject: [PATCH] Eliminate more circular dependencies on solver engine (#7311) This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility. --- src/prop/prop_engine.cpp | 2 +- src/prop/prop_engine.h | 2 +- src/prop/prop_proof_manager.cpp | 4 +- src/prop/prop_proof_manager.h | 2 +- src/smt/assertions.cpp | 29 +++++++++----- src/smt/assertions.h | 24 ++++++------ src/smt/check_models.cpp | 4 +- src/smt/check_models.h | 2 +- src/smt/preprocessor.cpp | 19 ++++----- src/smt/preprocessor.h | 18 ++++----- src/smt/process_assertions.cpp | 68 +++++++++++++++------------------ src/smt/process_assertions.h | 20 ++++------ src/smt/proof_manager.cpp | 10 ++--- src/smt/set_defaults.cpp | 7 ++++ src/smt/smt_solver.cpp | 2 +- src/smt/smt_solver.h | 6 +-- src/smt/solver_engine.cpp | 20 +++++----- src/smt/sygus_solver.cpp | 16 ++++---- src/smt/sygus_solver.h | 5 +-- src/smt/unsat_core_manager.cpp | 12 +++--- 20 files changed, 130 insertions(+), 142 deletions(-) diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a98ab02c7..5bd719fe9 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -656,7 +656,7 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const return true; } -void PropEngine::checkProof(context::CDList* assertions) +void PropEngine::checkProof(const context::CDList& assertions) { if (!d_env.isSatProofProducing()) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index ba2c80f46..3556108d1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -286,7 +286,7 @@ class PropEngine /** Checks that the proof is closed w.r.t. asserted formulas to this engine as * well as to the given assertions. */ - void checkProof(context::CDList* assertions); + void checkProof(const context::CDList& assertions); /** * Return the prop engine proof. This should be called only when proofs are diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 09c5fb915..4fb027e54 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -46,7 +46,7 @@ void PropPfManager::registerAssertion(Node assertion) d_assertions.push_back(assertion); } -void PropPfManager::checkProof(context::CDList* assertions) +void PropPfManager::checkProof(const context::CDList& assertions) { Trace("sat-proof") << "PropPfManager::checkProof: Checking if resolution " "proof of false is closed\n"; @@ -55,7 +55,7 @@ void PropPfManager::checkProof(context::CDList* assertions) // connect it with CNF proof d_pfpp->process(conflictProof); // add given assertions d_assertions - for (const Node& assertion : *assertions) + for (const Node& assertion : assertions) { d_assertions.push_back(assertion); } diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index e415ed441..0af1833c3 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -73,7 +73,7 @@ class PropPfManager * engine's proof with the preprocessing proof) and these changes survive for * a next check-sat call. */ - void checkProof(context::CDList* assertions); + void checkProof(const context::CDList& assertions); private: /** A node manager */ diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 704a36915..a9f7ce18e 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -35,10 +35,11 @@ namespace cvc5 { namespace smt { Assertions::Assertions(Env& env, AbstractValues& absv) - : d_env(env), + : EnvObj(env), d_absValues(absv), d_produceAssertions(false), - d_assertionList(env.getUserContext()), + d_assertionList(userContext()), + d_assertionListDefs(userContext()), d_globalNegation(false), d_assertions() { @@ -104,7 +105,7 @@ void Assertions::initializeCheckSat(const std::vector& assumptions, Node n = d_absValues.substituteAbstractValues(e); // Ensure expr is type-checked at this point. ensureBoolean(n); - addFormula(n, true, true, false, false); + addFormula(n, true, false, false); } if (d_globalDefineFunLemmas != nullptr) { @@ -113,7 +114,7 @@ void Assertions::initializeCheckSat(const std::vector& assumptions, // zero assertions) for (const Node& lemma : *d_globalDefineFunLemmas) { - addFormula(lemma, true, false, true, false); + addFormula(lemma, false, true, false); } } } @@ -122,7 +123,7 @@ void Assertions::assertFormula(const Node& n) { ensureBoolean(n); bool maybeHasFv = language::isLangSygus(options::inputLanguage()); - addFormula(n, true, false, false, maybeHasFv); + addFormula(n, false, false, maybeHasFv); } std::vector& Assertions::getAssumptions() { return d_assumptions; } @@ -134,13 +135,17 @@ preprocessing::AssertionPipeline& Assertions::getAssertionPipeline() return d_assertions; } -context::CDList* Assertions::getAssertionList() +const context::CDList& Assertions::getAssertionList() const { - return d_produceAssertions ? &d_assertionList : nullptr; + return d_assertionList; +} + +const context::CDList& Assertions::getAssertionListDefinitions() const +{ + return d_assertionListDefs; } void Assertions::addFormula(TNode n, - bool inInput, bool isAssumption, bool isFunDef, bool maybeHasFv) @@ -149,13 +154,17 @@ void Assertions::addFormula(TNode n, if (d_produceAssertions) { d_assertionList.push_back(n); + if (isFunDef) + { + d_assertionListDefs.push_back(n); + } } if (n.isConst() && n.getConst()) { // true, nothing to do return; } - Trace("smt") << "Assertions::addFormula(" << n << ", inInput = " << inInput + Trace("smt") << "Assertions::addFormula(" << n << ", isAssumption = " << isAssumption << ", isFunDef = " << isFunDef << std::endl; if (isFunDef) @@ -215,7 +224,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global) // definitions currently. Thus, we should check for free variables if the // input language is SyGuS. bool maybeHasFv = language::isLangSygus(options::inputLanguage()); - addFormula(n, true, false, true, maybeHasFv); + addFormula(n, false, true, maybeHasFv); } } diff --git a/src/smt/assertions.h b/src/smt/assertions.h index de7ba72c9..15131be60 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -23,11 +23,9 @@ #include "context/cdlist.h" #include "expr/node.h" #include "preprocessing/assertion_pipeline.h" +#include "smt/env_obj.h" namespace cvc5 { - -class Env; - namespace smt { class AbstractValues; @@ -39,7 +37,7 @@ class AbstractValues; * check-sat calls. It is *not* responsible for the preprocessing itself, and * instead is intended to be the input to a preprocessor utility. */ -class Assertions +class Assertions : protected EnvObj { /** The type of our internal assertion list */ typedef context::CDList AssertionList; @@ -94,9 +92,15 @@ class Assertions preprocessing::AssertionPipeline& getAssertionPipeline(); /** * Get assertions list corresponding to the original list of assertions, - * before preprocessing. + * before preprocessing. This includes assertions corresponding to define-fun + * and define-fun-rec. + */ + const context::CDList& getAssertionList() const; + /** + * Get assertions list corresponding to the original list of assertions + * that correspond to definitions (define-fun or define-fun-rec). */ - context::CDList* getAssertionList(); + const context::CDList& getAssertionListDefinitions() const; /** * Get the list of assumptions, which are those registered to this class * on initializeCheckSat. @@ -141,21 +145,19 @@ class Assertions * (this is used to distinguish assertions and assumptions) */ void addFormula(TNode n, - bool inInput, bool isAssumption, bool isFunDef, bool maybeHasFv); - /** Reference to the environment. */ - Env& d_env; /** 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(). Only maintained if in incremental mode. + * The assertion list (before any conversion) for supporting getAssertions(). */ AssertionList d_assertionList; + /** The subset of above the correspond to define-fun or define-fun-rec */ + AssertionList d_assertionListDefs; /** * List of lemmas generated for global (recursive) function definitions. We * assert this list of definitions in each check-sat call. diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index f928a2ce8..f148d1018 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -35,7 +35,7 @@ CheckModels::CheckModels(Env& e) : d_env(e) {} CheckModels::~CheckModels() {} void CheckModels::checkModel(TheoryModel* m, - context::CDList* al, + const context::CDList& al, bool hardFailure) { // Throughout, we use Notice() to give diagnostic output. @@ -57,7 +57,7 @@ void CheckModels::checkModel(TheoryModel* m, // the list of assertions that did not rewrite to true std::vector noCheckList; // Now go through all our user assertions checking if they're satisfied. - for (const Node& assertion : *al) + for (const Node& assertion : al) { Notice() << "SolverEngine::checkModel(): checking assertion " << assertion << std::endl; diff --git a/src/smt/check_models.h b/src/smt/check_models.h index fbfb1c2f5..d785b53d5 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -46,7 +46,7 @@ class CheckModels * given assertion list al based on the model checking policy. */ void checkModel(theory::TheoryModel* m, - context::CDList* al, + const context::CDList& al, bool hardFailure); private: diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index fd736860d..e66269f71 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -35,17 +35,15 @@ using namespace cvc5::kind; namespace cvc5 { namespace smt { -Preprocessor::Preprocessor(SolverEngine& slv, - Env& env, +Preprocessor::Preprocessor(Env& env, AbstractValues& abs, SmtEngineStatistics& stats) - : d_slv(slv), - d_env(env), + : EnvObj(env), d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(env.getUserContext(), false), d_exDefs(env, stats), - d_processor(slv, *env.getResourceManager(), stats), + d_processor(env, stats), d_pnm(nullptr) { } @@ -59,10 +57,10 @@ Preprocessor::~Preprocessor() } } -void Preprocessor::finishInit() +void Preprocessor::finishInit(SolverEngine* slv) { - d_ppContext.reset(new preprocessing::PreprocessingPassContext( - &d_slv, d_env, &d_propagator)); + d_ppContext.reset( + new preprocessing::PreprocessingPassContext(slv, d_env, &d_propagator)); // initialize the preprocessing passes d_processor.finishInit(d_ppContext.get()); @@ -149,8 +147,7 @@ Node Preprocessor::simplify(const Node& node) Trace("smt") << "SMT simplify(" << node << ")" << endl; if (Dump.isOn("benchmark")) { - d_slv.getOutputManager().getPrinter().toStreamCmdSimplify( - d_slv.getOutputManager().getDumpOut(), node); + d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node); } Node ret = expandDefinitions(node); ret = theory::Rewriter::rewrite(ret); @@ -162,7 +159,7 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) Assert(pppg != nullptr); d_pnm = pppg->getManager(); d_exDefs.setProofNodeManager(d_pnm); - d_propagator.setProof(d_pnm, d_env.getUserContext(), pppg); + d_propagator.setProof(d_pnm, userContext(), pppg); } } // namespace smt diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 2f5775ceb..35eb5d35a 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -20,12 +20,15 @@ #include +#include "smt/env_obj.h" #include "smt/expand_definitions.h" #include "smt/process_assertions.h" #include "theory/booleans/circuit_propagator.h" namespace cvc5 { -class Env; + +class SolverEngine; + namespace preprocessing { class PreprocessingPassContext; } @@ -43,18 +46,15 @@ class PreprocessProofGenerator; * (2) implementing methods for expanding and simplifying formulas. The latter * takes into account the substitutions inferred by this class. */ -class Preprocessor +class Preprocessor : protected EnvObj { public: - Preprocessor(SolverEngine& smt, - Env& env, - AbstractValues& abs, - SmtEngineStatistics& stats); + Preprocessor(Env& env, AbstractValues& abs, SmtEngineStatistics& stats); ~Preprocessor(); /** * Finish initialization */ - void finishInit(); + void finishInit(SolverEngine* slv); /** * Process the assertions that have been asserted in argument as. Returns * true if no conflict was discovered while preprocessing them. @@ -98,10 +98,6 @@ class Preprocessor void setProofGenerator(PreprocessProofGenerator* pppg); private: - /** Reference to the parent SolverEngine */ - SolverEngine& d_slv; - /** Reference to the env */ - Env& d_env; /** Reference to the abstract values utility */ AbstractValues& d_absValues; /** diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index c1f60530d..76059ac72 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -33,8 +33,8 @@ #include "smt/assertions.h" #include "smt/dump.h" #include "smt/expand_definitions.h" +#include "smt/print_benchmark.h" #include "smt/smt_engine_stats.h" -#include "smt/solver_engine.h" #include "theory/logic_info.h" #include "theory/theory_engine.h" @@ -57,13 +57,8 @@ class ScopeCounter unsigned& d_depth; }; -ProcessAssertions::ProcessAssertions(SolverEngine& slv, - ResourceManager& rm, - SmtEngineStatistics& stats) - : d_slv(slv), - d_resourceManager(rm), - d_smtStats(stats), - d_preprocessingPassContext(nullptr) +ProcessAssertions::ProcessAssertions(Env& env, SmtEngineStatistics& stats) + : EnvObj(env), d_smtStats(stats), d_preprocessingPassContext(nullptr) { d_true = NodeManager::currentNM()->mkConst(true); } @@ -93,7 +88,7 @@ void ProcessAssertions::cleanup() { d_passes.clear(); } void ProcessAssertions::spendResource(Resource r) { - d_resourceManager.spendResource(r); + resourceManager()->spendResource(r); } bool ProcessAssertions::apply(Assertions& as) @@ -101,7 +96,7 @@ bool ProcessAssertions::apply(Assertions& as) AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions - dumpAssertions("pre-everything", assertions); + dumpAssertions("pre-everything", as); Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl; Trace("smt") << "ProcessAssertions::processAssertions()" << endl; @@ -132,7 +127,7 @@ bool ProcessAssertions::apply(Assertions& as) Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; - dumpAssertions("pre-definition-expansion", assertions); + dumpAssertions("pre-definition-expansion", as); // Apply substitutions first. If we are non-incremental, this has only the // effect of replacing defined functions with their definitions. // We do not call theory-specific expand definitions here, since we want @@ -141,7 +136,7 @@ bool ProcessAssertions::apply(Assertions& as) Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; - dumpAssertions("post-definition-expansion", assertions); + dumpAssertions("post-definition-expansion", as); Debug("smt") << " assertions : " << assertions.size() << endl; @@ -229,7 +224,7 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["sep-skolem-emp"]->apply(&assertions); } - if (d_slv.getLogicInfo().isQuantified()) + if (logicInfo().isQuantified()) { // remove rewrite rules, apply pre-skolemization to existential quantifiers d_passes["quantifiers-preprocess"]->apply(&assertions); @@ -256,31 +251,28 @@ bool ProcessAssertions::apply(Assertions& as) } // rephrasing normal inputs as sygus problems - if (!d_slv.isInternalSubsolver()) + if (options().quantifiers.sygusInference) { - if (options::sygusInference()) - { - d_passes["sygus-infer"]->apply(&assertions); - } - else if (options::sygusRewSynthInput()) - { - // do candidate rewrite rule synthesis - d_passes["synth-rr"]->apply(&assertions); - } + d_passes["sygus-infer"]->apply(&assertions); + } + else if (options().quantifiers.sygusRewSynthInput) + { + // do candidate rewrite rule synthesis + d_passes["synth-rr"]->apply(&assertions); } Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify" << endl; - dumpAssertions("pre-simplify", assertions); + dumpAssertions("pre-simplify", as); Chat() << "simplifying assertions..." << endl; - noConflict = simplifyAssertions(assertions); + noConflict = simplifyAssertions(as); if (!noConflict) { ++(d_smtStats.d_simplifiedToFalse); } Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify" << endl; - dumpAssertions("post-simplify", assertions); + dumpAssertions("post-simplify", as); if (options::doStaticLearning()) { @@ -304,7 +296,7 @@ bool ProcessAssertions::apply(Assertions& as) d_smtStats.d_numAssertionsPost += assertions.size(); } - dumpAssertions("pre-repeat-simplify", assertions); + dumpAssertions("pre-repeat-simplify", as); if (options::repeatSimp()) { Trace("smt-proc") @@ -312,12 +304,12 @@ bool ProcessAssertions::apply(Assertions& as) << endl; Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); - noConflict &= simplifyAssertions(assertions); + noConflict &= simplifyAssertions(as); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-repeat-simplify" << endl; } - dumpAssertions("post-repeat-simplify", assertions); + dumpAssertions("post-repeat-simplify", as); if (options::ufHo()) { @@ -347,18 +339,19 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["bv-eager-atoms"]->apply(&assertions); } - Trace("smt-proc") << "ProcessAssertions::apply() end" << endl; - dumpAssertions("post-everything", assertions); + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() end" << endl; + dumpAssertions("post-everything", as); return noConflict; } // returns false if simplification led to "false" -bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) +bool ProcessAssertions::simplifyAssertions(Assertions& as) { spendResource(Resource::PreprocessStep); try { + AssertionPipeline& assertions = as.getAssertionPipeline(); ScopeCounter depth(d_simplifyAssertionsDepth); Trace("simplify") << "ProcessAssertions::simplify()" << endl; @@ -378,7 +371,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) if ( // check that option is on options::arithMLTrick() && // only useful in arith - d_slv.getLogicInfo().isTheoryEnabled(THEORY_ARITH) && + logicInfo().isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) @@ -426,7 +419,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) } } - dumpAssertions("post-repeatsimp", assertions); + dumpAssertions("post-repeatsimp", as); Trace("smt") << "POST repeatSimp" << endl; Debug("smt") << " assertions : " << assertions.size() << endl; } @@ -444,17 +437,16 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) return true; } -void ProcessAssertions::dumpAssertions(const char* key, - const AssertionPipeline& assertionList) +void ProcessAssertions::dumpAssertions(const char* key, Assertions& as) { if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key)) { + const AssertionPipeline& assertionList = as.getAssertionPipeline(); // Push the simplified assertions to the dump output stream for (unsigned i = 0; i < assertionList.size(); ++i) { TNode n = assertionList[i]; - d_slv.getOutputManager().getPrinter().toStreamCmdAssert( - d_slv.getOutputManager().getDumpOut(), n); + d_env.getPrinter().toStreamCmdAssert(d_env.getDumpOut(), n); } } } diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index d04663fe2..00b57813f 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -22,12 +22,11 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "smt/env_obj.h" #include "util/resource_manager.h" namespace cvc5 { -class SolverEngine; - namespace preprocessing { class AssertionPipeline; class PreprocessingPass; @@ -53,16 +52,14 @@ struct SmtEngineStatistics; * it processes assertions in a way that assumes that apply(...) could be * applied multiple times to different sets of assertions. */ -class ProcessAssertions +class ProcessAssertions : protected EnvObj { /** The types for the recursive function definitions */ typedef context::CDList NodeList; typedef std::unordered_map NodeToBoolHashMap; public: - ProcessAssertions(SolverEngine& smt, - ResourceManager& rm, - SmtEngineStatistics& stats); + ProcessAssertions(Env& env, SmtEngineStatistics& stats); ~ProcessAssertions(); /** Finish initialize * @@ -77,14 +74,12 @@ class ProcessAssertions /** * Process the formulas in as. Returns true if there was no conflict when * processing the assertions. + * + * @param as The assertions. */ bool apply(Assertions& as); private: - /** Reference to the SMT engine */ - SolverEngine& d_slv; - /** Reference to resource manager */ - ResourceManager& d_resourceManager; /** Reference to the SMT stats */ SmtEngineStatistics& d_smtStats; /** The preprocess context */ @@ -111,13 +106,12 @@ class ProcessAssertions * * Returns false if the formula simplifies to "false" */ - bool simplifyAssertions(preprocessing::AssertionPipeline& assertions); + bool simplifyAssertions(Assertions& as); /** * Dump assertions. Print the current assertion list to the dump * assertions:`key` if it is enabled. */ - void dumpAssertions(const char* key, - const preprocessing::AssertionPipeline& assertionList); + void dumpAssertions(const char* key, Assertions& as); }; } // namespace smt diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 6aaa6e267..4759008dc 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -279,12 +279,12 @@ std::shared_ptr PfManager::getFinalProof( void PfManager::getAssertions(Assertions& as, std::vector& assertions) { - context::CDList* al = as.getAssertionList(); - Assert(al != nullptr); - for (context::CDList::const_iterator i = al->begin(); i != al->end(); - ++i) + 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(*i); + assertions.push_back(a); } } diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 40c940b5a..31ccaacac 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -175,6 +175,13 @@ void SetDefaults::setDefaultsPre(Options& opts) opts.smt.checkProofs = false; } } + if (d_isInternalSubsolver) + { + // these options must be disabled on internal subsolvers, as they are + // used by the user to rephrase the input. + opts.quantifiers.sygusInference = false; + opts.quantifiers.sygusRewSynthInput = false; + } } void SetDefaults::finalizeLogic(LogicInfo& logic, Options& opts) const diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 8064086ad..cf2ecf387 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -48,7 +48,7 @@ SmtSolver::SmtSolver(Env& env, SmtSolver::~SmtSolver() {} -void SmtSolver::finishInit(const LogicInfo& logicInfo) +void SmtSolver::finishInit() { // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index d4e844b6c..9baaea302 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -70,11 +70,9 @@ class SmtSolver SmtEngineStatistics& stats); ~SmtSolver(); /** - * Create theory engine, prop engine based on the logic info. - * - * @param logicInfo the logic information + * Create theory engine, prop engine based on the environment. */ - void finishInit(const LogicInfo& logicInfo); + void finishInit(); /** Reset all assertions, global declarations, etc. */ void resetAssertions(); /** diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 094cc8e26..b458c421f 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -124,10 +124,9 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) // make statistics d_stats.reset(new SmtEngineStatistics()); // reset the preprocessor - d_pp.reset( - new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); + d_pp.reset(new smt::Preprocessor(*d_env, *d_absValues, *d_stats)); // make the SMT solver - d_smtSolver.reset(new SmtSolver(*d_env.get(), *d_state, *d_pp, *d_stats)); + d_smtSolver.reset(new SmtSolver(*d_env, *d_state, *d_pp, *d_stats)); // make the SyGuS solver d_sygusSolver.reset(new SygusSolver(*d_env.get(), *d_smtSolver, *d_pp)); // make the quantifier elimination solver @@ -209,7 +208,7 @@ void SolverEngine::finishInit() } Trace("smt-debug") << "SolverEngine::finishInit" << std::endl; - d_smtSolver->finishInit(logic); + d_smtSolver->finishInit(); // now can construct the SMT-level model object TheoryEngine* te = d_smtSolver->getTheoryEngine(); @@ -255,10 +254,10 @@ void SolverEngine::finishInit() if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { - d_interpolSolver.reset(new InterpolationSolver(*d_env.get())); + d_interpolSolver.reset(new InterpolationSolver(*d_env)); } - d_pp->finishInit(); + d_pp->finishInit(this); AlwaysAssert(getPropEngine()->getAssertionLevel() == 0) << "The PropEngine has pushed but the SolverEngine " @@ -1284,10 +1283,9 @@ std::pair SolverEngine::getSepHeapAndNilExpr(void) std::vector SolverEngine::getAssertionsInternal() { Assert(d_state->isFullyInited()); - context::CDList* al = d_asserts->getAssertionList(); - Assert(al != nullptr); + const context::CDList& al = d_asserts->getAssertionList(); std::vector res; - for (const Node& n : *al) + for (const Node& n : al) { res.emplace_back(n); } @@ -1515,10 +1513,10 @@ void SolverEngine::checkUnsatCore() void SolverEngine::checkModel(bool hardFailure) { - context::CDList* al = d_asserts->getAssertionList(); + const context::CDList& al = d_asserts->getAssertionList(); // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. - Assert(al != nullptr) + Assert(d_env->getOptions().smt.produceAssertions) << "don't have an assertion list to check in SolverEngine::checkModel()"; TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 69ea51dd1..ce98b820d 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -42,10 +42,10 @@ namespace cvc5 { namespace smt { SygusSolver::SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp) - : d_env(env), + : EnvObj(env), d_smtSolver(sms), d_pp(pp), - d_sygusConjectureStale(env.getUserContext(), true) + d_sygusConjectureStale(userContext(), true) { } @@ -301,17 +301,15 @@ void SygusSolver::checkSynthSolution(Assertions& as) Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions - context::CDList* alist = as.getAssertionList(); - if (alist == nullptr) - { - Trace("check-synth-sol") << "No assertions to check\n"; - return; - } + const context::CDList& alist = as.getAssertionList(); + Assert(options().smt.produceAssertions) + << "Expected produce assertions to be true when checking synthesis " + "solution"; // auxiliary assertions std::vector auxAssertions; // expand definitions cache std::unordered_map cache; - for (Node assertion : *alist) + for (const Node& assertion : alist) { Notice() << "SygusSolver::checkSynthSolution(): checking assertion " << assertion << std::endl; diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 90a6a87f0..aa0355fb8 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/type_node.h" #include "smt/assertions.h" +#include "smt/env_obj.h" #include "util/result.h" namespace cvc5 { @@ -42,7 +43,7 @@ class SmtSolver; * It also maintains a reference to a preprocessor for implementing * checkSynthSolution. */ -class SygusSolver +class SygusSolver : protected EnvObj { public: SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp); @@ -170,8 +171,6 @@ class SygusSolver * expansion. */ void expandDefinitionsSygusDt(TypeNode tn) const; - /** Reference to the env class */ - Env& d_env; /** The SMT solver, which is used during checkSynth. */ SmtSolver& d_smtSolver; /** The preprocessor, used for checkSynthSolution. */ diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index 27922acf9..4d47b57ea 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -32,16 +32,14 @@ void UnsatCoreManager::getUnsatCore(std::shared_ptr pfn, expr::getFreeAssumptions(pfn->getChildren()[0].get(), fassumps); Trace("unsat-core") << "UCManager::getUnsatCore: free assumptions: " << fassumps << "\n"; - context::CDList* al = as.getAssertionList(); - Assert(al != nullptr); - for (context::CDList::const_iterator i = al->begin(); i != al->end(); - ++i) + const context::CDList& al = as.getAssertionList(); + for (const Node& a : al) { - Trace("unsat-core") << "is assertion " << *i << " there?\n"; - if (std::find(fassumps.begin(), fassumps.end(), *i) != fassumps.end()) + Trace("unsat-core") << "is assertion " << a << " there?\n"; + if (std::find(fassumps.begin(), fassumps.end(), a) != fassumps.end()) { Trace("unsat-core") << "\tyes\n"; - core.push_back(*i); + core.push_back(a); } } if (Trace.isOn("unsat-core")) -- 2.30.2