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

14132 commits

Author SHA1 Message Date
Nikolaj Bjorner
02d6f6a613 fix build for Z3_mk_datatype_sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-27 10:01:51 +01: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
Kevin Gibbons
dc18b47967
automatically release wasm build (#5997) 2022-04-24 18:06:36 +01:00
Nikolaj Bjorner
24baf56e27 fix missing propagation on final 2022-04-24 16:29:25 +01:00
Kevin Gibbons
312e037458
wasm build: disable error handler (#5996) 
* wasm: set error handler to no-op

* wasm: better wrapper for use in html
 2022-04-24 11:04:08 +01:00
Victor
bd6b3027cd
Document gotcha with z3-js (#5994) 2022-04-23 19:52:35 +01:00
Nikolaj Bjorner
459cfc8eb4 fix #5993 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-23 19:33:55 +01:00
Nikolaj Bjorner
5a2c92f4af format 2022-04-22 17:25:37 +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
0dd0fd26d4 remove buggy prototype 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-21 10:44:49 +01:00
Nikolaj Bjorner
d9f3625f93 change default output to print objective value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-20 17:11:46 +01:00
Nikolaj Bjorner
e3c35840bb remove out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-20 11:26:16 +01:00
Nikolaj Bjorner
ec57d3b15c missing switch cases 2022-04-19 16:20:02 +01:00
Nikolaj Bjorner
5393f1d98f #5980 2022-04-19 11:10:37 +01:00
Nikolaj Bjorner
a180254c1a fix #5980 2022-04-19 11:10:20 +01:00
Nikolaj Bjorner
b7169e2a41 fix #5985 2022-04-19 07:54:55 +02:00
Nikolaj Bjorner
a1ead5f47d #5986 
add memory limit check to internalize
 2022-04-19 07:31:40 +02:00
Nikolaj Bjorner
9b66d8600b add shortcut to serialize/deserialize based on question at FV hangout 
use case
```
from z3 import *

x, y = Ints('x y')
s = (x + y).serialize()

y = deserialize(s)

print(y)
```
 2022-04-19 07:21:22 +02:00
Nikolaj Bjorner
09b0c4bc9d fix #5988 2022-04-19 07:17:24 +02:00
Nikolaj Bjorner
df981666fd na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-18 16:27:46 +02:00
Nikolaj Bjorner
98c7069f75 add rewrite for hoisting multipliers over modular inverses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-18 14:29:16 +02:00
Nikolaj Bjorner
c727e2d048 add rc2 option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-18 10:31:56 +02:00
Nikolaj Bjorner
4a59ae41b3 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-16 19:19:05 +02:00
Nikolaj Bjorner
7496f11542 na 2022-04-16 18:30:35 +02:00
Nikolaj Bjorner
b5309d5fd0 na 2022-04-16 16:42:57 +02:00
Nikolaj Bjorner
c131eb4db1 build fix 2022-04-16 16:42:45 +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
Nikolaj Bjorner
8e70112832 Update z3.py 
allow ading funcinterp to models
 2022-04-15 23:31:15 +02:00
Simon Cruanes
11d992a335
wip: tweak GC further (#5982) 2022-04-15 20:08:39 +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
Zachary Wimer
9ecd4f8406
MANIFEST.in will now include pyproject.toml (#5979) 2022-04-15 19:53:16 +02:00
Nikolaj Bjorner
c33611e9e0 include map for non vs builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-15 19:23:48 +02:00
Nikolaj Bjorner
cc36dd1e0d include map for non vs builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-15 19:18:17 +02: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
Zachary Wimer
7d47e45c6b
Add a hacky patch so that Z3 on M1 hardware can link to libs properly (#5974) 
* Add a hacky patch so that Z3 on M1 hardware can link to libs properly

* Update setup.py

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-15 09:57:51 +02:00
Nikolaj Bjorner
ddbe17d581 #5965 
define the is_bool on ArithSortRef
 2022-04-13 16:08:54 +02:00
Nikolaj Bjorner
3f5eb7fcf2 re-enable pre-process 2022-04-13 11:24:24 +02:00
Nikolaj Bjorner
c9fa00aec1 expose recursive functions with own op-code over API 2022-04-13 11:24:24 +02:00
Zachary Wimer
c0b455e010
Add cmake setup.py build dep (#5972) 
* Add wheel as build dependency

* Add cmake as a python build dependency

* pyproject toml update

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-13 08:48:08 +02:00
Zachary Wimer
9834d7aae0
Setup.py fix dependencies (#5971) 
* Add wheel as build dependency

* pyproject toml update
 2022-04-13 08:31:24 +02:00
Audrey Dutcher
032768b0fc
setup.py: copy generated python files correctly (#5975) 2022-04-13 08:29:36 +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
Nikolaj Bjorner
ac55e29a56 disable propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-11 22:23:42 +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