mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
16906 commits 23 branches 48 tags 156 MiB
Commit graph

16906 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Andrea Lattuada af80bd18ce
Flush the trace stream before displaying sat results (#6162) 2022-07-14 13:43:57 -07:00
Stefan Muenzel 2f5fef92b7
Cache param descrs when modifying solver params (#6156) 2022-07-14 11:11:56 -07:00
Nikolaj Bjorner 4a192850f2 add var_factors 
Add routine to partially factor polynomials. It factors out variables.
 2022-07-14 11:06:53 -07:00
Nikolaj Bjorner 981c82c814 fix initialization order 2022-07-13 18:11:18 -07:00
Nikolaj Bjorner 894fb836e2 fix build break (debug assertion) and isolate gomory functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-13 17:26:56 -07:00
Nikolaj Bjorner b253db2c0a redundant parenthesis 2022-07-13 16:20:03 -07:00
Nikolaj Bjorner dec87fe4d9 fix issue with set-logic for eval_smtlib2_string 2022-07-13 16:19:12 -07:00
Nikolaj Bjorner 1378e713ba fix #6157 2022-07-13 14:37:04 -07:00
Nikolaj Bjorner a3eb9da191 fix #6158 2022-07-13 14:33:42 -07:00
Nikolaj Bjorner 8e23af33d7 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-13 14:20:21 -07:00
Nikolaj Bjorner b81f70f6fc split nla_grobner to separate file 2022-07-13 13:05:57 -07:00
Nikolaj Bjorner 7d0c789af0 propagate has-length over map/mapi 2022-07-12 20:50:28 -07:00
Nikolaj Bjorner 8900db527f add diagnostics for grobner 2022-07-12 20:49:54 -07:00
Nikolaj Bjorner ca80d99617 fix #6153 2022-07-12 15:49:57 -07:00
Nikolaj Bjorner 43cf053066 fix #6128 2022-07-12 15:43:12 -07:00
Nikolaj Bjorner faf6c02cf8 remove --js from nightly and release doc builds as the npm run 'check-engine' fails 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-12 07:46:06 -07:00
Nikolaj Bjorner d5779bf99c handle trivial equalities in simplify_leaf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-11 21:05:26 -07:00
Nikolaj Bjorner 4dc88f0993 add --js to nightly and release scripts, nb @ritave 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-11 20:37:50 -07:00
Nikolaj Bjorner 2e797045fa remove space 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-07-11 20:33:12 -07:00
Nikolaj Bjorner 316ed778e0 Tune Grobner equations 
\brief convert p == 0 into a solved form v == r, such that
   v has bounds [lo, oo) iff r has bounds [lo', oo)
   v has bounds (oo,hi]  iff r has bounds (oo,hi']

   The solved form allows the Grobner solver identify more bounds conflicts.
   A bad leading term can miss bounds conflicts.
   For example for x + y + z == 0 where x, y : [0, oo) and z : (oo,0]
   we prefer to solve z == -x - y instead of x == -z - y
   because the solution -z - y has neither an upper, nor a lower bound.

The Grobner solver is augmented with a notion of a substitution that is applied before the solver is run.
 2022-07-11 16:14:26 -07:00
Nikolaj Bjorner f33c933241 Add substitution routine to pdd 
For Grobner we want to preserve directions of intervals for finding sign conflicts. This means that it makes sense to have external control over linear solutions.
 2022-07-11 12:10:28 -07:00
Nikolaj Bjorner 5c54d6564b fix #6143 2022-07-11 12:09:15 -07:00
Victor Paléologue 8b29f40152
Fix build on Mac (#6146) 
* Fix finding Python on Mac

On Mac you have to specify the version.
It also works well on other platforms this way.

* Ignore CMake build directories from index

* Fix warning about unused variable in release

The variable is used in debug only,
but it's legit that the compiler does not warn us for that in release.
 2022-07-11 09:46:23 -07:00
Nikolaj Bjorner 49b7e9084f Merge branch 'master' of https://github.com/z3prover/z3 2022-07-11 09:26:34 -07:00