API to expression classes for 'mathematical' expressions. More...

#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.

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

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

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

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

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.

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

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.

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

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.

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

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.

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

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 410 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 163 of file mathematical_expr.h.

◆ can_cast_expr< forall_exprt >()

template<>

bool can_cast_expr< forall_exprt > ( const exprt & base )

inline

Definition at line 368 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 246 of file mathematical_expr.h.

◆ can_cast_expr< lambda_exprt >()

template<>

bool can_cast_expr< lambda_exprt > ( const exprt & base )

inline

Definition at line 461 of file mathematical_expr.h.

◆ can_cast_expr< power_exprt >()

template<>

bool can_cast_expr< power_exprt > ( const exprt & base )

inline

Definition at line 126 of file mathematical_expr.h.

◆ can_cast_expr< quantifier_exprt >()

template<>

bool can_cast_expr< quantifier_exprt > ( const exprt & base )

inline

Definition at line 316 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 420 of file mathematical_expr.h.

◆ to_exists_expr() [2/2]

exists_exprt & to_exists_expr ( exprt & expr )

inline

Definition at line 428 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 189 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 179 of file mathematical_expr.h.

◆ to_forall_expr() [1/2]

const forall_exprt & to_forall_expr ( const exprt & expr )

inline

Definition at line 378 of file mathematical_expr.h.

◆ to_forall_expr() [2/2]

forall_exprt & to_forall_expr ( exprt & expr )

inline

Definition at line 386 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 263 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 273 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 477 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 488 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 137 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 145 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 335 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 344 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/7]

void validate_expr ( const exists_exprt & value )

inline

Definition at line 415 of file mathematical_expr.h.

◆ validate_expr() [2/7]

void validate_expr ( const factorial_power_exprt & value )

inline

Definition at line 168 of file mathematical_expr.h.

◆ validate_expr() [3/7]

void validate_expr ( const forall_exprt & value )

inline

Definition at line 373 of file mathematical_expr.h.

◆ validate_expr() [4/7]

void validate_expr ( const function_application_exprt & value )

inline

Definition at line 251 of file mathematical_expr.h.

◆ validate_expr() [5/7]

void validate_expr ( const lambda_exprt & value )

inline

Definition at line 466 of file mathematical_expr.h.

◆ validate_expr() [6/7]

void validate_expr ( const quantifier_exprt & value )

inline

Definition at line 321 of file mathematical_expr.h.

◆ validate_expr() [7/7]

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/7]

◆ validate_expr() [2/7]

◆ validate_expr() [3/7]

◆ validate_expr() [4/7]

◆ validate_expr() [5/7]

◆ validate_expr() [6/7]

◆ validate_expr() [7/7]