3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 11:07:51 +00:00
z3/src/tactic/smtlogics
Lev Nachmanson ab1b2ae86d remove dead code and a fix in no_lemmas_hold
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2020-01-28 10:04:21 -08:00
..
CMakeLists.txt address the NB's comments 2020-01-28 10:04:21 -08:00
nra_tactic.cpp fix #2546, retrieve model in optsmt lex before iterating 2019-09-10 11:19:59 +02:00
nra_tactic.h Made nra tactic public. 2016-05-25 18:21:04 +01:00
qfaufbv_tactic.cpp add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 2019-09-01 12:17:19 -07: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 fix #2873 2020-01-22 11:08:44 -06: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 fix #2390 2019-07-10 08:55:00 +01: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 remove dead code and a fix in no_lemmas_hold 2020-01-28 10:04:21 -08: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 remove cooperate 2019-06-12 20:15:46 -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