mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-30 06:50:08 +00:00
Code Activity
2481 commits 65 branches 52 tags 178 MiB
Commit graph

417 commits

Author SHA1 Message Date
Nikolaj Bjorner
c706e91019 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-05 10:37:55 -07:00
Nikolaj Bjorner
47b81d2ec0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-02 14:33:55 -07:00
Nikolaj Bjorner
d03a4bc306 check cancel flag after bcp. BCP returns in incomplete state after it check's the cancel flag. Propagate returns 'true' in this case so that the main loop exits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-02 14:33:42 -07:00
Nikolaj Bjorner
cce287eed1 fix bug in Shannon decomposition for translating PB constraints into formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-01 12:51:40 -07:00
Nikolaj Bjorner
989569b154 add bceq experiment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-29 10:57:31 -07:00
Nuno Lopes
97a5e6d326 assorted compiler warnings fixes 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-28 12:21:56 +01:00
Nikolaj Bjorner
9412890c63 trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:58:55 -07:00
Nikolaj Bjorner
e6725b2344 merge unstable into opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-26 12:12:24 -07: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
Nikolaj Bjorner
45bfcda16c remove typename 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-17 16:37:53 -07:00
Nikolaj Bjorner
e8b9c251d5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 17:13:20 -07:00
Nikolaj Bjorner
d01ca11001 reduce asymptotic overhead of asserting bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-16 17:13:09 -07:00
Nuno Lopes
f7c3559c31 fix a few compiler warnings 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-09-16 15:26:01 +01: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
019ff77613 fix sorting network bug, add network compilation,... 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-11 18:47:21 -07:00
Nikolaj Bjorner
f151879c0b enable neat vs. less neat pretty priting as an option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-09 16:25:41 -07:00
Nikolaj Bjorner
d9c61464d0 make difference logic simplex optimizer incremental 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-07 16:46:46 -07:00
Nikolaj Bjorner
c1580fb85a follow logic annotation/enable diff logic when configured 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-07 11:52:14 -07:00
Nikolaj Bjorner
b5bbf83847 update core generation to be partial, update maxres to use current model too 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-02 19:05:28 -07:00
Nikolaj Bjorner
3f8083dfa6 fix push/pop bugs in optimize context, add example to c++, fix bug in arithemtic bounds axiom addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-02 09:32:38 -07:00
Nikolaj Bjorner
75c114feab fix regression on push/pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-01 14:37:58 -07:00
Nikolaj Bjorner
89f0319043 tune assertions of bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-09-01 11:19:05 -07:00
Nikolaj Bjorner
7ee2844509 bounds axiom tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-31 12:49:12 -07:00
Nikolaj Bjorner
3cbcd19a9b bounds axiom tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-31 12:40:13 -07:00
Nikolaj Bjorner
7f49135b3b bounds axiom tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-31 11:48:00 -07:00
Nikolaj Bjorner
37b96a6133 bounds axiom tuning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-31 11:16:08 -07:00
Nikolaj Bjorner
afe7fc367b working on maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-30 12:40:37 -07:00
Nikolaj Bjorner
83a7d1a658 adding options to maxres for experiments, include option to pretty print module parameters in smt2 style 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-30 11:46:29 -07:00
Nikolaj Bjorner
ee1a1b1135 refactor sat/sls interface. Remove wpm2 and bvsls dependencies 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-15 10:40:44 -07:00
Nikolaj Bjorner
3d995648ee partial fix to model generation bug for non-linear constraints: avoid epsilon refinment for non-shared variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-08-07 20:39:20 +09:00
Ken McMillan
c007a5e5bd merged with unstable 2014-08-06 11:16:06 -07:00
Nikolaj Bjorner
0e9511b597 unsat core for SAT solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-29 08:39:34 -07:00
Nikolaj Bjorner
19050d1c4c merge Fixedpoint.cs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 12:20:48 -07:00
Nikolaj Bjorner
4ab27eff78 refactor weighted-maxsat into separate files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-28 08:31:57 -07:00
Nikolaj Bjorner
dd786bb5bf fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 15:41:03 +02:00
Nikolaj Bjorner
e4dedbbefc fix quantifier elimination bugs reported by Berdine and Bornat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-14 15:38:22 +02:00
Nikolaj Bjorner
465eafbf45 fix assertion for integrality, lax noprogress bail out code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-07-09 05:04:00 +02:00
Christoph M. Wintersteiger
3209cd2ded Disabled construction of partial model on theory failure as it caused buggy behavior. 
Thanks to parno (Codeplex Issue #117)!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-23 16:40:49 +01:00
Christoph M. Wintersteiger
000db81b4f Fixed bug where the random seed wasn't passed through to 
theory_arith. Thanks to Carsten! (Stackoverflow #24327987)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-06-23 15:47:47 +01:00
Nikolaj Bjorner
960e8ea1d5 working on hitting sets 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-08 14:12:54 +01:00
Nikolaj Bjorner
88bd01bc4f patching non-termination bug in datatype factory, reported by Tiago 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-06-03 23:03:34 +05:30
Nikolaj Bjorner
a10c318e15 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-31 12:04:28 +05:30
Nikolaj Bjorner
f76b343bfa expose parameter settings for controlling injectivity axiom. rquested by Jasmin Blanchette 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-31 11:25:54 +05:30
Christoph M. Wintersteiger
7288353575 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-30 18:14:46 +01:00
Christoph M. Wintersteiger
bc25ea404f Fixed potential bug (warning on OSX). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-05-30 18:14:33 +01:00
Nikolaj Bjorner
49f9f4b3b5 fix crash in model construction from finite domain theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-30 20:52:39 +05:30
Nikolaj Bjorner
57fc0f3f55 bug fixes to min-max, and experiments with hsmax 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-28 15:44:39 -07:00
Nikolaj Bjorner
2ee416fc8f deal with infinite loop in diagonalization attempt in datatype factory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-21 10:23:31 -07:00
Nikolaj Bjorner
8b5eb08e2d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-05-15 21:12:41 -07:00