mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 13:10:50 +00:00
Code Activity

adding lookahead mode to arithmetic sls solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-11 15:47:17 -08:00
parent 847278fba8
commit d97bd48669
7 changed files with 575 additions and 207 deletions
Download patch file Download diff file Expand all files Collapse all files

601
src/ast/sls/sls_arith_base.cpp
View file

@ -43,6 +43,7 @@ Done:
#include "ast/sls/sls_arith_base.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "params/sls_params.hpp"
#include <cmath>
namespace sls {
@ -388,7 +389,9 @@ namespace sls {
}
template<typename num_t>
void arith_base<num_t>::find_linear_moves(ineq const& ineq, var_t v, num_t const& coeff, num_t const& sum) {
void arith_base<num_t>::find_linear_moves(ineq const& ineq, var_t v, num_t const& coeff) {
num_t const& sum = ineq.m_args_value;
TRACE("arith_verbose", tout << ineq << " " << v << " " << value(v) << "\n");
if (ineq.is_true()) {
switch (ineq.m_op) {
case ineq_kind::LE:
@ -426,6 +429,7 @@ namespace sls {
delta = sum < 0 ? divide(v, abs(sum), coeff) : -divide(v, sum, coeff);
if (sum + coeff * delta == 0)
add_update(v, delta);
break;
}
default:
@ -441,17 +445,23 @@ namespace sls {
delta_out = delta;
if (m_last_var == v && m_last_delta == -delta)
if (m_last_var == v && m_last_delta == -delta) {
TRACE("arith", tout << "flip back " << v << " " << delta << "\n";);
return false;
}
if (m_use_tabu && vi.is_tabu(m_stats.m_num_steps, delta))
if (m_use_tabu && vi.is_tabu(m_stats.m_num_steps, delta)) {
TRACE("arith", tout << "tabu\n");
return false;
}
auto old_value = value(v);
auto new_value = old_value + delta;
if (!vi.in_range(new_value))
if (!vi.in_range(new_value)) {
TRACE("arith", tout << "out of range: v" << v << " " << old_value << " " << delta << " " << new_value << "\n";);
return false;
}
if (m_use_tabu && !in_bounds(v, new_value) && in_bounds(v, old_value)) {
@ -556,7 +566,7 @@ namespace sls {
for (auto const& [coeff, x] : ineq->m_args) {
if (is_fixed(x))
continue;
find_linear_moves(*ineq, x, coeff, ineq->m_args_value);
find_linear_moves(*ineq, x, coeff);
}
}
return apply_update();
@ -667,7 +677,7 @@ namespace sls {
}
buffer<sat::bool_var> to_flip;
for (auto const& [coeff, bv] : vi.m_ineqs) {
for (auto const& [coeff, bv] : vi.m_linear_occurs) {
auto& ineq = *get_ineq(bv);
bool old_sign = sign(bv);
sat::literal lit(bv, old_sign);
@ -781,11 +791,9 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::add_args(linear_term& term, expr* e, num_t const& coeff) {
auto v = m_expr2var.get(e->get_id(), UINT_MAX);
expr* x, * y;
expr* x, * y, * z, * u;
num_t i;
if (v != UINT_MAX)
add_arg(term, coeff, v);
else if (is_num(e, i))
if (is_num(e, i))
term.m_coeff += coeff * i;
else if (a.is_add(e)) {
for (expr* arg : *to_app(e))
@ -798,6 +806,18 @@ namespace sls {
else if (a.is_mul(e, x, y) && is_num(x, i)) {
add_args(term, y, i * coeff);
}
else if (a.is_mul(e, x, y) && a.is_add(y, z, u)) {
expr_ref t(a.mk_mul(x, z), m);
add_args(term, t, coeff);
t = a.mk_mul(x, u);
add_args(term, t, coeff);
}
else if (a.is_mul(e, x, y) && a.is_add(x, z, u)) {
expr_ref t(a.mk_mul(y, z), m);
add_args(term, t, coeff);
t = a.mk_mul(y, u);
add_args(term, t, coeff);
}
else if (a.is_mul(e)) {
unsigned_vector ms;
for (expr* arg : *to_app(e))
@ -812,7 +832,13 @@ namespace sls {
break;
default: {
v = mk_var(e);
unsigned idx = m_muls.size();
for (idx = 0; idx < m_muls.size(); ++idx)
if (m_muls[idx].m_var == v)
break;
if (idx == m_muls.size()) {
std::stable_sort(ms.begin(), ms.end(), [&](unsigned a, unsigned b) { return a < b; });
svector<std::pair<unsigned, unsigned>> mp;
for (unsigned i = 0; i < ms.size(); ++i) {
@ -822,6 +848,7 @@ namespace sls {
++p, ++i;
mp.push_back({ w, p });
}
m_muls.push_back({ v, mp });
num_t prod(1);
for (auto [w, p] : mp)
@ -829,6 +856,7 @@ namespace sls {
m_vars[v].m_def_idx = idx;
m_vars[v].m_op = arith_op_kind::OP_MUL;
m_vars[v].set_value(prod);
}
add_arg(term, coeff, v);
break;
}
@ -836,6 +864,8 @@ namespace sls {
}
else if (a.is_uminus(e, x))
add_args(term, x, -coeff);
else if (v != UINT_MAX)
add_arg(term, coeff, v);
else if (a.is_mod(e, x, y) || a.is_mod0(e, x, y))
add_arg(term, coeff, mk_op(arith_op_kind::OP_MOD, e, x, y));
else if (a.is_idiv(e, x, y) || a.is_idiv0(e, x, y))
@ -1004,7 +1034,7 @@ namespace sls {
// compute the value of the linear term, and accumulate non-linear sub-terms
i.m_args_value = i.m_coeff;
for (auto const& [coeff, v] : i.m_args) {
m_vars[v].m_ineqs.push_back({ coeff, bv });
m_vars[v].m_linear_occurs.push_back({ coeff, bv });
i.m_args_value += coeff * value(v);
if (is_mul(v)) {
auto const& [w, monomial] = get_mul(v);
@ -1202,6 +1232,8 @@ namespace sls {
void arith_base<num_t>::initialize() {
for (auto lit : ctx.unit_literals())
initialize_unit(lit);
for (auto f : ctx.input_assertions())
initialize_input_assertion(f);
for (unsigned v = 0; v < m_vars.size(); ++v) {
auto const& vi = m_vars[v];
if (vi.m_lo || vi.m_hi)
@ -1337,6 +1369,29 @@ namespace sls {
}
}
template<typename num_t>
void arith_base<num_t>::initialize_input_assertion(expr* f) {
if (m.is_or(f)) {
var_t v = UINT_MAX;
expr* x, * y;
vector<num_t> values;
for (expr* arg : *to_app(f)) {
num_t n;
if (m.is_eq(arg, x, y) && is_num(y, n)) {
var_t w = m_expr2var.get(x->get_id(), UINT_MAX);
if (w != UINT_MAX && (v == w || v == UINT_MAX))
v = w, values.push_back(n);
else
return;
}
else
return;
}
m_vars[v].m_finite_domain.append(values);
return;
}
}
template<typename num_t>
void arith_base<num_t>::initialize_unit(sat::literal lit) {
init_bool_var(lit.var());
@ -1630,12 +1685,11 @@ namespace sls {
double arith_base<num_t>::compute_score(var_t x, num_t const& delta) {
int result = 0;
int breaks = 0;
for (auto const& [coeff, bv] : m_vars[x].m_ineqs) {
for (auto const& [coeff, bv] : m_vars[x].m_linear_occurs) {
bool old_sign = sign(bv);
auto lit = sat::literal(bv, old_sign);
auto dtt_old = dtt(old_sign, *get_ineq(bv));
auto dtt_new = dtt(old_sign, *get_ineq(bv), coeff, delta);
#if 1
if (dtt_new == 0 && dtt_old != 0)
result += 1;
@ -1645,14 +1699,6 @@ namespace sls {
result -= 1;
breaks += 1;
}
#else
if (dtt_new == dtt_old)
continue;
if (m_use_tabu && ctx.is_unit(lit) && dtt_new != 0)
return 0;
double reward = ctx.reward(bv);
result += reward;
#endif
}
if (result < 0)
@ -1726,7 +1772,7 @@ namespace sls {
if (is_fixed(x))
continue;
if (is_linear(x, nl, b))
find_linear_moves(*ineq, x, b, ineq->m_args_value);
find_linear_moves(*ineq, x, b);
else if (is_quadratic(x, nl, a, b))
find_quadratic_moves(*ineq, x, a, b, ineq->m_args_value);
else
@ -2149,9 +2195,9 @@ namespace sls {
out << " ";
}
if (!vi.m_ineqs.empty()) {
if (!vi.m_linear_occurs.empty()) {
out << " bool: ";
for (auto [c, bv] : vi.m_ineqs)
for (auto [c, bv] : vi.m_linear_occurs)
out << c << "@" << bv << " ";
}
return out;
@ -2260,12 +2306,9 @@ namespace sls {
if (ineq)
invariant(*ineq);
}
auto& out = verbose_stream();
for (var_t v = 0; v < m_vars.size(); ++v) {
if (!eval_is_correct(v)) {
auto report_error = [&](std::ostream& out, var_t v) {
display(out);
display(out, v) << "\n";
display(out << "variable: ", v) << "\n";
out << mk_bounded_pp(m_vars[v].m_expr, m) << "\n";
if (is_mul(v)) {
@ -2289,7 +2332,12 @@ namespace sls {
out << "v" << ad.m_var << " := ";
display(out, ad) << "\n";
}
};
auto& out = verbose_stream();
for (var_t v = 0; v < m_vars.size(); ++v) {
if (!eval_is_correct(v)) {
report_error(verbose_stream(), v);
TRACE("arith", report_error(tout, v));
UNREACHABLE();
}
}
@ -2300,8 +2348,11 @@ namespace sls {
num_t val = i.m_coeff;
for (auto const& [c, v] : i.m_args)
val += c * value(v);
if (val != i.m_args_value)
if (val != i.m_args_value) {
verbose_stream() << val << ": " << i << "\n";
display(verbose_stream());
TRACE("arith", display(tout << val << ": " << i << "\n"));
}
SASSERT(val == i.m_args_value);
VERIFY(val == i.m_args_value);
}
@ -2310,6 +2361,7 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::collect_statistics(statistics& st) const {
st.update("sls-arith-flips", m_stats.m_num_steps);
st.update("sls-arith-moves", m_stats.m_moves);
}
template<typename num_t>
@ -2322,7 +2374,7 @@ namespace sls {
template<typename num_t>
arith_base<num_t>::bool_info& arith_base<num_t>::get_bool_info(expr* e) {
m_bool_info.reserve(e->get_id() + 1, { m_config.paws_init, 0, 1, l_undef });
m_bool_info.reserve(e->get_id() + 1, bool_info(m_config.paws_init));
return m_bool_info[e->get_id()];
}
@ -2334,12 +2386,11 @@ namespace sls {
if (is_uninterp(e))
return ctx.get_value(e) == l_true;
app* a = to_app(e);
if (a->get_family_id() == basic_family_id) {
bool r = get_basic_bool_value(a);
get_bool_info(e).value = to_lbool(r);
return r;
}
app* ap = to_app(e);
bool is_arith_eq = m.is_eq(e) && a.is_int_real(ap->get_arg(0));
if (ap->get_family_id() == basic_family_id && !is_arith_eq)
return get_basic_bool_value(ap);
auto v = ctx.atom2bool_var(e);
if (v == sat::null_bool_var)
@ -2347,9 +2398,7 @@ namespace sls {
auto const* ineq = get_ineq(v);
if (!ineq)
return false;
auto r = ineq->is_true() == ctx.is_true(v);
get_bool_info(e).value = to_lbool(r);
return r;
return ineq->is_true();
}
template<typename num_t>
@ -2384,9 +2433,9 @@ namespace sls {
case OP_EQ:
if (m.is_bool(e->get_arg(0)))
return get_bool_value(e->get_arg(0)) == get_bool_value(e->get_arg(1));
NOT_IMPLEMENTED_YET();
return ctx.get_value(e->get_arg(0)) == ctx.get_value(e->get_arg(1));
case OP_DISTINCT:
NOT_IMPLEMENTED_YET();
return false;
default:
NOT_IMPLEMENTED_YET();
}
@ -2397,7 +2446,15 @@ namespace sls {
void arith_base<num_t>::initialize_bool_assignment() {
for (auto t : ctx.subterms())
if (m.is_bool(t))
get_bool_value(t);
set_bool_value(t, get_bool_value_rec(t));
#if 0
for (auto t : ctx.subterms()) {
if (m.is_bool(t))
verbose_stream() << mk_bounded_pp(t, m) << " := " << get_bool_value(t) << "\n";
else
verbose_stream() << mk_bounded_pp(t, m) << " := " << ctx.get_value(t) << "\n";
}
#endif
}
template<typename num_t>
@ -2420,7 +2477,6 @@ namespace sls {
double arith_base<num_t>::new_score(expr* a, bool is_true) {
bool is_true_new = get_bool_value(a);
//verbose_stream() << "compute score " << mk_bounded_pp(a, m) << " is-true " << is_true << " is-true-new " << is_true_new << "\n";
if (is_true == is_true_new)
return 1;
if (is_uninterp(a))
@ -2502,12 +2558,14 @@ namespace sls {
break;
}
SASSERT(value > 0);
unsigned max_value = 10000;
unsigned max_value = 1000;
if (value > max_value)
return 1.0;
return 0.0;
auto d = value.get_double();
return 1.0 - ((d * d) / ((double)max_value * (double)max_value));
double score = 1.0 - ((d * d) / ((double)max_value * (double)max_value));
return score;
}
template<typename num_t>
@ -2547,9 +2605,10 @@ namespace sls {
}
}
}
m_update_stack.reserve(m_max_depth + 1);
}
template<typename num_t>
double arith_base<num_t>::lookahead(expr* t) {
double arith_base<num_t>::lookahead(expr* t, bool update_score) {
SASSERT(a.is_int_real(t) || m.is_bool(t));
double score = m_top_score;
for (unsigned depth = m_min_depth; depth <= m_max_depth; ++depth) {
@ -2558,8 +2617,12 @@ namespace sls {
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(a, m) << " depth: " << depth << "\n";);
if (t != a)
set_bool_value(a, get_bool_value_rec(a));
if (m_is_root.is_marked(a))
score += get_weight(a) * (new_score(a) - old_score(a));
if (m_is_root.is_marked(a)) {
auto nscore = new_score(a);
score += get_weight(a) * (nscore - old_score(a));
if (update_score)
set_score(a, nscore);
}
}
}
return score;
@ -2567,8 +2630,6 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::insert_update_stack(expr* t) {
if (!m.is_bool(t))
return;
unsigned depth = get_depth(t);
m_update_stack.reserve(depth + 1);
if (!m_in_update_stack.is_marked(t) && is_app(t)) {
@ -2579,39 +2640,51 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::clear_update_stack() {
lookahead(nullptr);
m_in_update_stack.reset();
m_update_stack.reserve(m_max_depth + 1);
for (unsigned i = m_min_depth; i <= m_max_depth; ++i)
m_update_stack[i].reset();
}
template<typename num_t>
void arith_base<num_t>::lookahead_num(var_t v, num_t const& new_value) {
void arith_base<num_t>::lookahead_num(var_t v, num_t const& delta) {
num_t old_value = value(v);
if (!update(v, new_value))
if (!update_num(v, delta))
return;
num_t new_value = old_value + delta;
expr* e = m_vars[v].m_expr;
auto score = lookahead(e);
if (m_last_expr != e) {
if (m_last_expr)
lookahead(m_last_expr, false);
clear_update_stack();
insert_update_stack_rec(e);
m_last_expr = e;
}
auto score = lookahead(e, false);
TRACE("arith_verbose", tout << "lookahead " << v << " " << mk_bounded_pp(e, m) << " := " << delta + old_value << " " << score << " (" << m_best_score << ")\n";);
if (score > m_best_score) {
m_best_score = score;
m_best_value = new_value;
m_best_expr = e;
}
VERIFY(update(v, old_value));
lookahead(e);
// revert back to old value
update_args_value(v, old_value);
}
template<typename num_t>
void arith_base<num_t>::lookahead_bool(expr* e) {
bool b = get_bool_value(e);
set_bool_value(e, !b);
auto score = lookahead(e);
auto score = lookahead(e, false);
if (score > m_best_score) {
m_best_score = score;
m_best_expr = e;
}
set_bool_value(e, b);
lookahead(e, false);
}
// for every variable e, for every atom containing e
@ -2619,38 +2692,60 @@ namespace sls {
// m_fixable_atoms contains atoms that can be fixed.
// m_fixable_vars contains variables that can be updated.
template<typename num_t>
void arith_base<num_t>::add_lookahead(expr* e) {
if (m.is_bool(e)) {
auto bv = ctx.atom2bool_var(e);
if (m_fixable_atoms.contains(bv))
lookahead_bool(e);
}
else if (a.is_int_real(e)) {
auto v = mk_term(e);
auto& vi = m_vars[v];
for (auto [coeff, bv] : vi.m_ineqs) {
if (!m_fixable_atoms.contains(bv))
continue;
void arith_base<num_t>::add_lookahead(bool_info& i, expr* e) {
auto add_atom = [&](sat::bool_var bv) {
if (!i.fixable_atoms.contains(bv))
return;
if (m_fixed_atoms.contains(bv))
return;
auto a = ctx.atom(bv);
if (!a)
continue;
return;
auto* ineq = get_ineq(bv);
if (!ineq)
continue;
return;
num_t na, nb;
for (auto const& [x, nl] : ineq->m_nonlinear) {
if (!m_fixable_vars.contains(x))
if (!i.fixable_vars.contains(x))
continue;
if (is_fixed(x))
continue;
if (is_linear(x, nl, nb))
find_linear_moves(*ineq, x, nb, ineq->m_args_value);
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
;
}
m_fixable_atoms.remove(bv);
m_fixed_atoms.insert(bv);
};
auto add_finite_domain = [&](var_t v) {
auto old_value = value(v);
for (auto const& n : m_vars[v].m_finite_domain)
add_update(v, n - old_value);
};
if (m.is_bool(e)) {
auto bv = ctx.atom2bool_var(e);
if (i.fixable_atoms.contains(bv))
lookahead_bool(e);
}
else if (a.is_int_real(e)) {
auto v = mk_term(e);
auto& vi = m_vars[v];
if (false && !vi.m_finite_domain.empty()) {
add_finite_domain(v);
return;
}
for (auto const& [coeff, bv] : vi.m_linear_occurs)
add_atom(bv);
for (auto const& idx : vi.m_muls) {
auto const& [x, monomial] = m_muls[idx];
for (auto [coeff, bv] : m_vars[x].m_linear_occurs)
add_atom(bv);
}
}
}
@ -2661,111 +2756,170 @@ namespace sls {
// candidate expressions may be either numeric or boolean variables.
//
template<typename num_t>
void arith_base<num_t>::add_fixable(expr* e) {
m_fixable_exprs.reset();
m_fixable_atoms.reset();
m_fixable_vars.reset();
ptr_vector<expr> const& arith_base<num_t>::get_fixable_exprs(expr* e) {
auto& i = get_bool_info(e);
if (!i.fixable_exprs.empty())
return i.fixable_exprs;
expr_mark visited;
buffer<std::pair<expr*, lbool>> todo;
expr* x, * y, * z;
todo.push_back({ e, l_true });
ptr_buffer<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
auto [e, is_true] = todo.back();
auto e = todo.back();
todo.pop_back();
if (visited.is_marked(e))
continue;
visited.mark(e);
if (is_true == l_true && get_bool_value(e))
continue;
if (is_true == l_false && !get_bool_value(e))
continue;
if (m.is_not(e, e))
todo.push_back({ e, ~is_true });
else if (m.is_and(e) || m.is_or(e)) {
if (m.is_xor(e) || m.is_and(e) || m.is_or(e) || m.is_implies(e) || m.is_iff(e) || m.is_ite(e) || m.is_not(e)) {
for (auto arg : *to_app(e))
todo.push_back({ arg, is_true });
}
else if (m.is_implies(e, x, y)) {
todo.push_back({ x, ~is_true });
todo.push_back({ y, is_true });
}
else if (m.is_iff(e, x, y)) {
todo.push_back({ x, l_undef });
todo.push_back({ y, l_undef });
}
else if (m.is_ite(e, x, y, z)) {
todo.push_back({ x, l_undef });
todo.push_back({ y, is_true });
todo.push_back({ z, ~is_true });
todo.push_back(arg);
}
else {
auto bv = ctx.atom2bool_var(e);
if (bv == sat::null_bool_var)
continue;
if (is_uninterp(e)) {
if (!m_fixable_atoms.contains(bv)) {
m_fixable_atoms.insert(bv);
m_fixable_exprs.push_back(e);
if (!i.fixable_atoms.contains(bv)) {
i.fixable_atoms.insert(bv);
i.fixable_exprs.push_back(e);
}
continue;
}
auto* ineq = get_ineq(bv);
if (!ineq)
continue;
m_fixable_atoms.insert(bv);
for (auto& [v, occ] : ineq->m_nonlinear) {
if (m_fixable_vars.contains(v))
i.fixable_atoms.insert(bv);
buffer<var_t> vars;
for (auto& [v, occ] : ineq->m_nonlinear)
vars.push_back(v);
for (unsigned j = 0; j < vars.size(); ++j) {
auto v = vars[j];
if (i.fixable_vars.contains(v))
continue;
m_fixable_vars.insert(v);
m_fixable_exprs.push_back(m_vars[v].m_expr);
if (is_add(v)) {
for (auto [c, w] : get_add(v).m_args)
vars.push_back(w);
}
else if (is_mul(v)) {
for (auto [w, p] : get_mul(v).m_monomial)
vars.push_back(w);
}
else {
i.fixable_exprs.push_back(m_vars[v].m_expr);
i.fixable_vars.insert(v);
}
}
}
}
return i.fixable_exprs;
}
template<typename num_t>
bool arith_base<num_t>::apply_move(expr* t, bool randomize) {
add_fixable(t);
auto& vars = m_fixable_exprs;
bool arith_base<num_t>::apply_move(expr* f, ptr_vector<expr> const& vars, arith_move_type t) {
if (vars.empty())
return false;
auto& info = get_bool_info(f);
m_best_expr = nullptr;
m_best_score = m_top_score;
unsigned sz = vars.size();
unsigned start = ctx.rand();
m_updates.reset();
insert_update_stack_rec(t);
for (unsigned i = 0; i < sz; ++i)
add_lookahead(vars[(start + i) % sz]);
m_fixed_atoms.reset();
if (randomize) {
switch (t) {
case arith_move_type::random_update: {
for (unsigned i = 0; i < sz; ++i)
add_lookahead(info, vars[(start + i) % sz]);
if (m_updates.empty())
return false;
auto& [v, new_value, score] = m_updates[ctx.rand() % m_updates.size()];
unsigned idx = ctx.rand() % m_updates.size();
auto& [v, delta, score] = m_updates[idx];
m_best_expr = m_vars[v].m_expr;
m_best_value = value(v) + delta;
break;
}
else {
for (auto const& [v, new_value, score] : m_updates)
lookahead_num(v, new_value);
case arith_move_type::hillclimb: {
for (unsigned i = 0; i < sz; ++i)
add_lookahead(info, vars[(start + i) % sz]);
if (m_updates.empty())
return false;
std::stable_sort(m_updates.begin(), m_updates.end(), [](auto const& a, auto const& b) { return a.m_var < b.m_var; });
m_last_expr = nullptr;
sz = m_updates.size();
for (unsigned i = 0; i < sz; ++i) {
auto const& [v, delta, score] = m_updates[(start + i) % m_updates.size()];
lookahead_num(v, delta);
}
if (m_best_expr)
m_top_score = lookahead(m_best_expr);
if (m_last_expr) {
lookahead(m_last_expr, false);
clear_update_stack();
}
break;
}
case arith_move_type::random_inc_dec: {
auto e = vars[ctx.rand() % sz];
m_best_expr = e;
if (a.is_int_real(e)) {
var_t v = mk_term(e);
if (ctx.rand(2) == 0)
m_best_value = value(v) + 1;
else
m_best_value = value(v) - 1;
}
break;
}
}
CTRACE("bv", !m_best_expr, tout << "no guided move\n";);
if (m_best_expr) {
if (m.is_bool(m_best_expr))
set_bool_value(m_best_expr, !get_bool_value(m_best_expr));
else {
var_t v = mk_term(m_best_expr);
if (!update_num(v, m_best_value - value(v))) {
TRACE("arith",
tout << "could not move v" << v << " " << t << " " << mk_bounded_pp(m_best_expr, m) << " := " << value(v) << " " << m_top_score << "\n";
);
return false;
}
}
insert_update_stack_rec(m_best_expr);
m_top_score = lookahead(m_best_expr, true);
clear_update_stack();
}
CTRACE("arith", !m_best_expr, tout << "no move " << t << "\n";);
CTRACE("arith", m_best_expr && a.is_int_real(m_best_expr), {
var_t v = mk_term(m_best_expr);
tout << t << " v" << v << " " << mk_bounded_pp(m_best_expr, m) << " := " << value(v) << " " << m_top_score << "\n";
});
return !!m_best_expr;
}
std::ostream& operator<<(std::ostream& out, arith_move_type mt) {
switch (mt) {
case arith_move_type::random_update: out << "random-update"; break;
case arith_move_type::hillclimb: out << "hillclimb"; break;
case arith_move_type::random_inc_dec: out << "random-inc-dec"; break;
}
return out;
}
template<typename num_t>
void arith_base<num_t>::global_search() {
initialize_bool_assignment();
rescore();
m_config.max_moves = m_stats.m_moves + m_config.max_moves_base;
TRACE("bv", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
TRACE("arith", tout << "search " << m_stats.m_moves << " " << m_config.max_moves << "\n";);
IF_VERBOSE(1, verbose_stream() << "lookahead-search moves:" << m_stats.m_moves << " max-moves:" << m_config.max_moves << "\n");
TRACE("arith", display(tout));
bool loop_again = true;
while (m.inc() && m_stats.m_moves < m_config.max_moves) {
loop_again = false;
m_stats.m_moves++;
check_restart();
@ -2774,31 +2928,204 @@ namespace sls {
if (!t)
break;
if (apply_move(t, false))
auto& vars = get_fixable_exprs(t);
if (vars.empty())
return;
if (ctx.rand(2047) < m_config.wp && apply_move(t, vars, arith_move_type::random_inc_dec))
continue;
if (apply_move(t, true))
if (apply_move(t, vars, arith_move_type::hillclimb))
continue;
if (apply_move(t, vars, arith_move_type::random_update))
recalibrate_weights();
loop_again = true;
}
if (loop_again)
m_config.max_moves_base += 100;
finalize_bool_assignment();
}
template<typename num_t>
expr* arith_base<num_t>::get_candidate_unsat() {
unsigned n = 0;
expr* r = nullptr;
expr* e = nullptr;
if (m_config.ucb) {
double max = -1.0;
for (auto a : ctx.input_assertions()) {
if (!get_bool_value(a) && (ctx.rand() % (++n)) == 0)
r = a;
if (get_bool_value(a))
continue;
auto const& vars = get_fixable_exprs(a);
if (vars.empty())
continue;
auto score = old_score(a);
auto q = score
+ m_config.ucb_constant * ::sqrt(log((double)m_touched) / get_touched(a))
+ m_config.ucb_noise * ctx.rand(512);
if (q > max)
max = q, e = a;
}
return r;
if (e) {
m_touched++;
inc_touched(e);
}
}
else {
unsigned n = 0;
for (auto a : ctx.input_assertions())
if (!get_bool_value(a) && !get_fixable_exprs(a).empty() && ctx.rand() % ++n == 0)
e = a;
}
m_last_atom = e;
CTRACE("arith", !e, "no candidate\n";);
CTRACE("arith", e,
tout << "select " << mk_bounded_pp(e, m) << " ";
for (auto v : get_fixable_exprs(e))
tout << mk_bounded_pp(v, m) << " ";
tout << "\n");
return e;
}
template<typename num_t>
bool arith_base<num_t>::can_update_num(var_t v, num_t const& delta) {
num_t old_value = value(v);
num_t new_value = old_value + delta;
auto& vi = m_vars[v];
//expr* e = vi.m_expr;
if (old_value == new_value)
return true;
if (!vi.in_range(new_value)) {
TRACE("arith", tout << "Not in range v" << v << " " << new_value << "\n");
return false;
}
if (!in_bounds(v, new_value) && in_bounds(v, old_value)) {
TRACE("arith", tout << "out of bounds v" << v << " " << new_value << "\n");
//verbose_stream() << "out of bounds v" << v << " " << new_value << "\n";
return false;
}
// check for overflow
try {
for (auto idx : vi.m_muls) {
auto const& [w, monomial] = m_muls[idx];
num_t prod(1);
for (auto [w, p] : monomial)
prod *= power_of(v == w ? new_value : value(w), p);
}
}
catch (overflow_exception const&) {
return false;
}
return true;
}
template<typename num_t>
bool arith_base<num_t>::update_num(var_t v, num_t const& delta) {
if (delta == 0)
return true;
if (!can_update_num(v, delta))
return false;
auto& vi = m_vars[v];
auto old_value = vi.value();
num_t new_value = old_value + delta;
update_args_value(v, new_value);
return true;
}
template<typename num_t>
void arith_base<num_t>::update_args_value(var_t v, num_t const& new_value) {
auto& vi = m_vars[v];
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);
update_args_value(x, new_prod);
}
for (auto const& idx : vi.m_adds) {
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));
update_args_value(ad.m_var, new_sum);
}
auto old_value = value(v);
for (auto const& [coeff, bv] : vi.m_linear_occurs) {
auto& ineq = *get_ineq(bv);
ineq.m_args_value += coeff * (new_value - old_value);
}
IF_VERBOSE(5, verbose_stream() << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
vi.set_value(new_value);
}
template<typename num_t>
void arith_base<num_t>::check_restart() {
if (m_stats.m_moves % m_config.restart_base == 0) {
ucb_forget();
rescore();
}
if (m_stats.m_moves < m_config.restart_next)
return;
++m_stats.m_restarts;
m_config.restart_next = std::max(m_config.restart_next, m_stats.m_moves);
if (0x1 == (m_stats.m_restarts & 0x1))
m_config.restart_next += m_config.restart_base;
else
m_config.restart_next += (2 * (m_stats.m_restarts >> 1)) * m_config.restart_base;
// reset_uninterp_in_false_literals
rescore();
}
template<typename num_t>
void arith_base<num_t>::ucb_forget() {
if (m_config.ucb_forget >= 1.0)
return;
for (auto a : ctx.input_assertions()) {
auto touched_old = get_touched(a);
auto touched_new = static_cast<unsigned>((touched_old - 1) * m_config.ucb_forget + 1);
set_touched(a, touched_new);
m_touched += touched_new - touched_old;
}
}
template<typename num_t>
void arith_base<num_t>::updt_params() {
if (m_config.config_initialized)
return;
sls_params p(ctx.get_params());
m_config.paws_init = p.paws_init();
m_config.paws_sp = p.paws_sp();
//m_config.ucb = p.ucb();
//m_config.ucb_constant = p.ucb_constant();
//m_config.ucb_noise = p.ucb_noise();
//m_config.ucb_forget = p.ucb_forget();
m_config.wp = p.wp();
m_config.restart_base = p.restart_base();
//m_config.restart_next = p.restart_next();
//m_config.max_moves_base = p.max_moves_base();
//m_config.max_moves = p.max_moves();
m_config.arith_use_lookahead = p.arith_use_lookahead();
m_config.config_initialized = true;
}
template<typename num_t>
void arith_base<num_t>::start_propagation() {
updt_params();
if (m_config.arith_use_lookahead)
global_search();
}
}

59
src/ast/sls/sls_arith_base.h
View file

@ -27,6 +27,14 @@ namespace sls {
using theory_var = int;
enum arith_move_type {
hillclimb,
random_update,
random_inc_dec
};
std::ostream& operator<<(std::ostream& out, arith_move_type mt);
// local search portion for arithmetic
template<typename num_t>
class arith_base : public plugin {
@ -37,6 +45,7 @@ namespace sls {
typedef unsigned atom_t;
struct config {
bool config_initialized = false;
double cb = 2.85;
unsigned L = 20;
unsigned t = 45;
@ -47,11 +56,22 @@ namespace sls {
bool paws = true;
unsigned max_moves = 500;
unsigned max_moves_base = 500;
unsigned wp = 100;
bool ucb = true;
double ucb_constant = 1.0;
double ucb_forget = 0.1;
bool ucb_init = false;
double ucb_noise = 0.1;
unsigned restart_base = 1000;
unsigned restart_next = 1000;
unsigned restart_init = 1000;
bool arith_use_lookahead = false;
};
struct stats {
unsigned m_num_steps = 0;
unsigned m_moves = 0;
unsigned m_restarts = 0;
};
public:
@ -93,10 +113,11 @@ namespace sls {
var_sort m_sort;
arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP;
unsigned m_def_idx = UINT_MAX;
vector<std::pair<num_t, sat::bool_var>> m_ineqs;
vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
unsigned_vector m_muls;
unsigned_vector m_adds;
optional<bound> m_lo, m_hi;
vector<num_t> m_finite_domain;
num_t const& value() const { return m_value; }
void set_value(num_t const& v) { m_value = v; }
@ -187,6 +208,7 @@ namespace sls {
unsigned get_num_vars() const { return m_vars.size(); }
void updt_params();
bool is_distinct(expr* e);
bool eval_distinct(expr* e);
void repair_distinct(expr* e);
@ -247,7 +269,7 @@ namespace sls {
bool find_lin_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_linear_moves(ineq const& i, var_t x, num_t const& coeff);
void find_quadratic_moves(ineq const& i, var_t x, num_t const& a, num_t const& b, num_t const& sum);
double compute_score(var_t x, num_t const& delta);
void save_best_values();
@ -273,6 +295,7 @@ namespace sls {
void check_ineqs();
void init_bool_var(sat::bool_var bv);
void initialize_unit(sat::literal lit);
void initialize_input_assertion(expr* f);
void add_le(var_t v, num_t const& n);
void add_ge(var_t v, num_t const& n);
void add_lt(var_t v, num_t const& n);
@ -288,20 +311,25 @@ namespace sls {
struct bool_info {
unsigned weight = 0;
double score = 0;
unsigned touched = 0;
unsigned touched = 1;
lbool value = l_undef;
sat::bool_var_set fixable_atoms;
uint_set fixable_vars;
ptr_vector<expr> fixable_exprs;
bool_info(unsigned w) : weight(w) {}
};
vector<ptr_vector<app>> m_update_stack;
expr_mark m_in_update_stack;
svector<bool_info> m_bool_info;
double m_best_score = 0, m_top_score = 0;
unsigned m_min_depth = 0, m_max_depth = 0;
num_t m_best_value;
expr* m_best_expr = nullptr, * m_last_atom = nullptr;
expr* m_best_expr = nullptr, * m_last_atom = nullptr, * m_last_expr = nullptr;
expr_mark m_is_root;
sat::bool_var_set m_fixable_atoms;
uint_set m_fixable_vars;
ptr_vector<expr> m_fixable_exprs;
unsigned m_touched = 1;
sat::bool_var_set m_fixed_atoms;
bool_info& get_bool_info(expr* e);
bool get_bool_value(expr* e);
bool get_bool_value_rec(expr* e);
@ -313,29 +341,36 @@ namespace sls {
double new_score(expr* e);
double new_score(expr* e, bool is_true);
void set_score(expr* e, double s) { get_bool_info(e).score = s; }
void rescore();
void recalibrate_weights();
void inc_weight(expr* e) { ++get_bool_info(e).weight; }
void dec_weight(expr* e) { auto& i = get_bool_info(e); i.weight = i.weight > m_config.paws_init ? i.weight - 1 : m_config.paws_init; }
unsigned get_weight(expr* e) { return get_bool_info(e).weight; }
unsigned get_touched(expr* e) { return get_bool_info(e).touched; }
void inc_touched(expr* e) { ++get_bool_info(e).touched; }
void set_touched(expr* e, unsigned t) { get_bool_info(e).touched = t; }
void insert_update_stack(expr* t);
void insert_update_stack_rec(expr* t);
void clear_update_stack();
void lookahead_num(var_t v, num_t const& value);
bool can_update_num(var_t v, num_t const& delta);
bool update_num(var_t v, num_t const& delta);
void lookahead_bool(expr* e);
double lookahead(expr* e);
void add_lookahead(expr* e);
void add_fixable(expr* e);
bool apply_move(expr* f, bool randomize);
double lookahead(expr* e, bool update_score);
void add_lookahead(bool_info& i, expr* e);
ptr_vector<expr> const& get_fixable_exprs(expr* e);
bool apply_move(expr* f, ptr_vector<expr> const& vars, arith_move_type t);
expr* get_candidate_unsat();
void check_restart();
void ucb_forget();
void update_args_value(var_t v, num_t const& new_value);
public:
arith_base(context& ctx);
~arith_base() override {}
void register_term(expr* e) override;
bool set_value(expr* e, expr* v) override;
expr_ref get_value(expr* e) override;
void start_propagation() override;
bool is_fixed(expr* e, expr_ref& value) override;
void initialize() override;
void propagate_literal(sat::literal lit) override;

4
src/ast/sls/sls_arith_plugin.cpp
View file

@ -72,6 +72,10 @@ namespace sls {
APPLY_BOTH(initialize());
}
void arith_plugin::start_propagation() {
WITH_FALLBACK(start_propagation());
}
void arith_plugin::propagate_literal(sat::literal lit) {
WITH_FALLBACK(propagate_literal(lit));
}

1
src/ast/sls/sls_arith_plugin.h
View file

@ -32,6 +32,7 @@ namespace sls {
~arith_plugin() override {}
void register_term(expr* e) override;
expr_ref get_value(expr* e) override;
void start_propagation() override;
bool is_fixed(expr* e, expr_ref& value) override;
void initialize() override;
void propagate_literal(sat::literal lit) override;

4
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -304,9 +304,9 @@ namespace sls {
void bv_lookahead::updt_params(params_ref const& _p) {
sls_params p(_p);
if (m_config.updated)
if (m_config.config_initialized)
return;
m_config.updated = true;
m_config.config_initialized = true;
m_config.walksat = p.walksat();
m_config.walksat_repick = p.walksat_repick();
m_config.paws_sp = p.paws_sp();

6
src/ast/sls/sls_bv_lookahead.h
View file

@ -26,7 +26,7 @@ namespace sls {
class bv_lookahead {
struct config {
bool updated = false;
bool config_initialized = false;
double cb = 2.85;
unsigned paws_init = 40;
unsigned paws_sp = 52;
@ -181,11 +181,11 @@ namespace sls {
void finalize_bool_values();
void updt_params(params_ref const& p);
public:
bv_lookahead(bv_eval& ev);
void updt_params(params_ref const& p);
void start_propagation();
void collect_statistics(statistics& st) const;

1
src/params/sls_params.pyg
View file

@ -25,6 +25,7 @@ def_module_params('sls',
('dt_axiomatic', BOOL, True, 'use axiomatic mode or model reduction for datatype solver'),
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed'),
('arith_use_lookahead', BOOL, False, 'use lookahead solver for NIRA'),
('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'),
('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'),