spot  2.7
Classes | Public Member Functions | Static Public Member Functions | List of all members
spot::fnode Class Referencefinal

Actual storage for formula nodes. More...

#include <spot/tl/formula.hh>

Collaboration diagram for spot::fnode:

Public Member Functions

const fnodeclone () const
 Clone an fnode. More...
 
void destroy () const
 Dereference an fnode. More...
 
op kind () const
 
std::string kindstr () const
 
bool is (op o) const
 
bool is (op o1, op o2) const
 
bool is (std::initializer_list< op > l) const
 
const fnodeget_child_of (op o) const
 
const fnodeget_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 fnodenth (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 fnodeall_but (unsigned i) const
 
unsigned boolean_count () const
 
const fnodeboolean_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
 

Static Public Member Functions

static constexpr uint8_t unbounded ()
 
static const fnodeap (const std::string &name)
 
static const fnodeunop (op o, const fnode *f)
 
static const fnodebinop (op o, const fnode *f, const fnode *g)
 
static const fnodemultop (op o, std::vector< const fnode *> l)
 
static const fnodebunop (op o, const fnode *f, uint8_t min, uint8_t max=unbounded())
 
static const fnodenested_unop_range (op uo, op bo, unsigned min, unsigned max, const fnode *f)
 
static const fnodeff ()
 
static const fnodett ()
 
static const fnodeeword ()
 
static const fnodeone_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

◆ all_but()

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

◆ 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

◆ 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

◆ boolean_operands()

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

◆ bunop()

static const fnode* spot::fnode::bunop ( op  o,
const fnode f,
uint8_t  min,
uint8_t  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

◆ has_lbt_atomic_props()

bool spot::fnode::has_lbt_atomic_props ( ) const
inline

◆ has_spin_atomic_props()

bool spot::fnode::has_spin_atomic_props ( ) const
inline

◆ 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

at the end of a program.

◆ is() [1/3]

bool spot::fnode::is ( op  o) const
inline
See also
formula::is

Referenced by is().

◆ is() [2/3]

bool spot::fnode::is ( op  o1,
op  o2 
) const
inline
See also
formula::is

◆ is() [3/3]

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

◆ is_constant()

bool spot::fnode::is_constant ( ) const
inline

◆ is_eventual()

bool spot::fnode::is_eventual ( ) const
inline

◆ 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

◆ is_in_nenoform()

bool spot::fnode::is_in_nenoform ( ) const
inline

◆ 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

◆ is_ltl_formula()

bool spot::fnode::is_ltl_formula ( ) const
inline

◆ is_marked()

bool spot::fnode::is_marked ( ) const
inline

◆ is_psl_formula()

bool spot::fnode::is_psl_formula ( ) const
inline

◆ is_sere_formula()

bool spot::fnode::is_sere_formula ( ) const
inline

◆ is_sugar_free_boolean()

bool spot::fnode::is_sugar_free_boolean ( ) const
inline

◆ is_sugar_free_ltl()

bool spot::fnode::is_sugar_free_ltl ( ) const
inline

◆ is_syntactic_guarantee()

bool spot::fnode::is_syntactic_guarantee ( ) const
inline

◆ is_syntactic_obligation()

bool spot::fnode::is_syntactic_obligation ( ) const
inline

◆ is_syntactic_persistence()

bool spot::fnode::is_syntactic_persistence ( ) const
inline

◆ is_syntactic_recurrence()

bool spot::fnode::is_syntactic_recurrence ( ) const
inline

◆ is_syntactic_safety()

bool spot::fnode::is_syntactic_safety ( ) const
inline

◆ is_syntactic_stutter_invariant()

bool spot::fnode::is_syntactic_stutter_invariant ( ) const
inline

◆ 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

◆ kind()

op spot::fnode::kind ( ) const
inline
See also
formula::kind

◆ kindstr()

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

◆ 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

◆ 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 ( )
inlinestatic
See also
formula::unbounded

References spot::ap.

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:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13