46 #include <spot/misc/common.hh> 49 #include <initializer_list> 58 #include <initializer_list> 65 enum class op: uint8_t
104 class SPOT_API fnode final
121 if (SPOT_UNLIKELY(!refs_))
133 if (SPOT_LIKELY(refs_))
135 else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
147 static const fnode*
ap(
const std::string& name);
149 static const fnode* unop(
op o,
const fnode* f);
151 static const fnode* binop(
op o,
const fnode* f,
const fnode* g);
153 static const fnode* multop(
op o, std::vector<const fnode*> l);
155 static const fnode* bunop(
op o,
const fnode* f,
156 uint8_t min, uint8_t max = unbounded());
165 std::string kindstr()
const;
176 return op_ == o1 || op_ == o2;
180 bool is(std::initializer_list<op> l)
const 182 const fnode* n =
this;
197 if (SPOT_UNLIKELY(size_ != 1))
198 report_get_child_of_expecting_single_child_node();
219 report_min_invalid_arg();
227 report_max_invalid_arg();
256 const fnode*
const*
end()
const 258 return children + size();
262 const fnode*
nth(
unsigned i)
const 264 if (SPOT_UNLIKELY(i >= size()))
265 report_non_existing_child();
270 static const fnode*
ff()
282 static const fnode*
tt()
316 return min_ == 0 && max_ == unbounded();
328 const std::string& ap_name()
const;
331 std::ostream& dump(std::ostream& os)
const;
334 const fnode* all_but(
unsigned i)
const;
341 while (pos < s && children[pos]->is_boolean())
347 const fnode* boolean_operands(
unsigned* width =
nullptr)
const;
359 static bool instances_check();
374 return is_.sugar_free_boolean;
380 return is_.in_nenoform;
386 return is_.syntactic_si;
392 return is_.sugar_free_ltl;
398 return is_.ltl_formula;
404 return is_.psl_formula;
410 return is_.sere_formula;
428 return is_.universal;
434 return is_.syntactic_safety;
440 return is_.syntactic_guarantee;
446 return is_.syntactic_obligation;
452 return is_.syntactic_recurrence;
458 return is_.syntactic_persistence;
464 return !is_.not_marked;
470 return is_.accepting_eword;
476 return is_.lbt_atomic_props;
482 return is_.spin_atomic_props;
486 void setup_props(
op o);
487 void destroy_aux()
const;
489 [[noreturn]]
static void report_non_existing_child();
490 [[noreturn]]
static void report_too_many_children();
491 [[noreturn]]
static void 492 report_get_child_of_expecting_single_child_node();
493 [[noreturn]]
static void report_min_invalid_arg();
494 [[noreturn]]
static void report_max_invalid_arg();
496 static const fnode* unique(fnode*);
501 fnode(
const fnode&) =
delete;
502 fnode& operator=(
const fnode&) =
delete;
507 fnode(
op o, iter begin, iter end)
524 size_t s = std::distance(begin, end);
525 if (SPOT_UNLIKELY(s > (
size_t) UINT16_MAX))
526 report_too_many_children();
529 for (
auto i = begin; i != end; ++i)
534 fnode(
op o, std::initializer_list<const fnode*> l)
535 : fnode(o, l.begin(), l.end())
539 fnode(
op o,
const fnode* f, uint8_t min, uint8_t max)
540 : op_(o), min_(min), max_(max), saturated_(0), size_(1)
546 static const fnode* ff_;
547 static const fnode* tt_;
548 static const fnode* ew_;
549 static const fnode* one_star_;
554 mutable uint8_t saturated_;
556 mutable uint16_t refs_ = 0;
558 static size_t next_id_;
576 bool sugar_free_boolean:1;
579 bool sugar_free_ltl:1;
586 bool syntactic_safety:1;
587 bool syntactic_guarantee:1;
588 bool syntactic_obligation:1;
589 bool syntactic_recurrence:1;
590 bool syntactic_persistence:1;
592 bool accepting_eword:1;
593 bool lbt_atomic_props:1;
594 bool spin_atomic_props:1;
603 const fnode* children[1];
613 operator()(
const fnode* left,
const fnode* right)
const 633 auto get_literal = [](
const fnode* f) ->
const fnode*
642 const fnode* litl = get_literal(left);
643 const fnode* litr = get_literal(right);
649 int cmp = atomic_prop_cmp(litl, litr);
656 size_t l = left->
id();
657 size_t r = right->
id();
670 std::ostringstream old;
672 std::ostringstream ord;
674 return old.str() < ord.str();
757 std::swap(f.ptr_, ptr_);
761 bool operator<(
const formula& other)
const noexcept
763 if (SPOT_UNLIKELY(!other.ptr_))
765 if (SPOT_UNLIKELY(!ptr_))
767 if (
id() < other.
id())
769 if (
id() > other.
id())
775 return ptr_ < other.ptr_;
778 bool operator<=(
const formula& other)
const noexcept
780 return *
this == other || *
this < other;
783 bool operator>(
const formula& other)
const noexcept
785 return !(*
this <= other);
788 bool operator>=(
const formula& other)
const noexcept
790 return !(*
this < other);
793 bool operator==(
const formula& other)
const noexcept
795 return other.ptr_ == ptr_;
798 bool operator==(std::nullptr_t)
const noexcept
800 return ptr_ ==
nullptr;
803 bool operator!=(
const formula& other)
const noexcept
805 return other.ptr_ != ptr_;
808 bool operator!=(std::nullptr_t)
const noexcept
810 return ptr_ !=
nullptr;
813 operator bool()
const 815 return ptr_ !=
nullptr;
842 report_ap_invalid_arg();
864 #define SPOT_DEF_UNOP(Name) \ 865 static formula Name(const formula& f) \ 867 return unop(op::Name, f); \ 870 #define SPOT_DEF_UNOP(Name) \ 871 static formula Name(const formula& f) \ 873 return unop(op::Name, f); \ 875 static formula Name(formula&& f) \ 877 return unop(op::Name, std::move(f)); \ 946 #define SPOT_DEF_BINOP(Name) \ 947 static formula Name(const formula& f, const formula& g) \ 949 return binop(op::Name, f, g); \ 952 #define SPOT_DEF_BINOP(Name) \ 953 static formula Name(const formula& f, const formula& g) \ 955 return binop(op::Name, f, g); \ 957 static formula Name(const formula& f, formula&& g) \ 959 return binop(op::Name, f, std::move(g)); \ 961 static formula Name(formula&& f, const formula& g) \ 963 return binop(op::Name, std::move(f), g); \ 965 static formula Name(formula&& f, formula&& g) \ 967 return binop(op::Name, std::move(f), std::move(g)); \ 1019 #undef SPOT_DEF_BINOP 1028 std::vector<const fnode*> tmp;
1029 tmp.reserve(l.size());
1032 tmp.emplace_back(f.ptr_->
clone());
1039 std::vector<const fnode*> tmp;
1040 tmp.reserve(l.size());
1050 #define SPOT_DEF_MULTOP(Name) \ 1051 static formula Name(const std::vector<formula>& l) \ 1053 return multop(op::Name, l); \ 1056 #define SPOT_DEF_MULTOP(Name) \ 1057 static formula Name(const std::vector<formula>& l) \ 1059 return multop(op::Name, l); \ 1062 static formula Name(std::vector<formula>&& l) \ 1064 return multop(op::Name, std::move(l)); \ 1067 SPOT_DEF_MULTOP(
Or);
1101 #undef SPOT_DEF_MULTOP 1109 uint8_t max = unbounded())
1117 uint8_t max = unbounded())
1125 #define SPOT_DEF_BUNOP(Name) \ 1126 static formula Name(const formula& f, \ 1128 uint8_t max = unbounded()) \ 1130 return bunop(op::Name, f, min, max); \ 1133 #define SPOT_DEF_BUNOP(Name) \ 1134 static formula Name(const formula& f, \ 1136 uint8_t max = unbounded()) \ 1138 return bunop(op::Name, f, min, max); \ 1140 static formula Name(formula&& f, \ 1142 uint8_t max = unbounded()) \ 1144 return bunop(op::Name, std::move(f), min, max); \ 1147 SPOT_DEF_BUNOP(
Star);
1171 SPOT_DEF_BUNOP(
FStar);
1174 #undef SPOT_DEF_BUNOP 1181 static formula sugar_goto(
const formula& b, uint8_t min, uint8_t max);
1188 static formula sugar_equal(
const formula& b, uint8_t min, uint8_t max);
1191 const fnode* to_node_()
1211 return ptr_->kind();
1217 return ptr_->kindstr();
1227 bool is(
op o1,
op o2)
const 1230 return ptr_->is(o1, o2);
1234 bool is(std::initializer_list<op> l)
const 1252 formula get_child_of(std::initializer_list<op> l)
const 1286 return ptr_->size();
1295 return ptr_->is_leaf();
1312 class SPOT_API formula_child_iterator final
1315 const fnode*
const* ptr_;
1317 formula_child_iterator()
1322 formula_child_iterator(
const fnode*
const* f)
1327 bool operator==(formula_child_iterator o)
1329 return ptr_ == o.ptr_;
1332 bool operator!=(formula_child_iterator o)
1334 return ptr_ != o.ptr_;
1339 return formula((*ptr_)->clone());
1342 formula_child_iterator operator++()
1348 formula_child_iterator operator++(
int)
1359 return ptr_->begin();
1363 formula_child_iterator
end()
const 1371 return formula(ptr_->nth(i)->clone());
1384 return ptr_->is_ff();
1396 return ptr_->is_tt();
1408 return ptr_->is_eword();
1414 return ptr_->is_constant();
1423 return ptr_->is_Kleene_star();
1440 (is(
op::Not) && is_boolean() && is_in_nenoform()));
1448 return ptr_->ap_name();
1455 std::ostream&
dump(std::ostream& os)
const 1457 return ptr_->dump(os);
1467 return formula(ptr_->all_but(i));
1481 return ptr_->boolean_count();
1499 return formula(ptr_->boolean_operands(width));
1502 #define SPOT_DEF_PROP(Name) \ 1505 return ptr_->Name(); \ 1512 SPOT_DEF_PROP(is_boolean);
1514 SPOT_DEF_PROP(is_sugar_free_boolean);
1519 SPOT_DEF_PROP(is_in_nenoform);
1521 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1523 SPOT_DEF_PROP(is_sugar_free_ltl);
1525 SPOT_DEF_PROP(is_ltl_formula);
1527 SPOT_DEF_PROP(is_psl_formula);
1529 SPOT_DEF_PROP(is_sere_formula);
1532 SPOT_DEF_PROP(is_finite);
1550 SPOT_DEF_PROP(is_eventual);
1576 SPOT_DEF_PROP(is_syntactic_safety);
1578 SPOT_DEF_PROP(is_syntactic_guarantee);
1580 SPOT_DEF_PROP(is_syntactic_obligation);
1582 SPOT_DEF_PROP(is_syntactic_recurrence);
1584 SPOT_DEF_PROP(is_syntactic_persistence);
1587 SPOT_DEF_PROP(is_marked);
1589 SPOT_DEF_PROP(accepts_eword);
1595 SPOT_DEF_PROP(has_lbt_atomic_props);
1604 SPOT_DEF_PROP(has_spin_atomic_props);
1605 #undef SPOT_DEF_PROP 1610 template<
typename Trans,
typename... Args>
1613 switch (
op o = kind())
1627 return unop(o, trans((*
this)[0], std::forward<Args>(args)...));
1639 formula tmp = trans((*
this)[0], std::forward<Args>(args)...);
1640 return binop(o, tmp,
1641 trans((*
this)[1], std::forward<Args>(args)...));
1651 std::vector<formula> tmp;
1652 tmp.reserve(size());
1654 tmp.emplace_back(trans(f, std::forward<Args>(args)...));
1655 return multop(o, std::move(tmp));
1659 return bunop(o, trans((*
this)[0], std::forward<Args>(args)...),
1673 template<
typename Func,
typename... Args>
1676 if (func(*
this, std::forward<Args>(args)...))
1679 f.
traverse(func, std::forward<Args>(args)...);
1684 [[noreturn]]
static void report_ap_invalid_arg();
1691 bool abbreviated =
false);
1699 std::ostream& operator<<(std::ostream& os,
const formula& f);
const fnode *const * begin() const
Definition: formula.hh:250
Definition: automata.hh:26
bool is_boolean() const
Definition: formula.hh:366
static const fnode * eword()
Definition: formula.hh:294
static const fnode * ap(const std::string &name)
std::ostream & dump(std::ostream &os) const
unsigned max() const
Definition: formula.hh:224
size_t id() const
Definition: formula.hh:244
bool is(op o) const
Definition: formula.hh:168
bool is_psl_formula() const
Definition: formula.hh:402
static const fnode * unop(op o, const fnode *f)
bool is_leaf() const
Definition: formula.hh:238
bool is_finite() const
Definition: formula.hh:414
bool is_eword() const
Definition: formula.hh:300
unsigned boolean_count() const
Definition: formula.hh:337
const fnode * get_child_of(op o) const
Definition: formula.hh:193
Definition: bitset.hh:405
bool is_syntactic_guarantee() const
Definition: formula.hh:438
static const fnode * tt()
Definition: formula.hh:282
bool is_syntactic_persistence() const
Definition: formula.hh:456
const fnode * nth(unsigned i) const
Definition: formula.hh:262
bool is_marked() const
Definition: formula.hh:462
bool is_syntactic_recurrence() const
Definition: formula.hh:450
bool is(std::initializer_list< op > l) const
Definition: formula.hh:180
bool is_syntactic_obligation() const
Definition: formula.hh:444
bool is(op o1, op o2) const
Definition: formula.hh:174
bool has_spin_atomic_props() const
Definition: formula.hh:480
bool is_constant() const
Definition: formula.hh:306
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:384
void destroy() const
Dereference an fnode.
Definition: formula.hh:131
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:270
static const fnode * one_star()
Definition: formula.hh:320
bool is_syntactic_safety() const
Definition: formula.hh:432
marked version of the Negated PSL Closure
bool is_sugar_free_boolean() const
Definition: formula.hh:372
bool is_ltl_formula() const
Definition: formula.hh:396
bool is_in_nenoform() const
Definition: formula.hh:378
bool is_ff() const
Definition: formula.hh:276
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:203
static constexpr uint8_t unbounded()
Definition: formula.hh:141
unsigned size() const
Definition: formula.hh:232
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:117
bool has_lbt_atomic_props() const
Definition: formula.hh:474
bool is_sugar_free_ltl() const
Definition: formula.hh:390
static const fnode * binop(op o, const fnode *f, const fnode *g)
bool is_sere_formula() const
Definition: formula.hh:408
op
Operator types.
Definition: formula.hh:65
bool is_tt() const
Definition: formula.hh:288
const fnode *const * end() const
Definition: formula.hh:256
bool is_universal(const const_twa_graph_ptr &aut)
Return true iff aut is universal.
op kind() const
Definition: formula.hh:159
bool is_eventual() const
Definition: formula.hh:420
unsigned min() const
Definition: formula.hh:216
bool is_universal() const
Definition: formula.hh:426
strong release (dual of weak until)
bool accepts_eword() const
Definition: formula.hh:468
static const fnode * multop(op o, std::vector< const fnode *> l)
bool is_Kleene_star() const
Definition: formula.hh:312