mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 06:15:37 +00:00
Code Activity
18852 commits 23 branches 48 tags 157 MiB
Commit graph

286 commits

Author SHA1 Message Date
Nikolaj Bjorner 9a87bb1097 #7362 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-30 14:30:14 -07:00
Nikolaj Bjorner af1f0e3184 fix #7268 2024-07-08 14:50:38 -07:00
Nikolaj Bjorner 8e482df62a fix #7264 2024-06-21 08:37:23 -07:00
Nikolaj Bjorner 908aaa06f7 fix #7101 2024-01-29 12:26:51 -08:00
Nikolaj Bjorner f8a3b6f521 fix #7102 2024-01-27 17:05:55 -08:00
Nuno Lopes b2d5c24c1d remove a few string copies 2023-12-20 16:55:09 +00:00
Nikolaj Bjorner 9efe6f6afa fix regression in fix for #7006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 14:54:54 -08:00
Nikolaj Bjorner 79bbbf76d0 fix #7006 2023-11-28 15:06:27 -08:00
Nikolaj Bjorner 267e9e827d #6935 2023-10-10 15:52:54 +09:00
Nikolaj Bjorner 09f911d8a8 include rewriter for recursive functions in model-evaluator 
fixes bug reported by Tahina and Nick, @tahina-pro
 2023-08-28 11:31:40 -07:00
Nikolaj Bjorner c6aab89662 add rewrite for partially interpreted arithmetic functions 2023-07-25 14:57:27 -07:00
Nikolaj Bjorner c64d61bd0a formatting updates 2023-05-02 12:17:32 -07:00
Nikolaj Bjorner 392266c278 fix processing of else expression for model table 2023-05-02 12:16:58 -07:00
Nikolaj Bjorner 444238bc53 formatting updates 2023-04-12 19:40:31 -07:00
Nikolaj Bjorner a9e6e567b0 make generation of "some" Boolean value fair 2023-03-20 17:07:04 +01:00
Nikolaj Bjorner 42076a3c13 bug fixes to new core, elim_predicates and elim_unconstrained 2023-03-05 22:26:37 -08:00
Nikolaj Bjorner 1fae3aa152 rename set-flat to set-flat-and-or to allow to differentiate parameters 2022-10-27 11:22:57 -07:00
Nikolaj Bjorner ac1552d194 wip - updates to proof logging and self-checking 
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line.

when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation.

new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation.

z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
 2022-10-16 23:33:30 +02:00
Nikolaj Bjorner bd4db4c41f add option to rewrite and for arithmetic simplification 2022-09-18 17:22:59 -07:00
Nikolaj Bjorner eb1ea9482e detect nested as-array in model values 2022-09-01 23:26:38 -07:00
Nikolaj Bjorner 6f2a6da600 address unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-08-28 18:50:54 -07:00
Nikolaj Bjorner 64e0e785e7 #5953 2022-08-21 18:28:07 -07:00
Bruce Mitchener 5014b1a34d Use = default for virtual constructors. 2022-08-05 18:11:46 +03:00
Bruce Mitchener 1d9345c3de Fix typos. 2022-08-05 07:40:50 +03:00
Bruce Mitchener 5d0dea05aa
Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
Nuno Lopes 73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Nikolaj Bjorner 8e2027107d fix spacing 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner 51ed13f96a update topological sort to use arrays instead of hash tables, expose Context over Z3Object for programmability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-08 06:28:24 -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 81084b8232 #5778 #5937 2022-04-01 13:07:17 -07:00
Nikolaj Bjorner 28e94583da break self recursion #5937 2022-03-31 21:49:08 -07:00
Nikolaj Bjorner 32233e1bf1 set default to true to avoid regression failures 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-23 12:20:53 -07:00
Nikolaj Bjorner 365b8f3281 change default to _not_ include auxiliary functions in model as this seems to break fewer' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-23 09:51:06 -07:00
Nikolaj Bjorner d790523c59 #5917 
Add model.user_functions (default true) to control whether user functions are added to the model.
 2022-03-23 09:49:44 -07:00
Nuno Lopes 43f7636826 remove some copies/moves 2022-03-09 12:46:41 +00:00
Nikolaj Bjorner 5672f5cc34 fix #5733 2022-01-01 16:40:48 -08:00
Henrich Lauko 96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Alexander Traud d1592c6abf
fix misspelled \brief for doxygen (#5632) 2021-10-29 15:34:28 +02:00
Nikolaj Bjorner 4dad414161 fix performance regression after adding user declared functions to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-28 05:49:15 +02:00
Nikolaj Bjorner bc2020a39b #5604 
retain array interpretation when available
 2021-10-17 20:24:26 -07:00
Nikolaj Bjorner 1fc7b63a80 ... 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 21:59:54 +01:00
Nikolaj Bjorner fe3f139eb2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 16:25:43 +01:00
Nikolaj Bjorner c3c5c14ead prepare for min/max i 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 16:23:10 +01:00
Nikolaj Bjorner be4df46f6f #5532 remove unsound rewrite rule that was recently added 2021-09-07 06:42:24 +02:00
Nikolaj Bjorner 72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
Nikolaj Bjorner 976c0a391c revisit as-array evaluation 2021-09-04 18:00:36 -07:00
Nikolaj Bjorner 8f306c6a8f handle constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 11:59:41 -07:00
Nikolaj Bjorner 09696e989e add missing lambda defs per #5509 
the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
 2021-08-27 11:57:26 -07:00
Nikolaj Bjorner 1db9f9a3b5 try vscode from github integration 2021-08-18 11:02:02 -07:00
Nikolaj Bjorner 800fef6653 fix #5424 2021-07-22 18:31:37 -07:00