mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
3559 commits 24 branches 48 tags 158 MiB
Commit graph

3559 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
f684675a6e FPA API: Added get_ebits/get_sbits + doc fixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:58:43 +00:00
Christoph M. Wintersteiger
09814128a6 Update MPF toString 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:57:38 +00:00
Christoph M. Wintersteiger
e1e594be75 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2015-01-02 18:11:16 +00:00
Christoph M. Wintersteiger
8e7278f02c Java API: Removed unnecessary imports 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-02 18:10:47 +00:00
Christoph M. Wintersteiger
b46d76cddb New FPA C-API example 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 19:16:44 +00:00
Christoph M. Wintersteiger
6e849d7f73 FPA API cosmetics 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 19:16:02 +00:00
Christoph M. Wintersteiger
076c709453 cosmetics 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 19:00:06 +00:00
Christoph M. Wintersteiger
09247d2e29 FPA theory and API overhaul 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 18:44:41 +00:00
Christoph M. Wintersteiger
a28454d95e FPA: sort names consistency fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 15:24:36 +00:00
Christoph M. Wintersteiger
97df505dba MPF consistency fix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 15:23:27 +00:00
Christoph M. Wintersteiger
4f453703f7 Added arguments of type float to the replayer. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-01 15:23:02 +00:00
Christoph M. Wintersteiger
7d61223a3a Improved FP theory 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-31 18:34:42 +00:00
Christoph M. Wintersteiger
3fe11e4c38 improved handling of unspecified values in FP 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-31 17:31:11 +00:00
Christoph M. Wintersteiger
7a5239ef70 QF_FP default tactic bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-31 17:30:45 +00:00
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
Nikolaj Bjorner
a296023823 incorrect offset calculation in diff logic optimization. codeplex issue 156 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-29 16:15:19 -08:00
Nikolaj Bjorner
7d62ceeadc Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-12-29 12:57:17 -08:00
Nikolaj Bjorner
c54a19b084 generate proof justifications in theory_pb: codeplex issue 157 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-29 12:57:02 -08: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
Nuno Lopes
a211fcfb9e muZ/datalog/udoc: fix bug in join_project 
The bug was that we could project out don't care columns and don't take copied bits into account.
Bug reported by Ari Fogel

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-12-28 17:05:17 +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
Nikolaj Bjorner
d827713ce3 revert to SMT tactic on bv1_blaster_tactic - equalities are not removed, and conjunctions are not converted to NNF (or/not), so the formula still isn't sufficiently blasted 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-22 15:40:02 -08:00
Nikolaj Bjorner
f373996f09 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-12-22 09:27:48 -08:00
Nikolaj Bjorner
c61e9f27db local changes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2014-12-22 09:27:33 -08: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
Nuno Lopes
ee71c434b6 muZ/datalog: remove a few spurious make_empty() calls from the instruction handlers 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-12-22 14:17:07 +00:00
Nuno Lopes
dddb31fc37 minor optimization to previous patch 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-12-22 13:03:06 +00:00
Nuno Lopes
4ee83c1774 Datalog/DoC: add fast path for join_project for the case 'h(X) :- f(X), g(X).' 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2014-12-22 12:53:35 +00:00
Nuno Lopes
a7c7b70e19 muZ Datalog: be more aggressive when forming join_project 2014-12-22 12:49:31 +00:00