diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/datatypes/sygus_extension.cpp | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 4 | ||||
-rw-r--r-- | src/theory/subs_minimize.cpp | 8 | ||||
-rw-r--r-- | src/theory/subs_minimize.h | 37 |
6 files changed, 30 insertions, 29 deletions
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<Node> 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 <vector> #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<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars); + bool find(Node t, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& 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<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars, - std::vector<Node>& impliedVars); + bool findWithImplied(Node t, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars, + std::vector<Node>& impliedVars); private: /** Common helper function for the above functions. */ - static bool findInternal(Node t, - Node target, - const std::vector<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars); + bool findInternal(Node t, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars); /** is singular arg * * Returns true if * <k>( ... 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 |