| .. |
|
bit2int.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
bit_blaster.cpp
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
|
bit_blaster.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
blast_term_ite_simplifier.h
|
Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite
|
2026-02-26 20:07:42 +00:00 |
|
bound_manager.cpp
|
Refactor bound_manager to use C++17 structured bindings (#8404)
|
2026-01-27 20:04:01 -08:00 |
|
bound_manager.h
|
move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532
|
2023-01-12 12:42:28 -08:00 |
|
bound_propagator.cpp
|
Modern C++: Add std::span overload for mk_or, adopt std::clamp, optimize stream output (#8507)
|
2026-02-06 11:54:06 +00:00 |
|
bound_propagator.h
|
Add new tactic bound-simplifier for integer-based bit-vector reasoning.
|
2023-01-22 22:07:28 -08:00 |
|
bound_simplifier.cpp
|
Standardize for-loop increments to prefix form (++i) (#8199)
|
2026-01-14 19:55:31 -08:00 |
|
bound_simplifier.h
|
Arith min max (#6864)
|
2023-08-19 17:44:09 -07:00 |
|
bv1_blaster.cpp
|
Convert bv1-blast tactic to a simplifier
|
2026-02-26 04:01:11 +00:00 |
|
bv1_blaster.h
|
Convert bv1-blast tactic to a simplifier
|
2026-02-26 04:01:11 +00:00 |
|
bv_bounds_simplifier.cpp
|
Remove redundant overridden default destructors (#8191)
|
2026-01-14 18:41:26 +00:00 |
|
bv_bounds_simplifier.h
|
move dominator simplifier functionality to rewriter and simplifier, move bv_bounds simplifier functionality to simplifier
|
2023-01-27 17:11:48 -08:00 |
|
bv_elim.h
|
cave in to supporting proofs (partially) in simplifiers, updated doc
|
2022-12-06 17:02:04 -08:00 |
|
bv_slice.cpp
|
cave in to supporting proofs (partially) in simplifiers, updated doc
|
2022-12-06 17:02:04 -08:00 |
|
bv_slice.h
|
move qhead to attribute on the state instead of the simplifier,
|
2022-11-29 16:36:02 +07:00 |
|
card2bv.cpp
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
|
card2bv.h
|
move qhead to attribute on the state instead of the simplifier,
|
2022-11-29 16:36:02 +07:00 |
|
CMakeLists.txt
|
Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier
|
2026-02-26 15:52:18 -08:00 |
|
cnf_nnf.h
|
cave in to supporting proofs (partially) in simplifiers, updated doc
|
2022-12-06 17:02:04 -08:00 |
|
demodulator_simplifier.cpp
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
|
demodulator_simplifier.h
|
add demodulator tactic based on demodulator-simplifier
|
2022-12-05 03:20:46 -08:00 |
|
dependent_expr.h
|
fix bugs in flatten_clauses simplifier, switch proof/fml
|
2023-01-04 11:56:28 -08:00 |
|
dependent_expr_state.cpp
|
Standardize for-loop increments to prefix form (++i) (#8199)
|
2026-01-14 19:55:31 -08:00 |
|
dependent_expr_state.h
|
Replace empty destructors with = default for compiler optimization (#8189)
|
2026-01-13 10:50:10 -08:00 |
|
der_simplifier.h
|
Convert der tactic to simplifier: add der_simplifier.h and update der_tactic.h
|
2026-02-21 23:49:05 +00:00 |
|
distribute_forall.cpp
|
distribute forall cpp code
|
2022-12-06 18:15:18 -08:00 |
|
distribute_forall.h
|
update distribute forall
|
2022-12-06 17:59:33 -08:00 |
|
dominator_simplifier.cpp
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
|
dominator_simplifier.h
|
fix #6659
|
2023-03-31 10:31:18 -07:00 |
|
elim_bounds.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
elim_term_ite.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
elim_unconstrained.cpp
|
respect smt configuration parameter in elim_unconstrained simplifier
|
2025-07-24 16:22:08 -07:00 |
|
elim_unconstrained.h
|
respect smt configuration parameter in elim_unconstrained simplifier
|
2025-07-24 16:22:08 -07:00 |
|
eliminate_predicates.cpp
|
Standardize for-loop increments to prefix form (++i) (#8199)
|
2026-01-14 19:55:31 -08:00 |
|
eliminate_predicates.h
|
bug fixes to new core, elim_predicates and elim_unconstrained
|
2023-03-05 22:26:37 -08:00 |
|
euf_completion.cpp
|
Replace empty destructors with = default for compiler optimization (#8189)
|
2026-01-13 10:50:10 -08:00 |
|
euf_completion.h
|
Remove redundant overridden default destructors (#8191)
|
2026-01-14 18:41:26 +00:00 |
|
extract_eqs.cpp
|
fix #7796
|
2025-08-18 09:30:03 -07:00 |
|
extract_eqs.h
|
Replace empty destructors with = default for compiler optimization (#8189)
|
2026-01-13 10:50:10 -08:00 |
|
factor_simplifier.cpp
|
Add factor_simplifier and factor2 tactic wrapping the simplifier
|
2026-02-21 23:45:51 +00:00 |
|
factor_simplifier.h
|
Add factor_simplifier and factor2 tactic wrapping the simplifier
|
2026-02-21 23:45:51 +00:00 |
|
flatten_clauses.h
|
bugfix to flatten-clases simplifier
|
2023-01-05 20:59:28 -08:00 |
|
linear_equation.cpp
|
Standardize for-loop increments to prefix form (++i) (#8199)
|
2026-01-14 19:55:31 -08:00 |
|
linear_equation.h
|
delete more default constructors
|
2024-09-23 12:59:04 +01:00 |
|
max_bv_sharing.cpp
|
#6538
|
2023-01-15 15:58:29 -05:00 |
|
max_bv_sharing.h
|
Register max_bv_sharing simplifier via ADD_SIMPLIFIER
|
2026-02-21 23:26:47 +00:00 |
|
model_reconstruction_trail.cpp
|
fix #7792
|
2025-08-17 17:08:27 -07:00 |
|
model_reconstruction_trail.h
|
fix #7582
|
2025-03-12 17:17:47 -07:00 |
|
propagate_values.cpp
|
update doc
|
2022-12-11 10:16:17 -08:00 |
|
propagate_values.h
|
fix perf bugs in new value propagation
|
2022-12-04 03:53:30 -08:00 |
|
pull_nested_quantifiers.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
push_ite.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
randomizer.h
|
add seed parameter, fix trail undo order from insertion to ensure lifetime
|
2025-05-27 18:03:00 +01:00 |
|
reduce_args_simplifier.cpp
|
Standardize for-loop increments to prefix form (++i) (#8199)
|
2026-01-14 19:55:31 -08:00 |
|
reduce_args_simplifier.h
|
convert reduce-args to a simplifier
|
2023-01-28 20:12:14 -08:00 |
|
refine_inj_axiom.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
rewriter_simplifier.h
|
update release notes
|
2023-01-31 12:19:33 -08:00 |
|
solve_context_eqs.cpp
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
|
solve_context_eqs.h
|
fix #6894
|
2023-09-14 17:14:14 -07:00 |
|
solve_eqs.cpp
|
remove verbose output
|
2025-07-25 20:22:52 -07:00 |
|
solve_eqs.h
|
add option to selectively disable variable solving for only ground expressions
|
2025-07-25 19:15:20 -07:00 |
|
then_simplifier.h
|
Centralize and document TRACE tags using X-macros (#7657)
|
2025-05-28 14:31:25 +01:00 |
