From 75adfe4e8ef1fab4b9cd4c31d40c15e9a1637a5e Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Mon, 21 Mar 2011 18:55:05 +0000 Subject: more bugfixes, some basic propagation, and testcases to cover them --- src/prop/cnf_stream.cpp | 2 +- src/theory/bv/equality_engine.h | 12 +++++++++--- src/theory/bv/kinds | 2 +- src/theory/bv/theory_bv.cpp | 23 +++++++++++++++++++---- src/theory/bv/theory_bv.h | 6 ++++-- src/theory/bv/theory_bv_utils.h | 13 ++++++++++++- 6 files changed, 46 insertions(+), 12 deletions(-) (limited to 'src') diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 0c692501f..99cd26297 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -147,7 +147,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { SatLiteral CnfStream::getLiteral(TNode node) { TranslationCache::iterator find = d_translationCache.find(node); - Assert(find != d_translationCache.end(), "Literal not in the CNF Cache"); + Assert(find != d_translationCache.end(), "Literal not in the CNF Cache: ", node.toString().c_str()); SatLiteral literal = find->second.literal; Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl; return literal; 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::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 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::edges template void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector& 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(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 assertions; - d_eqEngine.getExplanation(equality[0], equality[1], assertions); - assertions.push_back(equality.notNode()); - d_out->conflict(mkAnd(assertions)); + std::vector explanation; + d_eqEngine.getExplanation(equality[0], equality[1], explanation); + std::set 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 reasons; + d_eqEngine.getExplanation(node[0], node[1], reasons); + std::set 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 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& 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& children) { @@ -90,6 +94,13 @@ inline void getConjuncts(TNode node, std::set& conjuncts) { } } +inline void getConjuncts(std::vector& nodes, std::set& conjuncts) { + for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++ i) { + getConjuncts(nodes[i], conjuncts); + } +} + + inline Node mkConjunction(const std::set nodes) { std::set expandedNodes; -- cgit v1.2.3