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 121 class SPOT_API fnode final
138 if (SPOT_UNLIKELY(!refs_))
150 if (SPOT_LIKELY(refs_))
152 else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
164 static const fnode*
ap(
const std::string& name);
166 static const fnode* unop(
op o,
const fnode* f);
168 static const fnode* binop(
op o,
const fnode* f,
const fnode* g);
170 static const fnode* multop(
op o, std::vector<const fnode*> l);
172 static const fnode* bunop(
op o,
const fnode* f,
173 uint8_t min, uint8_t max = unbounded());
176 static const fnode* nested_unop_range(
op uo,
op bo,
unsigned min,
177 unsigned max,
const fnode* f);
186 std::string kindstr()
const;
197 return op_ == o1 || op_ == o2;
201 bool is(std::initializer_list<op> l)
const 203 const fnode* n =
this;
218 if (SPOT_UNLIKELY(size_ != 1))
219 report_get_child_of_expecting_single_child_node();
240 report_min_invalid_arg();
248 report_max_invalid_arg();
277 const fnode*
const*
end()
const 279 return children + size();
283 const fnode*
nth(
unsigned i)
const 285 if (SPOT_UNLIKELY(i >= size()))
286 report_non_existing_child();
291 static const fnode*
ff()
303 static const fnode*
tt()
337 return min_ == 0 && max_ == unbounded();
349 const std::string& ap_name()
const;
352 std::ostream& dump(std::ostream& os)
const;
355 const fnode* all_but(
unsigned i)
const;
362 while (pos < s && children[pos]->is_boolean())
368 const fnode* boolean_operands(
unsigned* width =
nullptr)
const;
380 static bool instances_check();
395 return is_.sugar_free_boolean;
401 return is_.in_nenoform;
407 return is_.syntactic_si;
413 return is_.sugar_free_ltl;
419 return is_.ltl_formula;
425 return is_.psl_formula;
431 return is_.sere_formula;
449 return is_.universal;
455 return is_.syntactic_safety;
461 return is_.syntactic_guarantee;
467 return is_.syntactic_obligation;
473 return is_.syntactic_recurrence;
479 return is_.syntactic_persistence;
485 return !is_.not_marked;
491 return is_.accepting_eword;
497 return is_.lbt_atomic_props;
503 return is_.spin_atomic_props;
507 static size_t bump_next_id();
508 void setup_props(
op o);
509 void destroy_aux()
const;
511 [[noreturn]]
static void report_non_existing_child();
512 [[noreturn]]
static void report_too_many_children();
513 [[noreturn]]
static void 514 report_get_child_of_expecting_single_child_node();
515 [[noreturn]]
static void report_min_invalid_arg();
516 [[noreturn]]
static void report_max_invalid_arg();
518 static const fnode* unique(fnode*);
523 fnode(
const fnode&) =
delete;
524 fnode& operator=(
const fnode&) =
delete;
529 fnode(
op o, iter begin, iter end)
546 size_t s = std::distance(begin, end);
547 if (SPOT_UNLIKELY(s > (
size_t) UINT16_MAX))
548 report_too_many_children();
551 for (
auto i = begin; i != end; ++i)
556 fnode(
op o, std::initializer_list<const fnode*> l)
557 : fnode(o, l.begin(), l.end())
561 fnode(
op o,
const fnode* f, uint8_t min, uint8_t max)
562 : op_(o), min_(min), max_(max), saturated_(0), size_(1)
568 static const fnode* ff_;
569 static const fnode* tt_;
570 static const fnode* ew_;
571 static const fnode* one_star_;
576 mutable uint8_t saturated_;
578 mutable uint16_t refs_ = 0;
580 static size_t next_id_;
598 bool sugar_free_boolean:1;
601 bool sugar_free_ltl:1;
608 bool syntactic_safety:1;
609 bool syntactic_guarantee:1;
610 bool syntactic_obligation:1;
611 bool syntactic_recurrence:1;
612 bool syntactic_persistence:1;
614 bool accepting_eword:1;
615 bool lbt_atomic_props:1;
616 bool spin_atomic_props:1;
625 const fnode* children[1];
635 operator()(
const fnode* left,
const fnode* right)
const 655 auto get_literal = [](
const fnode* f) ->
const fnode*
664 const fnode* litl = get_literal(left);
665 const fnode* litr = get_literal(right);
671 int cmp = atomic_prop_cmp(litl, litr);
678 size_t l = left->
id();
679 size_t r = right->
id();
692 std::ostringstream old;
694 std::ostringstream ord;
696 return old.str() < ord.str();
779 std::swap(f.ptr_, ptr_);
783 bool operator<(
const formula& other)
const noexcept
785 if (SPOT_UNLIKELY(!other.ptr_))
787 if (SPOT_UNLIKELY(!ptr_))
789 if (
id() < other.
id())
791 if (
id() > other.
id())
797 return ptr_ < other.ptr_;
800 bool operator<=(
const formula& other)
const noexcept
802 return *
this == other || *
this < other;
805 bool operator>(
const formula& other)
const noexcept
807 return !(*
this <= other);
810 bool operator>=(
const formula& other)
const noexcept
812 return !(*
this < other);
815 bool operator==(
const formula& other)
const noexcept
817 return other.ptr_ == ptr_;
820 bool operator==(std::nullptr_t)
const noexcept
822 return ptr_ ==
nullptr;
825 bool operator!=(
const formula& other)
const noexcept
827 return other.ptr_ != ptr_;
830 bool operator!=(std::nullptr_t)
const noexcept
832 return ptr_ !=
nullptr;
835 operator bool()
const 837 return ptr_ !=
nullptr;
864 report_ap_invalid_arg();
886 #define SPOT_DEF_UNOP(Name) \ 887 static formula Name(const formula& f) \ 889 return unop(op::Name, f); \ 892 #define SPOT_DEF_UNOP(Name) \ 893 static formula Name(const formula& f) \ 895 return unop(op::Name, f); \ 897 static formula Name(formula&& f) \ 899 return unop(op::Name, std::move(f)); \ 917 return nested_unop_range(
op::X,
op::Or , level, level, f);
920 #if SPOT_WANT_STRONG_X 921 SPOT_DEF_UNOP(strong_X);
931 return nested_unop_range(op::strong_X,
op::Or ,
949 return nested_unop_range(
op::X,
op::Or, min_level, max_level, f);
960 return nested_unop_range(
op::X,
op::And, min_level, max_level, f);
1019 #define SPOT_DEF_BINOP(Name) \ 1020 static formula Name(const formula& f, const formula& g) \ 1022 return binop(op::Name, f, g); \ 1025 #define SPOT_DEF_BINOP(Name) \ 1026 static formula Name(const formula& f, const formula& g) \ 1028 return binop(op::Name, f, g); \ 1030 static formula Name(const formula& f, formula&& g) \ 1032 return binop(op::Name, f, std::move(g)); \ 1034 static formula Name(formula&& f, const formula& g) \ 1036 return binop(op::Name, std::move(f), g); \ 1038 static formula Name(formula&& f, formula&& g) \ 1040 return binop(op::Name, std::move(f), std::move(g)); \ 1043 SPOT_DEF_BINOP(
Xor);
1092 #undef SPOT_DEF_BINOP 1101 std::vector<const fnode*> tmp;
1102 tmp.reserve(l.size());
1105 tmp.emplace_back(f.ptr_->
clone());
1112 std::vector<const fnode*> tmp;
1113 tmp.reserve(l.size());
1123 #define SPOT_DEF_MULTOP(Name) \ 1124 static formula Name(const std::vector<formula>& l) \ 1126 return multop(op::Name, l); \ 1129 #define SPOT_DEF_MULTOP(Name) \ 1130 static formula Name(const std::vector<formula>& l) \ 1132 return multop(op::Name, l); \ 1135 static formula Name(std::vector<formula>&& l) \ 1137 return multop(op::Name, std::move(l)); \ 1140 SPOT_DEF_MULTOP(
Or);
1174 #undef SPOT_DEF_MULTOP 1182 uint8_t max = unbounded())
1190 uint8_t max = unbounded())
1198 #define SPOT_DEF_BUNOP(Name) \ 1199 static formula Name(const formula& f, \ 1201 uint8_t max = unbounded()) \ 1203 return bunop(op::Name, f, min, max); \ 1206 #define SPOT_DEF_BUNOP(Name) \ 1207 static formula Name(const formula& f, \ 1209 uint8_t max = unbounded()) \ 1211 return bunop(op::Name, f, min, max); \ 1213 static formula Name(formula&& f, \ 1215 uint8_t max = unbounded()) \ 1217 return bunop(op::Name, std::move(f), min, max); \ 1220 SPOT_DEF_BUNOP(
Star);
1232 #undef SPOT_DEF_BUNOP 1257 static formula sugar_goto(
const formula& b, uint8_t min, uint8_t max);
1264 static formula sugar_equal(
const formula& b, uint8_t min, uint8_t max);
1288 unsigned min,
unsigned max);
1290 unsigned min,
unsigned max);
1294 const fnode* to_node_()
1314 return ptr_->kind();
1320 return ptr_->kindstr();
1330 bool is(
op o1,
op o2)
const 1333 return ptr_->is(o1, o2);
1337 bool is(std::initializer_list<op> l)
const 1355 formula get_child_of(std::initializer_list<op> l)
const 1389 return ptr_->size();
1398 return ptr_->is_leaf();
1415 class SPOT_API formula_child_iterator final
1418 const fnode*
const* ptr_;
1420 formula_child_iterator()
1425 formula_child_iterator(
const fnode*
const* f)
1430 bool operator==(formula_child_iterator o)
1432 return ptr_ == o.ptr_;
1435 bool operator!=(formula_child_iterator o)
1437 return ptr_ != o.ptr_;
1442 return formula((*ptr_)->clone());
1445 formula_child_iterator operator++()
1451 formula_child_iterator operator++(
int)
1462 return ptr_->begin();
1466 formula_child_iterator
end()
const 1474 return formula(ptr_->nth(i)->clone());
1487 return ptr_->is_ff();
1499 return ptr_->is_tt();
1511 return ptr_->is_eword();
1517 return ptr_->is_constant();
1526 return ptr_->is_Kleene_star();
1543 (is(
op::Not) && is_boolean() && is_in_nenoform()));
1551 return ptr_->ap_name();
1558 std::ostream&
dump(std::ostream& os)
const 1560 return ptr_->dump(os);
1570 return formula(ptr_->all_but(i));
1584 return ptr_->boolean_count();
1602 return formula(ptr_->boolean_operands(width));
1605 #define SPOT_DEF_PROP(Name) \ 1608 return ptr_->Name(); \ 1615 SPOT_DEF_PROP(is_boolean);
1617 SPOT_DEF_PROP(is_sugar_free_boolean);
1622 SPOT_DEF_PROP(is_in_nenoform);
1624 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1626 SPOT_DEF_PROP(is_sugar_free_ltl);
1628 SPOT_DEF_PROP(is_ltl_formula);
1630 SPOT_DEF_PROP(is_psl_formula);
1632 SPOT_DEF_PROP(is_sere_formula);
1635 SPOT_DEF_PROP(is_finite);
1643 SPOT_DEF_PROP(is_eventual);
1653 SPOT_DEF_PROP(is_syntactic_safety);
1655 SPOT_DEF_PROP(is_syntactic_guarantee);
1657 SPOT_DEF_PROP(is_syntactic_obligation);
1659 SPOT_DEF_PROP(is_syntactic_recurrence);
1661 SPOT_DEF_PROP(is_syntactic_persistence);
1664 SPOT_DEF_PROP(is_marked);
1666 SPOT_DEF_PROP(accepts_eword);
1672 SPOT_DEF_PROP(has_lbt_atomic_props);
1681 SPOT_DEF_PROP(has_spin_atomic_props);
1682 #undef SPOT_DEF_PROP 1687 template<
typename Trans,
typename... Args>
1690 switch (
op o = kind())
1699 #if SPOT_HAS_STRONG_X 1708 return unop(o, trans((*
this)[0], std::forward<Args>(args)...));
1720 formula tmp = trans((*
this)[0], std::forward<Args>(args)...);
1721 return binop(o, tmp,
1722 trans((*
this)[1], std::forward<Args>(args)...));
1732 std::vector<formula> tmp;
1733 tmp.reserve(size());
1735 tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1736 return multop(o, std::move(tmp));
1740 return bunop(o, trans((*
this)[0], std::forward<Args>(args)...),
1754 template<
typename Func,
typename... Args>
1757 if (func(*
this, std::forward<Args>(args)...))
1760 f.
traverse(func, std::forward<Args>(args)...);
1765 [[noreturn]]
static void report_ap_invalid_arg();
1772 bool abbreviated =
false);
1780 std::ostream& operator<<(std::ostream& os,
const formula& f);
const fnode *const * begin() const
Definition: formula.hh:271
Definition: automata.hh:26
bool is_boolean() const
Definition: formula.hh:387
static const fnode * eword()
Definition: formula.hh:315
static const fnode * ap(const std::string &name)
std::ostream & dump(std::ostream &os) const
unsigned max() const
Definition: formula.hh:245
size_t id() const
Definition: formula.hh:265
bool is(op o) const
Definition: formula.hh:189
bool is_psl_formula() const
Definition: formula.hh:423
static const fnode * unop(op o, const fnode *f)
bool is_leaf() const
Definition: formula.hh:259
bool is_finite() const
Definition: formula.hh:435
bool is_eword() const
Definition: formula.hh:321
unsigned boolean_count() const
Definition: formula.hh:358
const fnode * get_child_of(op o) const
Definition: formula.hh:214
Definition: bitset.hh:405
bool is_syntactic_guarantee() const
Definition: formula.hh:459
static const fnode * tt()
Definition: formula.hh:303
bool is_syntactic_persistence() const
Definition: formula.hh:477
const fnode * nth(unsigned i) const
Definition: formula.hh:283
bool is_marked() const
Definition: formula.hh:483
bool is_syntactic_recurrence() const
Definition: formula.hh:471
bool is(std::initializer_list< op > l) const
Definition: formula.hh:201
bool is_syntactic_obligation() const
Definition: formula.hh:465
bool is(op o1, op o2) const
Definition: formula.hh:195
bool has_spin_atomic_props() const
Definition: formula.hh:501
bool is_constant() const
Definition: formula.hh:327
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:405
void destroy() const
Dereference an fnode.
Definition: formula.hh:148
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:291
static const fnode * one_star()
Definition: formula.hh:341
bool is_syntactic_safety() const
Definition: formula.hh:453
marked version of the Negated PSL Closure
bool is_sugar_free_boolean() const
Definition: formula.hh:393
bool is_ltl_formula() const
Definition: formula.hh:417
bool is_in_nenoform() const
Definition: formula.hh:399
bool is_ff() const
Definition: formula.hh:297
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:224
static constexpr uint8_t unbounded()
Definition: formula.hh:158
unsigned size() const
Definition: formula.hh:253
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:134
bool has_lbt_atomic_props() const
Definition: formula.hh:495
bool is_sugar_free_ltl() const
Definition: formula.hh:411
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:429
op
Operator types.
Definition: formula.hh:78
bool is_tt() const
Definition: formula.hh:309
const fnode *const * end() const
Definition: formula.hh:277
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:180
static const fnode * nested_unop_range(op uo, op bo, unsigned min, unsigned max, const fnode *f)
bool is_eventual() const
Definition: formula.hh:441
unsigned min() const
Definition: formula.hh:237
bool is_universal() const
Definition: formula.hh:447
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:489
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:333