mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add psat to available tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
faf96ca910
commit
90fca8b378
|
@ -8,4 +8,6 @@ z3_add_component(sat_solver
|
|||
core_tactics
|
||||
sat_tactic
|
||||
solver
|
||||
TACTIC_HEADERS
|
||||
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);
|
||||
|
||||
|
|
Loading…
Reference in a new issue