mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 00:11:55 +00:00
Code Activity
2458 commits 29 branches 52 tags 172 MiB
Commit graph

184 commits

Author SHA1 Message Date
Nuno Lopes
e778f3e65b DoC: fix bug in insertion when inserting an element equal to on on the disjunction already 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 12:49:38 +01:00
Nuno Lopes
7d599fa047 DoC: fix bug I previously introduced in insert 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 11:54:53 +01:00
Nuno Lopes
9828b26379 DoC: fix slow path of filter_by_negation when columns are repeated in tgt relation 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-02 09:56:06 +01:00
Nikolaj Bjorner
bb15ddbf15 update unit tests to use filter_by_negation verifier from check_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 15:21:42 -07:00
Nuno Lopes
04b5d436b3 DoC: fix fast path of filter_negated 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 18:03:59 +01:00
Nuno Lopes
5211e9aa1a DoC: compact result of subtract 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-10-01 17:10:35 +01:00
Nuno Lopes
115ab12ade DoC: code cleanups 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 17:16:14 +01:00
Nuno Lopes
8d1177bf3f DoC: compact result of substract and maintain invariant 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 16:24:59 +01:00
Nuno Lopes
1606359dc9 DoC: add slow path to emptiness detection that uses SMT solving 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 15:58:38 +01:00
Nuno Lopes
938a5adafa DoC: make fold_neg detect empty TBVs 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 13:00:29 +01:00
Nuno Lopes
5176cbeefb fix printing of TBVs 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-30 11:26:49 +01:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07:00
Nikolaj Bjorner
08ef9f34bc add lipstick note 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 08:46:14 -07:00
Nikolaj Bjorner
061a18efcf move some configuration parameters into dl_context, add notes to udoc_relation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 08:22:25 -07:00
Nikolaj Bjorner
74053275cf consolidate rule checking in separate class 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-25 19:05:49 -07:00
Nikolaj Bjorner
8e2fedbc2e Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-09-25 09:33:20 -07:00
Nikolaj Bjorner
a2d8fd4c4b local opts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-25 09:33:12 -07:00
Nuno Lopes
b7397b6967 relations with no columns are not always non-empty. 
fix that in the udoc datalog backend

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-25 16:27:20 +01:00
Nuno Lopes
aaa931e0d5 fix build with gcc 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-25 15:56:01 +01:00
Nuno Lopes
84a61b5454 reenable datalog while loop priting 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-25 14:36:37 +01:00
Nuno Lopes
41d7c50e29 fix debug build 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-25 14:10:17 +01:00
Nuno Lopes
4a710cf86d sync with unstable (port bugfix) 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-25 11:35:32 +01:00
Nikolaj Bjorner
9cea3a1c02 last? bug-fix to new udoc_relation for feature parity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 22:08:49 -07:00
Nikolaj Bjorner
979d1f913a fix bug in union_fn: delta should not be reset, it is shared among several union computations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 16:46:00 -07:00
Nikolaj Bjorner
6457654e2e make self-contained bind-variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 14:30:30 -07:00
Nikolaj Bjorner
918d52f1b0 tune and fix doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 09:20:21 -07:00
Nikolaj Bjorner
16f80fce92 add check_relation for integrity checking of relational operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-24 01:06:58 -07:00
Nikolaj Bjorner
1111c0494f adding validation code to doc/udoc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-23 17:10:00 -07:00
Nikolaj Bjorner
54506408f9 fix overflow bugs in doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-22 22:03:59 -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
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