From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 1 Aug 2018 00:51:15 +0000 (-0700)
Subject: Remove hasAssertions() method from eager BV solver. (#2239)
X-Git-Tag: cvc5-1.0.0~4843
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=049bc7acdb7ecc50719175652028a51a8f996502;p=cvc5.git

Remove hasAssertions() method from eager BV solver. (#2239)
---

diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 7dd3fd3e7..27a48875d 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -122,17 +122,6 @@ bool EagerBitblastSolver::checkSat() {
   return d_bitblaster->solve();
 }
 
-bool EagerBitblastSolver::hasAssertions(const std::vector<TNode>& formulas) {
-  Assert(isInitialized());
-  if (formulas.size() != d_assertionSet.size()) return false;
-  for (unsigned i = 0; i < formulas.size(); ++i) {
-    Assert(formulas[i].getKind() == kind::BITVECTOR_EAGER_ATOM);
-    TNode formula = formulas[i][0];
-    if (d_assertionSet.find(formula) == d_assertionSet.end()) return false;
-  }
-  return true;
-}
-
 bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 {
   AlwaysAssert(!d_useAig && d_bitblaster);
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 6a89a0f7c..b17cd6ebc 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -42,8 +42,6 @@ class EagerBitblastSolver {
   ~EagerBitblastSolver();
   bool checkSat();
   void assertFormula(TNode formula);
-  // purely for debugging purposes
-  bool hasAssertions(const std::vector<TNode>& formulas);
 
   void turnOffAig();
   bool isInitialized();
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c4d419d83..d19378f72 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -346,7 +346,6 @@ void TheoryBV::check(Effort e)
       assertions.push_back(fact);
       d_eagerSolver->assertFormula(fact[0]);
     }
-    Assert (d_eagerSolver->hasAssertions(assertions));
 
     bool ok = d_eagerSolver->checkSat();
     if (!ok) {