From: Andrew Reynolds Date: Thu, 23 Sep 2021 18:54:03 +0000 (-0500) Subject: More uses of EnvObj (#7230) X-Git-Tag: cvc5-1.0.0~1174 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d0ec8ff649c7649c9f33e4290c6d7b426121d854;p=cvc5.git More uses of EnvObj (#7230) --- diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp index 9e9eb5f23..9a9c56972 100644 --- a/src/smt/model_core_builder.cpp +++ b/src/smt/model_core_builder.cpp @@ -21,6 +21,8 @@ using namespace cvc5::kind; namespace cvc5 { +ModelCoreBuilder::ModelCoreBuilder(Env& env) : EnvObj(env) {} + bool ModelCoreBuilder::setModelCore(const std::vector& assertions, theory::TheoryModel* m, options::ModelCoresMode mode) @@ -78,15 +80,14 @@ bool ModelCoreBuilder::setModelCore(const std::vector& assertions, std::vector coreVars; std::vector impliedVars; bool minimized = false; + theory::SubstitutionMinimize sm(d_env); if (mode == options::ModelCoresMode::NON_IMPLIED) { - minimized = theory::SubstitutionMinimize::findWithImplied( - formula, vars, subs, coreVars, impliedVars); + minimized = sm.findWithImplied(formula, vars, subs, coreVars, impliedVars); } else if (mode == options::ModelCoresMode::SIMPLE) { - minimized = theory::SubstitutionMinimize::find( - formula, truen, vars, subs, coreVars); + minimized = sm.find(formula, truen, vars, subs, coreVars); } else { diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h index aab4fab5e..8a0ca5c8a 100644 --- a/src/smt/model_core_builder.h +++ b/src/smt/model_core_builder.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" +#include "smt/env_obj.h" #include "theory/theory_model.h" namespace cvc5 { @@ -29,9 +30,10 @@ namespace cvc5 { /** * A utility for building model cores. */ -class ModelCoreBuilder +class ModelCoreBuilder : protected EnvObj { public: + ModelCoreBuilder(Env& env); /** set model core * * This function updates model m so that it has information regarding its @@ -55,9 +57,9 @@ class ModelCoreBuilder * If m is not a model for assertions, this method returns false and m is * left unchanged. */ - static bool setModelCore(const std::vector& assertions, - theory::TheoryModel* m, - options::ModelCoresMode mode); + bool setModelCore(const std::vector& assertions, + theory::TheoryModel* m, + options::ModelCoresMode mode); }; /* class TheoryModelCoreBuilder */ } // namespace cvc5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 28ad11f46..f447773ad 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1135,7 +1135,8 @@ bool SmtEngine::isModelCoreSymbol(Node n) // impact whether we are in "sat" mode std::vector asserts = getAssertionsInternal(); d_pp->expandDefinitions(asserts); - ModelCoreBuilder::setModelCore(asserts, tm, opts.smt.modelCoresMode); + ModelCoreBuilder mcb(*d_env.get()); + mcb.setModelCore(asserts, tm, opts.smt.modelCoresMode); } return tm->isModelCoreSymbol(n); } diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index d666cdac5..78ff93c1a 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -602,7 +602,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e, { Node szl = nm->mkNode(DT_SIZE, n); Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex)); - szr = Rewriter::rewrite(szr); + szr = rewrite(szr); sbp_conj.push_back(szl.eqNode(szr)); } if (isVarAgnostic) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 427e0251f..feb19b182 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -327,7 +327,7 @@ void TheoryDatatypes::postCheck(Effort level) if( options::dtBinarySplit() && consIndex!=-1 ){ Node test = utils::mkTester(n, consIndex, dt); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; - test = Rewriter::rewrite( test ); + test = rewrite(test); NodeBuilder nb(kind::OR); nb << test << test.notNode(); Node lemma = nb; @@ -1009,7 +1009,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { } else { - rrs = Rewriter::rewrite(r); + rrs = rewrite(r); } if (s != rrs) { @@ -1424,7 +1424,7 @@ Node TheoryDatatypes::getInstantiateCons(Node n, const DType& dt, int index) //add constructor to equivalence class Node k = getTermSkolemFor( n ); Node n_ic = utils::getInstCons(k, dt, index); - n_ic = Rewriter::rewrite( n_ic ); + n_ic = rewrite(n_ic); // it may be a new term, so we collect terms and add it to the equality engine collectTerms( n_ic ); d_equalityEngine->addTerm(n_ic); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index dfce485f2..e0863f953 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -622,7 +622,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ { if (Trace.isOn("quantifiers-sk-debug")) { - Node slem = Rewriter::rewrite(lem.getNode()); + Node slem = rewrite(lem.getNode()); Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index d28bae12a..dc72783c0 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -761,7 +761,7 @@ void TheorySep::postCheck(Effort level) } else { - inst = Rewriter::rewrite(inst); + inst = rewrite(inst); if (inst == (polarity ? d_true : d_false)) { inst_success = false; @@ -1768,7 +1768,7 @@ void TheorySep::mergePto( Node p1, Node p2 ) { void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer ) { Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl; - conc = Rewriter::rewrite( conc ); + conc = rewrite(conc); Trace("sep-lemma-debug") << "Got : " << conc << std::endl; if( conc!=d_true ){ if( infer && conc!=d_false ){ diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index 2ec945963..56b7a2fed 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -27,7 +27,7 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { -SubstitutionMinimize::SubstitutionMinimize() {} +SubstitutionMinimize::SubstitutionMinimize(Env& env) : EnvObj(env) {} bool SubstitutionMinimize::find(Node t, Node target, @@ -119,7 +119,7 @@ bool SubstitutionMinimize::findWithImplied(Node t, // try the current substitution Node tcs = tc.substitute( reqVars.begin(), reqVars.end(), reqSubs.begin(), reqSubs.end()); - Node tcsr = Rewriter::rewrite(tcs); + Node tcsr = rewrite(tcs); std::vector tcsrConj; getConjuncts(tcsr, tcsrConj); for (const Node& tcc : tcsrConj) @@ -246,7 +246,7 @@ bool SubstitutionMinimize::findInternal(Node n, nb << it->second; } ret = nb.constructNode(); - ret = Rewriter::rewrite(ret); + ret = rewrite(ret); } value[cur] = ret; } @@ -323,7 +323,7 @@ bool SubstitutionMinimize::findInternal(Node n, // i to visit, and update curr below. if (scurr != curr) { - curr = Rewriter::rewrite(scurr); + curr = rewrite(scurr); visit.push_back(cur[i]); } } diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index c78467508..571f629dd 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -21,6 +21,7 @@ #include #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -30,10 +31,10 @@ namespace theory { * This class is used for finding a minimal substitution under which an * evaluation holds. */ -class SubstitutionMinimize +class SubstitutionMinimize : protected EnvObj { public: - SubstitutionMinimize(); + SubstitutionMinimize(Env& env); ~SubstitutionMinimize() {} /** find * @@ -45,11 +46,11 @@ class SubstitutionMinimize * If t { vars -> subs } does not rewrite to target, this method returns * false. */ - static bool find(Node t, - Node target, - const std::vector& vars, - const std::vector& subs, - std::vector& reqVars); + bool find(Node t, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars); /** find with implied * * This method should be called on a formula t. @@ -73,26 +74,26 @@ class SubstitutionMinimize * to appear in reqVars, whereas those later in the vars are more likely to * appear in impliedVars. */ - static bool findWithImplied(Node t, - const std::vector& vars, - const std::vector& subs, - std::vector& reqVars, - std::vector& impliedVars); + bool findWithImplied(Node t, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars, + std::vector& impliedVars); private: /** Common helper function for the above functions. */ - static bool findInternal(Node t, - Node target, - const std::vector& vars, - const std::vector& subs, - std::vector& reqVars); + bool findInternal(Node t, + Node target, + const std::vector& vars, + const std::vector& subs, + std::vector& reqVars); /** is singular arg * * Returns true if * ( ... t_{arg-1}, n, t_{arg+1}...) = c * always holds for some constant c. */ - static bool isSingularArg(Node n, Kind k, unsigned arg); + bool isSingularArg(Node n, Kind k, unsigned arg); }; } // namespace theory