From c43514fef548f977e88e2986c2f993b975830cc2 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Thu, 14 Jun 2012 21:08:28 +0000 Subject: [PATCH] bug fixes in justification heuristic * remove assert iteSkolemMap gives ite-s (not true with repeatSimp) * handle a corner case in findSplitter triggered by repeatSimp --- src/decision/justification_heuristic.cpp | 27 +++++++- test/regress/regress0/decision/Makefile.am | 9 ++- .../regress0/decision/error122.delta01.smt | 19 ++++++ test/regress/regress0/decision/error122.smt | 53 +++++++++++++++ .../regress0/decision/error20.delta01.smt | 19 ++++++ test/regress/regress0/decision/error20.smt | 66 +++++++++++++++++++ 6 files changed, 189 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/decision/error122.delta01.smt create mode 100644 test/regress/regress0/decision/error122.smt create mode 100644 test/regress/regress0/decision/error20.delta01.smt create mode 100644 test/regress/regress0/decision/error20.smt diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 68c11295f..cd69eeb74 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -133,6 +133,13 @@ bool JustificationHeuristic::findSplitterRec(TNode node, node = node[0]; } + if(Debug.isOn("decision")) { + if(checkJustified(node)) + Debug("decision") << " justified, returning" << std::endl; + if(d_visited.find(node) != d_visited.end()) + Debug("decision") << " visited, returning" << std::endl; + } + /* Base case */ if (checkJustified(node) || d_visited.find(node) != d_visited.end()) return false; @@ -183,11 +190,19 @@ bool JustificationHeuristic::findSplitterRec(TNode node, Debug("jh-ite") << " ite size = " << l.size() << std::endl; d_visited.insert(node); for(unsigned i = 0; i < l.size(); ++i) { - Assert(l[i].getKind() == kind::ITE, "Expected ITE"); Debug("jh-ite") << " i = " << i << " l[i] = " << l[i] << std::endl; if (checkJustified(l[i])) continue; + // Assert(l[i].getKind() == kind::ITE, "Expected ITE"); + if(l[i].getKind() != kind::ITE) { + //this might happen because of repeatSimp + Debug("jh-ite") << " not an ite, must have got repeatSimp-ed" + << std::endl; + findSplitterRec(l[i], SAT_VALUE_TRUE, litDecision); + continue; + } + SatValue desiredVal = SAT_VALUE_TRUE; //NOTE: Reusing variable #ifdef CVC4_ASSERTIONS bool litPresent = d_decisionEngine->hasSatLiteral(l[i]); @@ -206,6 +221,16 @@ bool JustificationHeuristic::findSplitterRec(TNode node, if(findSplitterRec(l[i][0], ifDesiredVal, litDecision)) { return true; } + + // Handle special case when if node itself is visited. Decide + // on it. + if(d_visited.find(l[i][0]) != d_visited.end()) { + Assert(d_decisionEngine->hasSatLiteral(l[i][0])); + SatVariable v = d_decisionEngine->getSatLiteral(l[i][0]).getSatVariable(); + *litDecision = SatLiteral(v, ifDesiredVal != SAT_VALUE_TRUE ); + return true; + } + Assert(false, "No controlling input found (1)"); } else { diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index b098476fc..de3ccd60a 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -22,11 +22,14 @@ TESTS = \ uflia-error0.smt2 \ uflia-xs-09-16-3-4-1-5.smt \ uflia-xs-09-16-3-4-1-5.delta03.smt \ - aufbv-fuzz01.smt \ - bug347.smt + aufbv-fuzz01.smt \ + bug347.smt \ + error20.smt \ + error20.delta01.smt \ + error122.smt \ + error122.delta01.smt # Incorrect answers: -# aufbv-fuzz01.smt \ # EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/decision/error122.delta01.smt b/test/regress/regress0/decision/error122.delta01.smt new file mode 100644 index 000000000..7c8f930b8 --- /dev/null +++ b/test/regress/regress0/decision/error122.delta01.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v0 BitVec[16])) +:extrafuns ((a2 Array[16:7])) +:status sat +:formula +(let (?n1 bv0[7]) +(let (?n2 (store a2 v0 ?n1)) +(let (?n3 bv1[16]) +(let (?n4 (select ?n2 ?n3)) +(flet ($n5 (bvult ?n1 ?n4)) +(let (?n6 bv1[1]) +(let (?n7 bv0[1]) +(let (?n8 (ite $n5 ?n6 ?n7)) +(let (?n9 (sign_extend[15] ?n8)) +(flet ($n10 (distinct v0 ?n9)) +(flet ($n11 (not $n10)) +$n11 +)))))))))))) diff --git a/test/regress/regress0/decision/error122.smt b/test/regress/regress0/decision/error122.smt new file mode 100644 index 000000000..2503ba01e --- /dev/null +++ b/test/regress/regress0/decision/error122.smt @@ -0,0 +1,53 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unsat +:extrafuns ((v0 BitVec[16])) +:extrafuns ((a1 Array[16:4])) +:extrafuns ((a2 Array[16:7])) +:formula +(let (?e3 bv8911[14]) +(let (?e4 (ite (bvsgt (zero_extend[2] ?e3) v0) bv1[1] bv0[1])) +(let (?e5 (store a2 v0 (extract[13:7] v0))) +(let (?e6 (store a2 (zero_extend[15] ?e4) (zero_extend[6] ?e4))) +(let (?e7 (select ?e5 (zero_extend[2] ?e3))) +(let (?e8 (store ?e5 (sign_extend[2] ?e3) (sign_extend[6] ?e4))) +(let (?e9 (select a1 v0)) +(let (?e10 (store ?e8 (zero_extend[15] ?e4) (extract[6:0] v0))) +(let (?e11 (bvadd (zero_extend[6] ?e4) ?e7)) +(let (?e12 (ite (bvult ?e11 ?e7) bv1[1] bv0[1])) +(let (?e13 (ite (bvult (zero_extend[3] ?e12) ?e9) bv1[1] bv0[1])) +(let (?e14 (bvlshr (sign_extend[12] ?e9) v0)) +(let (?e15 (ite (= bv1[1] (extract[12:12] ?e3)) ?e14 ?e14)) +(flet ($e16 (bvslt ?e15 v0)) +(flet ($e17 (bvult (sign_extend[15] ?e4) ?e14)) +(flet ($e18 (= (sign_extend[15] ?e12) ?e15)) +(flet ($e19 (distinct (sign_extend[15] ?e12) v0)) +(flet ($e20 (bvugt ?e11 ?e11)) +(flet ($e21 (bvule ?e13 ?e13)) +(flet ($e22 (bvslt ?e15 (sign_extend[9] ?e11))) +(flet ($e23 (bvslt (zero_extend[9] ?e11) v0)) +(flet ($e24 (bvult v0 (sign_extend[15] ?e12))) +(flet ($e25 (bvslt ?e7 (sign_extend[6] ?e4))) +(flet ($e26 (bvule (zero_extend[12] ?e9) ?e15)) +(flet ($e27 (bvuge ?e13 ?e13)) +(flet ($e28 (distinct (zero_extend[6] ?e12) ?e7)) +(flet ($e29 (distinct ?e3 (sign_extend[13] ?e12))) +(flet ($e30 (xor $e27 $e17)) +(flet ($e31 (or $e25 $e28)) +(flet ($e32 (iff $e31 $e21)) +(flet ($e33 (and $e18 $e22)) +(flet ($e34 (iff $e30 $e33)) +(flet ($e35 (and $e24 $e24)) +(flet ($e36 (and $e29 $e20)) +(flet ($e37 (and $e34 $e26)) +(flet ($e38 (iff $e36 $e16)) +(flet ($e39 (or $e38 $e32)) +(flet ($e40 (not $e19)) +(flet ($e41 (xor $e23 $e35)) +(flet ($e42 (and $e41 $e40)) +(flet ($e43 (implies $e42 $e37)) +(flet ($e44 (not $e43)) +(flet ($e45 (and $e39 $e44)) +$e45 +)))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/decision/error20.delta01.smt b/test/regress/regress0/decision/error20.delta01.smt new file mode 100644 index 000000000..dfa582be9 --- /dev/null +++ b/test/regress/regress0/decision/error20.delta01.smt @@ -0,0 +1,19 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v0 BitVec[16])) +:extrafuns ((v1 BitVec[1])) +:extrafuns ((a4 Array[1:7])) +:status sat +:formula +(let (?n1 (select a4 v1)) +(let (?n2 bv0[7]) +(flet ($n3 (bvsle ?n1 ?n2)) +(let (?n4 bv0[16]) +(let (?n5 bv0[1]) +(flet ($n6 (= v1 ?n5)) +(let (?n7 (ite $n6 ?n4 v0)) +(flet ($n8 (= ?n4 ?n7)) +(flet ($n9 (not $n8)) +(flet ($n10 (and $n3 $n9)) +$n10 +))))))))))) diff --git a/test/regress/regress0/decision/error20.smt b/test/regress/regress0/decision/error20.smt new file mode 100644 index 000000000..adc638500 --- /dev/null +++ b/test/regress/regress0/decision/error20.smt @@ -0,0 +1,66 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[16])) +:extrafuns ((v1 BitVec[1])) +:extrafuns ((a2 Array[12:10])) +:extrafuns ((a3 Array[14:11])) +:extrafuns ((a4 Array[1:7])) +:formula +(let (?e5 bv1[1]) +(let (?e6 (ite (= bv1[1] (extract[0:0] v1)) (sign_extend[15] ?e5) v0)) +(let (?e7 (store a4 (extract[4:4] v0) (extract[9:3] v0))) +(let (?e8 (store ?e7 ?e5 (extract[12:6] v0))) +(let (?e9 (store ?e8 v1 (sign_extend[6] ?e5))) +(let (?e10 (select a4 v1)) +(let (?e11 (store ?e8 ?e5 (zero_extend[6] v1))) +(let (?e12 (select ?e8 v1)) +(let (?e13 (store a2 (extract[14:3] v0) (zero_extend[3] ?e10))) +(let (?e14 (rotate_right[0] v1)) +(let (?e15 (rotate_right[3] ?e10)) +(let (?e16 (ite (bvsge ?e12 (zero_extend[6] v1)) bv1[1] bv0[1])) +(let (?e17 (repeat[5] ?e14)) +(let (?e18 (bvsdiv (sign_extend[9] ?e15) ?e6)) +(let (?e19 (bvmul (zero_extend[15] ?e5) v0)) +(flet ($e20 (= (zero_extend[15] ?e5) ?e18)) +(flet ($e21 (bvugt (zero_extend[9] ?e10) ?e19)) +(flet ($e22 (bvsgt ?e15 (zero_extend[6] v1))) +(flet ($e23 (bvslt ?e14 ?e16)) +(flet ($e24 (bvugt ?e19 (zero_extend[15] v1))) +(flet ($e25 (distinct ?e12 ?e12)) +(flet ($e26 (bvule ?e17 (sign_extend[4] ?e5))) +(flet ($e27 (bvsle ?e18 (zero_extend[15] ?e16))) +(flet ($e28 (bvsle ?e10 ?e15)) +(flet ($e29 (bvsgt ?e12 (zero_extend[6] ?e16))) +(flet ($e30 (bvsgt (sign_extend[4] ?e5) ?e17)) +(flet ($e31 (bvsle ?e17 (zero_extend[4] ?e14))) +(flet ($e32 (bvult (zero_extend[11] ?e17) ?e6)) +(flet ($e33 (bvult ?e5 ?e5)) +(flet ($e34 (bvugt ?e12 (sign_extend[2] ?e17))) +(flet ($e35 (bvsle (sign_extend[6] v1) ?e15)) +(flet ($e36 (bvule ?e15 (zero_extend[6] ?e14))) +(flet ($e37 (bvsgt v0 ?e6)) +(flet ($e38 (if_then_else $e23 $e25 $e26)) +(flet ($e39 (iff $e33 $e35)) +(flet ($e40 (or $e21 $e36)) +(flet ($e41 (or $e20 $e32)) +(flet ($e42 (and $e22 $e39)) +(flet ($e43 (not $e41)) +(flet ($e44 (implies $e24 $e31)) +(flet ($e45 (or $e42 $e44)) +(flet ($e46 (iff $e27 $e37)) +(flet ($e47 (or $e29 $e46)) +(flet ($e48 (not $e28)) +(flet ($e49 (and $e47 $e43)) +(flet ($e50 (iff $e40 $e30)) +(flet ($e51 (xor $e34 $e50)) +(flet ($e52 (iff $e45 $e51)) +(flet ($e53 (if_then_else $e49 $e49 $e52)) +(flet ($e54 (or $e53 $e38)) +(flet ($e55 (iff $e54 $e54)) +(flet ($e56 (and $e48 $e55)) +(flet ($e57 (and $e56 (not (= ?e6 bv0[16])))) +(flet ($e58 (and $e57 (not (= ?e6 (bvnot bv0[16]))))) +$e58 +))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2