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

adding smt parallel solving

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-15 16:16:48 -07:00
parent 252fb4af6e
commit 012a96fd81
17 changed files with 174 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_lookahead.cpp
View file

@ -1034,7 +1034,7 @@ namespace sat {
}
if (m_s.m_ext) {
m_ext = m_s.m_ext->copy(this, learned);
// m_ext = m_s.m_ext->copy(this, learned);
}
propagate();
m_qhead = m_trail.size();

2
src/sat/sat_lookahead.h
View file

@ -247,7 +247,7 @@ namespace sat {
stats m_stats;
model m_model;
cube_state m_cube_state;
scoped_ptr<extension> m_ext;
//scoped_ptr<extension> m_ext;
// ---------------------------------------
// truth values

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

@ -39,6 +39,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_timeout = p.timeout();
m_rlimit = p.rlimit();
m_max_conflicts = p.max_conflicts();
m_restart_max = p.restart_max();
m_core_validate = p.core_validate();
m_logic = _p.get_sym("logic", m_logic);
m_string_solver = p.string_solver();

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

@ -99,6 +99,7 @@ struct smt_params : public preprocessor_params,
unsigned m_phase_caching_off;
bool m_minimize_lemmas;
unsigned m_max_conflicts;
unsigned m_restart_max;
bool m_simplify_clauses;
unsigned m_tick;
bool m_display_features;

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

@ -21,6 +21,7 @@ def_module_params(module_name='smt',
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('max_conflicts', UINT, UINT_MAX, 'maximum number of conflicts before giving up.'),
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),
('mbqi.max_cexs_incr', UINT, 0, 'increment for MBQI_MAX_CEXS, the increment is performed after each round of MBQI'),

20
src/smt/smt_context.cpp
View file

@ -1829,6 +1829,15 @@ namespace smt {
m_bvar_inc *= INV_ACTIVITY_LIMIT;
}
expr* context::next_decision() {
bool_var var;
lbool phase;
m_case_split_queue->next_case_split(var, phase);
if (var == null_bool_var) return m_manager.mk_true();
m_case_split_queue->unassign_var_eh(var);
return bool_var2expr(var);
}
/**
\brief Execute next clase split, return false if there are no
more case splits to be performed.
@ -3433,6 +3442,7 @@ namespace smt {
m_num_conflicts = 0;
m_num_conflicts_since_restart = 0;
m_num_conflicts_since_lemma_gc = 0;
m_num_restarts = 0;
m_restart_threshold = m_fparams.m_restart_initial;
m_restart_outer_threshold = m_fparams.m_restart_initial;
m_agility = 0.0;
@ -3564,7 +3574,7 @@ namespace smt {
inc_limits();
if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent());
IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
@ -3573,9 +3583,10 @@ namespace smt {
if (m_fparams.m_restart_adaptive) {
verbose_stream() << " :agility " << m_agility;
}
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
verbose_stream() << ")\n");
// execute the restart
m_stats.m_num_restarts++;
m_num_restarts++;
if (m_scope_lvl > curr_lvl) {
pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level());
@ -3593,6 +3604,11 @@ namespace smt {
status = l_false;
return false;
}
if (m_num_restarts >= m_fparams.m_restart_max) {
status = l_undef;
m_last_search_failure = NUM_CONFLICTS;
return false;
}
}
if (m_fparams.m_simplify_clauses)
simplify_clauses();

4
src/smt/smt_context.h
View file

@ -889,6 +889,8 @@ namespace smt {
unsigned m_num_conflicts;
unsigned m_num_conflicts_since_restart;
unsigned m_num_conflicts_since_lemma_gc;
unsigned m_num_restarts;
unsigned m_num_simplifications;
unsigned m_restart_threshold;
unsigned m_restart_outer_threshold;
unsigned m_luby_idx;
@ -1030,6 +1032,8 @@ namespace smt {
enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args);
expr* next_decision();
protected:
bool decide();

12
src/smt/smt_kernel.cpp
View file

@ -175,11 +175,15 @@ namespace smt {
void get_guessed_literals(expr_ref_vector & result) {
m_kernel.get_guessed_literals(result);
}
expr* next_decision() {
return m_kernel.next_decision();
}
void collect_statistics(::statistics & st) const {
m_kernel.collect_statistics(st);
}
void reset_statistics() {
}
@ -347,6 +351,10 @@ namespace smt {
m_imp->get_guessed_literals(result);
}
expr* kernel::next_decision() {
return m_imp->next_decision();
}
void kernel::display(std::ostream & out) const {
m_imp->display(out);
}

5
src/smt/smt_kernel.h
View file

@ -212,6 +212,11 @@ namespace smt {
*/
void get_guessed_literals(expr_ref_vector & result);
/**
\brief return the next case split literal.
*/
expr* next_decision();
/**
\brief (For debubbing purposes) Prints the state of the kernel
*/

54
src/smt/smt_solver.cpp
View file

@ -30,9 +30,35 @@ Notes:
namespace smt {
class smt_solver : public solver_na2as {
struct cuber {
smt_solver& m_solver;
unsigned m_round;
expr_ref m_result;
cuber(smt_solver& s):
m_solver(s),
m_round(0),
m_result(s.get_manager()) {}
expr_ref cube() {
switch (m_round) {
case 0:
m_result = m_solver.m_context.next_decision();
break;
case 1:
m_result = m_solver.get_manager().mk_not(m_result);
break;
default:
m_result = m_solver.get_manager().mk_false();
break;
}
++m_round;
return m_result;
}
};
smt_params m_smt_params;
smt::kernel m_context;
progress_callback * m_callback;
cuber* m_cuber;
symbol m_logic;
bool m_minimizing_core;
bool m_core_extend_patterns;
@ -45,6 +71,7 @@ namespace smt {
solver_na2as(m),
m_smt_params(p),
m_context(m, m_smt_params),
m_cuber(nullptr),
m_minimizing_core(false),
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX),
@ -72,6 +99,7 @@ namespace smt {
virtual ~smt_solver() {
dec_ref_values(get_manager(), m_name2assertion);
dealloc(m_cuber);
}
virtual void updt_params(params_ref const & p) {
@ -204,7 +232,6 @@ namespace smt {
virtual ast_manager & get_manager() const { return m_context.m(); }
virtual void set_progress_callback(progress_callback * callback) {
m_callback = callback;
m_context.set_progress_callback(callback);
}
@ -217,13 +244,24 @@ namespace smt {
return m_context.get_formula(idx);
}
virtual expr_ref lookahead(expr_ref_vector const& assumptions, expr_ref_vector const& candidates) {
virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) {
ast_manager& m = get_manager();
return expr_ref(m.mk_true(), m);
}
virtual expr_ref_vector cube(expr_ref_vector&, unsigned) {
return expr_ref_vector(get_manager());
if (!m_cuber) {
m_cuber = alloc(cuber, *this);
}
expr_ref result = m_cuber->cube();
expr_ref_vector lits(m);
if (m.is_false(result)) {
dealloc(m_cuber);
m_cuber = nullptr;
}
if (m.is_true(result)) {
dealloc(m_cuber);
m_cuber = nullptr;
return lits;
}
lits.push_back(result);
return lits;
}
struct collect_fds_proc {

1
src/tactic/portfolio/CMakeLists.txt
View file

@ -8,6 +8,7 @@ z3_add_component(portfolio
pb2bv_solver.cpp
smt_strategic_solver.cpp
solver2lookahead.cpp
solver_sat_extension.cpp
COMPONENT_DEPENDENCIES
aig_tactic
fp

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

@ -41,8 +41,13 @@ Notes:
#include "solver/solver.h"
#include "solver/solver2tactic.h"
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "tactic/portfolio/fd_solver.h"
#include "tactic/smtlogics/parallel_params.hpp"
#include "smt/tactic/smt_tactic.h"
#include "smt/smt_solver.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "sat/tactic/sat_tactic.h"
class parallel_tactic : public tactic {
@ -184,7 +189,6 @@ class parallel_tactic : public tactic {
ref<solver> m_solver; // solver state
unsigned m_depth; // number of nested calls to cubing
double m_width; // estimate of fraction of problem handled by state
unsigned m_restart_max; // saved configuration value
public:
solver_state(ast_manager* m, solver* s, params_ref const& p, task_type t):
@ -196,8 +200,6 @@ class parallel_tactic : public tactic {
m_depth(0),
m_width(1.0)
{
parallel_params pp(p);
m_restart_max = pp.restart_max();
}
ast_manager& m() { return m_solver->get_manager(); }
@ -255,27 +257,12 @@ class parallel_tactic : public tactic {
lbool simplify() {
lbool r = l_undef;
if (m_depth == 1) {
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
set_simplify_params(true, true); // retain PB, retain blocked
r = get_solver().check_sat(0,0);
if (r != l_undef) return r;
// copy over the resulting clauses with a configuration that blasts PB constraints
set_simplify_params(false, true);
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);
}
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
set_simplify_params(false, true); // remove PB, retain blocked
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";);
set_simplify_params(true); // retain blocked
r = get_solver().check_sat(0,0);
if (r != l_undef) return r;
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-3)\n";);
set_simplify_params(false, false); // remove any PB, remove blocked
IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";);
set_simplify_params(false); // remove blocked
r = get_solver().check_sat(0,0);
return r;
}
@ -299,27 +286,26 @@ class parallel_tactic : public tactic {
}
void set_conquer_params(solver& s) {
parallel_params pp(m_params);
params_ref p;
p.copy(m_params);
p.set_bool("gc.burst", true); // apply eager gc
p.set_uint("simplify.delay", 1000); // delay simplification by 1000 conflicts
p.set_bool("lookahead_simplify", false);
p.set_uint("restart.max", m_restart_max);
p.set_uint("restart.max", pp.conquer_restart_max());
p.set_uint("inprocess.max", UINT_MAX); // base bounds on restart.max
s.updt_params(p);
}
void set_simplify_params(bool pb_simp, bool retain_blocked) {
void set_simplify_params(bool retain_blocked) {
parallel_params pp(m_params);
double mul = pp.simplify_multiplier();
unsigned mult = (mul == 0 ? 1 : std::max((unsigned)1, static_cast<unsigned>(m_depth * mul)));
params_ref p;
p.copy(m_params);
p.set_bool("cardinality.solver", pb_simp);
p.set_sym ("pb.solver", pb_simp ? symbol("solver") : symbol("circuit"));
if (p.get_uint("inprocess.max", UINT_MAX) == UINT_MAX)
p.set_uint("inprocess.max", pp.inprocess_max());
p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult);
p.set_uint("restart.max", pp.simplify_restart_max() * mult);
p.set_bool("lookahead_simplify", true);
p.set_uint("restart.max", UINT_MAX);
p.set_bool("retain_blocked_clauses", retain_blocked);
get_solver().updt_params(p);
}
@ -337,6 +323,7 @@ class parallel_tactic : public tactic {
private:
solver_ref m_solver;
ast_manager& m_manager;
params_ref m_params;
sref_vector<model> m_models;
@ -355,7 +342,8 @@ private:
std::string m_exn_msg;
void init() {
m_num_threads = omp_get_num_procs(); // TBD adjust by possible threads used inside each solver.
parallel_params pp(m_params);
m_num_threads = std::min((unsigned)omp_get_num_procs(), pp.threads_max());
m_progress = 0;
m_has_undef = false;
m_allsat = false;
@ -375,6 +363,7 @@ private:
}
void add_branches(unsigned b) {
if (b == 0) return;
{
std::lock_guard<std::mutex> lock(m_mutex);
m_branches += b;
@ -617,7 +606,6 @@ private:
}
else if (cubes.empty()) {
dec_branch();
return;
}
else {
s.inc_width(width);
@ -746,15 +734,16 @@ private:
public:
parallel_tactic(ast_manager& m, params_ref const& p) :
m_manager(m),
parallel_tactic(solver* s, params_ref const& p) :
m_solver(s),
m_manager(s->get_manager()),
m_params(p) {
init();
}
void operator ()(const goal_ref & g,goal_ref_buffer & result) {
ast_manager& m = g->m();
solver* s = mk_fd_solver(m, m_params);
solver* s = m_solver->translate(m, m_params);
solver_state* st = alloc(solver_state, 0, s, m_params, cube_task);
m_queue.add_task(st);
expr_ref_vector clauses(m);
@ -799,7 +788,8 @@ public:
}
tactic* translate(ast_manager& m) {
return alloc(parallel_tactic, m, m_params);
solver* s = m_solver->translate(m, m_params);
return alloc(parallel_tactic, s, m_params);
}
virtual void updt_params(params_ref const & p) {
@ -817,12 +807,40 @@ public:
virtual void reset_statistics() {
m_stats.reset();
}
};
tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p) {
return alloc(parallel_tactic, m, p);
tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
solver* s = mk_fd_solver(m, p);
return alloc(parallel_tactic, s, p);
}
tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
return alloc(parallel_tactic, s, p);
}
tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) {
parallel_params pp(p);
bool use_parallel = pp.enable();
return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p), p) : mk_sat_tactic(m);
}
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
bool use_parallel = pp.enable();
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
}
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
parallel_params pp(_p);
bool use_parallel = pp.enable();
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
}
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
}

13
src/tactic/portfolio/parallel_tactic.h
View file

@ -21,11 +21,20 @@ Notes:
class solver;
class tactic;
class solver;
tactic * mk_parallel_tactic(ast_manager& m, params_ref const& p);
tactic * mk_parallel_tactic(solver* s, params_ref const& p);
tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p);
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
// create parallel sat/smt tactics if parallel.enable=true, otherwise return sequential versions.
tactic * mk_psat_tactic(ast_manager& m, params_ref const& p);
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
/*
ADD_TACTIC("qffdp", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_tactic(m, p)")
ADD_TACTIC("pqffd", "builtin strategy for solving QF_FD problems in parallel.", "mk_parallel_qffd_tactic(m, p)")
ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
*/
#endif

6
src/tactic/smtlogics/nra_tactic.cpp
View file

@ -19,13 +19,13 @@ Notes:
#include "tactic/tactical.h"
#include "tactic/core/simplify_tactic.h"
#include "tactic/core/propagate_values_tactic.h"
#include "smt/tactic/smt_tactic.h"
#include "tactic/core/nnf_tactic.h"
#include "tactic/arith/probe_arith.h"
#include "smt/tactic/smt_tactic.h"
#include "qe/qe_tactic.h"
#include "qe/nlqsat.h"
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
#include "qe/qe_lite.h"
#include "tactic/arith/probe_arith.h"
#include "nlsat/tactic/qfnra_nlsat_tactic.h"
tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p;

11
src/tactic/smtlogics/parallel_params.pyg
View file

@ -4,8 +4,11 @@ def_module_params('parallel',
export=True,
params=(
('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'),
('conquer_batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'),
('inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
('restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
('conquer_threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'),
('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'),
('simplify.multiplier', DOUBLE, 0, 'restart and inprocess max is increased by depth * simplify.multipler, unless the multiplier is 0'),
('conquer.batch_size', UINT, 1000, 'number of cubes to batch together for fast conquer'),
('conquer.threshold', UINT, 10, 'number of cubes generated before simple conquer solver is created'),
('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),
('simplify.restart.max', UINT, 5000, 'maximal number of restarts during simplification phase'),
('simplify.inprocess.max', UINT, 2, 'maximal number of inprocessing steps during simplification'),
))

7
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -28,6 +28,7 @@ Notes:
#include "tactic/bv/bv_size_reduction_tactic.h"
#include "tactic/aig/aig_tactic.h"
#include "sat/tactic/sat_tactic.h"
#include "sat/sat_solver/inc_sat_solver.h"
#include "tactic/portfolio/parallel_tactic.h"
#include "tactic/smtlogics/parallel_params.hpp"
#include "ackermannization/ackermannize_bv_tactic.h"
@ -129,12 +130,10 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
parallel_params pp(p);
bool use_parallel = pp.enable();
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
use_parallel ? mk_parallel_tactic(m, p): mk_sat_tactic(m));
mk_psat_tactic(m, p));
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic());
return mk_qfbv_tactic(m, p, new_sat, mk_psmt_tactic(m, p));
}

11
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -24,7 +24,6 @@ Notes:
#include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/elim_uncnstr_tactic.h"
#include "smt/tactic/smt_tactic.h"
// include"mip_tactic.h"
#include "tactic/arith/add_bounds_tactic.h"
#include "tactic/arith/pb2bv_tactic.h"
#include "tactic/arith/lia2pb_tactic.h"
@ -35,6 +34,7 @@ Notes:
#include "sat/tactic/sat_tactic.h"
#include "tactic/arith/bound_manager.h"
#include "tactic/arith/probe_arith.h"
#include "tactic/portfolio/parallel_tactic.h"
struct quasi_pb_probe : public probe {
virtual result operator()(goal const & g) {
@ -42,10 +42,7 @@ struct quasi_pb_probe : public probe {
bound_manager bm(g.m());
bm(g);
rational l, u; bool st;
bound_manager::iterator it = bm.begin();
bound_manager::iterator end = bm.end();
for (; it != end; ++it) {
expr * t = *it;
for (expr * t : bm) {
if (bm.has_lower(t, l, st) && bm.has_upper(t, u, st) && (l.is_zero() || l.is_one()) && (u.is_zero() || u.is_one()))
continue;
if (found_non_01)
@ -93,7 +90,7 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m),
mk_aig_tactic(),
mk_sat_tactic(m)),
mk_sat_tactic(m, solver_p)),
solver_p);
}
@ -224,7 +221,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_lia2sat_tactic(m), quasi_pb_p),
mk_fail_if_undecided_tactic()),
mk_bounded_tactic(m),
mk_smt_tactic())),
mk_psmt_tactic(m, p))),
main_p);
st->updt_params(p);