Christoph M. Wintersteiger
|
2b7f9b7e5c
|
build fix for floats
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 16:40:54 +00:00 |
|
Christoph M. Wintersteiger
|
80c025b289
|
Improved default tactic for QF_FP
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 16:15:55 +00:00 |
|
Christoph M. Wintersteiger
|
afae49b9ed
|
More renaming QF_FPA -> QF_FP
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 16:15:40 +00:00 |
|
Christoph M. Wintersteiger
|
21a847d299
|
More renamings for QF_FP/qffp/is-qffp
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 15:36:11 +00:00 |
|
Christoph M. Wintersteiger
|
208994e2dc
|
Renamed the default tactics form QF_FPA and QF_FPABV to QF_FP and QF_FPBV, in anticipation of the logic name QF_FPA to mean floats+arrays.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 15:33:50 +00:00 |
|
Christoph M. Wintersteiger
|
01d78b7274
|
added internal functions to fpa2bv converter
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 14:49:52 +00:00 |
|
Christoph M. Wintersteiger
|
4d18e24fb4
|
FPA rewriter bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 14:48:45 +00:00 |
|
Christoph M. Wintersteiger
|
2258988b37
|
MPF bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-31 14:48:06 +00:00 |
|
Christoph M. Wintersteiger
|
defb6158fe
|
MPF: bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-29 17:09:28 +00:00 |
|
Christoph M. Wintersteiger
|
33af7e8468
|
FPA: bugfixes for fp.to_ubv
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-29 17:09:18 +00:00 |
|
Christoph M. Wintersteiger
|
0ab2782048
|
FPA: name consistency
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-29 17:08:46 +00:00 |
|
Christoph M. Wintersteiger
|
05121e25d4
|
FPA theory support for conversion functions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 19:28:48 +00:00 |
|
Christoph M. Wintersteiger
|
621be0f47f
|
FPA: Added fp.to_ubv
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 18:01:18 +00:00 |
|
Christoph M. Wintersteiger
|
96c8bd7e91
|
MPF conversion bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 17:57:21 +00:00 |
|
Christoph M. Wintersteiger
|
12aaa0610b
|
FPA: added get_some_value/s for FP models
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 15:27:40 +00:00 |
|
Christoph M. Wintersteiger
|
4d1f71775d
|
FPA: added to_fp_unsigned
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 15:26:52 +00:00 |
|
Christoph M. Wintersteiger
|
1aae53f48c
|
FPA: comment fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 15:26:41 +00:00 |
|
Christoph M. Wintersteiger
|
23aa614d55
|
FPA: New theory implementation with support for "hidden" variables, relevancy, and eq/diseq.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:44:29 +00:00 |
|
Christoph M. Wintersteiger
|
7a15c41c47
|
FPA: improved error messages for to_fp
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:40:36 +00:00 |
|
Christoph M. Wintersteiger
|
d1cb2566e4
|
fpa2bv: adjustments for consistency
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:39:46 +00:00 |
|
Christoph M. Wintersteiger
|
55662bcf6b
|
fpa2bv: added reset(), adjustments for consistency
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:33:19 +00:00 |
|
Christoph M. Wintersteiger
|
6ebeebde50
|
Added parameter to display floating point numerals as reals
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:32:34 +00:00 |
|
Christoph M. Wintersteiger
|
7f8a34d2e1
|
Adjusted default model display for float literals.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-28 13:31:30 +00:00 |
|
Christoph M. Wintersteiger
|
65cc5fbe8b
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2014-12-27 11:09:03 +00:00 |
|
Christoph M. Wintersteiger
|
b8c373bbce
|
fpa2bv tactic bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-22 14:25:23 +00:00 |
|
Christoph M. Wintersteiger
|
9dd4d7b011
|
Python API bugfix. Thanks to Tom Ball for reporting this one.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 20:43:26 +00:00 |
|
Christoph M. Wintersteiger
|
0ceb67ae33
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2014-12-21 18:47:02 +00:00 |
|
Christoph M. Wintersteiger
|
cf4b7219e1
|
new theory_fpa. plenty of bugs remain.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 18:45:36 +00:00 |
|
Christoph M. Wintersteiger
|
d394b9579f
|
FPA: new conversion
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 18:45:05 +00:00 |
|
Christoph M. Wintersteiger
|
a1b4ef9e1b
|
fpa2bv refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 18:44:12 +00:00 |
|
Christoph M. Wintersteiger
|
d5fef38c00
|
FPA: Switched default value representation to 3-bitvector
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-21 18:43:22 +00:00 |
|
Christoph M. Wintersteiger
|
47325c5fd3
|
FPA: bugfixes, naming convention, core theory additions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-16 23:59:27 +00:00 |
|
Nikolaj Bjorner
|
18c3c1d9d6
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2014-12-16 11:21:24 -08:00 |
|
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 |
|
Christoph M. Wintersteiger
|
d53fdb2848
|
typo
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-16 15:36:31 +00:00 |
|
Christoph M. Wintersteiger
|
1244d5a22e
|
Python API: Added BVRedAnd, BVRedOr
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-16 15:28:52 +00:00 |
|
Christoph M. Wintersteiger
|
f11ee40c38
|
FPA: bug and leak fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-14 19:09:17 +00:00 |
|
Christoph M. Wintersteiger
|
4e913bb18c
|
FPA bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-14 17:34:18 +00:00 |
|
Christoph M. Wintersteiger
|
b30e61e528
|
FPA: bugfixes, leakfixes, added fp.to_real
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-13 19:34:55 +00:00 |
|
Christoph M. Wintersteiger
|
d6ac98a494
|
FPA API: reintroduced to_ieee_bv
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-11 12:05:52 +00:00 |
|
Christoph M. Wintersteiger
|
72dbb2a513
|
FPA API bugfix
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-10 20:04:24 +00:00 |
|
Christoph M. Wintersteiger
|
c2b5b6a36b
|
typo
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-10 19:45:18 +00:00 |
|
Christoph M. Wintersteiger
|
7965d24df8
|
FPA API: added conversion functions to float_decl_plugin
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-10 19:36:58 +00:00 |
|
Christoph M. Wintersteiger
|
657595818e
|
FPA API: Renaming for consistency with final SMT standard.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-10 18:45:44 +00:00 |
|
Christoph M. Wintersteiger
|
3418f1875e
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
|
2014-12-10 17:15:10 +00:00 |
|
Ken McMillan
|
882dbfc706
|
merge
|
2014-12-08 16:16:52 -08:00 |
|
Ken McMillan
|
8181b15a1b
|
attempted interp fixes
|
2014-12-08 15:46:55 -08:00 |
|
Nikolaj Bjorner
|
45755bbd14
|
fix context sensitivity. Codeplex issue 148, thanks to clockish
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
2014-12-03 08:55:14 +09:00 |
|
Christoph M. Wintersteiger
|
61c59fb4bf
|
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
|
2014-12-02 14:35:29 +00:00 |
|
Christoph M. Wintersteiger
|
c88b2f6b5e
|
.NET API: Added build instructions for .NET 3.5
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
|
2014-12-02 14:35:15 +00:00 |
|