Actual storage for formula nodes. More...

#include <spot/tl/formula.hh>

Collaboration diagram for spot::fnode:

Public Member Functions
const fnode *	clone () const
	Clone an fnode. More...

void	destroy () const
	Dereference an fnode. More...

op	kind () const

std::string	kindstr () const

const fnode *	get_child_of (op o) const

const fnode *	get_child_of (std::initializer_list< op > l) const

unsigned	min () const

unsigned	max () const

unsigned	size () const

bool	is_leaf () const

size_t	id () const

const fnode const	begin () const

const fnode const	end () const

const fnode *	nth (unsigned i) const

bool	is_ff () const

bool	is_tt () const

bool	is_eword () const

bool	is_constant () const

bool	is_Kleene_star () const

const std::string &	ap_name () const

std::ostream &	dump (std::ostream &os) const

const fnode *	all_but (unsigned i) const

unsigned	boolean_count () const

const fnode *	boolean_operands (unsigned *width=nullptr) const

bool	is_boolean () const

bool	is_sugar_free_boolean () const

bool	is_in_nenoform () const

bool	is_syntactic_stutter_invariant () const

bool	is_sugar_free_ltl () const

bool	is_ltl_formula () const

bool	is_psl_formula () const

bool	is_sere_formula () const

bool	is_finite () const

bool	is_eventual () const

bool	is_universal () const

bool	is_syntactic_safety () const

bool	is_syntactic_guarantee () const

bool	is_syntactic_obligation () const

bool	is_syntactic_recurrence () const

bool	is_syntactic_persistence () const

bool	is_marked () const

bool	accepts_eword () const

bool	has_lbt_atomic_props () const

bool	has_spin_atomic_props () const


bool	is (op o) const

bool	is (op o1, op o2) const

bool	is (op o1, op o2, op o3) const

bool	is (op o1, op o2, op o3, op o4) const

bool	is (std::initializer_list< op > l) const

Static Public Member Functions
static constexpr uint8_t	unbounded ()

static const fnode *	ap (const std::string &name)

static const fnode *	unop (op o, const fnode *f)

static const fnode *	binop (op o, const fnode f, const fnode g)

static const fnode *	multop (op o, std::vector< const fnode * > l)

static const fnode *	bunop (op o, const fnode *f, unsigned min, unsigned max=unbounded())

static const fnode *	nested_unop_range (op uo, op bo, unsigned min, unsigned max, const fnode *f)

static const fnode *	ff ()

static const fnode *	tt ()

static const fnode *	eword ()

static const fnode *	one_star ()

static bool	instances_check ()
	safety check for the reference counters More...

Detailed Description

Actual storage for formula nodes.

spot::formula objects contain references to instances of this class, and delegate most of their methods. Because spot::formula is meant to be the public interface, most of the methods are documented there, rather than here.

Member Function Documentation

◆ accepts_eword()

bool spot::fnode::accepts_eword ( ) const

inline

See also: formula::accepts_eword

◆ all_but()

const fnode* spot::fnode::all_but ( unsigned i ) const

See also: formula::all_but

◆ ap()

static const fnode* spot::fnode::ap ( const std::string & name )

static

See also: formula::ap

Referenced by spot::formula::ap().

◆ ap_name()

const std::string& spot::fnode::ap_name ( ) const

See also: formula::ap_name

◆ begin()

const fnode* const* spot::fnode::begin ( ) const

inline

See also: formula::begin

◆ binop()

static const fnode* spot::fnode::binop	(	op	o,
		const fnode *	f,
		const fnode *	g
	)

static

See also: formula::binop

Referenced by spot::formula::binop().

◆ boolean_count()

unsigned spot::fnode::boolean_count ( ) const

inline

See also: formula::boolean_count

◆ boolean_operands()

const fnode* spot::fnode::boolean_operands ( unsigned * width = nullptr ) const

See also: formula::boolean_operands

◆ bunop()

static const fnode* spot::fnode::bunop	(	op	o,
		const fnode *	f,
		unsigned	min,
		unsigned	max = `unbounded()`
	)

static

See also: formula::bunop

Referenced by spot::formula::bunop().

◆ clone()

const fnode* spot::fnode::clone ( ) const

inline

Clone an fnode.

This simply increment the reference counter. If the counter saturates, the fnode will stay permanently allocated.

Referenced by spot::formula::binop(), spot::formula::bunop(), spot::formula::multop(), spot::formula::nested_unop_range(), and spot::formula::unop().

◆ destroy()

void spot::fnode::destroy ( ) const

inline

