mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-06-01 15:03:55 -07:00
commit 833a910d57
3 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tactic/portfolio/fd_solver.cpp
View file

@ -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"

5
src/tactic/portfolio/fd_solver.h
View file

@ -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

1
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -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"