mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
16625 commits 24 branches 48 tags 158 MiB
Commit graph

3918 commits

Author SHA1 Message Date
Nikolaj Bjorner
30165ed40a fix #6105 
non-linear division axioms appear incomplete.
Fixed for legacy arithmetic. Fix pending for new arithmetic solver.
 2022-06-26 20:37:18 -07:00
Nikolaj Bjorner
56aa4261b6 fix #6082 2022-06-23 07:43:06 -07:00
Clemens Eisenhofer
2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096) 
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
 2022-06-19 10:49:25 -07: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
Nuno Lopes
70bcf0b51d reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields 
Yes, those 8 bytes are yours now, use responsibly.
 2022-06-17 12:07:15 +01:00
Nikolaj Bjorner
99b606b861 add logging 2022-06-16 15:40:00 -07:00
Nikolaj Bjorner
637120ced5 Treat arguments to recursive functions as beta redexes 
An argument to a recursive function would escape the scope of the function application when the recursive function definitions are unfolded. Therefore, such argument occurrences need not be considered for extensional equality / equality sharing.

This filter is mostly relevant for recursive functions that take a lambda expression as argument. Lambda expressions / arrays that occur in shared occurrences are checked for extensionality.
 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner
04f94d818f fix #6091 2022-06-14 09:51:06 -07:00
Nikolaj Bjorner
8efa3c8ade introduce notion of beta redex to deal with lambdas in non-extensional positions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 17:35:01 -07:00
Nikolaj Bjorner
b9b5377c69 add a way to supress lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 14:37:25 -07:00
Nikolaj Bjorner
5db133f875 add a way to supress lambdas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-10 14:35:20 -07:00
Nikolaj Bjorner
6a1193eebd reorg if-then-else structure 2022-06-08 10:00:45 -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
a9d70fca1a fix #6061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-31 19:09:10 -07:00
Nikolaj Bjorner
ca2497eecb na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-15 12:00:41 -07:00
Nikolaj Bjorner
7497856ded add ignore int to new arithmetic solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-11 15:14:22 -07:00
Nikolaj Bjorner
54648f6b50 add stats for binary clause creation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-10 14:58:15 -07:00
Nikolaj Bjorner
7def610a69 build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-08 10:31:11 -07:00
JohnLyu2
5a9b0dd747
Z3str3 Debug (#6000) 
* z3str3 debug

* add comments of reference to bugs in the report

Co-authored-by: John Lu <z52lu@uwaterloo.ca>
 2022-04-27 12:37:07 +02: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
Clemens Eisenhofer
81189d6fdd
Added bit2bool to the API (#5992) 
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate

* Added decide-callback to user-propagator

* Refactoring

* Fixed index

* Added bit2bool to the API
Fixed bug in user-propagator's decide callback

* Fixed typo
 2022-04-22 09:54:21 +01:00
Nikolaj Bjorner
a1ead5f47d #5986 
add memory limit check to internalize
 2022-04-19 07:31:40 +02:00
Nikolaj Bjorner
f4c500c519 fix build 
reference types are not part of C
 2022-04-16 15:16:53 +02:00
Nikolaj Bjorner
807121aa03 wip 2022-04-16 14:55:43 +02:00
Clemens Eisenhofer
e11496bc65
Added decide-callback to user-propagator (#5978) 
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate

* Added decide-callback to user-propagator

* Refactoring

* Fixed index
 2022-04-15 20:07:17 +02:00
Nikolaj Bjorner
3cc9d7f443 improve pre-processing 2022-04-15 12:55:26 +02:00
Clemens Eisenhofer
b264e6c290
Reverted reusing can_propagate (#5966) 
* Fixed registering expressions in push/pop

* Reused existing function

* Reverted reusing can_propagate
 2022-04-12 12:29:53 +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
0fa0feb979 allow add_expr during pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-06 16:27:10 +02:00
Nikolaj Bjorner
03a2d9a018 fix #5942 2022-04-03 11:03:28 -07:00
Nikolaj Bjorner
81084b8232 #5778 #5937 2022-04-01 13:07:17 -07:00
Nikolaj Bjorner
dd27f7e937 #5935 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-30 17:47:48 -10:00
Clemens Eisenhofer
7bb969ab52
Fixed problem with registering bitvector functions (#5923) 2022-03-26 16:36:15 -10: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
Nikolaj Bjorner
b4873d226c fix #5907 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-20 11:40:19 -07:00
Nikolaj Bjorner
dfa65443e9 fix name for artifact 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-03-19 13:51:58 -07:00
Nikolaj Bjorner
964e513353 re-add bv_eq_axioms, fix #5842 2022-03-19 12:37:01 -07:00
Nikolaj Bjorner
545341e699 fix #5895 2022-03-12 09:17:13 -08: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
Nuno Lopes
43f7636826 remove some copies/moves 2022-03-09 12:46:41 +00:00
Nikolaj Bjorner
deaad86d6a nit 2022-03-01 12:11:10 -08:00
Clemens Eisenhofer
412b05076c
User-functions fix (#5868) 2022-02-26 09:21:01 -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
6af170b058 fix #5861 
sigh
 2022-02-22 11:26:09 -08:00
Nikolaj Bjorner
b843618051 fix #5798 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 13:54:15 -08:00
Nikolaj Bjorner
1e463955c2 #4889 avoid double internalize of bvle 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-20 09:09:28 -08: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
6202cd5394 fix #5842 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-02-16 17:38:19 +02:00