Dereference an fnode.

This decrement the reference counter (unless the counter is saturated), and actually deallocate the fnode when the counder reaches 0 (unless the fnode denotes a constant).

◆ dump()

std::ostream& spot::fnode::dump ( std::ostream & os ) const

See also: formula::dump

◆ end()

const fnode* const* spot::fnode::end ( ) const

inline

See also: formula::end

◆ eword()

static const fnode* spot::fnode::eword ( )

inlinestatic

See also: formula::eword

Referenced by spot::formula::eword().

◆ ff()

static const fnode* spot::fnode::ff ( )

inlinestatic

See also: formula::ff

Referenced by spot::formula::ff().

◆ get_child_of() [1/2]

const fnode* spot::fnode::get_child_of ( op o ) const

inline

See also: formula::get_child_of

Referenced by get_child_of().

◆ get_child_of() [2/2]

const fnode* spot::fnode::get_child_of ( std::initializer_list< op > l ) const

inline

See also: formula::get_child_of

References get_child_of().

◆ has_lbt_atomic_props()

bool spot::fnode::has_lbt_atomic_props ( ) const

inline

See also: formula::has_lbt_atomic_props

◆ has_spin_atomic_props()

bool spot::fnode::has_spin_atomic_props ( ) const

inline

See also: formula::has_spin_atomic_props

◆ id()

size_t spot::fnode::id ( ) const

inline

See also: formula::id

◆ instances_check()

static bool spot::fnode::instances_check ( )

static

safety check for the reference counters

Returns: true iff the unicity map contains only the globally pre-allocated formulas.

This is meant to be used as

assert(spot::fnode::instances_check());

spot::fnode::instances_check

static bool instances_check()

safety check for the reference counters

at the end of a program.

◆ is() [1/5]

bool spot::fnode::is ( op o ) const

inline

See also: formula::is

Referenced by is().

◆ is() [2/5]

bool spot::fnode::is	(	op	o1,
		op	o2
	)		const

inline

See also: formula::is

◆ is() [3/5]

bool spot::fnode::is	(	op	o1,
		op	o2,
		op	o3
	)		const

inline

See also: formula::is

◆ is() [4/5]

bool spot::fnode::is	(	op	o1,
		op	o2,
		op	o3,
		op	o4
	)		const

inline

See also: formula::is

◆ is() [5/5]

bool spot::fnode::is ( std::initializer_list< op > l ) const

inline

See also: formula::is

References is(), and nth().

◆ is_boolean()

bool spot::fnode::is_boolean ( ) const

inline

See also: formula::is_boolean

◆ is_constant()

bool spot::fnode::is_constant ( ) const

inline

See also: formula::is_constant

References spot::eword, spot::ff, and spot::tt.

◆ is_eventual()

bool spot::fnode::is_eventual ( ) const

inline

See also: formula::is_eventual

◆ is_eword()

bool spot::fnode::is_eword ( ) const

inline

See also: formula::is_eword

References spot::eword.

◆ is_ff()

bool spot::fnode::is_ff ( ) const

inline

See also: formula::is_ff

References spot::ff.

◆ is_finite()

bool spot::fnode::is_finite ( ) const

inline

See also: formula::is_finite

◆ is_in_nenoform()

bool spot::fnode::is_in_nenoform ( ) const

inline

See also: formula::is_in_nenoform

◆ is_Kleene_star()

bool spot::fnode::is_Kleene_star ( ) const

inline

See also: formula::is_Kleene_star

References spot::Star.

◆ is_leaf()

bool spot::fnode::is_leaf ( ) const

inline

See also: formula::is_leaf

◆ is_ltl_formula()

bool spot::fnode::is_ltl_formula ( ) const

inline

See also: formula::is_ltl_formula

◆ is_marked()

bool spot::fnode::is_marked ( ) const

inline

See also: formula::is_marked

◆ is_psl_formula()

bool spot::fnode::is_psl_formula ( ) const

inline

See also: formula::is_psl_formula

◆ is_sere_formula()

bool spot::fnode::is_sere_formula ( ) const

inline

See also: formula::is_sere_formula

◆ is_sugar_free_boolean()

bool spot::fnode::is_sugar_free_boolean ( ) const

inline

See also: formula::is_sugar_free_boolean

◆ is_sugar_free_ltl()

bool spot::fnode::is_sugar_free_ltl ( ) const

inline

See also: formula::is_sugar_free_ltl

◆ is_syntactic_guarantee()

bool spot::fnode::is_syntactic_guarantee ( ) const

inline

See also: formula::is_syntactic_guarantee

