mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity
1780 commits 23 branches 48 tags 157 MiB
Commit graph

164 commits

Author SHA1 Message Date
Nikolaj Bjorner
d6964226c7 indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 15:38:44 -07:00
Nikolaj Bjorner
8438ac6e21 fix internalization bug when bit2bool is applied to numeral 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-06 15:43:24 -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
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
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
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
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
Nikolaj Bjorner
3d1ca5ecc9 make eval cache sensitive to model completion. Bug 110 reported by cipher1024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-05-15 21:12:16 -07:00
Christoph M. Wintersteiger
fb4c07a2ea FPA refactoring in preparation for FPA support in the kernel. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-04-23 18:36:38 +01:00
Nikolaj Bjorner
e27b7e3038 use size_t for return values from strlen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:09:57 -08:00
Nikolaj Bjorner
f2ecd70e65 fix ctx solver simplify, remove horn inequalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-03-01 11:02:18 -08:00
Nikolaj Bjorner
891d0d07f8 removig unsound simplification in ctx-solver-simplify tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-02-27 13:42:40 -08:00
Nikolaj Bjorner
b80302cfb0 generalize guard in conflict resolution to handle non-equality binary predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-13 13:41:47 -08:00
Nikolaj Bjorner
0d6220f383 revert is_all_int bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-18 21:53:04 +02:00
Ken McMillan
a318b0f104 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-16 12:45:52 -08:00
Nikolaj Bjorner
909408d6ef fix is_all_int bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-15 10:58:23 +02:00
Ken McMillan
56b3406ee5 added mbqi.id option, working on quantifiers in duality 2013-12-10 11:41:25 -08:00
Ken McMillan
a785a5a4b8 Merge branch 'unstable' into interp 2013-11-05 12:28:13 -08:00
Ken McMillan
3a0947b3ba merged with unstable 2013-10-18 17:26:41 -07:00
Christoph M. Wintersteiger
3d910028bf fixed potential performance problem with fully interpreted sorts in the quantifier instantiation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-09-27 16:55:05 +01:00
Nikolaj Bjorner
2e7f5303eb address incompleteness bug in axiomatization of int2bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-23 04:56:38 +03:00
Nikolaj Bjorner
fd1f4b9191 fix bugs reported by Anvesh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-23 04:07:08 +03:00
Nikolaj Bjorner
5be4365b47 redo edit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 16:53:52 -07:00
Nikolaj Bjorner
c54929e59f cycle through domain size before giving up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 04:52:21 -07:00
Nikolaj Bjorner
21b27cd2d1 patching crash in data-type factory when fresh values are not produced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-15 04:37:05 -07:00
Nikolaj Bjorner
419f99c329 fix bug found by Ethan: fresh values for bit-vectors loops if the domain of bit-vectors is truly small 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-09-13 15:30:56 -07:00
Nikolaj Bjorner
9e61820125 re-organizing muz 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-28 21:49:53 -07:00
Nikolaj Bjorner
6c5f7741b2 more on polynorm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-08-14 11:55:23 -07:00
Nikolaj Bjorner
d9e3881560 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-27 12:00:09 -05:00
Nikolaj Bjorner
619bd91ddb fix bug in ctx-solver-simplify reported @ http://z3.codeplex.com/workitem/51 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-27 11:59:40 -05:00
Leonardo de Moura
544dfde454 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-27 09:30:33 -07:00
Leonardo de Moura
5b7201a911 Fix minor problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-27 09:30:25 -07:00
Nikolaj Bjorner
324dc5869d fix substitution bug in qe, working on boogie trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-25 13:07:28 -05:00
Leonardo de Moura
185f125f7a Fix problem reported at http://stackoverflow.com/questions/17215640/getting-concrete-values-from-a-model-containing-array-ext 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:48:43 -07:00
Ken McMillan
a78564145b hooked up array.weak and array.extension params 2013-06-14 16:46:13 -07:00
Ken McMillan
886128c989 hooked up array.weak and array.extension params 2013-06-14 16:33:51 -07:00
Nikolaj Bjorner
56bfc06c4f fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:55:15 -07:00
Nikolaj Bjorner
d569027e36 fix reference count bugs in overflow/underflow APIs for bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-02 20:54:01 -07:00
Nikolaj Bjorner
76a269c85a clean up parity computation 
Signed-off-by: unknown <nbjorner@NIKOLAJ-ZEN.redmond.corp.microsoft.com>
 2013-06-01 17:14:18 -07:00
Nikolaj Bjorner
c0895e5548 remove hassel table from unstable: does not compile under other plantforms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-31 17:48:19 -07:00
Nikolaj Bjorner
56dedec740 fix build break include uint_set.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-18 10:02:53 -07:00
Nikolaj Bjorner
ef2a9994a9 fix UTVPI model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-16 19:58:14 -07:00
Nikolaj Bjorner
69b7c3ede7 fixing parity bug in model generation for UTVPI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-05-16 15:36:27 -07:00