diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 19:09:37 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 19:09:37 +0000 |
commit | da1e7aaacab8dd4e9b80b752f362d190c1472543 (patch) | |
tree | 637efe507b1a178420ef363464a9aa63bdfb7da6 /src | |
parent | b47e13e905458f6fbd112d3d201684f2766be6ef (diff) |
fix for clark's bug
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 31 |
1 files changed, 12 insertions, 19 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 811600ad4..273b406e6 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -225,27 +225,20 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) d_propagatedBy[literal] = subtheory; } - // See if the literal has been asserted already - bool satValue = false; - bool hasSatValue = d_valuation.hasSatValue(literal, satValue); - - // If asserted, we might be in conflict - if (hasSatValue && !satValue) { - Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => conflict" << std::endl; - std::vector<TNode> assumptions; - Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode(); - assumptions.push_back(negatedLiteral); - explain(literal, assumptions); - setConflict(mkAnd(assumptions)); - return false; + // Propagate differs depending on the subtheory + // * bitblaster needs to be left alone until it's done, otherwise it doesn't know how to explain + // * equality engine can propagate eagerly + bool ok = true; + if (subtheory == SUB_EQUALITY) { + d_out->propagate(literal); + if (!ok) { + setConflict(); + } + } else { + d_literalsToPropagate.push_back(literal); } + return ok; - // Nothing, just enqueue it for propagation and mark it as asserted already - Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => enqueuing for propagation" << std::endl; - d_literalsToPropagate.push_back(literal); - - // No conflict - return true; }/* TheoryBV::propagate(TNode) */ |