Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)

There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter.

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 4823c16e2584546ea6736a2c8fbfb7e1731f0bff..9db6149ef863c0e105c3a2607b8e3f16cb4b323e 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -185,7 +185,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m,
       elementReps[key] = value;
     }
     Node rep = NormalForm::constructBagFromElements(tn, elementReps);
-    rep = Rewriter::rewrite(rep);
+    rep = rewrite(rep);
     Trace("bags-model") << "rep of " << n << " is: " << rep << std::endl;
     m->assertEquality(rep, n, true);
     m->assertSkeleton(rep);

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 4e4ee78a82febbd3a67821a3f732f69b12dcce85..d2d7a636a33031e0f7451a1f440ff70eae1b7885 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -162,7 +162,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t)
       Node subset = nm->mkNode(kind::SUBSET, variable, proxy);
       // subset terms are rewritten as union terms: (subset A B) implies (=
       // (union A B) B)
-      subset = Rewriter::rewrite(subset);
+      subset = rewrite(subset);
       if (!d_state.isEntailed(subset, true))
       {
         d_im.assertInference(
@@ -242,7 +242,7 @@ void CardinalityExtension::checkRegister()
         // if setminus, do for intersection instead
         if (n.getKind() == SETMINUS)
         {
-          n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+          n = rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
         }
         registerCardinalityTerm(n);
       }
@@ -293,7 +293,7 @@ void CardinalityExtension::registerCardinalityTerm(Node n)
     if (nn != nk)
     {
       Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
-      lem = Rewriter::rewrite(lem);
+      lem = rewrite(lem);
       Trace("sets-card") << "  " << k << " : " << lem << std::endl;
       d_im.assertInference(lem, InferenceId::SETS_CARD_EQUAL, d_emp_exp, 1);
     }
@@ -393,21 +393,21 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       d_localBase[n] = n;
       for (unsigned e = 0; e < 2; e++)
       {
-        Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
+        Node sm = rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
         sib.push_back(sm);
       }
       true_sib = 2;
     }
     else
     {
-      Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
+      Node si = rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
       sib.push_back(si);
       d_localBase[n] = si;
-      Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
+      Node osm = rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
       sib.push_back(osm);
       true_sib = 1;
     }
