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
	Comparator for formula pointers that orders Boolean formulas before others. More...
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 >
	Hash specialization for spot::formula using its unique identifier. More...

Namespaces
	spot

Macros
#define	SPOT_HAS_STRONG_X   1
	Defined when strong X operator is available. More...
#define	SPOT_WANT_STRONG_X   1
	Legacy macro; prefer SPOT_HAS_STRONG_X. More...
#define	SPOT_HAS_QUANTIFIERS   1
	Defined when the exists/forall operators are available. More...

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 , spot::strong_X ,   spot::exists , spot::forall }
	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_HAS_QUANTIFIERS

#define SPOT_HAS_QUANTIFIERS   1

Defined when the exists/forall operators are available.

SPOT_HAS_STRONG_X

#define SPOT_HAS_STRONG_X   1

Defined when strong X operator is available.

SPOT_WANT_STRONG_X

#define SPOT_WANT_STRONG_X   1

Legacy macro; prefer SPOT_HAS_STRONG_X.