mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-02 18:44:53 -05:00
parent d9e77ba443
commit cf4bf7b591
20 changed files with 73 additions and 65 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/tactic/sat_tactic.cpp
View file

@ -17,12 +17,10 @@ Notes:
--*/
#include "ast/ast_pp.h"
#include "model/model_v2_pp.h"
#include "tactic/tactical.h"
#include "sat/tactic/goal2sat.h"
#include "sat/sat_solver.h"
#include "solver/parallel_tactic.h"
#include "solver/parallel_params.hpp"
#include "model/model_v2_pp.h"
class sat_tactic : public tactic {

31
src/smt/tactic/smt_tactic.cpp
View file

@ -289,30 +289,31 @@ public:
}
};
tactic * mk_smt_tactic(params_ref const & p) {
static tactic * mk_seq_smt_tactic(params_ref const & p) {
return alloc(smt_tactic, p);
}
tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
static tactic * mk_seq_smt_tactic_using(bool auto_config, params_ref const & _p) {
params_ref p = _p;
p.set_bool("auto_config", auto_config);
tactic * r = mk_smt_tactic(p);
tactic * r = mk_seq_smt_tactic(p);
TRACE("smt_tactic", tout << "auto_config: " << auto_config << "\nr: " << r << "\np: " << p << "\n";);
return using_params(r, p);
}
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
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);
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);
}
tactic * mk_smt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(p);
}
tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p) {
parallel_params pp(_p);
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(p), p);
}

8
src/smt/tactic/smt_tactic.h
View file

@ -27,17 +27,15 @@ Notes:
class tactic;
class filter_model_converter;
tactic * mk_smt_tactic(params_ref const & p = params_ref());
tactic * mk_smt_tactic(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
// syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config = true, params_ref const & p = params_ref());
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);
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(m, p)")
ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
*/
#endif

13
src/tactic/fd_solver/fd_solver.cpp
View file

@ -35,11 +35,18 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p, bool incremental_mo
return s;
}
tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) {
static tactic * mk_seq_fd_tactic(ast_manager & m, params_ref const& p) {
return mk_solver2tactic(mk_fd_solver(m, p, false));
}
tactic * mk_parallel_qffd_tactic(ast_manager& m, params_ref const& p) {
solver* s = mk_fd_solver(m, p);
return mk_parallel_tactic(s, p);
return mk_parallel_tactic(mk_fd_solver(m, p), p);
}
tactic * mk_fd_tactic(ast_manager & m, params_ref const& _p) {
parallel_params pp(_p);
params_ref p = _p;
return pp.enable() ? mk_parallel_qffd_tactic(m, p) : mk_seq_fd_tactic(m, p);
}

4
src/tactic/fpa/qffp_tactic.cpp
View file

@ -94,11 +94,11 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(),
cond(mk_produce_proofs_probe(),
mk_smt_tactic(p), // `sat' does not support proofs.
mk_smt_tactic(m, p), // `sat' does not support proofs.
mk_sat_tactic(m, p)),
cond(mk_is_fp_qfnra_probe(),
mk_qfnra_tactic(m, p),
mk_smt_tactic(p))));
mk_smt_tactic(m, p))));
st->updt_params(p);
return st;

2
src/tactic/portfolio/default_tactic.cpp
View file

@ -48,7 +48,7 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p),
//cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
mk_smt_tactic()))))))))))))),
mk_smt_tactic(m)))))))))))))),
p);
return st;
}

6
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -41,6 +41,9 @@ Notes:
#include "sat/sat_solver/inc_sat_solver.h"
#include "ast/rewriter/bv_rewriter.h"
#include "solver/solver2tactic.h"
#include "solver/parallel_tactic.h"
#include "solver/parallel_params.hpp"
tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
@ -99,7 +102,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
}
static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) {
if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled())
parallel_params pp(p);
if ((logic == "QF_FD" || logic == "SAT") && !m.proofs_enabled() && !pp.enable())
return mk_fd_solver(m, p);
return nullptr;
}

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

@ -44,7 +44,7 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
mk_qfnra_nlsat_tactic(m, p2)),
or_else(mk_nlqsat_tactic(m, p),
mk_smt_tactic(p))
mk_smt_tactic(m, p))
));
}

