mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

wip experiments with sls

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-14 15:06:21 -08:00
parent 9ce5fe707d
commit 44fcf60a72
3 changed files with 29 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/sat/smt/arith_sls.cpp
View file

@ -35,9 +35,8 @@ namespace arith {
unsigned num_steps = 0;
for (unsigned v = 0; v < s.s().num_vars(); ++v)
init_bool_var_assignment(v);
m_best_min_unsat = unsat().size();
verbose_stream() << "max arith steps " << m_max_arith_steps << "\n";
//m_max_arith_steps = 10000;
m_max_arith_steps = std::max(1000u, m_max_arith_steps);
while (m.inc() && m_best_min_unsat > 0 && num_steps < m_max_arith_steps) {
if (!flip())
break;
@ -50,6 +49,7 @@ namespace arith {
save_best_values();
}
}
store_best_values();
log();
return unsat().empty() ? l_true : l_undef;
}
@ -59,6 +59,11 @@ namespace arith {
}
void sls::save_best_values() {
for (unsigned v = 0; v < s.get_num_vars(); ++v)
m_vars[v].m_best_value = m_vars[v].m_value;
}
void sls::store_best_values() {
// first compute assignment to terms
// then update non-basic variables in tableau.
for (auto const& [t, v] : m_terms) {
@ -80,7 +85,7 @@ namespace arith {
int64_t old_value = 0;
if (s.is_registered_var(v))
old_value = to_numeral(s.get_ivalue(v).x);
int64_t new_value = value(v);
int64_t new_value = m_vars[v].m_best_value;
if (old_value == new_value)
continue;
s.ensure_column(v);
@ -104,6 +109,9 @@ namespace arith {
for (unsigned i = 0; i < d->num_clauses(); ++i)
for (sat::literal lit : *d->get_clause_info(i).m_clause)
init_literal(lit);
for (unsigned v = 0; v < s.s().num_vars(); ++v)
init_bool_var_assignment(v);
m_best_min_unsat = std::numeric_limits<unsigned>::max();
}
void sls::set_bounds_begin() {
@ -115,7 +123,7 @@ namespace arith {
}
void sls::set_bounds_end(unsigned num_literals) {
m_max_arith_steps = (m_config.L * m_max_arith_steps) / num_literals;
m_max_arith_steps = (m_config.L * m_max_arith_steps); // / num_literals;
}
bool sls::flip() {
@ -323,6 +331,9 @@ namespace arith {
int64_t dtt_old = dtt(ineq);
int64_t delta = coeff * (new_value - old_value);
int64_t dtt_new = dtt(ineq.m_args_value + delta, ineq);
if (dtt_old == dtt_new)
continue;
for (auto cl : m_bool_search->get_use_list(lit)) {
auto const& clause = get_clause_info(cl);

1
src/sat/smt/arith_sls.h
View file

@ -148,6 +148,7 @@ namespace arith {
void paws();
int64_t dscore(var_t v, int64_t new_value) const;
void save_best_values();
void store_best_values();
void add_vars();
sls::ineq& new_ineq(ineq_kind op, int64_t const& bound);
void add_arg(sat::literal lit, ineq& ineq, int64_t const& c, var_t v);

14
src/sat/smt/euf_local_search.cpp
View file

@ -40,9 +40,11 @@ namespace euf {
// Non-boolean literals are assumptions to Boolean search
literal_vector assumptions;
#if 0
for (unsigned v = 0; v < phase.size(); ++v)
if (!is_propositional(literal(v)))
assumptions.push_back(literal(v, !bool_search.get_value(v)));
#endif
verbose_stream() << "assumptions " << assumptions.size() << "\n";
@ -51,6 +53,14 @@ namespace euf {
lbool r = bool_search.check(assumptions.size(), assumptions.data(), nullptr);
bool_search.rlimit().pop();
#if 0
// restore state to optimal model
auto const& mdl = bool_search.get_model();
for (unsigned i = 0; i < mdl.size(); ++i)
if ((mdl[i] == l_true) != bool_search.get_value(i))
bool_search.flip(i);
#endif
for (auto* th : m_solvers)
th->local_search(phase);
@ -92,7 +102,9 @@ namespace euf {
count_literal(l);
}
m_max_bool_steps = (m_ls_config.L * num_bool) / num_literals;
m_max_bool_steps = (m_ls_config.L * num_bool); // / num_literals;
m_max_bool_steps = std::max(10000u, m_max_bool_steps);
verbose_stream() << "num literals " << num_literals << " num bool " << num_bool << " max bool steps " << m_max_bool_steps << "\n";
for (auto* th : m_solvers)
th->set_bounds_end(num_literals);