mirror of
https://github.com/Z3Prover/z3
synced 2026-07-28 01:42:43 +00:00
058a8c082d
* Initial plan
* Refactor mk_and and mk_app to use std::span
- Made mk_and(unsigned num_args, expr * const * args) private
- Added new public mk_and(std::span<expr* const> args) method
- Added new public mk_app(family_id fid, decl_kind k, std::span<expr* const> args) method
- Updated all convenience overloads to use std::span version
- Updated all external call sites to use the new std::span API
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix remaining test files to use std::span API
- Updated src/test/sorting_network.cpp
- Updated src/test/ho_matcher.cpp with explicit cast to resolve ambiguity
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Revert overlapping changes superseded by PR #8286
Reverted 30 files to match the state from PR #8286 (commit
|
||
|---|---|---|
| .. | ||
| CMakeLists.txt | ||
| maxcore.cpp | ||
| maxcore.h | ||
| maxlex.cpp | ||
| maxlex.h | ||
| maxsmt.cpp | ||
| maxsmt.h | ||
| opt_cmds.cpp | ||
| opt_cmds.h | ||
| opt_context.cpp | ||
| opt_context.h | ||
| opt_cores.cpp | ||
| opt_cores.h | ||
| opt_lns.cpp | ||
| opt_lns.h | ||
| opt_mux.h | ||
| opt_params.pyg | ||
| opt_pareto.cpp | ||
| opt_pareto.h | ||
| opt_parse.cpp | ||
| opt_parse.h | ||
| opt_preprocess.cpp | ||
| opt_preprocess.h | ||
| opt_sls_solver.h | ||
| opt_solver.cpp | ||
| opt_solver.h | ||
| optsmt.cpp | ||
| optsmt.h | ||
| pb_sls.cpp | ||
| pb_sls.h | ||
| sortmax.cpp | ||
| totalizer.cpp | ||
| totalizer.h | ||
| wmax.cpp | ||
| wmax.h | ||