3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Commit graph

2358 commits

Author SHA1 Message Date
Nikolaj Bjorner b57353eff2 fix bounds bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 18:06:18 -07:00
Nikolaj Bjorner 83e7107485 fix bugs in doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 17:45:01 -07:00
Nikolaj Bjorner 4cf8905a8f fixing join
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 11:08:23 -07:00
Nikolaj Bjorner 75b11d2b75 fix bugs in doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 03:22:26 -07:00
Nikolaj Bjorner 8c34cfca31 streamline condition, fix bugs in doc::subtract
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 01:54:51 -07:00
Nikolaj Bjorner 3203b6e2db fix bug in contains check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 01:42:14 -07:00
Nikolaj Bjorner 816119e8ae fix bug in contains check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-22 01:37:11 -07:00
Nikolaj Bjorner 22808a039d working on udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-21 20:25:11 -07:00
Nikolaj Bjorner a50cbef877 testing doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-20 19:01:15 -07:00
Nikolaj Bjorner 2552c1530b doc unit tests pass
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-20 10:19:54 -07:00
Nikolaj Bjorner f94bdf4035 updated unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-20 01:05:43 -07:00
Nikolaj Bjorner 2b2ba2d541 unit testing doc relation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-19 21:55:20 -07:00
Nikolaj Bjorner 25914c0492 testing filter interpreted
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-19 18:18:40 -07:00
Nikolaj Bjorner 6a8623ef0c remove extra udoc_relation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-19 11:01:38 -07:00
Nikolaj Bjorner 5679cc7567 move doc code to rel, adding unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-19 11:00:30 -07:00
Nikolaj Bjorner cb8ad76677 finished code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 23:51:11 -07:00
Nikolaj Bjorner adce20119f doing project
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 22:30:45 -07:00
Nikolaj Bjorner 6db3ca1236 unit test merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 21:58:11 -07:00
Nikolaj Bjorner 0d5b1637ba debug projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 20:45:13 -07:00
Nikolaj Bjorner b524603287 local
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 15:47:09 -07:00
Nikolaj Bjorner 8154fc24e1 testing projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 15:42:30 -07:00
Nikolaj Bjorner 4173bf930b fix-eq bits and projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 14:08:53 -07:00
Nikolaj Bjorner c2db127a45 fix-eq bits and projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 14:04:06 -07:00
Nikolaj Bjorner 8384a27eca handle fix_eq functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 11:43:18 -07:00
Nikolaj Bjorner 53ac452253 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 06:39:59 -07:00
Nikolaj Bjorner 9116d38628 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 06:07:03 -07:00
Nikolaj Bjorner 06f0037917 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 05:53:20 -07:00
Nikolaj Bjorner 9a3a1835cc doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 05:52:09 -07:00
Nikolaj Bjorner 2a00f2b38c adding unit tests for doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 05:19:52 -07:00
Nikolaj Bjorner 4eadaabe64 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-18 03:53:14 -07:00
Nikolaj Bjorner 4c3605421c doc snapshot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-17 16:48:41 -07:00
Nikolaj Bjorner c6e0a62cb9 udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-17 15:42:35 -07:00
Nikolaj Bjorner 99ff13b651 opt + udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-17 11:39:25 -07:00
Nikolaj Bjorner 7e91fb5c15 remove mk_or_reduced
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 22:14:58 -07:00
Nikolaj Bjorner e32448d7ea more fun with docs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 21:46:39 -07:00
Nikolaj Bjorner 44e8833369 more udoc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 17:06:05 -07:00
Nikolaj Bjorner f71730b0df porting fun
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 15:50:12 -07:00
Nikolaj Bjorner 1058de1aa7 adding udoc_relation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 13:22:04 -07:00
Nikolaj Bjorner 887e6e5392 doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 00:45:17 -07:00
Nikolaj Bjorner 31c7f79afd fix bv size
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 22:13:56 -07:00
Nikolaj Bjorner bae4d54955 fix bv size
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 22:11:35 -07:00
Nikolaj Bjorner 4e4346576a move to managed tbvs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 22:01:13 -07:00
Nikolaj Bjorner d9dafe7b94 tbv utilities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 21:23:03 -07:00
Nikolaj Bjorner cd12fa8461 adding fixed size bit-vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 20:00:45 -07:00
Nikolaj Bjorner c09903288f have free variable utility use a class for more efficient re-use
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-15 16:14:22 -07:00
Nikolaj Bjorner 73070585b8 fix bug in core generation in legacy core: it ignores complementary literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-14 13:06:01 -07:00
Nikolaj Bjorner a96fa0c555 remove deprecated maxsat solvers, adjust values inline
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-14 11:55:47 -07:00
Nikolaj Bjorner 770d0d58fe bug fixes to sorting network
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-11 21:53:12 -07:00
Nikolaj Bjorner e288b7795d add to unit test
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-11 20:33:37 -07:00
Nikolaj Bjorner 019ff77613 fix sorting network bug, add network compilation,...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-11 18:47:21 -07:00