-    Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
+    Node u = rewrite(nm->mkNode(UNION, n[0], n[1]));
     if (!d_state.hasTerm(u))
     {
       u = Node::null();
@@ -837,8 +837,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
               Assert(o0 != o1);
               Node kca = d_treg.getProxy(o0);
               Node kcb = d_treg.getProxy(o1);
-              Node intro =
-                  Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
+              Node intro = rewrite(nm->mkNode(INTERSECTION, kca, kcb));
               Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
                                << ", term is " << intro << std::endl;
               intro_sets.push_back(intro);

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 15c4fd405b35e95216cc49b1a427fd7329a243a5..96705c029347173832f24fd8e88bcd9b7d4e46a5 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -35,7 +35,7 @@ InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
 bool InferenceManager::assertFactRec(Node fact, InferenceId id, Node exp, int inferType)
 {
   // should we send this fact out as a lemma?
-  if ((options::setsInferAsLemmas() && inferType != -1) || inferType == 1)
+  if ((options().sets.setsInferAsLemmas && inferType != -1) || inferType == 1)
   {
     if (d_state.isEntailed(fact, true))
     {
@@ -172,7 +172,7 @@ void InferenceManager::assertInference(std::vector<Node>& conc,
 
 void InferenceManager::split(Node n, InferenceId id, int reqPol)
 {
-  n = Rewriter::rewrite(n);
+  n = rewrite(n);
   Node lem = NodeManager::currentNM()->mkNode(OR, n, n.negate());
   // send the lemma
   lemma(lem, id);

diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp
index f759c2a7b15ff093265b70410ea49e75ffcb4c48..646ae16626693aafca67bb29f7b1031bf42e89b9 100644 (file)
--- a/src/theory/sets/skolem_cache.cpp
+++ b/src/theory/sets/skolem_cache.cpp
@@ -24,14 +24,16 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-SkolemCache::SkolemCache() {}
+SkolemCache::SkolemCache(Rewriter* rr) : d_rewriter(rr) {}
 
 Node SkolemCache::mkTypedSkolemCached(
     TypeNode tn, Node a, Node b, SkolemId id, const char* c)
 {
-  a = a.isNull() ? a : Rewriter::rewrite(a);
-  b = b.isNull() ? b : Rewriter::rewrite(b);
-
+  if (d_rewriter != nullptr)
+  {
+    a = a.isNull() ? a : d_rewriter->rewrite(a);
+    b = b.isNull() ? b : d_rewriter->rewrite(b);
+  }
   std::map<SkolemId, Node>::iterator it = d_skolemCache[a][b].find(id);
   if (it == d_skolemCache[a][b].end())
   {

diff --git a/src/theory/sets/skolem_cache.h b/src/theory/sets/skolem_cache.h
index 62547a66e576c261a970bec205a98cc01f914552..a13c48f1e68891bb5bced796d011430bc1bcefbc 100644 (file)
--- a/src/theory/sets/skolem_cache.h
+++ b/src/theory/sets/skolem_cache.h
@@ -25,6 +25,9 @@
 
 namespace cvc5 {
 namespace theory {
+
+class Rewriter;
+
 namespace sets {
 
 /**
@@ -35,7 +38,7 @@ namespace sets {
 class SkolemCache
 {
  public:
-  SkolemCache();
+  SkolemCache(Rewriter* rr);
   /** Identifiers for skolem types
    *
    * The comments below document the properties of each skolem introduced by
@@ -75,6 +78,8 @@ class SkolemCache
   std::map<Node, std::map<Node, std::map<SkolemId, Node> > > d_skolemCache;
   /** the set of all skolems we have generated */
   std::unordered_set<Node> d_allSkolems;
+  /** the optional rewriter */
+  Rewriter* d_rewriter;
 };
 
 }  // namespace sets

diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 6f8976f4d1340f4d4332976d584993dd336fa99c..d9fb3073571f489c69ae5cba1f842fe37db79fad 100644 (file)
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -113,7 +113,7 @@ void SolverState::registerTerm(Node r, TypeNode tnn, Node n)
     }
     else if (nk == UNIVERSE_SET)
     {
-      Assert(options::setsExt());
+      Assert(options().sets.setsExt);
       d_eqc_univset[tnn] = r;
     }
     else

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 2901703ddbc12d67c036fc5b0972317fea73d873..3cb6c853c12aadec76c3a5f7f30758da669c61a2 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -29,7 +29,7 @@ namespace sets {
 
 TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SETS, env, out, valuation),
-      d_skCache(),
+      d_skCache(env.getRewriter()),
       d_state(env, valuation, d_skCache),
       d_im(env, *this, d_state),
       d_internal(
@@ -136,7 +136,7 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
   if (nk == UNIVERSE_SET || nk == COMPLEMENT || nk == JOIN_IMAGE
       || nk == COMPREHENSION)
   {
-    if (!options::setsExt())
+    if (!options().sets.setsExt)
     {
       std::stringstream ss;
       ss << "Extended set operators are not supported in default mode, try "
@@ -173,7 +173,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(
       // may appear when this option is enabled, and solving for such a set
       // impacts the semantics of universe set, see
       // regress0/sets/pre-proc-univ.smt2
-      if (!in[0].getType().isSet() || !options::setsExt())
+      if (!in[0].getType().isSet() || !options().sets.setsExt)
       {
         outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
         status = Theory::PP_ASSERT_STATUS_SOLVED;
@@ -181,7 +181,7 @@ Theory::PPAssertStatus TheorySets::ppAssert(
     }
     else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
     {
-      if (!in[0].getType().isSet() || !options::setsExt())
+      if (!in[0].getType().isSet() || !options().sets.setsExt)
       {
         outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
         status = Theory::PP_ASSERT_STATUS_SOLVED;

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 2164c26b061fd579bc9b68b33a80c9de299aaa98..324d6b7dce767766b8b2e0e0ee7cf44e5ae154c0 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -454,11 +454,11 @@ void TheorySetsPrivate::checkDownwardsClosure()
             {
               Trace("sets-debug") << "Downwards closure based on " << mem
                                   << ", eq_set = " << eq_set << std::endl;
-              if (!options::setsProxyLemmas())
+              if (!options().sets.setsProxyLemmas)
               {
                 Node nmem = NodeManager::currentNM()->mkNode(
                     kind::MEMBER, mem[0], eq_set);
-                nmem = Rewriter::rewrite(nmem);
+                nmem = rewrite(nmem);
                 std::vector<Node> exp;
                 exp.push_back(mem);
                 exp.push_back(mem[1].eqNode(eq_set));
@@ -476,7 +476,7 @@ void TheorySetsPrivate::checkDownwardsClosure()
                     NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
                 Node nmem = NodeManager::currentNM()->mkNode(
                     kind::MEMBER, mem[0], eq_set);
-                nmem = Rewriter::rewrite(nmem);
+                nmem = rewrite(nmem);
                 std::vector<Node> exp;
                 if (d_state.areEqual(mem, pmem))
                 {
@@ -635,7 +635,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
   }
   if (!d_im.hasSent())
   {
-    if (options::setsExt())
+    if (options().sets.setsExt)
     {
       // universal sets
       Trace("sets-debug") << "Check universe sets..." << std::endl;
@@ -737,7 +737,7 @@ void TheorySetsPrivate::checkDisequalities()
     Node mem1 = nm->mkNode(MEMBER, x, deq[0]);
     Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
     Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
-    lem = Rewriter::rewrite(lem);
+    lem = rewrite(lem);
     d_im.assertInference(lem, InferenceId::SETS_DEQ, d_true, 1);
     d_im.doPendingLemmas();
     if (d_im.hasSent())
@@ -1152,7 +1152,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
       }
 
       Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
-      rep = Rewriter::rewrite(rep);
+      rep = rewrite(rep);
       Trace("sets-model") << "* Assign representative of " << eqc << " to "
                           << rep << std::endl;
       mvals[eqc] = rep;
@@ -1361,7 +1361,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
 
   // we call the rewriter here to handle the pattern
   // (is_singleton (singleton x)) because the rewriter is called after expansion
-  Node rewritten = Rewriter::rewrite(node);
+  Node rewritten = rewrite(node);
   if (rewritten.getKind() != IS_SINGLETON)
   {
     return TrustNode::mkTrustRewrite(node, rewritten, nullptr);