spot  2.3.2
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
formula.hh
Go to the documentation of this file.
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3 // l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
22 #pragma once
23 
30 
33 
36 
39 
42 
43 #include <spot/misc/common.hh>
44 #include <memory>
45 #include <cstdint>
46 #include <initializer_list>
47 #include <cassert>
48 #include <vector>
49 #include <string>
50 #include <iterator>
51 #include <iosfwd>
52 #include <sstream>
53 #include <list>
54 #include <cstddef>
55 #include <initializer_list>
56 #include <limits>
57 
58 namespace spot
59 {
62  enum class op: uint8_t
63  {
64  ff,
65  tt,
66  eword,
67  ap,
68  // unary operators
69  Not,
70  X,
71  F,
72  G,
73  Closure,
74  NegClosure,
76  // binary operators
77  Xor,
78  Implies,
79  Equiv,
80  U,
81  R,
82  W,
83  M,
84  EConcat,
86  UConcat,
87  // n-ary operators
88  Or,
89  OrRat,
90  And,
91  AndRat,
92  AndNLM,
93  Concat,
94  Fusion,
95  // star-like operators
96  Star,
97  FStar,
98  };
99 
100 #ifndef SWIG
101  class SPOT_API fnode final
108  {
109  public:
114  const fnode* clone() const
115  {
116  // Saturate.
117  ++refs_;
118  if (SPOT_UNLIKELY(!refs_))
119  saturated_ = 1;
120  return this;
121  }
122 
128  void destroy() const
129  {
130  if (SPOT_LIKELY(refs_))
131  --refs_;
132  else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
133  // last reference to a node that is not a constant
134  destroy_aux();
135  }
136 
138  static constexpr uint8_t unbounded()
139  {
140  return UINT8_MAX;
141  }
142 
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());
154 
156  op kind() const
157  {
158  return op_;
159  }
160 
162  std::string kindstr() const;
163 
165  bool is(op o) const
166  {
167  return op_ == o;
168  }
169 
171  bool is(op o1, op o2) const
172  {
173  return op_ == o1 || op_ == o2;
174  }
175 
177  bool is(std::initializer_list<op> l) const
178  {
179  const fnode* n = this;
180  for (auto o: l)
181  {
182  if (!n->is(o))
183  return false;
184  n = n->nth(0);
185  }
186  return true;
187  }
188 
190  const fnode* get_child_of(op o) const
191  {
192  if (op_ != o)
193  return nullptr;
194  if (SPOT_UNLIKELY(size_ != 1))
195  throw std::invalid_argument
196  ("get_child_of() expecting single-child node");
197  return nth(0);
198  }
199 
201  const fnode* get_child_of(std::initializer_list<op> l) const
202  {
203  auto c = this;
204  for (auto o: l)
205  {
206  c = c->get_child_of(o);
207  if (c == nullptr)
208  return c;
209  }
210  return c;
211  }
212 
214  unsigned min() const
215  {
216  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
217  throw std::invalid_argument
218  ("min() only works on Star and FStar nodes");
219  return min_;
220  }
221 
223  unsigned max() const
224  {
225  if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
226  throw std::invalid_argument
227  ("max() only works on Star and FStar nodes");
228  return max_;
229  }
230 
232  unsigned size() const
233  {
234  return size_;
235  }
236 
238  size_t id() const
239  {
240  return id_;
241  }
242 
244  const fnode*const* begin() const
245  {
246  return children;
247  }
248 
250  const fnode*const* end() const
251  {
252  return children + size();
253  }
254 
256  const fnode* nth(unsigned i) const
257  {
258  if (i >= size())
259  throw std::runtime_error("access to non-existing child");
260  return children[i];
261  }
262 
264  static const fnode* ff()
265  {
266  return ff_;
267  }
268 
270  bool is_ff() const
271  {
272  return op_ == op::ff;
273  }
274 
276  static const fnode* tt()
277  {
278  return tt_;
279  }
280 
282  bool is_tt() const
283  {
284  return op_ == op::tt;
285  }
286 
288  static const fnode* eword()
289  {
290  return ew_;
291  }
292 
294  bool is_eword() const
295  {
296  return op_ == op::eword;
297  }
298 
300  bool is_constant() const
301  {
302  return op_ == op::ff || op_ == op::tt || op_ == op::eword;
303  }
304 
306  bool is_Kleene_star() const
307  {
308  if (op_ != op::Star)
309  return false;
310  return min_ == 0 && max_ == unbounded();
311  }
312 
314  static const fnode* one_star()
315  {
316  if (!one_star_)
317  one_star_ = bunop(op::Star, tt(), 0);
318  return one_star_;
319  }
320 
322  const std::string& ap_name() const;
323 
325  std::ostream& dump(std::ostream& os) const;
326 
328  const fnode* all_but(unsigned i) const;
329 
331  unsigned boolean_count() const
332  {
333  unsigned pos = 0;
334  unsigned s = size();
335  while (pos < s && children[pos]->is_boolean())
336  ++pos;
337  return pos;
338  }
339 
341  const fnode* boolean_operands(unsigned* width = nullptr) const;
342 
353  static bool instances_check();
354 
356  // Properties //
358 
360  bool is_boolean() const
361  {
362  return is_.boolean;
363  }
364 
367  {
368  return is_.sugar_free_boolean;
369  }
370 
372  bool is_in_nenoform() const
373  {
374  return is_.in_nenoform;
375  }
376 
379  {
380  return is_.syntactic_si;
381  }
382 
384  bool is_sugar_free_ltl() const
385  {
386  return is_.sugar_free_ltl;
387  }
388 
390  bool is_ltl_formula() const
391  {
392  return is_.ltl_formula;
393  }
394 
396  bool is_psl_formula() const
397  {
398  return is_.psl_formula;
399  }
400 
402  bool is_sere_formula() const
403  {
404  return is_.sere_formula;
405  }
406 
408  bool is_finite() const
409  {
410  return is_.finite;
411  }
412 
414  bool is_eventual() const
415  {
416  return is_.eventual;
417  }
418 
420  bool is_universal() const
421  {
422  return is_.universal;
423  }
424 
426  bool is_syntactic_safety() const
427  {
428  return is_.syntactic_safety;
429  }
430 
433  {
434  return is_.syntactic_guarantee;
435  }
436 
439  {
440  return is_.syntactic_obligation;
441  }
442 
445  {
446  return is_.syntactic_recurrence;
447  }
448 
451  {
452  return is_.syntactic_persistence;
453  }
454 
456  bool is_marked() const
457  {
458  return !is_.not_marked;
459  }
460 
462  bool accepts_eword() const
463  {
464  return is_.accepting_eword;
465  }
466 
468  bool has_lbt_atomic_props() const
469  {
470  return is_.lbt_atomic_props;
471  }
472 
475  {
476  return is_.spin_atomic_props;
477  }
478 
479  private:
480  void setup_props(op o);
481  void destroy_aux() const;
482 
483  static const fnode* unique(const fnode*);
484 
485  // Destruction may only happen via destroy().
486  ~fnode() = default;
487  // Disallow copies.
488  fnode(const fnode&) = delete;
489  fnode& operator=(const fnode&) = delete;
490 
491 
492 
493  template<class iter>
494  fnode(op o, iter begin, iter end)
495  // Clang has some optimization where is it able to combine the
496  // 4 movb initializing op_,min_,max_,saturated_ into a single
497  // movl. Also it can optimize the three byte-comparisons of
498  // is_Kleene_star() into a single masked 32-bit comparison.
499  // The latter optimization triggers warnings from valgrind if
500  // min_ and max_ are not initialized. So to benefit from the
501  // initialization optimization and the is_Kleene_star()
502  // optimization in Clang, we always initialize min_ and max_
503  // with this compiler. Do not do it the rest of the time,
504  // since the optimization is not done.
505  : op_(o),
506 #if __llvm__
507  min_(0), max_(0),
508 #endif
509  saturated_(0)
510  {
511  size_t s = std::distance(begin, end);
512  if (s > (size_t) UINT16_MAX)
513  throw std::runtime_error("too many children for formula");
514  size_ = s;
515  auto pos = children;
516  for (auto i = begin; i != end; ++i)
517  *pos++ = *i;
518  setup_props(o);
519  }
520 
521  fnode(op o, std::initializer_list<const fnode*> l)
522  : fnode(o, l.begin(), l.end())
523  {
524  }
525 
526  fnode(op o, const fnode* f, uint8_t min, uint8_t max)
527  : op_(o), min_(min), max_(max), saturated_(0), size_(1)
528  {
529  children[0] = f;
530  setup_props(o);
531  }
532 
533  static const fnode* ff_;
534  static const fnode* tt_;
535  static const fnode* ew_;
536  static const fnode* one_star_;
537 
538  op op_; // operator
539  uint8_t min_; // range minimum (for star-like operators)
540  uint8_t max_; // range maximum;
541  mutable uint8_t saturated_;
542  uint16_t size_; // number of children
543  mutable uint16_t refs_ = 0; // reference count - 1;
544  size_t id_; // Also used as hash.
545  static size_t next_id_;
546 
547  struct ltl_prop
548  {
549  // All properties here should be expressed in such a a way
550  // that property(f && g) is just property(f)&property(g).
551  // This allows us to compute all properties of a compound
552  // formula in one operation.
553  //
554  // For instance we do not use a property that says "has
555  // temporal operator", because it would require an OR between
556  // the two arguments. Instead we have a property that
557  // says "no temporal operator", and that one is computed
558  // with an AND between the arguments.
559  //
560  // Also choose a name that makes sense when prefixed with
561  // "the formula is".
562  bool boolean:1; // No temporal operators.
563  bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
564  bool in_nenoform:1; // Negative Normal Form.
565  bool syntactic_si:1; // LTL-X or siPSL
566  bool sugar_free_ltl:1; // No F and G operators.
567  bool ltl_formula:1; // Only LTL operators.
568  bool psl_formula:1; // Only PSL operators.
569  bool sere_formula:1; // Only SERE operators.
570  bool finite:1; // Finite SERE formulae, or Bool+X forms.
571  bool eventual:1; // Purely eventual formula.
572  bool universal:1; // Purely universal formula.
573  bool syntactic_safety:1; // Syntactic Safety Property.
574  bool syntactic_guarantee:1; // Syntactic Guarantee Property.
575  bool syntactic_obligation:1; // Syntactic Obligation Property.
576  bool syntactic_recurrence:1; // Syntactic Recurrence Property.
577  bool syntactic_persistence:1; // Syntactic Persistence Property.
578  bool not_marked:1; // No occurrence of EConcatMarked.
579  bool accepting_eword:1; // Accepts the empty word.
580  bool lbt_atomic_props:1; // Use only atomic propositions like p42.
581  bool spin_atomic_props:1; // Use only spin-compatible atomic props.
582  };
583  union
584  {
585  // Use an unsigned for fast computation of all properties.
586  unsigned props;
587  ltl_prop is_;
588  };
589 
590  const fnode* children[1];
591  };
592 
594  SPOT_API
595  int atomic_prop_cmp(const fnode* f, const fnode* g);
596 
598  {
599  bool
600  operator()(const fnode* left, const fnode* right) const
601  {
602  SPOT_ASSERT(left);
603  SPOT_ASSERT(right);
604  if (left == right)
605  return false;
606 
607  // We want Boolean formulae first.
608  bool lib = left->is_boolean();
609  if (lib != right->is_boolean())
610  return lib;
611 
612  // We have two Boolean formulae
613  if (lib)
614  {
615  bool lconst = left->is_constant();
616  if (lconst != right->is_constant())
617  return lconst;
618  if (!lconst)
619  {
620  auto get_literal = [](const fnode* f) -> const fnode*
621  {
622  if (f->is(op::Not))
623  f = f->nth(0);
624  if (f->is(op::ap))
625  return f;
626  return nullptr;
627  };
628  // Literals should come first
629  const fnode* litl = get_literal(left);
630  const fnode* litr = get_literal(right);
631  if (!litl != !litr)
632  return litl;
633  if (litl)
634  {
635  // And they should be sorted alphabetically
636  int cmp = atomic_prop_cmp(litl, litr);
637  if (cmp)
638  return cmp < 0;
639  }
640  }
641  }
642 
643  size_t l = left->id();
644  size_t r = right->id();
645  if (l != r)
646  return l < r;
647  // Because the hash code assigned to each formula is the
648  // number of formulae constructed so far, it is very unlikely
649  // that we will ever reach a case were two different formulae
650  // have the same hash. This will happen only ever with have
651  // produced 256**sizeof(size_t) formulae (i.e. max_count has
652  // looped back to 0 and started over). In that case we can
653  // order two formulas by looking at their text representation.
654  // We could be more efficient and look at their AST, but it's
655  // not worth the burden. (Also ordering pointers is ruled out
656  // because it breaks the determinism of the implementation.)
657  std::ostringstream old;
658  left->dump(old);
659  std::ostringstream ord;
660  right->dump(ord);
661  return old.str() < ord.str();
662  }
663  };
664 
665 #endif // SWIG
666 
669  class SPOT_API formula final
670  {
671  const fnode* ptr_;
672  public:
677  explicit formula(const fnode* f) noexcept
678  : ptr_(f)
679  {
680  }
681 
687  formula(std::nullptr_t) noexcept
688  : ptr_(nullptr)
689  {
690  }
691 
693  formula() noexcept
694  : ptr_(nullptr)
695  {
696  }
697 
699  formula(const formula& f) noexcept
700  : ptr_(f.ptr_)
701  {
702  if (ptr_)
703  ptr_->clone();
704  }
705 
707  formula(formula&& f) noexcept
708  : ptr_(f.ptr_)
709  {
710  f.ptr_ = nullptr;
711  }
712 
715  {
716  if (ptr_)
717  ptr_->destroy();
718  }
719 
727  const formula& operator=(std::nullptr_t)
728  {
729  this->~formula();
730  ptr_ = nullptr;
731  return *this;
732  }
733 
734  const formula& operator=(const formula& f)
735  {
736  this->~formula();
737  if ((ptr_ = f.ptr_))
738  ptr_->clone();
739  return *this;
740  }
741 
742  const formula& operator=(formula&& f) noexcept
743  {
744  std::swap(f.ptr_, ptr_);
745  return *this;
746  }
747 
748  bool operator<(const formula& other) const noexcept
749  {
750  if (SPOT_UNLIKELY(!other.ptr_))
751  return false;
752  if (SPOT_UNLIKELY(!ptr_))
753  return true;
754  if (id() < other.id())
755  return true;
756  if (id() > other.id())
757  return false;
758  // The case where id()==other.id() but ptr_ != other.ptr_ is
759  // very unlikely (we would need to build more that UINT_MAX
760  // formulas), so let's just compare pointer, and ignore the fact
761  // that it may give some nondeterminism.
762  return ptr_ < other.ptr_;
763  }
764 
765  bool operator<=(const formula& other) const noexcept
766  {
767  return *this == other || *this < other;
768  }
769 
770  bool operator>(const formula& other) const noexcept
771  {
772  return !(*this <= other);
773  }
774 
775  bool operator>=(const formula& other) const noexcept
776  {
777  return !(*this < other);
778  }
779 
780  bool operator==(const formula& other) const noexcept
781  {
782  return other.ptr_ == ptr_;
783  }
784 
785  bool operator==(std::nullptr_t) const noexcept
786  {
787  return ptr_ == nullptr;
788  }
789 
790  bool operator!=(const formula& other) const noexcept
791  {
792  return other.ptr_ != ptr_;
793  }
794 
795  bool operator!=(std::nullptr_t) const noexcept
796  {
797  return ptr_ != nullptr;
798  }
799 
800  operator bool() const
801  {
802  return ptr_ != nullptr;
803  }
804 
806  // Forwarded functions //
808 
810  static constexpr uint8_t unbounded()
811  {
812  return fnode::unbounded();
813  }
814 
816  static formula ap(const std::string& name)
817  {
818  return formula(fnode::ap(name));
819  }
820 
826  static formula ap(const formula& a)
827  {
828  if (a.kind() == op::ap)
829  return a;
830  else
831  throw std::invalid_argument("atomic propositions cannot be "
832  "constructed from arbitrary formulas");
833  }
834 
839  static formula unop(op o, const formula& f)
840  {
841  return formula(fnode::unop(o, f.ptr_->clone()));
842  }
843 
844 #ifndef SWIG
845  static formula unop(op o, formula&& f)
846  {
847  return formula(fnode::unop(o, f.to_node_()));
848  }
849 #endif // !SWIG
850 
852 #ifdef SWIG
853 #define SPOT_DEF_UNOP(Name) \
854  static formula Name(const formula& f) \
855  { \
856  return unop(op::Name, f); \
857  }
858 #else // !SWIG
859 #define SPOT_DEF_UNOP(Name) \
860  static formula Name(const formula& f) \
861  { \
862  return unop(op::Name, f); \
863  } \
864  static formula Name(formula&& f) \
865  { \
866  return unop(op::Name, std::move(f)); \
867  }
868 #endif // !SWIG
869  SPOT_DEF_UNOP(Not);
873 
876  SPOT_DEF_UNOP(X);
878 
881  SPOT_DEF_UNOP(F);
883 
886  SPOT_DEF_UNOP(G);
888 
891  SPOT_DEF_UNOP(Closure);
893 
896  SPOT_DEF_UNOP(NegClosure);
898 
901  SPOT_DEF_UNOP(NegClosureMarked);
903 #undef SPOT_DEF_UNOP
904 
910  static formula binop(op o, const formula& f, const formula& g)
911  {
912  return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
913  }
914 
915 #ifndef SWIG
916  static formula binop(op o, const formula& f, formula&& g)
917  {
918  return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
919  }
920 
921  static formula binop(op o, formula&& f, const formula& g)
922  {
923  return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
924  }
925 
926  static formula binop(op o, formula&& f, formula&& g)
927  {
928  return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
929  }
931 
932 #endif //SWIG
933 
934 #ifdef SWIG
935 #define SPOT_DEF_BINOP(Name) \
936  static formula Name(const formula& f, const formula& g) \
937  { \
938  return binop(op::Name, f, g); \
939  }
940 #else // !SWIG
941 #define SPOT_DEF_BINOP(Name) \
942  static formula Name(const formula& f, const formula& g) \
943  { \
944  return binop(op::Name, f, g); \
945  } \
946  static formula Name(const formula& f, formula&& g) \
947  { \
948  return binop(op::Name, f, std::move(g)); \
949  } \
950  static formula Name(formula&& f, const formula& g) \
951  { \
952  return binop(op::Name, std::move(f), g); \
953  } \
954  static formula Name(formula&& f, formula&& g) \
955  { \
956  return binop(op::Name, std::move(f), std::move(g)); \
957  }
958 #endif // !SWIG
959  SPOT_DEF_BINOP(Xor);
963 
966  SPOT_DEF_BINOP(Implies);
968 
971  SPOT_DEF_BINOP(Equiv);
973 
976  SPOT_DEF_BINOP(U);
978 
981  SPOT_DEF_BINOP(R);
983 
986  SPOT_DEF_BINOP(W);
988 
991  SPOT_DEF_BINOP(M);
993 
996  SPOT_DEF_BINOP(EConcat);
998 
1001  SPOT_DEF_BINOP(EConcatMarked);
1003 
1006  SPOT_DEF_BINOP(UConcat);
1008 #undef SPOT_DEF_BINOP
1009 
1015  static formula multop(op o, const std::vector<formula>& l)
1016  {
1017  std::vector<const fnode*> tmp;
1018  tmp.reserve(l.size());
1019  for (auto f: l)
1020  if (f.ptr_)
1021  tmp.emplace_back(f.ptr_->clone());
1022  return formula(fnode::multop(o, std::move(tmp)));
1023  }
1024 
1025 #ifndef SWIG
1026  static formula multop(op o, std::vector<formula>&& l)
1027  {
1028  std::vector<const fnode*> tmp;
1029  tmp.reserve(l.size());
1030  for (auto f: l)
1031  if (f.ptr_)
1032  tmp.emplace_back(f.to_node_());
1033  return formula(fnode::multop(o, std::move(tmp)));
1034  }
1035 #endif // !SWIG
1036 
1038 #ifdef SWIG
1039 #define SPOT_DEF_MULTOP(Name) \
1040  static formula Name(const std::vector<formula>& l) \
1041  { \
1042  return multop(op::Name, l); \
1043  }
1044 #else // !SWIG
1045 #define SPOT_DEF_MULTOP(Name) \
1046  static formula Name(const std::vector<formula>& l) \
1047  { \
1048  return multop(op::Name, l); \
1049  } \
1050  \
1051  static formula Name(std::vector<formula>&& l) \
1052  { \
1053  return multop(op::Name, std::move(l)); \
1054  }
1055 #endif // !SWIG
1056  SPOT_DEF_MULTOP(Or);
1060 
1063  SPOT_DEF_MULTOP(OrRat);
1065 
1068  SPOT_DEF_MULTOP(And);
1070 
1073  SPOT_DEF_MULTOP(AndRat);
1075 
1078  SPOT_DEF_MULTOP(AndNLM);
1080 
1083  SPOT_DEF_MULTOP(Concat);
1085 
1088  SPOT_DEF_MULTOP(Fusion);
1090 #undef SPOT_DEF_MULTOP
1091 
1096  static formula bunop(op o, const formula& f,
1097  uint8_t min = 0U,
1098  uint8_t max = unbounded())
1099  {
1100  return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
1101  }
1102 
1103 #ifndef SWIG
1104  static formula bunop(op o, formula&& f,
1105  uint8_t min = 0U,
1106  uint8_t max = unbounded())
1107  {
1108  return formula(fnode::bunop(o, f.to_node_(), min, max));
1109  }
1110 #endif // !SWIG
1111 
1113 #if SWIG
1114 #define SPOT_DEF_BUNOP(Name) \
1115  static formula Name(const formula& f, \
1116  uint8_t min = 0U, \
1117  uint8_t max = unbounded()) \
1118  { \
1119  return bunop(op::Name, f, min, max); \
1120  }
1121 #else // !SWIG
1122 #define SPOT_DEF_BUNOP(Name) \
1123  static formula Name(const formula& f, \
1124  uint8_t min = 0U, \
1125  uint8_t max = unbounded()) \
1126  { \
1127  return bunop(op::Name, f, min, max); \
1128  } \
1129  static formula Name(formula&& f, \
1130  uint8_t min = 0U, \
1131  uint8_t max = unbounded()) \
1132  { \
1133  return bunop(op::Name, std::move(f), min, max); \
1134  }
1135 #endif
1136  SPOT_DEF_BUNOP(Star);
1140 
1145 
1160  SPOT_DEF_BUNOP(FStar);
1163 #undef SPOT_DEF_BUNOP
1164 
1170  static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1171 
1177  static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1178 
1179 #ifndef SWIG
1180  const fnode* to_node_()
1190  {
1191  auto tmp = ptr_;
1192  ptr_ = nullptr;
1193  return tmp;
1194  }
1195 #endif
1196 
1198  op kind() const
1199  {
1200  return ptr_->kind();
1201  }
1202 
1204  std::string kindstr() const
1205  {
1206  return ptr_->kindstr();
1207  }
1208 
1210  bool is(op o) const
1211  {
1212  return ptr_->is(o);
1213  }
1214 
1215 #ifndef SWIG
1216  bool is(op o1, op o2) const
1218  {
1219  return ptr_->is(o1, o2);
1220  }
1221 
1223  bool is(std::initializer_list<op> l) const
1224  {
1225  return ptr_->is(l);
1226  }
1227 #endif
1228 
1233  {
1234  auto f = ptr_->get_child_of(o);
1235  if (f)
1236  f->clone();
1237  return formula(f);
1238  }
1239 
1240 #ifndef SWIG
1241  formula get_child_of(std::initializer_list<op> l) const
1248  {
1249  auto f = ptr_->get_child_of(l);
1250  if (f)
1251  f->clone();
1252  return formula(f);
1253  }
1254 #endif
1255 
1259  unsigned min() const
1260  {
1261  return ptr_->min();
1262  }
1263 
1267  unsigned max() const
1268  {
1269  return ptr_->max();
1270  }
1271 
1273  unsigned size() const
1274  {
1275  return ptr_->size();
1276  }
1277 
1286  size_t id() const
1287  {
1288  return ptr_->id();
1289  }
1290 
1291 #ifndef SWIG
1292  class SPOT_API formula_child_iterator final
1294  {
1295  const fnode*const* ptr_;
1296  public:
1297  formula_child_iterator()
1298  : ptr_(nullptr)
1299  {
1300  }
1301 
1302  formula_child_iterator(const fnode*const* f)
1303  : ptr_(f)
1304  {
1305  }
1306 
1307  bool operator==(formula_child_iterator o)
1308  {
1309  return ptr_ == o.ptr_;
1310  }
1311 
1312  bool operator!=(formula_child_iterator o)
1313  {
1314  return ptr_ != o.ptr_;
1315  }
1316 
1317  formula operator*()
1318  {
1319  return formula((*ptr_)->clone());
1320  }
1321 
1322  formula_child_iterator operator++()
1323  {
1324  ++ptr_;
1325  return *this;
1326  }
1327 
1328  formula_child_iterator operator++(int)
1329  {
1330  auto tmp = *this;
1331  ++ptr_;
1332  return tmp;
1333  }
1334  };
1335 
1338  {
1339  return ptr_->begin();
1340  }
1341 
1344  {
1345  return ptr_->end();
1346  }
1347 
1349  formula operator[](unsigned i) const
1350  {
1351  return formula(ptr_->nth(i)->clone());
1352  }
1353 #endif
1354 
1356  static formula ff()
1357  {
1358  return formula(fnode::ff());
1359  }
1360 
1362  bool is_ff() const
1363  {
1364  return ptr_->is_ff();
1365  }
1366 
1368  static formula tt()
1369  {
1370  return formula(fnode::tt());
1371  }
1372 
1374  bool is_tt() const
1375  {
1376  return ptr_->is_tt();
1377  }
1378 
1380  static formula eword()
1381  {
1382  return formula(fnode::eword());
1383  }
1384 
1386  bool is_eword() const
1387  {
1388  return ptr_->is_eword();
1389  }
1390 
1392  bool is_constant() const
1393  {
1394  return ptr_->is_constant();
1395  }
1396 
1401  bool is_Kleene_star() const
1402  {
1403  return ptr_->is_Kleene_star();
1404  }
1405 
1408  {
1409  return formula(fnode::one_star()->clone());
1410  }
1411 
1414  bool is_literal()
1415  {
1416  return (is(op::ap) ||
1417  // If f is in nenoform, Not can only occur in front of
1418  // an atomic proposition. So this way we do not have
1419  // to check the type of the child.
1420  (is(op::Not) && is_boolean() && is_in_nenoform()));
1421  }
1422 
1426  const std::string& ap_name() const
1427  {
1428  return ptr_->ap_name();
1429  }
1430 
1435  std::ostream& dump(std::ostream& os) const
1436  {
1437  return ptr_->dump(os);
1438  }
1439 
1445  formula all_but(unsigned i) const
1446  {
1447  return formula(ptr_->all_but(i));
1448  }
1449 
1459  unsigned boolean_count() const
1460  {
1461  return ptr_->boolean_count();
1462  }
1463 
1477  formula boolean_operands(unsigned* width = nullptr) const
1478  {
1479  return formula(ptr_->boolean_operands(width));
1480  }
1481 
1482 #define SPOT_DEF_PROP(Name) \
1483  bool Name() const \
1484  { \
1485  return ptr_->Name(); \
1486  }
1487  // Properties //
1490 
1492  SPOT_DEF_PROP(is_boolean);
1494  SPOT_DEF_PROP(is_sugar_free_boolean);
1499  SPOT_DEF_PROP(is_in_nenoform);
1501  SPOT_DEF_PROP(is_syntactic_stutter_invariant);
1503  SPOT_DEF_PROP(is_sugar_free_ltl);
1505  SPOT_DEF_PROP(is_ltl_formula);
1507  SPOT_DEF_PROP(is_psl_formula);
1509  SPOT_DEF_PROP(is_sere_formula);
1512  SPOT_DEF_PROP(is_finite);
1516 
1530  SPOT_DEF_PROP(is_eventual);
1537 
1551  SPOT_DEF_PROP(is_universal);
1556  SPOT_DEF_PROP(is_syntactic_safety);
1558  SPOT_DEF_PROP(is_syntactic_guarantee);
1560  SPOT_DEF_PROP(is_syntactic_obligation);
1562  SPOT_DEF_PROP(is_syntactic_recurrence);
1564  SPOT_DEF_PROP(is_syntactic_persistence);
1567  SPOT_DEF_PROP(is_marked);
1569  SPOT_DEF_PROP(accepts_eword);
1575  SPOT_DEF_PROP(has_lbt_atomic_props);
1584  SPOT_DEF_PROP(has_spin_atomic_props);
1585 #undef SPOT_DEF_PROP
1586 
1588  template<typename Trans>
1589  formula map(Trans trans)
1590  {
1591  switch (op o = kind())
1592  {
1593  case op::ff:
1594  case op::tt:
1595  case op::eword:
1596  case op::ap:
1597  return *this;
1598  case op::Not:
1599  case op::X:
1600  case op::F:
1601  case op::G:
1602  case op::Closure:
1603  case op::NegClosure:
1604  case op::NegClosureMarked:
1605  return unop(o, trans((*this)[0]));
1606  case op::Xor:
1607  case op::Implies:
1608  case op::Equiv:
1609  case op::U:
1610  case op::R:
1611  case op::W:
1612  case op::M:
1613  case op::EConcat:
1614  case op::EConcatMarked:
1615  case op::UConcat:
1616  {
1617  formula tmp = trans((*this)[0]);
1618  return binop(o, tmp, trans((*this)[1]));
1619  }
1620  case op::Or:
1621  case op::OrRat:
1622  case op::And:
1623  case op::AndRat:
1624  case op::AndNLM:
1625  case op::Concat:
1626  case op::Fusion:
1627  {
1628  std::vector<formula> tmp;
1629  tmp.reserve(size());
1630  for (auto f: *this)
1631  tmp.emplace_back(trans(f));
1632  return multop(o, std::move(tmp));
1633  }
1634  case op::Star:
1635  case op::FStar:
1636  return bunop(o, trans((*this)[0]), min(), max());
1637  }
1638  SPOT_UNREACHABLE();
1639  }
1640 
1646  template<typename Func>
1647  void traverse(Func func)
1648  {
1649  if (func(*this))
1650  return;
1651  for (auto f: *this)
1652  f.traverse(func);
1653  }
1654  };
1655 
1657  SPOT_API
1658  std::ostream& print_formula_props(std::ostream& out, const formula& f,
1659  bool abbreviated = false);
1660 
1662  SPOT_API
1663  std::list<std::string> list_formula_props(const formula& f);
1664 
1666  SPOT_API
1667  std::ostream& operator<<(std::ostream& os, const formula& f);
1668 }
1669 
1670 #ifndef SWIG
1671 namespace std
1672 {
1673  template <>
1674  struct hash<spot::formula>
1675  {
1676  size_t operator()(const spot::formula& x) const noexcept
1677  {
1678  return x.id();
1679  }
1680  };
1681 }
1682 #endif
static formula multop(op o, const std::vector< formula > &l)
Construct an n-ary operator.
Definition: formula.hh:1015
bool is_tt() const
Definition: formula.hh:282
Definition: graph.hh:33
static formula one_star()
Return a copy of the formula 1[*].
Definition: formula.hh:1407
bool is_constant() const
Whether the formula is op::ff, op::tt, or op::eword.
Definition: formula.hh:1392
~formula()
Destroy a formula.
Definition: formula.hh:714
bool is(op o) const
Definition: formula.hh:165
std::ostream & dump(std::ostream &os) const
Print the formula for debugging.
Definition: formula.hh:1435
static formula binop(op o, formula &&f, formula &&g)
Construct a binary operator.
Definition: formula.hh:926
const fnode *const * begin() const
Definition: formula.hh:244
static const fnode * eword()
Definition: formula.hh:288
static const fnode * ap(const std::string &name)
formula get_child_of(op o) const
Remove operator o and return the child.
Definition: formula.hh:1232
formula all_but(unsigned i) const
clone this formula, omitting child i
Definition: formula.hh:1445
bool is_syntactic_stutter_invariant() const
Definition: formula.hh:378
PSL Closure.
static const fnode * unop(op o, const fnode *f)
unsigned max() const
Return end of the range for star-like operators.
Definition: formula.hh:1267
const std::string & ap_name() const
Print the name of an atomic proposition.
Definition: formula.hh:1426
bool is_syntactic_safety() const
Definition: formula.hh:426
bool is_tt() const
Whether the formula is the true constant.
Definition: formula.hh:1374
bool is_eventual() const
Definition: formula.hh:414
static formula ap(const std::string &name)
Build an atomic proposition.
Definition: formula.hh:816
unsigned size() const
Return the number of children.
Definition: formula.hh:1273
bool is_ltl_formula() const
Definition: formula.hh:390
formula(const formula &f) noexcept
Clone a formula.
Definition: formula.hh:699
static formula tt()
Return the true constant.
Definition: formula.hh:1368
unsigned boolean_count() const
number of Boolean children
Definition: formula.hh:1459
Definition: formula.hh:1671
bool is_psl_formula() const
Definition: formula.hh:396
bool is_sere_formula() const
Definition: formula.hh:402
Empty word.
static const fnode * tt()
Definition: formula.hh:276
static formula binop(op o, formula &&f, const formula &g)
Construct a binary operator.
Definition: formula.hh:921
static formula binop(op o, const formula &f, formula &&g)
Construct a binary operator.
Definition: formula.hh:916
bool is_marked() const
Definition: formula.hh:456
Concatenation.
bool is(op o1, op o2) const
Definition: formula.hh:171
unsigned min() const
Return start of the range for star-like operators.
Definition: formula.hh:1259
bool is_syntactic_recurrence() const
Definition: formula.hh:444
const fnode * clone() const
Clone an fnode.
Definition: formula.hh:114
Main class for temporal logic formula.
Definition: formula.hh:669
Globally.
release (dual of until)
unsigned size() const
Definition: formula.hh:232
bool is_literal()
Whether the formula is an atomic proposition or its negation.
Definition: formula.hh:1414
formula boolean_operands(unsigned *width=nullptr) const
return a clone of the current node, restricted to its Boolean children
Definition: formula.hh:1477
static formula unop(op o, formula &&f)
Build a unary operator.
Definition: formula.hh:845
bool is_ff() const
Whether the formula is the false constant.
Definition: formula.hh:1362
bool is_Kleene_star() const
Definition: formula.hh:306
Fustion Star.
bool is_in_nenoform() const
Definition: formula.hh:372
unsigned boolean_count() const
Definition: formula.hh:331
weak until
bool is_sugar_free_boolean() const
Definition: formula.hh:366
unsigned max() const
Definition: formula.hh:223
unsigned min() const
Definition: formula.hh:214
static formula ff()
Return the false constant.
Definition: formula.hh:1356
static const fnode * multop(op o, std::vector< const fnode * > l)
static formula multop(op o, std::vector< formula > &&l)
Construct an n-ary operator.
Definition: formula.hh:1026
formula operator[](unsigned i) const
Return children number i.
Definition: formula.hh:1349
static const fnode * bunop(op o, const fnode *f, uint8_t min, uint8_t max=unbounded())
Equivalence.
Non-Length-Matching Rational-And.
static const fnode * ff()
Definition: formula.hh:264
Allow iterating over children.
Definition: formula.hh:1293
static formula bunop(op o, formula &&f, uint8_t min=0U, uint8_t max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1104
static const fnode * one_star()
Definition: formula.hh:314
formula(std::nullptr_t) noexcept
Create a null formula.
Definition: formula.hh:687
Exclusive Or.
marked version of the Negated PSL Clusure
bool is_constant() const
Definition: formula.hh:300
static formula eword()
Return the empty word constant.
Definition: formula.hh:1380
const fnode * get_child_of(op o) const
Definition: formula.hh:190
const fnode *const * end() const
Definition: formula.hh:250
op kind() const
Return top-most operator.
Definition: formula.hh:1198
bool is(op o) const
Return true if the formula is of kind o.
Definition: formula.hh:1210
Definition: formula.hh:597
formula map(Trans trans)
Clone this node after applying trans to its children.
Definition: formula.hh:1589
bool has_spin_atomic_props() const
Definition: formula.hh:474
bool accepts_eword() const
Definition: formula.hh:462
bool is_Kleene_star() const
Test whether the formula represent a Kleene star.
Definition: formula.hh:1401
const fnode * nth(unsigned i) const
Definition: formula.hh:256
(omega-Rational) Or
void destroy() const
Dereference an fnode.
Definition: formula.hh:128
op kind() const
Definition: formula.hh:156
formula(const fnode *f) noexcept
Create a formula from an fnode.
Definition: formula.hh:677
static constexpr uint8_t unbounded()
Unbounded constant to use as end of range for bounded operators.
Definition: formula.hh:810
static constexpr uint8_t unbounded()
Definition: formula.hh:138
Negation.
const formula & operator=(std::nullptr_t)
Reset a formula to null.
Definition: formula.hh:727
const fnode * to_node_()
Return the underlying pointer to the formula.
Definition: formula.hh:1189
static formula ap(const formula &a)
Build an atomic proposition from... an atomic proposition.
Definition: formula.hh:826
bool is_syntactic_guarantee() const
Definition: formula.hh:432
std::ostream & dump(std::ostream &os) const
formula_child_iterator begin() const
Allow iterating over children.
Definition: formula.hh:1337
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:450
bool is_ff() const
Definition: formula.hh:270
static formula unop(op o, const formula &f)
Build a unary operator.
Definition: formula.hh:839
bool is_universal() const
Definition: formula.hh:420
static formula bunop(op o, const formula &f, uint8_t min=0U, uint8_t max=unbounded())
Define a bounded unary-operator (i.e. star-like)
Definition: formula.hh:1096
Implication.
bool is_boolean() const
Definition: formula.hh:360
bool is_syntactic_obligation() const
Definition: formula.hh:438
formula_child_iterator end() const
Allow iterating over children.
Definition: formula.hh:1343
bool is_sugar_free_ltl() const
Definition: formula.hh:384
Actual storage for formula nodes.
Definition: formula.hh:107
size_t id() const
Return the id of a formula.
Definition: formula.hh:1286
Negated PSL Closure.
bool is(std::initializer_list< op > l) const
Definition: formula.hh:177
Rational And.
static formula binop(op o, const formula &f, const formula &g)
Construct a binary operator.
Definition: formula.hh:910
bool is(std::initializer_list< op > l) const
Return true if the formulas nests all the operators in l.
Definition: formula.hh:1223
bool is_finite() const
Definition: formula.hh:408
strong release (dual of weak until)
void traverse(Func func)
Apply func to each subformula.
Definition: formula.hh:1647
bool has_lbt_atomic_props() const
Definition: formula.hh:468
Atomic proposition.
const fnode * get_child_of(std::initializer_list< op > l) const
Definition: formula.hh:201
Eventually.
std::string kindstr() const
Return the name of the top-most operator.
Definition: formula.hh:1204
formula(formula &&f) noexcept
Move-construct a formula.
Definition: formula.hh:707
(omega-Rational) And
size_t id() const
Definition: formula.hh:238
bool is_eword() const
Whether the formula is the empty word constant.
Definition: formula.hh:1386
Rational Or.
bool is_eword() const
Definition: formula.hh:294
formula() noexcept
Default initialize a formula to nullptr.
Definition: formula.hh:693

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Wed Mar 15 2017 09:26:50 for spot by doxygen 1.8.8