introduce formula::is_leaf()

Fixes #307.

* spot/tl/formula.hh: Here.
* tests/python/ltlparse.py: Test it.
* NEWS: Mention it.

NEWS

@@ -187,6 +187,9 @@ New in spot 2.4.2.dev (not yet released)
       Fin(i) & Fin(j) = f          Inf(i) | Inf(j) = t
       Fin(i) & Inf(i) = f          Fin(i) | Inf(i) = t
 
+  - The new spot::formula::is_leaf() method can be used to detect
+    formulas without children (atomic propositions, or constants).
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)

spot/tl/formula.hh

@@ -231,6 +231,12 @@ namespace spot
         return size_;
       }
 
+      /// \see formula::is_leaf
+      bool is_leaf() const
+      {
+        return size_ == 0;
+      }
+
       /// \see formula::id
       size_t id() const
       {
@@ -1277,6 +1283,15 @@ namespace spot
       return ptr_->size();
     }
 
+    /// \brief Whether the formula is a leaf.
+    ///
+    /// Leaves are formulas without children.  They are either
+    /// constants (true, false, empty word) or atomic propositions.
+    bool is_leaf() const
+    {
+      return ptr_->is_leaf();
+    }
+
     /// \brief Return the id of a formula.
     ///
     /// Can be used as a hash number.

tests/python/ltlparse.py

@@ -25,9 +25,13 @@ import spot
 
 e = spot.default_environment.instance()
 
-l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \\/ a \\/ b \\/ a \\/ a']
+l = [('GFa', False),
+     ('a U (((b)) xor c)', False),
+     ('!(FFx <=> Fx)', True),
+     ('a \\/ a \\/ b \\/ a \\/ a', False)]
 
-for str1 in l:
+
+for str1, isl in l:
     pf = spot.parse_infix_psl(str1, e, False)
     if pf.format_errors(spot.get_cout()):
         sys.exit(1)
@@ -37,8 +41,12 @@ for str1 in l:
     pf = spot.parse_infix_psl(str2, e)
     if pf.format_errors(spot.get_cout()):
         sys.exit(1)
+    assert isl == pf.f.is_leaf()
     del pf
 
+assert spot.formula('a').is_leaf();
+assert spot.formula('0').is_leaf();
+
 for str1 in ['a * b', 'a xor b', 'a <-> b']:
     pf = spot.parse_infix_boolean(str1, e, False)
     if pf.format_errors(spot.get_cout()):