From 9154e647013e4575f60807d5b73582bccfd052e2 Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 16 May 2012 16:18:52 +0000 Subject: equality status for bitvectors can now look into the sat solver to check for IN_MODEL status --- src/theory/bv/bitblaster.cpp | 66 ++++++++++++++++++++++++++++-------------- src/theory/bv/bitblaster.h | 9 ++++-- src/theory/bv/bv_subtheory.cpp | 4 +++ src/theory/bv/bv_subtheory.h | 12 ++------ src/theory/bv/theory_bv.cpp | 7 ++++- 5 files changed, 63 insertions(+), 35 deletions(-) diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 6b59b9b00..d512847d5 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -110,31 +110,19 @@ void Bitblaster::bbAtom(TNode node) { void Bitblaster::bbTerm(TNode node, Bits& bits) { + if (hasBBTerm(node)) { getBBTerm(node, bits); return; } + BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; ++d_statistics.d_numTerms; - Node optimized = bbOptimize(node); - - // if we already bitblasted the optimized version - if(hasBBTerm(optimized)) { - getBBTerm(optimized, bits); - // cache it as the same for this node - cacheTermDef(node, bits); - return; - } - - d_termBBStrategies[optimized.getKind()] (optimized, bits,this); + d_termBBStrategies[node.getKind()] (node, bits,this); - Assert (bits.size() == utils::getSize(node) && - bits.size() == utils::getSize(optimized)); + Assert (bits.size() == utils::getSize(node)); - if(optimized != node) { - cacheTermDef(optimized, bits); - } cacheTermDef(node, bits); } @@ -306,7 +294,7 @@ void Bitblaster::initTermBBStrategies() { } -bool Bitblaster::hasBBAtom(TNode atom) { +bool Bitblaster::hasBBAtom(TNode atom) const { return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end(); } @@ -315,15 +303,14 @@ void Bitblaster::cacheTermDef(TNode term, Bits def) { d_termCache[term] = def; } -bool Bitblaster::hasBBTerm(TNode node) { +bool Bitblaster::hasBBTerm(TNode node) const { return d_termCache.find(node) != d_termCache.end(); } -void Bitblaster::getBBTerm(TNode node, Bits& bits) { - +void Bitblaster::getBBTerm(TNode node, Bits& bits) const { Assert (hasBBTerm(node)); // copy? - bits = d_termCache[node]; + bits = d_termCache.find(node)->second; } Bitblaster::Statistics::Statistics() : @@ -366,6 +353,43 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { } }; +EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) { + + // 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); + EqualityStatus status = 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])) { + SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]); + SatValue a_lit_value = d_satSolver->value(a_lit); + if (a_lit_value != SAT_VALUE_UNKNOWN) { + SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]); + SatValue b_lit_value = d_satSolver->value(b_lit); + if (b_lit_value != SAT_VALUE_UNKNOWN) { + if (a_lit_value != b_lit_value) { + return EQUALITY_FALSE_IN_MODEL; + } + } else { + status = EQUALITY_UNKNOWN; + } + } { + status = EQUALITY_UNKNOWN; + } + } else { + status = EQUALITY_UNKNOWN; + } + } + + return status; + + } else { + return EQUALITY_UNKNOWN; + } +} } /*bv namespace */ } /* theory namespace */ diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index 6de84fc01..b27415e0b 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -33,6 +33,7 @@ #include "context/cdhashset.h" #include "context/cdlist.h" +#include "theory/theory.h" #include "theory_bv_utils.h" #include "util/stats.h" #include "bitblast_strategies.h" @@ -99,10 +100,10 @@ class Bitblaster { /// helper methods public: - bool hasBBAtom(TNode node); + bool hasBBAtom(TNode node) const; private: - bool hasBBTerm(TNode node); - void getBBTerm(TNode node, Bits& bits); + bool hasBBTerm(TNode node) const; + void getBBTerm(TNode node, Bits& bits) const; /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; @@ -132,6 +133,8 @@ public: void getConflict(std::vector& conflict); void explain(TNode atom, std::vector& explanation); + EqualityStatus getEqualityStatus(TNode a, TNode b); + private: diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp index f55d231b2..502d59f8d 100644 --- a/src/theory/bv/bv_subtheory.cpp +++ b/src/theory/bv/bv_subtheory.cpp @@ -114,6 +114,10 @@ bool BitblastSolver::addAssertions(const std::vector& assertions, Theory: return true; } +EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { + return d_bitblaster->getEqualityStatus(a, b); +} + EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_notify(bv), diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index cc62013fd..db7bad30c 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -68,9 +68,7 @@ public: /** * BitblastSolver - * */ - class BitblastSolver : public SubtheorySolver { /** Bitblaster */ @@ -86,14 +84,13 @@ public: void preRegister(TNode node); bool addAssertions(const std::vector& assertions, Theory::Effort e); void explain(TNode literal, std::vector& assumptions); + EqualityStatus getEqualityStatus(TNode a, TNode b); }; /** * EqualitySolver - * */ - class EqualitySolver : public SubtheorySolver { // NotifyClass: handles call-back from congruence closure module @@ -107,7 +104,7 @@ class EqualitySolver : public SubtheorySolver { bool eqNotifyTriggerPredicate(TNode predicate, bool value); bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); bool eqNotifyConstantTermMerge(TNode t1, TNode t2); - }; +}; /** The notify class for d_equalityEngine */ @@ -140,11 +137,6 @@ public: }; -// class CoreSolver : public SubtheorySolver { - -// }; - - } } } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 26452e5e8..79ab955aa 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -296,6 +296,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) return EQUALITY_UNKNOWN; } - return d_equalitySolver.getEqualityStatus(a, b); + EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b); + if (status == EQUALITY_UNKNOWN) { + status = d_bitblastSolver.getEqualityStatus(a, b); + } + + return status; } -- cgit v1.2.3