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.
void	destroy () const
	Dereference an fnode.
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_sigma2 () const
bool	is_pi2 () const
bool	is_delta1 () const
bool	is_delta2 () 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 const fnode *	one_plus ()
static bool	instances_check ()
	safety check for the reference counters

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

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

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

static

See also: formula::binop

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

◆ boolean_count()

unsigned spot::fnode::boolean_count ( ) const

inline

See also: formula::boolean_count

References is_boolean(), and size().

◆ boolean_operands()

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

See also: formula::boolean_operands

◆ bunop()

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

static

See also: formula::bunop

References max(), min(), and unbounded().

Referenced by spot::formula::bunop(), and 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::binop(), 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 counter 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

References size().

◆ eword()

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

inlinestatic

See also: formula::eword

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

◆ ff()

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

References nth().

◆ 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

◆ 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()

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

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

Referenced by boolean_count().

◆ is_constant()

bool spot::fnode::is_constant ( ) const

inline

See also: formula::is_constant

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

◆ is_delta1()

bool spot::fnode::is_delta1 ( ) const

inline

See also: formula::is_delta1

◆ is_delta2()

bool spot::fnode::is_delta2 ( ) const

inline

See also: formula::is_delta2

◆ 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, and unbounded().

◆ 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_pi2()

bool spot::fnode::is_pi2 ( ) const

inline

See also: formula::is_pi2

◆ 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_sigma2()

bool spot::fnode::is_sigma2 ( ) const

inline

See also: formula::is_sigma2

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

Referenced by bunop(), and nested_unop_range().

◆ min()

unsigned spot::fnode::min ( ) const

inline

See also: formula::min

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

Referenced by bunop(), and nested_unop_range().

◆ multop()

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

static

See also: formula::multop

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

◆ nested_unop_range()

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

References max(), and min().

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

◆ nth()

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

inline

See also: formula::nth

References size().

Referenced by get_child_of(), and is().

◆ one_plus()

const fnode * spot::fnode::one_plus ( )

inlinestatic

See also: formula::one_plus

References spot::Star, and unbounded().

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

◆ one_star()

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

inlinestatic

See also: formula::one_star

References spot::Star, and unbounded().

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

◆ size()

unsigned spot::fnode::size ( ) const

inline

See also: formula::size

Referenced by boolean_count(), end(), and nth().

◆ tt()

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

inlinestatic

See also: formula::tt

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

◆ unbounded()

constexpr uint8_t spot::fnode::unbounded ( )

inlinestaticconstexpr

See also: formula::unbounded

Referenced by bunop(), is_Kleene_star(), one_plus(), one_star(), and spot::formula::unbounded().

◆ unop()

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

static

See also: formula::unop

Referenced by spot::formula::unop(), and 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_delta1()

◆ is_delta2()

◆ is_eventual()

◆ is_eword()

◆ is_ff()

◆ is_finite()

◆ is_in_nenoform()

◆ is_Kleene_star()

◆ is_leaf()

◆ is_ltl_formula()

◆ is_marked()

◆ is_pi2()

◆ is_psl_formula()

◆ is_sere_formula()

◆ is_sigma2()

◆ 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_plus()

◆ one_star()

◆ size()

◆ tt()

◆ unbounded()

◆ unop()