bv: Use EnvObj::rewrite() and EnvObj::options() in BvSolver. (#7171)

8 files changed, 57 insertions, 45 deletions

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index c959fb648..510c8a29a 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -20,17 +20,19 @@
 #ifndef CVC5__THEORY__BV__BV_SOLVER_H
 #define CVC5__THEORY__BV__BV_SOLVER_H
 
+#include "smt/env.h"
+#include "smt/env_obj.h"
 #include "theory/theory.h"
 
 namespace cvc5 {
 namespace theory {
 namespace bv {
 
-class BVSolver
+class BVSolver : protected EnvObj
 {
  public:
-  BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
-      : d_state(state), d_im(inferMgr){};
+  BVSolver(Env& env, TheoryState& state, TheoryInferenceManager& inferMgr)
+      : EnvObj(env), d_state(state), d_im(inferMgr){};
 
   virtual ~BVSolver() {}
 
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index ecd42e4a0..9d316e91e 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -108,10 +108,11 @@ class BBRegistrar : public prop::Registrar
   std::unordered_set<TNode> d_registeredAtoms;
 };
 
-BVSolverBitblast::BVSolverBitblast(TheoryState* s,
+BVSolverBitblast::BVSolverBitblast(Env& env,
+                                   TheoryState* s,
                                    TheoryInferenceManager& inferMgr,
                                    ProofNodeManager* pnm)
-    : BVSolver(*s, inferMgr),
+    : BVSolver(env, *s, inferMgr),
       d_bitblaster(new NodeBitblaster(s)),
       d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
       d_nullContext(new context::Context()),
@@ -123,7 +124,7 @@ BVSolverBitblast::BVSolverBitblast(TheoryState* s,
                 : nullptr),
       d_factLiteralCache(s->getSatContext()),
       d_literalFactCache(s->getSatContext()),
-      d_propagate(options::bitvectorPropagate()),
+      d_propagate(options().bv.bitvectorPropagate),
       d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
 {
   if (pnm != nullptr)
@@ -147,7 +148,7 @@ void BVSolverBitblast::postCheck(Theory::Effort level)
 
   // If we permanently added assertions to the SAT solver and the assertions
   // were reset, we have to reset the SAT solver and the CNF stream.
-  if (options::bvAssertInput() && d_resetNotify->doneResetAssertions())
+  if (options().bv.bvAssertInput && d_resetNotify->doneResetAssertions())
   {
     d_satSolver.reset(nullptr);
     d_cnfStream.reset(nullptr);
@@ -248,7 +249,7 @@ bool BVSolverBitblast::preNotifyFact(
    * If this is the case we can assert `fact` to the SAT solver instead of
    * using assumptions.
    */
-  if (options::bvAssertInput() && val.isSatLiteral(fact)
+  if (options().bv.bvAssertInput && val.isSatLiteral(fact)
       && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
   {
     Assert(!val.isDecision(fact));
@@ -277,7 +278,7 @@ void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
    * in BitblastMode::EAGER and therefore add all variables from the
    * bit-blaster to `termSet`.
    */
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     d_bitblaster->computeRelevantTerms(termSet);
   }
@@ -303,7 +304,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m,
 
   // In eager bitblast mode we also have to collect the model values for
   // Boolean variables in the CNF stream.
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     NodeManager* nm = NodeManager::currentNM();
     std::vector<TNode> vars;
@@ -327,7 +328,7 @@ bool BVSolverBitblast::collectModelValues(TheoryModel* m,
 
 void BVSolverBitblast::initSatSolver()
 {
-  switch (options::bvSatSolver())
+  switch (options().bv.bvSatSolver)
   {
     case options::SatSolverMode::CRYPTOMINISAT:
       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 3f4ab5025..e8931acff 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -42,7 +42,8 @@ class BBRegistrar;
 class BVSolverBitblast : public BVSolver
 {
  public:
-  BVSolverBitblast(TheoryState* state,
+  BVSolverBitblast(Env& env,
+                   TheoryState* state,
                    TheoryInferenceManager& inferMgr,
                    ProofNodeManager* pnm);
   ~BVSolverBitblast() = default;
diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
index 1b606a0e9..71a29f472 100644
--- a/src/theory/bv/bv_solver_bitblast_internal.cpp
+++ b/src/theory/bv/bv_solver_bitblast_internal.cpp
@@ -68,8 +68,11 @@ void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
 }  // namespace
 
 BVSolverBitblastInternal::BVSolverBitblastInternal(
-    TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
-    : BVSolver(*s, inferMgr),
+    Env& env,
+    TheoryState* s,
+    TheoryInferenceManager& inferMgr,
+    ProofNodeManager* pnm)
+    : BVSolver(env, *s, inferMgr),
       d_pnm(pnm),
       d_bitblaster(new BBProof(s, pnm, false))
 {
diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h
index 2fc7173d1..cc365e109 100644
--- a/src/theory/bv/bv_solver_bitblast_internal.h
+++ b/src/theory/bv/bv_solver_bitblast_internal.h
@@ -37,7 +37,8 @@ namespace bv {
 class BVSolverBitblastInternal : public BVSolver
 {
  public:
-  BVSolverBitblastInternal(TheoryState* state,
+  BVSolverBitblastInternal(Env& env,
+                           TheoryState* state,
                            TheoryInferenceManager& inferMgr,
                            ProofNodeManager* pnm);
   ~BVSolverBitblastInternal() = default;
diff --git a/src/theory/bv/bv_solver_layered.cpp b/src/theory/bv/bv_solver_layered.cpp
index 40daf1cb4..bf76ed2f9 100644
--- a/src/theory/bv/bv_solver_layered.cpp
+++ b/src/theory/bv/bv_solver_layered.cpp
@@ -38,11 +38,12 @@ namespace theory {
 namespace bv {
 
 BVSolverLayered::BVSolverLayered(TheoryBV& bv,
+                                 Env& env,
                                  context::Context* c,
                                  context::UserContext* u,
                                  ProofNodeManager* pnm,
                                  std::string name)
-    : BVSolver(bv.d_state, bv.d_im),
+    : BVSolver(env, bv.d_state, bv.d_im),
       d_bv(bv),
       d_context(c),
       d_alreadyPropagatedSet(c),
@@ -61,32 +62,32 @@ BVSolverLayered::BVSolverLayered(TheoryBV& bv,
       d_abstractionModule(new AbstractionModule(getStatsPrefix(THEORY_BV))),
       d_calledPreregister(false)
 {
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
     return;
   }
 
-  if (options::bitvectorEqualitySolver())
+  if (options().bv.bitvectorEqualitySolver)
   {
     d_subtheories.emplace_back(new CoreSolver(c, this));
     d_subtheoryMap[SUB_CORE] = d_subtheories.back().get();
   }
 
-  if (options::bitvectorInequalitySolver())
+  if (options().bv.bitvectorInequalitySolver)
   {
     d_subtheories.emplace_back(new InequalitySolver(c, u, this));
     d_subtheoryMap[SUB_INEQUALITY] = d_subtheories.back().get();
   }
 
-  if (options::bitvectorAlgebraicSolver())
+  if (options().bv.bitvectorAlgebraicSolver)
   {
     d_subtheories.emplace_back(new AlgebraicSolver(c, this));
     d_subtheoryMap[SUB_ALGEBRAIC] = d_subtheories.back().get();
   }
 
   BitblastSolver* bb_solver = new BitblastSolver(c, this);
-  if (options::bvAbstraction())
+  if (options().bv.bvAbstraction)
   {
     bb_solver->setAbstraction(d_abstractionModule.get());
   }
@@ -141,7 +142,7 @@ void BVSolverLayered::preRegisterTerm(TNode node)
   Debug("bitvector-preregister")
       << "BVSolverLayered::preRegister(" << node << ")" << std::endl;
 
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     // the aig bit-blaster option is set heuristically
     // if bv abstraction is used
@@ -235,7 +236,7 @@ void BVSolverLayered::check(Theory::Effort e)
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true);
   // if we are using the eager solver
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     // this can only happen on an empty benchmark
     if (!d_eagerSolver->isInitialized())
@@ -322,7 +323,7 @@ bool BVSolverLayered::collectModelValues(TheoryModel* m,
                                          const std::set<Node>& termSet)
 {
   Assert(!inConflict());
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     if (!d_eagerSolver->collectModelInfo(m, true))
     {
@@ -355,7 +356,7 @@ Node BVSolverLayered::getModelValue(TNode var)
 void BVSolverLayered::propagate(Theory::Effort e)
 {
   Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl;
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     return;
   }
@@ -394,15 +395,15 @@ TrustNode BVSolverLayered::ppRewrite(TNode t)
 {
   Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
   Node res = t;
-  if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t))
+  if (options().bv.bitwiseEq && RewriteRule<BitwiseEq>::applies(t))
   {
     Node result = RewriteRule<BitwiseEq>::run<false>(t);
-    res = Rewriter::rewrite(result);
+    res = rewrite(result);
   }
   else if (RewriteRule<UltAddOne>::applies(t))
   {
     Node result = RewriteRule<UltAddOne>::run<false>(t);
-    res = Rewriter::rewrite(result);
+    res = rewrite(result);
   }
   else if (res.getKind() == kind::EQUAL
            && ((res[0].getKind() == kind::BITVECTOR_ADD
@@ -419,7 +420,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t)
     Node rewr_eq = RewriteRule<SolveEq>::run<true>(new_eq);
     if (rewr_eq[0].isVar() || rewr_eq[1].isVar())
     {
-      res = Rewriter::rewrite(rewr_eq);
+      res = rewrite(rewr_eq);
     }
     else
     {
@@ -451,7 +452,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t)
   //   if (RewriteRule<MultSlice>::applies(mult)) {
   //     Node new_mult = RewriteRule<MultSlice>::run<false>(mult);
   //     Node new_eq =
-  //     Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
+  //     rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL,
   //     new_mult, add));
 
   //     // the simplification can cause the formula to blow up
@@ -475,7 +476,7 @@ TrustNode BVSolverLayered::ppRewrite(TNode t)
   //   }
   // }
 
-  if (options::bvAbstraction() && t.getType().isBoolean())
+  if (options().bv.bvAbstraction && t.getType().isBoolean())
   {
     d_abstractionModule->addInputAtom(res);
   }
@@ -595,9 +596,9 @@ void BVSolverLayered::notifySharedTerm(TNode t)
 
 EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
 {
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
     return EQUALITY_UNKNOWN;
-  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
+  Assert(options().bv.bitblastMode == options::BitblastMode::LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i)
   {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
@@ -665,8 +666,8 @@ bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
 {
   bool changed =
       d_abstractionModule->applyAbstraction(assertions, new_assertions);
-  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
-      && options::bitvectorAig())
+  if (changed && options().bv.bitblastMode == options::BitblastMode::EAGER
+      && options().bv.bitvectorAig)
   {
     // disable AIG mode
     AlwaysAssert(!d_eagerSolver->isInitialized());
@@ -678,7 +679,7 @@ bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
 
 void BVSolverLayered::setConflict(Node conflict)
 {
-  if (options::bvAbstraction())
+  if (options().bv.bvAbstraction)
   {
     NodeManager* const nm = NodeManager::currentNM();
     Node new_conflict = d_abstractionModule->simplifyConflict(conflict);
diff --git a/src/theory/bv/bv_solver_layered.h b/src/theory/bv/bv_solver_layered.h
index 023ff5a46..325f2fc72 100644
--- a/src/theory/bv/bv_solver_layered.h
+++ b/src/theory/bv/bv_solver_layered.h
@@ -58,6 +58,7 @@ class BVSolverLayered : public BVSolver
 
  public:
   BVSolverLayered(TheoryBV& bv,
+                  Env& env,
                   context::Context* c,
                   context::UserContext* u,
                   ProofNodeManager* pnm = nullptr,
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7493a54c7..96eccea57 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -43,20 +43,22 @@ TheoryBV::TheoryBV(Env& env,
       d_invalidateModelCache(context(), true),
       d_stats("theory::bv::")
 {
-  switch (options::bvSolver())
+  switch (options().bv.bvSolver)
   {
     case options::BVSolver::BITBLAST:
-      d_internal.reset(new BVSolverBitblast(&d_state, d_im, d_pnm));
+      d_internal.reset(new BVSolverBitblast(d_env, &d_state, d_im, d_pnm));
       break;
 
     case options::BVSolver::LAYERED:
-      d_internal.reset(
-          new BVSolverLayered(*this, context(), userContext(), d_pnm, name));
+      d_internal.reset(new BVSolverLayered(
+          *this, d_env, context(), userContext(), d_pnm, name));
       break;
 
     default:
-      AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
-      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, d_pnm));
+      AlwaysAssert(options().bv.bvSolver
+                   == options::BVSolver::BITBLAST_INTERNAL);
+      d_internal.reset(
+          new BVSolverBitblastInternal(d_env, &d_state, d_im, d_pnm));
   }
   d_theoryState = &d_state;
   d_inferManager = &d_im;
@@ -68,7 +70,7 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
 
 ProofRuleChecker* TheoryBV::getProofChecker()
 {
-  if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL)
+  if (options().bv.bvSolver == options::BVSolver::BITBLAST_INTERNAL)
   {
     return static_cast<BVSolverBitblastInternal*>(d_internal.get())
         ->getProofChecker();
@@ -222,7 +224,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(
      * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
      * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
      */
-    Node node = Rewriter::rewrite(in);
+    Node node = rewrite(in);
     if ((node[0].getKind() == kind::BITVECTOR_EXTRACT && node[1].isConst())
         || (node[1].getKind() == kind::BITVECTOR_EXTRACT
             && node[0].isConst()))
@@ -391,7 +393,7 @@ Node TheoryBV::getValue(TNode node)
         Assert(iit->second.isConst());
         nb << iit->second;
       }
-      it->second = Rewriter::rewrite(nb.constructNode());
+      it->second = rewrite(nb.constructNode());
     }
   } while (!visit.empty());