mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
15002 commits 49 branches 53 tags 182 MiB
Commit graph

1303 commits

Author SHA1 Message Date
Nikolaj Bjorner
185b01dd35 fix #2416 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Nikolaj Bjorner
c2264c73f2 debug mutex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Daniel Schemmel
77d5b381ea
Order initialization to avoid -Wreorder 2019-07-23 11:12:29 +02: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
a9a26e5f2e review comments by Elffers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-21 06:52:02 -07:00
Nikolaj Bjorner
43a19cadf6 avoid reorder regression. affects performance of SAT and also noticably for #2405 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-20 12:40:22 -07:00
Nikolaj Bjorner
41ca956012 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 13:45:13 -07:00
Nikolaj Bjorner
cd93cdd819 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-09 07:40:29 +01:00
Nikolaj Bjorner
1e21ea4645 fix cleanup bug exposed by reordering simplifcations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-23 01:25:50 +02:00
Nikolaj Bjorner
333b32b0d2 disable adding redundant ite clauses as lemma. Add as non-redundant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 16:32:45 +02:00
Nikolaj Bjorner
cbe52e298b remove tracing, fix doctext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 15:08:26 +02:00
Nikolaj Bjorner
b1dbea328a remove unreferenced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 09:17:17 +02:00
Nikolaj Bjorner
b1893f2a58 fix build issue for debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-20 17:21:04 +02:00
Nuno Lopes
1827f98851 more fixes for mutexes in shell 2019-06-19 16:42:00 +01:00
Nikolaj Bjorner
3985cfa33c ensure parameters are passed to local search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-17 12:31:13 -07: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
2bee9a062f merge more from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:24:37 -07:00
Nikolaj Bjorner
e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Nikolaj Bjorner
44b0b0148b deal with warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-06 17:13:38 -07:00
Nuno Lopes
a53ff6f21c turn locks into no-ops when compiled with -DSINGLE_THREAD 2019-06-05 12:11:27 +01:00
Nikolaj Bjorner
7f74382863 capture i by value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:18 +01:00
Nikolaj Bjorner
9f3089b098 try with std::vector and ptr_vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
f5511b4174 missing include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
1f84381c4c pfor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
59330b3855 pfor 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
9262908ebb mux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-05 09:06:17 +01:00
Nikolaj Bjorner
f1dee935d0 remove UNREACHABLE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 17:07:00 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
d4410d0872 address compilation warnings of unused parameters, add shorthands to set parameters on Optimize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-16 14:32:48 -07:00
Nikolaj Bjorner
5c67c9d907 print certificate for #2202, enable CTL-C for API fix #2203 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 17:09:02 -07:00
Nikolaj Bjorner
dc0e9c1919 completing user print experience with seq/re #2200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-24 11:46:36 -07:00
Nikolaj Bjorner
a74ac93bcc fix #2196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 13:34:31 -07:00
Nikolaj Bjorner
057151c7a8 fix #2188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-18 07:56:25 -07:00
Nikolaj Bjorner
7399f78dfd disable model compression for regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:40:59 -08:00
Nikolaj Bjorner
006590f329 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 14:29:20 -08: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
e76cea4684 Merge branch 'master' of https://github.com/z3prover/z3 2019-02-28 11:44:45 -08:00
Nikolaj Bjorner
69d7d8ff87 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 11:42:17 -08:00
Nikolaj Bjorner
4c76d43670 add binary_merge encoding option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-28 08:35:22 -08:00
Daniel Schemmel
c2ebbc9210
fix -Wsign-compare (len can never become negative anyway) 2019-02-23 10:57:41 +01:00
Nikolaj Bjorner
73060ecaec remove debug code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-22 13:57:09 +01:00
Nikolaj Bjorner
bceff4b3fa Merge branch 'master' of https://github.com/z3prover/z3 2019-02-22 11:17:03 +01:00
Nikolaj Bjorner
4c799c144a fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-22 11:14:20 +01:00
Nuno Lopes
6598aedbb2 fix VS build, take 2 2019-02-21 15:52:52 +00:00
Nuno Lopes
2f33bafd5a stopwatches: fix a few places that would call start/stop multiple times 2019-02-21 14:59:31 +00:00
Nikolaj Bjorner
3548057bd1 fix detection of arithmetic operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-20 14:00:05 +01:00
Nikolaj Bjorner
caa15ea04d enable cardinality constraints in nla2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 18:17:07 +01:00
Nikolaj Bjorner
2138a5232f fix #2142 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-19 10:16:50 +01:00
Nikolaj Bjorner
7fb2c6a908 turn off model validation unless specified by parameter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:55:24 +01:00
Nikolaj Bjorner
0aafa8b7ce optimize binary output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-18 15:52:42 +01:00