mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

work on parallel-tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-04 15:56:05 -05:00
parent 59ea11b1a3
commit e46e9cf86d
1 changed files with 59 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

112
src/tactic/portfolio/parallel_tactic.cpp
View file

@ -142,15 +142,16 @@ class parallel_tactic : public tactic {
}; };
class solver_state { class solver_state {
task_type m_type; task_type m_type; // current work role of the task
expr_ref_vector m_cubes, m_asserted_cubes; expr_ref_vector m_cubes; // set of cubes to process by task
params_ref m_params; expr_ref_vector m_asserted_cubes; // set of cubes asserted on the current solver
scoped_ptr<ast_manager> m_manager; params_ref m_params; // configuration parameters
ref<solver> m_solver; scoped_ptr<ast_manager> m_manager; // ownership handle to ast_manager
unsigned m_depth; ref<solver> m_solver; // solver state
unsigned m_width; unsigned m_depth; // number of nested calls to cubing
unsigned m_cube_cutoff; unsigned m_width; // estimate of fraction of problem handled by state
double m_cube_fraction; unsigned m_cube_cutoff; // saved configuration value
double m_cube_fraction; // saved configuration value
expr_ref_vector cube_literals(expr* cube) { expr_ref_vector cube_literals(expr* cube) {
expr_ref_vector literals(m()); expr_ref_vector literals(m());
@ -184,10 +185,6 @@ class parallel_tactic : public tactic {
solver const& get_solver() const { return *m_solver; } solver const& get_solver() const { return *m_solver; }
params_ref const& params() const { return m_params; }
params_ref& params() { return m_params; }
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();
@ -238,8 +235,13 @@ class parallel_tactic : public tactic {
if (r != l_undef) return r; if (r != l_undef) return r;
// copy over the resulting clauses with a configuration that blasts PB constraints // copy over the resulting clauses with a configuration that blasts PB constraints
set_simplify_params(false, true); set_simplify_params(false, true);
m_solver = get_solver().translate(m(), m_params); expr_ref_vector fmls(m());
get_solver().get_assertions(fmls);
model_converter_ref mc = get_solver().get_model_converter();
m_solver = mk_fd_solver(m(), m_params);
m_solver->set_model_converter(mc.get());
m_solver->assert_expr(fmls);
} }
set_simplify_params(false, true); // remove PB, retain blocked (TBD, sat solver does not blast PB constraints on its own) set_simplify_params(false, true); // remove PB, retain blocked (TBD, sat solver does not blast PB constraints on its own)
r = get_solver().check_sat(0,0); r = get_solver().check_sat(0,0);
@ -271,11 +273,13 @@ class parallel_tactic : public tactic {
} }
m_params.set_uint ("sat.lookahead.cube.cutoff", depth); m_params.set_uint ("sat.lookahead.cube.cutoff", depth);
m_params.set_double("sat.lookahead.cube.fraction", fraction); m_params.set_double("sat.lookahead.cube.fraction", fraction);
get_solver().updt_params(m_params);
} }
void set_conquer_params() { void set_conquer_params() {
m_params.set_bool("sat.lookahead_simplify", false); m_params.set_bool("sat.lookahead_simplify", false);
m_params.set_uint("sat.restart.max", 10); m_params.set_uint("sat.restart.max", 10);
get_solver().updt_params(m_params);
} }
void set_simplify_params(bool pb_simp, bool retain_blocked) { void set_simplify_params(bool pb_simp, bool retain_blocked) {
@ -288,6 +292,7 @@ class parallel_tactic : public tactic {
m_params.set_sym ("sat.pb.solver", pb_simp ? symbol("solver") : symbol("circuit")); m_params.set_sym ("sat.pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
m_params.set_uint("sat.restart.max", UINT_MAX); m_params.set_uint("sat.restart.max", UINT_MAX);
m_params.set_bool("sat.retain_blocked_clauses", retain_blocked); m_params.set_bool("sat.retain_blocked_clauses", retain_blocked);
get_solver().updt_params(m_params);
} }
bool canceled() { bool canceled() {
@ -296,7 +301,7 @@ class parallel_tactic : public tactic {
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
out << ":depth " << m_depth << " :width " << m_width << "\n"; out << ":depth " << m_depth << " :width " << m_width << "\n";
out << ":asserted cubes " << m_asserted_cubes << "\n"; out << ":asserted " << m_asserted_cubes.size() << "\n";
return out; return out;
} }
}; };
@ -313,12 +318,14 @@ private:
double m_progress; double m_progress;
bool m_has_undef; bool m_has_undef;
bool m_allsat; bool m_allsat;
unsigned m_num_unsat;
void init() { void init() {
m_num_threads = 2 * omp_get_num_procs(); // TBD adjust by possible threads used inside each solver. m_num_threads = 2 * omp_get_num_procs(); // TBD adjust by possible threads used inside each solver.
m_progress = 0; m_progress = 0;
m_has_undef = false; m_has_undef = false;
m_allsat = false; m_allsat = false;
m_num_unsat = 0;
} }
void close_branch(solver_state& s, lbool status) { void close_branch(solver_state& s, lbool status) {
@ -329,7 +336,6 @@ private:
IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << " " << st << ")\n";); IF_VERBOSE(1, verbose_stream() << "(tactic.parallel :progress " << m_progress << " " << st << ")\n";);
} }
void report_sat(solver_state& s) { void report_sat(solver_state& s) {
close_branch(s, l_true); close_branch(s, l_true);
model_ref mdl; model_ref mdl;
@ -347,8 +353,10 @@ private:
} }
} }
void report_unsat(solver_state& s) { void report_unsat(solver_state& s) {
close_branch(s, l_false); close_branch(s, l_false);
std::lock_guard<std::mutex> lock(m_mutex);
++m_num_unsat;
} }
void report_undef(solver_state& s) { void report_undef(solver_state& s) {
@ -357,7 +365,7 @@ private:
} }
void cube_and_conquer(solver_state& s) { void cube_and_conquer(solver_state& s) {
ast_manager& m = s.get_solver().get_manager(); ast_manager& m = s.m();
expr_ref_vector cubes(m), cube(m), hard_cubes(m); expr_ref_vector cubes(m), cube(m), hard_cubes(m);
switch (s.type()) { switch (s.type()) {
@ -365,7 +373,6 @@ private:
case conquer_task: goto conquer; case conquer_task: goto conquer;
} }
cube: cube:
SASSERT(s.type() == cube_task); SASSERT(s.type() == cube_task);
@ -374,22 +381,18 @@ private:
cube.reset(); cube.reset();
cube.append(s.split_cubes(1)); cube.append(s.split_cubes(1));
SASSERT(cube.size() <= 1); SASSERT(cube.size() <= 1);
if (!s.cubes().empty()) m_queue.add_task(s.clone());
if (!s.cubes().empty()) {
m_queue.add_task(s.clone());
}
if (!cube.empty()) s.assert_cube(cube.get(0)); if (!cube.empty()) s.assert_cube(cube.get(0));
// simplify
switch (s.simplify()) { switch (s.simplify()) {
case l_undef: break; case l_undef: break;
case l_true: report_sat(s); return; case l_true: report_sat(s); return;
case l_false: report_unsat(s); return; case l_false: report_unsat(s); return;
} }
if (s.canceled()) return; if (s.canceled()) return;
// extract cubes. // extract cubes.
cubes.reset(); cubes.reset();
s.set_cube_params(); s.set_cube_params();
while (true) { while (true) {
@ -418,16 +421,13 @@ private:
goto conquer; goto conquer;
} }
conquer: conquer:
SASSERT(s.type() == conquer_task); SASSERT(s.type() == conquer_task);
// extract a batch of cubes // extract a batch of cubes
cubes.reset(); cubes.reset();
cubes.append(s.split_cubes(conquer_batch_size())); cubes.append(s.split_cubes(conquer_batch_size()));
if (!s.cubes().empty()) { if (!s.cubes().empty()) m_queue.add_task(s.clone());
m_queue.add_task(s.clone());
}
s.set_conquer_params(); s.set_conquer_params();
hard_cubes.reset(); hard_cubes.reset();
@ -440,29 +440,33 @@ private:
if (s.canceled()) return; if (s.canceled()) return;
} }
IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes" << hard_cubes.size() << ")";); IF_VERBOSE(1, verbose_stream() << "(parallel_tactic :cubes " << cubes.size() << " :hard-cubes" << hard_cubes.size() << ")";);
if (!hard_cubes.empty()) { if (hard_cubes.empty()) return;
s.set_cubes(hard_cubes);
s.set_type(cube_task); s.set_cubes(hard_cubes);
goto cube; s.set_type(cube_task);
} goto cube;
else {
return;
}
} }
void run_solver() { void run_solver() {
while (solver_state* st = m_queue.get_task()) { try {
cube_and_conquer(*st); while (solver_state* st = m_queue.get_task()) {
{ cube_and_conquer(*st);
std::lock_guard<std::mutex> lock(m_mutex); collect_statistics(*st);
st->get_solver().collect_statistics(m_stats); m_queue.task_done(st);
if (st->m().canceled()) m_queue.shutdown();
IF_VERBOSE(1, display(verbose_stream()););
dealloc(st);
} }
m_queue.task_done(st);
if (st->m().canceled()) {
m_queue.shutdown();
}
dealloc(st);
} }
catch (z3_exception& ex) {
std::cout << ex.msg() << "\n";
m_queue.shutdown();
}
}
void collect_statistics(solver_state& s) {
std::lock_guard<std::mutex> lock(m_mutex);
s.get_solver().collect_statistics(m_stats);
} }
lbool solve(model_ref& mdl) { lbool solve(model_ref& mdl) {
@ -474,16 +478,19 @@ private:
t.join(); t.join();
} }
if (!m_models.empty()) { if (!m_models.empty()) {
mdl = m_models.back(); mdl = m_models.back();
return l_true; return l_true;
} }
if (m_has_undef) return l_undef; if (m_has_undef || m_manager.canceled())
return l_undef;
return l_false; return l_false;
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
m_stats.display(out); m_stats.display(out);
m_queue.display(out); m_queue.display(out);
std::lock_guard<std::mutex> lock(m_mutex);
out << "(parallel_tactic :unsat " << m_num_unsat << " :progress " << m_progress << " :models " << m_models.size() << ")\n";
return out; return out;
} }
@ -555,7 +562,6 @@ public:
} }
virtual void collect_statistics(statistics & st) const { virtual void collect_statistics(statistics & st) const {
// m_queue.collect_statistics(st);
st.copy(m_stats); st.copy(m_stats);
} }
virtual void reset_statistics() { virtual void reset_statistics() {