diff options
| -rw-r--r-- | src/theory/bv/bitblaster_template.h | 5 | ||||
| -rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 10 | ||||
| -rw-r--r-- | src/theory/theory.h | 5 | ||||
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bug733.smt2 | 8 |
5 files changed, 24 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()) { diff --git a/src/theory/theory.h b/src/theory/theory.h index d50d6b3f9..445d184e4 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -734,6 +734,11 @@ public: return !d_facts.empty(); } + /** Return total number of facts asserted to this theory */ + size_t numAssertions() { + return d_facts.size(); + } + typedef context::CDList<TNode>::const_iterator shared_terms_iterator; /** diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 0f41c22ec..da537bdae 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -117,6 +117,7 @@ BUG_TESTS = \ bug260a.smt \ bug260b.smt \ bug440.smt \ + bug733.smt2 \ bug734.smt2 \ bug_extract_mult_leading_bit.smt2 diff --git a/test/regress/regress0/bv/bug733.smt2 b/test/regress/regress0/bv/bug733.smt2 new file mode 100644 index 000000000..02ef85d82 --- /dev/null +++ b/test/regress/regress0/bv/bug733.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic QF_BV) +(declare-fun x2 () (_ BitVec 3)) +(declare-fun x1 () (_ BitVec 3)) +(declare-fun x0 () (_ BitVec 3)) +(assert (not (bvult (bvudiv (bvudiv (bvudiv x0 x0) x1) x2) x1))) +(assert (= #b000 x2)) +(check-sat) |