- Fix all compilation errors in Go bindings
- Add missing type definitions (Pattern, ASTVector, ParamDescrs)
- Fix boolean comparisons to use bool() casts
- Fix Z3_app type casts using unsafe.Pointer
- Fix null symbol handling to use nil
- Fix unused variable in basic_example.go
- Fix CMake test target to run from examples/go directory
- Restore CI steps to build and test Go bindings
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
- Fix malformed z3.go with duplicate function body fragments
- Fix datatype.go to use Z3_del_constructor and Z3_del_constructor_list instead of non-existent inc_ref/dec_ref functions
- Remove non-existent Push/Pop methods from fixedpoint.go
- Fix CMake Go bindings targets quoting for proper LDFLAGS handling
- Add Go bindings support to ubuntu-cmake CI jobs
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This improves the previously cryptic error message. I searched multiple
websites before Google AI suggested using model.eval(arr[0]) for getting
solutions out of arrays.
- Add negative index support to AstVector.__setitem__, ModelRef.__getitem__, ApplyResult.__getitem__
- Replace bare assertions with proper Z3Exception in z3num.Numeral methods
- All changes tested and validated with comprehensive test suite
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This fixes the install_name_tool issue on macOS where the tool fails
with "larger updated load commands do not fit". The linker flag
-Wl,-headerpad_max_install_names ensures sufficient header padding
in the Mach-O binary for install_name_tool to modify install names.
Changes made:
- CMake: Added flag to libz3, z3java, z3jl shared libraries on Darwin
- Python build: Changed flag from ML-only to all macOS builds
- OCaml CMake: Added flag to OCaml stublib build on APPLE
Fixes#7623 (regression in 4.15.5)
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Add Java APIs for polymorphic datatypes and type variables
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Fix code review issue and add documentation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Add TypeVarSort.java to CMakeLists.txt for Java bindings
The CMake build was failing because TypeVarSort.java was not included in the Z3_JAVA_JAR_SOURCE_FILES list in src/api/java/CMakeLists.txt. Added it in alphabetical order between TupleSort.java and UninterpretedSort.java.
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* Initial plan
* Refactor find_probe() to use std::optional
- Updated tactic_manager.h: Changed return type to std::optional<probe_info*>
- Updated tactic_manager.cpp: Modified implementation to return std::nullopt or probe pointer
- Updated api_tactic.cpp: Changed 2 call sites to use optional checks and dereference
- Updated tactic_cmds.cpp: Changed 1 call site to use optional check and dereference
- Build verified successfully
- Probe functionality tested with Python bindings
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
* preserve the initial state of the solver with push/pop for multiple objectives
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Fix memory corruption in Z3_polynomial_subresultants
The API function had a memory corruption bug where allocating the result
vector while the default_expr2polynomial converter was still in scope
could corrupt the converter's internal expr2var mapping.
Fixed by restructuring the code to:
1. Complete all polynomial computation in a scoped block
2. Store results in a temporary expr_ref_vector
3. Let the converter go out of scope
4. Then allocate and populate the result vector
Also improved the test to:
- Use randomized testing with 20 iterations
- Test both cases: variable in polynomials and variable not in polynomials
- Use proper reference counting (inc_ref before dec_ref)
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
* 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 ebc0688) which refactored mk_and/mk_or call sites to use vector overloads. This supersedes the std::span changes in those files.
Retained std::span changes in files unique to this PR:
- Core API changes (ast.h, ast.cpp)
- Files not affected by PR #8286 (api_context.cpp, ast_util.cpp, bool_rewriter.h, datatype_rewriter.cpp, dom_simplifier.cpp, factor_rewriter.cpp, pb2bv_rewriter.cpp, quant_hoist.cpp, spacer_cluster_util.cpp, sortmax.cpp, array_axioms.cpp, smtfd_solver.cpp, goal.cpp, ho_matcher.cpp, qe_arith.cpp, sorting_network.cpp)
- Special case in hnf.cpp where both PRs modified different lines
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
