From: Andrew Reynolds Date: Wed, 18 Nov 2020 16:20:18 +0000 (-0600) Subject: Minor cleanup of SmtEngine (#5450) X-Git-Tag: cvc5-1.0.0~2586 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a8ec602967719f48a0bd76b84976a9504ae209b;p=cvc5.git Minor cleanup of SmtEngine (#5450) --- diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 9b4d02032..a4e7ac703 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -34,8 +34,7 @@ UnconstrainedSimplifier::UnconstrainedSimplifier( : PreprocessingPass(preprocContext, "unconstrained-simplifier"), d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), d_context(preprocContext->getDecisionContext()), - d_substitutions(preprocContext->getDecisionContext()), - d_logicInfo(preprocContext->getLogicInfo()) + d_substitutions(preprocContext->getDecisionContext()) { smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); } @@ -588,7 +587,7 @@ void UnconstrainedSimplifier::processUnconstrained() // Uninterpreted function - if domain is infinite, no quantifiers are // used, and any child is unconstrained, result is unconstrained case kind::APPLY_UF: - if (d_logicInfo.isQuantified() + if (d_preprocContext->getLogicInfo().isQuantified() || !current.getType().getCardinality().isInfinite()) { break; diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index 8c7457b92..ebfe51e79 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -61,7 +61,6 @@ class UnconstrainedSimplifier : public PreprocessingPass context::Context* d_context; theory::SubstitutionMap d_substitutions; - const LogicInfo& d_logicInfo; /** * Visit all subterms in assertion. This method throws a LogicException if * there is a subterm that is unhandled by this preprocessing pass (e.g. a diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index d0747b5d9..824197bc5 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -66,7 +66,8 @@ class PreprocessingPassContext d_resourceManager->spendResource(r); } - const LogicInfo& getLogicInfo() { return d_smt->d_logic; } + /** Get the current logic info of the SmtEngine */ + const LogicInfo& getLogicInfo() { return d_smt->getLogicInfo(); } /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 912c0ea28..98a2a7a36 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -29,13 +29,14 @@ namespace smt { Preprocessor::Preprocessor(SmtEngine& smt, context::UserContext* u, - AbstractValues& abs) + AbstractValues& abs, + SmtEngineStatistics& stats) : d_context(u), d_smt(smt), d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(u, false), - d_processor(smt, *smt.getResourceManager()), + d_processor(smt, *smt.getResourceManager(), stats), d_rtf(u), d_pnm(nullptr) { diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index b07e7ec97..cb83f969e 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -41,7 +41,10 @@ class AbstractValues; class Preprocessor { public: - Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs); + Preprocessor(SmtEngine& smt, + context::UserContext* u, + AbstractValues& abs, + SmtEngineStatistics& stats); ~Preprocessor(); /** * Finish initialization diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 387085de8..2011e7b83 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -52,8 +52,13 @@ class ScopeCounter unsigned& d_depth; }; -ProcessAssertions::ProcessAssertions(SmtEngine& smt, ResourceManager& rm) - : d_smt(smt), d_resourceManager(rm), d_preprocessingPassContext(nullptr) +ProcessAssertions::ProcessAssertions(SmtEngine& smt, + ResourceManager& rm, + SmtEngineStatistics& stats) + : d_smt(smt), + d_resourceManager(rm), + d_smtStats(stats), + d_preprocessingPassContext(nullptr) { d_true = NodeManager::currentNM()->mkConst(true); } @@ -127,7 +132,7 @@ bool ProcessAssertions::apply(Assertions& as) Chat() << "expanding definitions..." << endl; Trace("simplify") << "ProcessAssertions::simplify(): expanding definitions" << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime); + TimerStat::CodeTimer codeTimer(d_smtStats.d_definitionExpansionTime); unordered_map cache; for (size_t i = 0, nasserts = assertions.size(); i < nasserts; ++i) { @@ -232,7 +237,7 @@ bool ProcessAssertions::apply(Assertions& as) d_passes["sep-skolem-emp"]->apply(&assertions); } - if (d_smt.d_logic.isQuantified()) + if (d_smt.getLogicInfo().isQuantified()) { // remove rewrite rules, apply pre-skolemization to existential quantifiers d_passes["quantifiers-preprocess"]->apply(&assertions); @@ -261,7 +266,7 @@ bool ProcessAssertions::apply(Assertions& as) } // rephrasing normal inputs as sygus problems - if (!d_smt.d_isInternalSubsolver) + if (!d_smt.isInternalSubsolver()) { if (options::sygusInference()) { @@ -281,7 +286,7 @@ bool ProcessAssertions::apply(Assertions& as) noConflict = simplifyAssertions(assertions); if (!noConflict) { - ++(d_smt.d_stats->d_simplifiedToFalse); + ++(d_smtStats.d_simplifiedToFalse); } Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify" << endl; @@ -294,13 +299,13 @@ bool ProcessAssertions::apply(Assertions& as) Debug("smt") << " assertions : " << assertions.size() << endl; { - d_smt.d_stats->d_numAssertionsPre += assertions.size(); + d_smtStats.d_numAssertionsPre += assertions.size(); d_passes["ite-removal"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. d_passes["apply-substs"]->apply(&assertions); - d_smt.d_stats->d_numAssertionsPost += assertions.size(); + d_smtStats.d_numAssertionsPost += assertions.size(); } dumpAssertions("pre-repeat-simplify", assertions); @@ -456,7 +461,7 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) if ( // check that option is on options::arithMLTrick() && // only useful in arith - d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && + d_smt.getLogicInfo().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) @@ -550,7 +555,7 @@ Node ProcessAssertions::expandDefinitions( unordered_map& cache, bool expandOnly) { - NodeManager* nm = d_smt.d_nodeManager; + NodeManager* nm = d_smt.getNodeManager(); std::stack> worklist; std::stack result; worklist.push(std::make_tuple(Node(n), Node(n), false)); @@ -577,9 +582,9 @@ Node ProcessAssertions::expandDefinitions( // we can short circuit (variable) leaves if (n.isVar()) { - SmtEngine::DefinedFunctionMap::const_iterator i = - d_smt.d_definedFunctions->find(n); - if (i != d_smt.d_definedFunctions->end()) + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(n); + if (i != dfuns->end()) { Node f = (*i).second.getFormula(); // must expand its definition @@ -651,9 +656,9 @@ Node ProcessAssertions::expandDefinitions( { // application of a user-defined symbol TNode func = n.getOperator(); - SmtEngine::DefinedFunctionMap::const_iterator i = - d_smt.d_definedFunctions->find(func); - if (i == d_smt.d_definedFunctions->end()) + SmtEngine::DefinedFunctionMap* dfuns = d_smt.getDefinedFunctionMap(); + SmtEngine::DefinedFunctionMap::const_iterator i = dfuns->find(func); + if (i == dfuns->end()) { throw TypeCheckingException( n.toExpr(), diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index a4f16ab1d..d260edf14 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -57,7 +57,9 @@ class ProcessAssertions typedef unordered_map NodeToBoolHashMap; public: - ProcessAssertions(SmtEngine& smt, ResourceManager& rm); + ProcessAssertions(SmtEngine& smt, + ResourceManager& rm, + SmtEngineStatistics& stats); ~ProcessAssertions(); /** Finish initialize * @@ -92,6 +94,8 @@ class ProcessAssertions SmtEngine& d_smt; /** Reference to resource manager */ ResourceManager& d_resourceManager; + /** Reference to the SMT stats */ + SmtEngineStatistics& d_smtStats; /** The preprocess context */ preprocessing::PreprocessingPassContext* d_preprocessingPassContext; /** True node */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9826cd097..8aad05235 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -18,21 +18,15 @@ #include "api/cvc4cpp.h" #include "base/check.h" -#include "base/configuration.h" -#include "base/configuration_private.h" #include "base/exception.h" #include "base/modal_exception.h" #include "base/output.h" #include "decision/decision_engine.h" #include "expr/node.h" -#include "expr/node_self_iterator.h" -#include "expr/node_visitor.h" #include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" -#include "options/option_exception.h" #include "options/printer_options.h" -#include "options/set_language.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "printer/printer.h" @@ -60,19 +54,18 @@ #include "smt/smt_engine_stats.h" #include "smt/smt_solver.h" #include "smt/sygus_solver.h" -#include "smt/term_formula_removal.h" -#include "smt/update_ostream.h" -#include "theory/logic_info.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" #include "theory/theory_engine.h" -#include "util/hash.h" #include "util/random.h" #include "util/resource_manager.h" +// required for hacks related to old proofs for unsat cores +#include "base/configuration.h" +#include "base/configuration_private.h" + using namespace std; -using namespace CVC4; using namespace CVC4::smt; using namespace CVC4::preprocessing; using namespace CVC4::prop; @@ -136,14 +129,15 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_resourceManager.reset( new ResourceManager(*d_statisticsRegistry.get(), d_options)); d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); - d_pp.reset( - new smt::Preprocessor(*this, getUserContext(), *d_absValues.get())); // listen to node manager events d_nodeManager->subscribeEvents(d_snmListener.get()); // listen to resource out d_resourceManager->registerListener(d_routListener.get()); // make statistics d_stats.reset(new SmtEngineStatistics()); + // reset the preprocessor + d_pp.reset(new smt::Preprocessor( + *this, getUserContext(), *d_absValues.get(), *d_stats)); // make the SMT solver d_smtSolver.reset( new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); @@ -397,9 +391,8 @@ void SmtEngine::setLogic(const std::string& s) } void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } -LogicInfo SmtEngine::getLogicInfo() const { - return d_logic; -} + +const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; } LogicInfo SmtEngine::getUserLogicInfo() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7a55d3b74..d8d2ea171 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -50,19 +50,13 @@ typedef NodeTemplate Node; typedef NodeTemplate TNode; struct NodeHashFunction; -class Command; -class GetModelCommand; - class SmtEngine; class DecisionEngine; class TheoryEngine; - class ProofManager; class UnsatCore; - class LogicRequest; class StatisticsRegistry; - class Printer; /* -------------------------------------------------------------------------- */ @@ -134,32 +128,15 @@ namespace theory { class Rewriter; }/* CVC4::theory namespace */ -// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the -// hood): use a type parameter and have check() delegate, or subclass -// SmtEngine and override check()? -// -// Probably better than that is to have a configuration object that -// indicates which passes are desired. The configuration occurs -// elsewhere (and can even occur at runtime). A simple "pass manager" -// of sorts determines check()'s behavior. -// -// The CNF conversion can go on in PropEngine. /* -------------------------------------------------------------------------- */ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::api::Solver; - // TODO (Issue #1096): Remove this friend relationship. - friend class ::CVC4::preprocessing::PreprocessingPassContext; friend class ::CVC4::smt::SmtEngineState; friend class ::CVC4::smt::SmtScope; - friend class ::CVC4::smt::ProcessAssertions; - friend class ::CVC4::smt::SmtSolver; - friend ProofManager* ::CVC4::smt::currentProofManager(); friend class ::CVC4::LogicRequest; - friend class ::CVC4::theory::TheoryModel; - friend class ::CVC4::theory::Rewriter; /* ....................................................................... */ public: @@ -237,7 +214,7 @@ class CVC4_PUBLIC SmtEngine void setLogic(const LogicInfo& logic); /** Get the logic information currently set. */ - LogicInfo getLogicInfo() const; + const LogicInfo& getLogicInfo() const; /** Get the logic information set by the user. */ LogicInfo getUserLogicInfo() const; @@ -865,6 +842,24 @@ class CVC4_PUBLIC SmtEngine Options& getOptions(); const Options& getOptions() const; + /** Get a pointer to the UserContext owned by this SmtEngine. */ + context::UserContext* getUserContext(); + + /** Get a pointer to the Context owned by this SmtEngine. */ + context::Context* getContext(); + + /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ + TheoryEngine* getTheoryEngine(); + + /** Get a pointer to the PropEngine owned by this SmtEngine. */ + prop::PropEngine* getPropEngine(); + + /** + * Get a pointer to the ProofManager owned by this SmtEngine. + * TODO (project #37): this is the old proof manager and will be deleted + */ + ProofManager* getProofManager() { return d_proofManager.get(); }; + /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager(); @@ -880,6 +875,12 @@ class CVC4_PUBLIC SmtEngine /** Get a pointer to the Rewriter owned by this SmtEngine. */ theory::Rewriter* getRewriter() { return d_rewriter.get(); } + /** The type of our internal map of defined functions */ + using DefinedFunctionMap = + context::CDHashMap; + + /** Get the defined function map */ + DefinedFunctionMap* getDefinedFunctionMap() { return d_definedFunctions; } /** * Get expanded assertions. * @@ -889,10 +890,6 @@ class CVC4_PUBLIC SmtEngine /* ....................................................................... */ private: /* ....................................................................... */ - - /** The type of our internal map of defined functions */ - typedef context::CDHashMap - DefinedFunctionMap; /** The type of our internal assertion list */ typedef context::CDList AssertionList; @@ -903,24 +900,6 @@ class CVC4_PUBLIC SmtEngine /** Set solver instance that owns this SmtEngine. */ void setSolver(api::Solver* solver) { d_solver = solver; } - /** Get a pointer to the UserContext owned by this SmtEngine. */ - context::UserContext* getUserContext(); - - /** Get a pointer to the Context owned by this SmtEngine. */ - context::Context* getContext(); - - /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ - TheoryEngine* getTheoryEngine(); - - /** Get a pointer to the PropEngine owned by this SmtEngine. */ - prop::PropEngine* getPropEngine(); - - /** - * Get a pointer to the ProofManager owned by this SmtEngine. - * TODO (project #37): this is the old proof manager and will be deleted - */ - ProofManager* getProofManager() { return d_proofManager.get(); }; - /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ StatisticsRegistry* getStatisticsRegistry() { @@ -1021,15 +1000,6 @@ class CVC4_PUBLIC SmtEngine */ void setLogicInternal(); - /** - * Add to Model command. This is used for recording a command - * that should be reported during a get-model call. - */ - void addToModelCommandAndDump(const Command& c, - uint32_t flags = 0, - bool userVisible = true, - const char* dumpTag = "declarations"); - /* * Check satisfiability (used to check satisfiability and entailment). */ @@ -1153,8 +1123,10 @@ class CVC4_PUBLIC SmtEngine */ std::map d_commandVerbosity; + /** The statistics registry */ std::unique_ptr d_statisticsRegistry; + /** The statistics class */ std::unique_ptr d_stats; /** The options object */