mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 01:46:39 +00:00
Code Activity
14221 commits 43 branches 51 tags 169 MiB
Commit graph

403 commits

Author SHA1 Message Date
Nikolaj Bjorner
45855fce06 fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 10:45:29 -07:00
Nikolaj Bjorner
dd5e2e8930 check for 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 10:44:00 -07:00
Nikolaj Bjorner
85cb0293f5 fix #4541 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-24 20:26:59 -07:00
Jack Yao
55cd1e996c
add sat option for doing a global simplification before the bounded search and the main CDCL search loop. The option is also used for the sat-preprocess tacitc (#4514) 
Co-authored-by: rainoftime <rainoftime@gmail.com>
 2020-06-12 16:45:50 -07:00
Nikolaj Bjorner
f538ee3fe2 another module level ifdef for #4382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-18 15:07:39 -07:00
Nikolaj Bjorner
73fa5995d4 fix #4316 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-13 19:35:17 -07:00
Nikolaj Bjorner
603b5552fa port progation from cons branch 2020-05-06 12:21:01 -07:00
Nikolaj Bjorner
95a78b2450
updates to seq and bug fixes (#4056) 
* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4037

* nicer output for skolem functions

* more overhaul of seq, some bug fixes

* na

* added offset_eq file

* na

* fix #4044

* fix #4040

* fix #4045

* updated ignore

* new rewrites for indexof based on #4036

* add shortcuts

* updated ne solver for seq, fix #4025

* use pair vectors for equalities that are reduced by seq_rewriter

* use erase_and_swap

* remove unit-walk

* na

* add check for #3200

* nits

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* name a type

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove fp check

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unsound axiom instantiation for non-contains

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix rewrites

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4053

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix #4052

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-22 13:18:55 -07:00
Nikolaj Bjorner
b42b329d6c initialize best-phase-size #3897 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-10 12:04:55 -07:00
Nikolaj Bjorner
1949a978ce fix #3760 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 11:39:25 -07:00
Nikolaj Bjorner
7e8753cd3f fix #3726 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 18:48:09 -07:00
Nikolaj Bjorner
9109a29a15 fix #3653 cubing could convert internal variables to external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:42:20 -07:00
Nikolaj Bjorner
3574a95e50 fix #3647 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:52:59 -07:00
Nikolaj Bjorner
ddc77b1100 fix #3632 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:53:10 -07:00
Nikolaj Bjorner
79183b6339 say no to local search + parallel #3636 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 20:11:25 -07:00
Nikolaj Bjorner
6635f92842 fix #3618 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 14:10:39 -07:00
Nikolaj Bjorner
55c285c0df fix #3620 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 14:01:00 -07:00
Nikolaj Bjorner
0ff97d5a31 fix #3626 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 11:51:52 -07:00
Nikolaj Bjorner
acb9376ea0 fix #3488 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-23 10:57:15 -07:00
Nikolaj Bjorner
e9f45695c1 fix #3443 - some properties checked by invariant isn't valid during destructor when using threads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 10:57:22 -07:00
Nikolaj Bjorner
945cd3169e fix #3440 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-22 10:43:52 -07:00
Nikolaj Bjorner
24dd047892 fix #3397, use it or lose it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 11:06:19 -07:00
Nikolaj Bjorner
0768701744 fix #3220 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-10 16:08:16 -07:00
Nikolaj Bjorner
6b0e599b88 fix #3140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 11:22:13 +01:00
Nikolaj Bjorner
76d91f7d2b fix #3142 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-04 14:27:32 -08:00
Nikolaj Bjorner
2989d9c241 fix #3124 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-03 12:39:25 -08:00
Nikolaj Bjorner
c71da17a10 add output for inprocessing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-22 11:50:51 -08:00
Nikolaj Bjorner
dd3e77107e rename aig_simplifier to cut_simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 18:29:59 -08:00
Nikolaj Bjorner
f1abc71c35 fix #2962 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-10 11:44:10 -08:00
Nuno Lopes
d79692b185 remove unused file & hide a few symbols 2020-01-31 17:13:28 +00:00
Nikolaj Bjorner
e0a41a18c3 add validation to aig_simplifier, start BIG-based masking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-11 20:47:38 -08:00
Nikolaj Bjorner
192c6e39c2 separate out aig_cuts class, make it fully incremental with eviction strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-09 02:16:23 -08:00
Nikolaj Bjorner
20618ff3b3 integrate aig further 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-08 19:41:23 -08:00
Nikolaj Bjorner
57846e50fa use variable id as level, separate cut-set updates, add missing reset in pdd 2020-01-08 02:15:45 -08:00
Nikolaj Bjorner
e1fb74edc5 add ite-finder, profile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:50 -08:00
Nikolaj Bjorner
d27a949ae9 add anf and aig simplifier modules, cut-set enumeration, aig_finder, hoist out xor_finder from ba_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Nikolaj Bjorner
40a4326ad4 add anf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Nikolaj Bjorner
216affd852 set defrag 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-31 11:55:44 -08:00
Nikolaj Bjorner
918846a97e fix #2814 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 16:35:38 -08:00
Nikolaj Bjorner
5dfe4a4b48 ensure relevancy isn't increased between calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-23 15:42:44 -08:00
Michał Janiszewski
3feb1479c9 Improve platform detection, in particular MSVC ARM64 2019-10-24 15:19:53 -07:00
Nikolaj Bjorner
e5504247e9 use propagation filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-20 16:00:20 -07:00
Nuno Lopes
4643fdaa4e remove a few str copies when throwing exceptions 2019-10-08 22:29:17 +01:00
Nikolaj Bjorner
a337a51374 fixes for #2513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner
53aded3198 fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-25 18:55:44 -07:00
Nikolaj Bjorner
604e6b2705 fix #2418, change types in sat_solver to avoid cast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-24 11:52:28 -07:00
Nikolaj Bjorner
1a70fce92e add back nvars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-24 09:51:04 -07:00
Nikolaj Bjorner
364fbda925 expose reorder config 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-22 15:30:06 -07:00
Nikolaj Bjorner
a9a26e5f2e review comments by Elffers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-21 06:52:02 -07:00
Nikolaj Bjorner
43a19cadf6 avoid reorder regression. affects performance of SAT and also noticably for #2405 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-20 12:40:22 -07:00