bv: Rename lazy solver to layered solver. (#6889)

26 files changed, 139 insertions, 130 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8dc1f986f..015f00f8f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -591,8 +591,8 @@ libcvc5_add_sources(
   theory/bv/bv_solver_bitblast.h
   theory/bv/bv_solver_bitblast_internal.cpp
   theory/bv/bv_solver_bitblast_internal.h
-  theory/bv/bv_solver_lazy.cpp
-  theory/bv/bv_solver_lazy.h
+  theory/bv/bv_solver_layered.cpp
+  theory/bv/bv_solver_layered.h
   theory/bv/bv_subtheory.h
   theory/bv/bv_subtheory_algebraic.cpp
   theory/bv/bv_subtheory_algebraic.h
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 3faf9a111..05ea7f512 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -66,7 +66,7 @@ name   = "Bitvector Theory"
   long       = "bv-eq-solver"
   type       = "bool"
   default    = "true"
-  help       = "use the equality engine for the bit-vector theory (only if --bitblast=lazy)"
+  help       = "use the equality engine for the bit-vector theory (only if --bv-solver=layered)"
 
 [[option]]
   name       = "bitvectorInequalitySolver"
@@ -74,7 +74,7 @@ name   = "Bitvector Theory"
   long       = "bv-inequality-solver"
   type       = "bool"
   default    = "true"
-  help       = "turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy)"
+  help       = "turn on the inequality solver for the bit-vector theory (only if --bv-solver=layered)"
 
 [[option]]
   name       = "bitvectorAlgebraicSolver"
@@ -82,7 +82,7 @@ name   = "Bitvector Theory"
   long       = "bv-algebraic-solver"
   type       = "bool"
   default    = "false"
-  help       = "turn on experimental algebraic solver for the bit-vector theory (only if --bitblast=lazy)"
+  help       = "turn on experimental algebraic solver for the bit-vector theory (only if --bv-solver=layered)"
 
 [[option]]
   name       = "bitvectorAlgebraicBudget"
@@ -217,12 +217,12 @@ name   = "Bitvector Theory"
 [[option.mode.BITBLAST]]
   name = "bitblast"
   help = "Enables bitblasting solver."
-[[option.mode.LAZY]]
-  name = "lazy"
-  help = "Enables the lazy BV solver infrastructure."
 [[option.mode.BITBLAST_INTERNAL]]
   name = "bitblast-internal"
   help = "Enables bitblasting to internal SAT solver with proof support."
+[[option.mode.LAYERED]]
+  name = "layered"
+  help = "Enables the layered BV solver."
 
 [[option]]
   name       = "bvAssertInput"
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 55ed6c41d..dd3a3e9ce 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -23,7 +23,7 @@
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
@@ -31,7 +31,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
+EagerBitblaster::EagerBitblaster(BVSolverLayered* theory_bv,
+                                 context::Context* c)
     : TBitblaster<Node>(),
       d_context(c),
       d_satSolver(),
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 9e5ace9d8..71bf50dd0 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -30,12 +30,12 @@ namespace theory {
 namespace bv {
 
 class BitblastingRegistrar;
-class BVSolverLazy;
+class BVSolverLayered;
 
 class EagerBitblaster : public TBitblaster<Node>
 {
  public:
-  EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context);
+  EagerBitblaster(BVSolverLayered* theory_bv, context::Context* context);
   ~EagerBitblaster();
 
   void addAtom(TNode atom);
@@ -60,7 +60,7 @@ class EagerBitblaster : public TBitblaster<Node>
   std::unique_ptr<prop::SatSolver> d_satSolver;
   std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
 
-  BVSolverLazy* d_bv;
+  BVSolverLayered* d_bv;
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 6a5372e04..3eb2eebe7 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Bitblaster for the lazy bv solver.
+ * Bitblaster for the layered BV solver.
  */
 
 #include "theory/bv/bitblast/lazy_bitblaster.h"
@@ -23,7 +23,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/abstraction.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
@@ -58,7 +58,7 @@ uint64_t numNodes(TNode node, utils::NodeSet& seen)
 }
 
 TLazyBitblaster::TLazyBitblaster(context::Context* c,
-                                 bv::BVSolverLazy* bv,
+                                 bv::BVSolverLayered* bv,
                                  const std::string name,
                                  bool emptyNotify)
     : TBitblaster<Node>(),
@@ -294,10 +294,10 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
   }
 
   Debug("bitvector-bb")
-      << "BVSolverLazy::TLazyBitblaster::assertToSat asserting node: " << atom
-      << "\n";
+      << "BVSolverLayered::TLazyBitblaster::assertToSat asserting node: "
+      << atom << "\n";
   Debug("bitvector-bb")
-      << "BVSolverLazy::TLazyBitblaster::assertToSat with literal:   "
+      << "BVSolverLayered::TLazyBitblaster::assertToSat with literal:   "
       << markerLit << "\n";
 
   prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
@@ -404,9 +404,9 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
       lemmab << d_cnf->getNode(clause[i]);
     }
     Node lemma = lemmab;
-    d_bv->d_im.lemma(lemma, InferenceId::BV_LAZY_LEMMA);
+    d_bv->d_im.lemma(lemma, InferenceId::BV_LAYERED_LEMMA);
   } else {
-    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAZY_LEMMA);
+    d_bv->d_im.lemma(d_cnf->getNode(clause[0]), InferenceId::BV_LAYERED_LEMMA);
   }
 }
 
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 15cbe1558..8d8723522 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -33,7 +33,7 @@ class NullRegistrat;
 namespace theory {
 namespace bv {
 
-class BVSolverLazy;
+class BVSolverLayered;
 
 class TLazyBitblaster : public TBitblaster<Node>
 {
@@ -46,7 +46,7 @@ class TLazyBitblaster : public TBitblaster<Node>
   bool hasBBAtom(TNode atom) const override;
 
   TLazyBitblaster(context::Context* c,
-                  BVSolverLazy* bv,
+                  BVSolverLayered* bv,
                   const std::string name = "",
                   bool emptyNotify = false);
   ~TLazyBitblaster();
@@ -109,11 +109,13 @@ class TLazyBitblaster : public TBitblaster<Node>
   class MinisatNotify : public prop::BVSatSolverNotify
   {
     prop::CnfStream* d_cnf;
-    BVSolverLazy* d_bv;
+    BVSolverLayered* d_bv;
     TLazyBitblaster* d_lazyBB;
 
    public:
-    MinisatNotify(prop::CnfStream* cnf, BVSolverLazy* bv, TLazyBitblaster* lbv)
+    MinisatNotify(prop::CnfStream* cnf,
+                  BVSolverLayered* bv,
+                  TLazyBitblaster* lbv)
         : d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
     {
     }
@@ -124,7 +126,7 @@ class TLazyBitblaster : public TBitblaster<Node>
     void safePoint(Resource r) override;
   };
 
-  BVSolverLazy* d_bv;
+  BVSolverLayered* d_bv;
   context::Context* d_ctx;
 
   std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index b0082b992..23b98ca54 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -27,7 +27,8 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-EagerBitblastSolver::EagerBitblastSolver(context::Context* c, BVSolverLazy* bv)
+EagerBitblastSolver::EagerBitblastSolver(context::Context* c,
+                                         BVSolverLayered* bv)
     : d_assertionSet(c),
       d_assumptionSet(c),
       d_context(c),
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index ab51ea844..fec4edee9 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -19,7 +19,7 @@
 #define CVC5__THEORY__BV__BV_EAGER_SOLVER_H
 
 #include "expr/node.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/theory_model.h"
 
 namespace cvc5 {
@@ -34,7 +34,7 @@ class AigBitblaster;
  */
 class EagerBitblastSolver {
  public:
-  EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLazy* bv);
+  EagerBitblastSolver(context::Context* c, theory::bv::BVSolverLayered* bv);
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
@@ -54,7 +54,7 @@ class EagerBitblastSolver {
   std::unique_ptr<AigBitblaster> d_aigBitblaster;
   bool d_useAig;
 
-  BVSolverLazy* d_bv;
+  BVSolverLayered* d_bv;
 };  // class EagerBitblastSolver
 
 }  // namespace bv
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 5d3e99253..dd9c1849d 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -17,7 +17,7 @@
 
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bitblast/lazy_bitblaster.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace cvc5::prop;
@@ -27,7 +27,7 @@ namespace theory {
 namespace bv {
 
 BVQuickCheck::BVQuickCheck(const std::string& name,
-                           theory::bv::BVSolverLazy* bv)
+                           theory::bv::BVSolverLayered* bv)
     : d_ctx(),
       d_bitblaster(new TLazyBitblaster(&d_ctx, bv, name, true)),
       d_conflict(),
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index d1411d784..b8274ce80 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -35,7 +35,7 @@ class TheoryModel;
 namespace bv {
 
 class TLazyBitblaster;
-class BVSolverLazy;
+class BVSolverLayered;
 
 class BVQuickCheck
 {
@@ -46,7 +46,7 @@ class BVQuickCheck
   void setConflict();
 
  public:
-  BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv);
+  BVQuickCheck(const std::string& name, theory::bv::BVSolverLayered* bv);
   ~BVQuickCheck();
   bool inConflict();
   Node getConflict() { return d_conflict; }
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_layered.cpp
index 5210117b8..40daf1cb4 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_layered.cpp
@@ -10,10 +10,10 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Lazy bit-vector solver.
+ * Layered bit-vector solver.
  */
 
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 
 #include "expr/node_algorithm.h"
 #include "options/bv_options.h"
@@ -37,11 +37,11 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BVSolverLazy::BVSolverLazy(TheoryBV& bv,
-                           context::Context* c,
-                           context::UserContext* u,
-                           ProofNodeManager* pnm,
-                           std::string name)
+BVSolverLayered::BVSolverLayered(TheoryBV& bv,
+                                 context::Context* c,
+                                 context::UserContext* u,
+                                 ProofNodeManager* pnm,
+                                 std::string name)
     : BVSolver(bv.d_state, bv.d_im),
       d_bv(bv),
       d_context(c),
@@ -94,9 +94,9 @@ BVSolverLazy::BVSolverLazy(TheoryBV& bv,
   d_subtheoryMap[SUB_BITBLAST] = bb_solver;
 }
 
-BVSolverLazy::~BVSolverLazy() {}
+BVSolverLayered::~BVSolverLayered() {}
 
-bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi)
+bool BVSolverLayered::needsEqualityEngine(EeSetupInfo& esi)
 {
   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
   if (core)
@@ -107,7 +107,7 @@ bool BVSolverLazy::needsEqualityEngine(EeSetupInfo& esi)
   return false;
 }
 
-void BVSolverLazy::finishInit()
+void BVSolverLayered::finishInit()
 {
   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
   if (core)
@@ -117,12 +117,9 @@ void BVSolverLazy::finishInit()
   }
 }
 
-void BVSolverLazy::spendResource(Resource r)
-{
-  d_im.spendResource(r);
-}
+void BVSolverLayered::spendResource(Resource r) { d_im.spendResource(r); }
 
-BVSolverLazy::Statistics::Statistics()
+BVSolverLayered::Statistics::Statistics()
     : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
         "theory::bv::lazy::AvgBVConflictSize")),
       d_solveTimer(smtStatisticsRegistry().registerTimer(
@@ -138,11 +135,11 @@ BVSolverLazy::Statistics::Statistics()
 {
 }
 
-void BVSolverLazy::preRegisterTerm(TNode node)
+void BVSolverLayered::preRegisterTerm(TNode node)
 {
   d_calledPreregister = true;
   Debug("bitvector-preregister")
-      << "BVSolverLazy::preRegister(" << node << ")" << std::endl;
+      << "BVSolverLayered::preRegister(" << node << ")" << std::endl;
 
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
@@ -171,7 +168,7 @@ void BVSolverLazy::preRegisterTerm(TNode node)
   // d_bv.d_extTheory->registerTermRec( node );
 }
 
-void BVSolverLazy::sendConflict()
+void BVSolverLayered::sendConflict()
 {
   Assert(d_conflict);
   if (d_conflictNode.isNull())
@@ -180,15 +177,15 @@ void BVSolverLazy::sendConflict()
   }
   else
   {
-    Debug("bitvector") << indent() << "BVSolverLazy::check(): conflict "
+    Debug("bitvector") << indent() << "BVSolverLayered::check(): conflict "
                        << d_conflictNode << std::endl;
-    d_im.conflict(d_conflictNode, InferenceId::BV_LAZY_CONFLICT);
+    d_im.conflict(d_conflictNode, InferenceId::BV_LAYERED_CONFLICT);
     d_statistics.d_avgConflictSize << d_conflictNode.getNumChildren();
     d_conflictNode = Node::null();
   }
 }
 
-void BVSolverLazy::checkForLemma(TNode fact)
+void BVSolverLayered::checkForLemma(TNode fact)
 {
   if (fact.getKind() == kind::EQUAL)
   {
@@ -220,20 +217,20 @@ void BVSolverLazy::checkForLemma(TNode fact)
   }
 }
 
-bool BVSolverLazy::preCheck(Theory::Effort e)
+bool BVSolverLayered::preCheck(Theory::Effort e)
 {
   check(e);
   return true;
 }
 
-void BVSolverLazy::check(Theory::Effort e)
+void BVSolverLayered::check(Theory::Effort e)
 {
   if (done() && e < Theory::EFFORT_FULL)
   {
     return;
   }
 
-  Debug("bitvector") << "BVSolverLazy::check(" << e << ")" << std::endl;
+  Debug("bitvector") << "BVSolverLayered::check(" << e << ")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true);
@@ -261,11 +258,11 @@ void BVSolverLazy::check(Theory::Effort e)
     {
       if (assertions.size() == 1)
       {
-        d_im.conflict(assertions[0], InferenceId::BV_LAZY_CONFLICT);
+        d_im.conflict(assertions[0], InferenceId::BV_LAYERED_CONFLICT);
         return;
       }
       Node conflict = utils::mkAnd(assertions);
-      d_im.conflict(conflict, InferenceId::BV_LAZY_CONFLICT);
+      d_im.conflict(conflict, InferenceId::BV_LAYERED_CONFLICT);
       return;
     }
     return;
@@ -321,8 +318,8 @@ void BVSolverLazy::check(Theory::Effort e)
   }
 }
 
-bool BVSolverLazy::collectModelValues(TheoryModel* m,
-                                      const std::set<Node>& termSet)
+bool BVSolverLayered::collectModelValues(TheoryModel* m,
+                                         const std::set<Node>& termSet)
 {
   Assert(!inConflict());
   if (options::bitblastMode() == options::BitblastMode::EAGER)
@@ -342,7 +339,7 @@ bool BVSolverLazy::collectModelValues(TheoryModel* m,
   return true;
 }
 
-Node BVSolverLazy::getModelValue(TNode var)
+Node BVSolverLayered::getModelValue(TNode var)
 {
   Assert(!inConflict());
   for (unsigned i = 0; i < d_subtheories.size(); ++i)
@@ -355,9 +352,9 @@ Node BVSolverLazy::getModelValue(TNode var)
   Unreachable();
 }
 
-void BVSolverLazy::propagate(Theory::Effort e)
+void BVSolverLayered::propagate(Theory::Effort e)
 {
-  Debug("bitvector") << indent() << "BVSolverLazy::propagate()" << std::endl;
+  Debug("bitvector") << indent() << "BVSolverLayered::propagate()" << std::endl;
   if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     return;
@@ -378,7 +375,7 @@ void BVSolverLazy::propagate(Theory::Effort e)
     if (d_state.isSatLiteral(literal))
     {
       Debug("bitvector::propagate")
-          << "BVSolverLazy:: propagating " << literal << "\n";
+          << "BVSolverLayered:: propagating " << literal << "\n";
       ok = d_im.propagateLit(literal);
     }
   }
@@ -386,15 +383,16 @@ void BVSolverLazy::propagate(Theory::Effort e)
   if (!ok)
   {
     Debug("bitvector::propagate")
-        << indent() << "BVSolverLazy::propagate(): conflict from theory engine"
+        << indent()
+        << "BVSolverLayered::propagate(): conflict from theory engine"
         << std::endl;
     setConflict();
   }
 }
 
-TrustNode BVSolverLazy::ppRewrite(TNode t)
+TrustNode BVSolverLayered::ppRewrite(TNode t)
 {
-  Debug("bv-pp-rewrite") << "BVSolverLazy::ppRewrite " << t << "\n";
+  Debug("bv-pp-rewrite") << "BVSolverLayered::ppRewrite " << t << "\n";
   Node res = t;
   if (options::bitwiseEq() && RewriteRule<BitwiseEq>::applies(t))
   {
@@ -489,25 +487,26 @@ TrustNode BVSolverLazy::ppRewrite(TNode t)
   return TrustNode::null();
 }
 
-void BVSolverLazy::presolve()
+void BVSolverLayered::presolve()
 {
-  Debug("bitvector") << "BVSolverLazy::presolve" << std::endl;
+  Debug("bitvector") << "BVSolverLayered::presolve" << std::endl;
 }
 
 static int prop_count = 0;
 
-bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory)
+bool BVSolverLayered::storePropagation(TNode literal, SubTheory subtheory)
 {
-  Debug("bitvector::propagate") << indent() << d_context->getLevel() << " "
-                                << "BVSolverLazy::storePropagation(" << literal
-                                << ", " << subtheory << ")" << std::endl;
+  Debug("bitvector::propagate")
+      << indent() << d_context->getLevel() << " "
+      << "BVSolverLayered::storePropagation(" << literal << ", " << subtheory
+      << ")" << std::endl;
   prop_count++;
 
   // If already in conflict, no more propagation
   if (d_conflict)
   {
     Debug("bitvector::propagate")
-        << indent() << "BVSolverLazy::storePropagation(" << literal << ", "
+        << indent() << "BVSolverLayered::storePropagation(" << literal << ", "
         << subtheory << "): already in conflict" << std::endl;
     return false;
   }
@@ -552,19 +551,19 @@ bool BVSolverLazy::storePropagation(TNode literal, SubTheory subtheory)
   }
   return ok;
 
-} /* BVSolverLazy::propagate(TNode) */
+} /* BVSolverLayered::propagate(TNode) */
 
