Eliminating static calls to rewriter in quantifiers (#7301)

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<Node>& 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<Node>& 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<Node>& 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<TypeNode>& 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]))