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

16432 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 33ffd464cf inc version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-24 12:17:07 +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
Nikolaj Bjorner 39f57fb7ca update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-23 20:02:16 +01:00
Victor bd6b3027cd
Document gotcha with z3-js (#5994) 2022-04-23 19:52:35 +01:00
Nikolaj Bjorner 0529e88589 enable pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-23 19:51:25 +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 8e509d34b5 remove test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-23 19:05:42 +01:00
Nikolaj Bjorner 8778f4d43f updated release script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-23 17:59:23 +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 e6e00d894f update nightly/release scripts to produce arm64 for what is tested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-21 10:18:40 +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
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