mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
remove dependencies on fd_tactic.h
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4e65c13726
commit
538411c67f
|
@ -18,7 +18,6 @@ Notes:
|
|||
--*/
|
||||
|
||||
#include "fd_solver.h"
|
||||
#include "fd_tactic.h"
|
||||
#include "tactic.h"
|
||||
#include "inc_sat_solver.h"
|
||||
#include "enum2bv_solver.h"
|
||||
|
|
|
@ -23,8 +23,13 @@ Notes:
|
|||
#include"params.h"
|
||||
|
||||
class solver;
|
||||
class tactic;
|
||||
|
||||
solver * mk_fd_solver(ast_manager & m, params_ref const & p);
|
||||
tactic * mk_fd_tactic(ast_manager & m, params_ref const & p);
|
||||
|
||||
/*
|
||||
ADD_TACTIC("qffd", "builtin strategy for solving QF_FD problems.", "mk_fd_tactic(m, p)")
|
||||
*/
|
||||
|
||||
#endif
|
||||
|
|
|
@ -38,7 +38,6 @@ Notes:
|
|||
#include"smt_solver.h"
|
||||
#include"inc_sat_solver.h"
|
||||
#include"fd_solver.h"
|
||||
#include"fd_tactic.h"
|
||||
#include"bv_rewriter.h"
|
||||
#include"solver2tactic.h"
|
||||
|
||||
|
|
Loading…
Reference in a new issue