mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

move sat_ddfw to sls, initiate sls-bv-plugin

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-06 20:14:44 -07:00
parent 833f524887
commit e7104ebb93
23 changed files with 484 additions and 141 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/CMakeLists.txt
View file

@ -4,9 +4,11 @@ z3_add_component(ast_sls
bv_sls.cpp
bv_sls_eval.cpp
bv_sls_fixed.cpp
bv_sls_terms.cpp
bv_sls_terms.cpp
sat_ddfw.cpp
sls_arith_base.cpp
sls_arith_plugin.cpp
sls_bv.cpp
sls_cc.cpp
sls_engine.cpp
sls_smt.cpp

601
src/ast/sls/sat_ddfw.cpp Normal file
View file

@ -0,0 +1,601 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
sat_ddfw.cpp
Abstract:
DDFW Local search module for clauses
Author:
Nikolaj Bjorner, Marijn Heule 2019-4-23
Notes:
http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf
Todo:
- rephase strategy
- experiment with backoff schemes for restarts
- parallel sync
--*/
#include "util/luby.h"
#include "util/trace.h"
#include "ast/sls/sat_ddfw.h"
#include "params/sat_params.hpp"
namespace sat {
ddfw::~ddfw() {
}
lbool ddfw::check(unsigned sz, literal const* assumptions) {
init(sz, assumptions);
if (m_plugin)
check_with_plugin();
else
check_without_plugin();
remove_assumptions();
log();
return m_min_sz == 0 ? l_true : l_undef;
}
void ddfw::check_without_plugin() {
while (m_limit.inc() && m_min_sz > 0) {
if (should_reinit_weights()) do_reinit_weights();
else if (do_flip<false>());
else if (should_restart()) do_restart();
else if (m_parallel_sync && m_parallel_sync());
else shift_weights();
}
}
void ddfw::check_with_plugin() {
m_plugin->init_search();
m_steps_since_progress = 0;
unsigned steps = 0;
save_best_values();
while (m_min_sz != 0 && m_steps_since_progress++ <= 1500000) {
if (should_reinit_weights()) do_reinit_weights();
else if (steps % 5000 == 0) shift_weights(), m_plugin->on_rescale();
else if (should_restart()) do_restart(), m_plugin->on_restart();
else if (do_flip<true>());
else shift_weights(), m_plugin->on_rescale();
++steps;
}
m_plugin->finish_search();
}
void ddfw::log() {
double sec = m_stopwatch.get_current_seconds();
double kflips_per_sec = sec > 0 ? (m_flips - m_last_flips) / (1000.0 * sec) : 0.0;
if (m_last_flips == 0) {
IF_VERBOSE(1, verbose_stream() << "(sat.ddfw :unsat :models :kflips/sec :flips :restarts :reinits :unsat_vars :shifts";
verbose_stream() << ")\n");
}
IF_VERBOSE(1, verbose_stream() << "(sat.ddfw "
<< std::setw(07) << m_min_sz
<< std::setw(07) << m_models.size()
<< std::setw(10) << kflips_per_sec
<< std::setw(10) << m_flips
<< std::setw(10) << m_restart_count
<< std::setw(11) << m_reinit_count
<< std::setw(13) << m_unsat_vars.size()
<< std::setw(9) << m_shifts;
verbose_stream() << ")\n");
m_stopwatch.start();
m_last_flips = m_flips;
}
template<bool uses_plugin>
bool ddfw::do_flip() {
double reward = 0;
bool_var v = pick_var<uses_plugin>(reward);
return apply_flip<uses_plugin>(v, reward);
}
template<bool uses_plugin>
bool ddfw::apply_flip(bool_var v, double reward) {
if (v == null_bool_var)
return false;
if (reward > 0 || (reward == 0 && m_rand(100) <= m_config.m_use_reward_zero_pct)) {
flip(v);
if (m_unsat.size() <= m_min_sz)
save_best_values();
return true;
}
return false;
}
template<bool uses_plugin>
bool_var ddfw::pick_var(double& r) {
double sum_pos = 0;
unsigned n = 1;
bool_var v0 = null_bool_var;
for (bool_var v : m_unsat_vars) {
r = uses_plugin ? plugin_reward(v) : reward(v);
if (r > 0.0)
sum_pos += score(r);
else if (r == 0.0 && sum_pos == 0 && (m_rand() % (n++)) == 0)
v0 = v;
}
if (sum_pos > 0) {
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
for (bool_var v : m_unsat_vars) {
r = uses_plugin && is_external(v) ? m_vars[v].m_last_reward : reward(v);
if (r > 0) {
lim_pos -= score(r);
if (lim_pos <= 0)
return v;
}
}
}
r = 0;
if (v0 != null_bool_var)
return v0;
if (m_unsat_vars.empty())
return null_bool_var;
return m_unsat_vars.elem_at(m_rand(m_unsat_vars.size()));
}
void ddfw::add(unsigned n, literal const* c) {
unsigned idx = m_clauses.size();
m_clauses.push_back(clause_info(n, c, m_config.m_init_clause_weight));
if (n > 2)
++m_num_non_binary_clauses;
for (literal lit : m_clauses.back().m_clause) {
m_use_list.reserve(2*(lit.var()+1));
m_vars.reserve(lit.var()+1);
m_use_list[lit.index()].push_back(idx);
}
}
sat::bool_var ddfw::add_var(bool is_internal) {
auto v = m_vars.size();
m_vars.reserve(v + 1);
m_vars[v].m_internal = is_internal;
return v;
}
/**
* Remove the last clause that was added
*/
void ddfw::del() {
auto& info = m_clauses.back();
for (literal lit : info.m_clause)
m_use_list[lit.index()].pop_back();
m_clauses.pop_back();
if (m_unsat.contains(m_clauses.size()))
m_unsat.remove(m_clauses.size());
}
void ddfw::add_assumptions() {
for (unsigned i = 0; i < m_assumptions.size(); ++i)
add(1, m_assumptions.data() + i);
}
void ddfw::remove_assumptions() {
if (m_assumptions.empty())
return;
for (unsigned i = 0; i < m_assumptions.size(); ++i)
del();
init(0, nullptr);
}
void ddfw::init(unsigned sz, literal const* assumptions) {
m_assumptions.reset();
m_assumptions.append(sz, assumptions);
add_assumptions();
for (unsigned v = 0; v < num_vars(); ++v) {
literal lit(v, false), nlit(v, true);
value(v) = (m_rand() % 2) == 0; // m_use_list[lit.index()].size() >= m_use_list[nlit.index()].size();
}
init_clause_data();
flatten_use_list();
m_reinit_count = 0;
m_reinit_next = m_config.m_reinit_base;
m_restart_count = 0;
m_restart_next = m_config.m_restart_base*2;
#if 0
m_parsync_count = 0;
m_parsync_next = m_config.m_parsync_base;
#endif
m_min_sz = m_unsat.size();
m_flips = 0;
m_last_flips = 0;
m_shifts = 0;
m_stopwatch.start();
}
void ddfw::reinit() {
add_assumptions();
init_clause_data();
flatten_use_list();
}
void ddfw::flatten_use_list() {
m_use_list_index.reset();
m_flat_use_list.reset();
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());
}
void ddfw::flip(bool_var v) {
++m_flips;
literal lit = literal(v, !value(v));
literal nlit = ~lit;
SASSERT(is_true(lit));
for (unsigned cls_idx : use_list(lit)) {
clause_info& ci = m_clauses[cls_idx];
ci.del(lit);
double w = ci.m_weight;
// cls becomes false: flip any variable in clause to receive reward w
switch (ci.m_num_trues) {
case 0: {
m_unsat.insert_fresh(cls_idx);
auto const& c = get_clause(cls_idx);
for (literal l : c) {
inc_reward(l, w);
inc_make(l);
}
inc_reward(lit, w);
break;
}
case 1:
dec_reward(to_literal(ci.m_trues), w);
break;
default:
break;
}
}
for (unsigned cls_idx : use_list(nlit)) {
clause_info& ci = m_clauses[cls_idx];
double w = ci.m_weight;
// the clause used to have a single true (pivot) literal, now it has two.
// Then the previous pivot is no longer penalized for flipping.
switch (ci.m_num_trues) {
case 0: {
m_unsat.remove(cls_idx);
auto const& c = get_clause(cls_idx);
for (literal l : c) {
dec_reward(l, w);
dec_make(l);
}
dec_reward(nlit, w);
break;
}
case 1:
inc_reward(to_literal(ci.m_trues), w);
break;
default:
break;
}
ci.add(nlit);
}
value(v) = !value(v);
update_reward_avg(v);
}
bool ddfw::should_reinit_weights() {
return m_flips >= m_reinit_next;
}
void ddfw::do_reinit_weights() {
log();
if (m_reinit_count % 2 == 0) {
for (auto& ci : m_clauses)
ci.m_weight += 1;
}
else {
for (auto& ci : m_clauses)
if (ci.is_true())
ci.m_weight = m_config.m_init_clause_weight;
else
ci.m_weight = m_config.m_init_clause_weight + 1;
}
init_clause_data();
++m_reinit_count;
m_reinit_next += m_reinit_count * m_config.m_reinit_base;
}
void ddfw::init_clause_data() {
for (unsigned v = 0; v < num_vars(); ++v) {
make_count(v) = 0;
reward(v) = 0;
}
m_unsat_vars.reset();
m_unsat.reset();
unsigned sz = m_clauses.size();
for (unsigned i = 0; i < sz; ++i) {
auto& ci = m_clauses[i];
auto const& c = get_clause(i);
ci.m_trues = 0;
ci.m_num_trues = 0;
for (literal lit : c)
if (is_true(lit))
ci.add(lit);
switch (ci.m_num_trues) {
case 0:
for (literal lit : c) {
inc_reward(lit, ci.m_weight);
inc_make(lit);
}
m_unsat.insert_fresh(i);
break;
case 1:
dec_reward(to_literal(ci.m_trues), ci.m_weight);
break;
default:
break;
}
}
}
bool ddfw::should_restart() {
return m_flips >= m_restart_next;
}
void ddfw::do_restart() {
reinit_values();
init_clause_data();
m_restart_next += m_config.m_restart_base*get_luby(++m_restart_count);
}
/**
\brief the higher the bias, the lower the probability to deviate from the value of the bias
during a restart.
bias = 0 -> flip truth value with 50%
|bias| = 1 -> toss coin with 25% probability
|bias| = 2 -> toss coin with 12.5% probability
etc
*/
void ddfw::reinit_values() {
for (unsigned i = 0; i < num_vars(); ++i) {
int b = bias(i);
if (0 == (m_rand() % (1 + abs(b))))
value(i) = (m_rand() % 2) == 0;
else
value(i) = bias(i) > 0;
}
}
void ddfw::save_priorities() {
m_probs.reset();
for (unsigned v = 0; v < num_vars(); ++v)
m_probs.push_back(-m_vars[v].m_reward_avg);
}
void ddfw::save_model() {
m_model.reserve(num_vars());
for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i));
save_priorities();
if (m_plugin)
m_plugin->on_save_model();
}
void ddfw::save_best_values() {
if (m_unsat.size() < m_min_sz || m_unsat.empty()) {
m_steps_since_progress = 0;
if (m_unsat.size() < 50 || m_min_sz * 10 > m_unsat.size() * 11)
save_model();
}
if (m_unsat.size() < m_min_sz) {
m_models.reset();
// skip saving the first model.
for (unsigned v = 0; v < num_vars(); ++v) {
int& b = bias(v);
if (abs(b) > 3) {
b = b > 0 ? 3 : -3;
}
}
}
unsigned h = value_hash();
unsigned occs = 0;
bool contains = m_models.find(h, occs);
if (!contains) {
for (unsigned v = 0; v < num_vars(); ++v)
bias(v) += value(v) ? 1 : -1;
if (m_models.size() > m_config.m_max_num_models)
m_models.erase(m_models.begin()->m_key);
}
m_models.insert(h, occs + 1);
if (occs > 100) {
m_restart_next = m_flips;
m_models.erase(h);
}
m_min_sz = m_unsat.size();
}
unsigned ddfw::value_hash() const {
unsigned s0 = 0, s1 = 0;
for (auto const& vi : m_vars) {
s0 += vi.m_value;
s1 += s0;
}
return s1;
}
/**
\brief Filter on whether to select a satisfied clause
1. with some probability prefer higher weight to lesser weight.
2. take into account number of trues ?
3. select multiple clauses instead of just one per clause in unsat.
*/
bool ddfw::select_clause(double max_weight, clause_info const& cn, unsigned& n) {
if (cn.m_num_trues == 0 || cn.m_weight + 1e-5 < max_weight)
return false;
if (cn.m_weight > max_weight) {
n = 2;
return true;
}
return (m_rand() % (n++)) == 0;
}
unsigned ddfw::select_max_same_sign(unsigned cf_idx) {
auto& ci = m_clauses[cf_idx];
unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause.
auto const& c = ci.m_clause;
double max_weight = m_init_weight;
unsigned n = 1;
for (literal lit : c) {
for (unsigned cn_idx : use_list(lit)) {
auto& cn = m_clauses[cn_idx];
if (select_clause(max_weight, cn, n)) {
cl = cn_idx;
max_weight = cn.m_weight;
}
}
}
return cl;
}
void ddfw::transfer_weight(unsigned from, unsigned to, double w) {
auto& cf = m_clauses[to];
auto& cn = m_clauses[from];
if (cn.m_weight < w)
return;
cf.m_weight += w;
cn.m_weight -= w;
for (literal lit : get_clause(to))
inc_reward(lit, w);
if (cn.m_num_trues == 1)
inc_reward(to_literal(cn.m_trues), w);
}
unsigned ddfw::select_random_true_clause() {
unsigned num_clauses = m_clauses.size();
unsigned rounds = 100 * num_clauses;
for (unsigned i = 0; i < rounds; ++i) {
unsigned idx = (m_rand() * m_rand()) % num_clauses;
auto & cn = m_clauses[idx];
if (cn.is_true() && cn.m_weight >= m_init_weight)
return idx;
}
return UINT_MAX;
}
// 1% chance to disregard neighbor
inline bool ddfw::disregard_neighbor() {
return false; // rand() % 1000 == 0;
}
double ddfw::calculate_transfer_weight(double w) {
return (w > m_init_weight) ? m_init_weight : 1;
}
void ddfw::shift_weights() {
++m_shifts;
for (unsigned to_idx : m_unsat) {
SASSERT(!m_clauses[to_idx].is_true());
unsigned from_idx = select_max_same_sign(to_idx);
if (from_idx == UINT_MAX || disregard_neighbor())
from_idx = select_random_true_clause();
if (from_idx == UINT_MAX)
continue;
auto & cn = m_clauses[from_idx];
SASSERT(cn.is_true());
double w = calculate_transfer_weight(cn.m_weight);
transfer_weight(from_idx, to_idx, w);
}
// DEBUG_CODE(invariant(););
}
std::ostream& ddfw::display(std::ostream& out) const {
unsigned num_cls = m_clauses.size();
for (unsigned i = 0; i < num_cls; ++i) {
out << get_clause(i) << " nt: ";
auto const& ci = m_clauses[i];
out << ci.m_num_trues << " w: " << ci.m_weight << "\n";
}
for (unsigned v = 0; v < num_vars(); ++v)
out << (is_true(literal(v, false)) ? "" : "-") << v << " rw: " << get_reward(v) << "\n";
out << "unsat vars: ";
for (bool_var v : m_unsat_vars)
out << v << " ";
out << "\n";
return out;
}
void ddfw::invariant() {
// every variable in unsat vars is in a false clause.
for (bool_var v : m_unsat_vars) {
bool found = false;
for (unsigned cl : m_unsat) {
for (literal lit : get_clause(cl)) {
if (lit.var() == v) { found = true; break; }
}
if (found) break;
}
if (!found) IF_VERBOSE(0, verbose_stream() << "unsat var not found: " << v << "\n"; );
VERIFY(found);
}
for (unsigned v = 0; v < num_vars(); ++v) {
double v_reward = 0;
literal lit(v, !value(v));
for (unsigned j : m_use_list[lit.index()]) {
clause_info const& ci = m_clauses[j];
if (ci.m_num_trues == 1) {
SASSERT(lit == to_literal(ci.m_trues));
v_reward -= ci.m_weight;
}
}
for (unsigned j : m_use_list[(~lit).index()]) {
clause_info const& ci = m_clauses[j];
if (ci.m_num_trues == 0) {
v_reward += ci.m_weight;
}
}
IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
// SASSERT(reward(v) == v_reward);
}
DEBUG_CODE(
for (auto const& ci : m_clauses) {
SASSERT(ci.m_weight > 0);
}
for (unsigned i = 0; i < m_clauses.size(); ++i) {
bool found = false;
for (literal lit : get_clause(i)) {
if (is_true(lit)) found = true;
}
SASSERT(found == !m_unsat.contains(i));
}
// every variable in a false clause is in unsat vars
for (unsigned cl : m_unsat) {
for (literal lit : get_clause(cl)) {
SASSERT(m_unsat_vars.contains(lit.var()));
}
});
}
void ddfw::updt_params(params_ref const& _p) {
sat_params p(_p);
m_config.m_init_clause_weight = p.ddfw_init_clause_weight();
m_config.m_use_reward_zero_pct = p.ddfw_use_reward_pct();
m_config.m_reinit_base = p.ddfw_reinit_base();
m_config.m_restart_base = p.ddfw_restart_base();
}
}

