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

align use_list with number of variables during flatten, push clause and bool_vars_of addition into clause and atom creation time.

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-25 20:47:57 -08:00
parent 7fc59b65ad
commit a7010574c8
6 changed files with 72 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/sls/sat_ddfw.cpp
View file

@ -255,12 +255,14 @@ namespace sat {
m_use_list_clauses = m_clauses.size();
m_use_list_index.reset();
m_flat_use_list.reset();
m_use_list.reserve(2 * num_vars());
for (auto const& ul : m_use_list) {
m_use_list_index.push_back(m_flat_use_list.size());
m_flat_use_list.append(ul);
}
m_use_list_index.push_back(m_flat_use_list.size());
init_clause_data();
SASSERT(2 * num_vars() + 1 == m_use_list_index.size());
return true;
}

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

@ -1145,6 +1145,8 @@ namespace sls {
else {
SASSERT(!a.is_arith_expr(e));
}
initialize_of_bool_var(bv);
add_new_terms();
}
@ -1527,52 +1529,72 @@ namespace sls {
throw default_exception("repair is not supported for " + mk_pp(e, m));
}
}
for (unsigned v = 0; v < m_vars.size(); ++v)
initialize_bool_vars_of(v);
}
template<typename num_t>
void arith_base<num_t>::initialize_bool_vars_of(var_t v) {
if (!m_vars[v].m_bool_vars_of.empty())
void arith_base<num_t>::initialize_of_bool_var(sat::bool_var bv) {
auto* ineq = get_ineq(bv);
if (!ineq)
return;
buffer<var_t> todo;
todo.push_back(v);
auto& vi = m_vars[v];
for (auto const& [coeff, v] : ineq->m_args)
todo.push_back(v);
m_tmp_set.reset();
for (unsigned i = 0; i < todo.size(); ++i) {
var_t u = todo[i];
auto& ui = m_vars[u];
for (auto const& idx : ui.m_muls) {
auto& [x, monomial] = m_muls[idx];
bool found = false;
for (auto u : todo) found |= u == x;
if (!found)
todo.push_back(x);
if (m_tmp_set.contains(u))
continue;
m_tmp_set.insert(u);
ui.m_bool_vars_of.push_back(bv);
if (is_add(u)) {
auto const& ad = get_add(u);
for (auto const& [c, w] : ad.m_args)
todo.push_back(w);
}
for (auto const& idx : ui.m_adds) {
auto x = m_adds[idx].m_var;
bool found = false;
for (auto u : todo) found |= u == x;
if (!found)
todo.push_back(x);
if (is_mul(u)) {
auto const& [w, monomial] = get_mul(u);
for (auto [w, p] : monomial)
todo.push_back(w);
}
if (is_op(u)) {
auto const& op = m_ops[ui.m_def_idx];
todo.push_back(op.m_arg1);
todo.push_back(op.m_arg2);
}
for (auto const& [coeff, bv] : ui.m_linear_occurs)
m_tmp_set.insert(bv);
}
for (auto bv : m_tmp_set)
vi.m_bool_vars_of.push_back(bv);
}
m_tmp_nat_set.reset();
m_tmp_nat_set.assure_domain(ctx.clauses().size() + 1);
for (auto bv : vi.m_bool_vars_of) {
for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
for (auto ci : ctx.get_use_list(lit)) {
if (m_tmp_nat_set.contains(ci))
continue;
m_tmp_nat_set.insert(ci);
vi.m_clauses_of.push_back(ci);
}
template<typename num_t>
void arith_base<num_t>::initialize_clauses_of(sat::bool_var bv, unsigned ci) {
auto* ineq = get_ineq(bv);
if (!ineq)
return;
buffer<var_t> todo;
for (auto const& [coeff, v] : ineq->m_args)
todo.push_back(v);
m_tmp_set.reset();
for (unsigned i = 0; i < todo.size(); ++i) {
var_t u = todo[i];
auto& ui = m_vars[u];
if (m_tmp_set.contains(u))
continue;
m_tmp_set.insert(u);
ui.m_clauses_of.push_back(ci);
if (is_add(u)) {
auto const& ad = get_add(u);
for (auto const& [c, w] : ad.m_args)
todo.push_back(w);
}
if (is_mul(u)) {
auto const& [w, monomial] = get_mul(u);
for (auto [w, p] : monomial)
todo.push_back(w);
}
if (is_op(u)) {
auto const& op = m_ops[ui.m_def_idx];
todo.push_back(op.m_arg1);
todo.push_back(op.m_arg2);
}
}
}

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

@ -295,7 +295,8 @@ namespace sls {
double compute_score(var_t x, num_t const& delta);
void save_best_values();
void initialize_bool_vars_of(var_t v);
void initialize_of_bool_var(sat::bool_var v);
void initialize_clauses_of(sat::bool_var v, unsigned cl);
var_t mk_var(expr* e);
var_t mk_term(expr* e);
var_t mk_op(arith_op_kind k, expr* e, expr* x, expr* y);

13
src/ast/sls/sls_arith_clausal.cpp
View file

@ -275,8 +275,8 @@ namespace sls {
DEBUG_CODE(
for (sat::bool_var bv = 0; bv < ctx.num_bool_vars(); ++bv) {
if (a.get_ineq(bv) && a.get_ineq(bv)->is_true() != ctx.is_true(bv)) {
TRACE("arith", tout << bv << " " << *a.get_ineq(bv) << "\n";
tout << a.m_vars[v].m_bool_vars_of << "\n");
TRACE("arith", tout << "bv:" << bv << " " << *a.get_ineq(bv) << ctx.is_true(bv) << "\n";
tout << "bool vars: " << a.m_vars[v].m_bool_vars_of << "\n");
}
VERIFY(!a.get_ineq(bv) || a.get_ineq(bv)->is_true() == ctx.is_true(bv));
});
@ -349,7 +349,6 @@ namespace sls {
vi.set_value(vi.m_hi->value);
else
vi.set_value(num_t(0));
vi.m_bool_vars_of.reset();
}
initialize();
}
@ -365,6 +364,14 @@ namespace sls {
m_no_improve = 0;
m_no_improve_bool = 0;
m_no_improve_arith = 0;
for (; m_num_clauses < ctx.clauses().size(); ++m_num_clauses) {
auto const& c = ctx.get_clause(m_num_clauses);
for (auto lit : c) {
auto bv = lit.var();
if (a.get_ineq(bv))
a.initialize_clauses_of(bv, m_num_clauses);
}
}
}

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

@ -81,6 +81,7 @@ namespace sls {
unsigned m_best_last_step = 0;
unsigned m_num_lookaheads = 0;
double m_best_score = 0;
unsigned m_num_clauses = 0;
// avoid checking the same updates twice
var_t m_last_var = UINT_MAX;

3
src/ast/sls/sls_context.cpp
View file

@ -450,7 +450,7 @@ namespace sls {
sat::literal context::mk_literal(expr* e) {
expr_ref _e(e, m);
SASSERT(!m_input_assertions.contains(e));
sat::literal lit;
bool neg = false;
expr* a, * b, * c;
@ -459,6 +459,7 @@ namespace sls {
auto v = m_atom2bool_var.get(e->get_id(), sat::null_bool_var);
if (v != sat::null_bool_var)
return sat::literal(v, neg);
SASSERT(!m_input_assertions.contains(e));
sat::literal_vector clause;
lit = mk_literal();
register_atom(lit.var(), e);