mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity
12956 commits 23 branches 48 tags 157 MiB
Commit graph

12956 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 894702d600 fix #3301 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 14:42:24 -07:00
Nikolaj Bjorner 42dbee9165 fix #3302 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 14:39:03 -07:00
Nikolaj Bjorner ec0349819f fix #3298 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 12:15:05 -07:00
Nikolaj Bjorner 47bd06338e fix #3283 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:54:24 -07:00
Nikolaj Bjorner 6b319f9ac3 fix #3297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:49:05 -07:00
Nikolaj Bjorner 974541e244 fix #3299 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:44:25 -07:00
Nikolaj Bjorner c613ab0ba0 fix #3286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 11:42:26 -07:00
Nikolaj Bjorner 9f6a0a0a48 fix #3289, recent regression introduced when dealing with push on inconsistent state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:50:41 -07:00
Nikolaj Bjorner 51e459d02b fix #3294 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 10:46:03 -07:00
Nikolaj Bjorner b29c77dc87 fix #3295 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-14 09:51:18 -07:00
Nikolaj Bjorner 6f2b5696d5 fix #3279 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 17:08:20 -07:00
Nikolaj Bjorner 31c3ac016a fix #3275 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 13:55:12 -07:00
Nikolaj Bjorner 59755dd72e fix #3260 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 11:42:25 -07:00
Nikolaj Bjorner d530d1314b fix #3276 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 11:20:12 -07:00
Nikolaj Bjorner 825fbf1832 fix #3268 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-13 10:49:39 -07:00
Nikolaj Bjorner a6fcdecfd7 Add accessor for lower/upper bounds of algebraic numerals #3245 
The pretty printer for algebraic numerals prints a polynomial root expression, however, polynomial root expressions are not exposed over the API. The C API contains methods for approximating root objects from above and below with arbitrary precision. These functions are now exposed over the C++ API.
Note that algebraic numbers are also disjoint from rcf (real closed field) objects.
Thus, z3 doesn't support adding "pi" as an extension field to algebraic numbers that are used by the nlsat solver. It operats on algebraic numbers formed by roots over polynomial with rational coefficients
 2020-03-12 14:23:45 -07:00
Nikolaj Bjorner 356a9bb9ed fix #3255 
The model is fine, but debug facility that checks the model reports a false positive.
It exposed some further opportunities for simplification
 2020-03-12 10:57:35 -07:00
Nikolaj Bjorner 7a80fe20ca fix #3242 2020-03-12 10:41:08 -07:00
Nikolaj Bjorner 1796fc32f5 breaking change to fix #3062 #3147 #2896 #2937 #3105 
This moves handling of contains into an axiomatization that unfolds on demand.
The previous handling, based on rewriting, proved too brittle. While it simplifies how contains is handled, it is likely to introduce regressions in terms of what constraints can now be handled.
 2020-03-12 10:16:48 -07:00
Nikolaj Bjorner 0a97f37be5 fix #3284 (and other recent regressions) 2020-03-12 08:37:43 -07:00
Nikolaj Bjorner 4e9005ac3d fix #3241 2020-03-12 07:55:16 -07:00
Nikolaj Bjorner 67d19cba4a fix #3105 fix #2937 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 14:13:12 -07:00
Nikolaj Bjorner d9c09dcdf9 disable extra model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 11:46:54 -07:00
Nikolaj Bjorner 36cddd0c46 fix #3235 - return early during lookaehad, avoid checking invariant when context is inconsistent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 10:55:56 -07:00
Nikolaj Bjorner 59acd1093d fix #3236 - fix also max conflict overwrite for incremental mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 10:13:20 -07:00
Nikolaj Bjorner c49d0c5033 fix #3236 relax restriction on nnf-cnf pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 10:04:15 -07:00
Nikolaj Bjorner e45871d7c5 fix #3239 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 09:35:28 -07:00
Nikolaj Bjorner e32020ba10 fix #3228 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-11 08:32:25 -07:00
Nikolaj Bjorner 7bcd3452b8 reduce invertible update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 21:02:54 -07:00
Nikolaj Bjorner 13883de389 fix #3177 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 20:13:25 -07:00
Nikolaj Bjorner f946fc516c copy usorts as well 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 19:18:59 -07:00
Nikolaj Bjorner 2d0d527fe1 preserve model order to avoid clobbering regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:56:49 -07:00
Nikolaj Bjorner 04a19cd1d8 fix #3219 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:21:01 -07:00
Nikolaj Bjorner 0768701744 fix #3220 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:08:16 -07:00
Nikolaj Bjorner 1bc6c6a2a5 fix #3221 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:04:35 -07:00
Nikolaj Bjorner 427358d0a1 fix #3233 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 15:59:20 -07:00
Nikolaj Bjorner 3dad24ace0 fix #3225 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 15:11:24 -07:00
Nikolaj Bjorner 99784a92ef fix #3225 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 15:10:18 -07:00
Nikolaj Bjorner dd4eb7f97c fix #3230 fix #3231 - make rmodel converter additive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 14:08:57 -07:00
Nikolaj Bjorner b3d41163f3 remove spurious print to stdout in check-lemmas #3232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 13:17:44 -07:00
Nikolaj Bjorner 89b5b3e69f fix #3223 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 13:15:02 -07:00
Nikolaj Bjorner c4c235e9d7 fix #3224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 12:52:49 -07:00
Nikolaj Bjorner a09ed766f5 fix #3226 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 11:41:41 -07:00
Nikolaj Bjorner 9e41e88392 delay-initialize solver to avoid conflicts with global parameters #3076 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 11:34:49 -07:00
Nikolaj Bjorner bed2097fc4 fix #3076 - need to apply relevancy propagation in mk_bits. Assume bv v is already relevant but did not have bits associated with it, the bits need to then be marked as relevant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 10:36:00 -07:00
ahumenberger df1b308dd0
Julia bindings (#3228) 
* First steps toward adding Julia bindings

* Simplifications

* Streamlining

* Friends of tactic and probe

* Add missing functions

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Update azure-pipelines.yml for Azure Pipelines

* Changes for CxxWrap v0.9.0

* Wrap enumeration and tuple sort

* Wrap z3::fixedpoint

* Wrap z3::optimize

* Wrap missing functions

* Fix aux types

* Add some missing functions

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 5aab9f9240.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit cfccd7ca2c.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit f24740c595.

* Revert "Update azure-pipelines.yml for Azure Pipelines"

This reverts commit 592499eaa0.

* Checkout current version of pipeline

* Build Julia bindings on macOS
 2020-03-10 09:16:34 -07:00
Nikolaj Bjorner a51d65d58a fix #3118 (without breaking #3101, #3111) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 21:20:27 +01:00
Nikolaj Bjorner f7747d9e76 fix parameter collection for tactic-based solvers reported in #3065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 19:59:26 +01:00
Nikolaj Bjorner c7a6721bf1 lessen depth expansin in nnf, add cancelation, add ast_marking to avoid repeated sub-expressions #3065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 19:50:43 +01:00
Nikolaj Bjorner 8beb6618d3 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 17:51:33 +01:00