3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 23:35:26 +00:00
z3/src/tactic/smtlogics
Nikolaj Bjorner 483a973b37 add pre-processing to default tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-16 20:20:59 +03:00
..
CMakeLists.txt move parallel-tactic to solver level 2018-04-16 08:21:21 -07:00
nra_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
nra_tactic.h Made nra tactic public. 2016-05-25 18:21:04 +01:00
qfaufbv_tactic.cpp fix another bug uncovered by Dunlop, prepare grounds for equality solving within NNFs 2019-01-14 01:25:25 -08:00
qfaufbv_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfauflia_tactic.cpp na 2019-05-16 19:21:00 +03:00
qfauflia_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfbv_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
qfbv_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfidl_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
qfidl_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qflia_tactic.cpp add pre-processing to default tactic 2019-05-16 20:20:59 +03:00
qflia_tactic.h add pre-processing to default tactic 2019-05-16 20:20:59 +03:00
qflra_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
qflra_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfnia_tactic.cpp fix #2238 2019-05-08 10:15:57 +02:00
qfnia_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfnra_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
qfnra_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfuf_tactic.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
qfuf_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfufbv_ackr_model_converter.cpp make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfufbv_ackr_model_converter.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfufbv_tactic.cpp Use nullptr rather than 0/NULL. 2018-11-28 14:57:01 +07:00
qfufbv_tactic.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00
qfufbv_tactic_params.pyg Inc sat for ackr. 2016-03-10 17:36:06 +00:00
quant_tactics.cpp more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode 2018-11-02 18:44:53 -05:00
quant_tactics.h make include paths uniformly use path relative to src. #534 2017-07-31 13:24:11 -07:00