#include "mathematical_types.h"
#include "std_expr.h"

Include dependency graph for mathematical_expr.h:

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

Classes
class	transt
	Transition system, consisting of state invariant, initial state predicate, and transition predicate. More...

class	power_exprt
	Exponentiation. More...

class	factorial_power_exprt
	Falling factorial power. More...

class	tuple_exprt

class	function_application_exprt
	Application of (mathematical) function. More...

class	quantifier_exprt
	A base class for quantifier expressions. More...

class	forall_exprt
	A forall expression. More...

class	exists_exprt
	An exists expression. More...

class	lambda_exprt
	A (mathematical) lambda expression. More...

Functions
template<>
bool	can_cast_expr< transt > (const exprt &base)

void	validate_expr (const transt &value)

const transt &	to_trans_expr (const exprt &expr)
	Cast an exprt to a transt expr must be known to be transt. More...

transt &	to_trans_expr (exprt &expr)
	Cast an exprt to a transt expr must be known to be transt. More...

template<>
bool	can_cast_expr< power_exprt > (const exprt &base)

void	validate_expr (const power_exprt &value)

const power_exprt &	to_power_expr (const exprt &expr)
	Cast an exprt to a power_exprt. More...

power_exprt &	to_power_expr (exprt &expr)
	Cast an exprt to a power_exprt. More...

template<>
bool	can_cast_expr< factorial_power_exprt > (const exprt &base)

void	validate_expr (const factorial_power_exprt &value)

const factorial_power_exprt &	to_factorial_power_expr (const exprt &expr)
	Cast an exprt to a factorial_power_exprt. More...

factorial_power_exprt &	to_factorial_expr (exprt &expr)
	Cast an exprt to a factorial_power_exprt. More...

template<>
bool	can_cast_expr< function_application_exprt > (const exprt &base)

void	validate_expr (const function_application_exprt &value)

const function_application_exprt &	to_function_application_expr (const exprt &expr)
	Cast an exprt to a function_application_exprt. More...

function_application_exprt &	to_function_application_expr (exprt &expr)
	Cast an exprt to a function_application_exprt. More...

template<>
bool	can_cast_expr< quantifier_exprt > (const exprt &base)

void	validate_expr (const quantifier_exprt &value)

const quantifier_exprt &	to_quantifier_expr (const exprt &expr)
	Cast an exprt to a quantifier_exprt. More...

quantifier_exprt &	to_quantifier_expr (exprt &expr)
	Cast an exprt to a quantifier_exprt. More...

template<>
bool	can_cast_expr< forall_exprt > (const exprt &base)

void	validate_expr (const forall_exprt &value)

const forall_exprt &	to_forall_expr (const exprt &expr)

forall_exprt &	to_forall_expr (exprt &expr)

template<>
bool	can_cast_expr< exists_exprt > (const exprt &base)

void	validate_expr (const exists_exprt &value)

const exists_exprt &	to_exists_expr (const exprt &expr)

exists_exprt &	to_exists_expr (exprt &expr)

template<>
bool	can_cast_expr< lambda_exprt > (const exprt &base)

void	validate_expr (const lambda_exprt &value)

const lambda_exprt &	to_lambda_expr (const exprt &expr)
	Cast an exprt to a lambda_exprt. More...

lambda_exprt &	to_lambda_expr (exprt &expr)
	Cast an exprt to a lambda_exprt. More...

Detailed Description

API to expression classes for 'mathematical' expressions

Definition in file mathematical_expr.h.

Function Documentation

◆ can_cast_expr< exists_exprt >()

template<>

bool can_cast_expr< exists_exprt > ( const exprt & base )

inline

Definition at line 394 of file mathematical_expr.h.

◆ can_cast_expr< factorial_power_exprt >()

template<>

bool can_cast_expr< factorial_power_exprt > ( const exprt & base )

inline

Definition at line 147 of file mathematical_expr.h.

◆ can_cast_expr< forall_exprt >()

template<>

bool can_cast_expr< forall_exprt > ( const exprt & base )

inline

Definition at line 352 of file mathematical_expr.h.