◆ is_syntactic_obligation()

bool spot::fnode::is_syntactic_obligation ( ) const

inline

See also: formula::is_syntactic_obligation

◆ is_syntactic_persistence()

bool spot::fnode::is_syntactic_persistence ( ) const

inline

See also: formula::is_syntactic_persistence

◆ is_syntactic_recurrence()

bool spot::fnode::is_syntactic_recurrence ( ) const

inline

See also: formula::is_syntactic_recurrence

◆ is_syntactic_safety()

bool spot::fnode::is_syntactic_safety ( ) const

inline

See also: formula::is_syntactic_safety

◆ is_syntactic_stutter_invariant()

bool spot::fnode::is_syntactic_stutter_invariant ( ) const

inline

See also: formula::is_syntactic_stutter_invariant

◆ is_tt()

bool spot::fnode::is_tt ( ) const

inline

See also: formula::is_tt

References spot::tt.

◆ is_universal()

bool spot::fnode::is_universal ( ) const

inline

See also: formula::is_universal

◆ kind()

op spot::fnode::kind ( ) const

inline

See also: formula::kind

◆ kindstr()

std::string spot::fnode::kindstr ( ) const

See also: formula::kindstr

◆ max()

unsigned spot::fnode::max ( ) const

inline

See also: formula::max

References spot::FStar, and spot::Star.

◆ min()

unsigned spot::fnode::min ( ) const

inline

See also: formula::min

References spot::FStar, and spot::Star.

◆ multop()

static const fnode* spot::fnode::multop	(	op	o,
		std::vector< const fnode * >	l
	)

static

See also: formula::multop

Referenced by spot::formula::multop().

◆ nested_unop_range()

static const fnode* spot::fnode::nested_unop_range	(	op	uo,
		op	bo,
		unsigned	min,
		unsigned	max,
		const fnode *	f
	)

static

See also: formula::nested_unop_range

Referenced by spot::formula::nested_unop_range().

◆ nth()

const fnode* spot::fnode::nth ( unsigned i ) const

inline

See also: formula::nth

Referenced by is().

◆ one_star()

static const fnode* spot::fnode::one_star ( )

inlinestatic

See also: formula::one_star

References spot::Star, and spot::tt.

Referenced by spot::formula::one_star().

◆ size()

unsigned spot::fnode::size ( ) const

inline

See also: formula::size

◆ tt()

static const fnode* spot::fnode::tt ( )

inlinestatic

See also: formula::tt

Referenced by spot::formula::tt().

◆ unbounded()

static constexpr uint8_t spot::fnode::unbounded ( )

inlinestaticconstexpr

See also: formula::unbounded

Referenced by spot::formula::unbounded().

◆ unop()

static const fnode* spot::fnode::unop	(	op	o,
		const fnode *	f
	)

static

See also: formula::unop

Referenced by spot::formula::unop().

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

spot/tl/formula.hh

Public Member Functions

Static Public Member Functions

Detailed Description

Member Function Documentation

◆ accepts_eword()

◆ all_but()

◆ ap()

◆ ap_name()

◆ begin()

◆ binop()

◆ boolean_count()

◆ boolean_operands()

◆ bunop()

◆ clone()

◆ destroy()

◆ dump()

◆ end()

◆ eword()

◆ ff()

◆ get_child_of() [1/2]

◆ get_child_of() [2/2]

◆ has_lbt_atomic_props()

◆ has_spin_atomic_props()

◆ id()

◆ instances_check()

◆ is() [1/5]

◆ is() [2/5]

◆ is() [3/5]

◆ is() [4/5]

◆ is() [5/5]

◆ is_boolean()

◆ is_constant()

◆ is_eventual()

◆ is_eword()

◆ is_ff()

◆ is_finite()

◆ is_in_nenoform()

◆ is_Kleene_star()

◆ is_leaf()

◆ is_ltl_formula()

◆ is_marked()

◆ is_psl_formula()

◆ is_sere_formula()

◆ is_sugar_free_boolean()

◆ is_sugar_free_ltl()

◆ is_syntactic_guarantee()

◆ is_syntactic_obligation()

◆ is_syntactic_persistence()

◆ is_syntactic_recurrence()

◆ is_syntactic_safety()

◆ is_syntactic_stutter_invariant()

◆ is_tt()

◆ is_universal()

◆ kind()

◆ kindstr()

◆ max()

◆ min()

◆ multop()

◆ nested_unop_range()

◆ nth()

◆ one_star()

◆ size()

◆ tt()

◆ unbounded()

◆ unop()