fp_conv.h

Go to the documentation of this file.

#ifndef SOLVERS_SMT_FP_CONV_H_
#define SOLVERS_SMT_FP_CONV_H_
 
#include <solvers/smt/smt_ast.h>
#include <solvers/smt/smt_sort.h>
 
class fp_convt
{
public:
  explicit fp_convt(smt_solver_baset *_ctx);
  virtual ~fp_convt() = default;

  virtual smt_astt mk_smt_fpbv(const ieee_floatt &thereal);

  virtual smt_sortt mk_fpbv_sort(const unsigned ew, const unsigned sw);

  virtual smt_sortt mk_fpbv_rm_sort();

  virtual smt_astt mk_smt_fpbv_nan(bool sgn, unsigned ew, unsigned sw);

  virtual smt_astt mk_smt_fpbv_inf(bool sgn, unsigned ew, unsigned sw);

  virtual smt_astt mk_smt_fpbv_rm(ieee_floatt::rounding_modet rm);

  virtual smt_astt
  mk_smt_typecast_from_fpbv_to_ubv(smt_astt from, std::size_t width);

  virtual smt_astt
  mk_smt_typecast_from_fpbv_to_sbv(smt_astt from, std::size_t width);

  virtual smt_astt
  mk_smt_typecast_from_fpbv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm);

  virtual smt_astt
  mk_smt_typecast_ubv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm);

  virtual smt_astt
  mk_smt_typecast_sbv_to_fpbv(smt_astt from, smt_sortt to, smt_astt rm);

  virtual smt_astt mk_smt_nearbyint_from_float(smt_astt from, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_add(smt_astt lhs, smt_astt rhs, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_sub(smt_astt lhs, smt_astt rhs, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_mul(smt_astt lhs, smt_astt rhs, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_div(smt_astt lhs, smt_astt rhs, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_rem(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_sqrt(smt_astt rd, smt_astt rm);

  virtual smt_astt
  mk_smt_fpbv_fma(smt_astt v1, smt_astt v2, smt_astt v3, smt_astt rm);

  virtual smt_astt mk_smt_fpbv_eq(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_gt(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_lt(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_gte(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_lte(smt_astt lhs, smt_astt rhs);

  virtual smt_astt mk_smt_fpbv_is_nan(smt_astt op);

  virtual smt_astt mk_smt_fpbv_is_inf(smt_astt op);

  virtual smt_astt mk_smt_fpbv_is_normal(smt_astt op);

  virtual smt_astt mk_smt_fpbv_is_zero(smt_astt op);

  virtual smt_astt mk_smt_fpbv_is_negative(smt_astt op);

  virtual smt_astt mk_smt_fpbv_is_positive(smt_astt op);

  virtual smt_astt mk_smt_fpbv_abs(smt_astt op);

  virtual smt_astt mk_smt_fpbv_neg(smt_astt op);

  virtual ieee_floatt get_fpbv(smt_astt a);

  virtual smt_astt mk_from_bv_to_fp(smt_astt op, smt_sortt to);

  virtual smt_astt mk_from_fp_to_bv(smt_astt op);
 
private:
  smt_solver_baset *ctx;
 
  void unpack(
    smt_astt &src,
    smt_astt &sgn,
    smt_astt &sig,
    smt_astt &exp,
    smt_astt &lz,
    bool normalize);
 
  smt_astt mk_unbias(smt_astt &src);
  smt_astt mk_leading_zeros(smt_astt &src, std::size_t max_bits);
 
  void round(
    smt_astt &rm,
    smt_astt &sgn,
    smt_astt &sig,
    smt_astt &exp,
    unsigned ebits,
    unsigned sbits,
    smt_astt &result);
 
  smt_astt mk_rounding_decision(
    smt_astt &rm,
    smt_astt &sgn,
    smt_astt &last,
    smt_astt &round,
    smt_astt &sticky);
 
  smt_astt mk_is_rm(smt_astt &rme, ieee_floatt::rounding_modet rm);
 
  smt_astt mk_top_exp(std::size_t sz);
  smt_astt mk_bot_exp(std::size_t sz);
  smt_astt mk_min_exp(std::size_t ebits);
  smt_astt mk_max_exp(std::size_t ebits);
  smt_astt mk_bias(smt_astt e);
 
  smt_astt mk_pzero(unsigned ew, unsigned sw);
  smt_astt mk_nzero(unsigned ew, unsigned sw);
  smt_astt mk_pinf(unsigned ew, unsigned sw);
  smt_astt mk_ninf(unsigned ew, unsigned sw);
  smt_astt mk_one(smt_astt sgn, unsigned ew, unsigned sw);
 
  smt_astt mk_is_pos(smt_astt op);
  smt_astt mk_is_neg(smt_astt op);
  smt_astt mk_is_pzero(smt_astt op);
  smt_astt mk_is_nzero(smt_astt op);
  smt_astt mk_is_pinf(smt_astt op);
  smt_astt mk_is_ninf(smt_astt op);
  smt_astt mk_is_denormal(smt_astt op);
 
  smt_astt mk_to_bv(smt_astt from, bool is_signed, std::size_t width);
};
 
#endif /* SOLVERS_SMT_FP_CONV_H_ */