◆ can_cast_expr< function_application_exprt >()

template<>

bool can_cast_expr< function_application_exprt > ( const exprt & base )

inline

Definition at line 230 of file mathematical_expr.h.

◆ can_cast_expr< lambda_exprt >()

template<>

bool can_cast_expr< lambda_exprt > ( const exprt & base )

inline

Definition at line 445 of file mathematical_expr.h.

◆ can_cast_expr< power_exprt >()

template<>

bool can_cast_expr< power_exprt > ( const exprt & base )

inline

Definition at line 103 of file mathematical_expr.h.

◆ can_cast_expr< quantifier_exprt >()

template<>

bool can_cast_expr< quantifier_exprt > ( const exprt & base )

inline

Definition at line 300 of file mathematical_expr.h.

◆ can_cast_expr< transt >()

template<>

bool can_cast_expr< transt > ( const exprt & base )

inline

Definition at line 61 of file mathematical_expr.h.

◆ to_exists_expr() [1/2]

const exists_exprt& to_exists_expr ( const exprt & expr )

inline

Definition at line 404 of file mathematical_expr.h.

◆ to_exists_expr() [2/2]

exists_exprt& to_exists_expr ( exprt & expr )

inline

Definition at line 412 of file mathematical_expr.h.

◆ to_factorial_expr()

factorial_power_exprt& to_factorial_expr ( exprt & expr )

inline

Cast an exprt to a factorial_power_exprt.

expr must be known to be factorial_power_exprt.

Parameters

expr	Source expression

Returns: Object of type factorial_power_exprt

Definition at line 173 of file mathematical_expr.h.

◆ to_factorial_power_expr()

const factorial_power_exprt& to_factorial_power_expr ( const exprt & expr )

inline

Cast an exprt to a factorial_power_exprt.

expr must be known to be factorial_power_exprt.

Parameters

expr	Source expression

Returns: Object of type factorial_power_exprt

Definition at line 163 of file mathematical_expr.h.

◆ to_forall_expr() [1/2]

const forall_exprt& to_forall_expr ( const exprt & expr )

inline

Definition at line 362 of file mathematical_expr.h.

◆ to_forall_expr() [2/2]

forall_exprt& to_forall_expr ( exprt & expr )

inline

Definition at line 370 of file mathematical_expr.h.

◆ to_function_application_expr() [1/2]

const function_application_exprt& to_function_application_expr ( const exprt & expr )

inline

Cast an exprt to a function_application_exprt.

expr must be known to be function_application_exprt.

Parameters

expr	Source expression

Returns: Object of type function_application_exprt

Definition at line 247 of file mathematical_expr.h.

◆ to_function_application_expr() [2/2]

function_application_exprt& to_function_application_expr ( exprt & expr )

inline

Cast an exprt to a function_application_exprt.

expr must be known to be function_application_exprt.

Parameters

expr	Source expression

Returns: Object of type function_application_exprt

Definition at line 257 of file mathematical_expr.h.

◆ to_lambda_expr() [1/2]

const lambda_exprt& to_lambda_expr ( const exprt & expr )

inline

Cast an exprt to a lambda_exprt.

expr must be known to be lambda_exprt.

Parameters

expr	Source expression

Returns: Object of type lambda_exprt

Definition at line 461 of file mathematical_expr.h.

◆ to_lambda_expr() [2/2]

lambda_exprt& to_lambda_expr ( exprt & expr )

inline

Cast an exprt to a lambda_exprt.

expr must be known to be lambda_exprt.

Parameters

expr	Source expression

Returns: Object of type lambda_exprt

Definition at line 472 of file mathematical_expr.h.

◆ to_power_expr() [1/2]

const power_exprt& to_power_expr ( const exprt & expr )

inline

Cast an exprt to a power_exprt.

expr must be known to be power_exprt.

Parameters

expr	Source expression

Returns: Object of type power_exprt

Definition at line 119 of file mathematical_expr.h.

◆ to_power_expr() [2/2]

power_exprt& to_power_expr ( exprt & expr )

inline

