From df980acd6723af0bcb7d2ff1c25974726722aa30 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Aug 2024 12:59:22 -0700 Subject: [PATCH] use unit coefficients for muls Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 58 ++++++++++++++++------------------ src/ast/sls/sls_arith_base.h | 2 +- src/ast/sls/sls_context.cpp | 5 +-- src/ast/sls/sls_context.h | 1 + 4 files changed, 32 insertions(+), 34 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 0d9fcd284..150e3a57a 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -553,18 +553,18 @@ namespace sls { template bool arith_base::repair(sat::literal lit) { - //verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n"; + //verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << " " << mk_bounded_pp(ctx.atom(lit.var()), m) << "\n"; + //verbose_stream() << *atom(lit.var()) << "\n"; m_last_literal = lit; if (find_nl_moves(lit)) return true; - if (find_lin_moves(lit)) - return true; - - flet _tabu(m_use_tabu, false); - find_reset_moves(lit); - return apply_update(); + if (find_nl_moves(lit)) + return true; + if (false && find_lin_moves(lit)) + return true; + return find_reset_moves(lit); } template @@ -860,25 +860,14 @@ namespace sls { add_args(term, x, coeff); add_args(term, y, -coeff); } + else if (a.is_mul(e, x, y) && is_num(x, i)) { + add_args(term, y, i * coeff); + } else if (a.is_mul(e)) { unsigned_vector ms; num_t c(1); - ptr_buffer muls; - muls.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - for (unsigned j = 0; j < muls.size(); ++j) { - expr* arg = muls[j]; - if (a.is_mul(arg)) { - //verbose_stream() << "nested " << mk_bounded_pp(arg, m) << "\n"; - muls.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); - muls[j] = muls.back(); - muls.pop_back(); - --j; - } - else if (is_num(arg, i)) - c *= i; - else - ms.push_back(mk_term(arg)); - } + for (expr* arg : *to_app(e)) + ms.push_back(mk_term(arg)); switch (ms.size()) { case 0: @@ -1118,8 +1107,8 @@ namespace sls { template void arith_base::init_bool_var_assignment(sat::bool_var v) { - auto* ineq = m_bool_vars.get(v, nullptr); - if (ineq && ctx.is_true(sat::literal(v, false)) != (dtt(false, *ineq) == 0)) + auto* ineq = atom(v); + if (ineq && ineq->is_true() != ctx.is_true(v)) ctx.flip(v); } @@ -1137,10 +1126,7 @@ namespace sls { template void arith_base::repair_literal(sat::literal lit) { - auto v = lit.var(); - auto const* ineq = atom(v); - if (ineq && ineq->is_true() != ctx.is_true(v)) - ctx.flip(v); + init_bool_var_assignment(lit.var()); } template @@ -1151,6 +1137,13 @@ namespace sls { template void arith_base::repair_up(app* e) { + if (m.is_bool(e)) { + auto v = ctx.atom2bool_var(e); + auto const* ineq = atom(v); + if (ineq && ineq->is_true() != ctx.is_true(v)) + ctx.flip(v); + return; + } auto v = m_expr2var.get(e->get_id(), UINT_MAX); if (v == UINT_MAX) return; @@ -1813,11 +1806,12 @@ namespace sls { } template - void arith_base::find_reset_moves(sat::literal lit) { + bool arith_base::find_reset_moves(sat::literal lit) { + m_updates.reset(); auto* ineq = atom(lit.var()); num_t a, b; if (!ineq) - return; + return false; for (auto const& [x, nl] : ineq->m_nonlinear) add_reset_update(x); @@ -1829,6 +1823,8 @@ namespace sls { } } verbose_stream() << "RESET moves num updates: " << lit << " " << m_updates.size() << "\n"); + + return apply_update(); } template diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h index 7f02bcebe..0d89ea98c 100644 --- a/src/ast/sls/sls_arith_base.h +++ b/src/ast/sls/sls_arith_base.h @@ -219,7 +219,7 @@ namespace sls { bool apply_update(); bool find_nl_moves(sat::literal lit); bool find_lin_moves(sat::literal lit); - void find_reset_moves(sat::literal lit); + bool find_reset_moves(sat::literal lit); void add_reset_update(var_t v); void find_linear_moves(ineq const& i, var_t x, num_t const& coeff, num_t const& sum); void find_quadratic_moves(ineq const& i, var_t x, num_t const& a, num_t const& b, num_t const& sum); diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 44dcec925..fdf364ed5 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -127,6 +127,7 @@ namespace sls { } } + repair_literals(); // propagate "final checks" bool propagated = true; @@ -136,9 +137,9 @@ namespace sls { propagated |= p && !m_new_constraint && p->propagate(); } - if (m_new_constraint) - return; + } + void context::repair_literals() { for (sat::bool_var v = 0; v < s.num_vars() && !m_new_constraint; ++v) { auto a = atom(v); if (!a) diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 4530f7042..599f25e77 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -123,6 +123,7 @@ namespace sls { void propagate_boolean_assignment(); void propagate_literal(sat::literal lit); + void repair_literals(); family_id get_fid(expr* e) const;