cprover
mathematical_expr.h File Reference

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

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

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...
 
const forall_exprtto_forall_expr (const exprt &expr)
 
forall_exprtto_forall_expr (exprt &expr)
 
const exists_exprtto_exists_expr (const exprt &expr)
 
exists_exprtto_exists_expr (exprt &expr)
 

Detailed Description

API to expression classes for 'mathematical' expressions.

Definition in file mathematical_expr.h.

Function Documentation

◆ can_cast_expr< factorial_power_exprt >()

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

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

◆ can_cast_expr< power_exprt >()

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

Definition at line 102 of file mathematical_expr.h.

◆ can_cast_expr< quantifier_exprt >()

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

Definition at line 303 of file mathematical_expr.h.

◆ can_cast_expr< transt >()

template<>
bool can_cast_expr< transt > ( const exprt base)
inline

Definition at line 60 of file mathematical_expr.h.

◆ to_exists_expr() [1/2]

const exists_exprt& to_exists_expr ( const exprt expr)
inline

Definition at line 375 of file mathematical_expr.h.

◆ to_exists_expr() [2/2]

exists_exprt& to_exists_expr ( exprt expr)
inline

Definition at line 383 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 172 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 162 of file mathematical_expr.h.

◆ to_forall_expr() [1/2]

const forall_exprt& to_forall_expr ( const exprt expr)
inline

Definition at line 349 of file mathematical_expr.h.

◆ to_forall_expr() [2/2]

forall_exprt& to_forall_expr ( exprt expr)
inline

Definition at line 357 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 250 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 260 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 118 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 127 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 322 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 331 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 74 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 83 of file mathematical_expr.h.

◆ validate_expr() [1/5]

void validate_expr ( const factorial_power_exprt value)
inline

Definition at line 151 of file mathematical_expr.h.

◆ validate_expr() [2/5]

void validate_expr ( const function_application_exprt value)
inline

Definition at line 238 of file mathematical_expr.h.

◆ validate_expr() [3/5]

void validate_expr ( const power_exprt value)
inline

Definition at line 107 of file mathematical_expr.h.

◆ validate_expr() [4/5]

void validate_expr ( const quantifier_exprt value)
inline

Definition at line 308 of file mathematical_expr.h.

◆ validate_expr() [5/5]

void validate_expr ( const transt value)
inline

Definition at line 65 of file mathematical_expr.h.