From: Andrew Reynolds Date: Thu, 26 Nov 2020 05:03:11 +0000 (-0600) Subject: Fully decouple SmtEngine and the Expr layer (#5532) X-Git-Tag: cvc5-1.0.0~2548 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c41a2e9be2422a211b9687833c97ba37485cd946;p=cvc5.git Fully decouple SmtEngine and the Expr layer (#5532) This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 9b79b5c45..5eabcfe62 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3093,7 +3093,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { d_exprMgr.reset(new ExprManager); - d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts)); + d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts)); d_smtEngine->setSolver(this); Options& o = d_smtEngine->getOptions(); d_rng.reset(new Random(o[options::seed])); diff --git a/src/expr/type.h b/src/expr/type.h index 69a8363dc..0b923f027 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -33,7 +33,7 @@ class Expr; class TypeNode; struct CVC4_PUBLIC ExprManagerMapCollection; -class CVC4_PUBLIC SmtEngine; +class SmtEngine; class CVC4_PUBLIC Datatype; class Record; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 154166eb7..fa3eb66c0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1442,8 +1442,8 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm) { solver->getSmtEngine()->setUserAttribute( d_attr, - d_term.getExpr(), - api::termVectorToExprs(d_termValues), + d_term.getNode(), + api::termVectorToNodes(d_termValues), d_strValue); } d_commandStatus = CommandSuccess::instance(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d623fdef..161c2eba6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -73,10 +73,9 @@ using namespace CVC4::theory; namespace CVC4 { -SmtEngine::SmtEngine(ExprManager* em, Options* optr) +SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_state(new SmtEngineState(*this)), - d_exprManager(em), - d_nodeManager(d_exprManager->getNodeManager()), + d_nodeManager(nm), d_absValues(new AbstractValues(d_nodeManager)), d_asserts(new Assertions(getUserContext(), *d_absValues.get())), d_dumpm(new DumpManager(getUserContext())), @@ -525,14 +524,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "all-statistics") { vector stats; - for (StatisticsRegistry::const_iterator i = - NodeManager::fromExprManager(d_exprManager) - ->getStatisticsRegistry() - ->begin(); - i - != NodeManager::fromExprManager(d_exprManager) - ->getStatisticsRegistry() - ->end(); + StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry(); + for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end(); ++i) { vector v; @@ -1637,7 +1630,6 @@ void SmtEngine::pop() { void SmtEngine::reset() { SmtScope smts(this); - ExprManager *em = d_exprManager; Trace("smt") << "SMT reset()" << endl; if(Dump.isOn("benchmark")) { getOutputManager().getPrinter().toStreamCmdReset( @@ -1647,7 +1639,7 @@ void SmtEngine::reset() Options opts; opts.copyValues(d_originalOptions); this->~SmtEngine(); - new (this) SmtEngine(em, &opts); + new (this) SmtEngine(d_nodeManager, &opts); // Restore data set after creation notifyStartParsing(filename); } @@ -1713,10 +1705,7 @@ unsigned long SmtEngine::getResourceRemaining() const return d_resourceManager->getResourceRemaining(); } -NodeManager* SmtEngine::getNodeManager() const -{ - return d_exprManager->getNodeManager(); -} +NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; } Statistics SmtEngine::getStatistics() const { @@ -1733,20 +1722,15 @@ void SmtEngine::safeFlushStatistics(int fd) const { } void SmtEngine::setUserAttribute(const std::string& attr, - Expr expr, - const std::vector& expr_values, + Node expr, + const std::vector& expr_values, const std::string& str_value) { SmtScope smts(this); finishInit(); - std::vector node_values; - for (std::size_t i = 0, n = expr_values.size(); i < n; i++) - { - node_values.push_back( expr_values[i].getNode() ); - } TheoryEngine* te = getTheoryEngine(); Assert(te != nullptr); - te->setUserAttribute(attr, expr.getNode(), node_values, str_value); + te->setUserAttribute(attr, expr, expr_values, str_value); } void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1c83fa61f..a55428b55 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -21,13 +21,12 @@ #include #include +#include #include "base/modal_exception.h" #include "context/cdhashmap_forward.h" #include "context/cdhashset_forward.h" #include "context/cdlist_forward.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" #include "options/options.h" #include "smt/logic_exception.h" #include "smt/output_manager.h" @@ -48,9 +47,10 @@ namespace CVC4 { template class NodeTemplate; typedef NodeTemplate Node; typedef NodeTemplate TNode; +class TypeNode; struct NodeHashFunction; -class SmtEngine; +class NodeManager; class DecisionEngine; class TheoryEngine; class ProofManager; @@ -58,6 +58,7 @@ class UnsatCore; class LogicRequest; class StatisticsRegistry; class Printer; +class ResourceManager; /* -------------------------------------------------------------------------- */ @@ -147,7 +148,7 @@ class CVC4_PUBLIC SmtEngine * If provided, optr is a pointer to a set of options that should initialize the values * of the options object owned by this class. */ - SmtEngine(ExprManager* em, Options* optr = nullptr); + SmtEngine(NodeManager* nm, Options* optr = nullptr); /** Destruct the SMT engine. */ ~SmtEngine(); @@ -691,7 +692,7 @@ class CVC4_PUBLIC SmtEngine /** * Completely reset the state of the solver, as though destroyed and * recreated. The result is as if newly constructed (so it still - * retains the same options structure and ExprManager). + * retains the same options structure and NodeManager). */ void reset(); @@ -785,9 +786,6 @@ class CVC4_PUBLIC SmtEngine */ unsigned long getResourceRemaining() const; - /** Permit access to the underlying ExprManager. */ - ExprManager* getExprManager() const { return d_exprManager; } - /** Permit access to the underlying NodeManager. */ NodeManager* getNodeManager() const; @@ -806,8 +804,8 @@ class CVC4_PUBLIC SmtEngine * In SMT-LIBv2 this is done via the syntax (! expr :attr) */ void setUserAttribute(const std::string& attr, - Expr expr, - const std::vector& expr_values, + Node expr, + const std::vector& expr_values, const std::string& str_value); /** Get the options object (const and non-const versions) */ @@ -1013,9 +1011,7 @@ class CVC4_PUBLIC SmtEngine */ std::unique_ptr d_state; - /** Our expression manager */ - ExprManager* d_exprManager; - /** Our internal expression/node manager */ + /** Our internal node manager */ NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index ed10e85ae..ee1ae198f 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -48,7 +48,7 @@ void initializeSubsolver(std::unique_ptr& smte, NodeManager* nm = NodeManager::currentNM(); SmtEngine* smtCurr = smt::currentSmtEngine(); // must copy the options - smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions())); + smte.reset(new SmtEngine(nm, &smtCurr->getOptions())); smte->setIsInternalSubsolver(); smte->setLogic(smtCurr->getLogicInfo()); // set the options diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index f1b782be2..de1795264 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -66,7 +66,7 @@ class AttributeWhite : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smtEngine = new SmtEngine(d_em); + d_smtEngine = new SmtEngine(d_nm); d_scope = new SmtScope(d_smtEngine); d_booleanType = new TypeNode(d_nm->booleanType()); } diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index 22d3f0d84..8ac17bbbd 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -42,7 +42,7 @@ class TypeNodeWhite : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = d_em->getNodeManager(); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new NodeManagerScope(d_nm); } diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index 0ff00a7d5..a0a708c5b 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -174,7 +174,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index ae79e1517..495097a79 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -131,9 +131,9 @@ class CnfStreamWhite : public CxxTest::TestSuite { void setUp() override { d_exprManager = new ExprManager(); - d_smt = new SmtEngine(d_exprManager); - d_smt->d_logic.lock(); d_nodeManager = NodeManager::fromExprManager(d_exprManager); + d_smt = new SmtEngine(d_nodeManager); + d_smt->d_logic.lock(); d_scope = new SmtScope(d_smt); // Notice that this unit test uses the theory engine of a created SMT diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 421987e3c..1f33d0fbf 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -50,7 +50,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em, &opts); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index 1215b4a31..09cb925a3 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -47,12 +47,11 @@ class SequencesRewriterWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); d_rewriter = new ExtendedRewriter(true); - - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index f0b3f18fe..3475b1dc8 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -101,7 +101,7 @@ public: { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_smt->setOption("incremental", CVC4::SExpr(false)); d_ctxt = d_smt->getContext(); d_uctxt = d_smt->getUserContext(); diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h index 4e19ba90e..72fc4284e 100644 --- a/test/unit/theory/theory_bags_normal_form_white.h +++ b/test/unit/theory/theory_bags_normal_form_white.h @@ -35,8 +35,8 @@ class BagsNormalFormWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); d_rewriter.reset(new BagsRewriter(nullptr)); } diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h index e47e32784..a58e2cdad 100644 --- a/test/unit/theory/theory_bags_rewriter_white.h +++ b/test/unit/theory/theory_bags_rewriter_white.h @@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); d_rewriter.reset(new BagsRewriter(nullptr)); } diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h index e454dfa28..8d1db858d 100644 --- a/test/unit/theory/theory_bags_type_rules_white.h +++ b/test/unit/theory/theory_bags_type_rules_white.h @@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index fae90918a..738a51831 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -41,11 +41,10 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); d_smt->finishInit(); - - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bfde7866e..f568dc779 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -54,7 +54,7 @@ public: { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); } diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 8a99946e5..97da7eb8b 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -192,8 +192,8 @@ public: void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_ctxt = d_smt->getContext(); diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index f2c5f0e1d..e19459f15 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -63,7 +63,7 @@ void BvInstantiatorWhite::setUp() { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h index bb44656bc..ac25f60a9 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h @@ -222,7 +222,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_smt->setOption("cegqi-full", CVC4::SExpr(true)); d_smt->setOption("produce-models", CVC4::SExpr(true)); d_scope = new SmtScope(d_smt); diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index 965e59267..1b5ba1dcb 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -36,8 +36,8 @@ class SetEnumeratorWhite : public CxxTest::TestSuite void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h index 66c8dc123..00b012745 100644 --- a/test/unit/theory/theory_sets_type_rules_white.h +++ b/test/unit/theory/theory_sets_type_rules_white.h @@ -28,8 +28,8 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite { d_slv.reset(new Solver()); d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); d_nm.reset(NodeManager::fromExprManager(d_em.get())); + d_smt.reset(new SmtEngine(d_nm.get())); d_smt->finishInit(); } diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h index 4135adb0c..dd70dd5b9 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.h +++ b/test/unit/theory/theory_strings_skolem_cache_black.h @@ -35,13 +35,13 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite void setUp() override { d_em.reset(new ExprManager()); - d_smt.reset(new SmtEngine(d_em.get())); + d_nm = NodeManager::fromExprManager(d_em.get()); + d_smt.reset(new SmtEngine(d_nm)); d_scope.reset(new SmtScope(d_smt.get())); // Ensure that the SMT engine is fully initialized (required for the // rewriter) d_smt->push(); - d_nm = NodeManager::fromExprManager(d_em.get()); } void tearDown() override {} diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index 69143a69c..ce432d385 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -38,10 +38,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); d_em = new ExprManager; - d_smt = new SmtEngine(d_em, &opts); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm, &opts); d_scope = new SmtScope(d_smt); - d_nm = NodeManager::currentNM(); } void tearDown() override diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 552aeb3c6..f69830fd8 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -175,7 +175,7 @@ class TheoryBlack : public CxxTest::TestSuite { { d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_nm); d_ctxt = d_smt->getContext(); d_uctxt = d_smt->getUserContext(); d_scope = new SmtScope(d_smt); diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index ea5a38913..24bf9922e 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -42,8 +42,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { void setUp() override { d_em = new ExprManager(); - d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_nm); d_scope = new SmtScope(d_smt); d_smt->finishInit(); }