From 1a890e13218be6e87dbf0124b03a73420631d816 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Wed, 16 May 2012 15:21:18 +0000 Subject: [PATCH] refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine --- src/theory/bv/Makefile.am | 2 + src/theory/bv/bitblaster.cpp | 2 +- src/theory/bv/bv_subtheory.cpp | 247 +++++++++++++++++++++++++++++++++ src/theory/bv/bv_subtheory.h | 152 ++++++++++++++++++++ src/theory/bv/theory_bv.cpp | 221 +++++------------------------ src/theory/bv/theory_bv.h | 97 +++---------- 6 files changed, 451 insertions(+), 270 deletions(-) create mode 100644 src/theory/bv/bv_subtheory.cpp create mode 100644 src/theory/bv/bv_subtheory.h diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 3bb7e3056..8f524c8fc 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -11,6 +11,8 @@ libbv_la_SOURCES = \ theory_bv_utils.h \ bitblaster.h \ bitblaster.cpp \ + bv_subtheory.h \ + bv_subtheory.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ theory_bv.h \ diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index 60fc8f9c1..6b59b9b00 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -350,7 +350,7 @@ Bitblaster::Statistics::~Statistics() { } bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) { - return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLASTER); + return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLAST); }; void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) { diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp new file mode 100644 index 000000000..f55d231b2 --- /dev/null +++ b/src/theory/bv/bv_subtheory.cpp @@ -0,0 +1,247 @@ +/********************* */ +/*! \file bv_subtheory.cpp + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/bv/bv_subtheory.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/bitblaster.h" + + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::context; + +using namespace std; +using namespace CVC4::theory::bv::utils; + + +BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) + : SubtheorySolver(c, bv), + d_bitblaster(new Bitblaster(c, bv)), + d_bitblastQueue(c) +{} + +BitblastSolver::~BitblastSolver() { + delete d_bitblaster; +} + +void BitblastSolver::preRegister(TNode node) { + 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->hasBBAtom(node)) { + d_bitblastQueue.push_back(node); + } +} + +void BitblastSolver::explain(TNode literal, std::vector& assumptions) { + d_bitblaster->explain(literal, assumptions); +} + +bool BitblastSolver::addAssertions(const std::vector& assertions, Theory::Effort e) { + BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl; + + //// Eager bit-blasting + if (Options::current()->bitvectorEagerBitblast) { + for (unsigned i = 0; i < assertions.size(); ++i) { + TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i]; + if (atom.getKind() != kind::BITVECTOR_BITOF) { + d_bitblaster->bbAtom(atom); + } + } + return true; + } + + //// Lazy bit-blasting + + // bit-blast enqueued nodes + while (!d_bitblastQueue.empty()) { + TNode atom = d_bitblastQueue.front(); + d_bitblaster->bbAtom(atom); + d_bitblastQueue.pop(); + } + + // propagation + for (unsigned i = 0; i < assertions.size(); ++i) { + TNode fact = assertions[i]; + if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) { + // 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 conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); + d_bv->setConflict(mkConjunction(conflictAtoms)); + return false; + } + } + } + + // solving + if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) { + Assert(!d_bv->inConflict()); + BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; + bool ok = d_bitblaster->solve(); + if (!ok) { + std::vector conflictAtoms; + d_bitblaster->getConflict(conflictAtoms); + Node conflict = mkConjunction(conflictAtoms); + d_bv->setConflict(conflict); + return false; + } + } + + return true; +} + +EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv) + : SubtheorySolver(c, bv), + d_notify(bv), + d_equalityEngine(d_notify, c, "theory::bv::TheoryBV") +{ + if (d_useEqualityEngine) { + + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + } +} + +void EqualitySolver::preRegister(TNode node) { + if (!d_useEqualityEngine) + return; + + if (node.getKind() == kind::EQUAL) { + d_equalityEngine.addTriggerEquality(node); + } else { + d_equalityEngine.addTerm(node); + } +} + +void EqualitySolver::explain(TNode literal, std::vector& assumptions) { + bool polarity = literal.getKind() != kind::NOT; + TNode atom = polarity ? literal : literal[0]; + if (atom.getKind() == kind::EQUAL) { + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + } else { + d_equalityEngine.explainPredicate(atom, polarity, assumptions); + } +} + +bool EqualitySolver::addAssertions(const std::vector& assertions, Theory::Effort e) { + BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; + Assert (!d_bv->inConflict()); + + for (unsigned i = 0; i < assertions.size(); ++i) { + TNode fact = assertions[i]; + + // Notify the equality engine + if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::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.assertEquality(predicate, false, fact); + } else { + // equality + d_equalityEngine.assertEquality(predicate, true, fact); + } + } else { + // Adding predicate if the congruence over it is turned on + if (d_equalityEngine.isFunctionKind(predicate.getKind())) { + d_equalityEngine.assertPredicate(predicate, !negated, fact); + } + } + } + + // checking for a conflict + if (d_bv->inConflict()) { + return false; + } + } + + return true; +} + +bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { + BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY); + } else { + return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY); + } +} + +bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { + BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY); + } else { + return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY); + } +} + +bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + if (value) { + return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); + } else { + return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY); + } +} + +bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + if (Theory::theoryOf(t1) == THEORY_BOOL) { + return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY); + } + return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); +} diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h new file mode 100644 index 000000000..cc62013fd --- /dev/null +++ b/src/theory/bv/bv_subtheory.h @@ -0,0 +1,152 @@ +/********************* */ +/*! \file bv_subtheory.h + ** \verbatim + ** Original author: lianah + ** Major contributors: dejan + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Algebraic solver. + ** + ** Algebraic solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BV_SUBTHEORY_H +#define __CVC4__THEORY__BV__BV_SUBTHEORY_H + +#include "context/context.h" +#include "context/cdqueue.h" +#include "theory/uf/equality_engine.h" +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +const bool d_useEqualityEngine = true; +const bool d_useSatPropagation = true; + +// forward declaration +class TheoryBV; +class Bitblaster; + +/** + * Abstract base class for bit-vector subtheory solvers + * + */ +class SubtheorySolver { + +protected: + + /** The context we are using */ + context::Context* d_context; + + /** The bit-vector theory */ + TheoryBV* d_bv; + +public: + + SubtheorySolver(context::Context* c, TheoryBV* bv) : + d_context(c), + d_bv(bv) + {} + virtual ~SubtheorySolver() {} + + virtual bool addAssertions(const std::vector& assertions, Theory::Effort e) = 0; + virtual void explain(TNode literal, std::vector& assumptions) = 0; + virtual void preRegister(TNode node) {} + +}; + + +/** + * BitblastSolver + * + */ + +class BitblastSolver : public SubtheorySolver { + + /** Bitblaster */ + Bitblaster* d_bitblaster; + + /** Nodes that still need to be bit-blasted */ + context::CDQueue d_bitblastQueue; + +public: + BitblastSolver(context::Context* c, TheoryBV* bv); + ~BitblastSolver(); + + void preRegister(TNode node); + bool addAssertions(const std::vector& assertions, Theory::Effort e); + void explain(TNode literal, std::vector& assumptions); +}; + + +/** + * EqualitySolver + * + */ + +class EqualitySolver : public SubtheorySolver { + + // NotifyClass: handles call-back from congruence closure module + + class NotifyClass : public eq::EqualityEngineNotify { + TheoryBV* d_bv; + + public: + NotifyClass(TheoryBV* bv): d_bv(bv) {} + bool eqNotifyTriggerEquality(TNode equality, bool value); + 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 */ + NotifyClass d_notify; + + /** Equality engine */ + eq::EqualityEngine d_equalityEngine; + +public: + + EqualitySolver(context::Context* c, TheoryBV* bv); + + void preRegister(TNode node); + bool addAssertions(const std::vector& assertions, Theory::Effort e); + void explain(TNode literal, std::vector& assumptions); + void addSharedTerm(TNode t) { + d_equalityEngine.addTriggerTerm(t); + } + EqualityStatus getEqualityStatus(TNode a, TNode b) { + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; + } + return EQUALITY_UNKNOWN; + } +}; + + +// class CoreSolver : public SubtheorySolver { + +// }; + + +} +} +} + +#endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 445b2d242..26452e5e8 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -31,66 +31,24 @@ using namespace std; using namespace CVC4::theory::bv::utils; -const bool d_useEqualityEngine = true; -const bool d_useSatPropagation = true; TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), - d_assertions(c), - d_bitblaster(new Bitblaster(c, this) ), - d_bitblastQueue(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), + d_bitblastSolver(c, this), + d_equalitySolver(c, this), d_statistics(), - 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_propagatedBy(c) - { - if (d_useEqualityEngine) { - - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); + {} - } - } +TheoryBV::~TheoryBV() {} -TheoryBV::~TheoryBV() { - delete d_bitblaster; -} TheoryBV::Statistics::Statistics(): d_avgConflictSize("theory::bv::AvgBVConflictSize"), d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0), @@ -115,141 +73,45 @@ void TheoryBV::preRegisterTerm(TNode node) { 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->hasBBAtom(node)) { - d_bitblastQueue.push_back(node); - } - - if (d_useEqualityEngine) { - switch (node.getKind()) { - case kind::EQUAL: - // Add the trigger for equality - d_equalityEngine.addTriggerEquality(node); - break; - default: - d_equalityEngine.addTerm(node); - break; - } - } - + d_bitblastSolver.preRegister(node); + d_equalitySolver.preRegister(node); } void TheoryBV::check(Effort e) { BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; - if (Options::current()->bitvectorEagerBitblast) { - 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); - } - } - } + // if we are already in conflict just return the conflict + if (d_conflict) { + BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; + d_out->conflict(d_conflictNode); + d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren()); return; } - - // getting the new assertions + // getting the new assertions std::vector new_assertions; - while (!done() && !d_conflict) { + while (!done()) { Assertion assertion = get(); TNode fact = assertion.assertion; new_assertions.push_back(fact); BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; } - // sending assertions to equality engine first - - for (unsigned i = 0; i < new_assertions.size(); ++i) { - TNode fact = new_assertions[i]; - TypeNode factType = fact[0].getType(); - - // 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.assertEquality(predicate, false, fact); - } else { - // equality - d_equalityEngine.assertEquality(predicate, true, fact); - } - } else { - // Adding predicate if the congruence over it is turned on - if (d_equalityEngine.isFunctionKind(predicate.getKind())) { - d_equalityEngine.assertPredicate(predicate, !negated, fact); - } - } - } - - // checking for a conflict - if (d_conflict) { - BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; - d_out->conflict(d_conflictNode); - return; - } - } - - // bit-blasting atoms on queue - - while (!d_bitblastQueue.empty()) { - TNode node = d_bitblastQueue.front(); - d_bitblaster->bbAtom(node); - d_bitblastQueue.pop(); - } + // sending assertions to the equality solver first + bool ok = d_equalitySolver.addAssertions(new_assertions, e); - // bit-blaster propagation - for (unsigned i = 0; i < new_assertions.size(); ++i) { - TNode fact = new_assertions[i]; - 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 conflictAtoms; - d_bitblaster->getConflict(conflictAtoms); - d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - d_conflict = true; - d_conflictNode = mkConjunction(conflictAtoms); - break; - } - } + if (ok) { + // sending assertions to the bitblast solver + ok = d_bitblastSolver.addAssertions(new_assertions, e); } - - // If in conflict, output the conflict - if (d_conflict) { + + if (!ok) { + // output conflict + Assert (d_conflict); BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode; d_out->conflict(d_conflictNode); - return; - } - - if (e == EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) { - Assert(done() && !d_conflict); - BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; - bool ok = d_bitblaster->solve(); - if (!ok) { - std::vector conflictAtoms; - d_bitblaster->getConflict(conflictAtoms); - d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size()); - Node conflict = mkConjunction(conflictAtoms); - d_out->conflict(conflict); - BVDebug("bitvector") << "TheoryBV::check returns conflict: " < assumptions; explain(literal, assumptions); explain(negLiteral, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; + setConflict(mkAnd(assumptions)); return; } @@ -311,14 +172,12 @@ void TheoryBV::propagate(Effort e) { d_alreadyPropagatedSet.insert(literal); } else { Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl; - Node negatedLiteral; std::vector assumptions; negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode(); assumptions.push_back(negatedLiteral); explain(literal, assumptions); - d_conflictNode = mkAnd(assumptions); - d_conflict = true; + setConflict(mkAnd(assumptions)); return; } } @@ -381,8 +240,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) 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; + setConflict(mkAnd(assumptions)); return false; } @@ -396,17 +254,12 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector& assumptions) { + // Ask the appropriate subtheory for the explanation if (propagatedBy(literal, SUB_EQUALITY)) { - bool polarity = literal.getKind() != kind::NOT; - TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); - } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); - } + d_equalitySolver.explain(literal, assumptions); } else { - Assert(propagatedBy(literal, SUB_BITBLASTER)); - d_bitblaster->explain(literal, assumptions); + Assert(propagatedBy(literal, SUB_BITBLAST)); + d_bitblastSolver.explain(literal, assumptions); } } @@ -432,7 +285,7 @@ void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) { - d_equalityEngine.addTriggerTerm(t); + d_equalitySolver.addSharedTerm(t); } } @@ -443,16 +296,6 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) return EQUALITY_UNKNOWN; } - if (d_useEqualityEngine) { - if (d_equalityEngine.areEqual(a, b)) { - // The terms are implied to be equal - return EQUALITY_TRUE; - } - if (d_equalityEngine.areDisequal(a, b)) { - // The terms are implied to be dis-equal - return EQUALITY_FALSE; - } - } - return EQUALITY_UNKNOWN; + return d_equalitySolver.getEqualityStatus(a, b); } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 9ab5f8e1c..214fa3b36 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -27,40 +27,24 @@ #include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" -#include "theory/uf/equality_engine.h" #include "context/cdqueue.h" - -namespace BVMinisat { -class SimpSolver; -} - +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { namespace bv { -/// forward declarations -class Bitblaster; - class TheoryBV : public Theory { - -private: - /** The context we are using */ context::Context* d_context; - /** The asserted stuff */ - context::CDList d_assertions; - - /** Bitblaster */ - Bitblaster* d_bitblaster; - - context::CDQueue d_bitblastQueue; - /** Context dependent set of atoms we already propagated */ context::CDHashSet d_alreadyPropagatedSet; context::CDHashSet d_sharedTermsSet; + + BitblastSolver d_bitblastSolver; + EqualitySolver d_equalitySolver; public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); @@ -70,6 +54,8 @@ public: void check(Effort e); + void propagate(Effort e); + Node explain(TNode n); Node getValue(TNode n); @@ -91,58 +77,6 @@ private: Statistics d_statistics; - // Added by Clark - // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module - class NotifyClass : public eq::EqualityEngineNotify { - - TheoryBV& d_bv; - - public: - - NotifyClass(TheoryBV& uf): d_bv(uf) {} - - bool eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_bv.storePropagation(equality, SUB_EQUALITY); - } else { - return d_bv.storePropagation(equality.notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_bv.storePropagation(predicate, SUB_EQUALITY); - } else { - return d_bv.storePropagation(predicate.notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { - Debug("bitvector") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; - if (value) { - return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); - } else { - return d_bv.storePropagation(t1.eqNode(t2).notNode(), SUB_EQUALITY); - } - } - - bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (Theory::theoryOf(t1) == THEORY_BOOL) { - return d_bv.storePropagation(t1.iffNode(t2), SUB_EQUALITY); - } - return d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY); - } - }; - - /** The notify class for d_equalityEngine */ - NotifyClass d_notify; - - /** Equaltity engine */ - eq::EqualityEngine d_equalityEngine; - // Are we in conflict? context::CDO d_conflict; @@ -155,11 +89,9 @@ private: /** Index of the next literal to propagate */ context::CDO d_literalsToPropagateIndex; - context::CDQueue d_toBitBlast; - enum SubTheory { SUB_EQUALITY = 1, - SUB_BITBLASTER = 2 + SUB_BITBLAST = 2 }; /** @@ -187,17 +119,22 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b); - friend class Bitblaster; - inline std::string indent() { std::string indentStr(getSatContext()->getLevel(), ' '); return indentStr; } - -public: - void propagate(Effort e); + void setConflict(Node conflict) { + d_conflict = true; + d_conflictNode = conflict; + } + + bool inConflict() { return d_conflict == true; } + + friend class Bitblaster; + friend class BitblastSolver; + friend class EqualitySolver; };/* class TheoryBV */ -- 2.30.2