mathematical_types.h File Reference

#include "expr_cast.h"
#include "invariant.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...

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

Detailed Description

Mathematical types

Definition in file mathematical_types.h.

Function Documentation

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 105 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 17 of file mathematical_types.cpp.

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 119 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 126 of file mathematical_types.h.