diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index d977ff40151..33753254451 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -166,11 +166,12 @@ namespace bv { void sls::try_repair_up(app* e) { m_repair_up.remove(e->get_id()); - if (m_terms.is_assertion(e)) { - m_repair_down.insert(e->get_id()); - } + if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) + m_repair_down.insert(e->get_id()); else { - m_eval.repair_up(e); + if (!eval_is_correct(e)) { + verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; + } SASSERT(eval_is_correct(e)); for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 0693ce7cc7e..cc754997f7a 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -12,6 +12,7 @@ Module Name: --*/ #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include "ast/sls/bv_sls.h" namespace bv { @@ -178,7 +179,9 @@ namespace bv { } return m.are_equal(a, b); } + case OP_DISTINCT: default: + verbose_stream() << mk_bounded_pp(e, m) << "\n"; UNREACHABLE(); break; } @@ -511,14 +514,16 @@ namespace bv { } case OP_SIGN_EXT: { auto& a = wval0(e->get_arg(0)); - val.set(a.bits); + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, a.get(a.bits, i)); bool sign = a.sign(); val.set_range(val.bits, a.bw, val.bw, sign); break; } case OP_ZERO_EXT: { auto& a = wval0(e->get_arg(0)); - val.set(a.bits); + for (unsigned i = 0; i < a.bw; ++i) + val.set(val.bits, i, a.get(a.bits, i)); val.set_range(val.bits, a.bw, val.bw, false); break; } @@ -1268,6 +1273,7 @@ namespace bv { a.set(m_tmp, i, e.get(e.bits, i - sh)); for (unsigned i = 0; i < sh; ++i) a.set(m_tmp, i, a.get(a.bits, i)); + a.clear_overflow_bits(m_tmp); return a.try_set(m_tmp); } } @@ -1500,7 +1506,7 @@ namespace bv { } bool sls_eval::try_repair_zero_ext(bvval const& e, bvval& a) { - for (unsigned i = 0; i < e.bw; ++i) + for (unsigned i = 0; i < a.bw; ++i) if (!a.get(a.fixed, i)) a.set(a.bits, i, e.get(e.bits, i)); return true; @@ -1509,21 +1515,25 @@ namespace bv { bool sls_eval::try_repair_concat(bvval const& e, bvval& a, bvval& b, unsigned i) { if (i == 0) { for (unsigned i = 0; i < a.bw; ++i) - if (!a.get(a.fixed, i)) - a.set(a.bits, i, e.get(e.bits, i + b.bw)); + a.set(m_tmp, i, e.get(e.bits, i + b.bw)); + a.clear_overflow_bits(m_tmp); + a.set_repair(random_bool(), m_tmp); } else { for (unsigned i = 0; i < b.bw; ++i) - if (!b.get(b.fixed, i)) - b.set(b.bits, i, e.get(e.bits, i)); + b.set(m_tmp, i, e.get(e.bits, i)); + b.clear_overflow_bits(m_tmp); + b.set_repair(random_bool(), m_tmp); } return true; } bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) { for (unsigned i = 0; i < e.bw; ++i) - if (!a.get(a.fixed, i + lo)) - a.set(a.bits, i + lo, e.get(e.bits, i)); + if (a.get(a.fixed, i + lo) && a.get(a.bits, i + lo) != e.get(e.bits, i)) + return false; + for (unsigned i = 0; i < e.bw; ++i) + a.set(a.bits, i + lo, e.get(e.bits, i)); return true; } @@ -1547,12 +1557,18 @@ namespace bv { } } - void sls_eval::repair_up(expr* e) { + bool sls_eval::repair_up(expr* e) { if (!is_app(e)) - return; - if (m.is_bool(e)) - set(e, bval1(to_app(e))); - else if (bv.is_bv(e)) - wval0(e).set(wval1(to_app(e))); + return false; + if (m.is_bool(e)) { + auto b = bval1(to_app(e)); + if (is_fixed0(e)) + return b == bval0(e); + m_eval[e->get_id()] = b; + return true; + } + if (bv.is_bv(e)) + return wval0(e).try_set(wval1(to_app(e))); + return false; } } diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index bdd6db0ed2f..ad9a06fb5ad 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -156,6 +156,6 @@ namespace bv { /* * Propagate repair up to parent */ - void repair_up(expr* e); + bool repair_up(expr* e); }; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index cb82a50dd9a..2423ad680c6 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -12,6 +12,7 @@ Module Name: --*/ #include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include "ast/sls/bv_sls_fixed.h" #include "ast/sls/bv_sls_eval.h" @@ -138,6 +139,7 @@ namespace bv { v.add_range(-b, a - b); } else if (!y) { + if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0) return; auto& v = wval0(x); @@ -300,21 +302,28 @@ namespace bv { if (j > 0 && k > 0) { - for (unsigned i = 0; i < std::min(k, j); ++i) + for (unsigned i = 0; i < std::min(k, j); ++i) { + SASSERT(!v.get(v.bits, i)); v.set(v.fixed, i, true); + } } // lower zj + jk bits are 0 if (zk > 0 || zj > 0) { - for (unsigned i = 0; i < zk + zj; ++i) + for (unsigned i = 0; i < zk + zj; ++i) { + SASSERT(!v.get(v.bits, i)); v.set(v.fixed, i, true); + } } // upper bits are 0, if enough high order bits of a, b are 0. - if (hzj < v.bw && hzk < v.bw && hzj + hzk > v.bw) { + // TODO - buggy + if (false && hzj < v.bw && hzk < v.bw && hzj + hzk > v.bw) { hzj = v.bw - hzj; hzk = v.bw - hzk; - for (unsigned i = hzj + hzk - 1; i < v.bw; ++i) + for (unsigned i = hzj + hzk - 1; i < v.bw; ++i) { + SASSERT(!v.get(v.bits, i)); v.set(v.fixed, i, true); - } + } + } break; } case OP_CONCAT: { diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp index df84075c932..41ab0bf1993 100644 --- a/src/ast/sls/bv_sls_terms.cpp +++ b/src/ast/sls/bv_sls_terms.cpp @@ -99,6 +99,13 @@ namespace bv { else if (bv.is_concat(e)) { FOLD_OP(bv.mk_concat); } + else if (m.is_distinct(e)) { + expr_ref_vector es(m); + for (unsigned i = 0; i < num_args; ++i) + for (unsigned j = i + 1; j < num_args; ++j) + es.push_back(m.mk_not(m.mk_eq(arg(i), arg(j)))); + r = m.mk_and(es); + } else if (bv.is_bv_sdiv(e, x, y) || bv.is_bv_sdiv0(e, x, y) || bv.is_bv_sdivi(e, x, y)) { r = mk_sdiv(x, y); }