From 6f8200beec0c219d01ce57dab2ad8e3aa283e872 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Oct 2021 12:54:58 -0500 Subject: [PATCH] Eliminating static calls to rewriter in quantifiers (#7301) --- .../quantifiers/candidate_rewrite_database.cpp | 4 ++-- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 4 ++-- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 6 +++--- src/theory/quantifiers/fmf/bounded_integers.cpp | 13 ++++++++----- src/theory/quantifiers/fmf/full_model_check.cpp | 2 +- src/theory/quantifiers/instantiate.cpp | 8 ++++---- src/theory/quantifiers/quant_conflict_find.cpp | 2 +- src/theory/quantifiers/sygus/cegis.cpp | 6 +++--- src/theory/quantifiers/sygus_inst.cpp | 1 - src/theory/quantifiers/term_database.cpp | 2 +- 10 files changed, 25 insertions(+), 23 deletions(-) diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index ab1efe728..eda56ef52 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -128,8 +128,8 @@ Node CandidateRewriteDatabase::addTerm(Node sol, } else { - solbr = Rewriter::rewrite(solb); - eq_solr = Rewriter::rewrite(eq_solb); + solbr = rewrite(solb); + eq_solr = rewrite(eq_solb); } bool verified = false; Trace("rr-check") << "Check candidate rewrite..." << std::endl; diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 5b5c1cc86..d1ac87626 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -101,7 +101,7 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, Node inst = d_inverter->solveBvLit(sv, slit, path, &m); if (!inst.isNull()) { - inst = Rewriter::rewrite(inst); + inst = rewrite(inst); if (inst.isConst() || !ci->hasNestedQuantification()) { Trace("cegqi-bv") << "...solved form is " << inst << std::endl; @@ -180,7 +180,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, // (not) s ~ t ---> s = t + ( s^M - t^M ) if (sm != tm) { - Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); + Node slack = rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); Assert(slack.isConst()); // remember the slack value for the asserted literal d_alit_to_model_slack[lit] = slack; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index e4a75cebb..0337d8959 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -114,7 +114,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) d_qim.addPendingPhaseRequirement(ceLit, true); Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma - lem = Rewriter::rewrite( lem ); + lem = rewrite(lem); Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl; registerCounterexampleLemma( q, lem ); @@ -353,7 +353,7 @@ TrustNode InstStrategyCegqi::rewriteInstantiation(Node q, if (doVts) { // do virtual term substitution - inst = Rewriter::rewrite(inst); + inst = rewrite(inst); Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl; inst = d_vtsCache->rewriteVtsSymbols(inst); Trace("quant-vts-debug") << "...got " << inst << std::endl; @@ -440,7 +440,7 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_check_vts_lemma_lc = false; d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const_multiplier); - d_small_const = Rewriter::rewrite( d_small_const ); + d_small_const = rewrite(d_small_const); //heuristic for now, until we know how to do nested quantification Node delta = d_vtsCache->getVtsDelta(true, false); if( !delta.isNull() ){ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 44352c6fe..656af0e2f 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -362,7 +362,7 @@ void BoundedIntegers::checkOwnership(Node f) d_bounds[b][f][v] = bound_int_range_term[b][v]; } Node r = nm->mkNode(MINUS, d_bounds[1][f][v], d_bounds[0][f][v]); - d_range[f][v] = Rewriter::rewrite(r); + d_range[f][v] = rewrite(r); Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; } }else if( it->second==BOUND_SET_MEMBER ){ @@ -804,9 +804,12 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node //failed, abort the iterator return false; }else{ + NodeManager* nm = NodeManager::currentNM(); Trace("bound-int-rsi") << "Can limit bounds of " << v << " to " << l << "..." << u << std::endl; - Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); - Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); + Node range = rewrite(nm->mkNode(MINUS, u, l)); + // 9999 is an arbitrary range past which we do not do exhaustive + // bounded instantation, based on the check below. + Node ra = rewrite(nm->mkNode(LEQ, range, nm->mkConst(Rational(9999)))); Node tl = l; Node tu = u; getBounds( q, v, rsi, tl, tu ); @@ -817,8 +820,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; for (long k = 0; k < rr; k++) { - Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) ); - t = Rewriter::rewrite( t ); + Node t = nm->mkNode(PLUS, tl, nm->mkConst(Rational(k))); + t = rewrite(t); elements.push_back( t ); } return true; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index f8b90f624..7c1d36ce8 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -1342,7 +1342,7 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) } Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children); Trace("fmc-eval") << "Evaluate " << nc << " to "; - nc = Rewriter::rewrite(nc); + nc = rewrite(nc); Trace("fmc-eval") << nc << std::endl; return nc; } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 4d90fe95b..0807188d5 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -303,7 +303,7 @@ bool Instantiate::addInstantiation(Node q, // store in the main proof d_pfInst->addProof(pfns); Node prevLem = lem; - lem = Rewriter::rewrite(lem); + lem = rewrite(lem); if (prevLem != lem) { d_pfInst->addStep(lem, PfRule::MACRO_SR_PRED_ELIM, {prevLem}, {}); @@ -312,7 +312,7 @@ bool Instantiate::addInstantiation(Node q, } else { - lem = Rewriter::rewrite(lem); + lem = rewrite(lem); } // added lemma, which checks for lemma duplication @@ -423,7 +423,7 @@ bool Instantiate::addInstantiationExpFail(Node q, InferenceId idNone = InferenceId::UNKNOWN; Node nulln; Node ibody = getInstantiation(q, vars, terms, idNone, nulln, doVts); - ibody = Rewriter::rewrite(ibody); + ibody = rewrite(ibody); for (size_t i = 0; i < tsize; i++) { // process consecutively in reverse order, which is important since we use @@ -452,7 +452,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (!success) { Node ibodyc = getInstantiation(q, vars, terms, idNone, nulln, doVts); - ibodyc = Rewriter::rewrite(ibodyc); + ibodyc = rewrite(ibodyc); success = (ibodyc == ibody); Trace("inst-exp-fail") << " rewrite invariant: " << success << std::endl; } diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b26b65018..361adfd54 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -653,7 +653,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl; - Node rew = Rewriter::rewrite( lit ); + Node rew = Rewriter::rewrite(lit); if (rew.isConst()) { Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to " diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index d9e4b61af..688d66cc3 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -366,7 +366,7 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, std::vector& waiting) { Node lem = waiting[wcounter]; - lem = Rewriter::rewrite(lem); + lem = rewrite(lem); // apply substitution and rewrite if applicable if (lem.isConst()) { @@ -632,7 +632,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, candidates.begin(), candidates.end(), vals.begin(), vals.end()); Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl; // do eager rewriting - sbody = Rewriter::rewrite(sbody); + sbody = rewrite(sbody); Trace("cegis-sample") << "Sample (after rewriting): " << sbody << std::endl; NodeManager* nm = NodeManager::currentNM(); @@ -656,7 +656,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector& candidates, Assert(d_base_vars.size() == pt.size()); Node rlem = d_base_body.substitute( d_base_vars.begin(), d_base_vars.end(), pt.begin(), pt.end()); - rlem = Rewriter::rewrite(rlem); + rlem = rewrite(rlem); if (std::find( d_refinement_lemmas.begin(), d_refinement_lemmas.end(), rlem) == d_refinement_lemmas.end()) diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 64bc578a5..d437bde8d 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -539,7 +539,6 @@ void SygusInst::registerCeLemma(Node q, std::vector& types) Node body = q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end()); Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate()); - lem = Rewriter::rewrite(lem); d_ce_lemmas.emplace(std::make_pair(q, lem)); Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 6644f2b27..b1537a390 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -586,7 +586,7 @@ Node TermDb::evaluateTerm2(TNode n, args.insert(args.begin(), n.getOperator()); } ret = NodeManager::currentNM()->mkNode(n.getKind(), args); - ret = Rewriter::rewrite(ret); + ret = rewrite(ret); if (ret.getKind() == EQUAL) { if (d_qstate.areDisequal(ret[0], ret[1])) -- 2.30.2