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);
150 static const fnode* multop(
op o, std::vector<const fnode*> l);
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;
246 return children + size();
253 throw std::runtime_error(
"access to non-existing child");
304 return min_ == 0 && max_ == unbounded();
316 const std::string& ap_name()
const;
319 std::ostream& dump(std::ostream& os)
const;
322 const fnode* all_but(
unsigned i)
const;
329 while (pos < s && children[pos]->is_boolean())
335 const fnode* boolean_operands(
unsigned* width =
nullptr)
const;
347 static bool instances_check();
362 return is_.sugar_free_boolean;
368 return is_.in_nenoform;
374 return is_.syntactic_si;
380 return is_.sugar_free_ltl;
386 return is_.ltl_formula;
392 return is_.psl_formula;
398 return is_.sere_formula;
416 return is_.universal;
422 return is_.syntactic_safety;
428 return is_.syntactic_guarantee;
434 return is_.syntactic_obligation;
440 return is_.syntactic_recurrence;
446 return is_.syntactic_persistence;
452 return !is_.not_marked;
458 return is_.accepting_eword;
464 return is_.lbt_atomic_props;
470 return is_.spin_atomic_props;
474 void setup_props(
op o);
475 void destroy_aux()
const;
488 fnode(
op o, iter begin, iter end)
490 size_t s = std::distance(begin, end);
491 if (s > (
size_t) UINT16_MAX)
492 throw std::runtime_error(
"too many children for formula");
495 for (
auto i = begin; i != end; ++i)
500 fnode(
op o, std::initializer_list<const fnode*> l)
501 : fnode(o, l.begin(), l.end())
505 fnode(
op o,
const fnode* f, uint8_t min, uint8_t max)
514 static const fnode* ff_;
515 static const fnode* tt_;
516 static const fnode* ew_;
517 static const fnode* one_star_;
522 mutable uint8_t saturated_ = 0;
524 mutable uint16_t refs_ = 0;
526 static size_t next_id_;
544 bool sugar_free_boolean:1;
547 bool sugar_free_ltl:1;
554 bool syntactic_safety:1;
555 bool syntactic_guarantee:1;
556 bool syntactic_obligation:1;
557 bool syntactic_recurrence:1;
558 bool syntactic_persistence:1;
560 bool accepting_eword:1;
561 bool lbt_atomic_props:1;
562 bool spin_atomic_props:1;
571 const fnode* children[1];
576 int atomic_prop_cmp(
const fnode* f,
const fnode* g);
581 operator()(
const fnode* left,
const fnode* right)
const
601 auto get_literal = [](
const fnode* f) ->
const fnode*
610 const fnode* litl = get_literal(left);
611 const fnode* litr = get_literal(right);
617 int cmp = atomic_prop_cmp(litl, litr);
624 size_t l = left->
id();
625 size_t r = right->
id();
638 std::ostringstream old;
640 std::ostringstream ord;
642 return old.str() < ord.str();
723 const formula& operator=(formula&& f) noexcept
725 std::swap(f.ptr_, ptr_);
729 bool operator<(
const formula& other)
const noexcept
731 if (SPOT_UNLIKELY(!other.ptr_))
733 if (SPOT_UNLIKELY(!ptr_))
735 if (
id() < other.id())
737 if (
id() > other.id())
743 return ptr_ < other.ptr_;
746 bool operator<=(
const formula& other)
const noexcept
748 return *
this == other || *
this < other;
751 bool operator>(
const formula& other)
const noexcept
753 return !(*
this <= other);
756 bool operator>=(
const formula& other)
const noexcept
758 return !(*
this < other);
761 bool operator==(
const formula& other)
const noexcept
763 return other.ptr_ == ptr_;
766 bool operator==(std::nullptr_t) const noexcept
768 return ptr_ ==
nullptr;
771 bool operator!=(
const formula& other)
const noexcept
773 return other.ptr_ != ptr_;
776 bool operator!=(std::nullptr_t) const noexcept
778 return ptr_ !=
nullptr;
781 operator bool()
const
783 return ptr_ !=
nullptr;
812 throw std::invalid_argument(
"atomic propositions cannot be "
813 "constructed from arbitrary formulas");
834 #define SPOT_DEF_UNOP(Name) \
835 static formula Name(const formula& f) \
837 return unop(op::Name, f); \
840 #define SPOT_DEF_UNOP(Name) \
841 static formula Name(const formula& f) \
843 return unop(op::Name, f); \
845 static formula Name(formula&& f) \
847 return unop(op::Name, std::move(f)); \
916 #define SPOT_DEF_BINOP(Name) \
917 static formula Name(const formula& f, const formula& g) \
919 return binop(op::Name, f, g); \
922 #define SPOT_DEF_BINOP(Name) \
923 static formula Name(const formula& f, const formula& g) \
925 return binop(op::Name, f, g); \
927 static formula Name(const formula& f, formula&& g) \
929 return binop(op::Name, f, std::move(g)); \
931 static formula Name(formula&& f, const formula& g) \
933 return binop(op::Name, std::move(f), g); \
935 static formula Name(formula&& f, formula&& g) \
937 return binop(op::Name, std::move(f), std::move(g)); \
989 #undef SPOT_DEF_BINOP
998 std::vector<const fnode*> tmp;
999 tmp.reserve(l.size());
1002 tmp.push_back(f.ptr_->
clone());
1009 std::vector<const fnode*> tmp;
1010 tmp.reserve(l.size());
1020 #define SPOT_DEF_MULTOP(Name) \
1021 static formula Name(const std::vector<formula>& l) \
1023 return multop(op::Name, l); \
1026 #define SPOT_DEF_MULTOP(Name) \
1027 static formula Name(const std::vector<formula>& l) \
1029 return multop(op::Name, l); \
1032 static formula Name(std::vector<formula>&& l) \
1034 return multop(op::Name, std::move(l)); \
1037 SPOT_DEF_MULTOP(
Or);
1071 #undef SPOT_DEF_MULTOP
1079 uint8_t max = unbounded())
1087 uint8_t max = unbounded())
1095 #define SPOT_DEF_BUNOP(Name) \
1096 static formula Name(const formula& f, \
1098 uint8_t max = unbounded()) \
1100 return bunop(op::Name, f, min, max); \
1103 #define SPOT_DEF_BUNOP(Name) \
1104 static formula Name(const formula& f, \
1106 uint8_t max = unbounded()) \
1108 return bunop(op::Name, f, min, max); \
1110 static formula Name(formula&& f, \
1112 uint8_t max = unbounded()) \
1114 return bunop(op::Name, std::move(f), min, max); \
1117 SPOT_DEF_BUNOP(
Star);
1141 SPOT_DEF_BUNOP(
FStar);
1144 #undef SPOT_DEF_BUNOP
1151 static formula sugar_goto(
const formula& b, uint8_t min, uint8_t max);
1158 static formula sugar_equal(
const formula& b, uint8_t min, uint8_t max);
1161 const fnode* to_node_()
1181 return ptr_->kind();
1187 return ptr_->kindstr();
1197 bool is(
op o1,
op o2)
const
1200 return ptr_->is(o1, o2);
1204 bool is(std::initializer_list<op> l)
const
1222 formula get_child_of(std::initializer_list<op> l)
const
1256 return ptr_->size();
1273 class SPOT_API formula_child_iterator final
1276 const fnode*
const* ptr_;
1278 formula_child_iterator()
1283 formula_child_iterator(
const fnode*
const* f)
1288 bool operator==(formula_child_iterator o)
1290 return ptr_ == o.ptr_;
1293 bool operator!=(formula_child_iterator o)
1295 return ptr_ != o.ptr_;
1300 return formula((*ptr_)->clone());
1303 formula_child_iterator operator++()
1309 formula_child_iterator operator++(
int)
1320 return ptr_->begin();
1332 return formula(ptr_->nth(i)->clone());
1345 return ptr_->is_ff();
1357 return ptr_->is_tt();
1369 return ptr_->is_eword();
1375 return ptr_->is_constant();
1384 return ptr_->is_Kleene_star();
1401 (is(
op::Not) && is_boolean() && is_in_nenoform()));
1409 return ptr_->ap_name();
1416 std::ostream&
dump(std::ostream& os)
const
1418 return ptr_->dump(os);
1428 return formula(ptr_->all_but(i));
1442 return ptr_->boolean_count();
1460 return formula(ptr_->boolean_operands(width));
1463 #define SPOT_DEF_PROP(Name) \
1466 return ptr_->Name(); \
1473 SPOT_DEF_PROP(is_boolean);
1475 SPOT_DEF_PROP(is_sugar_free_boolean);
1480 SPOT_DEF_PROP(is_in_nenoform);
1482 SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1484 SPOT_DEF_PROP(is_sugar_free_ltl);
1486 SPOT_DEF_PROP(is_ltl_formula);
1488 SPOT_DEF_PROP(is_psl_formula);
1490 SPOT_DEF_PROP(is_sere_formula);
1493 SPOT_DEF_PROP(is_finite);
1511 SPOT_DEF_PROP(is_eventual);
1532 SPOT_DEF_PROP(is_universal);
1537 SPOT_DEF_PROP(is_syntactic_safety);
1539 SPOT_DEF_PROP(is_syntactic_guarantee);
1541 SPOT_DEF_PROP(is_syntactic_obligation);
1543 SPOT_DEF_PROP(is_syntactic_recurrence);
1545 SPOT_DEF_PROP(is_syntactic_persistence);
1548 SPOT_DEF_PROP(is_marked);
1550 SPOT_DEF_PROP(accepts_eword);
1556 SPOT_DEF_PROP(has_lbt_atomic_props);
1565 SPOT_DEF_PROP(has_spin_atomic_props);
1566 #undef SPOT_DEF_PROP
1569 template<
typename Trans>
1572 switch (
op o = kind())
1586 return unop(o, trans((*
this)[0]));
1598 formula tmp = trans((*
this)[0]);
1599 return binop(o, tmp, trans((*
this)[1]));
1609 std::vector<formula> tmp;
1610 tmp.reserve(size());
1612 tmp.push_back(trans(f));
1613 return multop(o, std::move(tmp));
1617 return bunop(o, trans((*
this)[0]), min(), max());
1627 template<
typename Func>
1639 std::ostream& print_formula_props(std::ostream& out,
const formula& f,
1640 bool abbreviated =
false);
1644 std::list<std::string> list_formula_props(
const formula& f);
1648 std::ostream& operator<<(std::ostream& os,
const formula& f);
bool is_tt() const
Definition: formula.hh:276
bool is(op o) const
Definition: formula.hh:165
const fnode *const * begin() const
Definition: formula.hh:238
static const fnode * eword()
Definition: formula.hh:282
static const fnode * ap(const std::string &name)
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:372
static const fnode * unop(op o, const fnode *f)
bool is_syntactic_safety() const
Definition: formula.hh:420
bool is_eventual() const
Definition: formula.hh:408
bool is_ltl_formula() const
Definition: formula.hh:384
Definition: formula.hh:1652
bool is_psl_formula() const
Definition: formula.hh:390
bool is_sere_formula() const
Definition: formula.hh:396
static const fnode * tt()
Definition: formula.hh:270
bool is_marked() const
Definition: formula.hh:450
bool is(op o1, op o2) const
Definition: formula.hh:171
bool is_syntactic_recurrence() const
Definition: formula.hh:438
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:114
unsigned size() const
Definition: formula.hh:226
bool is_Kleene_star() const
Definition: formula.hh:300
bool is_in_nenoform() const
Definition: formula.hh:366
unsigned boolean_count() const
Definition: formula.hh:325
bool is_sugar_free_boolean() const
Definition: formula.hh:360
unsigned max() const
Definition: formula.hh:219
unsigned min() const
Definition: formula.hh:212
static const fnode * multop(op o, std::vector< const fnode * > l)
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:258
static const fnode * one_star()
Definition: formula.hh:308
marked version of the Negated PSL Clusure
bool is_constant() const
Definition: formula.hh:294
const fnode * get_child_of(op o) const
Definition: formula.hh:190
const fnode *const * end() const
Definition: formula.hh:244
bool has_spin_atomic_props() const
Definition: formula.hh:468
bool accepts_eword() const
Definition: formula.hh:456
const fnode * nth(unsigned i) const
Definition: formula.hh:250
void destroy() const
Dereference an fnode.
Definition: formula.hh:128
op kind() const
Definition: formula.hh:156
static constexpr uint8_t unbounded()
Definition: formula.hh:138
bool is_syntactic_guarantee() const
Definition: formula.hh:426
std::ostream & dump(std::ostream &os) const
static const fnode * binop(op o, const fnode *f, const fnode *g)
op
Operator types.
Definition: formula.hh:62
bool is_syntactic_persistence() const
Definition: formula.hh:444
bool is_ff() const
Definition: formula.hh:264
bool is_universal() const
Definition: formula.hh:414
bool is_boolean() const
Definition: formula.hh:354
bool is_syntactic_obligation() const
Definition: formula.hh:432
bool is_sugar_free_ltl() const
Definition: formula.hh:378
Actual storage for formula nodes.
Definition: formula.hh:107
bool is(std::initializer_list< op > l) const
Definition: formula.hh:177
bool is_finite() const
Definition: formula.hh:402
strong release (dual of weak until)
bool has_lbt_atomic_props() const
Definition: formula.hh:462
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:199
size_t id() const
Definition: formula.hh:232
bool is_eword() const
Definition: formula.hh:288