formula.hh File Reference

LTL/PSL formula interface. More...

#include <spot/misc/common.hh>
#include <memory>
#include <cstdint>
#include <initializer_list>
#include <cassert>
#include <vector>
#include <string>
#include <iterator>
#include <iosfwd>
#include <sstream>
#include <list>
#include <cstddef>
#include <limits>

Include dependency graph for formula.hh:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	spot::fnode
	Actual storage for formula nodes. More...
struct	spot::formula_ptr_less_than_bool_first
class	spot::formula
	Main class for temporal logic formula. More...
class	spot::formula::formula_child_iterator
	Allow iterating over children. More...
struct	std::hash< spot::formula >

Namespaces
	spot

Macros
#define	SPOT_DEF_UNOP(Name)
#define	SPOT_DEF_BINOP(Name)
#define	SPOT_DEF_MULTOP(Name)
#define	SPOT_DEF_BUNOP(Name)
#define	SPOT_DEF_PROP(Name)

Enumerations
enum class	spot::op : uint8_t {   spot::ff , spot::tt , spot::eword , spot::ap ,   spot::Not , spot::X , spot::F , spot::G ,   spot::Closure , spot::NegClosure , spot::NegClosureMarked , spot::Xor ,   spot::Implies , spot::Equiv , spot::U , spot::R ,   spot::W , spot::M , spot::EConcat , spot::EConcatMarked ,   spot::UConcat , spot::Or , spot::OrRat , spot::And ,   spot::AndRat , spot::AndNLM , spot::Concat , spot::Fusion ,   spot::Star , spot::FStar , spot::first_match }
	Operator types. More...

Functions
int	spot::atomic_prop_cmp (const fnode *f, const fnode *g)
	Order two atomic propositions. More...
std::ostream &	spot::print_formula_props (std::ostream &out, const formula &f, bool abbreviated=false)
	Print the properties of formula f on stream out. More...
std::list< std::string >	spot::list_formula_props (const formula &f)
	List the properties of formula f. More...
std::ostream &	spot::operator<< (std::ostream &os, const formula &f)
	Print a formula. More...

Detailed Description

LTL/PSL formula interface.

Macro Definition Documentation

SPOT_DEF_BINOP

#define SPOT_DEF_BINOP

(

Name

)

Value:

    static formula Name(const formula& f, const formula& g)          \
    {                                                                \
      return binop(op::Name, f, g);                                  \
    }                                                                \
    static formula Name(const formula& f, formula&& g)               \
    {                                                                \
      return binop(op::Name, f, std::move(g));                       \
    }                                                                \
    static formula Name(formula&& f, const formula& g)               \
    {                                                                \
      return binop(op::Name, std::move(f), g);                       \
    }                                                                \
    static formula Name(formula&& f, formula&& g)                    \
    {                                                                \
      return binop(op::Name, std::move(f), std::move(g));            \
    }

SPOT_DEF_BUNOP

#define SPOT_DEF_BUNOP

(

Name

)

Value:

    static formula Name(const formula& f,                   \
        unsigned min = 0U,                                  \
        unsigned max = unbounded())                         \
    {                                                       \
      return bunop(op::Name, f, min, max);                  \
    }                                                       \
    static formula Name(formula&& f,                        \
        unsigned min = 0U,                                  \
        unsigned max = unbounded())                         \
    {                                                       \
      return bunop(op::Name, std::move(f), min, max);       \
    }

SPOT_DEF_MULTOP

#define SPOT_DEF_MULTOP

(

Name

)

Value:

    static formula Name(const std::vector<formula>& l)       \
    {                                                        \
      return multop(op::Name, l);                            \
    }                                                        \
    \
    static formula Name(std::vector<formula>&& l)            \
    {                                                        \
      return multop(op::Name, std::move(l));                 \
    }

SPOT_DEF_PROP

#define SPOT_DEF_PROP

(

Name

)

Value:

    bool Name() const                              \
    {                                              \
      return ptr_->Name();                         \
    }

SPOT_DEF_UNOP

#define SPOT_DEF_UNOP

(

Name

)

Value:

    static formula Name(const formula& f)            \
    {                                                \
      return unop(op::Name, f);                      \
    }                                                \
    static formula Name(formula&& f)                 \
    {                                                \
      return unop(op::Name, std::move(f));           \
    }