-void BVSolverLazy::explain(TNode literal, std::vector<TNode>& assumptions)
+void BVSolverLayered::explain(TNode literal, std::vector<TNode>& assumptions)
 {
   Assert(wasPropagatedBySubtheory(literal));
   SubTheory sub = getPropagatingSubtheory(literal);
   d_subtheoryMap[sub]->explain(literal, assumptions);
 }
 
-TrustNode BVSolverLazy::explain(TNode node)
+TrustNode BVSolverLayered::explain(TNode node)
 {
   Debug("bitvector::explain")
-      << "BVSolverLazy::explain(" << node << ")" << std::endl;
+      << "BVSolverLayered::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
@@ -580,20 +579,21 @@ TrustNode BVSolverLazy::explain(TNode node)
     // return the explanation
     explanation = utils::mkAnd(assumptions);
   }
-  Debug("bitvector::explain") << "BVSolverLazy::explain(" << node << ") => "
+  Debug("bitvector::explain") << "BVSolverLayered::explain(" << node << ") => "
                               << explanation << std::endl;
-  Debug("bitvector::explain") << "BVSolverLazy::explain done. \n";
+  Debug("bitvector::explain") << "BVSolverLayered::explain done. \n";
   return TrustNode::mkTrustPropExp(node, explanation, nullptr);
 }
 
