3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Commit graph

1613 commits

Author SHA1 Message Date
Nikolaj Bjorner f928b44606 update version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-12 14:53:52 -07:00
Nikolaj Bjorner e417f7d785 updated release notes for 12.2
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-12 12:59:04 -07:00
Nikolaj Bjorner ba911009e4 disable publish
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-05-11 16:54:40 -07:00
Nikolaj Bjorner 6aaaa3b015 fix #6660
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-03-31 09:58:28 -07:00
Kevin Phoenix 1a9990a92f
Use sys.getdefaultencoding() instead of sys.stdout.encoding (#6612) 2023-02-28 11:46:10 -08:00
Nikolaj Bjorner a150e58893 update release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-02-07 09:21:02 -08:00
Nikolaj Bjorner f3ae7692ca update stage name 2023-02-06 16:08:14 -08:00
Nikolaj Bjorner c1cadd37cc update stage name 2023-02-06 16:07:12 -08:00
Nikolaj Bjorner a7231027c3 try side-by-side nightly 2023-02-06 16:04:54 -08:00
Nikolaj Bjorner 992793bd56 update nuget packaging targets #6570 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner 550619bfcf add API for creating and attaching simplifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 17:06:03 -08:00
Nikolaj Bjorner d263b373ed update release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-31 12:19:33 -08:00
Nikolaj Bjorner 6022c17131 Add simplification customization for SMTLIB2
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
2023-01-30 22:38:51 -08:00
Nikolaj Bjorner dd0decfe5d create simplifier_solver wrapper to supply simplifier layer
move sat_smt_preprocess to solver
fix bugs in model_reconstruction_trail for dependency replay

This is a preparatory step for exposing pre-processing as tactics.
2023-01-30 16:12:25 -08:00
Nikolaj Bjorner 83bd3d1e21 fix mk-project file for python build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-27 18:04:58 -08:00
Nikolaj Bjorner 3b5ae285d9 add outline for interval reasoning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-22 23:28:36 -08:00
Nikolaj Bjorner 59c41bd8ce increment release version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-18 07:59:47 -08:00
Nikolaj Bjorner 3012293c35 update release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-17 19:10:26 -08:00
Nikolaj Bjorner 7368f9f7d3 increase build version, better propagation in euf-egraph, handle assumptions in sat.smt
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
2023-01-17 14:07:07 -08:00
Nikolaj Bjorner c8f197d0ca specify macos-11 in nightly to force os11 build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-16 16:30:46 -05:00
Nikolaj Bjorner feda706d0d Update release.yml for Azure Pipelines 2023-01-14 06:24:26 -08:00
Nikolaj Bjorner 5dbd0bb658 add sign
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 23:33:39 -08:00
Nikolaj Bjorner 54524de784 Update release.yml for Azure Pipelines 2023-01-13 17:10:36 -08:00
Nikolaj Bjorner c33b1e3082 fixup manylinux reference in release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:27:58 -08:00
Nikolaj Bjorner 234ff28d18 prepare release script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:15:27 -08:00
Nikolaj Bjorner 60fef928cc missing code signing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 16:12:48 -08:00
Nikolaj Bjorner 42fbf23a8f update code signing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-13 14:01:18 -08:00
Nikolaj Bjorner d204413f2a remove update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-12 17:54:42 -08:00
Nikolaj Bjorner 85abbb8188 include apt-get update for doc build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2023-01-12 16:58:42 -08:00
Nikolaj Bjorner e4bd406675 update version of manylinux 2023-01-12 16:27:33 -08:00
Nikolaj Bjorner 1974c224ab add demodulator simplifier
refactor demodulator-rewriter a bit to separate reusable features.
2022-12-04 09:39:28 -08:00
Nikolaj Bjorner 847aec1d30 update dependencies 2022-11-30 22:48:10 -08:00
Nikolaj Bjorner 7b9dfb8e1e update dependencies for python build 2022-11-30 13:43:40 +07:00
Nikolaj Bjorner 4e9f21c2a1 add rewriter and seq simplifiers 2022-11-25 15:16:14 +07:00
Nikolaj Bjorner 203652da74 add converters module to python build 2022-11-03 05:26:06 -07:00
Nikolaj Bjorner e57674490f adding simplifiers layer
simplifiers layer is a common substrate for global non-incremental and incremental processing.
The first two layers are new, but others are to be ported form tactics.

- bv::slice - rewrites equations to cut-dice-slice bit-vector extractions until they align. It creates opportunities for rewriting portions of bit-vectors to common sub-expressions, including values.
- euf::completion - generalizes the KB simplifcation from asserted formulas to use the E-graph to establish a global and order-independent canonization.

The interface dependent_expr_simplifier is amenable to forming tactics. Plugins for asserted-formulas is also possible but not yet realized.
2022-11-02 08:51:30 -07:00
Nikolaj Bjorner a90c4f65cf increment version per release notes
incrementing minor version because the API has a new function.
This breaks log replay against old dlls and inclusion against z3++.h.
2022-10-19 13:21:26 -07:00
Nikolaj Bjorner 07dd1065db added API to monitor clause inferences
See RELEASE_NOTES for more information
examples pending.
2022-10-19 08:34:55 -07:00
Nikolaj Bjorner ea55f69a92 fix python build 2022-10-16 23:42:11 +02:00
Nikolaj Bjorner 6eb2d2acfa update dependencies for build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-28 11:25:36 -07:00
Nikolaj Bjorner ff679e0fce increment version number 2022-09-11 19:02:44 -07:00
Thomas Pani adf6e98cdf
Handle _out(STRING) parameters in Java API (#6325) 2022-09-06 15:29:12 -07:00
Nikolaj Bjorner 8e6f17ebd0 inc version
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-09-03 15:47:12 -07:00
John Fleisher f72cdda5fb
Change to 4 digit assembly version (#6297)
* WiP: test build specific version number

* update mk_win_dist for assembly-version

* Add print statements for version

* remove stray semicolon

* undo quote change in projectstr

* nit fixes

* revert print formatting for Mac build

* fix spaces
2022-08-31 06:46:06 -07:00
Nikolaj Bjorner 4d29925c3f build fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-28 18:43:50 -07:00
Nikolaj Bjorner ce1f3987d9 fix unsoundness in quantifier propagation #6116 and add initial lemma logging 2022-08-23 19:10:01 -07:00
Nuno Lopes d5d77dfe64 minor code simplifications 2022-08-20 12:56:45 +01:00
Nikolaj Bjorner 514eaf33aa Merge branch 'master' of https://github.com/z3prover/z3 2022-08-18 19:07:55 -07:00
Nikolaj Bjorner 600b4491aa don't forget parameter documentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-18 19:07:39 -07:00
Nikolaj Bjorner 540e36e6cb roll version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-18 15:47:08 -07:00