diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 149a4e853..ef8a9e77e 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -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 { diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 6aa365383..730061c8b 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -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); +} + diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h index fbee950c2..733413bb2 100644 --- a/src/smt/tactic/smt_tactic.h +++ b/src/smt/tactic/smt_tactic.h @@ -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 diff --git a/src/tactic/fd_solver/fd_solver.cpp b/src/tactic/fd_solver/fd_solver.cpp index 2af30b089..8e32b74d0 100644 --- a/src/tactic/fd_solver/fd_solver.cpp +++ b/src/tactic/fd_solver/fd_solver.cpp @@ -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); +} + diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index 1c48fef38..9f4f1b604 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -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; diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 3e479524e..23334bf07 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -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; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 6718eb13f..fee3bed77 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -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; } diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index a9b32e5a8..8aefad0a0 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -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)) )); } diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index 601f872aa..b35bc1f20 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -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); diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp index 4a0e9eb34..206914a0f 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.cpp +++ b/src/tactic/smtlogics/qfauflia_tactic.cpp @@ -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; diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 7c410e721..11d05cde6 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -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)); } diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp index a34a25e67..109089c2e 100644 --- a/src/tactic/smtlogics/qfidl_tactic.cpp +++ b/src/tactic/smtlogics/qfidl_tactic.cpp @@ -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); diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index eed4e4425..d2fcc922d 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -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); diff --git a/src/tactic/smtlogics/qflra_tactic.cpp b/src/tactic/smtlogics/qflra_tactic.cpp index b44ace7b1..90532cef6 100644 --- a/src/tactic/smtlogics/qflra_tactic.cpp +++ b/src/tactic/smtlogics/qflra_tactic.cpp @@ -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 } diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index b92e08006..02e3349aa 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -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) { diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index cc01950a2..7d93abe25 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -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))); } diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index 2de9612c6..6af75b13f 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -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)); } diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index a4e169856..38eaa25fb 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -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))); } diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 8438d1a32..910a5d53c 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -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", "") << "\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(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; } diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 1fb4486ec..09b2bd00c 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -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);