-void BVSolverLazy::notifySharedTerm(TNode t)
+void BVSolverLayered::notifySharedTerm(TNode t)
 {
   Debug("bitvector::sharing")
-      << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl;
+      << indent() << "BVSolverLayered::notifySharedTerm(" << t << ")"
+      << std::endl;
   d_sharedTermsSet.insert(t);
 }
 
-EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
+EqualityStatus BVSolverLayered::getEqualityStatus(TNode a, TNode b)
 {
   if (options::bitblastMode() == options::BitblastMode::EAGER)
     return EQUALITY_UNKNOWN;
@@ -610,7 +610,7 @@ EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)
   ;
 }
 
-void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
+void BVSolverLayered::ppStaticLearn(TNode in, NodeBuilder& learned)
 {
   if (d_staticLearnCache.find(in) != d_staticLearnCache.end())
   {
@@ -660,8 +660,8 @@ void BVSolverLazy::ppStaticLearn(TNode in, NodeBuilder& learned)
   }
 }
 
-bool BVSolverLazy::applyAbstraction(const std::vector<Node>& assertions,
-                                    std::vector<Node>& new_assertions)
+bool BVSolverLayered::applyAbstraction(const std::vector<Node>& assertions,
+                                       std::vector<Node>& new_assertions)
 {
   bool changed =
       d_abstractionModule->applyAbstraction(assertions, new_assertions);
@@ -676,7 +676,7 @@ bool BVSolverLazy::applyAbstraction(const std::vector<Node>& assertions,
   return changed;
 }
 
-void BVSolverLazy::setConflict(Node conflict)
+void BVSolverLayered::setConflict(Node conflict)
 {
   if (options::bvAbstraction())
   {
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_layered.h
index 4f73354bc..023ff5a46 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_layered.h
@@ -10,13 +10,13 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Lazy bit-vector solver.
+ * Layered bit-vector solver.
  */
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H
-#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_LAYERED_H
+#define CVC5__THEORY__BV__BV_SOLVER_LAYERED_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -40,7 +40,7 @@ class BitblastSolver;
 class EagerBitblastSolver;
 class AbstractionModule;
 
-class BVSolverLazy : public BVSolver
+class BVSolverLayered : public BVSolver
 {
   /** Back reference to TheoryBV */
   TheoryBV& d_bv;
@@ -57,13 +57,13 @@ class BVSolverLazy : public BVSolver
       d_subtheoryMap;
 
  public:
-  BVSolverLazy(TheoryBV& bv,
-               context::Context* c,
-               context::UserContext* u,
-               ProofNodeManager* pnm = nullptr,
-               std::string name = "");
+  BVSolverLayered(TheoryBV& bv,
+                  context::Context* c,
+                  context::UserContext* u,
+                  ProofNodeManager* pnm = nullptr,
+                  std::string name = "");
 
-  ~BVSolverLazy();
+  ~BVSolverLayered();
 
   //--------------------------------- initialization
 
@@ -89,7 +89,10 @@ class BVSolverLazy : public BVSolver
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 
-  std::string identify() const override { return std::string("BVSolverLazy"); }
+  std::string identify() const override
+  {
+    return std::string("BVSolverLayered");
+  }
 
   TrustNode ppRewrite(TNode t) override;
 
@@ -197,7 +200,7 @@ class BVSolverLazy : public BVSolver
 
   void lemma(TNode node)
   {
-    d_im.lemma(node, InferenceId::BV_LAZY_LEMMA);
+    d_im.lemma(node, InferenceId::BV_LAYERED_LEMMA);
     d_lemmasAdded = true;
   }
 
@@ -218,7 +221,7 @@ class BVSolverLazy : public BVSolver
   friend class InequalitySolver;
   friend class AlgebraicSolver;
   friend class EagerBitblastSolver;
-}; /* class BVSolverLazy */
+}; /* class BVSolverLayered */
 
 }  // namespace bv
 }  // namespace theory
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 8a81a5ef8..6c887424a 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -54,7 +54,7 @@ inline std::ostream& operator<<(std::ostream& out, SubTheory subtheory) {
 }
 
 // forward declaration