2
src/tactic/smtlogics/qfaufbv_tactic.cpp
View file

@ -57,7 +57,7 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
);
tactic * st = using_params(and_then(preamble_st,
using_params(mk_smt_tactic(), solver_p)),
using_params(mk_smt_tactic(m), solver_p)),
main_p);
st->updt_params(p);

2
src/tactic/smtlogics/qfauflia_tactic.cpp
View file

@ -45,7 +45,7 @@ tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) {
);
tactic * st = and_then(using_params(preamble_st, main_p),
using_params(mk_smt_tactic(), solver_p));
using_params(mk_smt_tactic(m), solver_p));
st->updt_params(p);
return st;

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

@ -121,9 +121,9 @@ 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) {
tactic * new_sat = cond(mk_produce_proofs_probe(),
and_then(mk_simplify_tactic(m), mk_smt_tactic()),
and_then(mk_simplify_tactic(m), mk_smt_tactic(m)),
mk_psat_tactic(m, p));
return mk_qfbv_tactic(m, p, new_sat, mk_psmt_tactic(m, p));
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));
}

4
src/tactic/smtlogics/qfidl_tactic.cpp
View file

@ -101,9 +101,9 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
using_params(and_then(preamble_st,
or_else(using_params(mk_diff_neq_tactic(m), diff_neq_p),
try2bv,
mk_smt_tactic())),
mk_smt_tactic(m))),
main_p),
mk_smt_tactic());
mk_smt_tactic(m));
st->updt_params(p);

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

@ -58,21 +58,21 @@ probe * mk_is_quasi_pb_probe() {
}
// Create SMT solver that does not use cuts
static tactic * mk_no_cut_smt_tactic(unsigned rs) {
static tactic * mk_no_cut_smt_tactic(ast_manager& m, unsigned rs) {
params_ref solver_p;
solver_p.set_sym(symbol("smt.logic"), symbol("QF_LIA")); // force smt_setup to use the new solver
solver_p.set_uint("arith.branch_cut_ratio", 10000000);
solver_p.set_uint("random_seed", rs);
return annotate_tactic("no-cut-smt-tactic", using_params(mk_smt_tactic_using(false), solver_p));
return annotate_tactic("no-cut-smt-tactic", using_params(mk_smt_tactic_using(m, false), solver_p));
}
// Create SMT solver that does not use cuts
static tactic * mk_no_cut_no_relevancy_smt_tactic(unsigned rs) {
static tactic * mk_no_cut_no_relevancy_smt_tactic(ast_manager& m, unsigned rs) {
params_ref solver_p;
solver_p.set_uint("arith.branch_cut_ratio", 10000000);
solver_p.set_uint("random_seed", rs);
solver_p.set_uint("relevancy", 0);
return annotate_tactic("no-cut-relevancy-tactic", using_params(mk_smt_tactic_using(false), solver_p));
return annotate_tactic("no-cut-relevancy-tactic", using_params(mk_smt_tactic_using(m, false), solver_p));
}
static tactic * mk_bv2sat_tactic(ast_manager & m) {
@ -155,10 +155,10 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
or_else(// try_for(mk_mip_tactic(m), 5000),
try_for(mk_no_cut_smt_tactic(100), 2000),
try_for(mk_no_cut_smt_tactic(m, 100), 2000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
try_for(mk_lia2sat_tactic(m), 5000)),
try_for(mk_no_cut_smt_tactic(200), 5000),
try_for(mk_no_cut_smt_tactic(m, 200), 5000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
try_for(mk_lia2sat_tactic(m), 10000))
// , mk_mip_tactic(m)
@ -170,9 +170,9 @@ static tactic * mk_bounded_tactic(ast_manager & m) {
return annotate_tactic(
"bounded-tactic",
and_then(fail_if(mk_is_unbounded_probe()),
or_else(try_for(mk_no_cut_smt_tactic(100), 5000),
try_for(mk_no_cut_no_relevancy_smt_tactic(200), 5000),
try_for(mk_no_cut_smt_tactic(300), 15000)
or_else(try_for(mk_no_cut_smt_tactic(m, 100), 5000),
try_for(mk_no_cut_no_relevancy_smt_tactic(m, 200), 5000),
try_for(mk_no_cut_smt_tactic(m, 300), 15000)
),
mk_fail_if_undecided_tactic()));
}
@ -218,7 +218,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_smt_tactic(m))),
main_p);

4
src/tactic/smtlogics/qflra_tactic.cpp
View file

@ -68,7 +68,7 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
#endif
// return using_params(or_else(mip,
// using_params(mk_smt_tactic(), pivot_p)),
// using_params(mk_smt_tactic(m), pivot_p)),
// p);
#if 0
@ -82,7 +82,7 @@ tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
using_params(mk_smt_tactic(), simplex_1),
using_params(mk_smt_tactic(), simplex_2));
#else
return using_params(using_params(mk_smt_tactic(), pivot_p), p);
return using_params(using_params(mk_smt_tactic(m), pivot_p), p);
#endif
}

