theory_bv_utils.h \
bitblaster.h \
bitblaster.cpp \
+ bv_subtheory.h \
+ bv_subtheory.cpp \
bitblast_strategies.h \
bitblast_strategies.cpp \
theory_bv.h \
}
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) {
--- /dev/null
+/********************* */
+/*! \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<TNode>& assumptions) {
+ d_bitblaster->explain(literal, assumptions);
+}
+
+bool BitblastSolver::addAssertions(const std::vector<TNode>& 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<TNode> 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<TNode> 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<TNode>& 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<TNode>& 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);
+}
--- /dev/null
+/********************* */
+/*! \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<TNode>& assertions, Theory::Effort e) = 0;
+ virtual void explain(TNode literal, std::vector<TNode>& 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<TNode> d_bitblastQueue;
+
+public:
+ BitblastSolver(context::Context* c, TheoryBV* bv);
+ ~BitblastSolver();
+
+ void preRegister(TNode node);
+ bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+ void explain(TNode literal, std::vector<TNode>& 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<TNode>& assertions, Theory::Effort e);
+ void explain(TNode literal, std::vector<TNode>& 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 */
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),
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<TNode> 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<TNode> 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<TNode> 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: " <<conflict <<" \n ";
- return;
- }
+ d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
}
}
std::vector<TNode> assumptions;
explain(literal, assumptions);
explain(negLiteral, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
+ setConflict(mkAnd(assumptions));
return;
}
d_alreadyPropagatedSet.insert(literal);
} else {
Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
-
Node negatedLiteral;
std::vector<TNode> 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;
}
}
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;
}
void TheoryBV::explain(TNode literal, std::vector<TNode>& 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);
}
}
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);
}
}
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);
}
#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<TNode> d_assertions;
-
- /** Bitblaster */
- Bitblaster* d_bitblaster;
-
- context::CDQueue<TNode> d_bitblastQueue;
-
/** Context dependent set of atoms we already propagated */
context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
+
+ BitblastSolver d_bitblastSolver;
+ EqualitySolver d_equalitySolver;
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
void check(Effort e);
+ void propagate(Effort e);
+
Node explain(TNode n);
Node getValue(TNode n);
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<bool> d_conflict;
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
- context::CDQueue<Node> d_toBitBlast;
-
enum SubTheory {
SUB_EQUALITY = 1,
- SUB_BITBLASTER = 2
+ SUB_BITBLAST = 2
};
/**
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 */
projects / cvc5.git / commitdiff