-class BVSolverLazy;
+class BVSolverLayered;
 
 using AssertionQueue = context::CDQueue<Node>;
 
@@ -64,7 +64,7 @@ using AssertionQueue = context::CDQueue<Node>;
  */
 class SubtheorySolver {
  public:
-  SubtheorySolver(context::Context* c, BVSolverLazy* bv)
+  SubtheorySolver(context::Context* c, BVSolverLayered* bv)
       : d_context(c), d_bv(bv), d_assertionQueue(c), d_assertionIndex(c, 0)
   {
   }
@@ -99,7 +99,7 @@ class SubtheorySolver {
   context::Context* d_context;
 
   /** The bit-vector theory */
-  BVSolverLazy* d_bv;
+  BVSolverLayered* d_bv;
   AssertionQueue d_assertionQueue;
   context::CDO<uint32_t> d_assertionIndex;
 }; /* class SubtheorySolver */
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 65c1ec79c..d6e60d1f4 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -25,7 +25,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -232,7 +232,7 @@ void SubstitutionEx::storeCache(TNode from, TNode to, Node reason) {
   d_cache[from] = SubstitutionElement(to, reason);
 }
 
-AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLazy* bv)
+AlgebraicSolver::AlgebraicSolver(context::Context* c, BVSolverLayered* bv)
     : SubtheorySolver(c, bv),
       d_modelMap(),
       d_quickSolver(new BVQuickCheck("theory::bv::algebraic", bv)),
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index b93ff235f..16cf3d53b 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -222,7 +222,7 @@ class AlgebraicSolver : public SubtheorySolver
   bool quickCheck(std::vector<Node>& facts);
 
  public:
