fp_conv.cpp File Reference

#include <solvers/smt/smt_solver.h>

Include dependency graph for fp_conv.cpp:

Functions
static smt_astt	extract_exponent (smt_solver_baset *ctx, smt_astt fp)
static smt_astt	extract_significand (smt_solver_baset *ctx, smt_astt fp)
static smt_astt	extract_signbit (smt_solver_baset *ctx, smt_astt fp)
static smt_astt	extract_exp_sig (smt_solver_baset *ctx, smt_astt fp)
static void	add_core (smt_solver_baset *ctx, unsigned sbits, unsigned ebits, smt_astt &c_sgn, smt_astt &c_sig, smt_astt &c_exp, smt_astt &d_sgn, smt_astt &d_sig, smt_astt &d_exp, smt_astt &res_sgn, smt_astt &res_sig, smt_astt &res_exp)

Function Documentation

add_core()

void add_core ( smt_solver_baset * ctx, unsigned sbits, unsigned ebits, smt_astt & c_sgn, smt_astt & c_sig, smt_astt & c_exp, smt_astt & d_sgn, smt_astt & d_sig, smt_astt & d_exp, smt_astt & res_sgn, smt_astt & res_sig, smt_astt & res_exp )

static

extract_exp_sig()

smt_astt extract_exp_sig ( smt_solver_baset * ctx, smt_astt fp )

static

extract_exponent()

smt_astt extract_exponent ( smt_solver_baset * ctx, smt_astt fp )

static

extract_signbit()

smt_astt extract_signbit ( smt_solver_baset * ctx, smt_astt fp )

static

extract_significand()

smt_astt extract_significand ( smt_solver_baset * ctx, smt_astt fp )

static