2
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -105,7 +105,7 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) {
static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) {
params_ref simp_p = p;
simp_p.set_bool("som", true); // expand into sums of monomials
return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic());
return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic(m));
}
tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {

4
src/tactic/smtlogics/qfnra_tactic.cpp
View file

@ -28,7 +28,7 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne
nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size));
return and_then(mk_nla2bv_tactic(m, nra2sat_p),
mk_smt_tactic(),
mk_smt_tactic(m),
mk_fail_if_undecided_tactic());
}
@ -47,7 +47,7 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000),
try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
mk_qfnra_sat_solver(m, p, 4),
and_then(try_for(mk_smt_tactic(), 5000), mk_fail_if_undecided_tactic()),
and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()),
mk_qfnra_sat_solver(m, p, 6),
mk_qfnra_nlsat_tactic(m, p2)));
}

2
src/tactic/smtlogics/qfuf_tactic.cpp
View file

@ -34,7 +34,7 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
mk_solve_eqs_tactic(m, p),
using_params(mk_simplify_tactic(m, p), s2_p),
if_no_proofs(if_no_unsat_cores(mk_symmetry_reduce_tactic(m, p))),
mk_smt_tactic(p));
mk_smt_tactic(m, p));
}

4
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -176,7 +176,7 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
tactic * const preamble_st = mk_qfufbv_preamble(m, p);
tactic * st = using_params(and_then(preamble_st,
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic())),
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m))),
main_p);
st->updt_params(p);
@ -188,5 +188,5 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
return and_then(preamble_t,
cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m)));
}

18
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -64,14 +64,14 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
mk_qe_lite_tactic(m, p),
mk_smt_tactic());
mk_smt_tactic(m));
st->updt_params(p);
return st;
}
tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_quant_preprocessor(m),
mk_smt_tactic());
mk_smt_tactic(m));
st->updt_params(p);
return st;
}
@ -82,23 +82,23 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) {
TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "<null>") << "\n";);
tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast<double>(128)))),
using_params(mk_smt_tactic(), qi_p),
using_params(mk_smt_tactic(m), qi_p),
mk_fail_if_undecided_tactic()),
mk_smt_tactic()));
mk_smt_tactic(m)));
st->updt_params(p);
return st;
}
tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_quant_preprocessor(m),
mk_smt_tactic());
mk_smt_tactic(m));
st->updt_params(p);
return st;
}
tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_quant_preprocessor(m),
mk_smt_tactic());
mk_smt_tactic(m));
st->updt_params(p);
return st;
}
@ -109,9 +109,9 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
cond(mk_has_quantifier_probe(),
cond(mk_is_lira_probe(),
or_else(mk_qsat_tactic(m, p),
and_then(mk_qe_tactic(m), mk_smt_tactic())),
mk_smt_tactic()),
mk_smt_tactic()));
and_then(mk_qe_tactic(m), mk_smt_tactic(m))),
mk_smt_tactic(m)),
mk_smt_tactic(m)));
st->updt_params(p);
return st;
}

2
src/tactic/ufbv/ufbv_tactic.cpp
View file

@ -67,7 +67,7 @@ tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {
main_p.set_bool("elim_and", true);
tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2),
mk_smt_tactic_using(false, main_p));
mk_smt_tactic_using(m, false, main_p));
t->updt_params(p);