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 7dd3fd3e79928723ea6c08116beb2bc91d12fbba..27a48875d86da7f4e9001a7ac237b8a0acfb0e09 100644 (file)
--- 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 6a89a0f7cc661c315323e52ef5b1314aede323be..b17cd6ebcad498813b8709968afb22bd3c908f9c 100644 (file)
--- 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 c4d419d835cda47bf910567d82dfd4df0458a00f..d19378f72cd2ce62bb0bb883e2deeb7dd90ba289 100644 (file)
--- 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) {