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

add support for core extraction in parallel mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-12 07:49:11 +02:00
parent 618d394ab5
commit 9e2625e629
1 changed files with 42 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/solver/parallel_tactic.cpp
View file

@ -183,6 +183,7 @@ class parallel_tactic : public tactic {
scoped_ptr<ast_manager> m_manager; // ownership handle to ast_manager scoped_ptr<ast_manager> m_manager; // ownership handle to ast_manager
vector<cube_var> m_cubes; // set of cubes to process by task vector<cube_var> m_cubes; // set of cubes to process by task
expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver
expr_ref_vector m_assumptions; // set of auxiliary assumptions passed in
params_ref m_params; // configuration parameters params_ref m_params; // configuration parameters
ref<solver> m_solver; // solver state ref<solver> m_solver; // solver state
unsigned m_depth; // number of nested calls to cubing unsigned m_depth; // number of nested calls to cubing
@ -192,6 +193,7 @@ class parallel_tactic : public tactic {
solver_state(ast_manager* m, solver* s, params_ref const& p): solver_state(ast_manager* m, solver* s, params_ref const& p):
m_manager(m), m_manager(m),
m_asserted_cubes(s->get_manager()), m_asserted_cubes(s->get_manager()),
m_assumptions(s->get_manager()),
m_params(p), m_params(p),
m_solver(s), m_solver(s),
m_depth(0), m_depth(0),
@ -207,6 +209,12 @@ class parallel_tactic : public tactic {
solver const& get_solver() const { return *m_solver; } solver const& get_solver() const { return *m_solver; }
void set_assumptions(ptr_vector<expr> const& asms) {
m_assumptions.append(asms.size(), asms.c_ptr());
}
bool has_assumptions() const { return !m_assumptions.empty(); }
solver_state* clone() { solver_state* clone() {
SASSERT(!m_cubes.empty()); SASSERT(!m_cubes.empty());
ast_manager& m = m_solver->get_manager(); ast_manager& m = m_solver->get_manager();
@ -216,6 +224,7 @@ class parallel_tactic : public tactic {
solver_state* st = alloc(solver_state, new_m, s, m_params); solver_state* st = alloc(solver_state, new_m, s, m_params);
for (auto& c : m_cubes) st->m_cubes.push_back(c(tr)); for (auto& c : m_cubes) st->m_cubes.push_back(c(tr));
for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c)); for (expr* c : m_asserted_cubes) st->m_asserted_cubes.push_back(tr(c));
for (expr* c : m_assumptions) st->m_assumptions.push_back(tr(c));
st->m_depth = m_depth; st->m_depth = m_depth;
st->m_width = m_width; st->m_width = m_width;
return st; return st;
@ -250,11 +259,11 @@ class parallel_tactic : public tactic {
lbool r = l_undef; lbool r = l_undef;
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";); IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
set_simplify_params(true); // retain blocked set_simplify_params(true); // retain blocked
r = get_solver().check_sat(0,0); r = get_solver().check_sat(m_assumptions);
if (r != l_undef) return r; if (r != l_undef) return r;
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";); IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
set_simplify_params(false); // remove blocked set_simplify_params(false); // remove blocked
r = get_solver().check_sat(0,0); r = get_solver().check_sat(m_assumptions);
return r; return r;
} }
@ -314,6 +323,7 @@ private:
ast_manager& m_manager; ast_manager& m_manager;
params_ref m_params; params_ref m_params;
sref_vector<model> m_models; sref_vector<model> m_models;
expr_ref_vector m_core;
unsigned m_num_threads; unsigned m_num_threads;
statistics m_stats; statistics m_stats;
task_queue m_queue; task_queue m_queue;
@ -340,6 +350,7 @@ private:
m_conquer_delay = pp.conquer_delay(); m_conquer_delay = pp.conquer_delay();
m_exn_code = 0; m_exn_code = 0;
m_params.set_bool("override_incremental", true); m_params.set_bool("override_incremental", true);
m_core.reset();
} }
void log_branches(lbool status) { void log_branches(lbool status) {
@ -363,6 +374,15 @@ private:
--m_branches; --m_branches;
} }
void collect_core(expr_ref_vector const& core) {
std::lock_guard<std::mutex> lock(m_mutex);
ast_translation tr(core.get_manager(), m_manager);
expr_ref_vector core1(tr(core));
for (expr* c : core1) {
if (!m_core.contains(c)) m_core.push_back(c);
}
}
void close_branch(solver_state& s, lbool status) { void close_branch(solver_state& s, lbool status) {
double f = 100.0 / s.get_width(); double f = 100.0 / s.get_width();
{ {
@ -398,6 +418,11 @@ private:
void report_unsat(solver_state& s) { void report_unsat(solver_state& s) {
inc_unsat(); inc_unsat();
close_branch(s, l_false); close_branch(s, l_false);
if (s.has_assumptions()) {
expr_ref_vector core(s.m());
s.get_solver().get_unsat_core(core);
collect_core(core);
}
} }
void report_undef(solver_state& s) { void report_undef(solver_state& s) {
@ -454,7 +479,7 @@ private:
break; break;
} }
lbool is_sat = l_undef; lbool is_sat = l_undef;
if (width >= m_conquer_delay && !conquer) { if (!s.has_assumptions() && width >= m_conquer_delay && !conquer) {
conquer = s.copy_solver(); conquer = s.copy_solver();
s.set_conquer_params(*conquer.get()); s.set_conquer_params(*conquer.get());
} }
@ -647,37 +672,43 @@ public:
parallel_tactic(solver* s, params_ref const& p) : parallel_tactic(solver* s, params_ref const& p) :
m_solver(s), m_solver(s),
m_manager(s->get_manager()), m_manager(s->get_manager()),
m_params(p) { m_params(p),
m_core(m_manager) {
init(); init();
} }
void operator ()(const goal_ref & g,goal_ref_buffer & result) { void operator ()(const goal_ref & g,goal_ref_buffer & result) {
fail_if_proof_generation("parallel-tactic", g);
ast_manager& m = g->m(); ast_manager& m = g->m();
solver* s = m_solver->translate(m, m_params); solver* s = m_solver->translate(m, m_params);
solver_state* st = alloc(solver_state, 0, s, m_params); solver_state* st = alloc(solver_state, 0, s, m_params);
m_queue.add_task(st); m_queue.add_task(st);
expr_ref_vector clauses(m); expr_ref_vector clauses(m);o
ptr_vector<expr> assumptions; ptr_vector<expr> assumptions;
obj_map<expr, expr*> bool2dep; obj_map<expr, expr*> bool2dep;
ref<generic_model_converter> fmc; ref<generic_model_converter> fmc;
expr_dependency * lcore = nullptr;
proof* pr = nullptr;
extract_clauses_and_dependencies(g, clauses, assumptions, bool2dep, fmc); extract_clauses_and_dependencies(g, clauses, assumptions, bool2dep, fmc);
for (expr * clause : clauses) { for (expr * clause : clauses) {
s->assert_expr(clause); s->assert_expr(clause);
} }
SASSERT(assumptions.empty()); st->set_assumptions(assumptions);
model_ref mdl; model_ref mdl;
lbool is_sat = solve(mdl); lbool is_sat = solve(mdl);
switch (is_sat) { switch (is_sat) {
case l_true: case l_true:
g->reset();
if (g->models_enabled()) { if (g->models_enabled()) {
g->add(concat(fmc.get(), model2model_converter(mdl.get()))); g->add(concat(fmc.get(), model2model_converter(mdl.get())));
} }
g->reset();
break; break;
case l_false: case l_false:
SASSERT(!g->proofs_enabled()); SASSERT(!g->proofs_enabled());
SASSERT(!g->unsat_core_enabled()); for (expr * c : m_core) {
g->assert_expr(m.mk_false(), nullptr, nullptr); lcore = m.mk_join(lcore, m.mk_leaf(bool2dep.find(c)));
}
g->assert_expr(m.mk_false(), pr, lcore);
break; break;
case l_undef: case l_undef:
if (m.canceled()) { if (m.canceled()) {