mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
1628 commits 46 branches 52 tags 178 MiB
Commit graph

1628 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
a9c4470a6b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-25 14:53:28 +01:00
Leonardo de Moura
efb6b2453e Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-24 15:37:49 -07:00
Leonardo de Moura
205520ed6c Move AssemblyInfo.cs AssemblyInfo. Update mk_util.py to generate AssemblyInfo.cs instead of modifying it. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-24 15:34:42 -07:00
Christoph M. Wintersteiger
127402c10b FPA: fpa2bv fma bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 16:33:09 +01:00
Christoph M. Wintersteiger
9581055f97 FPA: debug output disabled 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 13:30:36 +01:00
Christoph M. Wintersteiger
13206f2fe7 FPA: FMA bugfixes. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-24 13:29:04 +01:00
Nikolaj Bjorner
5b5a474b54 experiment with point-based generalization method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-21 16:23:37 -07:00
Christoph M. Wintersteiger
9489c9b08b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-21 21:16:12 +01:00
Christoph M. Wintersteiger
0b6250253a FPA2BV: added sqrt function 
(Currently, there are a few corner cases where it doesn't round correctly.)

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-21 21:16:03 +01:00
Leonardo de Moura
42898f3276 Fix bug reported by Florian <corzilius@cs.rwth-aachen.de> 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-21 10:31:11 -07:00
Leonardo de Moura
a60b53bfd8 Fix compilation errors/warnings when using GCC 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:52:20 -07:00
Leonardo de Moura
f5f04e583b Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-20 17:48:57 -07: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
Leonardo de Moura
cd485f03dd Add trace msg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-20 17:02:15 -07:00
Ken McMillan
1578a7fd95 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-18 12:29:58 -07:00
Ken McMillan
0f13ec6e42 adding timeout to duality 2013-06-18 12:28:20 -07:00
Ken McMillan
c448b2a430 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-17 18:07:23 -07:00
Ken McMillan
64acd9cac0 fixed some bugs with quantifiers in rule bodies 2013-06-17 18:04:23 -07:00
Ken McMillan
7a85c8951e Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-14 16:46:41 -07:00
Ken McMillan
a78564145b hooked up array.weak and array.extension params 2013-06-14 16:46:13 -07:00
Ken McMillan
782ffc32e8 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-14 16:34:41 -07:00
Ken McMillan
886128c989 hooked up array.weak and array.extension params 2013-06-14 16:33:51 -07:00
Christoph M. Wintersteiger
ecceb0accc FPA: debug output disabled. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:16:02 +01:00
Christoph M. Wintersteiger
92c1b25978 FPA: bugfix for float to float conversion (subnormal numbers). 
Thanks to Gabriele Paganelli for reporting this bug!

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 20:14:00 +01:00
Christoph M. Wintersteiger
76c59cb85c MPF conversion bugfix. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 17:22:25 +01:00
Christoph M. Wintersteiger
1a26c9726b .NET API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 13:15:48 +01:00
Leonardo de Moura
894fd8b967 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-13 13:45:55 -07:00
Leonardo de Moura
40b1137b30 Fix issue https://z3.codeplex.com/workitem/47 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-13 13:45:14 -07:00
Leonardo de Moura
2c8b314a15 Fix issue https://z3.codeplex.com/workitem/48 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-13 13:34:20 -07:00
Nikolaj Bjorner
6184c5fdbc reorder attibutes to match initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-11 15:29:22 -04:00
Ken McMillan
a4584f4eaa Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-10 14:46:40 -07:00
Ken McMillan
30a4627a1e fixed problem with nullary background constants in duality 2013-06-10 14:46:15 -07:00
Nikolaj Bjorner
0210156bf0 add convex interior generalizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-10 10:51:56 -04:00
Ken McMillan
a6d61e3404 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-07 16:17:16 -07:00
Ken McMillan
c21cd6ffa5 fixed model completion problem in duality 2013-06-07 16:16:56 -07:00
Ken McMillan
b78752ef04 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-07 11:51:33 -07:00
Ken McMillan
adb1f95e0a small fixes in duality 2013-06-07 11:51:22 -07:00
Ken McMillan
40fe1f6e99 adjusting stratified inlining in duality 2013-06-07 11:50:01 -07:00
Christoph M. Wintersteiger
455618bb2b FPA: added is_nan 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:34:31 +01:00
Christoph M. Wintersteiger
d7639557d2 FPA: added rewriting and fpa2bv conversion rules for new operations. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 18:03:46 +01:00
Christoph M. Wintersteiger
123d3ec3a7 New FPA operators added. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:55:29 +01:00
Christoph M. Wintersteiger
e5c720de29 FPA: bugfix for abs 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 17:36:34 +01:00
Christoph M. Wintersteiger
724f2af8c7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-07 17:34:38 +01:00
Leonardo de Moura
2b59f2ecc2 Fix issue https://z3.codeplex.com/workitem/37 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 18:29:29 -07:00
Leonardo de Moura
f4f1c63abb Fix issue https://z3.codeplex.com/workitem/38 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-06 13:20:43 -07:00
Ken McMillan
c57509d795 Merge branch 'interp' of https://git01.codeplex.com/z3 into interp 2013-06-05 18:02:14 -07:00
Ken McMillan
de7a675afa a mistake 2013-06-05 18:02:07 -07:00
Ken McMillan
97a7ae1589 add profiling option 2013-06-05 18:01:05 -07:00
Ken McMillan
c3eae9bf2a working on incremental stratified inlining in duality 2013-06-05 17:02:13 -07:00
Leonardo de Moura
110fa0b7fb Fix issue http://z3.codeplex.com/workitem/45 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-06-05 13:50:22 -07:00