#include <fp_conv.h>

Inheritance diagram for fp_convt:

Public Member Functions
	fp_convt (smt_solver_baset *_ctx)
virtual	~fp_convt ()=default
virtual smt_astt	mk_smt_fpbv (const ieee_floatt &thereal)
	Create a floating point bitvector.
virtual smt_sortt	mk_fpbv_sort (const unsigned ew, const unsigned sw)
	Create a sort representing a floating-point number.
virtual smt_sortt	mk_fpbv_rm_sort ()
	Create a sort representing a floating-point rounding mode.
virtual smt_astt	mk_smt_fpbv_nan (bool sgn, unsigned ew, unsigned sw)
	Create a NaN floating point bitvector.
virtual smt_astt	mk_smt_fpbv_inf (bool sgn, unsigned ew, unsigned sw)
	Create a (+/-)inf floating point bitvector.
virtual smt_astt	mk_smt_fpbv_rm (ieee_floatt::rounding_modet rm)
	Create a rounding mode to be used by floating point cast and arith ops.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_ubv (smt_astt from, std::size_t width)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_sbv (smt_astt from, std::size_t width)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_from_fpbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast from a floating point.
virtual smt_astt	mk_smt_typecast_ubv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast to a floating point.
virtual smt_astt	mk_smt_typecast_sbv_to_fpbv (smt_astt from, smt_sortt to, smt_astt rm)
	Typecast to a floating point.
virtual smt_astt	mk_smt_nearbyint_from_float (smt_astt from, smt_astt rm)
	Calculate the nearby int from a floating point, considering the rounding mode.
