mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
17911 commits 49 branches 53 tags 182 MiB
Commit graph

17911 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
3533bf486f merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-16 18:30:03 +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
f1b10b0ea4 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2022-04-13 12:22:49 +02:00
Nikolaj Bjorner
da168cad2d track _all_ interval end-points for propagation (in fact only need end-points at unit location, not the others so this can be tuned 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-13 12:22:43 +02:00
Jakob Rath
88a17ef33e print more 2022-04-13 11:42:41 +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
Jakob Rath
be488f75ab Add some fi info 2022-04-13 09:34:59 +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
Jakob Rath
d59c32261f Merge remote-tracking branch 'origin/polysat' into polysat 2022-04-12 16:08:09 +02:00
Jakob Rath
9fa5096776 conflict logging 2022-04-12 16:06:20 +02:00
Jakob Rath
00fa4b3320 Better search stack printing 2022-04-12 14:13:20 +02:00
Jakob Rath
8b2f1654fa Better search stack printing 2022-04-12 13:48:06 +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
59f2603a3a add parameter class for polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-12 10:36:01 +02:00
Nikolaj Bjorner
afa7162ab1 add parameter class for polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-12 10:35:23 +02:00
Nikolaj Bjorner
f2b9c27ed6 use simpler looking for loop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-04-12 10:13:44 +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