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)
 
void validate_expr (const power_exprt &value)
 
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 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
exprSource 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
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/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.