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

enable concurrent sls with new solver core

Browse source 
allow using sls engine (for bit-vectors) with the new core.

Examples

z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=0 /st C:\QF_BV_SAT\bench_10.smt2
z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st C:\QF_BV_SAT\bench_10.smt2
z3 C:\QF_BV_SAT\bench_11100.smt2 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st
This commit is contained in:
Nikolaj Bjorner 2024-04-11 10:49:30 +02:00
parent 510534dbd4
commit c0bdc7cdd6
19 changed files with 206 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/sls/bv_sls.cpp
View file

@ -93,6 +93,18 @@ namespace bv {
if (m_to_repair.empty())
return;
// add fresh units, if any
bool new_assertion = false;
while (m_get_unit) {
auto e = m_get_unit();
if (!e)
break;
new_assertion = true;
assert_expr(e);
}
if (new_assertion)
init();
std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned i) {
unsigned id = e->get_id();
@ -212,9 +224,7 @@ namespace bv {
void sls::try_repair_down(app* e) {
unsigned n = e->get_num_args();
if (n == 0) {
m_eval.commit_eval(e);
IF_VERBOSE(3, verbose_stream() << "done\n");
m_eval.commit_eval(e);
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());

7
src/ast/sls/bv_sls.h
View file

@ -53,6 +53,7 @@ namespace bv {
sls_engine m_engine;
bool m_engine_model = false;
bool m_engine_init = false;
std::function<expr_ref()> m_get_unit;
std::pair<bool, app*> next_to_repair();
@ -81,7 +82,6 @@ namespace bv {
/*
* Invoke init after all expressions are asserted.
* No other expressions can be asserted after init.
*/
void init();
@ -91,6 +91,11 @@ namespace bv {
*/
void init_eval(std::function<bool(expr*, unsigned)>& eval);
/**
* add callback to retrieve new units
*/
void init_unit(std::function<expr_ref()> get_unit) { m_get_unit = get_unit; }
/**
* Run (bounded) local search to find feasible assignments.
*/

16
src/ast/sls/bv_sls_fixed.cpp
View file

@ -58,16 +58,16 @@ namespace bv {
expr* t, * s;
rational v;
if (bv.is_concat(e, t, s)) {
auto& val = wval(s);
if (val.lo() != val.hi() && (val.lo() < val.hi() || val.hi() == 0))
auto& vals = wval(s);
if (vals.lo() != vals.hi() && (vals.lo() < vals.hi() || vals.hi() == 0))
// lo <= e
add_range(e, val.lo(), rational::zero(), false);
add_range(e, vals.lo(), rational::zero(), false);
auto valt = wval(t);
#if 0
if (val.lo() < val.hi())
// e < (2^|s|) * hi
add_range(e, rational::zero(), val.hi() * rational::power_of_two(bv.get_bv_size(s)), false);
#endif
if (valt.lo() != valt.hi() && (valt.lo() < valt.hi() || valt.hi() == 0)) {
// (2^|s|) * lo <= e < (2^|s|) * hi
auto p = rational::power_of_two(bv.get_bv_size(s));
add_range(e, valt.lo() * p, valt.hi() * p, false);
}
}
else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) {
auto& val = wval(t);

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

@ -206,6 +206,7 @@ namespace bv {
m_todo.push_back(arg);
}
// populate parents
m_parents.reset();
m_parents.reserve(m_terms.size());
for (expr* e : m_terms) {
if (!e || !is_app(e))
@ -213,6 +214,7 @@ namespace bv {
for (expr* arg : *to_app(e))
m_parents[arg->get_id()].push_back(e);
}
m_assertion_set.reset();
for (auto a : m_assertions)
m_assertion_set.insert(a->get_id());
}

9
src/ast/sls/sls_valuation.cpp
View file

@ -245,6 +245,7 @@ namespace bv {
}
bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
m_tmp.set_bw(bw);
if (!get_at_most(src, m_tmp))
return false;
@ -639,6 +640,14 @@ namespace bv {
if (has_range() && !in_range(m_bits))
m_bits = m_lo;
if (mod(lo() + 1, rational::power_of_two(bw)) == hi())
for (unsigned i = 0; i < nw; ++i)
fixed[i] = ~0;
if (lo() < hi() && hi() < rational::power_of_two(bw - 1))
for (unsigned i = 0; i < bw; ++i)
if (hi() < rational::power_of_two(i))
fixed.set(i, true);
SASSERT(well_formed());
}

3
src/sat/sat_solver.cpp
View file

@ -1314,7 +1314,7 @@ namespace sat {
}
bool solver::should_cancel() {
if (limit_reached() || memory_exceeded()) {
if (limit_reached() || memory_exceeded() || m_solver_canceled) {
return true;
}
if (m_config.m_restart_max <= m_restarts) {
@ -1959,6 +1959,7 @@ namespace sat {
void solver::init_search() {
m_model_is_current = false;
m_solver_canceled = false;
m_phase_counter = 0;
m_search_state = s_unsat;
m_search_unsat_conflicts = m_config.m_search_unsat_conflicts;

2
src/sat/sat_solver.h
View file

@ -177,6 +177,7 @@ namespace sat {
clause_wrapper_vector m_clauses_to_reinit;
std::string m_reason_unknown;
bool m_trim = false;
bool m_solver_canceled = false;
visit_helper m_visited;
@ -287,6 +288,7 @@ namespace sat {
random_gen& rand() { return m_rand; }
void set_trim() { m_trim = true; }
void set_canceled() { m_solver_canceled = true; }
protected:
void reset_var(bool_var v, bool ext, bool dvar);

14
src/sat/sat_solver/sat_smt_solver.cpp
View file

@ -197,10 +197,16 @@ public:
case l_false:
extract_core();
break;
default:
default: {
auto* ext = get_euf();
if (ext && ext->get_sls_model()) {
r = l_true;
break;
}
set_reason_unknown(m_solver.get_reason_unknown());
break;
}
}
return r;
}
@ -576,6 +582,7 @@ private:
void add_assumption(expr* a) {
init_goal2sat();
m_dep.insert(a, m_goal2sat.internalize(a));
get_euf()->add_assertion(a);
}
void internalize_assumptions(expr_ref_vector const& asms) {
@ -632,6 +639,11 @@ private:
void get_model_core(model_ref & mdl) override {
TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";);
mdl = nullptr;
auto ext = get_euf();
if (ext)
mdl = ext->get_sls_model();
if (mdl)
return;
if (!m_solver.model_is_current())
return;
if (m_fmls.size() > m_qhead)

4
src/sat/smt/euf_internalize.cpp
View file

@ -525,4 +525,8 @@ namespace euf {
return n;
}
void solver::add_assertion(expr* f) {
m_assertions.push_back(f);
m_trail.push(push_back_vector(m_assertions));
}
}

9
src/sat/smt/euf_model.cpp
View file

@ -18,6 +18,7 @@ Author:
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/sls_solver.h"
#include "model/value_factory.h"
namespace euf {
@ -67,6 +68,14 @@ namespace euf {
m_qmodel = mdl;
}
model_ref solver::get_sls_model() {
model_ref mdl;
auto s = get_solver(m.mk_family_id("sls"), nullptr);
if (s)
mdl = dynamic_cast<sls::solver*>(s)->get_model();
return mdl;
}
void solver::update_model(model_ref& mdl, bool validate) {
TRACE("model", tout << "create model\n";);
if (m_qmodel) {

13
src/sat/smt/euf_solver.cpp
View file

@ -28,6 +28,7 @@ Author:
#include "sat/smt/q_solver.h"
#include "sat/smt/fpa_solver.h"
#include "sat/smt/dt_solver.h"
#include "sat/smt/sls_solver.h"
#include "sat/smt/recfun_solver.h"
#include "sat/smt/specrel_solver.h"
@ -54,6 +55,7 @@ namespace euf {
m_smt_proof_checker(m, p),
m_clause(m),
m_expr_args(m),
m_assertions(m),
m_values(m)
{
updt_params(p);
@ -77,6 +79,7 @@ namespace euf {
};
m_egraph.set_on_merge(on_merge);
}
}
void solver::updt_params(params_ref const& p) {
@ -185,7 +188,9 @@ namespace euf {
IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
}
void solver::init_search() {
void solver::init_search() {
if (get_config().m_sls_enable)
add_solver(alloc(sls::solver, *this));
TRACE("before_search", s().display(tout););
m_reason_unknown.clear();
for (auto* s : m_solvers)
@ -217,7 +222,7 @@ namespace euf {
mark_relevant(lit);
s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx));
}
lbool solver::resolve_conflict() {
for (auto* s : m_solvers) {
lbool r = s->resolve_conflict();
@ -664,7 +669,9 @@ namespace euf {
if (give_up)
return sat::check_result::CR_GIVEUP;
if (m_qsolver && m_config.m_arith_ignore_int)
return sat::check_result::CR_GIVEUP;
return sat::check_result::CR_GIVEUP;
for (auto s : m_solvers)
s->finalize();
return sat::check_result::CR_DONE;
}

6
src/sat/smt/euf_solver.h
View file

@ -154,6 +154,7 @@ namespace euf {
svector<scope> m_scopes;
scoped_ptr_vector<th_solver> m_solvers;
ptr_vector<th_solver> m_id2solver;
constraint* m_conflict = nullptr;
constraint* m_eq = nullptr;
@ -173,6 +174,7 @@ namespace euf {
symbol m_smt = symbol("smt");
expr_ref_vector m_clause;
expr_ref_vector m_expr_args;
expr_ref_vector m_assertions;
// internalization
@ -482,6 +484,10 @@ namespace euf {
bool enable_ackerman_axioms(expr* n) const;
bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain);
void add_assertion(expr* f);
expr_ref_vector const& get_assertions() { return m_assertions; }
model_ref get_sls_model();
// relevancy
bool relevancy_enabled() const { return m_relevancy.enabled(); }

3
src/sat/smt/sat_th.h
View file

@ -148,6 +148,8 @@ namespace euf {
virtual void set_bounds(enode* n) {}
virtual void finalize() {}
};
class th_proof_hint : public sat::proof_hint {
@ -225,6 +227,7 @@ namespace euf {
void push() override { m_num_scopes++; }
void pop(unsigned n) override;
unsigned random();
};

151
src/sat/smt/sls_solver.cpp
View file

@ -23,38 +23,79 @@ Author:
namespace sls {
solver::solver(euf::solver& ctx):
th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {}
th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")),
m_units(m) {}
solver::~solver() {
if (m_bvsls) {
m_bvsls->cancel();
finalize();
}
void solver::finalize() {
if (!m_completed && m_bvsls) {
m_bvsls->cancel();
m_thread.join();
m_bvsls->collect_statistics(m_st);
m_bvsls = nullptr;
}
}
void solver::push_core() {
if (s().scope_lvl() == s().search_lvl() + 1)
init_local_search();
}
void solver::pop_core(unsigned n) {
if (s().scope_lvl() - n <= s().search_lvl())
sample_local_search();
sat::check_result solver::check() {
return sat::check_result::CR_DONE;
}
void solver::simplify() {
void solver::simplify() {
}
bool solver::unit_propagate() {
force_push();
sample_local_search();
return false;
}
bool solver::is_unit(expr* e) {
if (!e)
return false;
m.is_not(e, e);
if (is_uninterp_const(e))
return true;
bv_util bu(m);
expr* s;
if (bu.is_bit2bool(e, s))
return is_uninterp_const(s);
return false;
}
void solver::push_core() {
}
void solver::pop_core(unsigned n) {
for (; m_trail_lim < s().init_trail_size(); ++m_trail_lim) {
auto lit = s().trail_literal(m_trail_lim);
auto e = ctx.literal2expr(lit);
if (is_unit(e)) {
// IF_VERBOSE(1, verbose_stream() << "add unit " << mk_pp(e, m) << "\n");
std::lock_guard<std::mutex> lock(m_mutex);
m_units.push_back(e);
m_has_units = true;
}
}
}
void solver::init_search() {
init_local_search();
}
void solver::init_local_search() {
if (m_bvsls) {
m_bvsls->cancel();
m_thread.join();
if (m_result == l_true) {
verbose_stream() << "Found model using local search - INIT\n";
exit(1);
}
m_result = l_undef;
m_completed = false;
m_has_units = false;
m_model = nullptr;
m_units.reset();
}
// set up state for local search solver here
@ -64,43 +105,12 @@ namespace sls {
params_ref p;
m_completed = false;
m_result = l_undef;
m_model = nullptr;
m_bvsls = alloc(bv::sls, *m_m, p);
// walk clauses, add them
// walk trail stack until search level, add units
// encapsulate bvsls within the arguments of run-local-search.
// ensure bvsls does not touch ast-manager.
for (expr* a : ctx.get_assertions())
m_bvsls->assert_expr(tr(a));
unsigned trail_sz = s().trail_size();
for (unsigned i = 0; i < trail_sz; ++i) {
auto lit = s().trail_literal(i);
if (s().lvl(lit) > s().search_lvl())
break;
expr_ref fml = literal2expr(lit);
m_bvsls->assert_expr(tr(fml.get()));
}
unsigned num_vars = s().num_vars();
for (unsigned i = 0; i < 2*num_vars; ++i) {
auto l1 = ~sat::to_literal(i);
auto const& wlist = s().get_wlist(l1);
for (sat::watched const& w : wlist) {
if (!w.is_binary_non_learned_clause())
continue;
sat::literal l2 = w.get_literal();
if (l1.index() > l2.index())
continue;
expr_ref fml(m.mk_or(literal2expr(l1), literal2expr(l2)), m);
m_bvsls->assert_expr(tr(fml.get()));
}
}
for (auto clause : s().clauses()) {
expr_ref_vector cls(m);
for (auto lit : *clause)
cls.push_back(literal2expr(lit));
expr_ref fml(m.mk_or(cls), m);
m_bvsls->assert_expr(tr(fml.get()));
}
// use phase assignment from literals?
std::function<bool(expr*, unsigned)> eval = [&](expr* e, unsigned r) {
return false;
};
@ -108,23 +118,42 @@ namespace sls {
m_bvsls->init();
m_bvsls->init_eval(eval);
m_bvsls->updt_params(s().params());
m_bvsls->init_unit([&]() {
if (!m_has_units)
return expr_ref(*m_m);
expr_ref e(m);
{
std::lock_guard<std::mutex> lock(m_mutex);
if (m_units.empty())
return expr_ref(*m_m);
e = m_units.back();
m_units.pop_back();
}
ast_translation tr(m, *m_m);
return expr_ref(tr(e.get()), *m_m);
});
m_thread = std::thread([this]() { run_local_search(); });
}
void solver::sample_local_search() {
if (m_completed) {
m_thread.join();
if (m_result == l_true) {
verbose_stream() << "Found model using local search\n";
exit(1);
}
if (!m_completed)
return;
m_thread.join();
m_completed = false;
m_bvsls->collect_statistics(m_st);
if (m_result == l_true) {
IF_VERBOSE(2, verbose_stream() << "(sat.sls :model-completed)\n";);
auto mdl = m_bvsls->get_model();
ast_translation tr(*m_m, m);
m_model = mdl->translate(tr);
s().set_canceled();
}
m_bvsls = nullptr;
}
void solver::run_local_search() {
lbool r = (*m_bvsls)();
m_result = r;
m_result = (*m_bvsls)();
m_completed = true;
}

23
src/sat/smt/sls_solver.h
View file

@ -30,30 +30,43 @@ namespace sls {
class solver : public euf::th_euf_solver {
std::atomic<lbool> m_result;
std::atomic<bool> m_completed;
std::atomic<bool> m_completed, m_has_units;
std::thread m_thread;
std::mutex m_mutex;
scoped_ptr<ast_manager> m_m;
scoped_ptr<bv::sls> m_bvsls;
model_ref m_model;
unsigned m_trail_lim = 0;
expr_ref_vector m_units;
statistics m_st;
void run_local_search();
void init_local_search();
void sample_local_search();
bool is_unit(expr*);
public:
solver(euf::solver& ctx);
~solver();
void simplify() override;
void init_search() override;
void push_core() override;
void pop_core(unsigned n) override;
void simplify() override;
sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; }
void internalize(expr* e) override { UNREACHABLE(); }
th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
void collect_statistics(statistics& st) const override { st.copy(m_st); }
bool unit_propagate() override { return false; }
model_ref get_model() { return m_model; }
void finalize() override;
bool unit_propagate() override;
void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); }
sat::check_result check() override { return sat::check_result::CR_DONE; }
sat::check_result check() override;
std::ostream & display(std::ostream & out) const override { return out; }
std::ostream & display_justification(std::ostream & out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; }
std::ostream & display_constraint(std::ostream & out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; }

7
src/sat/tactic/goal2sat.cpp
View file

@ -895,6 +895,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
process(n, true);
CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";);
SASSERT(m_result_stack.empty());
add_assertion(n);
}
void insert_dep(expr* dep0, expr* dep, bool sign) {
@ -989,6 +990,12 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
}
void add_assertion(expr* f) {
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
if (ext)
ext->add_assertion(f);
}
void update_model(model_ref& mdl) {
auto* ext = dynamic_cast<euf::solver*>(m_solver.get_extension());
if (ext)

2
src/smt/params/smt_params.cpp
View file

@ -49,6 +49,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_threads_max_conflicts = p.threads_max_conflicts();
m_threads_cube_frequency = p.threads_cube_frequency();
m_core_validate = p.core_validate();
m_sls_enable = p.sls_enable();
m_logic = _p.get_sym("logic", m_logic);
m_string_solver = p.string_solver();
m_up_persist_clauses = p.up_persist_clauses();
@ -66,6 +67,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_lemmas2console = sp.lemmas2console();
m_instantiations2console = sp.instantiations2console();
m_proof_log = sp.proof_log();
}
void smt_params::updt_params(params_ref const & p) {

1
src/smt/params/smt_params.h
View file

@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params,
bool m_induction = false;
bool m_clause_proof = false;
symbol m_proof_log;
bool m_sls_enable = false;
// -----------------------------------
//

1
src/smt/params/smt_params_helper.pyg
View file

@ -135,6 +135,7 @@ def_module_params(module_name='smt',
('str.regex_automata_length_attempt_threshold', UINT, 10, 'number of length/path constraint attempts before checking unsatisfiability of regex terms'),
('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'),
('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'),
('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),