43 #include <spot/misc/common.hh> 46 #include <initializer_list> 55 #include <initializer_list> 62 enum class op: uint8_t
101 class SPOT_API fnode final
118 if (SPOT_UNLIKELY(!refs_))
130 if (SPOT_LIKELY(refs_))
132 else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
144 static const fnode*
ap(
const std::string& name);
146 static const fnode* unop(
op o,
const fnode* f);
148 static const fnode* binop(
op o,
const fnode* f,
const fnode* g);
150 static const fnode* multop(
op o, std::vector<const fnode*> l);
152 static const fnode* bunop(
op o,
const fnode* f,
153 uint8_t min, uint8_t max = unbounded());
162 std::string kindstr()
const;
173 return op_ == o1 || op_ == o2;
177 bool is(std::initializer_list<op> l)
const 179 const fnode* n =
this;
194 if (SPOT_UNLIKELY(size_ != 1))
195 report_get_child_of_expecting_single_child_node();
216 report_min_invalid_arg();
224 report_max_invalid_arg();
247 const fnode*
const*
end()
const 249 return children + size();
253 const fnode*
nth(
unsigned i)
const 255 if (SPOT_UNLIKELY(i >= size()))
256 report_non_existing_child();
261 static const fnode*
ff()
273 static const fnode*
tt()
307 return min_ == 0 && max_ == unbounded();
319 const std::string& ap_name()
const;
322 std::ostream& dump(std::ostream& os)
const;
325 const fnode* all_but(
unsigned i)
const;
332 while (pos < s && children[pos]->is_boolean())
338 const fnode* boolean_operands(
unsigned* width =
nullptr)
const;
350 static bool instances_check();
365 return is_.sugar_free_boolean;
371 return is_.in_nenoform;
377 return is_.syntactic_si;
383 return is_.sugar_free_ltl;
389 return is_.ltl_formula;
395 return is_.psl_formula;
401 return is_.sere_formula;
419 return is_.universal;
425 return is_.syntactic_safety;
431 return is_.syntactic_guarantee;
437 return is_.syntactic_obligation;
443 return is_.syntactic_recurrence;
449 return is_.syntactic_persistence;
455 return !is_.not_marked;
461 return is_.accepting_eword;
467 return is_.lbt_atomic_props;
473 return is_.spin_atomic_props;
477 void setup_props(
op o);
478 void destroy_aux()
const;
480 [[noreturn]]
static void report_non_existing_child();
481 [[noreturn]]
static void report_too_many_children();
482 [[noreturn]]
static void 483 report_get_child_of_expecting_single_child_node();
484 [[noreturn]]
static void report_min_invalid_arg();
485 [[noreturn]]
static void report_max_invalid_arg();
487 static const fnode* unique(
const fnode*);
492 fnode(
const fnode&) =
delete;
493 fnode& operator=(
const fnode&) =
delete;
498 fnode(
op o, iter begin, iter end)
515 size_t s = std::distance(begin, end);
516 if (SPOT_UNLIKELY(s > (
size_t) UINT16_MAX))
517 report_too_many_children();
520 for (
auto i = begin; i != end; ++i)
525 fnode(
op o, std::initializer_list<const fnode*> l)
526 : fnode(o, l.begin(), l.end())
530 fnode(
op o,
const fnode* f, uint8_t min, uint8_t max)
531 : op_(o), min_(min), max_(max), saturated_(0), size_(1)
537 static const fnode* ff_;
538 static const fnode* tt_;
539 static const fnode* ew_;
540 static const fnode* one_star_;
545 mutable uint8_t saturated_;
547 mutable uint16_t refs_ = 0;
549 static size_t next_id_;
567 bool sugar_free_boolean:1;
570 bool sugar_free_ltl:1;
577 bool syntactic_safety:1;
578 bool syntactic_guarantee:1;
579 bool syntactic_obligation:1;
580 bool syntactic_recurrence:1;
581 bool syntactic_persistence:1;
583 bool accepting_eword:1;
584 bool lbt_atomic_props:1;
585 bool spin_atomic_props:1;
594 const fnode* children[1];
604 operator()(
const fnode* left,
const fnode* right)
const 624 auto get_literal = [](
const fnode* f) ->
const fnode*
633 const fnode* litl = get_literal(left);
634 const fnode* litr = get_literal(right);
640 int cmp = atomic_prop_cmp(litl, litr);
647 size_t l = left->
id();
648 size_t r = right->
id();
661 std::ostringstream old;
663 std::ostringstream ord;
665 return old.str() < ord.str();
748 std::swap(f.ptr_, ptr_);
752 bool operator<(
const formula& other)
const noexcept
754 if (SPOT_UNLIKELY(!other.ptr_))
756 if (SPOT_UNLIKELY(!ptr_))
758 if (
id() < other.
id())
760 if (
id() > other.
id())
766 return ptr_ < other.ptr_;
769 bool operator<=(
const formula& other)
const noexcept
771 return *
this == other || *
this < other;
774 bool operator>(
const formula& other)
const noexcept
776 return !(*
this <= other);
779 bool operator>=(
const formula& other)
const noexcept
781 return !(*
this < other);
784 bool operator==(
const formula& other)
const noexcept
786 return other.ptr_ == ptr_;
789 bool operator==(std::nullptr_t)
const noexcept
791 return ptr_ ==
nullptr;
794 bool operator!=(
const formula& other)
const noexcept
796 return other.ptr_ != ptr_;
799 bool operator!=(std::nullptr_t)
const noexcept
801 return ptr_ !=
nullptr;
804 operator bool()
const 806 return ptr_ !=
nullptr;
833 report_ap_invalid_arg();
855 #define SPOT_DEF_UNOP(Name) \ 856 static formula Name(const formula& f) \ 858 return unop(op::Name, f); \ 861 #define SPOT_DEF_UNOP(Name) \ 862 static formula Name(const formula& f) \ 864 return unop(op::Name, f); \ 866 static formula Name(formula&& f) \ 868 return unop(op::Name, std::move(f)); \ 937 #define SPOT_DEF_BINOP(Name) \ 938 static formula Name(const formula& f, const formula& g) \ 940 return binop(op::Name, f, g); \ 943 #define SPOT_DEF_BINOP(Name) \ 944 static formula Name(const formula& f, const formula& g) \ 946 return binop(op::Name, f, g); \ 948 static formula Name(const formula& f, formula&& g) \ 950 return binop(op::Name, f, std::move(g)); \ 952 static formula Name(formula&& f, const formula& g) \ 954 return binop(op::Name, std::move(f), g); \ 956 static formula Name(formula&& f, formula&& g) \ 958 return binop(op::Name, std::move(f), std::move(g)); \ 1010 #undef SPOT_DEF_BINOP 1019 std::vector<const fnode*> tmp;
1020 tmp.reserve(l.size());
1023 tmp.emplace_back(f.ptr_->
clone());
1030 std::vector<const fnode*> tmp;
1031 tmp.reserve(l.size());
1041 #define SPOT_DEF_MULTOP(Name) \ 1042 static formula Name(const std::vector<formula>& l) \ 1044 return multop(op::Name, l); \ 1047 #define SPOT_DEF_MULTOP(Name) \ 1048 static formula Name(const std::vector<formula>& l) \ 1050 return multop(op::Name, l); \ 1053 static formula Name(std::vector<formula>&& l) \ 1055 return multop(op::Name, std::move(l)); \ 1058 SPOT_DEF_MULTOP(
Or);
1092 #undef SPOT_DEF_MULTOP 1100 uint8_t max = unbounded())
1108 uint8_t max = unbounded())
1116 #define SPOT_DEF_BUNOP(Name) \ 1117 static formula Name(const formula& f, \ 1119 uint8_t max = unbounded()) \ 1121 return bunop(op::Name, f, min, max); \ 1124 #define SPOT_DEF_BUNOP(Name) \ 1125 static formula Name(const formula& f, \ 1127 uint8_t max = unbounded()) \ 1129 return bunop(op::Name, f, min, max); \ 1131 static formula Name(formula&& f, \ 1133 uint8_t max = unbounded()) \ 1135 return bunop(op::Name, std::move(f), min, max); \ 1138 SPOT_DEF_BUNOP(
Star);
1162 SPOT_DEF_BUNOP(
FStar);
1165 #undef SPOT_DEF_BUNOP 1172 static formula sugar_goto(
const formula& b, uint8_t min, uint8_t max);
1179 static formula sugar_equal(
const formula& b, uint8_t min, uint8_t max);
1182 const fnode* to_node_()
1202 return ptr_->kind();
1208 return ptr_->kindstr();
1218 bool is(
op o1,
op o2)
const 1221 return ptr_->is(o1, o2);
1225 bool is(std::initializer_list<op> l)
const 1243 formula get_child_of(std::initializer_list<op> l)
const 1277 return ptr_->size();
1294 class SPOT_API formula_child_iterator final
1297 const fnode*
const* ptr_;
1299 formula_child_iterator()
1304 formula_child_iterator(
const fnode*
const* f)
1309 bool operator==(formula_child_iterator o)
1311 return ptr_ == o.ptr_;
1314 bool operator!=(formula_child_iterator o)
1316 return ptr_ != o.ptr_;
1321 return formula((*ptr_)->clone());
1324 formula_child_iterator operator++()
1330 formula_child_iterator operator++(
int)
1341 return ptr_->begin();
1345 formula_child_iterator
end()
const 1353 return formula(ptr_->nth(i)->clone());
1366 return ptr_->is_ff();
1378 return ptr_->is_tt();
1390 return ptr_->is_eword();
1396 return ptr_->is_constant();
1405 return ptr_->is_Kleene_star();
1422 (is(
op::Not) && is_boolean() && is_in_nenoform()));
1430 return ptr_->ap_name();
1437 std::ostream&
dump(std::ostream& os)
const 1439 return ptr_->dump(os);
1449 return formula(ptr_->all_but(i));
1463 return ptr_->boolean_count();
1481 return formula(ptr_->boolean_operands(width));
1484 #define SPOT_DEF_PROP(Name) \ 1487 return ptr_->Name(); \ 1494 SPOT_DEF_PROP(is_boolean);
1496 SPOT_DEF_PROP(is_sugar_free_boolean);
1501 SPOT_DEF_PROP(is_in_nenoform);
1503 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1505 SPOT_DEF_PROP(is_sugar_free_ltl);
1507 SPOT_DEF_PROP(is_ltl_formula);
1509 SPOT_DEF_PROP(is_psl_formula);
1511 SPOT_DEF_PROP(is_sere_formula);
1514 SPOT_DEF_PROP(is_finite);
1532 SPOT_DEF_PROP(is_eventual);
1558 SPOT_DEF_PROP(is_syntactic_safety);
1560 SPOT_DEF_PROP(is_syntactic_guarantee);
1562 SPOT_DEF_PROP(is_syntactic_obligation);
1564 SPOT_DEF_PROP(is_syntactic_recurrence);
1566 SPOT_DEF_PROP(is_syntactic_persistence);
1569 SPOT_DEF_PROP(is_marked);
1571 SPOT_DEF_PROP(accepts_eword);
1577 SPOT_DEF_PROP(has_lbt_atomic_props);
1586 SPOT_DEF_PROP(has_spin_atomic_props);
1587 #undef SPOT_DEF_PROP 1590 template<
typename Trans>
1593 switch (
op o = kind())
1607 return unop(o, trans((*
this)[0]));
1619 formula tmp = trans((*
this)[0]);
1620 return binop(o, tmp, trans((*
this)[1]));
1630 std::vector<formula> tmp;
1631 tmp.reserve(size());
1633 tmp.emplace_back(trans(f));
1634 return multop(o, std::move(tmp));
1638 return bunop(o, trans((*
this)[0]), min(), max());
1648 template<
typename Func>
1659 [[noreturn]]
static void report_ap_invalid_arg();
1666 bool abbreviated =
false);
1674 std::ostream& operator<<(std::ostream& os,
const formula& f);
const fnode *const * begin() const
Definition: formula.hh:241
Definition: automata.hh:26
bool is_boolean() const
Definition: formula.hh:357
static const fnode * eword()
Definition: formula.hh:285
static const fnode * ap(const std::string &name)
std::ostream & dump(std::ostream &os) const
unsigned max() const
Definition: formula.hh:221
size_t id() const
Definition: formula.hh:235
bool is(op o) const
Definition: formula.hh:165
bool is_psl_formula() const
Definition: formula.hh:393
static const fnode * unop(op o, const fnode *f)
bool is_finite() const
Definition: formula.hh:405
bool is_eword() const
Definition: formula.hh:291
unsigned boolean_count() const
Definition: formula.hh:328
const fnode * get_child_of(op o) const
Definition: formula.hh:190
Definition: formula.hh:1678
bool is_syntactic_guarantee() const
Definition: formula.hh:429
static const fnode * tt()
Definition: formula.hh:273
bool is_syntactic_persistence() const
Definition: formula.hh:447
const fnode * nth(unsigned i) const
Definition: formula.hh:253
bool is_marked() const
Definition: formula.hh:453
bool is_syntactic_recurrence() const
Definition: formula.hh:441
bool is(std::initializer_list< op > l) const
Definition: formula.hh:177
bool is_syntactic_obligation() const
Definition: formula.hh:435
bool is(op o1, op o2) const
Definition: formula.hh:171
bool has_spin_atomic_props() const
Definition: formula.hh:471
bool is_constant() const
Definition: formula.hh:297
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:375
void destroy() const
Dereference an fnode.
Definition: formula.hh:128
static const fnode * bunop(op o, const fnode *f, uint8_t min, uint8_t max=unbounded())
Non-Length-Matching Rational-And.
static const fnode * ff()
Definition: formula.hh:261
static const fnode * one_star()
Definition: formula.hh:311
bool is_syntactic_safety() const
Definition: formula.hh:423
marked version of the Negated PSL Clusure
bool is_sugar_free_boolean() const
Definition: formula.hh:363
bool is_ltl_formula() const
Definition: formula.hh:387
bool is_in_nenoform() const
Definition: formula.hh:369
bool is_ff() const
Definition: formula.hh:267
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:200
static constexpr uint8_t unbounded()
Definition: formula.hh:138
unsigned size() const
Definition: formula.hh:229
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:114
bool has_lbt_atomic_props() const
Definition: formula.hh:465
bool is_sugar_free_ltl() const
Definition: formula.hh:381
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:399
op
Operator types.
Definition: formula.hh:62
bool is_tt() const
Definition: formula.hh:279
const fnode *const * end() const
Definition: formula.hh:247
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:156
bool is_eventual() const
Definition: formula.hh:411
unsigned min() const
Definition: formula.hh:213
bool is_universal() const
Definition: formula.hh:417
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:459
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:303