mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity
1558 commits 23 branches 48 tags 157 MiB
Commit graph

1558 commits

This branch
This branch
All branches
Author SHA1 Message Date
Ken McMillan f45ad4bdc0 disable silly warnings and add needed header for VS 2014-02-10 12:56:39 -08:00
Ken McMillan 19830bcd33 fix a few warnings 2014-01-28 11:43:00 -08:00
Ken McMillan 466c35100d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-28 11:28:24 -08:00
Christoph M. Wintersteiger f111dd4e61 Fixes for the build on OS X 10.9 2014-01-28 14:00:42 +00:00
Christoph M. Wintersteiger 0e74362ecb Added support for the final draft of the FPA standard (and fpa2bv conversion). 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-01-24 15:36:23 +00:00
Christoph M. Wintersteiger b2be81fd4d bugfix for OSX build configuration 2014-01-22 13:41:48 +00:00
Christoph M. Wintersteiger 73a1dddc45 Bugfixes for the build on new OSX machines (XCode 5.0 on). 2014-01-21 17:06:13 +00:00
Nikolaj Bjorner d548c51a98 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-01-13 13:42:15 -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 da4793de76 fix type checking bug reported by Nate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-09 21:14:30 -08:00
Ken McMillan f380e31a6b runs the integer/cntrol svcomp examples from the Horn repo 2014-01-09 17:16:10 -08:00
Nikolaj Bjorner 084a6f35eb fix bug reported by Nuno Lopes: inlining is unsound for negated predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-01-02 17:37:35 -08:00
Nikolaj Bjorner 81f1f7690d fix bug in rational.is_int32, it recognized rationals; fix bug reported by Anvesh for integer arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-12-31 15:59:56 -08:00
Ken McMillan 11ba2178a9 speeding up interpolation in RPFP_caching 2013-12-24 17:20:12 -08:00
Ken McMillan 1b9f1ea6b3 remove assert on failed label compuation in duality 2013-12-23 11:47:24 -08:00
Ken McMillan 673ba137e5 added qe_lite preprocessing pass to duality 2013-12-23 11:17:38 -08:00
Ken McMillan 9e88691c69 optimizing solver performance in duality 2013-12-22 18:33:40 -08:00
Ken McMillan c98b853917 speeding up Generalize and adding Lazy Propagation 2013-12-21 16:54:35 -08:00
Ken McMillan 48e10a9e2d dealing with incompleteness issues in duality 2013-12-19 11:05:56 -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
Christoph M. Wintersteiger 8fb36bd41d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-17 13:53:28 +00:00
Christoph M. Wintersteiger 0b3e50d6e6 Added #include <algorithm> because VS2013 needs that for std::max/std::min 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-17 13:53:10 +00:00
Ken McMillan a318b0f104 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-12-16 12:45:52 -08:00
Ken McMillan 3588d4a1ca fixing templates for broken windows hash functions 2013-12-16 12:41:43 -08:00
Ken McMillan 1e8c04be8e fixing templates for broken windows hash functions 2013-12-15 17:31:46 -08:00
Ken McMillan 852f53d6a6 fixed memory error 2013-12-15 17:24:51 -08:00
Ken McMillan ebc8a43fe3 removing address dependencies 2013-12-15 15:49:06 -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 eee2d7af94 porting to linux 2013-12-14 12:47:02 -08:00
Ken McMillan 3764064e98 fixed some address dependencies 2013-12-13 18:41:35 -08:00
Ken McMillan bb61f17989 trying to figure out address dependency 2013-12-13 13:45:40 -08:00
Ken McMillan ac9a7748e8 trying to fix address depedency in duality_solver.cpp 2013-12-13 13:14:04 -08:00
Ken McMillan 0449598530 fussing more with qe in duality 2013-12-13 12:41:51 -08:00
Ken McMillan a410e7f716 fussing with qe in duality 2013-12-13 12:21:54 -08:00
Ken McMillan bfa6c99676 still trying to get stl to work 2013-12-12 18:38:09 -08:00
Ken McMillan cf3ede92ad fix for broken windows stl 2013-12-12 18:35:43 -08:00
Ken McMillan 2cc8132191 still simplifying quantified interpolants in duality 2013-12-12 18:25:24 -08:00
Ken McMillan ea8eb74744 simplifying quantified interpolants in duality 2013-12-11 16:25:59 -08:00
Ken McMillan d45cbb3cb2 fixed interpolation bug 2013-12-10 16:26:35 -08:00
Ken McMillan 7043386915 enabled extensional arrays in duality and added theory axioms lazily in GreedyReduce 2013-12-10 14:34:14 -08:00
Ken McMillan 56b3406ee5 added mbqi.id option, working on quantifiers in duality 2013-12-10 11:41:25 -08:00
Christoph M. Wintersteiger a533527004 exception message clarity fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-12-05 12:45:14 +00:00
Ken McMillan a3462ba6aa working on duality 2013-11-27 17:39:49 -08:00
Ken McMillan a93f8b04e5 working on duality and quantified arithmetic in interpolation 2013-11-21 18:10:21 -08:00
Nikolaj Bjorner 61385c8489 a.ctx -> self.ctx, thanks gario 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-11-20 09:54:37 -08:00
Ken McMillan 8320144af0 fixed bug in duality logging 2013-11-15 11:24:02 -08:00
Christoph M. Wintersteiger 31495bb9d9 bugfix for float rounding to integral values for cases where ebits >= sbits 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-15 17:19:41 +00:00
Christoph M. Wintersteiger c96f7b5a51 bugfixes for float to float conversion 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-14 20:13:37 +00:00
Christoph M. Wintersteiger b77d408128 bugfix for FPA rounding when ebits is very small. 2013-11-14 19:11:19 +00:00
Christoph M. Wintersteiger bb8373151d Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-11-14 19:09:30 +00:00