-  AlgebraicSolver(context::Context* c, BVSolverLazy* bv);
+  AlgebraicSolver(context::Context* c, BVSolverLayered* bv);
   ~AlgebraicSolver();
 
   void preRegister(TNode node) override {}
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index b86809a91..cdc2fc143 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -22,7 +22,7 @@
 #include "theory/bv/abstraction.h"
 #include "theory/bv/bitblast/lazy_bitblaster.h"
 #include "theory/bv/bv_quick_check.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
@@ -32,7 +32,7 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
+BitblastSolver::BitblastSolver(context::Context* c, BVSolverLayered* bv)
     : SubtheorySolver(c, bv),
       d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
       d_bitblastQueue(c),
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 439bd33ed..3ad707482 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -63,7 +63,7 @@ class BitblastSolver : public SubtheorySolver
   void setConflict(TNode conflict);
 
  public:
-  BitblastSolver(context::Context* c, BVSolverLazy* bv);
+  BitblastSolver(context::Context* c, BVSolverLayered* bv);
   ~BitblastSolver();
 
   void preRegister(TNode node) override;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index fa71641ad..3f3384257 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -19,7 +19,7 @@
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"
@@ -32,7 +32,7 @@ using namespace cvc5::theory;
 using namespace cvc5::theory::bv;
 using namespace cvc5::theory::bv::utils;
 
