CBMC
guard_exprt Class Reference

#include <guard_expr.h>

+ Collaboration diagram for guard_exprt:

Public Member Functions

 guard_exprt (const exprt &e, guard_expr_managert &)
 Construct a BDD from an expression The guard_managert parameter is not used, but we keep it for uniformity with other implementations of guards which may use it. More...
 
guard_exprtoperator= (const guard_exprt &other)
 
void add (const exprt &expr)
 
void append (const guard_exprt &guard)
 
exprt as_expr () const
 
exprt guard_expr (exprt expr) const
 Return guard => dest or a simplified variant thereof if either guard or dest are trivial. More...
 
bool is_true () const
 
bool is_false () const
 
bool disjunction_may_simplify (const guard_exprt &other_guard)
 Returns true if operator|= with other_guard may result in a simpler expression. More...
 

Static Public Attributes

static constexpr bool is_always_simplified = false
 The result of as_expr is not always in a simplified form and may requires some simplification. More...
 

Private Attributes

exprt expr
 

Friends

guard_exprtoperator-= (guard_exprt &g1, const guard_exprt &g2)
 
guard_exprtoperator|= (guard_exprt &g1, const guard_exprt &g2)
 

Detailed Description

Definition at line 23 of file guard_expr.h.

Constructor & Destructor Documentation

◆ guard_exprt()

guard_exprt::guard_exprt ( const exprt e,
guard_expr_managert  
)
inlineexplicit

Construct a BDD from an expression The guard_managert parameter is not used, but we keep it for uniformity with other implementations of guards which may use it.

Definition at line 29 of file guard_expr.h.

Member Function Documentation

◆ add()

void guard_exprt::add ( const exprt expr)

Definition at line 38 of file guard_expr.cpp.

◆ append()

void guard_exprt::append ( const guard_exprt guard)
inline

Definition at line 41 of file guard_expr.h.

◆ as_expr()

exprt guard_exprt::as_expr ( ) const
inline

Definition at line 46 of file guard_expr.h.

◆ disjunction_may_simplify()

bool guard_exprt::disjunction_may_simplify ( const guard_exprt other_guard)

Returns true if operator|= with other_guard may result in a simpler expression.

For guard_exprt in practice this means they're both conjunctions, since for other things we just OR them together.

Definition at line 123 of file guard_expr.cpp.

◆ guard_expr()

exprt guard_exprt::guard_expr ( exprt  expr) const

Return guard => dest or a simplified variant thereof if either guard or dest are trivial.

Definition at line 18 of file guard_expr.cpp.

◆ is_false()

bool guard_exprt::is_false ( ) const
inline

Definition at line 65 of file guard_expr.h.

◆ is_true()

bool guard_exprt::is_true ( ) const
inline

Definition at line 60 of file guard_expr.h.

◆ operator=()

guard_exprt& guard_exprt::operator= ( const guard_exprt other)
inline

Definition at line 33 of file guard_expr.h.

Friends And Related Function Documentation

◆ operator-=

guard_exprt& operator-= ( guard_exprt g1,
const guard_exprt g2 
)
friend

Definition at line 64 of file guard_expr.cpp.

◆ operator|=

guard_exprt& operator|= ( guard_exprt g1,
const guard_exprt g2 
)
friend

Definition at line 134 of file guard_expr.cpp.

Member Data Documentation

◆ expr

exprt guard_exprt::expr
private

Definition at line 79 of file guard_expr.h.

◆ is_always_simplified

constexpr bool guard_exprt::is_always_simplified = false
staticconstexpr

The result of as_expr is not always in a simplified form and may requires some simplification.

This can vary according to the guard implementation.

Definition at line 54 of file guard_expr.h.


The documentation for this class was generated from the following files: