CBMC
mathematical_expr.h File Reference

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:

Go to the source code of 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 transtto_trans_expr (const exprt &expr)
 Cast an exprt to a transt expr must be known to be transt. More...
 
transtto_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)
 
const power_exprtto_power_expr (const exprt &expr)
 Cast an exprt to a power_exprt. More...
 
power_exprtto_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_exprtto_factorial_power_expr (const exprt &expr)
 Cast an exprt to a factorial_power_exprt. More...
 
factorial_power_exprtto_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_exprtto_function_application_expr (const exprt &expr)
 Cast an exprt to a function_application_exprt. More...
 
function_application_exprtto_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_exprtto_quantifier_expr (const exprt &expr)
 Cast an exprt to a quantifier_exprt. More...
 
quantifier_exprtto_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_exprtto_forall_expr (const exprt &expr)
 
forall_exprtto_forall_expr (exprt &expr)
 
template<>
bool can_cast_expr< exists_exprt > (const exprt &base)
 
void validate_expr (const exists_exprt &value)
 
const exists_exprtto_exists_expr (const exprt &expr)
 
exists_exprtto_exists_expr (exprt &expr)
 
template<>
bool can_cast_expr< lambda_exprt > (const exprt &base)
 
void validate_expr (const lambda_exprt &value)
 
const lambda_exprtto_lambda_expr (const exprt &expr)
 Cast an exprt to a lambda_exprt. More...
 
lambda_exprtto_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 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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.