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

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e001dd462c29e13501c9e462d505c0fa978b10fe..8dc1f986fa6a1f7d323794a45897fd6be74c3fe9 100644 (file)
--- 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 8d4c2b1de77baf71b12f2907e0de26d5bd3c3b66..3faf9a11123f1ddd92f64a418dfdd76e8905fe43 100644 (file)
--- 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_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
new file mode 100644 (file)
index 0000000..bd47cc4
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast_internal.cpp
@@ -0,0 +1,157 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, Gereon Kremer, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Bit-blast solver that sends bit-blast lemmas directly to the internal
+ * MiniSat.
+ */
+
+#include "theory/bv/bv_solver_bitblast_internal.h"
+
+#include "proof/conv_proof_generator.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/theory_model.h"
+
+namespace cvc5 {
+namespace theory {
+namespace bv {
+
+/* -------------------------------------------------------------------------- */
+
+namespace {
+
+bool isBVAtom(TNode n)
+{
+  return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
+         || n.getKind() == kind::BITVECTOR_ULT
+         || n.getKind() == kind::BITVECTOR_ULE
+         || n.getKind() == kind::BITVECTOR_SLT
+         || n.getKind() == kind::BITVECTOR_SLE;
+}
+
+/* Traverse Boolean nodes and collect BV atoms. */
+void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
+{
+  std::vector<TNode> visit;
+  std::unordered_set<TNode> visited;
+
+  visit.push_back(n);
+
+  do
+  {
+    TNode cur = visit.back();
+    visit.pop_back();
+
+    if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
+      continue;
+
+    visited.insert(cur);
+    if (isBVAtom(cur))
+    {
+      atoms.insert(cur);
+      continue;
+    }
+
+    visit.insert(visit.end(), cur.begin(), cur.end());
+  } while (!visit.empty());
+}
+
+}  // namespace
+
+BVSolverBitblastInternal::BVSolverBitblastInternal(
+    TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
+    : BVSolver(*s, inferMgr),
+      d_pnm(pnm),
+      d_bitblaster(new BBProof(s, pnm, false))
+{
+}
+
+void BVSolverBitblastInternal::addBBLemma(TNode fact)
+{
+  if (!d_bitblaster->hasBBAtom(fact))
+  {
+    d_bitblaster->bbAtom(fact);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+
+  Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
+  Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
+
+  if (d_pnm == nullptr)
+  {
+    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_BITBLAST_INTERNAL_BITBLAST_LEMMA);
+  }
+}
+
+bool BVSolverBitblastInternal::preNotifyFact(
+    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+{
+  if (fact.getKind() == kind::NOT)
+  {
+    fact = fact[0];
+  }
+
+  if (isBVAtom(fact))
+  {
+    addBBLemma(fact);
+  }
+  else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
+  {
+    TNode n = fact[0];
+
+    NodeManager* nm = NodeManager::currentNM();
+    Node lemma = nm->mkNode(kind::EQUAL, fact, n);
+
+    if (d_pnm == nullptr)
+    {
+      d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
+    }
+    else
+    {
+      d_bitblaster->getProofGenerator()->addRewriteStep(
+          fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
+      TrustNode tlem =
+          TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
+      d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
+    }
+
+    std::unordered_set<Node> bv_atoms;
+    collectBVAtoms(n, bv_atoms);
+    for (const Node& nn : bv_atoms)
+    {
+      addBBLemma(nn);
+    }
+  }
+
+  return true;
+}
+
+bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
+                                                  const std::set<Node>& termSet)
+{
+  return d_bitblaster->collectModelValues(m, termSet);
+}
+
+BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
+{
+  return &d_checker;
+}
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5

diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h
new file mode 100644 (file)
index 0000000..8a18860
--- /dev/null
+++ b/src/theory/bv/bv_solver_bitblast_internal.h
@@ -0,0 +1,80 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Mathias Preiner, Haniel Barbosa, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Bit-blast solver that sends bit-blast lemmas directly to the internal
+ * MiniSat.
+ */
+
+#include "cvc5_private.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 {
+namespace theory {
+namespace bv {
+
+/**
+ * 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 BVSolverBitblastInternal : public BVSolver
+{
+ public:
+  BVSolverBitblastInternal(TheoryState* state,
+                           TheoryInferenceManager& inferMgr,
+                           ProofNodeManager* pnm);
+  ~BVSolverBitblastInternal() = default;
+
+  void preRegisterTerm(TNode n) override {}
+
+  bool preNotifyFact(TNode atom,
+                     bool pol,
+                     TNode fact,
+                     bool isPrereg,
+                     bool isInternal) override;
+
+  std::string identify() const override { return "BVSolverBitblastInternal"; };
+
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
+
+  /** get the proof checker of this theory */
+  BVProofRuleChecker* getProofChecker();
+
+ private:
+  /**
+   * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
+   * inference manager.
+   */
+  void addBBLemma(TNode fact);
+
+  /** Proof node manager. */
+  ProofNodeManager* d_pnm;
+  /** Bit-blaster used to bit-blast atoms/terms. */
+  std::unique_ptr<BBProof> d_bitblaster;
+  /** Proof rule checker */
+  BVProofRuleChecker d_checker;
+};
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace cvc5
+
+#endif

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
deleted file mode 100644 (file)
index 414de41..0000000
--- a/src/theory/bv/bv_solver_simple.cpp
+++ /dev/null
@@ -1,154 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Gereon Kremer, Haniel Barbosa
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Simple bit-blast solver that sends bitblast lemmas directly to MiniSat.
- */
-
-#include "theory/bv/bv_solver_simple.h"
-
-#include "proof/conv_proof_generator.h"
-#include "theory/bv/theory_bv.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/theory_model.h"
-
-namespace cvc5 {
-namespace theory {
-namespace bv {
-
-/* -------------------------------------------------------------------------- */
-
-namespace {
-
-bool isBVAtom(TNode n)
-{
-  return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
-         || n.getKind() == kind::BITVECTOR_ULT
-         || n.getKind() == kind::BITVECTOR_ULE
-         || n.getKind() == kind::BITVECTOR_SLT
-         || n.getKind() == kind::BITVECTOR_SLE;
-}
-
-/* Traverse Boolean nodes and collect BV atoms. */
-void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
-{
-  std::vector<TNode> visit;
-  std::unordered_set<TNode> visited;
-
-  visit.push_back(n);
-
-  do
-  {
-    TNode cur = visit.back();
-    visit.pop_back();
-
-    if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
-      continue;
-
-    visited.insert(cur);
-    if (isBVAtom(cur))
-    {
-      atoms.insert(cur);
-      continue;
-    }
-
-    visit.insert(visit.end(), cur.begin(), cur.end());
-  } while (!visit.empty());
-}
-
-}  // namespace
-
-BVSolverSimple::BVSolverSimple(TheoryState* s,
-                               TheoryInferenceManager& inferMgr,
-                               ProofNodeManager* pnm)
-    : BVSolver(*s, inferMgr),
-      d_pnm(pnm),
-      d_bitblaster(new BBProof(s, pnm, false))
-{
-}
-
-void BVSolverSimple::addBBLemma(TNode fact)
-{
-  if (!d_bitblaster->hasBBAtom(fact))
-  {
-    d_bitblaster->bbAtom(fact);
-  }
-  NodeManager* nm = NodeManager::currentNM();
-
-  Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
-  Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
-
-  if (d_pnm == nullptr)
-  {
-    d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
-  }
-  else
-  {
-    TrustNode tlem =
-        TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
-    d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_LEMMA);
-  }
-}
-
-bool BVSolverSimple::preNotifyFact(
-    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
-{
-  if (fact.getKind() == kind::NOT)
-  {
-    fact = fact[0];
-  }
-
-  if (isBVAtom(fact))
-  {
-    addBBLemma(fact);
-  }
-  else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
-  {
-    TNode n = fact[0];
-
-    NodeManager* nm = NodeManager::currentNM();
-    Node lemma = nm->mkNode(kind::EQUAL, fact, n);
-
-    if (d_pnm == nullptr)
-    {
-      d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA);
-    }
-    else
-    {
-      d_bitblaster->getProofGenerator()->addRewriteStep(
-          fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
-      TrustNode tlem =
-          TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
-      d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_LEMMA);
-    }
-
-    std::unordered_set<Node> bv_atoms;
-    collectBVAtoms(n, bv_atoms);
-    for (const Node& nn : bv_atoms)
-    {
-      addBBLemma(nn);
-    }
-  }
-
-  return true;
-}
-
-bool BVSolverSimple::collectModelValues(TheoryModel* m,
-                                        const std::set<Node>& termSet)
-{
-  return d_bitblaster->collectModelValues(m, termSet);
-}
-
-BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; }
-
-}  // namespace bv
-}  // namespace theory
-}  // namespace cvc5

diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
deleted file mode 100644 (file)
index 0af4f5b..0000000
--- a/src/theory/bv/bv_solver_simple.h
+++ /dev/null
@@ -1,82 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Mathias Preiner, Haniel Barbosa, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat.
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
-#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_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
- * 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
-{
- public:
-  BVSolverSimple(TheoryState* state,
-                 TheoryInferenceManager& inferMgr,
-                 ProofNodeManager* pnm);
-  ~BVSolverSimple() = default;
-
-  void preRegisterTerm(TNode n) override {}
-
-  bool preNotifyFact(TNode atom,
-                     bool pol,
-                     TNode fact,
-                     bool isPrereg,
-                     bool isInternal) override;
-
-  std::string identify() const override { return "BVSolverSimple"; };
-
-  bool collectModelValues(TheoryModel* m,
-                          const std::set<Node>& termSet) override;
-
-  /** get the proof checker of this theory */
-  BVProofRuleChecker* getProofChecker();
-
- private:
-  /**
-   * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the
-   * inference manager.
-   */
-  void addBBLemma(TNode fact);
-
-  /** Proof node manager. */
-  ProofNodeManager* d_pnm;
-  /** Bit-blaster used to bit-blast atoms/terms. */
-  std::unique_ptr<BBProof> d_bitblaster;
-  /** Proof rule checker */
-  BVProofRuleChecker d_checker;
-};
-
-}  // namespace bv
-}  // namespace theory
-}  // namespace cvc5
-
-#endif

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 3d7f11f6d2cbcbe5a91782c7f595e3eef55a1eba..b3cf6da590e9d5ddb1c303e44399d6f090c13c29 100644 (file)
--- 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 0ef0ad6bd5ef089998b019407f58cad0a2e58bca..612c99d8275e740616f0b265a28610dcd77c439a 100644 (file)
--- 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 ba268b39684ac3e34c8e59c6fb4f262511a4b842..ebbccfd548be20eacc7e731a493a5496d7235c48 100644 (file)
--- 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 579e438a56082b70f224848c7229e97307430171..f70dc4a3d05e22ac26d78393ce72f2d40502e33d 100644 (file)
--- 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 f30dbef6f07657d7f1fc650e423c4f7cb38ad1d2..2a2998b35b71ffcc168670ce56a8f1358771d08b 100644 (file)
--- 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 de0ec889741d6e666e9fac3d77595ec86a1ce298..09fcb4e11878f82853cf4a4a24753735b82a7f59 100644 (file)
--- 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 5e92036ecb6252807707f96b97e46d7d206cb3c3..0e392d3c6a45a843d79f8c7b6a03dbd08d0d66c2 100644 (file)
--- 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 e94779439570ab7f0a0f77616e77a883a68b1e7e..12bc3e4ca07e3621372fec77085c720e0946a696 100644 (file)
--- 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 0c6e7e0eb2c14224bd768e65a918e90e0f3baa16..2a924dac89c0f9a2adb07b74d3a9363fc7e349e0 100644 (file)
--- 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 98d75d74f67210be6ec7a1b5cc1c6c30401ba02a..8cb7172585bf91de54b149d975c75e7cd7bad438 100644 (file)
--- 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 7095ec9427a7295e0909efa16d222754ba97fc1b..8773891847e20a5fd7712c29879a18eb05f64676 100644 (file)
--- 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 cfafc0a0a5326282a5638f9b8fd2e57bc0af90de..238fec9141aab22829085a11fcb0a570823f1c19 100644 (file)
--- 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)