From 88c982ff0b64f450a3fbd45edc015ac34da75d68 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 May 2023 16:55:32 +0200 Subject: [PATCH] experiments with arith Signed-off-by: Nikolaj Bjorner --- .../rewriter/bit_blaster/bit_blaster_tpl.h | 3 + .../bit_blaster/bit_blaster_tpl_def.h | 147 ++++++++++- src/math/lp/int_solver.cpp | 228 ++++++++++++++++-- src/math/lp/int_solver.h | 7 +- src/math/lp/nla_core.cpp | 7 +- src/math/lp/numeric_pair.h | 2 +- src/params/tactic_params.pyg | 1 + src/smt/smt_context_pp.cpp | 2 +- src/smt/theory_arith_aux.h | 6 +- src/smt/theory_arith_core.h | 6 + src/smt/theory_arith_int.h | 15 +- src/smt/theory_lra.cpp | 70 +++--- src/tactic/smtlogics/qflia_tactic.cpp | 4 +- src/test/bit_blaster.cpp | 40 +++ 14 files changed, 471 insertions(+), 67 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h index bfe63def7..07413aff9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl.h @@ -37,6 +37,7 @@ protected: unsigned long long m_max_memory; void checkpoint(); + public: bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX): Cfg(cfg), @@ -119,6 +120,8 @@ public: void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits); bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits); void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer& a_bits, ptr_buffer& b_bits, expr_ref_vector & out_bits); + void mk_const_case1_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits); + void mk_generic_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits); bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); } void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 7a3ee0ea6..5dddf6d7e 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -183,24 +183,29 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp SASSERT(sz > 0); numeral n_a, n_b; out_bits.reset(); - if (is_numeral(sz, a_bits, n_b)) + if (is_numeral(sz, b_bits, n_b)) std::swap(a_bits, b_bits); - if (is_minus_one(sz, b_bits)) { - mk_neg(sz, a_bits, out_bits); + if (is_minus_one(sz, a_bits)) { + mk_neg(sz, b_bits, out_bits); SASSERT(sz == out_bits.size()); - return; } - if (is_numeral(sz, a_bits, n_a)) { + else if (is_numeral(sz, b_bits, n_a)) { n_a *= n_b; num2bits(n_a, sz, out_bits); SASSERT(sz == out_bits.size()); - return; } - - if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) { + else if (is_numeral(sz, a_bits, n_a)) + mk_const_case1_multiplier(sz, a_bits, b_bits, out_bits); + else if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) { SASSERT(sz == out_bits.size()); - return; } + else + mk_generic_multiplier(sz, a_bits, b_bits, out_bits); +} + +template +void bit_blaster_tpl::mk_generic_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { + out_bits.reset(); #if 0 static unsigned counter = 0; @@ -268,7 +273,6 @@ void bit_blaster_tpl::mk_multiplier(unsigned sz, expr * const * a_bits, exp out_bits.push_back(out); } } - } @@ -1113,6 +1117,124 @@ void bit_blaster_tpl::mk_carry_save_adder(unsigned sz, expr * const * a_bit } } +template +void bit_blaster_tpl::mk_const_case1_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { + DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) VERIFY(is_bool_const(a_bits[i]));); + + unsigned num_ones = 0; + for (unsigned i = 0; i < sz; ++i) + if (m().is_true(a_bits[i])) + ++num_ones; + + + // for each run-length of ones, add contribution to out_bits. + // + // c = 2^i + 2^{i+1} + ... + 2^k + // x * c + // + // i = k + // x * 2^i + // + // i > 0, k < sz - 1 + // x * (2^i + 2^{i+1} + ... + 2^k) + // x * (2^(k+1) - 2^{i}) + // 4 + 8 + 16 = 32 - 4 = 30 + + // i = 0, k < sz - 1 + // x * 2^(k+1) - 1 + + // i = 0, k = sz - 1 + // -x + + // i > 0, k = sz - 1 + // x*2^{sz} - 1 - x*2^{i} + 1 + // = -x - x*2^i + 1 + // 8 + 16 + 32 = + // 64 - 1 - 8 + 1 + + SASSERT(out_bits.empty()); + for (unsigned i = 0; i < sz; ++i) + out_bits.push_back(m().mk_false()); + expr_ref cout(m()); + + auto mul2_i = [&](unsigned i, ptr_buffer& sbits) { + for (unsigned j = 0; j < sz; ++j) + if (j < i) + sbits.push_back(m().mk_false()); + else + sbits.push_back(b_bits[j-i]); + }; + + for (unsigned i = 0; i < sz; ++i) { + if (!m().is_true(a_bits[i])) + continue; + + ptr_buffer one, sbits; + expr_ref_vector out_bits1(m()); + + unsigned k = 0; + for (k = i + 1; k < sz && m().is_true(a_bits[k]); ++k); + --k; + + if (i == 0 && k == 0) { + for (unsigned i = 0; i < sz; ++i) + out_bits[i] = b_bits[i]; + } + else if (i == 0 && k == sz - 1) { + out_bits.reset(); + mk_neg(sz, b_bits, out_bits); + } + else if (i == 0) { + SASSERT(k < sz - 1); + // shift by k+1, subtract x + out_bits.reset(); + + mul2_i(k + 1, sbits); + mk_adder(sz, out_bits.data(), sbits.data(), out_bits1); + out_bits.reset(); + out_bits.append(out_bits1); + out_bits1.reset(); + + // subtract x + mk_subtracter(sz, out_bits.data(), b_bits, out_bits1, cout); + out_bits.reset(); + out_bits.append(out_bits1); + out_bits1.reset(); + } + else if (i == k) { + mul2_i(i, sbits); + mk_adder(sz, out_bits.data(), sbits.data(), out_bits1); + out_bits.reset(); + out_bits.append(out_bits1); + out_bits1.reset(); + } + else if (k == sz - 1) { + // 2^sz - 2^i = - 2^i + // -= x*2^i + mul2_i(i, sbits); + mk_subtracter(sz, out_bits.data(), sbits.data(), out_bits1, cout); + out_bits.reset(); + out_bits.append(out_bits1); + } + else { + SASSERT(0 < i && i < k && k < sz - 1); + // += x*2^{k+1} - x*2^i + mul2_i(i, ibits); + mul2_i(k + 1, kbits); + mk_adder(sz, kbits.data(), out_bits.data(), out_bits1); + out_bits.reset(); + out_bits.append(out_bits1); + out_bits1.reset(); + mk_subtracter(sz, out_bits.data(), ibits.data(), out_bits1, cout); + out_bits.reset(); + out_bits.append(out_bits1); + out_bits1.reset(); + } + i = k; + } +} + + template bool bit_blaster_tpl::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { unsigned case_size = 1; @@ -1133,10 +1255,11 @@ bool bit_blaster_tpl::mk_const_case_multiplier(unsigned sz, expr * const * na_bits.append(sz, a_bits); ptr_buffer nb_bits; nb_bits.append(sz, b_bits); - mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); + mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); return true; } - + + template void bit_blaster_tpl::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer& a_bits, ptr_buffer& b_bits, expr_ref_vector & out_bits) { while (is_a && i < sz && is_bool_const(a_bits[i])) ++i; diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 099d97f6c..ff698fa10 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -35,6 +35,152 @@ namespace lp { } } + + unsigned int_solver::patcher::count_non_int() { + unsigned non_int = 0; + for (auto j : lra.r_basis()) + if (lra.column_is_int(j) && !lra.column_value_is_int(j)) + ++non_int; + return non_int; + } + + lia_move int_solver::patcher::patch_basic_columns() { + remove_fixed_vars_from_base(); + lia.settings().stats().m_patches++; + lp_assert(lia.is_feasible()); + + //unsigned non_int_before = count_non_int(); + unsigned num = lra.A_r().column_count(); + for (unsigned j : lra.r_basis()) + if (!lra.get_value(j).is_int()) + patch_basic_column(j); + //unsigned non_int_after = count_non_int(); + // verbose_stream() << non_int_before << " -> " << non_int_after << "\n"; + if (!lia.has_inf_int()) { + lia.settings().stats().m_patches_success++; + return lia_move::sat; + } + return lia_move::undef; + } + + /*** + * v + r + a*j = 0 + * val(v) is rational + * a is rational + * val(j) is integer + * find min delta > 0 such that frac(a*delta) = frac(val(v)) + * then r + a*(j - delta) is an integer + * find min delta > 0 such that frac(a*-delta) = frac(val(v)) + * then r + a*(j + delta) is an integer + * + * Note: frac(a*delta) = frac(frac(a)*delta) + * Let x1/x2 = frac(val(v)) + * let a1/a2 = frac(a) + * + * x1/x2 = frac(a1*delta/a2) + * requires that a2 | x2, otherwise not possible. + * + * x2 = a2, 0 < x1 < a2 + * -> x1 = a1*delta mod a2 + * -> x1 = a1*delta + a2*gamma + * let g, x, y = extended_gcd(a1, a2) + * a1*x + a2*y = g + * if g does not divide x1 then no solution. + * therefore assume g | x1 + * Set delta = x*x1/g + * + * Initial experiment: use bare bones case x1/x2 = a1/a2, x1/x2 = 1 - a1/a2 + */ + + bool int_solver::patcher::patch_basic_column(unsigned v, row_cell const& c) { + if (v == c.var()) + return false; + if (!lra.column_is_int(c.var())) // could use real to patch integer + return false; + if (c.coeff().is_int()) + return false; + mpq a = fractional_part(c.coeff()); + mpq r = fractional_part(lra.get_value(v)); + SASSERT(0 < a && a < 1); + SASSERT(0 < r && r < 1); + if (!divides(denominator(a), denominator(r))) + return false; + // stronger filter for now: + if (denominator(a) != denominator(r)) + return false; + if (a == r) { + if (try_patch_column(c.var(), mpq(a.is_pos() ? 1 : -1))) + return true; + } + if (a == 1 - r) { + if (try_patch_column(c.var(), mpq(a.is_pos() ? -1 : 1))) + return true; + } + rational x, y; + rational g = gcd(numerator(a), denominator(a), x, y); + // g = numerator(a)*x + denominator(a)*y + x = abs(x); + if (divides(g, numerator(r))) { + auto xs = a.is_pos() ? x : -x; + if (try_patch_column(c.var(), xs*(numerator(r)/g))) + return true; + } + if (divides(g, numerator(1 - r))) { + auto xs = a.is_pos() ? -x : x; + if (try_patch_column(c.var(), xs*(numerator(r)/g))) + return true; + } + return false; + } + + bool int_solver::patcher::try_patch_column(unsigned j, mpq const& delta) { + const auto & A = lra.A_r(); + unsigned make_count = 0, break_count = 0; + if (delta < 0) { + if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j)) + return false; + } + else { + if (lia.has_upper(j) && lia.get_value(j) + impq(delta) > lra.get_upper_bound(j)) + return false; + } + for (auto const& c : A.column(j)) { + unsigned row_index = c.var(); + unsigned i = lrac.m_r_basis[row_index]; + auto old_val = lia.get_value(i); + auto new_val = old_val - impq(c.coeff()*delta); + if (lia.has_lower(i) && new_val < lra.get_lower_bound(i)) + return false; + if (lia.has_upper(i) && new_val > lra.get_upper_bound(i)) + return false; + if (old_val.is_int() && !new_val.is_int()) + break_count++; + else if (!old_val.is_int() && new_val.is_int()) + make_count++; + } + if (make_count > break_count) { +#if 0 + for (auto const& c : A.column(j)) { + unsigned row_index = c.var(); + unsigned i = lrac.m_r_basis[row_index]; + verbose_stream() << "basis " << i << "\n"; + } + verbose_stream() << j << " delta " << delta << " make " << make_count << " break " << break_count << "\n"; + lra.display(verbose_stream()); +#endif + lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta)); + return true; + } + return false; + } + + void int_solver::patcher::patch_basic_column(unsigned v) { + SASSERT(!lia.is_fixed(v)); + for (auto const& c : lra.basic2row(v)) + if (patch_basic_column(v, c)) + return; + } + lia_move int_solver::patcher::patch_nbasic_columns() { remove_fixed_vars_from_base(); lia.settings().stats().m_patches++; @@ -43,6 +189,8 @@ namespace lp { m_patch_fail = 0; m_num_ones = 0; m_num_divides = 0; + //unsigned non_int_before = count_non_int(); + unsigned num = lra.A_r().column_count(); for (unsigned v = 0; v < num; v++) { if (lia.is_base(v)) @@ -55,9 +203,12 @@ namespace lp { ++num_fixed; lp_assert(lia.is_feasible()); - verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n"; + //verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n"; //lra.display(verbose_stream()); //exit(0); + //unsigned non_int_after = count_non_int(); + + // verbose_stream() << non_int_before << " -> " << non_int_after << "\n"; if (!lia.has_inf_int()) { lia.settings().stats().m_patches_success++; return lia_move::sat; @@ -76,19 +227,30 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { bool m_is_one = m.is_one(); bool val_is_int = lia.value_is_int(j); - - + const auto & A = lra.A_r(); // check whether value of j is already a multiple of m. if (val_is_int && (m_is_one || (val.x / m).is_int())) { if (m_is_one) ++m_num_ones; else ++m_num_divides; +#if 0 + for (auto c : A.column(j)) { + unsigned row_index = c.var(); + unsigned i = lrac.m_r_basis[row_index]; + if (!lia.get_value(i).is_int() || + (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || + (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { + verbose_stream() << "skip " << j << " " << m << ": "; + lia.display_row(verbose_stream(), A.m_rows[row_index]); + verbose_stream() << "\n"; + } + } +#endif return; } #if 0 - const auto & A = lra.A_r(); if (!m_is_one) { // lia.display_column(verbose_stream(), j); for (auto c : A.column(j)) { @@ -120,12 +282,19 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { #if 0 verbose_stream() << "TARGET v" << j << " -> ["; - if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x); + if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x) << " " << l << "\n"; verbose_stream() << ", "; - if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x); + if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x) << " " << u << "\n"; verbose_stream() << "]"; verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n"; #endif + +#if 0 + if (!inf_l) + l = impq(ceil(l)); + if (!inf_u) + u = impq(floor(u)); +#endif if (!inf_l) { l = impq(m_is_one ? ceil(l) : m * ceil(l / m)); @@ -134,10 +303,23 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { lra.set_value_for_nbasic_column(j, l); } else { - verbose_stream() << "fail: " << j << " " << m << "\n"; - --m_patch_success; + //verbose_stream() << "fail: " << j << " " << m << "\n"; ++m_patch_fail; TRACE("patch_int", tout << "not patching " << l << "\n";); +#if 0 + verbose_stream() << "not patched\n"; + for (auto c : A.column(j)) { + unsigned row_index = c.var(); + unsigned i = lrac.m_r_basis[row_index]; + if (!lia.get_value(i).is_int() || + (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || + (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { + lia.display_row(verbose_stream(), A.m_rows[row_index]); + verbose_stream() << "\n"; + } + } +#endif + return; } } else if (!inf_u) { @@ -150,6 +332,20 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) { TRACE("patch_int", tout << "patching with 0\n";); } ++m_patch_success; +#if 0 + verbose_stream() << "patched " << j << "\n"; + for (auto c : A.column(j)) { + unsigned row_index = c.var(); + unsigned i = lrac.m_r_basis[row_index]; + if (!lia.get_value(i).is_int() || + (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) || + (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) { + lia.display_row(verbose_stream(), A.m_rows[row_index]); + verbose_stream() << "\n"; + } + } +#endif + } int_solver::int_solver(lar_solver& lar_slv) : @@ -398,10 +594,9 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq unsigned i = lrac.m_r_basis[row_index]; impq const & xi = get_value(i); lp_assert(lrac.m_r_solver.column_is_feasible(i)); - if (column_is_int(i) && !a.is_int()) + if (column_is_int(i) && !a.is_int() && xi.is_int()) m = lcm(m, denominator(a)); - - + if (!inf_l && !inf_u) { if (l == u) continue; @@ -409,15 +604,15 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq if (a.is_neg()) { if (has_lower(i)) - set_lower(l, inf_l, delta(a, xi, lrac.m_r_lower_bounds()[i])); + set_lower(l, inf_l, delta(a, xi, lra.get_lower_bound(i))); if (has_upper(i)) - set_upper(u, inf_u, delta(a, xi, lrac.m_r_upper_bounds()[i])); + set_upper(u, inf_u, delta(a, xi, lra.get_upper_bound(i))); } else { if (has_upper(i)) - set_lower(l, inf_l, delta(a, xi, lrac.m_r_upper_bounds()[i])); + set_lower(l, inf_l, delta(a, xi, lra.get_upper_bound(i))); if (has_lower(i)) - set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i])); + set_upper(u, inf_u, delta(a, xi, lra.get_lower_bound(i))); } } @@ -575,7 +770,8 @@ bool int_solver::shift_var(unsigned j, unsigned range) { bool inf_l = false, inf_u = false; impq l, u; mpq m; - VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m) || settings().get_cancel_flag()); + if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m)) + return false; if (settings().get_cancel_flag()) return false; const impq & x = get_value(j); diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 9a7d75573..94802c648 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -51,11 +51,16 @@ class int_solver { public: patcher(int_solver& lia); bool should_apply() const { return true; } - lia_move operator()() { return patch_nbasic_columns(); } + lia_move operator()() { return patch_basic_columns(); } void patch_nbasic_column(unsigned j); + bool patch_basic_column(unsigned v, row_cell const& c); + void patch_basic_column(unsigned j); + bool try_patch_column(unsigned j, mpq const& delta); + unsigned count_non_int(); private: void remove_fixed_vars_from_base(); lia_move patch_nbasic_columns(); + lia_move patch_basic_columns(); }; lar_solver& lra; diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4d1cc6edb..ccf851cff 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1373,7 +1373,7 @@ void core::patch_monomial(lpvar j) { // handle perfect squares if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) { rational root; - if (v.is_perfect_square(root)) { + if (v.get_num_bits() <= 1024 && v.is_perfect_square(root)) { m_patched_var = (*m_patched_monic).vars()[0]; if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) { TRACE("nla_solver", tout << "patched square\n";); @@ -1420,11 +1420,12 @@ void core::patch_monomials_on_to_refine() { } void core::patch_monomials() { - m_cautious_patching = true; - patch_monomials_on_to_refine(); if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching) { return; } + m_cautious_patching = true; + patch_monomials_on_to_refine(); + NOT_IMPLEMENTED_YET(); m_cautious_patching = false; patch_monomials_on_to_refine(); diff --git a/src/math/lp/numeric_pair.h b/src/math/lp/numeric_pair.h index 251274006..3a5bcd6a4 100644 --- a/src/math/lp/numeric_pair.h +++ b/src/math/lp/numeric_pair.h @@ -269,12 +269,12 @@ numeric_pair operator*(const numeric_pair & r, const X & a) { return numeric_pair(a * r.x, a * r.y); } - template numeric_pair operator/(const numeric_pair & r, const X & a) { return numeric_pair(r.x / a, r.y / a); } + template double get_double(const lp::numeric_pair & ) { /* UNREACHABLE(); */ return 0;} template class numeric_traits> { diff --git a/src/params/tactic_params.pyg b/src/params/tactic_params.pyg index 3870e90ad..89c270e6b 100644 --- a/src/params/tactic_params.pyg +++ b/src/params/tactic_params.pyg @@ -10,6 +10,7 @@ def_module_params('tactic', ('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."), ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."), ('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"), + ('local_ctx', BOOL, True, "enable local context simplifier in default tactic pre-amble"), # ('aig.per_assertion', BOOL, True, "process one assertion at a time"), # ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."), diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index a6088fdf7..0e72f2f93 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -166,7 +166,7 @@ namespace smt { unsigned num = get_num_bool_vars(); for (unsigned v = 0; v < num; v++) { expr * n = m_bool_var2expr[v]; - ast_def_ll_pp(out << v << " ", m, n, get_pp_visited(), true, false); + out << "b" << v << " := #" << n->get_id() << "\n"; } } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 4b244ca88..625fbbf57 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -582,12 +582,14 @@ namespace smt { // If the row contains non integer coefficients, then v may be assigned // to a non-integer value even if all non-base variables are integer. // So, v should not be "eliminated" - break; + break; + verbose_stream() << "eliminate " << v << "\n"; eliminate(v, m_eager_gcd); break; case NON_BASE: { col_entry const * entry = get_row_for_eliminating(v); if (entry) { + verbose_stream() << "moving " << v << "\n"; TRACE("move_unconstrained_to_base", tout << "moving v" << v << " to the base\n";); row & r = m_rows[entry->m_row_id]; SASSERT(r[entry->m_row_idx].m_var == v); @@ -2144,7 +2146,7 @@ namespace smt { if (candidates.empty()) return; - verbose_stream() << "candidates " << candidates.size() << "\n"; + // verbose_stream() << "candidates " << candidates.size() << "\n"; m_tmp_var_set.reset(); m_tmp_var_set2.reset(); for (theory_var v : candidates) { diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 513ce6851..6f0820ca7 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1466,6 +1466,7 @@ namespace smt { template void theory_arith::restart_eh() { + return; m_arith_eq_adapter.restart_eh(); } @@ -1556,6 +1557,11 @@ namespace smt { template final_check_status theory_arith::final_check_eh() { + + // verbose_stream() << "final " << ctx.get_scope_level() << " " << ctx.assigned_literals().size() << "\n"; + // ctx.display(verbose_stream()); + // exit(0); + TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout);); TRACE("arith", display(tout);); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index e28113863..2692acb5a 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -958,7 +958,7 @@ namespace smt { } if (!inf_l && !inf_u && l > u) { ++num_not_patched; - verbose_stream() << "fail: " << v << " " << m << "\n"; + // verbose_stream() << "fail: " << v << " " << m << "\n"; continue; // cannot patch } ++num_patched; @@ -968,9 +968,20 @@ namespace smt { set_value(v, u); else set_value(v, inf_numeral(0)); + +#if 0 + verbose_stream() << "Patch " << v << "\n"; + for (auto const& ce : m_columns[v]) { + if (ce.is_dead()) + continue; + row const & r = m_rows[ce.m_row_id]; + theory_var s = r.get_base_var(); + display_row(verbose_stream() << s << " " << get_value(s) << " ", r, true); + } +#endif } SASSERT(m_to_patch.empty()); - verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n"; + // verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n"; //display(verbose_stream()); //exit(0); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9b5a13c22..cee367ad7 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -458,9 +458,19 @@ class theory_lra::imp { if (!ctx().relevancy()) mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1)); return s; - } + theory_var internalize_div(app * n) { + rational r(1); + theory_var s = mk_binary_op(n); + if (!a.is_numeral(n->get_arg(1), r) || r.is_zero()) + found_underspecified(n); + if (!ctx().relevancy()) + mk_div_axiom(n->get_arg(0), n->get_arg(1)); + return s; + } + + theory_var mk_binary_op(app * n) { SASSERT(n->get_num_args() == 2); if (ctx().e_internalized(n)) @@ -499,24 +509,23 @@ class theory_lra::imp { return internalize_mod(n); else if (a.is_idiv(n)) return internalize_mod(n); + else if (a.is_div(n)) + return internalize_div(n); + else if (a.get_family_id() == n->get_family_id()) { + if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) + found_unsupported(n); + if (ctx().e_internalized(n)) + return mk_var(n); + for (expr* arg : *n) + ctx().internalize(arg, false); + mk_enode(n); + return mk_var(n); + } else if (a.is_arith_expr(n)) { verbose_stream() << "nyi " << mk_pp(n, m) << "\n"; NOT_IMPLEMENTED_YET(); } #if 0 - - else if (a.is_div(n)) - return internalize_div(n); - else if (a.is_rem(n)) - return internalize_rem(n); - else if (a.is_to_real(n)) - return internalize_to_real(n); - else if (a.is_to_int(n)) - return internalize_to_int(n); - - else if (a.is_sub(n)) - return internalize_sub(n); - if (a.is_power(n)) { // unsupported found_unsupported_op(n); return mk_binary_op(n); @@ -527,14 +536,6 @@ class theory_lra::imp { enode* e = mk_enode(n); return mk_var(e); } - if (a.get_family_id() == n->get_family_id()) { - if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) - found_unsupported_op(n); - if (ctx().e_internalized(n)) - return expr2var(n); - for (expr* arg : *n) - ctx().internalize(arg, false); - return mk_var(mk_enode(n)); } #endif @@ -1097,7 +1098,6 @@ class theory_lra::imp { return v; } if (!st.offset().is_zero()) { - verbose_stream() << "Offset row " << st.offset() << "\n"; m_left_side.push_back({ st.offset(), get_one(a.is_int(term)) }); } @@ -1255,13 +1255,21 @@ public: } void internalize_eq_eh(app * atom, bool_var) { + return; + if (!ctx().get_fparams().m_arith_eager_eq_axioms) + return; expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); enode * n2 = get_enode(rhs); - TRACE("arith_verbose", tout << mk_pp(atom, m) << " " << is_arith(n1) << " " << is_arith(n2) << "\n";); - if (is_arith(n1) && is_arith(n2) && n1 != n2) + if (is_arith(n1) && is_arith(n2) && + n1->get_th_var(get_id()) != null_theory_var && + n2->get_th_var(get_id()) != null_theory_var && n1 != n2) { + verbose_stream() << "ineq\n"; m_arith_eq_adapter.mk_axioms(n1, n2); + } + else + verbose_stream() << "skip\n"; } void assign_eh(bool_var v, bool is_true) { @@ -1353,6 +1361,7 @@ public: } void restart_eh() { + return; m_arith_eq_adapter.restart_eh(); } @@ -1778,7 +1787,7 @@ public: tout << "v" << v << " "; tout << "\n"; ); if (!vars.empty()) { - verbose_stream() << "random update " << vars.size() << "\n"; + // verbose_stream() << "random update " << vars.size() << "\n"; lp().random_update(vars.size(), vars.data()); m_changed_assignment = true; } @@ -1933,6 +1942,11 @@ public: bool m_changed_assignment = false; final_check_status final_check_eh() { + + verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n"; + //ctx().display(verbose_stream()); + //exit(0); + TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout);); TRACE("arith", display(tout);); @@ -2525,6 +2539,7 @@ public: m_bv_to_propagate.reset(); return true; } + lbool lbl = make_feasible(); if (!m.inc()) @@ -2629,9 +2644,7 @@ public: continue; TRACE("arith", tout << lit << " bound: " << *b << " first: " << first << "\n";); ctx().display_literal_verbose(verbose_stream() << "miss ", lit) << "\n"; - display(verbose_stream()); TRACE("arith", ctx().display_literal_verbose(tout << "miss ", lit) << "\n"); - exit(0); ++count; } @@ -3562,6 +3575,7 @@ public: TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, // TIME_EXAUSTED, EMPTY, UNSTABLE + return l_undef; } diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index e72a63087..0b0d4ada1 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -34,6 +34,7 @@ Notes: #include "sat/tactic/sat_tactic.h" #include "ast/simplifiers/bound_manager.h" #include "tactic/arith/probe_arith.h" +#include "params/tactic_params.hpp" struct quasi_pb_probe : public probe { result operator()(goal const & g) override { @@ -181,6 +182,7 @@ static tactic * mk_bounded_tactic(ast_manager & m) { tactic * mk_preamble_tactic(ast_manager& m) { params_ref pull_ite_p; + tactic_params tp; pull_ite_p.set_bool("pull_cheap_ite", true); pull_ite_p.set_bool("push_ite_arith", false); pull_ite_p.set_bool("local_ctx", true); @@ -195,7 +197,7 @@ tactic * mk_preamble_tactic(ast_manager& m) { and_then( mk_simplify_tactic(m), mk_propagate_values_tactic(m), - using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), + tp.local_ctx() ? using_params(mk_ctx_simplify_tactic(m), ctx_simp_p) : mk_skip_tactic(), using_params(mk_simplify_tactic(m), pull_ite_p), mk_solve_eqs_tactic(m), mk_elim_uncnstr_tactic(m)); diff --git a/src/test/bit_blaster.cpp b/src/test/bit_blaster.cpp index fa623f767..309e3e05c 100644 --- a/src/test/bit_blaster.cpp +++ b/src/test/bit_blaster.cpp @@ -23,6 +23,10 @@ Revision History: #include "ast/rewriter/bit_blaster/bit_blaster.h" #include "model/model.h" #include "model/model_evaluator.h" +#include "smt/smt_kernel.h" +#include "smt/params/smt_params.h" +#include "ast/for_each_expr.h" + void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) { sort_ref b(m); @@ -184,6 +188,41 @@ void tst_multiplier(ast_manager & m, bit_blaster & blaster) { ENSURE_INT(mdl, c, 7); // b111 * b001 } +void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) { + expr_ref_vector x(m); + mk_bits(m, "x", sz, x); + for (unsigned i = 0; i < (1ul << sz); ++i) { + expr_ref_vector c(m), out1(m), out2(m); + for (unsigned j = 0; j < sz; ++j) + c.push_back((i & (1ul << j)) ? m.mk_true() : m.mk_false()); + for (auto xi : x) + verbose_stream() << mk_pp(xi, m); + verbose_stream() << " "; + for (auto ci : c) + verbose_stream() << mk_pp(ci, m); + verbose_stream() << "\n"; + blaster.mk_const_case1_multiplier(sz, c.data(), x.data(), out1); + + blaster.mk_generic_multiplier(sz, c.data(), x.data(), out2); + expr_ref fml(m.mk_true(), m); + for (unsigned j = 0; j < sz; ++j) + fml = m.mk_and(fml, m.mk_eq(out1.get(j), out2.get(j))); + smt_params fp; + smt::kernel solver(m, fp); + solver.assert_expr(m.mk_not(fml)); + auto r = solver.check(); + verbose_stream() << r << "\n"; + VERIFY(r == l_false); + expr_mark vis1, vis2; + unsigned sz1 = 0, sz2 = 0; + for (auto o : out1) + sz1 += get_num_exprs(o, vis1); + for (auto o : out2) + sz2 += get_num_exprs(o, vis2); + verbose_stream() << "sizes " << sz1 << " vs " << sz2 << "\n"; + } +} + void tst_le(ast_manager & m, unsigned sz) { // expr_ref_vector a(m); // expr_ref_vector b(m); @@ -233,6 +272,7 @@ void tst_bit_blaster() { bit_blaster_params params; bit_blaster blaster(m, params); + tst_const_multiplier(m, blaster, 7); tst_adder(m, blaster); tst_multiplier(m, blaster); tst_le(m, 4);