46#include <spot/misc/common.hh>
49#include <initializer_list>
63#if defined(SPOT_BUILD) or defined(SPOT_USES_STRONG_X)
66# define SPOT_HAS_STRONG_X 1
69# define SPOT_WANT_STRONG_X 1
78 enum class op: uint8_t
115#ifdef SPOT_WANT_STRONG_X
138 if (SPOT_UNLIKELY(!refs_))
150 if (SPOT_LIKELY(refs_))
152 else if (SPOT_LIKELY(!saturated_))
164 static const fnode*
ap(
const std::string& name);
173 unsigned min,
unsigned max = unbounded());
177 unsigned max,
const fnode* f);
197 return op_ == o1 || op_ == o2;
202 return op_ == o1 || op_ == o2 || op_ == o3;
207 return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
210 bool is(std::initializer_list<op> l)
const
212 const fnode* n =
this;
228 if (SPOT_UNLIKELY(size_ != 1))
229 report_get_child_of_expecting_single_child_node();
249 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
250 report_min_invalid_arg();
257 if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
258 report_max_invalid_arg();
289 return children + size();
295 if (SPOT_UNLIKELY(i >= size()))
296 report_non_existing_child();
297 const fnode* c = children[i];
298 SPOT_ASSUME(c !=
nullptr);
311 return op_ == op::ff;
323 return op_ == op::tt;
335 return op_ == op::eword;
341 return op_ == op::ff || op_ == op::tt || op_ == op::eword;
349 return min_ == 0 && max_ == unbounded();
356 one_star_ =
new fnode(op::Star, tt_, 0, unbounded(),
true);
364 one_plus_ =
new fnode(op::Star, tt_, 1, unbounded(),
true);
372 std::ostream&
dump(std::ostream& os)
const;
382 while (pos < s && children[pos]->is_boolean())
415 return is_.sugar_free_boolean;
421 return is_.in_nenoform;
427 return is_.syntactic_si;
433 return is_.sugar_free_ltl;
439 return is_.ltl_formula;
445 return is_.psl_formula;
451 return is_.sere_formula;
469 return is_.universal;
475 return is_.syntactic_safety;
481 return is_.syntactic_guarantee;
487 return is_.syntactic_obligation;
493 return is_.syntactic_recurrence;
499 return is_.syntactic_persistence;
505 return !is_.not_marked;
511 return is_.accepting_eword;
517 return is_.lbt_atomic_props;
523 return is_.spin_atomic_props;
527 static size_t bump_next_id();
528 void setup_props(
op o);
529 void destroy_aux()
const;
531 [[noreturn]]
static void report_non_existing_child();
532 [[noreturn]]
static void report_too_many_children();
533 [[noreturn]]
static void
534 report_get_child_of_expecting_single_child_node();
535 [[noreturn]]
static void report_min_invalid_arg();
536 [[noreturn]]
static void report_max_invalid_arg();
549 fnode(
op o, iter begin, iter end,
bool saturated =
false)
564 saturated_(saturated)
566 size_t s = std::distance(begin, end);
567 if (SPOT_UNLIKELY(s > (
size_t) UINT16_MAX))
568 report_too_many_children();
571 for (
auto i = begin; i != end; ++i)
576 fnode(op o, std::initializer_list<const fnode*> l,
577 bool saturated =
false)
578 : fnode(o, l.begin(), l.end(), saturated)
582 fnode(op o,
const fnode* f, uint8_t min, uint8_t max,
583 bool saturated =
false)
584 : op_(o), min_(min), max_(max), saturated_(saturated), size_(1)
590 static const fnode* ff_;
591 static const fnode* tt_;
592 static const fnode* ew_;
593 static const fnode* one_star_;
594 static const fnode* one_plus_;
599 mutable uint8_t saturated_;
601 mutable uint16_t refs_ = 0;
603 static size_t next_id_;
621 bool sugar_free_boolean:1;
624 bool sugar_free_ltl:1;
631 bool syntactic_safety:1;
632 bool syntactic_guarantee:1;
633 bool syntactic_obligation:1;
634 bool syntactic_recurrence:1;
635 bool syntactic_persistence:1;
637 bool accepting_eword:1;
638 bool lbt_atomic_props:1;
639 bool spin_atomic_props:1;
648 const fnode* children[1];
660 operator()(
const fnode* left,
const fnode* right)
const
680 auto get_literal = [](
const fnode* f) ->
const fnode*
689 const fnode* litl = get_literal(left);
690 const fnode* litr = get_literal(right);
703 size_t l = left->
id();
704 size_t r = right->
id();
717 std::ostringstream old;
719 std::ostringstream ord;
721 return old.str() < ord.str();
806 const formula& operator=(formula&& f)
noexcept
808 std::swap(f.ptr_, ptr_);
812 bool operator<(
const formula& other)
const noexcept
814 if (SPOT_UNLIKELY(!other.ptr_))
816 if (SPOT_UNLIKELY(!ptr_))
818 if (
id() < other.id())
820 if (
id() > other.id())
826 return ptr_ < other.ptr_;
829 bool operator<=(
const formula& other)
const noexcept
831 return *
this == other || *
this < other;
834 bool operator>(
const formula& other)
const noexcept
836 return !(*
this <= other);
839 bool operator>=(
const formula& other)
const noexcept
841 return !(*
this < other);
844 bool operator==(
const formula& other)
const noexcept
846 return other.ptr_ == ptr_;
849 bool operator==(std::nullptr_t)
const noexcept
851 return ptr_ ==
nullptr;
854 bool operator!=(
const formula& other)
const noexcept
856 return other.ptr_ != ptr_;
859 bool operator!=(std::nullptr_t)
const noexcept
861 return ptr_ !=
nullptr;
864 explicit operator bool() const noexcept
866 return ptr_ !=
nullptr;
876 return fnode::unbounded();
882 return formula(fnode::ap(name));
892 if (SPOT_UNLIKELY(a.
kind() != op::ap))
893 report_ap_invalid_arg();
915#define SPOT_DEF_UNOP(Name) \
916 static formula Name(const formula& f) \
918 return unop(op::Name, f); \
921#define SPOT_DEF_UNOP(Name) \
922 static formula Name(const formula& f) \
924 return unop(op::Name, f); \
926 static formula Name(formula&& f) \
928 return unop(op::Name, std::move(f)); \
946 return nested_unop_range(op::X, op::Or , level, level, f);
949#if SPOT_WANT_STRONG_X
952 SPOT_DEF_UNOP(strong_X);
960 return nested_unop_range(op::strong_X, op::Or ,
978 return nested_unop_range(op::X, op::Or, min_level, max_level, f);
989 return nested_unop_range(op::X, op::And, min_level, max_level, f);
999 SPOT_DEF_UNOP(Closure);
1004 SPOT_DEF_UNOP(NegClosure);
1009 SPOT_DEF_UNOP(NegClosureMarked);
1014 SPOT_DEF_UNOP(first_match);
1031 return formula(fnode::binop(o, f.ptr_->
clone(), g.to_node_()));
1048#define SPOT_DEF_BINOP(Name) \
1049 static formula Name(const formula& f, const formula& g) \
1051 return binop(op::Name, f, g); \
1054#define SPOT_DEF_BINOP(Name) \
1055 static formula Name(const formula& f, const formula& g) \
1057 return binop(op::Name, f, g); \
1059 static formula Name(const formula& f, formula&& g) \
1061 return binop(op::Name, f, std::move(g)); \
1063 static formula Name(formula&& f, const formula& g) \
1065 return binop(op::Name, std::move(f), g); \
1067 static formula Name(formula&& f, formula&& g) \
1069 return binop(op::Name, std::move(f), std::move(g)); \
1074 SPOT_DEF_BINOP(Xor);
1079 SPOT_DEF_BINOP(Implies);
1084 SPOT_DEF_BINOP(Equiv);
1109 SPOT_DEF_BINOP(EConcat);
1114 SPOT_DEF_BINOP(EConcatMarked);
1119 SPOT_DEF_BINOP(UConcat);
1121#undef SPOT_DEF_BINOP
1130 std::vector<const fnode*> tmp;
1131 tmp.reserve(l.size());
1134 tmp.emplace_back(f.ptr_->
clone());
1135 return formula(fnode::multop(o, std::move(tmp)));
1141 std::vector<const fnode*> tmp;
1142 tmp.reserve(l.size());
1146 return formula(fnode::multop(o, std::move(tmp)));
1152#define SPOT_DEF_MULTOP(Name) \
1153 static formula Name(const std::vector<formula>& l) \
1155 return multop(op::Name, l); \
1158#define SPOT_DEF_MULTOP(Name) \
1159 static formula Name(const std::vector<formula>& l) \
1161 return multop(op::Name, l); \
1164 static formula Name(std::vector<formula>&& l) \
1166 return multop(op::Name, std::move(l)); \
1171 SPOT_DEF_MULTOP(Or);
1176 SPOT_DEF_MULTOP(OrRat);
1181 SPOT_DEF_MULTOP(And);
1186 SPOT_DEF_MULTOP(AndRat);
1191 SPOT_DEF_MULTOP(AndNLM);
1196 SPOT_DEF_MULTOP(Concat);
1201 SPOT_DEF_MULTOP(Fusion);
1203#undef SPOT_DEF_MULTOP
1211 unsigned max = unbounded())
1213 return formula(fnode::bunop(o, f.ptr_->
clone(), min, max));
1219 unsigned max = unbounded())
1227#define SPOT_DEF_BUNOP(Name) \
1228 static formula Name(const formula& f, \
1229 unsigned min = 0U, \
1230 unsigned max = unbounded()) \
1232 return bunop(op::Name, f, min, max); \
1235#define SPOT_DEF_BUNOP(Name) \
1236 static formula Name(const formula& f, \
1237 unsigned min = 0U, \
1238 unsigned max = unbounded()) \
1240 return bunop(op::Name, f, min, max); \
1242 static formula Name(formula&& f, \
1243 unsigned min = 0U, \
1244 unsigned max = unbounded()) \
1246 return bunop(op::Name, std::move(f), min, max); \
1251 SPOT_DEF_BUNOP(Star);
1259 SPOT_DEF_BUNOP(FStar);
1261#undef SPOT_DEF_BUNOP
1277 return formula(fnode::nested_unop_range(uo, bo, min, max,
1317 unsigned min,
unsigned max);
1319 unsigned min,
unsigned max);
1343 return ptr_->kind();
1349 return ptr_->kindstr();
1362 return ptr_->is(o1, o2);
1368 return ptr_->is(o1, o2, o3);
1375 return ptr_->is(o1, o2, o3, o4);
1379 bool is(std::initializer_list<op> l)
const
1431 return ptr_->size();
1440 return ptr_->is_leaf();
1460 const fnode*
const* ptr_;
1474 return ptr_ == o.ptr_;
1479 return ptr_ != o.ptr_;
1484 return formula((*ptr_)->clone());
1504 return ptr_->begin();
1516 return formula(ptr_->nth(i)->clone());
1529 return ptr_->is_ff();
1541 return ptr_->is_tt();
1547 return formula(fnode::eword());
1553 return ptr_->is_eword();
1559 return ptr_->is_constant();
1568 return ptr_->is_Kleene_star();
1575 return formula(fnode::one_star());
1582 return formula(fnode::one_plus());
1589 return (is(op::ap) ||
1593 (is(op::Not) && is_boolean() && is_in_nenoform()));
1601 return ptr_->ap_name();
1608 std::ostream&
dump(std::ostream& os)
const
1610 return ptr_->dump(os);
1620 return formula(ptr_->all_but(i));
1634 return ptr_->boolean_count();
1652 return formula(ptr_->boolean_operands(width));
1655#define SPOT_DEF_PROP(Name) \
1658 return ptr_->Name(); \
1665 SPOT_DEF_PROP(is_boolean);
1667 SPOT_DEF_PROP(is_sugar_free_boolean);
1672 SPOT_DEF_PROP(is_in_nenoform);
1674 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1676 SPOT_DEF_PROP(is_sugar_free_ltl);
1678 SPOT_DEF_PROP(is_ltl_formula);
1680 SPOT_DEF_PROP(is_psl_formula);
1682 SPOT_DEF_PROP(is_sere_formula);
1685 SPOT_DEF_PROP(is_finite);
1693 SPOT_DEF_PROP(is_eventual);
1701 SPOT_DEF_PROP(is_universal);
1703 SPOT_DEF_PROP(is_syntactic_safety);
1705 SPOT_DEF_PROP(is_syntactic_guarantee);
1707 SPOT_DEF_PROP(is_syntactic_obligation);
1709 SPOT_DEF_PROP(is_syntactic_recurrence);
1711 SPOT_DEF_PROP(is_syntactic_persistence);
1714 SPOT_DEF_PROP(is_marked);
1716 SPOT_DEF_PROP(accepts_eword);
1722 SPOT_DEF_PROP(has_lbt_atomic_props);
1731 SPOT_DEF_PROP(has_spin_atomic_props);
1737 template<
typename Trans,
typename... Args>
1740 switch (
op o = kind())
1749#if SPOT_HAS_STRONG_X
1755 case op::NegClosure:
1756 case op::NegClosureMarked:
1757 case op::first_match:
1758 return unop(o, trans((*
this)[0], std::forward<Args>(args)...));
1767 case op::EConcatMarked:
1770 formula tmp = trans((*
this)[0], std::forward<Args>(args)...);
1771 return binop(o, tmp,
1772 trans((*
this)[1], std::forward<Args>(args)...));
1782 std::vector<formula> tmp;
1783 tmp.reserve(size());
1785 tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1786 return multop(o, std::move(tmp));
1790 return bunop(o, trans((*
this)[0], std::forward<Args>(args)...),
1804 template<
typename Func,
typename... Args>
1807 if (func(*
this, std::forward<Args>(args)...))
1810 f.
traverse(func, std::forward<Args>(args)...);
1815 [[noreturn]]
static void report_ap_invalid_arg();
1822 bool abbreviated =
false);
1830 std::ostream& operator<<(std::ostream& os,
const formula& f);
Actual storage for formula nodes.
Definition formula.hh:128
std::string kindstr() const
const fnode * boolean_operands(unsigned *width=nullptr) const
bool is_boolean() const
Definition formula.hh:407
size_t id() const
Definition formula.hh:275
bool is_ff() const
Definition formula.hh:309
bool is_sugar_free_boolean() const
Definition formula.hh:413
bool is_Kleene_star() const
Definition formula.hh:345
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
const fnode *const * end() const
Definition formula.hh:287
unsigned min() const
Definition formula.hh:247
bool is_syntactic_safety() const
Definition formula.hh:473
bool is_syntactic_stutter_invariant() const
Definition formula.hh:425
static const fnode * binop(op o, const fnode *f, const fnode *g)
unsigned size() const
Definition formula.hh:263
static constexpr uint8_t unbounded()
Definition formula.hh:158
const fnode * get_child_of(std::initializer_list< op > l) const
Definition formula.hh:234
unsigned max() const
Definition formula.hh:255
const fnode * get_child_of(op o) const
Definition formula.hh:224
const fnode * all_but(unsigned i) const
bool accepts_eword() const
Definition formula.hh:509
bool is_eventual() const
Definition formula.hh:461
bool is(op o1, op o2, op o3, op o4) const
Definition formula.hh:205
static bool instances_check()
safety check for the reference counters
bool is_leaf() const
Definition formula.hh:269
bool has_spin_atomic_props() const
Definition formula.hh:521
bool is_eword() const
Definition formula.hh:333
bool is(op o1, op o2, op o3) const
Definition formula.hh:200
op kind() const
Definition formula.hh:180
const fnode * clone() const
Clone an fnode.
Definition formula.hh:134
bool has_lbt_atomic_props() const
Definition formula.hh:515
bool is_sugar_free_ltl() const
Definition formula.hh:431
const std::string & ap_name() const
bool is_syntactic_persistence() const
Definition formula.hh:497
unsigned boolean_count() const
Definition formula.hh:378
static const fnode * tt()
Definition formula.hh:315
bool is_universal() const
Definition formula.hh:467
bool is_tt() const
Definition formula.hh:321
bool is_constant() const
Definition formula.hh:339
bool is_syntactic_recurrence() const
Definition formula.hh:491
bool is(std::initializer_list< op > l) const
Definition formula.hh:210
bool is_syntactic_obligation() const
Definition formula.hh:485
static const fnode * unop(op o, const fnode *f)
const fnode * nth(unsigned i) const
Definition formula.hh:293
bool is_ltl_formula() const
Definition formula.hh:437
static const fnode * ff()
Definition formula.hh:303
bool is_finite() const
Definition formula.hh:455
bool is_psl_formula() const
Definition formula.hh:443
static const fnode * eword()
Definition formula.hh:327
bool is_marked() const
Definition formula.hh:503
std::ostream & dump(std::ostream &os) const
void destroy() const
Dereference an fnode.
Definition formula.hh:148
static const fnode * one_plus()
Definition formula.hh:361
static const fnode * ap(const std::string &name)
bool is(op o1, op o2) const
Definition formula.hh:195
bool is_in_nenoform() const
Definition formula.hh:419
static const fnode * bunop(op o, const fnode *f, unsigned min, unsigned max=unbounded())
bool is_syntactic_guarantee() const
Definition formula.hh:479
static const fnode * multop(op o, std::vector< const fnode * > l)
bool is_sere_formula() const
Definition formula.hh:449
static const fnode * one_star()
Definition formula.hh:353
const fnode *const * begin() const
Definition formula.hh:281
bool is(op o) const
Definition formula.hh:190
op
Operator types.
Definition formula.hh:79
@ first_match
first_match(sere)
@ EConcatMarked
Seq, Marked.
@ NegClosure
Negated PSL Closure.
@ M
strong release (dual of weak until)
@ NegClosureMarked
marked version of the Negated PSL Closure
@ And
(omega-Rational) And
@ AndNLM
Non-Length-Matching Rational-And.
@ R
release (dual of until)
Definition automata.hh:27
int atomic_prop_cmp(const fnode *f, const fnode *g)
Order two atomic propositions.
std::list< std::string > list_formula_props(const formula &f)
List the properties of formula f.
std::ostream & print_formula_props(std::ostream &out, const formula &f, bool abbreviated=false)
Print the properties of formula f on stream out.