From 90fca8b378b493b4213711fa91edfe29a6a3031d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Sep 2018 17:44:28 -0700 Subject: [PATCH] add psat to available tactics Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/CMakeLists.txt | 2 ++ src/sat/sat_solver/inc_sat_solver.h | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt index 14eb4ac25..45a673367 100644 --- a/src/sat/sat_solver/CMakeLists.txt +++ b/src/sat/sat_solver/CMakeLists.txt @@ -8,4 +8,6 @@ z3_add_component(sat_solver core_tactics sat_tactic solver + TACTIC_HEADERS + inc_sat_solver.h ) diff --git a/src/sat/sat_solver/inc_sat_solver.h b/src/sat/sat_solver/inc_sat_solver.h index 71ec48b99..b1cf7ad37 100644 --- a/src/sat/sat_solver/inc_sat_solver.h +++ b/src/sat/sat_solver/inc_sat_solver.h @@ -28,6 +28,9 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p, bool incremental_ tactic* mk_psat_tactic(ast_manager& m, params_ref const& p); +/* + ADD_TACTIC('psat', '(try to) solve goal using a parallel SAT solver.', 'mk_psat_tactic(m, p)') +*/ void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);