278
src/ast/sls/sat_ddfw.h Normal file
View file

@ -0,0 +1,278 @@
/*++
Copyright (c) 2019 Microsoft Corporation
Module Name:
sat_ddfw.h
Abstract:
DDFW Local search module for clauses
Author:
Nikolaj Bjorner, Marijn Heule 2019-4-23
Notes:
http://www.ict.griffith.edu.au/~johnt/publications/CP2006raouf.pdf
--*/
#pragma once
#include "util/uint_set.h"
#include "util/rlimit.h"
#include "util/params.h"
#include "util/ema.h"
#include "util/sat_sls.h"
#include "util/map.h"
#include "util/sat_literal.h"
#include "util/statistics.h"
#include "util/stopwatch.h"
namespace sat {
class local_search_plugin {
public:
virtual ~local_search_plugin() {}
virtual void init_search() = 0;
virtual void finish_search() = 0;
virtual double reward(bool_var v) = 0;
virtual void on_rescale() = 0;
virtual void on_save_model() = 0;
virtual void on_restart() = 0;
};
class ddfw {
friend class ddfw_wrapper;
protected:
struct config {
config() { reset(); }
unsigned m_use_reward_zero_pct;
unsigned m_init_clause_weight;
unsigned m_max_num_models;
unsigned m_restart_base;
unsigned m_reinit_base;
unsigned m_parsync_base;
double m_itau;
void reset() {
m_init_clause_weight = 8;
m_use_reward_zero_pct = 15;
m_max_num_models = (1 << 10);
m_restart_base = 100333;
m_reinit_base = 10000;
m_parsync_base = 333333;
m_itau = 0.5;
}
};
struct var_info {
var_info() {}
bool m_internal = false;
bool m_value = false;
double m_reward = 0;
double m_last_reward = 0;
unsigned m_make_count = 0;
int m_bias = 0;
bool m_external = false;
ema m_reward_avg = 1e-5;
};
config m_config;
reslimit m_limit;
vector<clause_info> m_clauses;
literal_vector m_assumptions;
svector<var_info> m_vars; // var -> info
svector<double> m_probs; // var -> probability of flipping
svector<double> m_scores; // reward -> score
svector<lbool> m_model; // var -> best assignment
unsigned m_init_weight = 2;
vector<unsigned_vector> m_use_list;
unsigned_vector m_flat_use_list;
unsigned_vector m_use_list_index;
indexed_uint_set m_unsat;
indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses
random_gen m_rand;
unsigned m_num_non_binary_clauses = 0;
unsigned m_restart_count = 0, m_reinit_count = 0;
uint64_t m_restart_next = 0, m_reinit_next = 0;
uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0;
unsigned m_min_sz = 0, m_steps_since_progress = 0;
u_map<unsigned> m_models;
stopwatch m_stopwatch;
scoped_ptr<local_search_plugin> m_plugin = nullptr;
std::function<bool(void)> m_parallel_sync;
void flatten_use_list();
/**
* TBD: map reward value to a score, possibly through an exponential function, such as
* exp(-tau/r), where tau > 0
*/
inline double score(double r) { return r; }
inline unsigned& make_count(bool_var v) { return m_vars[v].m_make_count; }
inline bool& value(bool_var v) { return m_vars[v].m_value; }
inline bool value(bool_var v) const { return m_vars[v].m_value; }
inline double& reward(bool_var v) { return m_vars[v].m_reward; }
inline double plugin_reward(bool_var v) { return is_external(v) ? (m_vars[v].m_last_reward = m_plugin->reward(v)) : reward(v); }
void set_external(bool_var v) { m_vars[v].m_external = true; }
inline bool is_external(bool_var v) const { return m_vars[v].m_external; }
inline int& bias(bool_var v) { return m_vars[v].m_bias; }
unsigned value_hash() const;
inline bool is_true(literal lit) const { return value(lit.var()) != lit.sign(); }
inline sat::literal_vector const& get_clause(unsigned idx) const { return m_clauses[idx].m_clause; }
inline double get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); }
void update_reward_avg(bool_var v) { m_vars[v].m_reward_avg.update(reward(v)); }
unsigned select_max_same_sign(unsigned cf_idx);
inline void inc_make(literal lit) {
bool_var v = lit.var();
if (make_count(v)++ == 0) m_unsat_vars.insert_fresh(v);
}
inline void dec_make(literal lit) {
bool_var v = lit.var();
if (--make_count(v) == 0) m_unsat_vars.remove(v);
}
inline void inc_reward(literal lit, double w) { reward(lit.var()) += w; }
inline void dec_reward(literal lit, double w) { reward(lit.var()) -= w; }
void check_with_plugin();
void check_without_plugin();
// flip activity
template<bool uses_plugin>
bool do_flip();
template<bool uses_plugin>
bool_var pick_var(double& reward);
template<bool uses_plugin>
bool apply_flip(bool_var v, double reward);
void save_best_values();
void save_model();
void save_priorities();
// shift activity
void shift_weights();
inline double calculate_transfer_weight(double w);
// reinitialize weights activity
bool should_reinit_weights();
void do_reinit_weights();
inline bool select_clause(double max_weight, clause_info const& cn, unsigned& n);
// restart activity
bool should_restart();
void do_restart();
void reinit_values();
unsigned select_random_true_clause();
void log();
void init(unsigned sz, literal const* assumptions);
void init_clause_data();
void invariant();
void del();
void add_assumptions();
inline void transfer_weight(unsigned from, unsigned to, double w);
inline bool disregard_neighbor();
public:
ddfw() {}
~ddfw();
void set_plugin(local_search_plugin* p) { m_plugin = p; }
lbool check(unsigned sz, literal const* assumptions);
void updt_params(params_ref const& p);
svector<lbool> const& get_model() const { return m_model; }
reslimit& rlimit() { return m_limit; }
void set_seed(unsigned n) { m_rand.set_seed(n); }
bool get_value(bool_var v) const { return value(v); }
std::ostream& display(std::ostream& out) const;
// for parallel integration
unsigned num_non_binary_clauses() const { return m_num_non_binary_clauses; }
void collect_statistics(statistics& st) const {}
double get_priority(bool_var v) const { return m_probs[v]; }
// access clause information and state of Boolean search
indexed_uint_set& unsat_set() { return m_unsat; }
vector<clause_info> const& clauses() const { return m_clauses; }
clause_info& get_clause_info(unsigned idx) { return m_clauses[idx]; }
void remove_assumptions();
void flip(bool_var v);
inline double get_reward(bool_var v) const { return m_vars[v].m_reward; }
void add(unsigned sz, literal const* c);
sat::bool_var add_var(bool is_internal = true);
// is this a variable that was added during initialization?
bool is_initial_var(sat::bool_var v) const {
return m_vars.size() > v && !m_vars[v].m_internal;
}
void reinit();
inline unsigned num_vars() const { return m_vars.size(); }
std::initializer_list<unsigned> use_list(literal lit) {
unsigned i = lit.index();
auto const* b = m_flat_use_list.data() + m_use_list_index[i];
auto const* e = m_flat_use_list.data() + m_use_list_index[i + 1];
return std::initializer_list(b, e);
}
};
}

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

