From dfaba6987ded6afc0d9502b5f85088260a5a2d96 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 24 May 2012 16:03:38 +0000 Subject: [PATCH] Separating the subtheory implementations in the bitvector theory. --- src/theory/bv/Makefile.am | 5 +- src/theory/bv/bv_subtheory.h | 73 ----------- src/theory/bv/bv_subtheory_bitblast.cpp | 115 +++++++++++++++++ src/theory/bv/bv_subtheory_bitblast.h | 52 ++++++++ .../{bv_subtheory.cpp => bv_subtheory_eq.cpp} | 117 ++---------------- src/theory/bv/bv_subtheory_eq.h | 78 ++++++++++++ src/theory/bv/theory_bv.h | 2 + 7 files changed, 264 insertions(+), 178 deletions(-) create mode 100644 src/theory/bv/bv_subtheory_bitblast.cpp create mode 100644 src/theory/bv/bv_subtheory_bitblast.h rename src/theory/bv/{bv_subtheory.cpp => bv_subtheory_eq.cpp} (67%) create mode 100644 src/theory/bv/bv_subtheory_eq.h 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.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.cpp b/src/theory/bv/bv_subtheory_eq.cpp similarity index 67% rename from src/theory/bv/bv_subtheory.cpp rename to src/theory/bv/bv_subtheory_eq.cpp index fa36236c9..807d90137 100644 --- a/src/theory/bv/bv_subtheory.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -1,8 +1,8 @@ /********************* */ -/*! \file bv_subtheory.cpp +/*! \file bv_subtheory_eq.cpp ** \verbatim ** Original author: lianah - ** Major contributors: + ** 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) @@ -11,113 +11,22 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Algebraic solver. ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Algebraic solver. **/ -#include "theory/bv/bv_subtheory.h" +#include "theory/bv/bv_subtheory_eq.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::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), @@ -180,12 +89,12 @@ void EqualitySolver::explain(TNode literal, std::vector& assumptions) { } bool EqualitySolver::addAssertions(const std::vector& assertions, Theory::Effort e) { - BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; + 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; @@ -206,13 +115,13 @@ bool EqualitySolver::addAssertions(const std::vector& assertions, Theory: } } - // checking for a conflict + // checking for a conflict if (d_bv->inConflict()) { return false; } } - - return true; + + return true; } bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) { 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 { -- 2.30.2