diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-05-08 21:54:55 +0000 |
commit | 8a0c0562cb8d0e26ea019ff782b25c1997a49a0b (patch) | |
tree | 28239db9bcb26b03d893ad61dd1a7ea099391fbe /src/theory/bv | |
parent | 5082cb8349efbb287084293cd4bc6c3fa5a34f26 (diff) |
Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_sat.cpp | 91 | ||||
-rw-r--r-- | src/theory/bv/bv_sat.h | 36 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 308 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 35 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 5 |
5 files changed, 248 insertions, 227 deletions
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index 2f4ac1324..dcb33c9af 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -23,7 +23,8 @@ #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" -#include "theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv_rewrite_rules_simplification.h" +#include "theory/bv/theory_bv.h" using namespace std; @@ -35,7 +36,6 @@ namespace CVC4 { namespace theory { namespace bv{ - std::string toString(Bits& bits) { ostringstream os; for (int i = bits.size() - 1; i >= 0; --i) { @@ -52,7 +52,8 @@ std::string toString(Bits& bits) { } /////// Bitblaster -Bitblaster::Bitblaster(context::Context* c) : +Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) : + d_bvOutput(bv->d_out), d_termCache(), d_bitblastedAtoms(), d_assertedAtoms(c), @@ -61,6 +62,8 @@ Bitblaster::Bitblaster(context::Context* c) : d_satSolver = prop::SatSolverFactory::createMinisat(c); d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar()); + MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv); + d_satSolver->setNotify(notify); // initializing the bit-blasting strategies initAtomBBStrategies(); initTermBBStrategies(); @@ -79,6 +82,8 @@ Bitblaster::~Bitblaster() { * */ void Bitblaster::bbAtom(TNode node) { + node = node.getKind() == kind::NOT? node[0] : node; + if (hasBBAtom(node)) { return; } @@ -94,8 +99,13 @@ void Bitblaster::bbAtom(TNode node) { Node atom_definition = mkNode(kind::IFF, node, atom_bb); // do boolean simplifications if possible Node rewritten = Rewriter::rewrite(atom_definition); - d_cnfStream->convertAndAssert(rewritten, true, false); - d_bitblastedAtoms.insert(node); + + if (!Options::current()->bitvector_eager_bitblast) { + d_cnfStream->convertAndAssert(rewritten, true, false); + d_bitblastedAtoms.insert(node); + } else { + d_bvOutput->lemma(rewritten, false); + } } @@ -154,65 +164,21 @@ Node Bitblaster::bbOptimize(TNode node) { /// Public methods void Bitblaster::addAtom(TNode atom) { - d_cnfStream->ensureLiteral(atom); - SatLiteral lit = d_cnfStream->getLiteral(atom); - d_satSolver->addMarkerLiteral(lit); -} -bool Bitblaster::getPropagations(std::vector<TNode>& propagations) { - std::vector<SatLiteral> propagated_literals; - if (d_satSolver->getPropagations(propagated_literals)) { - for (unsigned i = 0; i < propagated_literals.size(); ++i) { - propagations.push_back(d_cnfStream->getNode(propagated_literals[i])); - } - return true; + if (!Options::current()->bitvector_eager_bitblast) { + d_cnfStream->ensureLiteral(atom); + SatLiteral lit = d_cnfStream->getLiteral(atom); + d_satSolver->addMarkerLiteral(lit); } - return false; } -void Bitblaster::explainPropagation(TNode atom, std::vector<Node>& explanation) { +void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) { std::vector<SatLiteral> literal_explanation; - d_satSolver->explainPropagation(d_cnfStream->getLiteral(atom), literal_explanation); + d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation); for (unsigned i = 0; i < literal_explanation.size(); ++i) { explanation.push_back(d_cnfStream->getNode(literal_explanation[i])); } } -/** - * Called from preregistration bitblasts the node - * - * @param node - * - * @return - */ -void Bitblaster::bitblast(TNode node) { - TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer); - - /// strip the not - if (node.getKind() == kind::NOT) { - node = node[0]; - } - - if (node.getKind() == kind::EQUAL || - node.getKind() == kind::BITVECTOR_ULT || - node.getKind() == kind::BITVECTOR_ULE || - node.getKind() == kind::BITVECTOR_SLT || - node.getKind() == kind::BITVECTOR_SLE) - { - bbAtom(node); - } - else if (node.getKind() == kind::BITVECTOR_UGT || - node.getKind() == kind::BITVECTOR_UGE || - node.getKind() == kind::BITVECTOR_SGT || - node.getKind() == kind::BITVECTOR_SGE ) - { - Unhandled(node.getKind()); - } - else - { - Bits bits; - bbTerm(node, bits); - } -} /** * Asserts the clauses corresponding to the atom to the Sat Solver @@ -383,7 +349,22 @@ Bitblaster::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_bitblastTimer); } +bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) { + return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLASTER); +}; +void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { + if (clause.size() > 1) { + NodeBuilder<> lemmab(kind::OR); + for (unsigned i = 0; i < clause.size(); ++ i) { + lemmab << d_cnf->getNode(clause[i]); + } + Node lemma = lemmab; + d_bv->d_out->lemma(lemma); + } else { + d_bv->d_out->lemma(d_cnf->getNode(clause[0])); + } +}; } /*bv namespace */ diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 2422da0b7..7016879a0 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -47,22 +47,37 @@ class CnfStream; class BVSatSolverInterface; } - namespace theory { + +class OutputChannel; + namespace bv { +typedef std::vector<Node> Bits; std::string toString (Bits& bits); +class TheoryBV; + /** * The Bitblaster that manages the mapping between Nodes * and their bitwise definition * */ - -typedef std::vector<Node> Bits; - class Bitblaster { + + /** This class gets callbacks from minisat on propagations */ + class MinisatNotify : public prop::BVSatSolverInterface::Notify { + prop::CnfStream* d_cnf; + TheoryBV *d_bv; + public: + MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv) + : d_cnf(cnf) + , d_bv(bv) + {} + bool notify(prop::SatLiteral lit); + void notify(prop::SatClause& clause); + }; typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap; typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; @@ -71,6 +86,7 @@ class Bitblaster { typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); // sat solver used for bitblasting and associated CnfStream + theory::OutputChannel* d_bvOutput; prop::BVSatSolverInterface* d_satSolver; prop::CnfStream* d_cnfStream; @@ -88,9 +104,6 @@ class Bitblaster { bool hasBBTerm(TNode node); void getBBTerm(TNode node, Bits& bits); - - - /// function tables for the various bitblasting strategies indexed by node kind TermBBStrategy d_termBBStrategies[kind::LAST_KIND]; AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; @@ -102,7 +115,6 @@ class Bitblaster { // returns a node that might be easier to bitblast Node bbOptimize(TNode node); - void bbAtom(TNode node); void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface @@ -111,17 +123,15 @@ class Bitblaster { public: void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division void bbTerm(TNode node, Bits& bits); + void bbAtom(TNode node); -public: - Bitblaster(context::Context* c); + Bitblaster(context::Context* c, bv::TheoryBV* bv); ~Bitblaster(); bool assertToSat(TNode node, bool propagate = true); bool solve(bool quick_solve = false); - void bitblast(TNode node); void getConflict(std::vector<TNode>& conflict); + void explain(TNode atom, std::vector<TNode>& explanation); - bool getPropagations(std::vector<TNode>& propagations); - void explainPropagation(TNode atom, std::vector<Node>& explanation); private: diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index b6f12793d..c9d58574e 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -40,15 +40,17 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_assertions(c), - d_bitblaster(new Bitblaster(c) ), + d_bitblaster(new Bitblaster(c, this) ), d_alreadyPropagatedSet(c), d_statistics(), + d_sharedTermsSet(c), d_notify(*this), d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"), d_conflict(c, false), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), - d_toBitBlast(c) + d_toBitBlast(c), + d_propagatedBy(c) { d_true = utils::mkTrue(); d_false = utils::mkFalse(); @@ -58,6 +60,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_equalityEngine.addTerm(d_false); d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + // add disequality between 0 and 1 bits + d_equalityEngine.addDisequality(utils::mkConst(BitVector((unsigned)1, (unsigned)0)), + utils::mkConst(BitVector((unsigned)1, (unsigned)1)), + d_true); + // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); @@ -113,12 +120,18 @@ TheoryBV::Statistics::~Statistics() { void TheoryBV::preRegisterTerm(TNode node) { BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; + + if (Options::current()->bitvector_eager_bitblast) { + // don't use the equality engine in the eager bit-blasting + return; + } + if (node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT || node.getKind() == kind::BITVECTOR_ULE || node.getKind() == kind::BITVECTOR_SLT || node.getKind() == kind::BITVECTOR_SLE) { - d_bitblaster->bitblast(node); + d_bitblaster->bbAtom(node); } if (d_useEqualityEngine) { @@ -140,56 +153,56 @@ void TheoryBV::preRegisterTerm(TNode node) { void TheoryBV::check(Effort e) { - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl; + BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + + if (Options::current()->bitvector_eager_bitblast) { + while (!done()) { + Assertion assertion = get(); + TNode fact = assertion.assertion; + if (fact.getKind() == kind::NOT) { + if (fact[0].getKind() != kind::BITVECTOR_BITOF) { + d_bitblaster->bbAtom(fact[0]); + } + } else { + if (fact.getKind() != kind::BITVECTOR_BITOF) { + d_bitblaster->bbAtom(fact); + } + } + } + return; + } + while (!done() && !d_conflict) { Assertion assertion = get(); TNode fact = assertion.assertion; BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; - // If the assertion doesn't have a literal, it's a shared equality - bool shared = !assertion.isPreregistered; - Assert(!d_useEqualityEngine || !shared || - ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) || - (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL && - d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1])))); - - // Notify the Equality Engine - switch (fact.getKind()) { - case kind::EQUAL: - if (d_useEqualityEngine) { - d_equalityEngine.addEquality(fact[0], fact[1], fact); - } - if (shared && !d_bitblaster->hasBBAtom(fact)) { - d_bitblaster->bitblast(fact); - } - break; - case kind::NOT: - if (fact[0].getKind() == kind::EQUAL) { - // Assert the dis-equality - if (d_useEqualityEngine) { - d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact); - } - if (shared && !d_bitblaster->hasBBAtom(fact[0])) { - d_bitblaster->bitblast(fact[0]); - } + // Notify the equality engine + if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) { + bool negated = fact.getKind() == kind::NOT; + TNode predicate = negated ? fact[0] : fact; + if (predicate.getKind() == kind::EQUAL) { + if (negated) { + // dis-equality + d_equalityEngine.addDisequality(predicate[0], predicate[1], fact); } else { - if (d_useEqualityEngine) { - d_equalityEngine.addPredicate(fact[0], false, fact); - } - break; + // equality + d_equalityEngine.addEquality(predicate[0], predicate[1], fact); } - break; - default: - if (d_useEqualityEngine) { - d_equalityEngine.addPredicate(fact, true, fact); + } else { + // Adding predicate if the congruence over it is turned on + if (d_equalityEngine.isFunctionKind(predicate.getKind())) { + d_equalityEngine.addPredicate(predicate, !negated, fact); } - break; + } } - // make sure we do not assert things we propagated - if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) { + // Bit-blaster + if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) { + // Some atoms have not been bit-blasted yet + d_bitblaster->bbAtom(fact); + // Assert to sat bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation); if (!ok) { std::vector<TNode> conflictAtoms; @@ -204,17 +217,15 @@ void TheoryBV::check(Effort e) // If in conflict, output the conflict if (d_conflict) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl; + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); return; } - if (e == EFFORT_FULL) { - + if (e == EFFORT_FULL || Options::current()->bitvector_eager_fullcheck) { Assert(done() && !d_conflict); BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - // in standard effort we only do boolean constraint propagation - bool ok = d_bitblaster->solve(false); + bool ok = d_bitblaster->solve(); if (!ok) { std::vector<TNode> conflictAtoms; d_bitblaster->getConflict(conflictAtoms); @@ -225,7 +236,6 @@ void TheoryBV::check(Effort e) return; } } - } @@ -253,77 +263,55 @@ void TheoryBV::propagate(Effort e) { return; } - // get new propagations from the equality engine - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { + // go through stored propagations + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); + d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) + { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl; - bool satValue; Node normalized = Rewriter::rewrite(literal); - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - d_out->propagate(literal); - } else { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; - std::vector<TNode> assumptions; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } - explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; - return; - } - } - // get new propagations from the sat solver - std::vector<TNode> propagations; - d_bitblaster->getPropagations(propagations); - - // propagate the facts on the propagation queue - for (unsigned i = 0; i < propagations.size(); ++ i) { - TNode node = propagations[i]; - BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n"; - if (!d_valuation.isSatLiteral(node)) { - // TODO: maybe propagate shared terms too? - continue; - } - if (d_valuation.getSatValue(node) == Node::null()) { - vector<Node> explanation; - d_bitblaster->explainPropagation(node, explanation); - if (explanation.size() == 0) { - d_out->lemma(node); + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + // check if it's a shared equality in the current context + if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) || + (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && + d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) { + + bool satValue; + if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { + // check if we already propagated the negation + Node neg_literal = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); + if (d_alreadyPropagatedSet.find(neg_literal) != d_alreadyPropagatedSet.end()) { + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; + // we are in conflict + std::vector<TNode> assumptions; + explain(literal, assumptions); + explain(neg_literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return; + } + + BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl; + d_out->propagate(literal); + d_alreadyPropagatedSet.insert(literal); } else { - NodeBuilder<> nb(kind::OR); - nb << node; - for (unsigned i = 0; i < explanation.size(); ++ i) { - nb << explanation[i].notNode(); + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; + + Node negatedLiteral; + std::vector<TNode> assumptions; + if (normalized != d_false) { + negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); + assumptions.push_back(negatedLiteral); } - Node lemma = nb; - d_out->lemma(lemma); + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return; } - d_alreadyPropagatedSet.insert(node); } } - } -// Node TheoryBV::explain(TNode n) { -// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n"; -// std::vector<Node> explanation; -// d_bitblaster->explainPropagation(n, explanation); -// Node exp; - -// if (explanation.size() == 0) { -// return utils::mkTrue(); -// } - -// exp = utils::mkAnd(explanation); - -// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n"; -// return exp; -// } - Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { switch(in.getKind()) { case kind::EQUAL: @@ -351,42 +339,44 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu } -bool TheoryBV::propagate(TNode literal) +bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ")" << std::endl; // If already in conflict, no more propagation if (d_conflict) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl; + Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl; return false; } + // If propagated already, just skip + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find != d_propagatedBy.end()) { + //unsigned theories = (*find).second | (unsigned) subtheory; + //d_propagatedBy[literal] = theories; + return true; + } else { + d_propagatedBy[literal] = subtheory; + } + // See if the literal has been asserted already - Node normalized = Rewriter::rewrite(literal); bool satValue = false; - bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue); - + bool hasSatValue = d_valuation.hasSatValue(literal, satValue); // If asserted, we might be in conflict - if (isAsserted) { - if (!satValue) { - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl; + + if (hasSatValue && !satValue) { + Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl; std::vector<TNode> assumptions; - Node negatedLiteral; - if (normalized != d_false) { - negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); - assumptions.push_back(negatedLiteral); - } + Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); + assumptions.push_back(negatedLiteral); explain(literal, assumptions); d_conflictNode = mkAnd(assumptions); d_conflict = true; return false; - } - // Propagate even if already known in SAT - could be a new equation between shared terms - // (terms that weren't shared when the literal was asserted!) } // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl; + Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl; d_literalsToPropagate.push_back(literal); return true; @@ -394,46 +384,60 @@ bool TheoryBV::propagate(TNode literal) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { - TNode lhs, rhs; - switch (literal.getKind()) { - case kind::EQUAL: - lhs = literal[0]; - rhs = literal[1]; - break; - case kind::NOT: - if (literal[0].getKind() == kind::EQUAL) { - // Disequalities - d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); - return; - } else { - // Predicates + + if (propagatedBy(literal, SUB_EQUALITY)) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: lhs = literal[0]; + rhs = literal[1]; + break; + case kind::NOT: + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } else { + // Predicates + lhs = literal[0]; + rhs = d_false; + break; + } + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; rhs = d_false; break; - } - case kind::CONST_BOOLEAN: - // we get to explain true = false, since we set false to be the trigger of this - lhs = d_true; - rhs = d_false; - break; - default: - Unreachable(); + default: + Unreachable(); + } + d_equalityEngine.explainEquality(lhs, rhs, assumptions); + } else { + Assert(propagatedBy(literal, SUB_BITBLASTER)); + d_bitblaster->explain(literal, assumptions); } - d_equalityEngine.explainEquality(lhs, rhs, assumptions); } Node TheoryBV::explain(TNode node) { BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; + + // Ask for the explanation explain(node, assumptions); + // this means that it is something true at level 0 + if (assumptions.size() == 0) { + return utils::mkTrue(); + } + // return the explanation return mkAnd(assumptions); } void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; - if (d_useEqualityEngine) { + d_sharedTermsSet.insert(t); + if (!Options::current()->bitvector_eager_bitblast && d_useEqualityEngine) { d_equalityEngine.addTriggerTerm(t); } } @@ -441,6 +445,10 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { + if (Options::current()->bitvector_eager_bitblast) { + return EQUALITY_UNKNOWN; + } + if (d_useEqualityEngine) { if (d_equalityEngine.areEqual(a, b)) { // The terms are implied to be equal diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c4953213d..0ced179ec 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -66,7 +66,7 @@ private: /** Context dependent set of atoms we already propagated */ context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; - + context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet; public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -74,8 +74,6 @@ public: void preRegisterTerm(TNode n); - //void registerTerm(TNode n) { } - void check(Effort e); Node explain(TNode n); @@ -84,7 +82,6 @@ public: std::string identify() const { return std::string("TheoryBV"); } - //Node preprocessTerm(TNode term); PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); private: @@ -110,14 +107,14 @@ private: bool notify(TNode propagation) { Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl; // Just forward to bv - return d_bv.propagate(propagation); + return d_bv.storePropagation(propagation, SUB_EQUALITY); } void notify(TNode t1, TNode t2) { Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl; // Propagate equality between shared terms Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2)); - d_bv.propagate(t1.eqNode(t2)); + d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); } }; @@ -141,16 +138,38 @@ private: context::CDQueue<Node> d_toBitBlast; + enum SubTheory { + SUB_EQUALITY = 1, + SUB_BITBLASTER = 2 + }; + + /** + * Keeps a map from nodes to the subtheory that propagated it so that we can explain it + * properly. + */ + typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap; + PropagatedMap d_propagatedBy; + + bool propagatedBy(TNode literal, SubTheory subtheory) const { + PropagatedMap::const_iterator find = d_propagatedBy.find(literal); + if (find == d_propagatedBy.end()) return false; + else return (*find).second == subtheory; + } + /** Should be called to propagate the literal. */ - bool propagate(TNode literal); + bool storePropagation(TNode literal, SubTheory subtheory); - /** Explain why this literal is true by adding assumptions */ + /** + * Explains why this literal (propagated by subtheory) is true by adding assumptions. + */ void explain(TNode literal, std::vector<TNode>& assumptions); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); + friend class Bitblaster; + public: void propagate(Effort e); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 38547ad99..78835b75c 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -326,7 +326,10 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) { ++ it; } - Assert(expandedNodes.size() > 0); + if (expandedNodes.size() == 0) { + return mkTrue(); + } + if (expandedNodes.size() == 1) { return *expandedNodes.begin(); } |