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

110 commits

Author SHA1 Message Date
Nikolaj Bjorner
4455f6caf8 move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail 2021-02-02 03:58:19 -08:00
Nikolaj Bjorner
a764d528a1 'clean 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-30 13:14:48 -07:00
Nikolaj Bjorner
ed7d969366 elaborate on smt/drat format outline, expose euf mode as config 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-31 19:29:23 -07:00
Nikolaj Bjorner
c41abf2241 fix #4624 #4633 #4632 #4631 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 08:36:16 -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
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
b4e7730034 fix #3938 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-13 13:05:53 -07:00
Nikolaj Bjorner
9b609af8fc fix #3924 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-12 16:19:54 -07:00
Nikolaj Bjorner
c85113acdb fix #3928 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-12 15:25:08 -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
fcbf660592 fix #3133 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-03 19:29:15 -08:00
Nikolaj Bjorner
05158b3914 add cut redundancies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-01 12:49:59 -08:00
Nikolaj Bjorner
e8f7a08289 add stubs for npn3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-27 21:19:40 -08:00
Nikolaj Bjorner
dddd740846 make aig/ite extraction conditional 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-25 16:27:13 -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
d1e95a133b add simplifiation pass 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-22 11:21:53 -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
c46e36ce58 bug fixes to LUT extraction, bug fix for real value case of freedom intervals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-11 14:25:25 -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
5dfe4a4b48 ensure relevancy isn't increased between calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-23 15:42:44 -08: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
364fbda925 expose reorder config 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-22 15:30:06 -07:00
Nikolaj Bjorner
cd93cdd819 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-09 07:40:29 +01:00
Nikolaj Bjorner
d17248821a include chronological backtracking, two-phase sat, xor inprocessing, probsat, ddfw 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-13 08:45:21 -07:00
Nikolaj Bjorner
a2dddbd7a5 check pb solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 14:28:03 -08:00
Nikolaj Bjorner
69d7d8ff87 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 11:42:17 -08:00
Nikolaj Bjorner
5cdfa7cd1c variations on unit-walk 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-13 17:43:15 -08:00
Nikolaj Bjorner
24dfdfe9bc disable fixes for #2128 and related as it breaks model evaluation time in regressions, set longer delay for inprocessing in sat solver, report stats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-09 16:06:02 -08:00
Nikolaj Bjorner
08ce6f7ac1 working on binary drat format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-30 08:54:59 -08:00
Nikolaj Bjorner
dc77579707 delta faction to control double lookahead eagerness 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-04 23:41:03 -08:00
Nikolaj Bjorner
719bc5cd5d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-30 17:23:31 -05:00
Nikolaj Bjorner
3c1c3d5987 fix #1908 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-30 14:15:29 -05:00
Nikolaj Bjorner
e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Nikolaj Bjorner
f5fea8ae30 add parameter to force sat-cleaning on initialization and on simplification phases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-11 22:05:04 -07:00
Nikolaj Bjorner
f53b7aaca2 fix none-case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-04 15:46:10 -07:00
Nikolaj Bjorner
9ad17296c2 update parameters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 17:22:48 -07:00
Nikolaj Bjorner
c8730daea7 fix memory leak, add strengthening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 16:56:07 -07:00
Nikolaj Bjorner
13b54f379c fix ema 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-05 13:58:47 +02:00
Nikolaj Bjorner
e940f53e9c n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 07:57:33 -07:00
Nikolaj Bjorner
563f337997 testing memory defragmentation, prefetch, delay ate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-27 17:59:03 +02:00
Nikolaj Bjorner
252fb4af6e add backtracking conquer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 15:34:33 -07:00
Nikolaj Bjorner
f7e49501af updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-13 16:22:36 -07:00
Nikolaj Bjorner
59b142f803 fixing local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-15 06:48:26 -07:00
Nikolaj Bjorner
4c1379e8c9 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-19 21:49:03 -08:00
Nikolaj Bjorner
db347c007d remove legacy bce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 09:39:39 -08:00
Nikolaj Bjorner
eca250933d disable uhle from lookahead solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-01 19:56:01 -08:00
Nikolaj Bjorner
5a2b072ddf working on completing ATE/ALA for acce and abce 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-29 20:32:06 -08:00
Nikolaj Bjorner
c80f34102f adding ad-hoc method for converting models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-28 17:29:31 -08:00