mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 23:52:02 +00:00
Code Activity
20106 commits 50 branches 53 tags 183 MiB
Commit graph

2667 commits

Author SHA1 Message Date
Nikolaj Bjorner
5079b10597 fix up documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-24 13:13:52 +02:00
Nikolaj Bjorner
69e0793f6c add overloads for finite sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-10-23 17:29:11 +02:00
Copilot
541a554ecd
Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) 
* Initial plan

* Add C API for finite sets

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add Python bindings for finite sets

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add C++ bindings for finite sets

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add documentation for finite set API

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>
 2025-10-23 17:10:47 +02:00
Ruijie Fang
339f0cd5f9
Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955) 
* Distinguish between Quantifier and Lambda in AST.java

* Distinguish betwee Lambda and Quantifier in Expr.java

* Make things compile
 2025-09-30 09:55:14 -07:00
Wael Boutglay
391880b6fc
Add missing ::z3::sdiv to z3++.h (#7947) 2025-09-25 22:04:15 +03:00
Nikolaj Bjorner
6e767795db set status to unknown 2025-09-14 13:43:10 -07:00
Nikolaj Bjorner
928a2e7cf2 update python doc tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-14 10:56:26 -07:00
Copilot
294f0578b0
Fix Java API mkString to properly handle Unicode surrogate pairs (#7865) 
* Initial plan

* Fix Java API mkString to properly handle surrogate pairs

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>
 2025-09-11 11:13:31 -07:00
Copilot
b2acbaa0c9
Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854) 
* Initial plan

* Fix .NET performance issues by reducing multiple enumerations in constraint methods

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor MkApp and related methods for null checks

* Update null checks for MkApp method arguments

* Fix assertion condition for MkApp method

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-07 16:43:13 -07:00
Copilot
90e610eb23
Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851) 
* Initial plan

* Fix performance issue in MkAnd(IEnumerable<BoolExpr>) method

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor IEnumerable methods to call params array variants

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>
 2025-09-06 19:50:38 -07:00
Karlheinz Friedberger
3e216dbb20
Fix method signature for onBindingWrapper, again (#7829) 
#7828
 2025-08-28 18:21:51 -07:00
Nikolaj Bjorner
a5609364dd
Fix method signature for onBindingWrapper 
#7828
 2025-08-28 13:04:04 -07:00
Shiwei Weng 翁士伟
894c0e9fbe
Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815) 
* fix: add generating META for ocamlfind.

* Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers.

* Trigger CI.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Hacky fix for ocaml building warning.

* Fix typo and rename variables.

* Fix cmake for ocaml test, using local libz3 explicit.
 2025-08-24 20:49:04 -07:00
