diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 5 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 10 |
2 files changed, 10 insertions, 5 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index aa5ae9c16..8a7ccf8c6 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -161,7 +161,10 @@ class TLazyBitblaster : public TBitblaster<Node> { AbstractionModule* d_abstraction; bool d_emptyNotify; - context::CDO<bool> d_satSolverFullModel; + // The size of the fact queue when we most recently called solve() in the + // bit-vector SAT solver. This is the level at which we should have + // a full model in the bv SAT solver. + context::CDO<int> d_fullModelAssertionLevel; void addAtom(TNode atom); bool hasValue(TNode a); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 1477f183e..e89cacb40 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -45,7 +45,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, , d_bbAtoms() , d_abstraction(NULL) , d_emptyNotify(emptyNotify) - , d_satSolverFullModel(c, false) + , d_fullModelAssertionLevel(c, 0) , d_name(name) , d_statistics(name) { @@ -290,7 +290,7 @@ bool TLazyBitblaster::solve() { } } Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; - d_satSolverFullModel.set(true); + d_fullModelAssertionLevel.set(d_bv->numAssertions()); return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } @@ -393,8 +393,9 @@ void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) { EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { + int numAssertions = d_bv->numAssertions(); Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n"; - Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n"; + Debug("bv-equality-status")<< "BVSatSolver has full model? " << (d_fullModelAssertionLevel.get() == numAssertions) <<"\n"; // First check if it trivially rewrites to false/true Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b)); @@ -402,8 +403,9 @@ EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - if (!d_satSolverFullModel.get()) + if (d_fullModelAssertionLevel.get() != numAssertions) { return theory::EQUALITY_UNKNOWN; + } // Check if cache is valid (invalidated in check and pops) if (d_bv->d_invalidateModelCache.get()) { |