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;
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]);
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 {
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)
--- /dev/null
+(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
+))))))))))))
--- /dev/null
+(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
+))))))))))))))))))))))))))))))))))))))))))))
+
--- /dev/null
+(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
+)))))))))))
--- /dev/null
+(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
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))
+
projects / cvc5.git / commitdiff