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

1918 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
165da842b7 Numeral API: added floating-point numeral cases. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 13:12:44 +01:00
Christoph M. Wintersteiger
4af39b432c FPA API: dotnet bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 12:25:43 +01:00
Christoph M. Wintersteiger
cc5081587f FPA API: made FPA functions public 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-14 12:00:10 +01:00
Christoph M. Wintersteiger
8b43a1b5f6 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-14 11:35:22 +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
Christoph M. Wintersteiger
ab462dd1cb Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-10 19:07:10 +01:00
Christoph M. Wintersteiger
a9840b291f FPA API: Tied into rest of the API; 
added numeral/value handling through existing functions;
added trivial .NET example.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-10 19:06:45 +01:00
Christoph M. Wintersteiger
e14819c1b1 FPA: Added .NET API calls 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-10 15:54:20 +01:00
Christoph M. Wintersteiger
a36a09e081 FPA API: minor fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-10 15:53:41 +01:00
Christoph M. Wintersteiger
ebbdff8757 doc bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-10 15:53:24 +01: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
573ec293dc FPA: Added core C API. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-07 19:09:41 +01:00
Christoph M. Wintersteiger
dd6dc5e165 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-07 18:34:57 +01: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
bc4da23037 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-07 18:06:41 +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
73b2abef88 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-07 17:37:40 +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
Christoph M. Wintersteiger
a88a15ac67 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-07 12:21:06 +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
Christoph M. Wintersteiger
9b13ca5260 Added first FPA API functions. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-06 14:50:01 +01:00
Christoph M. Wintersteiger
3f50750d1f Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2013-06-06 14:10:20 +01: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
Christoph M. Wintersteiger
d301bd35a9 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-05 14:36:18 +01:00
Ken McMillan
418f148ecf working on incremental stratified inlining in duality 2013-06-04 18:22:54 -07:00
Nikolaj Bjorner
b6d9d8a601 fix bugs reported by Nuno Lopes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-04 12:55:35 -07:00
Nikolaj Bjorner
aa0d921240 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-03 11:48:21 -07:00
Nikolaj Bjorner
bd064bf5d0 enable UTVPI by default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2013-06-03 11:46:13 -07:00
Christoph M. Wintersteiger
093fe945bc FPA: min/max/fma bugfixes + partial quantifier support 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:19:45 +01:00
Christoph M. Wintersteiger
7c32df93a4 SLS tactic: compilation fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-06-03 18:17:41 +01: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
89d8970d41 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2013-06-02 12:03:01 -07:00