Cast an exprt to a power_exprt.

expr must be known to be power_exprt.

Parameters

expr	Source expression

Returns: Object of type power_exprt

Definition at line 128 of file mathematical_expr.h.

◆ to_quantifier_expr() [1/2]

const quantifier_exprt& to_quantifier_expr ( const exprt & expr )

inline

Cast an exprt to a quantifier_exprt.

expr must be known to be quantifier_exprt.

Parameters

expr	Source expression

Returns: Object of type quantifier_exprt

Definition at line 319 of file mathematical_expr.h.

◆ to_quantifier_expr() [2/2]

quantifier_exprt& to_quantifier_expr ( exprt & expr )

inline

Cast an exprt to a quantifier_exprt.

expr must be known to be quantifier_exprt.

Parameters

expr	Source expression

Returns: Object of type quantifier_exprt

Definition at line 328 of file mathematical_expr.h.

◆ to_trans_expr() [1/2]

const transt& to_trans_expr ( const exprt & expr )

inline

Cast an exprt to a transt expr must be known to be transt.

Parameters

expr	Source expression

Returns: Object of type transt

Definition at line 75 of file mathematical_expr.h.

◆ to_trans_expr() [2/2]

transt& to_trans_expr ( exprt & expr )

inline

Cast an exprt to a transt expr must be known to be transt.

Parameters

expr	Source expression

Returns: Object of type transt

Definition at line 84 of file mathematical_expr.h.

◆ validate_expr() [1/8]

void validate_expr ( const exists_exprt & value )

inline

Definition at line 399 of file mathematical_expr.h.

◆ validate_expr() [2/8]

void validate_expr ( const factorial_power_exprt & value )

inline

Definition at line 152 of file mathematical_expr.h.

◆ validate_expr() [3/8]

void validate_expr ( const forall_exprt & value )

inline

Definition at line 357 of file mathematical_expr.h.

◆ validate_expr() [4/8]

void validate_expr ( const function_application_exprt & value )

inline

Definition at line 235 of file mathematical_expr.h.

◆ validate_expr() [5/8]

void validate_expr ( const lambda_exprt & value )

inline

Definition at line 450 of file mathematical_expr.h.

◆ validate_expr() [6/8]

void validate_expr ( const power_exprt & value )

inline

Definition at line 108 of file mathematical_expr.h.

◆ validate_expr() [7/8]

void validate_expr ( const quantifier_exprt & value )

inline

Definition at line 305 of file mathematical_expr.h.

◆ validate_expr() [8/8]

void validate_expr ( const transt & value )

inline

Definition at line 66 of file mathematical_expr.h.

Classes

Functions

Detailed Description

Function Documentation

◆ can_cast_expr< exists_exprt >()

◆ can_cast_expr< factorial_power_exprt >()

◆ can_cast_expr< forall_exprt >()

◆ can_cast_expr< function_application_exprt >()

◆ can_cast_expr< lambda_exprt >()

◆ can_cast_expr< power_exprt >()

◆ can_cast_expr< quantifier_exprt >()

◆ can_cast_expr< transt >()

◆ to_exists_expr() [1/2]

◆ to_exists_expr() [2/2]

◆ to_factorial_expr()

◆ to_factorial_power_expr()

◆ to_forall_expr() [1/2]

◆ to_forall_expr() [2/2]

◆ to_function_application_expr() [1/2]

◆ to_function_application_expr() [2/2]

◆ to_lambda_expr() [1/2]

◆ to_lambda_expr() [2/2]

◆ to_power_expr() [1/2]

◆ to_power_expr() [2/2]

◆ to_quantifier_expr() [1/2]

◆ to_quantifier_expr() [2/2]

◆ to_trans_expr() [1/2]

◆ to_trans_expr() [2/2]

◆ validate_expr() [1/8]

◆ validate_expr() [2/8]

◆ validate_expr() [3/8]

◆ validate_expr() [4/8]

◆ validate_expr() [5/8]

◆ validate_expr() [6/8]

◆ validate_expr() [7/8]

◆ validate_expr() [8/8]