diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index c196abe08..58473ad31 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -543,7 +543,7 @@ namespace sls { bool arith_base::find_lin_moves(sat::literal lit) { m_updates.reset(); auto* ineq = get_ineq(lit.var()); - num_t a, b; + num_t a(0), b(0); if (!ineq) return false; if (!ineq->m_is_linear) { @@ -947,6 +947,9 @@ namespace sls { m_vars[v].m_def_idx = idx; m_vars[v].m_op = k; m_vars[v].set_value(val); + m_vars[vx].m_ops.push_back(v); + if (vy != vx) + m_vars[vy].m_ops.push_back(v); return v; } @@ -1854,7 +1857,7 @@ namespace sls { for (auto const& [x, nl] : ineq->m_nonlinear) { if (is_fixed(x)) continue; - if (is_add(x) || is_mul(x)) + if (is_add(x) || is_mul(x) || is_op(x)) ; else if (is_linear(x, nl, b)) find_linear_moves(*ineq, x, b); @@ -1905,7 +1908,7 @@ namespace sls { bool arith_base::find_reset_moves(sat::literal lit) { m_updates.reset(); auto* ineq = get_ineq(lit.var()); - num_t a, b; + num_t a(0), b(0); if (!ineq) return false; for (auto const& [x, nl] : ineq->m_nonlinear) @@ -2853,25 +2856,6 @@ namespace sls { m_fixed_atoms.insert(bv); } - template - void arith_base::add_lookahead(sat::bool_var bv) { - auto* ineq = get_ineq(bv); - if (!ineq) - return; - num_t na, nb; - for (auto const& [x, nl] : ineq->m_nonlinear) { - if (is_fixed(x)) - continue; - if (is_add(x) || is_mul(x)) - ; - else if (is_linear(x, nl, nb)) - find_linear_moves(*ineq, x, nb); - else if (is_quadratic(x, nl, na, nb)) - find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value); - else - ; - } - } // for every variable e, for every atom containing e // add lookahead for e. @@ -3211,8 +3195,8 @@ namespace sls { for (auto const& idx : vi.m_muls) { auto& [x, monomial] = m_muls[idx]; num_t new_prod(1); - for (auto [w, p] : monomial) - new_prod *= power_of(v == w ? new_value : value(w), p); + for (auto [w, p] : monomial) + new_prod *= power_of(value(w), p); update_args_value(x, new_prod); } @@ -3220,10 +3204,12 @@ namespace sls { auto& ad = m_adds[idx]; num_t new_sum(ad.m_coeff); for (auto [c, w] : ad.m_args) - new_sum += c * (v == w ? new_value : value(w)); + new_sum += c * value(w); update_args_value(ad.m_var, new_sum); } + for (auto const& x : vi.m_ops) + update_args_value(x, value1(x)); for (auto const& [coeff, bv] : vi.m_linear_occurs) { auto& ineq = *get_ineq(bv); diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h index a1f6d87bb..80a85fca3 100644 --- a/src/ast/sls/sls_arith_base.h +++ b/src/ast/sls/sls_arith_base.h @@ -122,8 +122,7 @@ namespace sls { vector> m_linear_occurs; sat::bool_var_vector m_bool_vars_of; unsigned_vector m_clauses_of; - unsigned_vector m_muls; - unsigned_vector m_adds; + unsigned_vector m_muls, m_adds, m_ops; optional m_lo, m_hi; vector m_finite_domain; @@ -277,6 +276,7 @@ namespace sls { bool is_mul(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_MUL; } bool is_add(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_ADD; } + bool is_op(var_t v) const { return m_vars[v].m_op != arith_op_kind::LAST_ARITH_OP && m_vars[v].m_op != arith_op_kind::OP_MUL && m_vars[v].m_op != arith_op_kind::OP_ADD; } mul_def const& get_mul(var_t v) const { SASSERT(is_mul(v)); return m_muls[m_vars[v].m_def_idx]; } add_def const& get_add(var_t v) const { SASSERT(is_add(v)); return m_adds[m_vars[v].m_def_idx]; } @@ -385,7 +385,6 @@ namespace sls { double lookahead(expr* e, bool update_score); void add_lookahead(bool_info& i, expr* e); void add_lookahead(bool_info& i, sat::bool_var bv); - void add_lookahead(sat::bool_var bv); ptr_vector const& get_fixable_exprs(expr* e); bool apply_move(expr* f, ptr_vector const& vars, arith_move_type t); expr* get_candidate_unsat(); diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp index 322ca2320..837a67b9f 100644 --- a/src/ast/sls/sls_arith_clausal.cpp +++ b/src/ast/sls/sls_arith_clausal.cpp @@ -127,10 +127,30 @@ namespace sls { tout << "\n";); for (auto v : ctx.unsat_vars()) - a.add_lookahead(v); + add_lookahead(v); } + template + void arith_clausal::add_lookahead(sat::bool_var bv) { + auto* ineq = a.get_ineq(bv); + if (!ineq) + return; + num_t na, nb; + for (auto const& [x, nl] : ineq->m_nonlinear) { + if (a.is_fixed(x)) + continue; + if (a.is_add(x) || a.is_mul(x) || a.is_op(x)) + ; + else if (a.is_linear(x, nl, nb)) + a.find_linear_moves(*ineq, x, nb); + else if (a.is_quadratic(x, nl, na, nb)) + a.find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value); + else + ; + } + } + /** * \brief walk over literals that are false in some clause. * Try to determine if flipping them to true improves the overall score. @@ -162,7 +182,7 @@ namespace sls { --sz; a.m_bool_var_atoms.swap_elems(idx, sz); if (occurs_negative(bv)) - a.add_lookahead(bv); + add_lookahead(bv); else ++i; } @@ -171,7 +191,7 @@ namespace sls { for (unsigned i = 0; i < sz; ++i) { bv = a.m_bool_var_atoms[i]; if (occurs_negative(bv)) - a.add_lookahead(bv); + add_lookahead(bv); } } } diff --git a/src/ast/sls/sls_arith_clausal.h b/src/ast/sls/sls_arith_clausal.h index ba9109b9a..32413bf06 100644 --- a/src/ast/sls/sls_arith_clausal.h +++ b/src/ast/sls/sls_arith_clausal.h @@ -64,6 +64,7 @@ namespace sls { void critical_move(var_t v, num_t const& delta, move_t mt); void lookahead(var_t v, num_t const& delta); double get_score(var_t v, num_t const& delta); + void add_lookahead(sat::bool_var bv); unsigned m_no_improve_bool = 0;