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