diff options
author | lianah <lianahady@gmail.com> | 2014-08-15 19:46:06 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2014-08-18 23:14:48 -0400 |
commit | 866492a200cbbf069b6c3466e36c30ac13741ae3 (patch) | |
tree | ae0cb1a0761c8ff99f5380fada056d27446cb9ae /src/theory/bv/lazy_bitblaster.cpp | |
parent | 6bebe3957e98e1eba9621b03bfd129a5db441194 (diff) |
Making getEqualityStatus more powerful for bit-vector theory.
Diffstat (limited to 'src/theory/bv/lazy_bitblaster.cpp')
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 104 |
1 files changed, 53 insertions, 51 deletions
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index f721a22f0..101d8b082 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -41,6 +41,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st , d_bbAtoms() , d_abstraction(NULL) , d_emptyNotify(emptyNotify) + , d_satSolverFullModel(c, false) , d_name(name) , d_statistics(name) { d_satSolver = prop::SatSolverFactory::createMinisat(c, name); @@ -258,6 +259,7 @@ bool TLazyBitblaster::solve() { } } Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n"; + d_satSolverFullModel.set(true); return prop::SAT_VALUE_TRUE == d_satSolver->solve(); } @@ -354,42 +356,38 @@ void TLazyBitblaster::MinisatNotify::safePoint() { d_bv->d_out->safePoint(); } + EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) { + Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n"; + Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n"; - // We don't want to bit-blast every possibly expensive term for the sake of equality checking - if (hasBBTerm(a) && hasBBTerm(b)) { - - Bits a_bits, b_bits; - getBBTerm(a, a_bits); - getBBTerm(b, b_bits); - theory::EqualityStatus status = theory::EQUALITY_TRUE_IN_MODEL; - for (unsigned i = 0; i < a_bits.size(); ++ i) { - if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) { - prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); - prop::SatValue a_lit_value = d_satSolver->value(a_lit); - if (a_lit_value != prop::SAT_VALUE_UNKNOWN) { - prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); - prop::SatValue b_lit_value = d_satSolver->value(b_lit); - if (b_lit_value != prop::SAT_VALUE_UNKNOWN) { - if (a_lit_value != b_lit_value) { - return theory::EQUALITY_FALSE_IN_MODEL; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } { - status = theory::EQUALITY_UNKNOWN; - } - } else { - status = theory::EQUALITY_UNKNOWN; - } - } + // First check if it trivially rewrites to false/true + Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b)); - return status; + if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE; + if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE; - } else { - return theory::EQUALITY_UNKNOWN; + if (!d_satSolverFullModel.get()) + return theory::EQUALITY_UNKNOWN; + + // Check if cache is valid (invalidated in check and pops) + if (d_bv->d_invalidateModelCache.get()) { + invalidateModelCache(); } + d_bv->d_invalidateModelCache.set(false); + + Node a_value = getTermModel(a, true); + Node b_value = getTermModel(b, true); + + Assert (a_value.isConst() && + b_value.isConst()); + + if (a_value == b_value) { + Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n"; + return theory::EQUALITY_TRUE_IN_MODEL; + } + Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n"; + return theory::EQUALITY_FALSE_IN_MODEL; } @@ -424,11 +422,11 @@ bool TLazyBitblaster::hasValue(TNode a) { * * @return */ -Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { +Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { if (!hasBBTerm(a)) { - Assert(isSharedTerm(a)); - return Node(); + return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); } + Bits bits; getBBTerm(a, bits); Integer value(0); @@ -439,7 +437,8 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { bit_value = d_satSolver->value(bit); Assert (bit_value != prop::SAT_VALUE_UNKNOWN); } else { - // the bit is unconstrainted so we can give it an arbitrary value + if (!fullModel) return Node(); + // unconstrained bits default to false bit_value = prop::SAT_VALUE_FALSE; } Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0); @@ -449,23 +448,26 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) { } void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { - TNodeSet::iterator it = d_variables.begin(); - for (; it!= d_variables.end(); ++it) { + std::set<Node> termSet; + d_bv->computeRelevantTerms(termSet); + + for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { TNode var = *it; - if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) { - Node const_value = getVarValue(var, fullModel); - if(const_value == Node()) { - if( fullModel ){ - // if the value is unassigned just set it to zero - const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); - } - } - if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; + // not actually a leaf of the bit-vector theory + if (d_variables.find(var) == d_variables.end()) + continue; + + Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); + // only shared terms could not have been bit-blasted + Assert (hasBBTerm(var) || isSharedTerm(var)); + + Node const_value = getModelFromSatSolver(var, fullModel); + Assert (const_value.isNull() || const_value.isConst()); + if(const_value != Node()) { + Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " + << var << " " + << const_value << "))\n"; m->assertEquality(var, const_value, true); - } } } } @@ -481,7 +483,7 @@ void TLazyBitblaster::clearSolver() { d_bbAtoms.clear(); d_variables.clear(); d_termCache.clear(); - + // recreate sat solver d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, |