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

16458 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 3ae781039b inc version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-05 07:09:54 -07:00
Nikolaj Bjorner d420706eae enable pypi release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 17:16:30 -07:00
Nikolaj Bjorner b8d05135db Merge branch 'master' of https://github.com/z3prover/z3 2022-05-04 12:08:07 -07:00
Nikolaj Bjorner cf1802dac7 release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 12:07:54 -07:00
Nikolaj Bjorner 47459ca795 pre-release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 12:04:51 -07:00
Sacha Ayoun ffbabf251d
enhance ocaml seq api (#6010) 
Signed-off-by: Sacha Ayoun <sachaayoun@gmail.com>
 2022-05-04 12:03:22 -07:00
Nikolaj Bjorner 5a685ba9b5 expose maxdiff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 08:52:42 -07:00
Nikolaj Bjorner 367bfedab0 add min/max diff in final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 07:39:38 -07:00
Nikolaj Bjorner c29cfa81ae prep for max/min diff 2022-05-04 02:08:11 -07:00
Nikolaj Bjorner 87d2a3b4e5 map/mapi/foldl/foldli 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-04 01:10:18 -07:00
Nikolaj Bjorner b3e0213cab missing object ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-02 12:35:28 -07:00
Nikolaj Bjorner be653dab0e init value 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner d1f1e4ce34 selectively enable dual strengthening 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner 98e1c86128 na 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner 9cc5f6901a na 2022-05-01 15:26:57 -07:00
Nikolaj Bjorner b5c7f000de add option to "rotate" cores during core finding 
enable to find multiple cores in a round and at the same time facilitate rotation around satisfiable subsets to explore neighborhoods for improved assignments.
 2022-05-01 15:26:56 -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
Ryan Goulden 99e299b90c
ocaml: fix is_arithmetic_numeral and is_bv_numeral (#6003) 2022-04-27 12:36:09 +02:00
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
Nikolaj Bjorner 0b453a4af5 set release version 2022-04-25 08:57:32 +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
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