guard_bddt Class Reference

#include <guard_bdd.h>

Collaboration diagram for guard_bddt:

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

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(). More...

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. More...
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 21 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 66 of file guard_bdd.cpp.

append()

guard_bddt & guard_bddt::append

(

const guard_bddt &

guard

)

Definition at line 60 of file guard_bdd.cpp.

as_expr()

exprt guard_bddt::as_expr

(

)

const

Definition at line 84 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 40 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 26 of file guard_bdd.cpp.

operator=() [2/2]

guard_bddt & guard_bddt::operator=

(

guard_bddt &&

other

)

Definition at line 33 of file guard_bdd.cpp.

Friends And Related Function 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 72 of file guard_bdd.cpp.

operator|=

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

friend

Definition at line 78 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-documentation/cbmc-documentation/src/analyses/guard_bdd.h
• /home/runner/work/cbmc-documentation/cbmc-documentation/src/analyses/guard_bdd.cpp