smt_fp_conv.cpp File Reference

#include "irep2/irep2_expr.h"
#include <solvers/smt/smt_solver.h>
#include <solvers/smt/smt_fp_rounding_utils.h>
#include <solvers/smt/fp/ir_ieee_conv.h>
#include <util/arith/arith_tools.h>
#include <util/expr/expr_util.h>
#include <util/message/message.h>
#include <util/message/format.h>

Include dependency graph for smt_fp_conv.cpp:

Functions
static smt_astt	get_max_normal (smt_solver_baset &conv, const floatbv_type2t &fbv_type)
static smt_astt	get_min_normal (smt_solver_baset &conv, const floatbv_type2t &fbv_type)

Function Documentation

get_max_normal()

smt_astt get_max_normal ( smt_solver_baset & conv, const floatbv_type2t & fbv_type )

static

get_min_normal()

smt_astt get_min_normal ( smt_solver_baset & conv, const floatbv_type2t & fbv_type )

static