3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Commit graph

12141 commits

Author SHA1 Message Date
Nikolaj Bjorner
65d818437a add simplification routines
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-25 19:31:18 -08:00
Nikolaj Bjorner
de6409f558 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-25 11:07:14 -08:00
Nikolaj Bjorner
5a68fc8c07 fix pdd_stack for gc on reduce, add unit test for linear_simplify
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-25 11:05:59 -08:00
Nikolaj Bjorner
78feac4465 different kind of loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-23 19:36:13 -08:00
Nikolaj Bjorner
34ae55f4f5 fix gc bug 2019-12-23 18:29:42 -08:00
Nikolaj Bjorner
3df6080a27 Update dd_pdd.cpp
dbg
2019-12-23 15:53:10 -08:00
Nikolaj Bjorner
38f74297a9 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-23 15:30:06 -08:00
Nikolaj Bjorner
beb4c0f27b added notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-23 12:34:30 -08:00
Nikolaj Bjorner
77868f3d96 added notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-23 12:32:02 -08:00
Lev Nachmanson
3aff0bd7db add a unit test to pdd
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-12-22 19:37:29 -08:00
Nikolaj Bjorner
25b98f497a adding level2var
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-22 11:51:04 -08:00
Nikolaj Bjorner
58be42d2a9 initial unit test for pdd_grobner
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-22 10:59:12 -08:00
Nikolaj Bjorner
3fca59ac84 add missing scoped_push
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-21 18:06:28 -08:00
Nikolaj Bjorner
c4da5caf69 update comment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-21 17:59:00 -08:00
Nikolaj Bjorner
72b47ba519 use while loop for reduce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-21 17:57:01 -08:00
Nikolaj Bjorner
efbcdcbffd simplify diff rewriting 2019-12-20 23:20:19 -08:00
Nikolaj Bjorner
4a94abe7d7 Update nightly.yaml
update name
2019-12-20 23:18:19 -08:00
Nikolaj Bjorner
b13e7b9df3 Update nightly.yaml
again
2019-12-20 22:29:47 -08:00
Nikolaj Bjorner
c8703cbc42 Update nightly.yaml
try again
2019-12-20 22:26:14 -08:00
Nikolaj Bjorner
f977e1a3e2 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 22:02:01 -08:00
Nikolaj Bjorner
90ca594835 remove unsound use of sat_big reduction 2019-12-20 22:01:18 -08:00
Nikolaj Bjorner
8a75e9090b Update nightly.yaml
mac -> osx
2019-12-20 21:16:11 -08:00
Nikolaj Bjorner
c5d31be613 Update nightly.yaml
add Python top zip
2019-12-20 21:12:13 -08:00
Nikolaj Bjorner
495658e07a try adding macos to nightly
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 20:16:28 -08:00
Nikolaj Bjorner
4389ed0f58 fix #2812
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 17:12: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
d2108ad043 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 15:42:30 -08:00
Nikolaj Bjorner
cb21f70cc3 fix #2813
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 15:42:03 -08:00
Nikolaj Bjorner
485ca725de fix #2811
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 15:27:38 -08:00
Nikolaj Bjorner
fec94d1552 fix #2805
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 12:48:19 -08:00
Nikolaj Bjorner
feff6a2add fix build, add ZDD reference
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 11:49:50 -08:00
Nikolaj Bjorner
1f9aff04df fix 2808
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-20 11:29:08 -08:00
Nikolaj Bjorner
6ad55cc8f6 add tuned implementation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-19 15:26:55 -08:00
Nikolaj Bjorner
78b022491d comments
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-19 09:26:02 -08:00
Nikolaj Bjorner
49b6d5b6fb rm typedef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 21:20:20 -08:00
Nikolaj Bjorner
036d5c02f4 add typedef
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 20:59:56 -08:00
Nikolaj Bjorner
a068ee9748 extract generic content from nla_intervals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 20:33:48 -08:00
Nikolaj Bjorner
27b69cf280 updates
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 17:03:56 -08:00
Nikolaj Bjorner
1287572f4f add complexity throttle
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 14:31:31 -08:00
Nikolaj Bjorner
f5164d166b unused / return warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 14:25:18 -08:00
Nikolaj Bjorner
13e335f062 fix
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 14:14:46 -08:00
Nikolaj Bjorner
98bfbc2d62 tidy
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 13:59:45 -08:00
Nikolaj Bjorner
469f618742 build dependencies, invariant annotation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 13:48:27 -08:00
Nikolaj Bjorner
5e0799225d adding pdd-grobner
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-18 12:03:13 -08:00
Nikolaj Bjorner
ca0a52c930 some const qualifiers
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 21:59:05 -08:00
Nikolaj Bjorner
1680585827 swap sub with minus
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 21:46:55 -08:00
Nikolaj Bjorner
a744a465e6 pdd fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 21:25:18 -08:00
Nikolaj Bjorner
f2149fb5a6 na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 17:14:51 -08:00
Nikolaj Bjorner
f7eb5f8840 merge unary minus
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 17:10:35 -08:00
Nikolaj Bjorner
9e4a7ae4b8 add pdd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-17 16:59:33 -08:00