From: Dejan Jovanović Date: Mon, 21 Mar 2011 18:55:05 +0000 (+0000) Subject: more bugfixes, some basic propagation, and testcases to cover them X-Git-Tag: cvc5-1.0.0~8638 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75adfe4e8ef1fab4b9cd4c31d40c15e9a1637a5e;p=cvc5.git more bugfixes, some basic propagation, and testcases to cover them --- 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; diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 9182bfbc6..e204a29b5 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -64,7 +64,12 @@ TESTS = \ slice-19.smt \ slice-20.smt \ ext_con_004_001_1024.smt \ - a78test0002.smt + a78test0002.smt \ + a95test0002.smt \ + bitvec0.smt \ + bitvec2.smt \ + bitvec3.smt \ + bitvec5.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/bv/core/a95test0002.smt b/test/regress/regress0/bv/core/a95test0002.smt new file mode 100644 index 000000000..3a4862a24 --- /dev/null +++ b/test/regress/regress0/bv/core/a95test0002.smt @@ -0,0 +1,17 @@ +(benchmark a95test0002.smt + :source { +Bit-vector benchmarks from Dawson Engler's tool contributed by Vijay Ganesh +(vganesh@stanford.edu). Translated into SMT-LIB format by Clark Barrett using +CVC3. + +} + :status sat + :difficulty { 0 } + :category { industrial } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :assumption +(not (not (= (concat bv0[16] (extract[15:0] a)) a))) + :formula +(not false) +) diff --git a/test/regress/regress0/bv/core/bitvec1.smt b/test/regress/regress0/bv/core/bitvec1.smt new file mode 100644 index 000000000..345bc6e6d --- /dev/null +++ b/test/regress/regress0/bv/core/bitvec1.smt @@ -0,0 +1,18 @@ +(benchmark bitvec1.smt + :source { +Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :extrafuns ((b BitVec[32])) + :extrafuns ((c BitVec[32])) + :extrafuns ((res BitVec[32])) + :formula +(flet ($cvc_1 (= (extract[0:0] a) bv1[1])) (flet ($cvc_2 (= (extract[0:0] b) bv1[1])) (let (?cvc_0 (extract[0:0] c)) (flet ($cvc_6 (= ?cvc_0 bv1[1])) (let (?cvc_3 (extract[0:0] res)) (flet ($cvc_4 (= (extract[1:1] a) bv1[1])) (flet ($cvc_5 (= (extract[1:1] b) bv1[1])) (flet ($cvc_8 (if_then_else $cvc_4 (not $cvc_5) $cvc_5)) (let (?cvc_7 (extract[1:1] c)) (let (?cvc_9 (extract[1:1] res)) (not (implies (and (and (and (= (extract[1:0] a) bv1[2]) (= (extract[1:0] b) bv1[2])) (and (if_then_else (and $cvc_1 $cvc_2) $cvc_6 (= ?cvc_0 bv0[1])) (if_then_else (if_then_else $cvc_1 (not $cvc_2) $cvc_2) (= ?cvc_3 bv1[1]) (= ?cvc_3 bv0[1])))) (and (if_then_else (or (and $cvc_4 $cvc_5) (and $cvc_8 $cvc_6) ) (= ?cvc_7 bv1[1]) (= ?cvc_7 bv0[1])) (if_then_else (if_then_else $cvc_6 (not $cvc_8) $cvc_8) (= ?cvc_9 bv1[1]) (= ?cvc_9 bv0[1])))) (and (= (extract[1:0] res) bv2[2]) (= (extract[1:0] c) bv1[2])))))))))))))) +) diff --git a/test/regress/regress0/bv/core/bitvec2.smt b/test/regress/regress0/bv/core/bitvec2.smt new file mode 100644 index 000000000..bb479a5f8 --- /dev/null +++ b/test/regress/regress0/bv/core/bitvec2.smt @@ -0,0 +1,15 @@ +(benchmark bitvec2.smt + :source { +Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrapreds ((a)) + :formula +(not (= (concat bv1[1] (ite a bv0[1] bv1[1])) (ite a bv2[2] bv3[2]))) +) diff --git a/test/regress/regress0/bv/core/bitvec3.smt b/test/regress/regress0/bv/core/bitvec3.smt new file mode 100644 index 000000000..054ec25ac --- /dev/null +++ b/test/regress/regress0/bv/core/bitvec3.smt @@ -0,0 +1,20 @@ +(benchmark bitvec3.smt + :source { +Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :extrafuns ((b BitVec[32])) + :extrafuns ((c1 BitVec[32])) + :extrafuns ((c2 BitVec[32])) + :extrafuns ((out BitVec[32])) + :extrafuns ((carry BitVec[32])) + :formula +(let (?cvc_0 (extract[1:0] b)) (let (?cvc_1 (extract[2:0] c1)) (let (?cvc_3 (concat bv0[1] bv0[2])) (let (?cvc_2 (extract[2:0] c2)) (flet ($cvc_4 (= (extract[0:0] c1) bv1[1])) (flet ($cvc_5 (= (extract[0:0] c2) bv1[1])) (let (?cvc_6 (extract[0:0] carry)) (let (?cvc_7 (extract[1:1] c1)) (flet ($cvc_11 (= ?cvc_7 bv1[1])) (let (?cvc_8 (extract[1:1] c2)) (flet ($cvc_10 (= ?cvc_8 bv0[1])) (flet ($cvc_9 (= ?cvc_7 bv0[1])) (flet ($cvc_12 (= ?cvc_8 bv1[1])) (flet ($cvc_14 (or (and $cvc_11 $cvc_10) (and $cvc_9 $cvc_12) )) (flet ($cvc_13 (= ?cvc_6 bv1[1])) (let (?cvc_15 (extract[1:1] carry)) (let (?cvc_16 (extract[2:2] c1)) (flet ($cvc_20 (= ?cvc_16 bv1[1])) (let (?cvc_17 (extract[2:2] c2)) (flet ($cvc_19 (= ?cvc_17 bv0[1])) (flet ($cvc_18 (= ?cvc_16 bv0[1])) (flet ($cvc_21 (= ?cvc_17 bv1[1])) (flet ($cvc_22 (= ?cvc_15 bv1[1])) (not (implies (and (= (extract[1:0] a) bv3[2]) (= ?cvc_0 bv3[2])) (implies (and (and (and (and (and (and (and (if_then_else (= (extract[0:0] a) bv1[1]) (= ?cvc_1 (concat bv0[1] ?cvc_0)) (= ?cvc_1 ?cvc_3)) (if_then_else (= (extract[1:1] a) bv1[1]) (= ?cvc_2 (concat ?cvc_0 bv0[1])) (= ?cvc_2 ?cvc_3))) (= (extract[0:0] out) (ite (or $cvc_4 $cvc_5 ) bv1[1] bv0[1]))) (= ?cvc_6 (ite (and $cvc_4 $cvc_5) bv1[1] bv0[1]))) (= (extract[1:1] out) (ite (or (and (= ?cvc_6 bv0[1]) $cvc_14) (and $cvc_13 (and $cvc_9 $cvc_10)) ) bv1[1] bv0[1]))) (= ?cvc_15 (ite (or (and $cvc_11 $cvc_12) (and $cvc_13 $cvc_14) ) bv1[1] bv0[1]))) (= (extract[2:2] out) (ite (or (and (= ?cvc_15 bv0[1]) (or (and $cvc_20 $cvc_19) (and $cvc_18 $cvc_21) )) (and $cvc_22 (and $cvc_18 $cvc_19)) ) bv1[1] bv0[1]))) (= (extract[2:2] carry) (ite (or (and $cvc_20 $cvc_21) (and $cvc_22 (or $cvc_20 $cvc_21 )) ) bv1[1] bv0[1]))) (and (= (extract[2:0] out) bv1[3]) (= (extract[2:0] carry) bv6[3])))))))))))))))))))))))))))) +) diff --git a/test/regress/regress0/bv/core/bitvec5.smt b/test/regress/regress0/bv/core/bitvec5.smt new file mode 100644 index 000000000..3b6f2f3b9 --- /dev/null +++ b/test/regress/regress0/bv/core/bitvec5.smt @@ -0,0 +1,19 @@ +(benchmark bitvec5.smt + :source { +Hand-crafted bit-vector benchmarks. Some are from the SVC benchmark suite. +Contributed by Vijay Ganesh (vganesh@stanford.edu). Translated into SMT-LIB +format by Clark Barrett using CVC3. + +} + :status unsat + :difficulty { 0 } + :category { crafted } + :logic QF_BV + :extrafuns ((a BitVec[32])) + :extrafuns ((b BitVec[32])) + :extrafuns ((c BitVec[32])) + :extrafuns ((d BitVec[32])) + :extrafuns ((e BitVec[32])) + :formula +(not (and (implies (and (and (= (extract[31:0] a) (extract[31:0] b)) (= (extract[31:16] a) (extract[15:0] c))) (= (extract[31:8] b) (extract[23:0] d))) (= (extract[11:8] c) (extract[19:16] d))) (implies (= (extract[30:0] e) (extract[31:1] e)) (= (extract[0:0] e) (extract[31:31] e))))) +)