-CoreSolver::CoreSolver(context::Context* c, BVSolverLazy* bv)
+CoreSolver::CoreSolver(context::Context* c, BVSolverLayered* bv)
     : SubtheorySolver(c, bv),
       d_notify(*this),
       d_isComplete(c, true),
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 46c4559ea..2e6312144 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -74,7 +74,7 @@ class CoreSolver : public SubtheorySolver {
   bool d_checkCalled;
 
   /** Pointer to the parent theory solver that owns this */
-  BVSolverLazy* d_bv;
+  BVSolverLayered* d_bv;
   /** Pointer to the equality engine of the parent */
   eq::EqualityEngine* d_equalityEngine;
 
@@ -87,7 +87,7 @@ class CoreSolver : public SubtheorySolver {
   Statistics d_statistics;
 
  public:
-  CoreSolver(context::Context* c, BVSolverLazy* bv);
+  CoreSolver(context::Context* c, BVSolverLayered* bv);
   ~CoreSolver();
   bool needsEqualityEngine(EeSetupInfo& esi);
   void finishInit();
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index aa93008c2..3bd3e9c3e 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -17,7 +17,7 @@
 
 #include "options/smt_options.h"
 #include "smt/smt_statistics_registry.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index f8a7bf113..8a76a6bf1 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -62,7 +62,9 @@ class InequalitySolver : public SubtheorySolver
   Statistics d_statistics;
 
  public:
-  InequalitySolver(context::Context* c, context::Context* u, BVSolverLazy* bv)
+  InequalitySolver(context::Context* c,
+                   context::Context* u,
+                   BVSolverLayered* bv)
       : SubtheorySolver(c, bv),
         d_assertionSet(c),
         d_inequalityGraph(c, u),
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b3cf6da59..37881f9b2 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,7 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_bitblast.h"
 #include "theory/bv/bv_solver_bitblast_internal.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 #include "theory/trust_substitutions.h"
@@ -51,8 +51,8 @@ TheoryBV::TheoryBV(context::Context* c,
       d_internal.reset(new BVSolverBitblast(&d_state, d_im, pnm));
       break;
 
-    case options::BVSolver::LAZY:
-      d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name));
+    case options::BVSolver::LAYERED:
+      d_internal.reset(new BVSolverLayered(*this, c, u, pnm, name));
       break;
 
     default:
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index e884f621c..f2d6bb47e 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -34,9 +34,9 @@ class BVSolver;
 
 class TheoryBV : public Theory
 {
-  /* BVSolverLazy accesses methods from theory in a way that is deprecated and
-   * will be removed in the future. For now we allow direct access. */
-  friend class BVSolverLazy;
+  /* BVSolverLayered accesses methods from theory in a way that is deprecated
+   * and will be removed in the future. For now we allow direct access. */
+  friend class BVSolverLayered;
 
  public:
   TheoryBV(context::Context* c,
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 612c99d82..a26147f09 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -110,12 +110,12 @@ const char* toString(InferenceId i)
     case InferenceId::BAG_DUPLICATE_REMOVAL: return "BAG_DUPLICATE_REMOVAL";
 
     case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT";
-    case InferenceId::BV_LAZY_CONFLICT: return "BV_LAZY_CONFLICT";
-    case InferenceId::BV_LAZY_LEMMA: return "BV_LAZY_LEMMA";
     case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA:
       return "BV_BITBLAST_EAGER_LEMMA";
     case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA:
       return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA";
+    case InferenceId::BV_LAYERED_CONFLICT: return "BV_LAYERED_CONFLICT";
+    case InferenceId::BV_LAYERED_LEMMA: return "BV_LAYERED_LEMMA";
     case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA";
     case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE";
 
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index ebbccfd54..f32c80b68 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -173,10 +173,10 @@ enum class InferenceId
 
   // ---------------------------------- bitvector theory
   BV_BITBLAST_CONFLICT,
-  BV_LAZY_CONFLICT,
-  BV_LAZY_LEMMA,
   BV_BITBLAST_INTERNAL_EAGER_LEMMA,
   BV_BITBLAST_INTERNAL_BITBLAST_LEMMA,
+  BV_LAYERED_CONFLICT,
+  BV_LAYERED_LEMMA,
   BV_EXTF_LEMMA,
   BV_EXTF_COLLAPSE,
   // ---------------------------------- end bitvector theory
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 150320824..4cf695609 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "test_smt.h"
 #include "theory/bv/bitblast/eager_bitblaster.h"
-#include "theory/bv/bv_solver_lazy.h"
+#include "theory/bv/bv_solver_layered.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
@@ -45,7 +45,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
   d_smtEngine->setLogic("QF_BV");
 
   d_smtEngine->setOption("bitblast", "eager");
-  d_smtEngine->setOption("bv-solver", "lazy");
+  d_smtEngine->setOption("bv-solver", "layered");
   d_smtEngine->setOption("incremental", "false");
   // Notice that this unit test uses the theory engine of a created SMT
   // engine d_smtEngine. We must ensure that d_smtEngine is properly initialized
@@ -53,7 +53,7 @@ TEST_F(TestTheoryWhiteBv, bitblaster_core)
   d_smtEngine->finishInit();
   TheoryBV* tbv = dynamic_cast<TheoryBV*>(
       d_smtEngine->getTheoryEngine()->d_theoryTable[THEORY_BV]);
-  BVSolverLazy* bvsl = dynamic_cast<BVSolverLazy*>(tbv->d_internal.get());
+  BVSolverLayered* bvsl = dynamic_cast<BVSolverLayered*>(tbv->d_internal.get());
   std::unique_ptr<EagerBitblaster> bb(
       new EagerBitblaster(bvsl, d_smtEngine->getContext()));