From 049bc7acdb7ecc50719175652028a51a8f996502 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 31 Jul 2018 17:51:15 -0700 Subject: [PATCH] Remove hasAssertions() method from eager BV solver. (#2239) --- src/theory/bv/bv_eager_solver.cpp | 11 ----------- src/theory/bv/bv_eager_solver.h | 2 -- src/theory/bv/theory_bv.cpp | 1 - 3 files changed, 14 deletions(-) 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& 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& 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) { -- 2.30.2