Loading...

Searching...

No Matches

Public Member Functions | Static Public Attributes | Private Attributes | Friends | List of all members

guard_exprt Class Reference

#include <guard_expr.h>

+ Collaboration diagram for guard_exprt:

[フレーム]

[legend]

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.

guard_exprt & operator= (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.

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.

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.

Private Attributes

exprt expr

Friends

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

guard_exprt & operator|= (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 Symbol 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:

/home/runner/work/cbmc/cbmc/src/analyses/guard_expr.h
/home/runner/work/cbmc/cbmc/src/analyses/guard_expr.cpp