Loading...

Searching...

No Matches

guard_bddt Class Reference

#include <guard_bdd.h>

+ Collaboration diagram for guard_bddt:

[フレーム]

[legend]

Public Member Functions

guard_bddt (const exprt &e, bdd_exprt &manager)

guard_bddt (const guard_bddt &other)

guard_bddt & operator= (const guard_bddt &other)

guard_bddt & operator= (guard_bddt &&other)

guard_bddt & add (const exprt &expr)

guard_bddt & append (const guard_bddt &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

guard_bddt operator! () const

bool disjunction_may_simplify (const guard_bddt &other_guard)

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

Static Public Attributes

static constexpr bool is_always_simplified = true

BDDs are always in a simplified form and thus no further simplification is required after calls to as_expr().

Private Member Functions

guard_bddt (bdd_exprt &manager, bddt bdd)

Private Attributes

bdd_exprt & manager

bddt bdd

Friends

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

Transforms g1 into g1' such that ‘g1’ & g2 => g1 => g1'` and returns a reference to g1.

guard_bddt & operator|= (guard_bddt &g1, const guard_bddt &g2)

Detailed Description

Definition at line 21 of file guard_bdd.h.

Constructor & Destructor Documentation

◆ guard_bddt() [1/3]

guard_bddt::guard_bddt ( const exprt & e,

bdd_exprt & manager

)

Definition at line 19 of file guard_bdd.cpp.

◆ guard_bddt() [2/3]

guard_bddt::guard_bddt ( const guard_bddt & other )

inline

Definition at line 25 of file guard_bdd.h.

◆ guard_bddt() [3/3]

guard_bddt::guard_bddt ( bdd_exprt & manager,

bddt bdd

)

inlineprivate

Definition at line 76 of file guard_bdd.h.

Member Function Documentation

◆ add()

guard_bddt & guard_bddt::add ( const exprt & expr )

Definition at line 64 of file guard_bdd.cpp.

◆ append()

guard_bddt & guard_bddt::append ( const guard_bddt & guard )

Definition at line 58 of file guard_bdd.cpp.

◆ as_expr()

exprt guard_bddt::as_expr ( ) const

Definition at line 82 of file guard_bdd.cpp.

◆ disjunction_may_simplify()

bool guard_bddt::disjunction_may_simplify ( const guard_bddt & other_guard )

inline

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

For bdd_exprt we always simplify maximally.

Definition at line 67 of file guard_bdd.h.

◆ guard_expr()

exprt guard_bddt::guard_expr ( exprt expr ) const

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

Definition at line 38 of file guard_bdd.cpp.

◆ is_false()

bool guard_bddt::is_false ( ) const

inline

Definition at line 49 of file guard_bdd.h.

◆ is_true()

bool guard_bddt::is_true ( ) const

inline

Definition at line 44 of file guard_bdd.h.

◆ operator!()

guard_bddt guard_bddt::operator! ( ) const

inline

Definition at line 60 of file guard_bdd.h.

◆ operator=() [1/2]

guard_bddt & guard_bddt::operator= ( const guard_bddt & other )

Definition at line 24 of file guard_bdd.cpp.

◆ operator=() [2/2]

guard_bddt & guard_bddt::operator= ( guard_bddt && other )

Definition at line 31 of file guard_bdd.cpp.

Friends And Related Symbol Documentation

◆ operator-=

guard_bddt & operator-= ( guard_bddt & g1,

const guard_bddt & g2

)

friend

Transforms g1 into g1' such that ‘g1’ & g2 => g1 => g1'` and returns a reference to g1.

Definition at line 70 of file guard_bdd.cpp.

◆ operator|=

guard_bddt & operator|= ( guard_bddt & g1,

const guard_bddt & g2

)

friend

Definition at line 76 of file guard_bdd.cpp.

Member Data Documentation

◆ bdd

bddt guard_bddt::bdd

private

Definition at line 74 of file guard_bdd.h.

◆ is_always_simplified

constexpr bool guard_bddt::is_always_simplified = true

staticconstexpr

BDDs are always in a simplified form and thus no further simplification is required after calls to as_expr().

This can vary according to the guard implementation.

Definition at line 38 of file guard_bdd.h.

◆ manager

bdd_exprt& guard_bddt::manager

private

Definition at line 73 of file guard_bdd.h.

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

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