From: Dejan Jovanović Date: Thu, 24 May 2012 16:03:38 +0000 (+0000) Subject: Separating the subtheory implementations in the bitvector theory. X-Git-Tag: cvc5-1.0.0~8145 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dfaba6987ded6afc0d9502b5f85088260a5a2d96;p=cvc5.git Separating the subtheory implementations in the bitvector theory. --- diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 8f524c8fc..7748817e3 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -12,7 +12,10 @@ libbv_la_SOURCES = \ bitblaster.h \ bitblaster.cpp \ bv_subtheory.h \ - bv_subtheory.cpp \ + bv_subtheory_eq.h \ + bv_subtheory_eq.cpp \ + bv_subtheory_bitblast.h \ + bv_subtheory_bitblast.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ theory_bv.h \ diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp deleted file mode 100644 index fa36236c9..000000000 --- a/src/theory/bv/bv_subtheory.cpp +++ /dev/null @@ -1,251 +0,0 @@ -/********************* */ -/*! \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; -} - -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), - 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(TheoryId tag, 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 index d508976ae..a8813b7aa 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -35,7 +35,6 @@ const bool d_useSatPropagation = true; // forward declaration class TheoryBV; -class Bitblaster; /** * Abstract base class for bit-vector subtheory solvers @@ -65,78 +64,6 @@ public: }; - -/** - * 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); - EqualityStatus getEqualityStatus(TNode a, TNode b); -}; - - -/** - * 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(TheoryId tag, 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, THEORY_BV); - } - 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; - } -}; - - } } } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp new file mode 100644 index 000000000..ff0fc2b1a --- /dev/null +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file bv_subtheory_eq_bitblast.cpp + ** \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 "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/bitblaster.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +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; +} + +EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { + return d_bitblaster->getEqualityStatus(a, b); +} diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h new file mode 100644 index 000000000..0a8f046b7 --- /dev/null +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file bv_subtheory_eq_bitblast.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. + **/ + +#pragma once + +#include "theory/bv/bv_subtheory.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +class Bitblaster; + +/** + * 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); + EqualityStatus getEqualityStatus(TNode a, TNode b); +}; + +} +} +} diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp new file mode 100644 index 000000000..807d90137 --- /dev/null +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -0,0 +1,160 @@ +/********************* */ +/*! \file bv_subtheory_eq.cpp + ** \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 "theory/bv/bv_subtheory_eq.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv::utils; + +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(TheoryId tag, 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_eq.h b/src/theory/bv/bv_subtheory_eq.h new file mode 100644 index 000000000..241dd5919 --- /dev/null +++ b/src/theory/bv/bv_subtheory_eq.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \file bv_subtheory_eq.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. + **/ + +#pragma once + +#include "theory/bv/bv_subtheory.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +/** + * Bitvector equality solver + */ +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(TheoryId tag, 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, THEORY_BV); + } + 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; + } +}; + + +} +} +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 214fa3b36..9c27f62c5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -29,6 +29,8 @@ #include "util/stats.h" #include "context/cdqueue.h" #include "theory/bv/bv_subtheory.h" +#include "theory/bv/bv_subtheory_eq.h" +#include "theory/bv/bv_subtheory_bitblast.h" namespace CVC4 { namespace theory {