mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-19 07:09:03 +00:00
Code Activity
20014 commits 23 branches 48 tags 157 MiB
Commit graph

238 commits

Author SHA1 Message Date
Jakob Rath cd50f2ea88 Merge remote-tracking branch 'origin/master' into polysat 2023-12-07 16:00:15 +01:00
Nikolaj Bjorner 6afed0819c update minor version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-06 07:13:07 -08:00
Nikolaj Bjorner 389aea3330 update release notes, update version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-04 19:48:43 -08:00
Jakob Rath 661bea91de fix component dependencies 2023-07-10 09:45:21 +02:00
Jakob Rath f54f33551e Merge branch 'master' into polysat 2023-05-26 15:58:09 +02:00
Nikolaj Bjorner f928b44606 update version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-05-12 14:53:52 -07:00
Jakob Rath 20b5455d08 Merge branch 'master' into polysat 2023-02-01 16:28:57 +01: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 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 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 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
Jakob Rath 1df749ad33 Merge branch 'master' into polysat 2022-09-23 17:14:26 +02:00
Jakob Rath 2f65ce1026 try to fix build 2022-09-21 14:03:07 +02:00
Nikolaj Bjorner ff679e0fce increment version number 2022-09-11 19:02:44 -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
Nikolaj Bjorner 540e36e6cb roll version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-18 15:47:08 -07:00
Nikolaj Bjorner 78eaefe5a8 move solver-params to params 2022-08-08 11:34:41 +03:00
Jakob Rath 220a63e8bd Merge branch 'master' into polysat 2022-08-01 11:27:49 +02:00
Nikolaj Bjorner a6fe260354 update minor versin number to ABI change to remove Z3_bool from z3_api.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-30 06:31:22 +02:00
Nikolaj Bjorner 591d485358 update versions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-30 05:26:43 +02:00
Nikolaj Bjorner 3a8eb1e7ec increase version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-22 12:43:19 -07:00
Nikolaj Bjorner 845e852dba increment to include python fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-22 11:44:32 -07:00
Nikolaj Bjorner adcb3e8f86 set version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-21 20:27:50 -07:00
Jakob Rath e168d8a2eb Merge branch 'master' into polysat 2022-07-21 12:56:50 +02:00
Nikolaj Bjorner 9d9414c111 inc version number 2022-07-06 14:00:40 -07:00
Nikolaj Bjorner cc841caf08 increment minor version for dev branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-06 10:15:34 -07:00
Nikolaj Bjorner 282c786f1c setting version to release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-05 11:51:12 -07:00
Jakob Rath e5e79c1d4b Merge branch 'master' into polysat 2022-07-01 16:11:17 +02:00
Nikolaj Bjorner 3ae781039b inc version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-05 07:09:54 -07:00
Nikolaj Bjorner 33ffd464cf inc version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-24 12:17:07 +01:00
Nikolaj Bjorner 3533bf486f merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-16 18:30:03 +02:00
Nikolaj Bjorner a418678cd4 increment version number 2022-03-20 14:34:34 -07:00
Nikolaj Bjorner 0895ce8723 update mk_project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 21:44:56 +01:00
Nikolaj Bjorner 3f5df04dc4 prepare polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 06:19:24 +01:00
Nikolaj Bjorner b259f46f85 dependencies 2022-01-13 12:34:58 -08:00
Nikolaj Bjorner 08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner ecf41972b1 increase minor version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-23 14:41:52 -08:00