diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 18:55:05 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-21 18:55:05 +0000 |
commit | 75adfe4e8ef1fab4b9cd4c31d40c15e9a1637a5e (patch) | |
tree | dc866579086454092edaecd78bcfadf2da03b08c /src/theory | |
parent | 7f49a7aedc16cb46216f92d00881cd3485acc206 (diff) |
more bugfixes, some basic propagation, and testcases to cover them
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/bv/equality_engine.h | 12 | ||||
-rw-r--r-- | src/theory/bv/kinds | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 23 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 13 |
5 files changed, 45 insertions, 11 deletions
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 6fa1b7d22..5d4212849 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -30,6 +30,7 @@ #include "util/output.h" #include "util/stats.h" #include "theory/rewriter.h" +#include "theory/bv/theory_bv_utils.h" namespace CVC4 { namespace theory { @@ -447,7 +448,11 @@ bool EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::addEquality( // Check for constants if (d_nodes[t1classId].getMetaKind() == kind::metakind::CONSTANT && d_nodes[t2classId].getMetaKind() == kind::metakind::CONSTANT) { - d_notify.conflict(reason); + std::vector<TNode> reasons; + getExplanation(t1, d_nodes[t1classId], reasons); + getExplanation(t2, d_nodes[t2classId], reasons); + reasons.push_back(reason); + d_notify.conflict(utils::mkAnd(reasons)); return false; } @@ -665,12 +670,13 @@ std::string EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::edges template <typename OwnerClass, typename NotifyClass, typename UnionFindPreferences> void EqualityEngine<OwnerClass, NotifyClass, UnionFindPreferences>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const { - Assert(equalities.empty()); - Assert(t1 != t2); Assert(getRepresentative(t1) == getRepresentative(t2)); Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl; + // If the nodes are the same, we're done + if (t1 == t2) return; + const_cast<EqualityEngine*>(this)->backtrack(); // Queue for the BFS containing nodes diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 2df4c361c..381e90d47 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -6,7 +6,7 @@ theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" -properties finite check +properties finite check propagate rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h" diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 2d989a563..51de8df28 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -139,10 +139,12 @@ bool TheoryBV::triggerEquality(size_t triggerId) { // If we have a negation asserted, we have a confict if (d_assertions.contains(equality.notNode())) { - vector<TNode> assertions; - d_eqEngine.getExplanation(equality[0], equality[1], assertions); - assertions.push_back(equality.notNode()); - d_out->conflict(mkAnd(assertions)); + std::vector<TNode> explanation; + d_eqEngine.getExplanation(equality[0], equality[1], explanation); + std::set<TNode> assumptions; + assumptions.insert(equality.notNode()); + utils::getConjuncts(explanation, assumptions); + d_out->conflict(utils::mkConjunction(assumptions)); return false; } @@ -169,3 +171,16 @@ Node TheoryBV::getValue(TNode n, Valuation* valuation) { Unhandled(n.getKind()); } } + +void TheoryBV::explain(TNode node) { + Debug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl; + if(node.getKind() == kind::EQUAL) { + std::vector<TNode> reasons; + d_eqEngine.getExplanation(node[0], node[1], reasons); + std::set<TNode> simpleReasons; + utils::getConjuncts(reasons, simpleReasons); + d_out->explanation(utils::mkConjunction(simpleReasons)); + return; + } + Unreachable(); +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 474c4d0cd..f2c2fa332 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -45,7 +45,9 @@ public: return d_theoryBV.triggerEquality(triggerId); } void conflict(Node explanation) { - d_theoryBV.d_out->conflict(explanation); + std::set<TNode> assumptions; + utils::getConjuncts(explanation, assumptions); + d_theoryBV.d_out->conflict(utils::mkConjunction(assumptions)); } }; @@ -119,7 +121,7 @@ public: void propagate(Effort e) { } - void explain(TNode n) { } + void explain(TNode n); Node getValue(TNode n, Valuation* valuation); diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index ad924f8a0..781b5cddb 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -50,7 +50,11 @@ inline Node mkFalse() { } inline Node mkAnd(std::vector<TNode>& children) { - return NodeManager::currentNM()->mkNode(kind::AND, children); + if (children.size() > 1) { + return NodeManager::currentNM()->mkNode(kind::AND, children); + } else { + return children[0]; + } } inline Node mkAnd(std::vector<Node>& children) { @@ -90,6 +94,13 @@ inline void getConjuncts(TNode node, std::set<TNode>& conjuncts) { } } +inline void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts) { + for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) { + getConjuncts(nodes[i], conjuncts); + } +} + + inline Node mkConjunction(const std::set<TNode> nodes) { std::set<TNode> expandedNodes; |