Nikolaj Bjorner
12563c6963 clean up a little of the handling of VERSION.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 16:38:15 -07:00
Copilot
300e0ae69e
Move VERSION.txt to scripts directory and update all references (#7811) 
* Initial plan

* Move VERSION.txt to scripts/ and update all references

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>
 2025-08-24 16:36:05 -07:00
Nikolaj Bjorner
287464567b copy VERSION from SRC_DIR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 15:10:49 -07:00
Nikolaj Bjorner
116e1eca8b print dirs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 15:02:50 -07:00
Nikolaj Bjorner
be22111df5 more output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 14:49:56 -07:00
Nikolaj Bjorner
867bc6aee6 remove extra characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 14:36:23 -07:00
Nikolaj Bjorner
438b41acbf try other dir 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:27:26 -07:00
Nikolaj Bjorner
1987b3dde1 try src_dir_repo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:20:32 -07:00
Nikolaj Bjorner
778b9a57c3 try diferennt dirs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:13:18 -07:00
Nikolaj Bjorner
3b036369f9 add more logging to setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 16:37:06 -07:00
Nikolaj Bjorner
21e63dba8d add print for version file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 14:41:28 -07:00
Copilot
8d395d63ae
Fix Julia bindings linker errors on Windows MSVC (#7794) 
* Initial plan

* Fix Julia bindings linker errors on Windows MSVC

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete Julia bindings fix validation and testing

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix Julia bindings linker errors on Windows MSVC

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>
 2025-08-23 14:24:20 -07:00
Copilot
5d29eb1060
Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution (#7808) 
* Initial plan

* Fix Azure Pipeline PyPI package builds by including VERSION.txt in source distribution

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>
 2025-08-23 10:51:35 -07:00
Nikolaj Bjorner
fa0f9c97bc fix parsing of version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-20 09:45:06 -07:00
Nikolaj Bjorner
02f195a380 fix version parse 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-20 09:39:36 -07:00
Nikolaj Bjorner
72655637de read version from VERSION.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-20 09:24:58 -07:00
Copilot
1e7832a391
Use solver factory translate method in Z3_solver_translate (#7782) 
* Initial plan

* Fix Z3_solver_translate to use solver factory translate method

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>
 2025-08-14 18:13:23 -07:00
Nikolaj Bjorner
57a60c832b add > operator as shorthand for Array 2025-08-13 10:24:46 -07:00
Nikolaj Bjorner
3abb091336 fix #7776 2025-08-13 10:24:46 -07:00
Nikolaj Bjorner
fcd3a70c92 remove theory_str and classes that are only used by it 2025-08-07 21:05:12 -07:00
Nikolaj Bjorner
7ba967e136 fix java build for java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-07 14:37:29 -07:00
Nikolaj Bjorner
0cefc926b0 register on_binding attribute 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-07 13:46:07 -07:00
Nikolaj Bjorner
d57dd6ef73 use jboolean in Native interface 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-07 13:11:11 -07:00
Nikolaj Bjorner
fa3d341b18 add on_binding callbacks across APIs 
update release notes,
add to Java, .Net, C++
 2025-08-07 12:55:50 -07:00
Nikolaj Bjorner
aad511d40b missing new closure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-06 21:22:23 -07:00
Nikolaj Bjorner
b33f444545 add an option to register callback on quantifier instantiation 
Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation
 2025-08-06 21:11:55 -07:00
Nuno Lopes
b1ab695eb6
fix #7603: race condition in Ctrl-C handling (#7755) 
* fix #7603: race condition in Ctrl-C handling

* fix race in cancel_eh

* fix build
 2025-08-06 14:27:28 -07:00
Copilot
7a8ba4b474
Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) 
* Initial plan

* Add datatype type definitions to types.ts (work in progress)

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype type definitions with working TypeScript compilation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Implement core datatype functionality with TypeScript compilation success

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete datatype implementation with full Context integration and tests

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>
 2025-08-04 20:58:42 -07:00
Nikolaj Bjorner
07613942da Add parameter validation for selected API functions 2025-07-27 13:38:37 -07:00
humnrdble
eb24488c3e
FreshConst is_sort (#7748) 2025-07-27 03:19:43 -07:00
Nikolaj Bjorner
661ccb3702
Revert "Fix source installation to create dist-info directory for package dis…" (#7704) 
This reverts commit ad0afbb792.
 2025-06-29 09:11:32 -07:00
Copilot
ad0afbb792
Fix source installation to create dist-info directory for package discovery (#7695) 
* Initial plan

* Add proper pyproject.toml metadata for dist-info creation

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Clean up setup.py and add comprehensive test for dist-info fix

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix build errors in setup.py and pyproject.toml

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix ModuleNotFoundError by removing dynamic version loading from pyproject.toml

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Remove hardcoded version from pyproject.toml, use dynamic version from setup.py

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>
 2025-06-28 16:06:03 -07:00
Copilot
84a6e4d672
Fix pydoc doctest failures by updating expected output format for string operations (#7703) 
* Initial plan

* Fix pydoc doctest failures by updating expected output format

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>
 2025-06-27 19:11:04 -07:00
Shiwei Weng 翁士伟
c2efd3dc6d
Update on building OCaml binding with CMake (#7698) 
* fix: add generating META for ocamlfind.

* Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers.

* Trigger CI.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Hacky fix for ocaml building warning.

* Fix typo and rename variables.
 2025-06-27 17:55:58 -07:00
Copilot
2de40ff220
Improve Extract function documentation to clarify bit-vector vs sequence usage (#7701) 
* Initial plan

* Improve Extract function documentation to clarify bit-vector vs sequence usage

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>
 2025-06-27 10:21:23 -07:00
Dongjae Lee
3916c451e5
Fix: typo in z3 python api (#7693) 2025-06-24 07:13:44 -07:00
Nikolaj Bjorner
c387b20ac6 move smt params to params directory, update release.yml 2025-06-09 10:47:22 -07:00