1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     float_rewriter.h
7 
8 Abstract:
9 
10     Basic rewriting rules for floating point numbers.
11 
12 Author:
13 
14     Leonardo (leonardo) 2012-02-02
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "ast/rewriter/rewriter.h"
23 #include "ast/fpa_decl_plugin.h"
24 #include "ast/expr_map.h"
25 #include "util/params.h"
26 #include "util/mpf.h"
27 
28 class fpa_rewriter {
29     fpa_util      m_util;
30     mpf_manager & m_fm;
31     bool          m_hi_fp_unspecified;
32 
33     app * mk_eq_nan(expr * arg);
34     app * mk_neq_nan(expr * arg);
35 
36     br_status mk_to_bv(func_decl * f, expr * arg1, expr * arg2, bool is_signed, expr_ref & result);
37     br_status mk_to_bv_unspecified(func_decl * f, expr_ref & result);
38 
39 public:
40     fpa_rewriter(ast_manager & m, params_ref const & p = params_ref());
41     ~fpa_rewriter();
42 
m()43     ast_manager & m() const { return m_util.m(); }
get_fid()44     family_id get_fid() const { return m_util.get_fid(); }
45 
46     void updt_params(params_ref const & p);
47     static void get_param_descrs(param_descrs & r);
48 
49     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
50     br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
51 
52     br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
53     br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
54     br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
55     br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
56     br_status mk_neg(expr * arg1, expr_ref & result);
57     br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
58     br_status mk_abs(expr * arg1, expr_ref & result);
59     br_status mk_min(expr * arg1, expr * arg2, expr_ref & result);
60     br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
61     br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
62     br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
63     br_status mk_round_to_integral(expr * arg1, expr * arg2, expr_ref & result);
64     br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
65     br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
66     br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);
67     br_status mk_le(expr * arg1, expr * arg2, expr_ref & result);
68     br_status mk_ge(expr * arg1, expr * arg2, expr_ref & result);
69     br_status mk_is_zero(expr * arg1, expr_ref & result);
70     br_status mk_is_nzero(expr * arg1, expr_ref & result);
71     br_status mk_is_pzero(expr * arg1, expr_ref & result);
72     br_status mk_is_nan(expr * arg1, expr_ref & result);
73     br_status mk_is_inf(expr * arg1, expr_ref & result);
74     br_status mk_is_normal(expr * arg1, expr_ref & result);
75     br_status mk_is_subnormal(expr * arg1, expr_ref & result);
76     br_status mk_is_negative(expr * arg1, expr_ref & result);
77     br_status mk_is_positive(expr * arg1, expr_ref & result);
78 
79     br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
80     br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
81 
82     br_status mk_bv2rm(expr * arg, expr_ref & result);
83     br_status mk_fp(expr * sgn, expr * exp, expr * sig, expr_ref & result);
84     br_status mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
85     br_status mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
86     br_status mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result);
87     br_status mk_to_real(expr * arg, expr_ref & result);
88     br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
89     br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result);
90 
91     br_status mk_bvwrap(expr * arg, expr_ref & result);
92 };
93 
94