mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
2127 commits 24 branches 48 tags 158 MiB
Commit graph

174 commits

Author SHA1 Message Date
Nikolaj Bjorner
b9bbfbdbb7 fix interval dependencies bug. Codeplex issue 163 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-16 12:05:12 +05:30
Nikolaj Bjorner
f4d256ef30 fix issue 153: assert rem/mod axiom no matter what is status of second argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-16 11:20:34 -08:00
Nikolaj Bjorner
cf8ad072d0 remove unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-11-07 16:03:27 +01:00
Ken McMillan
d815af9f0f merge duality changes with unstable 2014-10-22 10:14:05 -07:00
Nikolaj Bjorner
7767a23626 improve error messages on incorrect parameter passing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-15 21:37:37 -07:00
Nikolaj Bjorner
1bb4d52cb8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-07 15:38:57 -07:00
Nikolaj Bjorner
d6964226c7 indentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 15:38:44 -07:00
Nikolaj Bjorner
4ea3ed7e27 ensure parameters are updated and ensure that global use of auto-config is not obscured by smt.auto-config scoping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-10-07 11:00:45 -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
Ken McMillan
c5f17df310 fixing an assert caused by previous change in theory_array_base.cpp 2014-10-01 18:15:33 -07:00
Ken McMillan
4763532501 adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) 2014-09-30 11:25:47 -07:00
Ken McMillan
4c71e9479d optimizing array final check 2014-09-30 11:21:34 -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