3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
z3/src/ast/sls
Nikolaj Bjorner 059ccd67bb disable nested mul
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-08-24 13:27:09 -07:00
..
bv_sls_eval.cpp fixes and rename sls-cc to sls-euf-plugin 2024-07-15 21:45:30 -07:00
bv_sls_eval.h na 2024-07-15 22:26:18 -07:00
bv_sls_fixed.cpp bv updates 2024-07-14 19:34:24 -07:00
bv_sls_fixed.h na 2024-07-14 15:38:56 -07:00
bv_sls_terms.cpp na 2024-07-14 15:38:56 -07:00
bv_sls_terms.h na 2024-07-14 15:38:56 -07:00
bvsls_opt_engine.cpp remove reference to tactic.h 2023-12-22 13:17:04 -08:00
bvsls_opt_engine.h move sls core functionality to be independent of tactic 2023-12-22 12:00:52 -08:00
CMakeLists.txt fixes and rename sls-cc to sls-euf-plugin 2024-07-15 21:45:30 -07:00
sat_ddfw.cpp bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
sat_ddfw.h updates 2024-08-19 16:04:28 -07:00
sls_arith_base.cpp disable nested mul 2024-08-24 13:27:09 -07:00
sls_arith_base.h updates 2024-08-19 16:04:28 -07:00
sls_arith_plugin.cpp fixes to ite and other 2024-08-16 16:48:12 -07:00
sls_arith_plugin.h bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
sls_basic_plugin.cpp fixes to ite and other 2024-08-16 16:48:12 -07:00
sls_basic_plugin.h refactor basic plugin and clause generation 2024-08-15 14:04:03 -07:00
sls_bv_plugin.cpp bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
sls_bv_plugin.h bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
sls_context.cpp updates 2024-08-19 16:04:28 -07:00
sls_context.h updates 2024-08-19 16:04:28 -07:00
sls_engine.cpp updates to sls 2024-03-30 12:59:05 -07:00
sls_engine.h updates to sls 2024-03-30 12:59:05 -07:00
sls_euf_plugin.cpp fixes and rename sls-cc to sls-euf-plugin 2024-07-15 21:45:30 -07:00
sls_euf_plugin.h bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
sls_evaluator.h move sls core functionality to be independent of tactic 2023-12-22 12:00:52 -08:00
sls_powers.h initial stab at new bv-sls based on repair actions 2024-03-05 12:28:29 -08:00
sls_smt_solver.cpp updates 2024-08-19 16:04:28 -07:00
sls_smt_solver.h refactor basic plugin and clause generation 2024-08-15 14:04:03 -07:00
sls_stats.h na 2024-03-05 12:28:30 -08:00
sls_tracker.h move sls core functionality to be independent of tactic 2023-12-22 12:00:52 -08:00
sls_valuation.cpp reshuffle priorities on multiplication allow non-determinism. 2024-06-15 10:47:10 -07:00
sls_valuation.h cleanup 2024-04-10 19:09:30 -07:00