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

1702 commits

Author SHA1 Message Date
Nikolaj Bjorner 7def610a69 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:31:11 -07:00
Nikolaj Bjorner 14214c5a07 exposing user propagators over .Net 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-07 11:08:40 -07:00
Nikolaj Bjorner 367bfedab0 add min/max diff in final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 07:39:38 -07:00
Nikolaj Bjorner c29cfa81ae prep for max/min diff 2022-05-04 02:08:11 -07:00
Nikolaj Bjorner 81d97a81af enable nested ADT and sequences 
add API to define forward reference to recursively defined datatype.
The forward reference should be used only when passed to constructor declarations that are used in a datatype definition (Z3_mk_datatypes). The call to Z3_mk_datatypes ensures that the forward reference can be resolved with respect to constructors.
 2022-04-27 09:58:38 +01:00
Nikolaj Bjorner 8e2f09b517 #5778 - ensure arrays used inside of extensionality function are treated as shared 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-25 17:17:59 +01:00
Nikolaj Bjorner 0a665b0fa0 #5778 2022-04-25 14:27:38 +01:00
Nikolaj Bjorner 489459a1f7 #5778 
reprogram flush, mark clauses during reinit as non-redundant.
 2022-04-25 11:22:00 +01:00
Nikolaj Bjorner 24baf56e27 fix missing propagation on final 2022-04-24 16:29:25 +01:00
Nikolaj Bjorner ec57d3b15c missing switch cases 2022-04-19 16:20:02 +01:00
Nikolaj Bjorner 3cc9d7f443 improve pre-processing 2022-04-15 12:55:26 +02:00
Nikolaj Bjorner a634876180 sort muxes 2022-04-15 12:55:26 +02:00
Nikolaj Bjorner eb2dd92d37 Merge branch 'master' of https://github.com/z3prover/z3 2022-04-11 17:06:03 +02:00
Nikolaj Bjorner c996a66da0 separate pre-processing, add callback parameter to push/pop in python API 2022-04-11 17:05:59 +02:00
Clemens Eisenhofer b0d8b27f37
Fixed registering expressions in push/pop (#5964) 
* Fixed registering expressions in push/pop

* Reused existing function
 2022-04-11 16:50:13 +02:00
Nikolaj Bjorner f55b233228 #5778 2022-04-09 12:06:39 +02:00
Nikolaj Bjorner 405a26c585 allow adding constraints during on_model 2022-04-09 09:55:02 +02:00
Nikolaj Bjorner b0dce5b27d remove debug asserts 2022-04-06 08:53:12 +02:00
Nikolaj Bjorner 2f63747c7b #5778 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 08:17:27 +02:00
Nikolaj Bjorner cebbc71330 #5778 ensure else value so that defaults align across equivalence class 2022-04-06 07:58:32 +02:00
Nikolaj Bjorner ef28f0e2f0 #5778 
deal with recursive calls to internalization with the same formula
 2022-04-02 01:28:58 -07:00
Nikolaj Bjorner 2fedcbd41e #5778 2022-04-02 01:27:56 -07:00
Nikolaj Bjorner 229ea569f1 #5778 2022-04-02 00:56:51 -07:00
Nikolaj Bjorner 97115e5ebd #5778 
add new clauses created during propagation to use-list
 2022-04-02 00:14:59 -07:00
Nikolaj Bjorner 4cc33277fa #5778 2022-04-01 14:27:40 -07:00
Nikolaj Bjorner c7922d69ac #5778 2022-04-01 14:17:45 -07:00
Nikolaj Bjorner 81084b8232 #5778 #5937 2022-04-01 13:07:17 -07:00
Nikolaj Bjorner 4b1419261f #5778 2022-03-21 16:23:43 -07:00
Nikolaj Bjorner 20bd59bb20 #5778 - missed tracking literal assignment justification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-21 10:15:00 -07:00
Nikolaj Bjorner 6d836e7e2f expose model update 2022-03-19 09:23:08 -07:00
Nikolaj Bjorner 580012e19f fix #5894 
expp is not implemented. This is the second time a fuzz bug reports it. Instead of closing the bug, just disable code path as fuzzers are not considering the comment from previous bug.
 2022-03-10 09:45:09 -08:00
Nikolaj Bjorner 1d224d1bcd na 2022-03-08 08:51:00 -08:00
Nikolaj Bjorner c6f8ee33d4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-08 08:36:19 -08:00
Nikolaj Bjorner 3293aeb7c7 na 2022-03-08 08:36:19 -08:00
Nikolaj Bjorner 7b4f1ed530 missing initialization of m_user_propagator, disable unsound in-processing in pb_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-23 04:49:42 -08:00
Nikolaj Bjorner 10b611b3ba fix #5850 2022-02-20 10:30:52 +02:00
Nikolaj Bjorner 2e00f2f32d
Propagator (#5845) 
* user propagator without ids

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* user propagator without ids

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix signature

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* references #5818

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix c++ build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch to vs 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update propagator example (I) (#5835)

* fix #5829

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* switch to vs 2022

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Adapted the example to the changes in the propagator

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* context goes out of scope in stack allocation, so can't used scoped context when passing objects around

* parameter check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add rewriter

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Fixed bug in user-propagator "created" (#5843)

Co-authored-by: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
 2022-02-17 09:21:41 +02:00
Qix 9cf50766a6
fix compiler warnings under clang (#5839) 2022-02-16 23:36:34 +02:00
Nikolaj Bjorner 1e0d49512b call mux finder 2022-01-31 12:00:16 -08:00
Nikolaj Bjorner 4392b88718 return negated literal when expression is "not" 2022-01-31 12:00:00 -08:00
Nikolaj Bjorner 7ddfc54250 shortcut negation 2022-01-31 11:58:02 -08:00
Nikolaj Bjorner 6422b783b2 fix mux extraction to check for top-level assertion 2022-01-31 11:57:16 -08:00
Nikolaj Bjorner 62bb234251 expose extract roots as separate 2022-01-31 11:56:44 -08:00
Nikolaj Bjorner 9e5b6e0c9c #5778 2022-01-27 12:12:58 -08:00
Nikolaj Bjorner 9969809745 #5778 2022-01-21 09:40:06 +01:00
Nikolaj Bjorner a3d4e9a4e8 adding created to sat/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 11:48:27 +01:00
Nikolaj Bjorner c00591daaf finish is-fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 16:28:34 +01:00
Nikolaj Bjorner e5767bf2b8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 15:19:07 +01:00
Nikolaj Bjorner 06feb71eb1 fix bug in root setting exposed by incremental mode pb_solver 2022-01-18 10:55:27 +01:00
Nikolaj Bjorner d777306bb6 #5778 2022-01-17 10:43:15 -08:00