CBMC
mathematical_types.h File Reference

Mathematical types. More...

#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_typetto_mathematical_function_type (const typet &type)
 Cast a typet to a mathematical_function_typet. More...
 
mathematical_function_typetto_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
typeSource 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
typeSource 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
typeSource type.
Returns
Object of type mathematical_function_typet.

Definition at line 126 of file mathematical_types.h.