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
namespace	spot

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

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

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

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.