@ -324,6 +324,11 @@ namespace sls {
SASSERT(dtt(sign(bv), ineq) == 0);
}
vi.m_value = new_value;
if (vi.m_shared) {
sort* s = vi.m_sort == var_sort::INT ? a.mk_int() : a.mk_real();
expr_ref num = from_num(s, new_value);
ctx.set_value(vi.m_expr, num);
}
for (auto idx : vi.m_muls) {
auto const& [v, monomial] = m_muls[idx];
num_t prod(1);
@ -380,6 +385,20 @@ namespace sls {
return false;
}
expr_ref arith_base<rational>::from_num(sort* s, rational const& n) {
return expr_ref(a.mk_numeral(n, s), m);
}
expr_ref arith_base<checked_int64<true>>::from_num(sort* s, checked_int64<true> const& n) {
return expr_ref(a.mk_numeral(rational(n.get_int64(), rational::i64()), s), m);
}
template<typename num_t>
expr_ref arith_base<num_t>::from_num(sort* s, num_t const& n) {
return expr_ref(m);
}
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);
@ -444,15 +463,12 @@ namespace sls {
else if (a.is_to_int(e, x))
add_arg(term, coeff, mk_op(arith_op_kind::OP_TO_INT, e, x, x));
else if (a.is_to_real(e, x))
add_arg(term, coeff, mk_op(arith_op_kind::OP_TO_REAL, e, x, x));
else if (is_uninterp(e))
add_arg(term, coeff, mk_var(e));
add_arg(term, coeff, mk_op(arith_op_kind::OP_TO_REAL, e, x, x));
else if (a.is_arith_expr(e)) {
NOT_IMPLEMENTED_YET();
}
else {
NOT_IMPLEMENTED_YET();
}
else
add_arg(term, coeff, mk_var(e));
}
template<typename num_t>
@ -950,6 +966,29 @@ namespace sls {
void arith_base<num_t>::register_term(expr* e) {
}
template<typename num_t>
void arith_base<num_t>::set_shared(expr* e) {
if (!a.is_int_real(e))
return;
var_t v = m_expr2var.get(e->get_id(), UINT_MAX);
if (v == UINT_MAX)
v = mk_term(e);
m_vars[v].m_shared = true;
}
template<typename num_t>
void arith_base<num_t>::set_value(expr* e, expr* v) {
auto w = m_expr2var.get(e->get_id(), UINT_MAX);
if (w == UINT_MAX)
return;
num_t n;
if (!is_num(v, n))
return;
if (n == value(w))
return;
update(w, n);
}
template<typename num_t>
expr_ref arith_base<num_t>::get_value(expr* e) {
auto v = mk_var(e);

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

@ -90,6 +90,7 @@ namespace sls {
expr* m_expr;
num_t m_value{ 0 };
num_t m_best_value{ 0 };
bool m_shared = false;
var_sort m_sort;
arith_op_kind m_op = arith_op_kind::LAST_ARITH_OP;
unsigned m_def_idx = UINT_MAX;
@ -147,9 +148,7 @@ namespace sls {
double reward(sat::literal lit);
bool sign(sat::bool_var v) const { return !ctx.is_true(sat::literal(v, false)); }
ineq* atom(sat::bool_var bv) const { return m_bool_vars.get(bv, nullptr); }
ineq* atom(sat::bool_var bv) const { return m_bool_vars.get(bv, nullptr); }
num_t dtt(bool sign, ineq const& ineq) const { return dtt(sign, ineq.m_args_value, ineq); }
num_t dtt(bool sign, num_t const& args_value, ineq const& ineq) const;
num_t dtt(bool sign, ineq const& ineq, var_t v, num_t const& new_value) const;
@ -178,19 +177,19 @@ namespace sls {
num_t value(var_t v) const { return m_vars[v].m_value; }
bool is_num(expr* e, num_t& i);
expr_ref from_num(sort* s, num_t const& n);
void check_ineqs();
public:
arith_base(context& ctx);
~arith_base() override {}
void init_bool_var(sat::bool_var v) override;
void register_term(expr* e) override;
void set_shared(expr* e) override;
void set_value(expr* e, expr* v) override;
expr_ref get_value(expr* e) override;
lbool check() override;
bool is_sat() override;
void reset() override;
void on_rescale() override;
void on_restart() override;
std::ostream& display(std::ostream& out) const override;

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

@ -29,6 +29,8 @@ namespace sls {
}
catch (overflow_exception&) {
m_arith = alloc(arith_base<rational>, ctx);
for (auto e : m_shared)
m_arith->set_shared(e);
return; // initialization happens on check-sat calls
}
}
@ -44,6 +46,8 @@ namespace sls {
}
catch (overflow_exception&) {
m_arith = alloc(arith_base<rational>, ctx);
for (auto e : m_shared)
m_arith->set_shared(e);
}
}
m_arith->register_term(e);
@ -56,6 +60,8 @@ namespace sls {
}
catch (overflow_exception&) {
m_arith = alloc(arith_base<rational>, ctx);
for (auto e : m_shared)
m_arith->set_shared(e);
}
}
return m_arith->get_value(e);
@ -68,6 +74,8 @@ namespace sls {
}
catch (overflow_exception&) {
m_arith = alloc(arith_base<rational>, ctx);
for (auto e : m_shared)
m_arith->set_shared(e);
}
}
return m_arith->check();
@ -79,35 +87,54 @@ namespace sls {
return m_arith->is_sat();
}
void arith_plugin::reset() {
if (!m_arith)
m_arith64->reset();
else
if (m_arith)
m_arith->reset();
else
m_arith64->reset();
m_shared.reset();
}
void arith_plugin::on_rescale() {
if (!m_arith)
m_arith64->on_rescale();
else
if (m_arith)
m_arith->on_rescale();
}
void arith_plugin::on_restart() {
if (!m_arith)
m_arith64->on_restart();
else
m_arith->on_restart();
m_arith64->on_rescale();
}
void arith_plugin::on_restart() {
if (m_arith)
m_arith->on_restart();
else
m_arith64->on_restart();
}
std::ostream& arith_plugin::display(std::ostream& out) const {
if (!m_arith)
return m_arith64->display(out);
return m_arith->display(out);
if (m_arith)
return m_arith->display(out);
else
return m_arith64->display(out);
}
void arith_plugin::mk_model(model& mdl) {
if (!m_arith)
m_arith64->mk_model(mdl);
else
if (m_arith)
m_arith->mk_model(mdl);
else
m_arith64->mk_model(mdl);
}
void arith_plugin::set_shared(expr* e) {
if (m_arith)
m_arith->set_shared(e);
else {
m_arith64->set_shared(e);
m_shared.push_back(e);
}
}
void arith_plugin::set_value(expr* e, expr* v) {
if (m_arith)
m_arith->set_value(e, v);
else
m_arith->set_value(e, v);
}
}

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

