diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index 12842daac..c56c0359e 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -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" diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h index 41605c460..a52245e0d 100644 --- a/src/tactic/portfolio/fd_solver.h +++ b/src/tactic/portfolio/fd_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 diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 15d2e02c2..188174eca 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -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"