3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 01:54:08 +00:00
Commit graph

18574 commits

Author SHA1 Message Date
Nikolaj Bjorner c67200ef72 update versions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-26 08:28:18 -08:00
Nikolaj Bjorner fa2c0e0278 enable release publish
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-24 14:35:07 -08:00
John Fleisher 85425a6e08
Update nightly.yaml for Azure Pipelines (#7139)
* Update nightly.yaml for Azure Pipelines

match nightly builds to release builds

* Fix nightly.yaml

* fix indent

* fix indent

* Update nightly.yaml

* Update nightly.yaml

* Update nightly.yaml for Azure Pipelines

* Update nightly.yaml for Azure Pipelines

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-24 02:13:35 -08:00
Bruce Mitchener 19f5e7ffea
ci: Really fix set-output. (#7138)
I accidentally left the old line in PR #7136.
2024-02-22 10:36:13 -08:00
Nikolaj Bjorner 019c0648fa
Update coverage.yml 2024-02-22 09:37:08 -08:00
Bruce Mitchener c0621cb760
ci: Stop using deprecated ::set-output. (#7136)
This has been deprecated and the replacement functionality is
described here:

https://github.blog/changelog/2022-10-11-github-actions-deprecating-save-state-and-set-output-commands/
2024-02-22 09:35:47 -08:00
Bruce Mitchener 143a35d370
Fix typos. (#7137) 2024-02-22 09:35:15 -08:00
Nikolaj Bjorner 785f71b1a6 prepare for 12.6
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-21 19:35:24 -08:00
Nikolaj Bjorner 79b7d8a9e2 throttle squash-store #7134
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-21 10:00:11 -08:00
Thomas Haas a3d00ce356
Improved Java phantom references (#7131)
* Reworked phantom reference handling.
 - Replaced IDecRefQueue with a new Z3ReferenceQueue class
 - Z3ReferenceQueue manages custom subclasses of phantom references in a doubly-linked list
 - Replaced all subclasses of IDecRefQueue with subclasses of Z3ReferenceQueue.Reference. These custom reference classes are embedded in the class they reference count.
 - Context now owns a single Z3ReferenceQueue for all types of references.

* Made Statistics.Entry a static subclass

* Made Context.close idempotent (as recommended)

* Update CMakeLists.txt for building the Java API.

* Updated CMakeLists.txt again.

* Use correct SuppressWarning annotation to silence the compiler

* Formatting
2024-02-21 08:39:58 -08:00
Nikolaj Bjorner f7691d34fd fix generic example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-21 08:16:01 -08:00
Cal Jacobson 199ef30e0c
conditionally depend on importlib_resources (#7116)
In python >= 3.9, it's available as part of the stdlib.
2024-02-18 12:20:24 +07:00
Nikolaj Bjorner 84d592c1f2 fix #7121
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-16 09:59:57 +07:00
Nikolaj Bjorner 2b14793213 #7117
probably overflow of unsigned for large capacity
2024-02-14 17:08:09 +07:00
Bruce Mitchener 155dfb10c4
Fix some typos in identifiers. (#7118) 2024-02-14 09:25:32 +07:00
Bruce Mitchener dba2f788df
ci: Update microsoft/setup-msbuild to v2 from v1.3. (#7119)
This changes from using Node 16 to Node 20 internally, eliminating
some deprecation warnings from within GitHub Actions.
2024-02-14 09:24:31 +07:00
Lev Nachmanson 4d06c399cc replace DEBUG_CODE by #ifdef Z3DEBUG in nlsat
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2024-02-13 10:51:44 -10:00
Nikolaj Bjorner f1d97c7a3a allow callbacks to be nested 2024-02-13 20:30:17 +07:00
Bruce Mitchener 53f89a81c1
Fix some typos. (#7115) 2024-02-07 23:06:43 -08:00
Nikolaj Bjorner 937d4aa8f4 move files from lib and java directory to bin
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-06 12:40:30 -08:00
Nikolaj Bjorner c40e72aaa3 include debug output 2024-02-05 15:31:33 -08:00
Nikolaj Bjorner f4eaa6fc98 improve logging
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-05 14:41:29 -08:00
Nikolaj Bjorner 683070a175 finish encoding of n'th root
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-05 10:44:41 -08:00
Nikolaj Bjorner 8555f25587 add todo note, and log more lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 21:08:04 -08:00
Nikolaj Bjorner f4474a3edb typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 20:30:56 -08:00
Nikolaj Bjorner 446a9dec08 distinguish vs-arch from arch identifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 19:26:50 -08:00
Nikolaj Bjorner d743e1b47c add note that the encoding is a first approximation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 19:11:35 -08:00
Nikolaj Bjorner b9528b1c56 update self-validator to handle root expressions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 19:06:30 -08:00
Nikolaj Bjorner 548b9d091f move libz3.so from lib to bin, remove lib from distribution
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 18:23:46 -08:00
Nikolaj Bjorner 7970e4fe51 add clause persistence to sat/smt solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 16:42:10 -08:00
Nikolaj Bjorner 3cec3fc63d bypass replaying new clause within propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 15:26:17 -08:00
Nikolaj Bjorner 3b90816025 add option to persist clauses #7109
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-04 11:15:59 -08:00
Nikolaj Bjorner a2fa4ff1bc update assembly names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 16:52:20 -08:00
Nikolaj Bjorner c9267055c2 update assembly names
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 16:14:03 -08:00
Nikolaj Bjorner b9bec1861a copy over dotnet files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 16:08:31 -08:00
Nikolaj Bjorner bc70282a18 mute some compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 15:42:06 -08:00
Nikolaj Bjorner 9425c419ad port remaining egraph update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 15:38:05 -08:00
Nikolaj Bjorner a5a819c291 port updates to egraph from poly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 12:48:58 -08:00
Nikolaj Bjorner 24ffef8ac5 fix typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 12:26:27 -08:00
Nikolaj Bjorner e295ac93af update build-win-signed-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 11:46:11 -08:00
Nikolaj Bjorner e398f84e85 update build-win-signed-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-03 11:35:13 -08:00
Nikolaj Bjorner bd082ab653 update mk-win-dist-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 16:33:27 -08:00
Nikolaj Bjorner 14fb235dd8 update mk-win-dist-cmake
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 16:16:19 -08:00
Nikolaj Bjorner 736d6348e6 move windows builds to use mk_win_dist_cmake in nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 13:05:01 -08:00
Nikolaj Bjorner cfc8774dac move windows builds to use mk_win_dist_cmake in nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 13:04:09 -08:00
Nikolaj Bjorner 05d625bf0b fixing paths and re-add arm64
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 11:07:17 -08:00
Nikolaj Bjorner 485a018c59 add back legacy build-win-signed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 09:57:47 -08:00
Nikolaj Bjorner 9db834c223 add back legacy build-win-signed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 09:57:47 -08:00
Yisu Remy Wang 2280e9562a
Improve instructions for working with the Julia API (#7108) 2024-02-02 09:46:31 -08:00
Nikolaj Bjorner 0d24ec3613 add 'dist' to folder path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-02-02 09:45:38 -08:00