From 7e3676e24ac31d1c9b3f71c8a38f041142ff1069 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Jan 2016 13:25:14 +0000 Subject: [PATCH 1/2] bugfix for ML example --- examples/ml/ml_example.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index df062bde4..5b1c05069 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -287,16 +287,15 @@ let fpa_example ( ctx : context ) = (* ((_ to_fp 11 53) #x401c000000000000)) *) (* ((_ to_fp 11 53) RTZ 1.75 2))) *) (* ((_ to_fp 11 53) RTZ 7.0))) *) - let c1 = (mk_fp ctx - (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) - (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52)) - (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in + let c1 = (mk_fp ctx (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1)) + (mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11)) + (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))) in let c2 = (mk_to_fp_bv ctx (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) (mk_sort ctx 11 53)) in let c3 = (mk_to_fp_int_real ctx (RoundingMode.mk_rtz ctx) - (mk_numeral_string ctx "2" (Integer.mk_sort ctx)) + (mk_numeral_string ctx "2" (Integer.mk_sort ctx)) (mk_numeral_string ctx "1.75" (Real.mk_sort ctx)) (FloatingPoint.mk_sort ctx 11 53)) in let c4 = (mk_to_fp_real ctx (RoundingMode.mk_rtz ctx) From 3d01246f71ced42b8da55e8ae3866d2820b35a0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2016 08:17:18 -0800 Subject: [PATCH 2/2] Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed. Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index cef8d5fc7..e4f698914 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1176,31 +1176,37 @@ namespace smt { unsigned idx = entry.second; if (m_wpos[v] == idx) - find_wpos(v); - + find_wpos(v); literal_vector & bits = m_bits[v]; literal bit = bits[idx]; - lbool val = ctx.get_assignment(bit); + lbool val = ctx.get_assignment(bit); + if (val == l_undef) { + continue; + } theory_var v2 = next(v); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";); + literal antecedent = bit; + + if (val == l_false) { + antecedent.neg(); + } while (v2 != v) { literal_vector & bits2 = m_bits[v2]; literal bit2 = bits2[idx]; SASSERT(bit != ~bit2); lbool val2 = ctx.get_assignment(bit2); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); + if (val != val2) { - literal antecedent = bit; literal consequent = bit2; if (val == l_false) { - antecedent.neg(); consequent.neg(); } - SASSERT(ctx.get_assignment(antecedent) == l_true); assign_bit(consequent, v, v2, idx, antecedent, false); if (ctx.inconsistent()) { TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";); + m_prop_queue.reset(); return; } }