virtual smt_astt	mk_smt_fpbv_add (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee addition.
virtual smt_astt	mk_smt_fpbv_sub (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee subtraction.
virtual smt_astt	mk_smt_fpbv_mul (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert a ieee multiplication.
virtual smt_astt	mk_smt_fpbv_div (smt_astt lhs, smt_astt rhs, smt_astt rm)
	Convert the ieee division.
virtual smt_astt	mk_smt_fpbv_rem (smt_astt lhs, smt_astt rhs)
	Convert the ieee remainder (SMT-LIB fp.rem, C's remainder()).
virtual smt_astt	mk_smt_fpbv_sqrt (smt_astt rd, smt_astt rm)
	Convert the ieee arithmetic square-root (sqrt).
virtual smt_astt	mk_smt_fpbv_fma (smt_astt v1, smt_astt v2, smt_astt v3, smt_astt rm)
	Convert the ieee arithmetic fused-multiply add (fma): round((v1 * v2) + v3).
virtual smt_astt	mk_smt_fpbv_eq (smt_astt lhs, smt_astt rhs)
	Convert an ieee equality.
virtual smt_astt	mk_smt_fpbv_gt (smt_astt lhs, smt_astt rhs)
	Convert an ieee greater than.
virtual smt_astt	mk_smt_fpbv_lt (smt_astt lhs, smt_astt rhs)
	Convert an ieee less than.
virtual smt_astt	mk_smt_fpbv_gte (smt_astt lhs, smt_astt rhs)
	Convert an ieee greater than or equal.
virtual smt_astt	mk_smt_fpbv_lte (smt_astt lhs, smt_astt rhs)
	Convert an ieee less than or equal.
virtual smt_astt	mk_smt_fpbv_is_nan (smt_astt op)
	Convert an ieee is_nan operation.
virtual smt_astt	mk_smt_fpbv_is_inf (smt_astt op)
	Convert an ieee is_inf operation.
virtual smt_astt	mk_smt_fpbv_is_normal (smt_astt op)
	Convert an ieee is_normal operation.
virtual smt_astt	mk_smt_fpbv_is_zero (smt_astt op)
	Convert an ieee is_zero operation.
virtual smt_astt	mk_smt_fpbv_is_negative (smt_astt op)
	Convert an ieee is_neg operation.
virtual smt_astt	mk_smt_fpbv_is_positive (smt_astt op)
	Convert an ieee is_pos operation.
virtual smt_astt	mk_smt_fpbv_abs (smt_astt op)
	Convert an ieee abs operation.
virtual smt_astt	mk_smt_fpbv_neg (smt_astt op)
	Convert an ieee negation operation.
virtual ieee_floatt	get_fpbv (smt_astt a)
	Extract the assignment to a floating-point from the SMT solvers model.
virtual smt_astt	mk_from_bv_to_fp (smt_astt op, smt_sortt to)
	Convert BV to FP.
virtual smt_astt	mk_from_fp_to_bv (smt_astt op)
	Convert FP to BV.

Constructor & Destructor Documentation

◆ fp_convt()

fp_convt::fp_convt ( smt_solver_baset * _ctx )

explicit

◆ ~fp_convt()

virtual fp_convt::~fp_convt ( )

virtualdefault

Member Function Documentation

◆ get_fpbv()

ieee_floatt fp_convt::get_fpbv ( smt_astt a )

virtual

Extract the assignment to a floating-point from the SMT solvers model.

Parameters

a	the AST whos value we wish to know.

Returns: the ieee floating-point

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_fpbv_rm_sort()

smt_sortt fp_convt::mk_fpbv_rm_sort ( )

virtual

Create a sort representing a floating-point rounding mode.

Returns: The floating-point rounding mode representation of the type, wrapped in an smt_sort.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_fpbv_sort()

smt_sortt fp_convt::mk_fpbv_sort	(	const unsigned	ew,
		const unsigned	sw )

virtual

Create a sort representing a floating-point number.

Parameters

ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The floating-point representation of the type, wrapped in an smt_sort.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_from_bv_to_fp()

smt_astt fp_convt::mk_from_bv_to_fp	(	smt_astt	op,
		smt_sortt	to )

virtual

Convert BV to FP.

Parameters

op	the bitvector
to	the floating-point type

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_from_fp_to_bv()

smt_astt fp_convt::mk_from_fp_to_bv ( smt_astt op )

virtual

Convert FP to BV.

Parameters

op	the floating-point

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv()

smt_astt fp_convt::mk_smt_fpbv ( const ieee_floatt & thereal )

virtual

Create a floating point bitvector.

Parameters

thereal	the floating-point number
ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_abs()

smt_astt fp_convt::mk_smt_fpbv_abs ( smt_astt op )

virtual

Convert an ieee abs operation.

Parameters

op	the operand

Returns: The newly created fp.abs smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_add()

smt_astt fp_convt::mk_smt_fpbv_add	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

virtual

Convert a ieee addition.

Parameters

lhs	left hand side of the addition
rhs	right hand side of the addition
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_div()

smt_astt fp_convt::mk_smt_fpbv_div	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

virtual

Convert the ieee division.

Parameters

lhs	left hand side of the division
rhs	right hand side of the division
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_eq()

smt_astt fp_convt::mk_smt_fpbv_eq	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert an ieee equality.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.eq smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_fma()

smt_astt fp_convt::mk_smt_fpbv_fma	(	smt_astt	v1,
		smt_astt	v2,
		smt_astt	v3,
		smt_astt	rm )

virtual

Convert the ieee arithmetic fused-multiply add (fma): round((v1 * v2) + v3).

Parameters

v1	in the equation
v2	in the equation
v3	in the equation
rm	the rounding mode

Returns: The newly created fma smt_ast

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_gt()

smt_astt fp_convt::mk_smt_fpbv_gt	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert an ieee greater than.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.gt smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, and z3_convt.

◆ mk_smt_fpbv_gte()

smt_astt fp_convt::mk_smt_fpbv_gte	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert an ieee greater than or equal.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.gt smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, and z3_convt.

◆ mk_smt_fpbv_inf()

smt_astt fp_convt::mk_smt_fpbv_inf	(	bool	sgn,
		unsigned	ew,
		unsigned	sw )

virtual

Create a (+/-)inf floating point bitvector.

Parameters

sgn	Whether this bitvector is negative or positive.
ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_inf()

smt_astt fp_convt::mk_smt_fpbv_is_inf ( smt_astt op )

virtual

Convert an ieee is_inf operation.

Parameters

op	the operand

Returns: The newly created fp.isInfinite smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_nan()

smt_astt fp_convt::mk_smt_fpbv_is_nan ( smt_astt op )

virtual

Convert an ieee is_nan operation.

Parameters

op	the operand

Returns: The newly created fp.isNaN smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_negative()

smt_astt fp_convt::mk_smt_fpbv_is_negative ( smt_astt op )

virtual

Convert an ieee is_neg operation.

Parameters

op	the operand

Returns: The newly created fp.isNegative smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_normal()

smt_astt fp_convt::mk_smt_fpbv_is_normal ( smt_astt op )

virtual

Convert an ieee is_normal operation.

Parameters

op	the operand

Returns: The newly created fp.isNormal smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_positive()

smt_astt fp_convt::mk_smt_fpbv_is_positive ( smt_astt op )

virtual

Convert an ieee is_pos operation.

Parameters

op	the operand

Returns: The newly created fp.isPositive smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_is_zero()

smt_astt fp_convt::mk_smt_fpbv_is_zero ( smt_astt op )

virtual

Convert an ieee is_zero operation.

Parameters

op	the operand

Returns: The newly created fp.isZero smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_lt()

smt_astt fp_convt::mk_smt_fpbv_lt	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert an ieee less than.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.lt smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_lte()

smt_astt fp_convt::mk_smt_fpbv_lte	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert an ieee less than or equal.

Parameters

lhs	left hand side
rhs	right hand side

Returns: The newly created fp.lt smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_mul()

smt_astt fp_convt::mk_smt_fpbv_mul	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

virtual

Convert a ieee multiplication.

Parameters

lhs	left hand side of the multiplication
rhs	right hand side of the multiplication
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_nan()

smt_astt fp_convt::mk_smt_fpbv_nan	(	bool	sgn,
		unsigned	ew,
		unsigned	sw )

virtual

Create a NaN floating point bitvector.

Parameters

ew	Exponent width, in bits, of the bitvector to create.
sw	Significand width, in bits, of the bitvector to create.

Returns: The newly created terminal smt_ast of this bitvector.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_neg()

smt_astt fp_convt::mk_smt_fpbv_neg ( smt_astt op )

virtual

Convert an ieee negation operation.

Parameters

op	the operand

Returns: The newly created fp.neg smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_rem()

smt_astt fp_convt::mk_smt_fpbv_rem	(	smt_astt	lhs,
		smt_astt	rhs )

virtual

Convert the ieee remainder (SMT-LIB fp.rem, C's remainder()).

The operation is exact, so it takes no rounding mode.

Parameters

lhs	left hand side of the remainder
rhs	right hand side of the remainder

Returns: The newly created fp.rem smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_rm()

smt_astt fp_convt::mk_smt_fpbv_rm ( ieee_floatt::rounding_modet rm )

virtual

Create a rounding mode to be used by floating point cast and arith ops.

Parameters

rm	the kind of rounding mode

Returns: The newly created rounding mode smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_sqrt()

smt_astt fp_convt::mk_smt_fpbv_sqrt	(	smt_astt	rd,
		smt_astt	rm )

virtual

Convert the ieee arithmetic square-root (sqrt).

Parameters

op	the sqrt radicand
rm	the rounding mode

Returns: The newly created sqrt smt_ast

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_fpbv_sub()

smt_astt fp_convt::mk_smt_fpbv_sub	(	smt_astt	lhs,
		smt_astt	rhs,
		smt_astt	rm )

virtual

Convert a ieee subtraction.

Parameters

lhs	left hand side of the subtraction
rhs	right hand side of the subtraction
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_nearbyint_from_float()

smt_astt fp_convt::mk_smt_nearbyint_from_float	(	smt_astt	from,
		smt_astt	rm )

virtual

Calculate the nearby int from a floating point, considering the rounding mode.

Parameters

from	the floating-point
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_typecast_from_fpbv_to_fpbv()

smt_astt fp_convt::mk_smt_typecast_from_fpbv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

virtual

Typecast from a floating point.

Parameters

from	the floating point being casted to floating-point
to	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_typecast_from_fpbv_to_sbv()

smt_astt fp_convt::mk_smt_typecast_from_fpbv_to_sbv	(	smt_astt	from,
		std::size_t	width )

virtual

Typecast from a floating point.

Parameters

from	the floating point being casted to signed bitvector
to	the signed bitvector resulting type

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_typecast_from_fpbv_to_ubv()

smt_astt fp_convt::mk_smt_typecast_from_fpbv_to_ubv	(	smt_astt	from,
		std::size_t	width )

virtual

Typecast from a floating point.

Parameters

from	the floating point being casted to unsigned bitvector
to	the unsigned bitvector resulting type

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_typecast_sbv_to_fpbv()

smt_astt fp_convt::mk_smt_typecast_sbv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

virtual

Typecast to a floating point.

Parameters

from	the signed bitvector being casted to a floating-point
cast	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

◆ mk_smt_typecast_ubv_to_fpbv()

smt_astt fp_convt::mk_smt_typecast_ubv_to_fpbv	(	smt_astt	from,
		smt_sortt	to,
		smt_astt	rm )

virtual

Typecast to a floating point.

Parameters

from	the unsigned bitvector being casted to a floating-point
cast	the floating-point resulting type
rm	the rounding mode

Returns: The newly created cast smt_ast.

Reimplemented in bitwuzla_convt, cvc5_convt, cvc_convt, mathsat_convt, and z3_convt.

The documentation for this class was generated from the following files:

src/solvers/smt/fp/fp_conv.h
src/solvers/smt/fp/fp_conv.cpp

Public Member Functions

Constructor & Destructor Documentation

◆ fp_convt()

◆ ~fp_convt()

Member Function Documentation

◆ get_fpbv()

◆ mk_fpbv_rm_sort()

◆ mk_fpbv_sort()

◆ mk_from_bv_to_fp()

◆ mk_from_fp_to_bv()

◆ mk_smt_fpbv()

◆ mk_smt_fpbv_abs()

◆ mk_smt_fpbv_add()

◆ mk_smt_fpbv_div()

◆ mk_smt_fpbv_eq()

◆ mk_smt_fpbv_fma()

◆ mk_smt_fpbv_gt()

◆ mk_smt_fpbv_gte()

◆ mk_smt_fpbv_inf()

◆ mk_smt_fpbv_is_inf()

◆ mk_smt_fpbv_is_nan()

◆ mk_smt_fpbv_is_negative()

◆ mk_smt_fpbv_is_normal()

◆ mk_smt_fpbv_is_positive()

◆ mk_smt_fpbv_is_zero()

◆ mk_smt_fpbv_lt()

◆ mk_smt_fpbv_lte()

◆ mk_smt_fpbv_mul()

◆ mk_smt_fpbv_nan()

◆ mk_smt_fpbv_neg()

◆ mk_smt_fpbv_rem()

◆ mk_smt_fpbv_rm()

◆ mk_smt_fpbv_sqrt()

◆ mk_smt_fpbv_sub()

◆ mk_smt_nearbyint_from_float()

◆ mk_smt_typecast_from_fpbv_to_fpbv()

◆ mk_smt_typecast_from_fpbv_to_sbv()

◆ mk_smt_typecast_from_fpbv_to_ubv()

◆ mk_smt_typecast_sbv_to_fpbv()

◆ mk_smt_typecast_ubv_to_fpbv()