bv: Rename simple solver to bitblast-internal. (#6888)

16 files changed, 54 insertions, 50 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e001dd462..8dc1f986f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -589,10 +589,10 @@ libcvc5_add_sources(
   theory/bv/bv_solver.h
   theory/bv/bv_solver_bitblast.cpp
   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_simple.cpp
-  theory/bv/bv_solver_simple.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 8d4c2b1de..3faf9a111 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -220,9 +220,9 @@ name   = "Bitvector Theory"
 [[option.mode.LAZY]]
   name = "lazy"
   help = "Enables the lazy BV solver infrastructure."
-[[option.mode.SIMPLE]]
-  name = "simple"
-  help = "Enables simple bitblasting solver with proof support."
+[[option.mode.BITBLAST_INTERNAL]]
+  name = "bitblast-internal"
+  help = "Enables bitblasting to internal SAT solver with proof support."
 
 [[option]]
   name       = "bvAssertInput"
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
index 414de41ce..bd47cc45e 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_bitblast_internal.cpp
@@ -10,10 +10,11 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Simple bit-blast solver that sends bitblast lemmas directly to MiniSat.
+ * Bit-blast solver that sends bit-blast lemmas directly to the internal
+ * MiniSat.
  */
 
-#include "theory/bv/bv_solver_simple.h"
+#include "theory/bv/bv_solver_bitblast_internal.h"
 
 #include "proof/conv_proof_generator.h"
 #include "theory/bv/theory_bv.h"
@@ -66,16 +67,15 @@ void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
 
 }  // namespace
 
-BVSolverSimple::BVSolverSimple(TheoryState* s,
-                               TheoryInferenceManager& inferMgr,
-                               ProofNodeManager* pnm)
+BVSolverBitblastInternal::BVSolverBitblastInternal(
+    TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
     : BVSolver(*s, inferMgr),
       d_pnm(pnm),
       d_bitblaster(new BBProof(s, pnm, false))
 {
 }
 
-void BVSolverSimple::addBBLemma(TNode fact)
+void BVSolverBitblastInternal::addBBLemma(TNode fact)
 {
   if (!d_bitblaster->hasBBAtom(fact))
   {
@@ -88,17 +88,17 @@ void BVSolverSimple::addBBLemma(TNode fact)
 
   if (d_pnm == nullptr)
   {
-    d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
+    d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
   }
   else
   {
     TrustNode tlem =
         TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
-    d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
+    d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
   }
 }
 
-bool BVSolverSimple::preNotifyFact(
+bool BVSolverBitblastInternal::preNotifyFact(
     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 {
   if (fact.getKind() == kind::NOT)
@@ -119,7 +119,7 @@ bool BVSolverSimple::preNotifyFact(
 
     if (d_pnm == nullptr)
     {
-      d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA);
+      d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
     }
     else
     {
@@ -127,7 +127,7 @@ bool BVSolverSimple::preNotifyFact(
           fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
       TrustNode tlem =
           TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
-      d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
+      d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
     }
 
     std::unordered_set<Node> bv_atoms;
@@ -141,13 +141,16 @@ bool BVSolverSimple::preNotifyFact(
   return true;
 }
 
-bool BVSolverSimple::collectModelValues(TheoryModel* m,
-                                        const std::set<Node>& termSet)
+bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
+                                                  const std::set<Node>& termSet)
 {
   return d_bitblaster->collectModelValues(m, termSet);
 }
 
-BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; }
+BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
+{
+  return &d_checker;
+}
 
 }  // namespace bv
 }  // namespace theory
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_bitblast_internal.h
index 0af4f5b89..8a1886084 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_bitblast_internal.h
@@ -10,39 +10,37 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
+ * Bit-blast solver that sends bit-blast lemmas directly to the internal
+ * MiniSat.
  */
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
-#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
+#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H
 
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"
 
 namespace cvc5 {
-
-class TConvProofGenerator;
-
 namespace theory {
 namespace bv {
 
 /**
- * Simple bit-blasting solver that sends bit-blasting lemmas directly to the
+ * Bit-blasting solver that sends bit-blasting lemmas directly to the
  * internal MiniSat. It is also ablo to handle atoms of kind
  * BITVECTOR_EAGER_ATOM.
  *
  * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact().
  */
-class BVSolverSimple : public BVSolver
+class BVSolverBitblastInternal : public BVSolver
 {
  public:
-  BVSolverSimple(TheoryState* state,
-                 TheoryInferenceManager& inferMgr,
-                 ProofNodeManager* pnm);
-  ~BVSolverSimple() = default;
+  BVSolverBitblastInternal(TheoryState* state,
+                           TheoryInferenceManager& inferMgr,
+                           ProofNodeManager* pnm);
+  ~BVSolverBitblastInternal() = default;
 
   void preRegisterTerm(TNode n) override {}
 
@@ -52,7 +50,7 @@ class BVSolverSimple : public BVSolver
                      bool isPrereg,
                      bool isInternal) override;
 
-  std::string identify() const override { return "BVSolverSimple"; };
+  std::string identify() const override { return "BVSolverBitblastInternal"; };
 
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 3d7f11f6d..b3cf6da59 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -20,8 +20,8 @@
 #include "proof/proof_checker.h"
 #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_simple.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 #include "theory/trust_substitutions.h"
@@ -56,8 +56,8 @@ TheoryBV::TheoryBV(context::Context* c,
       break;
 
     default:
-      AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE);
-      d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm));
+      AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL);
+      d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm));
   }
   d_theoryState = &d_state;
   d_inferManager = &d_im;
