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

16780 commits

Author SHA1 Message Date
Nikolaj Bjorner 3a8eb1e7ec increase version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 12:43:19 -07:00
Nikolaj Bjorner 1155ea69a1 add await
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 12:42:19 -07:00
Nikolaj Bjorner 212a0657a2 try .ast
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 12:34:07 -07:00
Nikolaj Bjorner 7c0ec21af8 try to add basic expression simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 12:21:25 -07:00
Nikolaj Bjorner 4368ec9953 startswith
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 11:53:07 -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 c6dad4a9ea Update release.yml for Azure Pipelines
Enable pypi publishing for 4.10 wheels
2022-07-22 10:01:49 -07:00
Bruce Mitchener 1eb2472b19
README: Fix release notes link. (#6185) 2022-07-22 09:45:07 -07:00
Nikolaj Bjorner 1e0f71c971 add way to access range bounds directly #6186
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-22 09:35:37 -07:00
Nikolaj Bjorner 87dd837b55 Merge branch 'master' of https://github.com/Z3Prover/z3 2022-07-21 23:22:37 -07:00
Nikolaj Bjorner 89af9df02d add IEnumerable for distinct
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 23:22:24 -07:00
Nikolaj Bjorner 0f9684e1f8 make fresh_eh() work for Python bindings of user-propagator 2022-07-21 21:44:02 -07:00
Nikolaj Bjorner 907dc2c2d2 adding toString() to model object
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 20:45:45 -07:00
Nikolaj Bjorner 9cd3b9cad7 Merge branch 'master' of https://github.com/z3prover/z3 2022-07-21 20:28:02 -07:00
Nikolaj Bjorner adcb3e8f86 set version number
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 20:27:50 -07:00
Nikolaj Bjorner 59d47e3055 don't publish pypi yet
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 14:43:49 -07:00
Nikolaj Bjorner efa74fe6c6 fix #6180
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 12:20:36 -07:00
Nikolaj Bjorner cf5a8fd248 fix validation code for pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-21 08:58:32 -07:00
Nikolaj Bjorner a66095bb08 fix the path to ../build/z3-built
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 22:36:34 -07:00
Nikolaj Bjorner dc9565990c did I mess up wasm paths in jest - or not?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 22:15:22 -07:00
Nikolaj Bjorner 37008226c3 did I mess up wasm paths in jest?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 22:14:21 -07:00
Nikolaj Bjorner 32c0d1f636 fix #6168 2022-07-20 21:48:47 -07:00
Nikolaj Bjorner 7f983e7d9e fix #6174
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 21:22:41 -07:00
Nikolaj Bjorner 32614722ef fix #6176
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 21:19:20 -07:00
Nikolaj Bjorner 1b83a4556b fix #6178
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 20:48:23 -07:00
Nikolaj Bjorner 5b219aab76 add mutual recursive datatypes to c++ API #6179
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-20 20:32:00 -07:00
Nikolaj Bjorner 2e13c0bf41 add API and example for one dimensional algebraic datatype #6179 2022-07-20 19:43:18 -07:00
Nikolaj Bjorner 81cb575c22 simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-19 22:58:12 -07:00
Nikolaj Bjorner 2e52029114 add command-line overwrite capability to setup.py
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-19 22:53:25 -07:00
Nikolaj Bjorner 2c8df54b70 enable fresh for python wrapper for user-propagator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-19 13:48:44 -07:00
Nikolaj Bjorner 914cfca24b updated release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-19 09:54:43 -07:00
Nikolaj Bjorner 111d27cbee remove dependency on pragma
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-19 09:36:22 -07:00
Nikolaj Bjorner dead0c9de2 reverting relative path
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-18 11:47:57 -07:00
Nikolaj Bjorner afcfc80c42 the relative path seems out of sync with how it is set up in node.ts 2022-07-18 11:21:16 -07:00
Nikolaj Bjorner 7f1893d781 add missing MkSub to NativeContext
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-18 10:21:27 -07:00
Nikolaj Bjorner 7ded856bb1 script to test jsdoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-18 09:51:34 -07:00
Nikolaj Bjorner 393c63fe0c fix #6114 2022-07-18 09:33:39 -07:00
Nikolaj Bjorner 527914db05 update documentation to use latest conventions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-17 11:49:28 -07:00
Nikolaj Bjorner b5a89eb4ab add missing generation of z3.z3 for pydoc and add some explanations to logging function declaration 2022-07-17 11:03:55 -07:00
Clemens Eisenhofer 95c3dd9224
Added missing decide-callback for tactics (#6166)
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int

* Fixed missing assignment for binary clauses

* Added missing decide-callback for tactics
2022-07-17 10:07:52 -07:00
Nuno Lopes 6e5ced0080 optimizations to api ctx ref counting 2022-07-17 11:44:35 +01:00
Nikolaj Bjorner eb2ee34dfe fix typo
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-16 16:58:57 -07:00
Nikolaj Bjorner aefd336c18 set OCaml default behaivor to enable concurrent dec ref #6160
Add Z3_enable_concurrent_dec_ref to the API.
It is enables behavior of dec_ref functions that are exposed over the API to work with concurrent GC. The API calls to dec_ref are queued and processed in the main thread where context operations take place (in a way that is assumed thread safe as context operations are only allowed to be serialized on one thread at a time).
2022-07-16 16:49:39 -07:00
Nikolaj Bjorner 6c5747a80e guard against lemmas that are already true
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-15 10:03:31 -07:00
Nikolaj Bjorner 4ecb61aeaa neatify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-07-15 09:53:56 -07:00
Nikolaj Bjorner b743e210f8 give java dynamic lib a chance for extra flags for #5848 2022-07-15 08:44:05 -07:00
Nikolaj Bjorner 2696775088 remove stale assertion
with support for substitutions we allow the simplifier to change the state of equations.
2022-07-15 04:03:25 -07:00
Nikolaj Bjorner 6688c1d62a prepare for #6160
The idea is to set _concurrent_dec_ref from the API
(function not yet provided externally, but you can experiment with it by setting the default of m_concurrent_dec_ref to true).
It then provides concurrency support for dec_ref operations.
2022-07-15 03:53:15 -07:00
Nikolaj Bjorner b29cdca936 integrate factorization to Grobner 2022-07-14 21:24:27 -07:00
Nikolaj Bjorner 7c177584f3 add propagators to grobner 2022-07-14 15:45:07 -07:00