mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-01-08 13:39:34 -08:00
commit 52284922a0
2 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

7
examples/ml/ml_example.ml
View file

@ -287,10 +287,9 @@ let fpa_example ( ctx : context ) =
(* ((_ to_fp 11 53) #x401c000000000000)) *) (* ((_ to_fp 11 53) #x401c000000000000)) *)
(* ((_ to_fp 11 53) RTZ 1.75 2))) *) (* ((_ to_fp 11 53) RTZ 1.75 2))) *)
(* ((_ to_fp 11 53) RTZ 7.0))) *) (* ((_ to_fp 11 53) RTZ 7.0))) *)
let c1 = (mk_fp ctx let c1 = (mk_fp ctx (mk_numeral_string ctx "0" (BitVector.mk_sort ctx 1))
(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)) (mk_numeral_string ctx "3377699720527872" (BitVector.mk_sort ctx 52))) in
(mk_numeral_string ctx "1025" (BitVector.mk_sort ctx 11))) in
let c2 = (mk_to_fp_bv ctx let c2 = (mk_to_fp_bv ctx
(mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64)) (mk_numeral_string ctx "4619567317775286272" (BitVector.mk_sort ctx 64))
(mk_sort ctx 11 53)) in (mk_sort ctx 11 53)) in

14
src/smt/theory_bv.cpp
View file

@ -1178,29 +1178,35 @@ namespace smt {
if (m_wpos[v] == idx) if (m_wpos[v] == idx)
find_wpos(v); find_wpos(v);
literal_vector & bits = m_bits[v]; literal_vector & bits = m_bits[v];
literal bit = bits[idx]; 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); theory_var v2 = next(v);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";); 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) { while (v2 != v) {
literal_vector & bits2 = m_bits[v2]; literal_vector & bits2 = m_bits[v2];
literal bit2 = bits2[idx]; literal bit2 = bits2[idx];
SASSERT(bit != ~bit2); SASSERT(bit != ~bit2);
lbool val2 = ctx.get_assignment(bit2); lbool val2 = ctx.get_assignment(bit2);
TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
if (val != val2) { if (val != val2) {
literal antecedent = bit;
literal consequent = bit2; literal consequent = bit2;
if (val == l_false) { if (val == l_false) {
antecedent.neg();
consequent.neg(); consequent.neg();
} }
SASSERT(ctx.get_assignment(antecedent) == l_true);
assign_bit(consequent, v, v2, idx, antecedent, false); assign_bit(consequent, v, v2, idx, antecedent, false);
if (ctx.inconsistent()) { if (ctx.inconsistent()) {
TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";); TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";);
m_prop_queue.reset();
return; return;
} }
} }