@@ -69,9 +69,10 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; }
 
 ProofRuleChecker* TheoryBV::getProofChecker()
 {
-  if (options::bvSolver() == options::BVSolver::SIMPLE)
+  if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL)
   {
-    return static_cast<BVSolverSimple*>(d_internal.get())->getProofChecker();
+    return static_cast<BVSolverBitblastInternal*>(d_internal.get())
+        ->getProofChecker();
   }
   return nullptr;
 }
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index 0ef0ad6bd..612c99d82 100644
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -112,8 +112,10 @@ const char* toString(InferenceId i)
     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_SIMPLE_LEMMA: return "BV_SIMPLE_LEMMA";
-    case InferenceId::BV_SIMPLE_BITBLAST_LEMMA: return "BV_SIMPLE_BITBLAST_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_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 ba268b396..ebbccfd54 100644
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -175,8 +175,8 @@ enum class InferenceId
   BV_BITBLAST_CONFLICT,
   BV_LAZY_CONFLICT,
   BV_LAZY_LEMMA,
-  BV_SIMPLE_LEMMA,
-  BV_SIMPLE_BITBLAST_LEMMA,
+  BV_BITBLAST_INTERNAL_EAGER_LEMMA,
+  BV_BITBLAST_INTERNAL_BITBLAST_LEMMA,
   BV_EXTF_LEMMA,
   BV_EXTF_COLLAPSE,
   // ---------------------------------- end bitvector theory
diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2
index 579e438a5..f70dc4a3d 100644
--- a/test/regress/regress0/bv/ackermann1.smt2
+++ b/test/regress/regress0/bv/ackermann1.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models 
-; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models 
+; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal --no-check-models 
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2
index f30dbef6f..2a2998b35 100644
--- a/test/regress/regress0/bv/bool-model.smt2
+++ b/test/regress/regress0/bv/bool-model.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bitblast=eager
-; COMMAND-LINE: --bitblast=eager --bv-solver=simple
+; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal
 (set-info :status sat)
 (set-logic QF_BV)
 (declare-fun x () Bool)
diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2
index de0ec8897..09fcb4e11 100644
--- a/test/regress/regress0/bv/bool-to-bv-ite.smt2
+++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --bool-to-bv=ite
-; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple
+; COMMAND-LINE: --bool-to-bv=ite --bv-solver=bitblast-internal
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun x2 () (_ BitVec 3))
diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2
index 5e92036ec..0e392d3c6 100644
--- a/test/regress/regress0/bv/bug734.smt2
+++ b/test/regress/regress0/bv/bug734.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --incremental
-; COMMAND-LINE: --incremental --bv-solver=simple
+; COMMAND-LINE: --incremental --bv-solver=bitblast-internal
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic QF_BV)
diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2
index e94779439..12bc3e4ca 100644
--- a/test/regress/regress0/bv/issue-4076.smt2
+++ b/test/regress/regress0/bv/issue-4076.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE: --incremental
-; COMMAND-LINE: --incremental --bv-solver=simple
+; COMMAND-LINE: --incremental --bv-solver=bitblast-internal
 ; EXPECT: sat
 ; EXPECT: sat
 (set-logic ALL)
diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
index 0c6e7e0eb..2a924dac8 100644
--- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
+++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE:
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 (set-logic QF_BV)
 (set-info :status unsat)
 (declare-const x (_ BitVec 4))
diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
index 98d75d74f..8cb717258 100644
--- a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
+++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const __ (_ BitVec 3))
diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2
index 7095ec942..877389184 100644
--- a/test/regress/regress0/proofs/open-pf-rederivation.smt2
+++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-const __ (_ BitVec 7))
diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2
index cfafc0a0a..238fec914 100644
--- a/test/regress/regress1/bug520.smt2
+++ b/test/regress/regress1/bug520.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --bitblast=lazy
 ; COMMAND-LINE: --bitblast=eager --no-check-models
-; COMMAND-LINE: --bv-solver=simple
+; COMMAND-LINE: --bv-solver=bitblast-internal
 ; EXPECT: sat
 ; Automatically generated by SBV. Do not edit.
 (set-logic QF_UFBV)