From a09a4a300d52cdb4026bbba0184da152e0a65296 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 3 Feb 2022 13:19:31 -0600 Subject: [PATCH] Eliminate more static uses of rewrite (#8040) --- src/expr/subs.cpp | 21 +-- src/expr/subs.h | 8 +- src/theory/quantifiers/cegqi/nested_qe.cpp | 4 +- .../quantifiers/ematching/im_generator.cpp | 7 +- .../quantifiers/ematching/im_generator.h | 127 +++++++++--------- .../ematching/inst_match_generator.cpp | 32 +++-- .../ematching/inst_match_generator.h | 12 +- .../ematching/inst_match_generator_multi.cpp | 7 +- .../ematching/inst_match_generator_multi.h | 5 +- .../inst_match_generator_multi_linear.cpp | 6 +- .../inst_match_generator_multi_linear.h | 3 +- .../ematching/inst_match_generator_simple.cpp | 5 +- .../ematching/inst_match_generator_simple.h | 2 +- .../ematching/pattern_term_selector.cpp | 1 - .../ematching/relational_match_generator.cpp | 8 +- .../ematching/relational_match_generator.h | 6 +- src/theory/quantifiers/ematching/trigger.cpp | 9 +- .../ematching/var_match_generator.cpp | 7 +- .../ematching/var_match_generator.h | 2 +- .../sygus/ce_guided_single_inv.cpp | 7 +- 20 files changed, 148 insertions(+), 131 deletions(-) diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index f08cf18c1..d01fa0843 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -18,7 +18,6 @@ #include #include "expr/skolem_manager.h" -#include "theory/rewriter.h" namespace cvc5 { @@ -98,7 +97,7 @@ void Subs::append(Subs& s) add(s.d_vars, s.d_subs); } -Node Subs::apply(Node n, bool doRewrite) const +Node Subs::apply(Node n) const { if (d_vars.empty()) { @@ -106,13 +105,9 @@ Node Subs::apply(Node n, bool doRewrite) const } Node ns = n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end()); - if (doRewrite) - { - ns = theory::Rewriter::rewrite(ns); - } return ns; } -Node Subs::rapply(Node n, bool doRewrite) const +Node Subs::rapply(Node n) const { if (d_vars.empty()) { @@ -120,14 +115,10 @@ Node Subs::rapply(Node n, bool doRewrite) const } Node ns = n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end()); - if (doRewrite) - { - ns = theory::Rewriter::rewrite(ns); - } return ns; } -void Subs::applyToRange(Subs& s, bool doRewrite) const +void Subs::applyToRange(Subs& s) const { if (d_vars.empty()) { @@ -135,11 +126,11 @@ void Subs::applyToRange(Subs& s, bool doRewrite) const } for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) { - s.d_subs[i] = apply(s.d_subs[i], doRewrite); + s.d_subs[i] = apply(s.d_subs[i]); } } -void Subs::rapplyToRange(Subs& s, bool doRewrite) const +void Subs::rapplyToRange(Subs& s) const { if (d_vars.empty()) { @@ -147,7 +138,7 @@ void Subs::rapplyToRange(Subs& s, bool doRewrite) const } for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) { - s.d_subs[i] = rapply(s.d_subs[i], doRewrite); + s.d_subs[i] = rapply(s.d_subs[i]); } } diff --git a/src/expr/subs.h b/src/expr/subs.h index 245c6d77a..fb68c9fce 100644 --- a/src/expr/subs.h +++ b/src/expr/subs.h @@ -58,13 +58,13 @@ class Subs /** Append the substitution s to this */ void append(Subs& s); /** Return the result of this substitution on n */ - Node apply(Node n, bool doRewrite = false) const; + Node apply(Node n) const; /** Return the result of the reverse of this substitution on n */ - Node rapply(Node n, bool doRewrite = false) const; + Node rapply(Node n) const; /** Apply this substitution to all nodes in the range of s */ - void applyToRange(Subs& s, bool doRewrite = false) const; + void applyToRange(Subs& s) const; /** Apply the reverse of this substitution to all nodes in the range of s */ - void rapplyToRange(Subs& s, bool doRewrite = false) const; + void rapplyToRange(Subs& s) const; /** Get equality (= v s) where v -> s is the i^th position in the vectors */ Node getEquality(size_t i) const; /** Convert substitution to map */ diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index fddcb0712..1b6ba44f2 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "expr/subs.h" #include "smt/env.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" namespace cvc5 { @@ -119,7 +120,8 @@ Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel) Node qeBody = sk.apply(q[1]); qeBody = snqe.apply(qeBody); // undo the skolemization - qeBody = sk.rapply(qeBody, true); + qeBody = sk.rapply(qeBody); + qeBody = env.getRewriter()->rewrite(qeBody); // reconstruct the body std::vector qargs; qargs.push_back(q[0]); diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp index b6df03644..c933f592f 100644 --- a/src/theory/quantifiers/ematching/im_generator.cpp +++ b/src/theory/quantifiers/ematching/im_generator.cpp @@ -24,8 +24,11 @@ namespace theory { namespace quantifiers { namespace inst { -IMGenerator::IMGenerator(Trigger* tparent) - : d_tparent(tparent), d_qstate(tparent->d_qstate), d_treg(tparent->d_treg) +IMGenerator::IMGenerator(Env& env, Trigger* tparent) + : EnvObj(env), + d_tparent(tparent), + d_qstate(tparent->d_qstate), + d_treg(tparent->d_treg) { } diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h index 12126b31b..8f26e552a 100644 --- a/src/theory/quantifiers/ematching/im_generator.h +++ b/src/theory/quantifiers/ematching/im_generator.h @@ -19,7 +19,9 @@ #define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H #include + #include "expr/node.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" #include "theory/quantifiers/inst_match.h" @@ -51,69 +53,70 @@ class Trigger; * point in which instantiate lemmas are enqueued to be sent on the output * channel. */ -class IMGenerator { -public: - IMGenerator(Trigger* tparent); - virtual ~IMGenerator() {} - /** Reset instantiation round. - * - * Called once at beginning of an instantiation round. - */ - virtual void resetInstantiationRound() {} - /** Reset. - * - * eqc is the equivalence class to search in (any if eqc=null). - * Returns true if this generator can produce instantiations, and false - * otherwise. An example of when it returns false is if it can be determined - * that no appropriate matchable terms occur based on eqc. - */ - virtual bool reset(Node eqc) { return true; } - /** Get the next match. - * - * Must call reset( eqc ) before this function. This constructs an - * instantiation, which it populates in data structure m, - * based on the current context using the implemented matching algorithm. - * - * q is the quantified formula we are adding instantiations for - * m is the InstMatch object we are generating - * - * Returns a value >0 if an instantiation was successfully generated - */ - virtual int getNextMatch(Node q, InstMatch& m) { return 0; } - /** add instantiations - * - * This adds all available instantiations for q based on the current context - * using the implemented matching algorithm. It typically is implemented as a - * fixed point of getNextMatch above. - * - * It returns the number of instantiations added using calls to - * Instantiate::addInstantiation(...). - */ - virtual uint64_t addInstantiations(Node q) { return 0; } - /** get active score - * - * A heuristic value indicating how active this generator is. - */ - virtual int getActiveScore() { return 0; } +class IMGenerator : protected EnvObj +{ + public: + IMGenerator(Env& env, Trigger* tparent); + virtual ~IMGenerator() {} + /** Reset instantiation round. + * + * Called once at beginning of an instantiation round. + */ + virtual void resetInstantiationRound() {} + /** Reset. + * + * eqc is the equivalence class to search in (any if eqc=null). + * Returns true if this generator can produce instantiations, and false + * otherwise. An example of when it returns false is if it can be determined + * that no appropriate matchable terms occur based on eqc. + */ + virtual bool reset(Node eqc) { return true; } + /** Get the next match. + * + * Must call reset( eqc ) before this function. This constructs an + * instantiation, which it populates in data structure m, + * based on the current context using the implemented matching algorithm. + * + * q is the quantified formula we are adding instantiations for + * m is the InstMatch object we are generating + * + * Returns a value >0 if an instantiation was successfully generated + */ + virtual int getNextMatch(Node q, InstMatch& m) { return 0; } + /** add instantiations + * + * This adds all available instantiations for q based on the current context + * using the implemented matching algorithm. It typically is implemented as a + * fixed point of getNextMatch above. + * + * It returns the number of instantiations added using calls to + * Instantiate::addInstantiation(...). + */ + virtual uint64_t addInstantiations(Node q) { return 0; } + /** get active score + * + * A heuristic value indicating how active this generator is. + */ + virtual int getActiveScore() { return 0; } -protected: - /** send instantiation - * - * This method sends instantiation, specified by m, to the parent trigger - * object, which will in turn make a call to - * Instantiate::addInstantiation(...). This method returns true if a - * call to Instantiate::addInstantiation(...) was successfully made, - * indicating that an instantiation was enqueued in the quantifier engine's - * lemma cache. - */ - bool sendInstantiation(InstMatch& m, InferenceId id); - /** The parent trigger that owns this */ - Trigger* d_tparent; - /** Reference to the state of the quantifiers engine */ - QuantifiersState& d_qstate; - /** Reference to the term registry */ - TermRegistry& d_treg; -};/* class IMGenerator */ + protected: + /** send instantiation + * + * This method sends instantiation, specified by m, to the parent trigger + * object, which will in turn make a call to + * Instantiate::addInstantiation(...). This method returns true if a + * call to Instantiate::addInstantiation(...) was successfully made, + * indicating that an instantiation was enqueued in the quantifier engine's + * lemma cache. + */ + bool sendInstantiation(InstMatch& m, InferenceId id); + /** The parent trigger that owns this */ + Trigger* d_tparent; + /** Reference to the state of the quantifiers engine */ + QuantifiersState& d_qstate; + /** Reference to the term registry */ + TermRegistry& d_treg; +}; /* class IMGenerator */ } // namespace inst } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 51a36518b..1adf50ddd 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -30,6 +30,7 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "util/rational.h" using namespace cvc5::kind; @@ -39,8 +40,8 @@ namespace theory { namespace quantifiers { namespace inst { -InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat) - : IMGenerator(tparent) +InstMatchGenerator::InstMatchGenerator(Env& env, Trigger* tparent, Node pat) + : IMGenerator(env, tparent) { d_cg = nullptr; d_needsReset = true; @@ -184,7 +185,8 @@ void InstMatchGenerator::initialize(Node q, } else { - InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat); + InstMatchGenerator* cimg = + getInstMatchGenerator(d_env, d_tparent, q, pat); if (cimg) { d_children.push_back(cimg); @@ -576,22 +578,23 @@ uint64_t InstMatchGenerator::addInstantiations(Node f) return addedLemmas; } -InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent, +InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Env& env, + Trigger* tparent, Node q, Node pat) { std::vector< Node > pats; pats.push_back( pat ); std::map< Node, InstMatchGenerator * > pat_map_init; - return mkInstMatchGenerator(tparent, q, pats, pat_map_init); + return mkInstMatchGenerator(env, tparent, q, pats, pat_map_init); } InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( - Trigger* tparent, Node q, std::vector& pats) + Env& env, Trigger* tparent, Node q, std::vector& pats) { Assert(pats.size() > 1); InstMatchGeneratorMultiLinear* imgm = - new InstMatchGeneratorMultiLinear(tparent, q, pats); + new InstMatchGeneratorMultiLinear(env, tparent, q, pats); std::vector< InstMatchGenerator* > gens; imgm->initialize(q, gens); Assert(gens.size() == pats.size()); @@ -603,11 +606,12 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( patsn.push_back( pn ); pat_map_init[pn] = g; } - imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init); + imgm->d_next = mkInstMatchGenerator(env, tparent, q, patsn, pat_map_init); return imgm; } InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( + Env& env, Trigger* tparent, Node q, std::vector& pats, @@ -622,7 +626,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( InstMatchGenerator* init; std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] ); if( iti==pat_map_init.end() ){ - init = getInstMatchGenerator(tparent, q, pats[pCounter]); + init = getInstMatchGenerator(env, tparent, q, pats[pCounter]); }else{ init = iti->second; } @@ -645,7 +649,8 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( return oinit; } -InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, +InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Env& env, + Trigger* tparent, Node q, Node n) { @@ -670,8 +675,9 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, if (!x.isNull()) { Node s = PatternTermSelector::getInversion(n, x); + s = env.getRewriter()->rewrite(s); VarMatchGeneratorTermSubs* vmg = - new VarMatchGeneratorTermSubs(tparent, x, s); + new VarMatchGeneratorTermSubs(env, tparent, x, s); Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl; return vmg; @@ -685,9 +691,9 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit)) { Trace("relational-trigger") << "...yes, for literal " << lit << std::endl; - return new RelationalMatchGenerator(tparent, lit, hasPol, pol); + return new RelationalMatchGenerator(env, tparent, lit, hasPol, pol); } - return new InstMatchGenerator(tparent, n); + return new InstMatchGenerator(env, tparent, n); } } // namespace inst diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 684751292..75c8435ee 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -149,7 +149,8 @@ class InstMatchGenerator : public IMGenerator { void setIndependent() { d_independent_gen = true; } //-------------------------------construction of inst match generators /** mkInstMatchGenerator for single triggers, calls the method below */ - static InstMatchGenerator* mkInstMatchGenerator(Trigger* tparent, + static InstMatchGenerator* mkInstMatchGenerator(Env& env, + Trigger* tparent, Node q, Node pat); /** mkInstMatchGenerator for the multi trigger case @@ -159,7 +160,8 @@ class InstMatchGenerator : public IMGenerator { * InstMatchGenerators corresponding to each unique subterm of pats with * free variables. */ - static InstMatchGenerator* mkInstMatchGeneratorMulti(Trigger* tparent, + static InstMatchGenerator* mkInstMatchGeneratorMulti(Env& env, + Trigger* tparent, Node q, std::vector& pats); /** mkInstMatchGenerator @@ -176,6 +178,7 @@ class InstMatchGenerator : public IMGenerator { * It calls initialize(...) for all InstMatchGenerators generated by this call. */ static InstMatchGenerator* mkInstMatchGenerator( + Env& env, Trigger* tparent, Node q, std::vector& pats, @@ -188,7 +191,7 @@ class InstMatchGenerator : public IMGenerator { * These are intentionally private, and are called during linked list * construction in mkInstMatchGenerator. */ - InstMatchGenerator(Trigger* tparent, Node pat); + InstMatchGenerator(Env& env, Trigger* tparent, Node pat); /** The pattern we are producing matches for. * * This term and d_match_pattern can be different since this @@ -319,7 +322,8 @@ class InstMatchGenerator : public IMGenerator { * appropriate matching algorithm for n within q * within a linked list of InstMatchGenerators. */ - static InstMatchGenerator* getInstMatchGenerator(Trigger* tparent, + static InstMatchGenerator* getInstMatchGenerator(Env& env, + Trigger* tparent, Node q, Node n); };/* class InstMatchGenerator */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 4d8280c83..10d296db0 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -26,10 +26,11 @@ namespace theory { namespace quantifiers { namespace inst { -InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent, +InstMatchGeneratorMulti::InstMatchGeneratorMulti(Env& env, + Trigger* tparent, Node q, std::vector& pats) - : IMGenerator(tparent), d_quant(q) + : IMGenerator(env, tparent), d_quant(q) { Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl; @@ -57,7 +58,7 @@ InstMatchGeneratorMulti::InstMatchGeneratorMulti(Trigger* tparent, Node n = pats[i]; // make the match generator InstMatchGenerator* img = - InstMatchGenerator::mkInstMatchGenerator(tparent, q, n); + InstMatchGenerator::mkInstMatchGenerator(env, tparent, q, n); img->setActiveAdd(false); d_children.push_back(img); // compute unique/shared variables diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h index c3549f870..d8ebdee3f 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h @@ -40,7 +40,10 @@ class InstMatchGeneratorMulti : public IMGenerator { public: /** constructors */ - InstMatchGeneratorMulti(Trigger* tparent, Node q, std::vector& pats); + InstMatchGeneratorMulti(Env& env, + Trigger* tparent, + Node q, + std::vector& pats); /** destructor */ ~InstMatchGeneratorMulti() override; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 0b19361d5..1b9443dc6 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -26,8 +26,8 @@ namespace quantifiers { namespace inst { InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( - Trigger* tparent, Node q, std::vector& pats) - : InstMatchGenerator(tparent, Node::null()) + Env& env, Trigger* tparent, Node q, std::vector& pats) + : InstMatchGenerator(env, tparent, Node::null()) { // order patterns to maximize eager matching failures std::map > var_contains; @@ -102,7 +102,7 @@ InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( { Node po = pats_ordered[i]; Trace("multi-trigger-linear") << "...make for " << po << std::endl; - InstMatchGenerator* cimg = getInstMatchGenerator(tparent, q, po); + InstMatchGenerator* cimg = getInstMatchGenerator(env, tparent, q, po); Assert(cimg != nullptr); d_children.push_back(cimg); // this could be improved diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h index afe43a604..cb3476ab7 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h @@ -78,7 +78,8 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator /** reset the children of this generator */ int resetChildren(); /** constructor */ - InstMatchGeneratorMultiLinear(Trigger* tparent, + InstMatchGeneratorMultiLinear(Env& env, + Trigger* tparent, Node q, std::vector& pats); }; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index a64f268ca..10dcfe129 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -29,10 +29,11 @@ namespace theory { namespace quantifiers { namespace inst { -InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent, +InstMatchGeneratorSimple::InstMatchGeneratorSimple(Env& env, + Trigger* tparent, Node q, Node pat) - : IMGenerator(tparent), d_quant(q), d_match_pattern(pat) + : IMGenerator(env, tparent), d_quant(q), d_match_pattern(pat) { if (d_match_pattern.getKind() == NOT) { diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h index 8078087c8..2d26919ac 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h @@ -47,7 +47,7 @@ class InstMatchGeneratorSimple : public IMGenerator { public: /** constructors */ - InstMatchGeneratorSimple(Trigger* tparent, Node q, Node pat); + InstMatchGeneratorSimple(Env& env, Trigger* tparent, Node q, Node pat); /** Reset instantiation round. */ void resetInstantiationRound() override; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index 77ab46868..405f1fd69 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -694,7 +694,6 @@ Node PatternTermSelector::getInversion(Node n, Node x) x = nm->mkNode(MULT, x, coeff); } } - x = Rewriter::rewrite(x); } else { diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp index 8c467489d..db523683c 100644 --- a/src/theory/quantifiers/ematching/relational_match_generator.cpp +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -25,11 +25,9 @@ namespace theory { namespace quantifiers { namespace inst { -RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, - Node rtrigger, - bool hasPol, - bool pol) - : InstMatchGenerator(tparent, Node::null()), +RelationalMatchGenerator::RelationalMatchGenerator( + Env& env, Trigger* tparent, Node rtrigger, bool hasPol, bool pol) + : InstMatchGenerator(env, tparent, Node::null()), d_vindex(-1), d_hasPol(hasPol), d_pol(pol), diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h index eead2876a..4aec7ae87 100644 --- a/src/theory/quantifiers/ematching/relational_match_generator.h +++ b/src/theory/quantifiers/ematching/relational_match_generator.h @@ -55,10 +55,8 @@ class RelationalMatchGenerator : public InstMatchGenerator * @param hasPol Whether the trigger has an entailed polarity * @param pol The entailed polarity of the relational trigger. */ - RelationalMatchGenerator(Trigger* tparent, - Node rtrigger, - bool hasPol, - bool pol); + RelationalMatchGenerator( + Env& env, Trigger* tparent, Node rtrigger, bool hasPol, bool pol); /** Reset */ bool reset(Node eqc) override; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index e267b470d..1a7946564 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -88,20 +88,21 @@ Trigger::Trigger(Env& env, if( d_nodes.size()==1 ){ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) { - d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); + d_mg = new InstMatchGeneratorSimple(env, this, q, d_nodes[0]); ++(stats.d_triggers); }else{ - d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); + d_mg = InstMatchGenerator::mkInstMatchGenerator(env, this, q, d_nodes[0]); ++(stats.d_simple_triggers); } }else{ if (options().quantifiers.multiTriggerCache) { - d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); + d_mg = new InstMatchGeneratorMulti(env, this, q, d_nodes); } else { - d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); + d_mg = + InstMatchGenerator::mkInstMatchGeneratorMulti(env, this, q, d_nodes); } if (Trace.isOn("multi-trigger")) { diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index c03bf6960..9ad52a1da 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -24,10 +24,11 @@ namespace theory { namespace quantifiers { namespace inst { -VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Trigger* tparent, +VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs(Env& env, + Trigger* tparent, Node var, Node subs) - : InstMatchGenerator(tparent, Node::null()), + : InstMatchGenerator(env, tparent, Node::null()), d_var(var), d_subs(subs), d_rm_prev(false) @@ -51,7 +52,7 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m) << d_var << " in " << d_subs << std::endl; TNode tvar = d_var; Node s = d_subs.substitute(tvar, d_eq_class); - s = Rewriter::rewrite(s); + s = rewrite(s); Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl; d_eq_class = Node::null(); diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h index e664ac1db..4cdb4e620 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.h +++ b/src/theory/quantifiers/ematching/var_match_generator.h @@ -32,7 +32,7 @@ namespace inst { class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: - VarMatchGeneratorTermSubs(Trigger* tparent, Node var, Node subs); + VarMatchGeneratorTermSubs(Env& env, Trigger* tparent, Node var, Node subs); /** Reset */ bool reset(Node eqc) override; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 10e70d76a..127edac52 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -431,7 +431,12 @@ void CegSingleInv::setSolution() if (!d_solvedf.empty()) { // replace the final solution into the solved functions - finalSol.applyToRange(d_solvedf, true); + finalSol.applyToRange(d_solvedf); + // rewrite the solution + for (Node& n : d_solvedf.d_subs) + { + n = rewrite(n); + } } } -- 2.30.2