3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 15:33:59 +00:00
z3/src/tactic/portfolio
Nikolaj Bjorner 6caef86738 translate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-22 21:05:54 -07:00
..
bounded_int2bv_solver.cpp add facility to add lemmas 2017-06-12 19:44:02 -07:00
bounded_int2bv_solver.h add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 2016-10-23 20:31:59 -07:00
default_tactic.cpp enable exposing internal solver state on interrupted solvers 2017-05-30 17:33:27 -07:00
default_tactic.h Export default tactic for use via the SMT-LIB 2 interface. 2016-05-26 09:55:08 -03:00
enum2bv_solver.cpp add facility to add lemmas 2017-06-12 19:44:02 -07:00
enum2bv_solver.h add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 2016-10-23 20:31:59 -07:00
fd_solver.cpp remove dependencies on fd_tactic.h 2017-06-01 15:03:34 -07:00
fd_solver.h remove dependencies on fd_tactic.h 2017-06-01 15:03:34 -07:00
pb2bv_solver.cpp translate 2017-06-22 21:05:54 -07:00
pb2bv_solver.h add bounded-int and pb2bv solvers to fd_solver, use sorting networks for pb2bv rewriter when applicable, hoist to pb2bv_rewriter module and remove it from the pb2bv_tactic 2016-10-23 20:31:59 -07:00
smt_strategic_solver.cpp remove dependencies on fd_tactic.h 2017-06-01 15:03:34 -07:00
smt_strategic_solver.h update header guards to be C++ style. Fixes issue #9 2015-07-08 23:18:40 -07:00