From 09b75d2122077c75bf6e4b1c3c3a1b9a0b9f5dc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 May 2026 14:58:55 -0700 Subject: [PATCH] connect parallel tactical2 as side load Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 7 ++++++- src/smt/tactic/smt_tactic_core.cpp | 17 +++++++++++++++-- src/solver/parallel_params.pyg | 1 + 3 files changed, 22 insertions(+), 3 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7e7200832..11b5c771d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -27,6 +27,7 @@ Notes: #include "solver/tactic2solver.h" #include "solver/parallel_params.hpp" #include "solver/parallel_tactical.h" +#include "solver/parallel_tactical2.h" #include "tactic/tactical.h" #include "tactic/aig/aig_tactic.h" #include "tactic/core/propagate_values_tactic.h" @@ -1183,5 +1184,9 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof tactic * mk_psat_tactic(ast_manager& m, params_ref const& p) { parallel_params pp(p); - return pp.enable() ? mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p) : mk_sat_tactic(m); + if (pp.enable()) + return mk_parallel_tactic(mk_inc_sat_solver(m, p, false), p); + if (pp.enable2()) + return mk_parallel_tactic2(mk_inc_sat_solver(m, p, false), p); + return mk_sat_tactic(m); } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 69d38a35b..6a624b59a 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -31,6 +31,7 @@ Notes: #include "solver/solver.h" #include "solver/mus.h" #include "solver/parallel_tactical.h" +#include "solver/parallel_tactical2.h" #include "solver/parallel_params.hpp" #include @@ -429,18 +430,30 @@ static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) { tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) { + parallel_params pp(p); + if (pp.enable2()) + return mk_parallel_tactic2(mk_smt_solver(m, p, symbol::null), p); return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p); } tactic * mk_smt_tactic_core(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(m, p); + if (pp.enable()) + return mk_parallel_tactic(mk_smt_solver(m, p, logic), p); + if (pp.enable2()) + return mk_parallel_tactic2(mk_smt_solver(m, p, logic), p); + return mk_seq_smt_tactic(m, p); } tactic * mk_smt_tactic_core_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(m, p), p); + tactic *t = nullptr; + if (pp.enable() || pp.enable2()) + t = mk_parallel_smt_tactic(m, p); + else + t = mk_seq_smt_tactic(m, p); + return using_params(t, p); } diff --git a/src/solver/parallel_params.pyg b/src/solver/parallel_params.pyg index 60a77d49a..2aa2acf77 100644 --- a/src/solver/parallel_params.pyg +++ b/src/solver/parallel_params.pyg @@ -4,6 +4,7 @@ def_module_params('parallel', export=True, params=( ('enable', BOOL, False, 'enable parallel solver by default on selected tactics (for QF_BV)'), + ('enable2', BOOL, False, 'enable (experimental) parallel solver by default on selected tactics (for QF_BV)'), ('threads.max', UINT, 10000, 'caps maximal number of threads below the number of processors'), ('conquer.batch_size', UINT, 100, 'number of cubes to batch together for fast conquer'), ('conquer.restart.max', UINT, 5, 'maximal number of restarts during conquer phase'),