diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bv_subtheory_eq.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 57 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 23 |
3 files changed, 27 insertions, 59 deletions
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp index 807d90137..98678a9b4 100644 --- a/src/theory/bv/bv_subtheory_eq.cpp +++ b/src/theory/bv/bv_subtheory_eq.cpp @@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v } bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) { - BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl; + BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl; if (value) { return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY); } else { @@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool } bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; + Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl; if (value) { return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); } else { @@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod } bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + 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); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 251650bf2..30493737a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) { } // go through stored propagations - for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); - d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) - { + for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) { TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex]; - Node normalized = Rewriter::rewrite(literal); - - TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - bool isSharedLiteral = (atom.getKind() == kind::EQUAL && - (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() && - d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())); - - // Check if this is a SAT literal - if (d_valuation.isSatLiteral(normalized)) { - bool satValue = false; - if (!d_valuation.hasSatValue(normalized, satValue) || satValue) { - // check if we already propagated the negation - Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal); - if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) { - Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; - // we are in conflict - std::vector<TNode> assumptions; - explain(literal, assumptions); - explain(negLiteral, assumptions); - setConflict(mkAnd(assumptions)); - return; - } - // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version - // shared literals are handled below - if (!isSharedLiteral && !satValue) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl; - d_out->propagate(normalized); - d_alreadyPropagatedSet.insert(normalized); - return; - } - } 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); - setConflict(mkAnd(assumptions)); - return; - } - } - // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one) - if (isSharedLiteral) { - BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl; - d_out->propagate(literal); - d_alreadyPropagatedSet.insert(literal); - } + d_out->propagate(literal); } } @@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory) void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) { // Ask the appropriate subtheory for the explanation if (propagatedBy(literal, SUB_EQUALITY)) { + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl; d_equalitySolver.explain(literal, assumptions); } else { Assert(propagatedBy(literal, SUB_BITBLAST)); + BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl; d_bitblastSolver.explain(literal, assumptions); } } Node TheoryBV::explain(TNode node) { - BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl; std::vector<TNode> assumptions; // Ask for the explanation diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 3736da639..c456ef73f 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) { } inline Node mkAnd(std::vector<TNode>& children) { - if (children.size() > 1) { - return NodeManager::currentNM()->mkNode(kind::AND, children); - } else { - return children[0]; + std::set<TNode> distinctChildren; + distinctChildren.insert(children.begin(), children.end()); + + if (children.size() == 0) { + return mkTrue(); + } + + if (children.size() == 1) { + return *children.begin(); } + + NodeBuilder<> conjunction(kind::AND); + std::set<TNode>::const_iterator it = distinctChildren.begin(); + std::set<TNode>::const_iterator it_end = distinctChildren.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; } inline Node mkSortedNode(Kind kind, std::vector<Node>& children) { |