3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Commit graph

11792 commits

Author SHA1 Message Date
Nikolaj Bjorner e73ce6e712 build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-12-25 20:05:03 -08:00
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