mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-04 23:13:57 +00:00
Code Activity
7388 commits 26 branches 52 tags 171 MiB
Commit graph

1114 commits

Author SHA1 Message Date
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -07:00
Christoph M. Wintersteiger
c8af48d7ef Bugfix for bvurem0 model evaluation (+1 rewriting step) 2016-03-17 13:09:52 +00:00
Christoph M. Wintersteiger
6b2d84b2be Fixed model evaluation/simplification for to_ieee_bv. 2016-03-16 17:46:52 +00:00
Christoph M. Wintersteiger
7ec70c1686 bug fixes for unspecified FP results 2016-03-16 16:57:20 +00:00
Christoph M. Wintersteiger
db6b9faabc Bugfix for FPA rewriter. 2016-03-16 16:35:45 +00:00
Christoph M. Wintersteiger
778c7fcc64 Bugfix for model evaluator and internal, uninterpreted FPA functions. 
Fixes #518
 2016-03-16 16:17:08 +00:00
Christoph M. Wintersteiger
cdc8e1303a Bugfix for fp.to_*_unspecified. 
Fixes #507
 2016-03-16 16:16:29 +00:00
Christoph M. Wintersteiger
99d7a47f82 Bugfixes for unspecified results from fp.to_* (models are still incomplete). 
Relates to #507
 2016-03-15 21:45:54 +00:00
Christoph M. Wintersteiger
3101d281e4 Removed unused variable 2016-03-15 15:12:54 +00:00
Christoph M. Wintersteiger
371573cbff More implementation of fp.to_ieee_bv for unspecified input/output 
Relates to #507
 2016-03-15 15:11:37 +00:00
Christoph M. Wintersteiger
a9df4a208f More bugfixes for fp.to_ieee_bv for unspecified input/output. 
Relates to #507
 2016-03-15 14:58:55 +00:00
Christoph M. Wintersteiger
ce64999ee2 More bugfixes for fp.to_ieee_bv for unspecified input/output 2016-03-15 14:50:59 +00:00
Christoph M. Wintersteiger
176782d62b Bugfix for fp.to_ieee_bv for unspecified input/output. 2016-03-15 14:38:11 +00:00
Christoph M. Wintersteiger
5463167a84 Bugfix for fp.rem (denormal numbers) 
Fixes #508.
 2016-03-14 15:52:09 +00:00
Christoph M. Wintersteiger
badf9e6e67 whitespace 2016-03-11 14:05:32 +00:00
Christoph M. Wintersteiger
3e61ee2331 disabled "hardware interpretation" of fp.min/fp.max because the unspecified, standard-compliant behaviour is cheap anyways. 2016-03-11 12:52:00 +00:00
Christoph M. Wintersteiger
b5279d1da8 Bugfix for fp.to_ieee_bv. 
Fixes #507.
 2016-03-11 12:35:41 +00:00
Nuno Lopes
d0de8fff62 ensure ast_manager::are_equal returns true if expr ptrs are equal 
found by Nikolaj
 2016-03-08 16:53:09 +00:00
Nuno Lopes
9c620376c2 simplify ast::are_equal(), since pointer equality is sufficient 2016-03-07 13:15:12 +00:00
Nikolaj Bjorner
aa1ddd169a fix bug in offset for shift amount for free bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 15:25:14 -08:00
Nikolaj Bjorner
640308b546 make proto-model evaluation use model_evaluator instead of legacy evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 10:27:19 -08:00
Nikolaj Bjorner
70f13ced33 make proto-model evaluation use model_evaluator instead of legacy evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-05 10:14:15 -08:00
Christoph M. Wintersteiger
f34e15f289 whitespace 2016-03-05 16:47:39 +00:00
Christoph M. Wintersteiger
9dfc2bc61e Fixed memory leaks in fpa2bv converter. 
Fixes #480
 2016-03-05 16:47:08 +00:00
Zephyr Pellerin
b13db1e82e Bugfix for arith_rewriter single operand division 2016-03-04 18:26:00 -08:00
Nikolaj Bjorner
50b2389e7f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-03 07:59:13 -08:00
Nikolaj Bjorner
7c6540e18f recursive function definitions; combine model-building functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-03 07:59:03 -08:00
Christoph M. Wintersteiger
dbf9609b4c added assertion 2016-03-02 18:06:14 +00:00
Christoph M. Wintersteiger
f128c76f23 whitespace 2016-03-02 18:05:14 +00:00
Nikolaj Bjorner
67397bf71e enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:48:24 -08:00
Nuno Lopes
006dc147a8 fix build with gcc 5 2016-02-29 14:34:48 +00:00
Nikolaj Bjorner
df2d7e7628 add intersection using symbolic automata facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-28 17:05:12 -08:00
Nikolaj Bjorner
ce8862d415 fix bug in conflict clause generation in seq-branch-variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-26 18:15:45 -08:00
Nikolaj Bjorner
d5383e2387 fix bug in definition of rewrite rule for replace, tighten constraints for tightest-prefix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-23 18:41:56 -08:00
Nuno Lopes
73da4dda07 add a bv rewrite pattern: 
(bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
 2016-02-18 17:45:55 +00:00
Nikolaj Bjorner
e2dc7c6f64 add note that current re.complement is non-standard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 17:12:43 +00:00
Nikolaj Bjorner
94453033b6 add partial support for complementation of regular expressions. Handles case of complementing character ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 15:59:33 +00:00
Nuno Lopes
564343c39c remove unused methods in ast.cpp 2016-02-09 15:30:05 +00:00
Nikolaj Bjorner
60c0e73b2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 11:08:52 +00:00
Nikolaj Bjorner
133e3693de fix bug in replace built-in and move length-equality propagation to branch final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 11:08:33 +00:00
Christoph M. Wintersteiger
92b6a3e134 Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). 
Fixes #439.
 2016-02-07 17:33:33 +00:00
Christoph M. Wintersteiger
e9d94e53f6 Improved FPA simplifier plugin 2016-02-07 15:01:22 +00:00
Christoph M. Wintersteiger
37b11cdc74 Comments, whitespace. 2016-02-07 15:01:09 +00:00
Nikolaj Bjorner
fc1f37efc9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-06 16:14:07 +00:00
Nikolaj Bjorner
5b50d98b89 ensure that seq rewriter gets invoked during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-06 16:13:31 +00:00
Christoph M. Wintersteiger
7ddd2856c8 Added is_considered_uninterpreted() to decl_plugins. 2016-02-05 15:22:37 +00:00
Christoph M. Wintersteiger
3d37c25bcc whitespace 2016-02-05 15:16:54 +00:00
Christoph M. Wintersteiger
c11b6d90ce whitespace 2016-02-05 15:16:19 +00:00
Christoph M. Wintersteiger
ac19bfb032 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 13:53:41 +00:00
Christoph M. Wintersteiger
bb5118acbb Bugfix for bv*div0 model construction. 2016-02-05 13:53:35 +00:00