mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 07:23:58 +00:00
Code Activity
5535 commits 28 branches 52 tags 171 MiB
Commit graph

289 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
bd94b59a92 Bugfix for arith rewriter to avoid rewriting loops. 2015-11-03 13:00:10 +00:00
Christoph M. Wintersteiger
27140c527c trailing whitespace 2015-11-03 12:56:29 +00:00
Christoph M. Wintersteiger
92152b16ca Bugfixes for model verification of unspecified values of fp.min/fp.max 2015-11-02 19:25:44 +00:00
Nikolaj Bjorner
7838213675 eliminate to_real coersions to make mixed integer problems easier to digest. Issue #277 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-30 15:12:21 -07:00
Christoph M. Wintersteiger
8fffa9f188 Removed trailing whitespace. 2015-10-30 12:20:41 +00:00
Christoph M. Wintersteiger
9b5abcd55a Improved support for FPA unspecified min/max values, model validation, and proof generation. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger
ca496f20cb Partial refactoring of fpa2bv conversion to support proofs. 2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger
099775947e Partial fix for fp,min/fp.max models 2015-10-25 13:10:40 +00:00
Nuno Lopes
0e387b2abe use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-10-09 18:06:49 +01:00
Christoph M. Wintersteiger
de39173f6f Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa. 
Fixes #68
 2015-10-07 20:44:08 +01:00
Christoph M. Wintersteiger
8a026c355f Corrected unspecified behavior of corner cases in fp.min/fp.max. 
Partially addresses #68.
 2015-10-07 20:39:36 +01:00
Nikolaj Bjorner
d9b6623400 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:16:46 -07:00
Nikolaj Bjorner
9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
Christoph M. Wintersteiger
79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00
Christoph M. Wintersteiger
a1073206f9 Bugfix for FP rewriter. 2015-09-15 16:23:24 +01:00
Christoph M. Wintersteiger
25f75b60fe Bugfix for fp.mul and fp.fma for small numbers of e/s bits. 
Fixes #215.
 2015-09-10 11:37:06 +01:00
Nikolaj Bjorner
cc5d719d9e enable incremental bit-vector solving 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-01 09:48:35 -07:00
Nikolaj Bjorner
ef7915858b add filter to detect circumventing the default semantics of bit-vector division with the use of the sat-based bit-vector solver. Provides a way to fix issue #190 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-24 16:27:07 -07:00
Nikolaj Bjorner
8505ca843b recognize more pb patterns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-08 13:39:39 +02:00
Nikolaj Bjorner
4bc044c982 update header guards to be C++ style. Fixes issue #9 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-07-08 23:18:40 -07:00
Nuno Lopes
b65d5797f8 optimize expr_safe_replace for when a subexpression has no substitutions 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-03 17:21:01 +01:00
Christoph M. Wintersteiger
fec815b41e Various variable renamings to avoid conflicts with previously defined local variables, function parameters, or members (Visual Studio 2015 warnings). 2015-05-29 18:13:39 +01:00
Christoph M. Wintersteiger
9428acd578 Bugfix for FPA rewriter. 2015-05-29 13:58:33 +01:00
Christoph M. Wintersteiger
7619d609f9 FPA min/max -+0.0 special cases changed to +0.0 instead of second argument. 
Fixes #68
 2015-05-28 12:20:48 +01:00
Christoph M. Wintersteiger
eee076b9f8 Bugfixes for fp.min, fp.max. 
Fixes the fix for #68
 2015-05-21 18:16:02 +01:00
Matthias Schlaipfer
c82319b358 Refactor count_vars and count_rule_vars 
ast_manager m was not used
 2015-05-14 17:04:38 +01:00
Nikolaj Bjorner
ab5022888c Merge branch 'opt' of https://github.com/Z3Prover/z3 into unstable 2015-05-14 12:11:17 +01:00
Christoph M. Wintersteiger
73eb7cbf5c Bugfix for mpf roundToIntegral. 
Partially fixes #69
 2015-05-05 23:53:33 +01:00
Christoph M. Wintersteiger
57af3a4c6e FPA min/max refactoring and fixes. 
Fixes #68

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-05-04 13:47:04 +01:00
Nikolaj Bjorner
9377779e58 merge with unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-30 10:40:03 -07:00
Nikolaj Bjorner
6c1a5390ef fix big-int bug for shift amounts, github issue 44, reported by Dejan 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-04-20 10:20:06 +02:00
Nikolaj Bjorner
52619b9dbb pull unstable 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
 2015-04-01 14:57:11 -07:00
Nuno Lopes
5676fbbc9e compiler love: make a few symbols static and avoid unneeded relocations 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
 2015-02-22 11:13:51 +00:00
Christoph M. Wintersteiger
359c7e4da9 Removed unnecessary variables and added initialization to others to silence warnings. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-07 14:47:26 +00:00
Christoph M. Wintersteiger
941d1063dd FPA rewriter and MPF bugfixes 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-06 18:48:14 +00:00
Christoph M. Wintersteiger
5e60bcd920 FPA: fixes for the fpa_rewriter to enable model extraction and validation. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-06 16:53:31 +00:00
Christoph M. Wintersteiger
a4c599a435 typo 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-02-04 18:25:32 +00:00
Christoph M. Wintersteiger
95300e801d fixed build errors and warnings 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-21 18:24:36 +00:00
Christoph M. Wintersteiger
5344d6f3c0 various bugfixes and extensions for FPA 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-15 19:25:49 +00:00
Christoph M. Wintersteiger
0381e4317a Formatting, mostly tabs. 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 17:54:04 +00:00
Christoph M. Wintersteiger
c0bc2518b0 Renaming for consistency mk_value -> mk_numeral 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:22:44 +00:00
Christoph M. Wintersteiger
c0a027fc80 FPA: Elminated nzero/pzero AST kinds 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 14:07:47 +00:00
Christoph M. Wintersteiger
5e5758bb25 More float -> fpa renaming 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 13:37:18 +00:00
Christoph M. Wintersteiger
dd17f3c7d6 Renaming floats, float, Floats, Float -> FPA, fpa 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2015-01-08 13:18:56 +00:00
Nikolaj Bjorner
129e048a1b Adding field update feature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-01-03 01:27:52 -08: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
d394b9579f FPA: new conversion 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2014-12-21 18:45:05 +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
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
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