summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/bv/bv_sat.cpp91
-rw-r--r--src/theory/bv/bv_sat.h36
-rw-r--r--src/theory/bv/theory_bv.cpp308
-rw-r--r--src/theory/bv/theory_bv.h35
-rw-r--r--src/theory/bv/theory_bv_utils.h5
-rw-r--r--src/theory/term_registration_visitor.cpp4
-rw-r--r--src/theory/theory.cpp1
-rw-r--r--src/theory/theory_engine.cpp43
-rw-r--r--src/theory/theory_engine.h10
-rw-r--r--src/theory/uf/equality_engine.h7
-rw-r--r--src/theory/valuation.cpp1
11 files changed, 307 insertions, 234 deletions
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index 2f4ac1324..dcb33c9af 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -23,7 +23,8 @@
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
-#include "theory_bv_rewrite_rules_simplification.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/bv/theory_bv.h"
using namespace std;
@@ -35,7 +36,6 @@ namespace CVC4 {
namespace theory {
namespace bv{
-
std::string toString(Bits& bits) {
ostringstream os;
for (int i = bits.size() - 1; i >= 0; --i) {
@@ -52,7 +52,8 @@ std::string toString(Bits& bits) {
}
/////// Bitblaster
-Bitblaster::Bitblaster(context::Context* c) :
+Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
+ d_bvOutput(bv->d_out),
d_termCache(),
d_bitblastedAtoms(),
d_assertedAtoms(c),
@@ -61,6 +62,8 @@ Bitblaster::Bitblaster(context::Context* c) :
d_satSolver = prop::SatSolverFactory::createMinisat(c);
d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar());
+ MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
+ d_satSolver->setNotify(notify);
// initializing the bit-blasting strategies
initAtomBBStrategies();
initTermBBStrategies();
@@ -79,6 +82,8 @@ Bitblaster::~Bitblaster() {
*
*/
void Bitblaster::bbAtom(TNode node) {
+ node = node.getKind() == kind::NOT? node[0] : node;
+
if (hasBBAtom(node)) {
return;
}
@@ -94,8 +99,13 @@ void Bitblaster::bbAtom(TNode node) {
Node atom_definition = mkNode(kind::IFF, node, atom_bb);
// do boolean simplifications if possible
Node rewritten = Rewriter::rewrite(atom_definition);
- d_cnfStream->convertAndAssert(rewritten, true, false);
- d_bitblastedAtoms.insert(node);
+
+ if (!Options::current()->bitvector_eager_bitblast) {
+ d_cnfStream->convertAndAssert(rewritten, true, false);
+ d_bitblastedAtoms.insert(node);
+ } else {
+ d_bvOutput->lemma(rewritten, false);
+ }
}
@@ -154,65 +164,21 @@ Node Bitblaster::bbOptimize(TNode node) {
/// Public methods
void Bitblaster::addAtom(TNode atom) {
- d_cnfStream->ensureLiteral(atom);
- SatLiteral lit = d_cnfStream->getLiteral(atom);
- d_satSolver->addMarkerLiteral(lit);
-}
-bool Bitblaster::getPropagations(std::vector<TNode>& propagations) {
- std::vector<SatLiteral> propagated_literals;
- if (d_satSolver->getPropagations(propagated_literals)) {
- for (unsigned i = 0; i < propagated_literals.size(); ++i) {
- propagations.push_back(d_cnfStream->getNode(propagated_literals[i]));
- }
- return true;
+ if (!Options::current()->bitvector_eager_bitblast) {
+ d_cnfStream->ensureLiteral(atom);
+ SatLiteral lit = d_cnfStream->getLiteral(atom);
+ d_satSolver->addMarkerLiteral(lit);
}
- return false;
}
-void Bitblaster::explainPropagation(TNode atom, std::vector<Node>& explanation) {
+void Bitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
std::vector<SatLiteral> literal_explanation;
- d_satSolver->explainPropagation(d_cnfStream->getLiteral(atom), literal_explanation);
+ d_satSolver->explain(d_cnfStream->getLiteral(atom), literal_explanation);
for (unsigned i = 0; i < literal_explanation.size(); ++i) {
explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
}
}
-/**
- * Called from preregistration bitblasts the node
- *
- * @param node
- *
- * @return
- */
-void Bitblaster::bitblast(TNode node) {
- TimerStat::CodeTimer codeTimer(d_statistics.d_bitblastTimer);
-
- /// strip the not
- if (node.getKind() == kind::NOT) {
- node = node[0];
- }
-
- if (node.getKind() == kind::EQUAL ||
- node.getKind() == kind::BITVECTOR_ULT ||
- node.getKind() == kind::BITVECTOR_ULE ||
- node.getKind() == kind::BITVECTOR_SLT ||
- node.getKind() == kind::BITVECTOR_SLE)
- {
- bbAtom(node);
- }
- else if (node.getKind() == kind::BITVECTOR_UGT ||
- node.getKind() == kind::BITVECTOR_UGE ||
- node.getKind() == kind::BITVECTOR_SGT ||
- node.getKind() == kind::BITVECTOR_SGE )
- {
- Unhandled(node.getKind());
- }
- else
- {
- Bits bits;
- bbTerm(node, bits);
- }
-}
/**
* Asserts the clauses corresponding to the atom to the Sat Solver
@@ -383,7 +349,22 @@ Bitblaster::Statistics::~Statistics() {
StatisticsRegistry::unregisterStat(&d_bitblastTimer);
}
+bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
+ return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLASTER);
+};
+void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
+ if (clause.size() > 1) {
+ NodeBuilder<> lemmab(kind::OR);
+ for (unsigned i = 0; i < clause.size(); ++ i) {
+ lemmab << d_cnf->getNode(clause[i]);
+ }
+ Node lemma = lemmab;
+ d_bv->d_out->lemma(lemma);
+ } else {
+ d_bv->d_out->lemma(d_cnf->getNode(clause[0]));
+ }
+};
} /*bv namespace */
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index 2422da0b7..7016879a0 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -47,22 +47,37 @@ class CnfStream;
class BVSatSolverInterface;
}
-
namespace theory {
+
+class OutputChannel;
+
namespace bv {
+typedef std::vector<Node> Bits;
std::string toString (Bits& bits);
+class TheoryBV;
+
/**
* The Bitblaster that manages the mapping between Nodes
* and their bitwise definition
*
*/
-
-typedef std::vector<Node> Bits;
-
class Bitblaster {
+
+ /** This class gets callbacks from minisat on propagations */
+ class MinisatNotify : public prop::BVSatSolverInterface::Notify {
+ prop::CnfStream* d_cnf;
+ TheoryBV *d_bv;
+ public:
+ MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv)
+ : d_cnf(cnf)
+ , d_bv(bv)
+ {}
+ bool notify(prop::SatLiteral lit);
+ void notify(prop::SatClause& clause);
+ };
typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
@@ -71,6 +86,7 @@ class Bitblaster {
typedef Node (*AtomBBStrategy) (TNode, Bitblaster*);
// sat solver used for bitblasting and associated CnfStream
+ theory::OutputChannel* d_bvOutput;
prop::BVSatSolverInterface* d_satSolver;
prop::CnfStream* d_cnfStream;
@@ -88,9 +104,6 @@ class Bitblaster {
bool hasBBTerm(TNode node);
void getBBTerm(TNode node, Bits& bits);
-
-
-
/// function tables for the various bitblasting strategies indexed by node kind
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
@@ -102,7 +115,6 @@ class Bitblaster {
// returns a node that might be easier to bitblast
Node bbOptimize(TNode node);
- void bbAtom(TNode node);
void addAtom(TNode atom);
// division is bitblasted in terms of constraints
// so it needs to use private bitblaster interface
@@ -111,17 +123,15 @@ class Bitblaster {
public:
void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
void bbTerm(TNode node, Bits& bits);
+ void bbAtom(TNode node);
-public:
- Bitblaster(context::Context* c);
+ Bitblaster(context::Context* c, bv::TheoryBV* bv);
~Bitblaster();
bool assertToSat(TNode node, bool propagate = true);
bool solve(bool quick_solve = false);
- void bitblast(TNode node);
void getConflict(std::vector<TNode>& conflict);
+ void explain(TNode atom, std::vector<TNode>& explanation);
- bool getPropagations(std::vector<TNode>& propagations);
- void explainPropagation(TNode atom, std::vector<Node>& explanation);
private:
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index b6f12793d..c9d58574e 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -40,15 +40,17 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
: Theory(THEORY_BV, c, u, out, valuation, logicInfo),
d_context(c),
d_assertions(c),
- d_bitblaster(new Bitblaster(c) ),
+ d_bitblaster(new Bitblaster(c, this) ),
d_alreadyPropagatedSet(c),
d_statistics(),
+ d_sharedTermsSet(c),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
d_conflict(c, false),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
- d_toBitBlast(c)
+ d_toBitBlast(c),
+ d_propagatedBy(c)
{
d_true = utils::mkTrue();
d_false = utils::mkFalse();
@@ -58,6 +60,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
d_equalityEngine.addTerm(d_false);
d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+ // add disequality between 0 and 1 bits
+ d_equalityEngine.addDisequality(utils::mkConst(BitVector((unsigned)1, (unsigned)0)),
+ utils::mkConst(BitVector((unsigned)1, (unsigned)1)),
+ d_true);
+
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
// d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
@@ -113,12 +120,18 @@ TheoryBV::Statistics::~Statistics() {
void TheoryBV::preRegisterTerm(TNode node) {
BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
+
+ if (Options::current()->bitvector_eager_bitblast) {
+ // don't use the equality engine in the eager bit-blasting
+ return;
+ }
+
if (node.getKind() == kind::EQUAL ||
node.getKind() == kind::BITVECTOR_ULT ||
node.getKind() == kind::BITVECTOR_ULE ||
node.getKind() == kind::BITVECTOR_SLT ||
node.getKind() == kind::BITVECTOR_SLE) {
- d_bitblaster->bitblast(node);
+ d_bitblaster->bbAtom(node);
}
if (d_useEqualityEngine) {
@@ -140,56 +153,56 @@ void TheoryBV::preRegisterTerm(TNode node) {
void TheoryBV::check(Effort e)
{
- BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
- BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
+ BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+
+ if (Options::current()->bitvector_eager_bitblast) {
+ while (!done()) {
+ Assertion assertion = get();
+ TNode fact = assertion.assertion;
+ if (fact.getKind() == kind::NOT) {
+ if (fact[0].getKind() != kind::BITVECTOR_BITOF) {
+ d_bitblaster->bbAtom(fact[0]);
+ }
+ } else {
+ if (fact.getKind() != kind::BITVECTOR_BITOF) {
+ d_bitblaster->bbAtom(fact);
+ }
+ }
+ }
+ return;
+ }
+
while (!done() && !d_conflict) {
Assertion assertion = get();
TNode fact = assertion.assertion;
BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
- // If the assertion doesn't have a literal, it's a shared equality
- bool shared = !assertion.isPreregistered;
- Assert(!d_useEqualityEngine || !shared ||
- ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
- (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
- d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
-
- // Notify the Equality Engine
- switch (fact.getKind()) {
- case kind::EQUAL:
- if (d_useEqualityEngine) {
- d_equalityEngine.addEquality(fact[0], fact[1], fact);
- }
- if (shared && !d_bitblaster->hasBBAtom(fact)) {
- d_bitblaster->bitblast(fact);
- }
- break;
- case kind::NOT:
- if (fact[0].getKind() == kind::EQUAL) {
- // Assert the dis-equality
- if (d_useEqualityEngine) {
- d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
- }
- if (shared && !d_bitblaster->hasBBAtom(fact[0])) {
- d_bitblaster->bitblast(fact[0]);
- }
+ // Notify the equality engine
+ if (d_useEqualityEngine && !d_conflict && !propagatedBy(fact, SUB_EQUALITY) ) {
+ bool negated = fact.getKind() == kind::NOT;
+ TNode predicate = negated ? fact[0] : fact;
+ if (predicate.getKind() == kind::EQUAL) {
+ if (negated) {
+ // dis-equality
+ d_equalityEngine.addDisequality(predicate[0], predicate[1], fact);
} else {
- if (d_useEqualityEngine) {
- d_equalityEngine.addPredicate(fact[0], false, fact);
- }
- break;
+ // equality
+ d_equalityEngine.addEquality(predicate[0], predicate[1], fact);
}
- break;
- default:
- if (d_useEqualityEngine) {
- d_equalityEngine.addPredicate(fact, true, fact);
+ } else {
+ // Adding predicate if the congruence over it is turned on
+ if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+ d_equalityEngine.addPredicate(predicate, !negated, fact);
}
- break;
+ }
}
- // make sure we do not assert things we propagated
- if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) {
+ // Bit-blaster
+ if (!d_conflict && !propagatedBy(fact, SUB_BITBLASTER)) {
+ // Some atoms have not been bit-blasted yet
+ d_bitblaster->bbAtom(fact);
+ // Assert to sat
bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
if (!ok) {
std::vector<TNode> conflictAtoms;
@@ -204,17 +217,15 @@ void TheoryBV::check(Effort e)
// If in conflict, output the conflict
if (d_conflict) {
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode;
d_out->conflict(d_conflictNode);
return;
}
- if (e == EFFORT_FULL) {
-
+ if (e == EFFORT_FULL || Options::current()->bitvector_eager_fullcheck) {
Assert(done() && !d_conflict);
BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
- // in standard effort we only do boolean constraint propagation
- bool ok = d_bitblaster->solve(false);
+ bool ok = d_bitblaster->solve();
if (!ok) {
std::vector<TNode> conflictAtoms;
d_bitblaster->getConflict(conflictAtoms);
@@ -225,7 +236,6 @@ void TheoryBV::check(Effort e)
return;
}
}
-
}
@@ -253,77 +263,55 @@ void TheoryBV::propagate(Effort e) {
return;
}
- // get new propagations from the equality engine
- for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+ // go through stored propagations
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size();
+ d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
+ {
TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
- BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
- bool satValue;
Node normalized = Rewriter::rewrite(literal);
- if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
- d_out->propagate(literal);
- } else {
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
- Node negatedLiteral;
- std::vector<TNode> assumptions;
- if (normalized != d_false) {
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- }
- explain(literal, assumptions);
- d_conflictNode = mkAnd(assumptions);
- d_conflict = true;
- return;
- }
- }
- // get new propagations from the sat solver
- std::vector<TNode> propagations;
- d_bitblaster->getPropagations(propagations);
-
- // propagate the facts on the propagation queue
- for (unsigned i = 0; i < propagations.size(); ++ i) {
- TNode node = propagations[i];
- BVDebug("bitvector") << "TheoryBV::propagate " << node <<" \n";
- if (!d_valuation.isSatLiteral(node)) {
- // TODO: maybe propagate shared terms too?
- continue;
- }
- if (d_valuation.getSatValue(node) == Node::null()) {
- vector<Node> explanation;
- d_bitblaster->explainPropagation(node, explanation);
- if (explanation.size() == 0) {
- d_out->lemma(node);
+ TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+ // check if it's a shared equality in the current context
+ if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) ||
+ (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
+ d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) {
+
+ bool satValue;
+ if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+ // check if we already propagated the negation
+ Node neg_literal = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
+ if (d_alreadyPropagatedSet.find(neg_literal) != d_alreadyPropagatedSet.end()) {
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n";
+ // we are in conflict
+ std::vector<TNode> assumptions;
+ explain(literal, assumptions);
+ explain(neg_literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return;
+ }
+
+ BVDebug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): " << literal << std::endl;
+ d_out->propagate(literal);
+ d_alreadyPropagatedSet.insert(literal);
} else {
- NodeBuilder<> nb(kind::OR);
- nb << node;
- for (unsigned i = 0; i < explanation.size(); ++ i) {
- nb << explanation[i].notNode();
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+
+ Node negatedLiteral;
+ std::vector<TNode> assumptions;
+ if (normalized != d_false) {
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
}
- Node lemma = nb;
- d_out->lemma(lemma);
+ explain(literal, assumptions);
+ d_conflictNode = mkAnd(assumptions);
+ d_conflict = true;
+ return;
}
- d_alreadyPropagatedSet.insert(node);
}
}
-
}
-// Node TheoryBV::explain(TNode n) {
-// BVDebug("bitvector") << "TheoryBV::explain node " << n <<"\n";
-// std::vector<Node> explanation;
-// d_bitblaster->explainPropagation(n, explanation);
-// Node exp;
-
-// if (explanation.size() == 0) {
-// return utils::mkTrue();
-// }
-
-// exp = utils::mkAnd(explanation);
-
-// BVDebug("bitvector") << "TheoryBV::explain with " << exp <<"\n";
-// return exp;
-// }
-
Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
switch(in.getKind()) {
case kind::EQUAL:
@@ -351,42 +339,44 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
}
-bool TheoryBV::propagate(TNode literal)
+bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
{
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ")" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ")" << std::endl;
// If already in conflict, no more propagation
if (d_conflict) {
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+ Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl;
return false;
}
+ // If propagated already, just skip
+ PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+ if (find != d_propagatedBy.end()) {
+ //unsigned theories = (*find).second | (unsigned) subtheory;
+ //d_propagatedBy[literal] = theories;
+ return true;
+ } else {
+ d_propagatedBy[literal] = subtheory;
+ }
+
// See if the literal has been asserted already
- Node normalized = Rewriter::rewrite(literal);
bool satValue = false;
- bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
-
+ bool hasSatValue = d_valuation.hasSatValue(literal, satValue);
// If asserted, we might be in conflict
- if (isAsserted) {
- if (!satValue) {
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+
+ if (hasSatValue && !satValue) {
+ Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
- Node negatedLiteral;
- if (normalized != d_false) {
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- }
+ Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
+ assumptions.push_back(negatedLiteral);
explain(literal, assumptions);
d_conflictNode = mkAnd(assumptions);
d_conflict = true;
return false;
- }
- // Propagate even if already known in SAT - could be a new equation between shared terms
- // (terms that weren't shared when the literal was asserted!)
}
// Nothing, just enqueue it for propagation and mark it as asserted already
- Debug("bitvector") << spaces(getSatContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+ Debug("bitvector-prop") << spaces(getSatContext()->getLevel()) << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl;
d_literalsToPropagate.push_back(literal);
return true;
@@ -394,46 +384,60 @@ bool TheoryBV::propagate(TNode literal)
void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
- TNode lhs, rhs;
- switch (literal.getKind()) {
- case kind::EQUAL:
- lhs = literal[0];
- rhs = literal[1];
- break;
- case kind::NOT:
- if (literal[0].getKind() == kind::EQUAL) {
- // Disequalities
- d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
- return;
- } else {
- // Predicates
+
+ if (propagatedBy(literal, SUB_EQUALITY)) {
+ TNode lhs, rhs;
+ switch (literal.getKind()) {
+ case kind::EQUAL:
lhs = literal[0];
+ rhs = literal[1];
+ break;
+ case kind::NOT:
+ if (literal[0].getKind() == kind::EQUAL) {
+ // Disequalities
+ d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+ return;
+ } else {
+ // Predicates
+ lhs = literal[0];
+ rhs = d_false;
+ break;
+ }
+ case kind::CONST_BOOLEAN:
+ // we get to explain true = false, since we set false to be the trigger of this
+ lhs = d_true;
rhs = d_false;
break;
- }
- case kind::CONST_BOOLEAN:
- // we get to explain true = false, since we set false to be the trigger of this
- lhs = d_true;
- rhs = d_false;
- break;
- default:
- Unreachable();
+ default:
+ Unreachable();
+ }
+ d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+ } else {
+ Assert(propagatedBy(literal, SUB_BITBLASTER));
+ d_bitblaster->explain(literal, assumptions);
}
- d_equalityEngine.explainEquality(lhs, rhs, assumptions);
}
Node TheoryBV::explain(TNode node) {
BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
std::vector<TNode> assumptions;
+
+ // Ask for the explanation
explain(node, assumptions);
+ // this means that it is something true at level 0
+ if (assumptions.size() == 0) {
+ return utils::mkTrue();
+ }
+ // return the explanation
return mkAnd(assumptions);
}
void TheoryBV::addSharedTerm(TNode t) {
Debug("bitvector::sharing") << spaces(getSatContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
- if (d_useEqualityEngine) {
+ d_sharedTermsSet.insert(t);
+ if (!Options::current()->bitvector_eager_bitblast && d_useEqualityEngine) {
d_equalityEngine.addTriggerTerm(t);
}
}
@@ -441,6 +445,10 @@ void TheoryBV::addSharedTerm(TNode t) {
EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
{
+ if (Options::current()->bitvector_eager_bitblast) {
+ return EQUALITY_UNKNOWN;
+ }
+
if (d_useEqualityEngine) {
if (d_equalityEngine.areEqual(a, b)) {
// The terms are implied to be equal
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c4953213d..0ced179ec 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -66,7 +66,7 @@ private:
/** Context dependent set of atoms we already propagated */
context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
-
+ context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
@@ -74,8 +74,6 @@ public:
void preRegisterTerm(TNode n);
- //void registerTerm(TNode n) { }
-
void check(Effort e);
Node explain(TNode n);
@@ -84,7 +82,6 @@ public:
std::string identify() const { return std::string("TheoryBV"); }
- //Node preprocessTerm(TNode term);
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
private:
@@ -110,14 +107,14 @@ private:
bool notify(TNode propagation) {
Debug("bitvector") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
// Just forward to bv
- return d_bv.propagate(propagation);
+ return d_bv.storePropagation(propagation, SUB_EQUALITY);
}
void notify(TNode t1, TNode t2) {
Debug("arrays") << spaces(d_bv.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
// Propagate equality between shared terms
Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
- d_bv.propagate(t1.eqNode(t2));
+ d_bv.storePropagation(t1.eqNode(t2), SUB_EQUALITY);
}
};
@@ -141,16 +138,38 @@ private:
context::CDQueue<Node> d_toBitBlast;
+ enum SubTheory {
+ SUB_EQUALITY = 1,
+ SUB_BITBLASTER = 2
+ };
+
+ /**
+ * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
+ * properly.
+ */
+ typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
+ PropagatedMap d_propagatedBy;
+
+ bool propagatedBy(TNode literal, SubTheory subtheory) const {
+ PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
+ if (find == d_propagatedBy.end()) return false;
+ else return (*find).second == subtheory;
+ }
+
/** Should be called to propagate the literal. */
- bool propagate(TNode literal);
+ bool storePropagation(TNode literal, SubTheory subtheory);
- /** Explain why this literal is true by adding assumptions */
+ /**
+ * Explains why this literal (propagated by subtheory) is true by adding assumptions.
+ */
void explain(TNode literal, std::vector<TNode>& assumptions);
void addSharedTerm(TNode t);
EqualityStatus getEqualityStatus(TNode a, TNode b);
+ friend class Bitblaster;
+
public:
void propagate(Effort e);
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 38547ad99..78835b75c 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -326,7 +326,10 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) {
++ it;
}
- Assert(expandedNodes.size() > 0);
+ if (expandedNodes.size() == 0) {
+ return mkTrue();
+ }
+
if (expandedNodes.size() == 1) {
return *expandedNodes.begin();
}
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 1ed4525f4..75426cba4 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -103,6 +103,10 @@ void PreRegisterVisitor::start(TNode node) {
}
bool PreRegisterVisitor::done(TNode node) {
+// <<<<<<< .working
+// d_engine->markActive(d_theories[node]);
+// =======
+// >>>>>>> .merge-right.r3396
return d_multipleTheories;
}
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index cde65aa0f..1ed1f99ff 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -45,6 +45,7 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level){
void Theory::addSharedTermInternal(TNode n) {
Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
+ Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
d_sharedTerms.push_back(n);
addSharedTerm(n);
}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1122e09c6..a3aee985d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -59,6 +59,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
d_decisionRequests(context),
d_decisionRequestsIndex(context, 0),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+ d_inPreregister(false),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms)
{
@@ -84,15 +85,43 @@ TheoryEngine::~TheoryEngine() {
}
void TheoryEngine::preRegister(TNode preprocessed) {
+
if(Dump.isOn("missed-t-propagations")) {
d_possiblePropagations.push_back(preprocessed);
}
- // Pre-register the terms in the atom
- bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
- if (multipleTheories) {
- // Collect the shared terms if there are multipe theories
- NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+ //<<<<<<< .working
+ d_preregisterQueue.push(preprocessed);
+
+ if (!d_inPreregister) {
+ // We're in pre-register
+ d_inPreregister = true;
+
+ // Process the pre-registration queue
+ while (!d_preregisterQueue.empty()) {
+ // Get the next atom to pre-register
+ preprocessed = d_preregisterQueue.front();
+ d_preregisterQueue.pop();
+
+ // Pre-register the terms in the atom
+ bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+ if (multipleTheories) {
+ // Collect the shared terms if there are multipe theories
+ NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+ // Mark the multiple theories flag
+ //d_sharedTermsExist = true;
+ }
+ }
+ // Leaving pre-register
+ d_inPreregister = false;
}
+// =======
+ // Pre-register the terms in the atom
+ // bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
+ // if (multipleTheories) {
+ // // Collect the shared terms if there are multipe theories
+ // NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
+ // //>>>>>>> .merge-right.r3396
+ // }
}
/**
@@ -618,7 +647,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
void TheoryEngine::assertFact(TNode node)
{
Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
- Trace("theory::assertFact") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
+ // Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): d_sharedTermsExist = " << (d_sharedTermsExist ? "true" : "false") << std::endl;
d_propEngine->checkTime();
@@ -629,6 +658,8 @@ void TheoryEngine::assertFact(TNode node)
if (d_logicInfo.isSharingEnabled()) {
+ Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): hasShared terms = " << (d_sharedTerms.hasSharedTerms(atom) ? "true" : "false") << std::endl;
+
// If any shared terms, notify the theories
if (d_sharedTerms.hasSharedTerms(atom)) {
SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 2b4fd24d1..0a0778ebc 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -499,6 +499,16 @@ private:
*/
Node ppTheoryRewrite(TNode term);
+ /**
+ * Queue of nodes for pre-registration.
+ */
+ std::queue<TNode> d_preregisterQueue;
+
+ /**
+ * Boolean flag denoting we are in pre-registration.
+ */
+ bool d_inPreregister;
+
public:
/**
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 4eabf63de..dccd5ba56 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -613,6 +613,13 @@ public:
}
/**
+ * Returns true if this kind is used for congruence closure.
+ */
+ bool isFunctionKind(Kind fun) {
+ return d_congruenceKinds.tst(fun);
+ }
+
+ /**
* Adds a function application term to the database.
*/
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 5eb4f0dc7..cae62570c 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -79,7 +79,6 @@ Node Valuation::getSatValue(TNode n) const {
}
bool Valuation::hasSatValue(TNode n, bool& value) const {
- // Node normalized = Rewriter::rewrite(n);
if (d_engine->getPropEngine()->isSatLiteral(n)) {
return d_engine->getPropEngine()->hasValue(n, value);
} else {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback