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

[cvc5.git] / src / theory / sets / theory_sets.cpp

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 23ac0874936c6eed4ec38953be1f1ecb5c789cc3..3cb6c853c12aadec76c3a5f7f30758da669c61a2 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -29,10 +29,11 @@ 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(*this, d_state, d_pnm),
-      d_internal(new TheorySetsPrivate(*this, d_state, d_im, d_skCache, d_pnm)),
+      d_im(env, *this, d_state),
+      d_internal(
+          new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)),
       d_notify(*d_internal.get(), d_im)
 {
   // use the official theory state and inference manager objects
@@ -135,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 "
@@ -146,7 +147,7 @@ TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
   if (nk == COMPREHENSION)
   {
     // set comprehension is an implicit quantifier, require it in the logic
-    if (!getLogicInfo().isQuantified())
+    if (!logicInfo().isQuantified())
     {
       std::stringstream ss;
       ss << "Set comprehensions require quantifiers in the background logic.";
@@ -172,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;
@@ -180,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;