mathematical_types.h File Reference

Mathematical types. More...

#include "expr_cast.h"
#include "invariant.h"
#include "mp_arith.h"
#include "type.h"

Include dependency graph for mathematical_types.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	integer_typet
	Unbounded, signed integers (mathematical integers, not bitvectors) More...
class	natural_typet
	Natural numbers including zero (mathematical integers, not bitvectors) More...
class	rational_typet
	Unbounded, signed rational numbers. More...
class	real_typet
	Unbounded, signed real numbers. More...
class	mathematical_function_typet
	A type for mathematical functions (do not confuse with functions/methods in code) More...
class	integer_range_typet
	A type for closed integer intervals [from, to]. More...

Functions
template<>
bool	can_cast_type< mathematical_function_typet > (const typet &type)
	Check whether a reference to a typet is a mathematical_function_typet.
const mathematical_function_typet &	to_mathematical_function_type (const typet &type)
	Cast a typet to a mathematical_function_typet.
mathematical_function_typet &	to_mathematical_function_type (typet &type)
	Cast a typet to a mathematical_function_typet.
template<>
bool	can_cast_type< integer_range_typet > (const typet &type)
	Check whether a reference to a typet is a integer_range_typet.
const integer_range_typet &	to_integer_range_type (const typet &type)
	Cast a typet to a integer_range_typet.
integer_range_typet &	to_integer_range_type (typet &type)
	Cast a typet to a integer_range_typet.
bool	is_number (const typet &type)
	Returns true if the type is a rational, real, integer, natural, complex, unsignedbv, signedbv, floatbv or fixedbv.

Detailed Description

Mathematical types.

Definition in file mathematical_types.h.

Function Documentation

can_cast_type< integer_range_typet >()

template<>

bool can_cast_type< integer_range_typet > ( const typet &  type )

inline

Check whether a reference to a typet is a integer_range_typet.

Parameters

type	Source type.

Returns

True if type is a integer_range_typet.

Definition at line 195 of file mathematical_types.h.

can_cast_type< mathematical_function_typet >()

template<>

bool can_cast_type< mathematical_function_typet > ( const typet &  type )

inline

Check whether a reference to a typet is a mathematical_function_typet.

Parameters

type	Source type.

Returns

True if type is a mathematical_function_typet.

Definition at line 120 of file mathematical_types.h.

is_number()

bool is_number

(

const typet &

type

)

Returns true if the type is a rational, real, integer, natural, complex, unsignedbv, signedbv, floatbv or fixedbv.

Definition at line 19 of file mathematical_types.cpp.

to_integer_range_type() [1/2]

const integer_range_typet & to_integer_range_type ( const typet &  type )

inline

Cast a typet to a integer_range_typet.

This is an unchecked conversion. type must be known to be integer_range_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns

Object of type integer_range_typet.

Definition at line 208 of file mathematical_types.h.

to_integer_range_type() [2/2]

integer_range_typet & to_integer_range_type ( typet &  type )

inline

Cast a typet to a integer_range_typet.

This is an unchecked conversion. type must be known to be integer_range_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns

Object of type integer_range_typet.

Definition at line 215 of file mathematical_types.h.

to_mathematical_function_type() [1/2]

const mathematical_function_typet & to_mathematical_function_type ( const typet &  type )

inline

Cast a typet to a mathematical_function_typet.

This is an unchecked conversion. type must be known to be mathematical_function_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns

Object of type mathematical_function_typet.

Definition at line 134 of file mathematical_types.h.

to_mathematical_function_type() [2/2]

mathematical_function_typet & to_mathematical_function_type ( typet &  type )

inline

Cast a typet to a mathematical_function_typet.

This is an unchecked conversion. type must be known to be mathematical_function_typet. Will fail with a precondition violation if type doesn't match.

Parameters

type	Source type.

Returns

Object of type mathematical_function_typet.

Definition at line 141 of file mathematical_types.h.