@ -24,8 +24,12 @@ namespace sls {
class arith_plugin : public plugin {
scoped_ptr<arith_base<checked_int64<true>>> m_arith64;
scoped_ptr<arith_base<rational>> m_arith;
expr_ref_vector m_shared;
public:
arith_plugin(context& ctx) : plugin(ctx) { m_arith64 = alloc(arith_base<checked_int64<true>>,ctx); }
arith_plugin(context& ctx) :
plugin(ctx), m_shared(ctx.get_manager()) {
m_arith64 = alloc(arith_base<checked_int64<true>>,ctx);
}
~arith_plugin() override {}
void init_bool_var(sat::bool_var v) override;
void register_term(expr* e) override;
@ -38,6 +42,8 @@ namespace sls {
void on_restart() override;
std::ostream& display(std::ostream& out) const override;
void mk_model(model& mdl) override;
void set_shared(expr* e) override;
void set_value(expr* e, expr* v) override;
};
}

93
src/ast/sls/sls_bv.cpp Normal file
View file

@ -0,0 +1,93 @@
#include "ast/sls/sls_bv.h"
namespace sls {
bv_plugin::bv_plugin(context& ctx):
plugin(ctx),
bv(m),
m_terms(m),
m_eval(m)
{}
void bv_plugin::init_bool_var(sat::bool_var v) {
}
void bv_plugin::register_term(expr* e) {
}
expr_ref bv_plugin::get_value(expr* e) {
return expr_ref(m);
}
lbool bv_plugin::check() {
return l_undef;
}
bool bv_plugin::is_sat() {
return false;
}
void bv_plugin::reset() {
}
void bv_plugin::on_rescale() {
}
void bv_plugin::on_restart() {
}
std::ostream& bv_plugin::display(std::ostream& out) const {
return out;
}
void bv_plugin::mk_model(model& mdl) {
}
void bv_plugin::set_shared(expr* e) {
}
void bv_plugin::set_value(expr* e, expr* v) {
}
std::pair<bool, app*> bv_plugin::next_to_repair() {
app* e = nullptr;
if (m_repair_down != UINT_MAX) {
e = m_terms.term(m_repair_down);
m_repair_down = UINT_MAX;
return { true, e };
}
if (!m_repair_up.empty()) {
unsigned index = m_repair_up.elem_at(ctx.rand(m_repair_up.size()));
m_repair_up.remove(index);
e = m_terms.term(index);
return { false, e };
}
while (!m_repair_roots.empty()) {
unsigned index = m_repair_roots.elem_at(ctx.rand(m_repair_roots.size()));
e = m_terms.term(index);
if (m_terms.is_assertion(e) && !m_eval.bval1(e)) {
SASSERT(m_eval.bval0(e));
return { true, e };
}
if (!m_eval.re_eval_is_correct(e)) {
init_repair_goal(e);
return { true, e };
}
m_repair_roots.remove(index);
}
return { false, nullptr };
}
void bv_plugin::init_repair_goal(app* e) {
m_eval.init_eval(e);
}
}

55
src/ast/sls/sls_bv.h Normal file
View file

@ -0,0 +1,55 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sls_bv.h
Abstract:
Theory plugin for bit-vector local search
Author:
Nikolaj Bjorner (nbjorner) 2024-07-06
--*/
#pragma once
#include "ast/sls/sls_smt.h"
#include "ast/bv_decl_plugin.h"
#include "ast/sls/bv_sls_terms.h"
#include "ast/sls/bv_sls_eval.h"
namespace sls {
class bv_plugin : public plugin {
bv_util bv;
bv::sls_terms m_terms;
bv::sls_eval m_eval;
bv::sls_stats m_stats;
indexed_uint_set m_repair_up, m_repair_roots;
unsigned m_repair_down = UINT_MAX;
std::pair<bool, app*> next_to_repair();
void init_repair_goal(app* e);
public:
bv_plugin(context& ctx);
~bv_plugin() override {}
void init_bool_var(sat::bool_var v) override;
void register_term(expr* e) override;
expr_ref get_value(expr* e) override;
lbool check() override;
bool is_sat() override;
void reset() override;
void on_rescale() override;
void on_restart() override;
std::ostream& display(std::ostream& out) const override;
void mk_model(model& mdl) override;
void set_shared(expr* e) override;
void set_value(expr* e, expr* v) override;
};
}

2
src/ast/sls/sls_cc.h
View file

@ -46,6 +46,8 @@ namespace sls {
void init_bool_var(sat::bool_var v) override {}
std::ostream& display(std::ostream& out) const override;
void mk_model(model& mdl) override;
void set_value(expr* e, expr* v) override {}
void set_shared(expr* e) override {}
};
}

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

@ -101,7 +101,9 @@ namespace sls {
}
void context::set_value(expr* e, expr* v) {
NOT_IMPLEMENTED_YET();
for (auto p : m_plugins)
if (p)
p->set_value(e, v);
}
bool context::is_relevant(expr* e) {

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

@ -46,6 +46,8 @@ namespace sls {
virtual void on_restart() {};
virtual std::ostream& display(std::ostream& out) const = 0;
virtual void mk_model(model& mdl) = 0;
virtual void set_shared(expr* e) = 0;
virtual void set_value(expr* e, expr* v) = 0;
};
using clause = std::initializer_list <sat::literal>;
@ -110,6 +112,7 @@ namespace sls {
double reward(sat::bool_var v) { return s.reward(v); }
indexed_uint_set const& unsat() const { return s.unsat(); }
unsigned rand() { return m_rand(); }
unsigned rand(unsigned n) { return m_rand(n); }
sat::literal_vector const& root_literals() const { return m_root_literals; }
void reinit_relevant();