mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-13 13:11:26 +00:00
Code Activity
19928 commits 74 branches 52 tags 181 MiB
Commit graph

19928 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
3224b75767 Initial plan 2025-09-04 01:44:31 +00:00
Nikolaj Bjorner
e0c315bc3e filter pseudo-linear monomials 2025-09-03 17:51:12 -07:00
Copilot
449704ef64
Enable ARM64 support in .NET NuGet package (#7846) 
* Initial plan

* Enable ARM64 support in .NET NuGet package by adding Linux ARM64 and macOS ARM64 to os_info mapping

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-03 15:20:54 -07:00
Nikolaj Bjorner
7005d04755 propagate mod over ite even if it hurts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-02 18:39:29 -07:00
Nikolaj Bjorner
a382ddbd8a add rewrite for mod over negation, refine axioms for grobner quotients 2025-09-02 18:26:22 -07:00
Nikolaj Bjorner
e2235d81d3 add option for gcd-test to grobner 2025-09-01 16:37:21 -07:00
Nikolaj Bjorner
49703f8bba remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 17:41:42 -07:00
Nikolaj Bjorner
4c0c199e32 take into account integer coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 16:07:37 -07:00
Nikolaj Bjorner
e91e432496 add option to propagation quotients 
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
 2025-08-31 14:41:23 -07:00
Nikolaj Bjorner
91b4873b79 categorize lp stats 2025-08-29 17:06:13 -07:00
Nikolaj Bjorner
06de5f422c remove str parameters 2025-08-29 17:06:13 -07:00
Andrew V. Teylu
9d16020a06
Use '--tags' rather than '--long' for git describe. Closes #6823 (#7833) 
Signed-off-by: Andrew V. Teylu <andrew.teylu@vector.com>
 2025-08-29 14:15: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
Nikolaj Bjorner
2337e68169 fix #7822 2025-08-27 09:17:55 -07:00
Copilot
b8b9327a70
[CMake] Document hybrid approach and fix FetchContent C++ header path issue (#7819) 
* Initial plan

* Add hybrid approach documentation for CMake

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

* Fix FetchContent C++ header include path issue

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

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>
 2025-08-27 08:45:10 -07:00
Nikolaj Bjorner
1bed5a4306 remove double tweak versioning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-26 09:51:11 -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
ba068d751c
Document how to use system-installed Z3 with CMake projects (#7809) 
* Initial plan

* Add documentation for using system-installed Z3 with CMake

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:23:49 -07:00
Nikolaj Bjorner
7e6e96f6aa remove resources directive again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 11:44:55 -07:00
Nikolaj Bjorner
12e74783b6 add resources 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 11:40:57 -07:00
Solal Pirelli
4792068517
Attempt at adding the README to the NuGet package (#7807) 
* Attempt at adding README to NuGet package

* Forgot to enable publishing
 2025-08-23 11:15:51 -07:00
Copilot
64419ad85b
Update nightly.yaml to match release.yml NuGet tool installer changes (#7810) 
* Initial plan

* Update nightly.yaml to match release.yml NuGet tool installer changes

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 11:15:21 -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
265265a68c
Create centralized version management with VERSION.txt (#7802) 
* Initial plan

* Create VERSION.txt and update CMakeLists.txt to read version from file

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

* Complete centralized version management system

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

* Fix version update script and finalize implementation

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

* Create centralized version management with VERSION.txt

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-20 09:12:33 -07:00
Nikolaj Bjorner
debe04350c fix #7796 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-18 09:30:03 -07:00
Nikolaj Bjorner
21e3168421 fix #7753 2025-08-17 17:20:10 -07:00
Nikolaj Bjorner
4542fc0b3b update version number to 4.15.4 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-17 17:09:56 -07:00
Nikolaj Bjorner
7ff0b246e8 fix #7792 
add missing revert operations
 2025-08-17 17:08:27 -07:00
Nikolaj Bjorner
ff74af7eaa check for internalized in solve_for 2025-08-17 16:51:02 -07:00
Nikolaj Bjorner
4082e4e56a update on euf 2025-08-17 16:51:00 -07:00
Nikolaj Bjorner
c75b8ec752 add option to control epsilon #7791 
#7791 reports on using model values during lex optimization that break soft constraints.
This is an artifact of using optimization where optimal values can be arbitrarily close to a rational.
In a way it is by design, but we give the user now an option to control the starting point for epsilon when converting infinitesimals into rationals.
 2025-08-17 16:51:00 -07:00
Copilot
d8bf0e047f
Fix nullptr dereference in pp_symbol when handling null symbol names (#7790) 
* Initial plan

* Fix nullptr dereference in pp_symbol with null symbol names

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-17 10:25:51 -07:00
Nikolaj Bjorner
a121e6c6e9 enable pypi public 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-15 16:09:34 -07:00
Copilot
7b8482a093
Remove NugetPublishNightly stage from nightly.yaml (#7787) 
* Initial plan

* Remove NugetPublishNightly stage from nightly.yaml

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-15 09:51:25 -07:00