ir_ieee_conv.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_FP_IR_IEEE_CONV_H_
#define SOLVERS_SMT_FP_IR_IEEE_CONV_H_
 
#include <solvers/smt/smt_ast.h>
#include <irep2/irep2_expr.h>
#include <irep2/irep2_type.h>
#include <string>
#include <unordered_map>
#include <unordered_set>
#include <utility>
 
class smt_solver_baset;

class ir_ieee_convt
{
public:
  explicit ir_ieee_convt(smt_solver_baset *ctx);

  struct ra_interval_t
  {
    smt_astt lo;
    smt_astt hi;
  };

  void propagate_interval(smt_astt lhs, smt_astt rhs);

  void assert_symbol_range(
    const std::string &name,
    smt_astt sym_ast,
    const symbol2t &sym);

  void assert_representable_magnitude(
    smt_astt sym_ast,
    const floatbv_type2t &fbv_type);

  ra_interval_t get_interval(smt_astt t) const;

  void store_interval(smt_astt t, smt_astt lo, smt_astt hi);

  smt_astt encode_ieee_add(const expr2tc &expr);

  smt_astt encode_ieee_sub(const expr2tc &expr);

  smt_astt encode_ieee_mul(const expr2tc &expr);

  smt_astt encode_ieee_div(const expr2tc &expr);

  smt_astt encode_ieee_fma(const expr2tc &expr);

  smt_astt encode_ieee_rem(const expr2tc &expr);

  void store_nan_pred(smt_astt t, smt_astt nan_pred);

  smt_astt get_nan_pred(smt_astt t) const;

  void propagate_nan_pred(smt_astt lhs, smt_astt rhs);

  smt_astt apply_nan_cmp(smt_astt cmp, smt_astt a, smt_astt b, bool is_neq);

  smt_astt combine_nan_preds(smt_astt a, smt_astt b) const;

  void store_neg_zero_pred(smt_astt t, smt_astt neg_zero_pred);

  smt_astt get_neg_zero_pred(smt_astt t) const;

  void propagate_neg_zero_pred(smt_astt lhs, smt_astt rhs);

  void propagate_neg_zero_through_ite(
    smt_astt outer,
    smt_astt inner,
    smt_astt guard);

  std::pair<smt_astt, smt_astt> apply_ieee754_rne_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type);

  std::pair<smt_astt, smt_astt> apply_ieee754_rna_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type);

  std::pair<smt_astt, smt_astt> apply_ieee754_rup_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type);

  std::pair<smt_astt, smt_astt> apply_ieee754_rdn_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type);

  std::pair<smt_astt, smt_astt> apply_ieee754_rtz_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type);
 
private:
  smt_solver_baset *ctx;

  std::unordered_map<const smt_ast *, ra_interval_t> ir_ra_interval_map;

  std::unordered_map<const smt_ast *, smt_astt> ir_ieee_nan_map;

  std::unordered_map<const smt_ast *, smt_astt> ir_ieee_neg_zero_map;

  std::unordered_set<std::string> ir_ieee_ranged_syms;

  void store_combined_nan_pred(smt_astt result, smt_astt s1, smt_astt s2);

  smt_astt get_max_normal_real(const floatbv_type2t &fbv_type) const;

  smt_astt is_pos_inf_real(smt_astt x, const floatbv_type2t &fbv_type) const;

  smt_astt is_neg_inf_real(smt_astt x, const floatbv_type2t &fbv_type) const;

  smt_astt is_inf_real(smt_astt x, const floatbv_type2t &fbv_type) const;

  std::pair<smt_astt, smt_astt> apply_enclosure(
    smt_astt real_result,
    smt_astt lo_r,
    smt_astt hi_r,
    const floatbv_type2t &fbv_type,
    const expr2tc &rounding_mode);

  std::pair<smt_astt, smt_astt> widen_for_flush(smt_astt lo, smt_astt hi);
};
 
#endif /* SOLVERS_SMT_FP_IR_IEEE_CONV_H_ */