Sort comutative binops like we sort multops.

* src/ltlast/formula.hh (is_literal): Rename as...
(get_literal): ... this.
(is_literal): New method.
(formula_ptr_less_than_multop): Rename as...
(formula_ptr_less_than_bool_first): ... this.
* src/ltlast/binop.cc: Use formula_ptr_less_than_bool_first.
* src/ltlast/multop.cc, src/ltlast/formula.cc: Adjust
to renamings.

src/ltlast/binop.cc

@@ -339,9 +339,9 @@ namespace spot
 	case Xor:
 	  {
 	    // Xor is commutative: sort operands.
-	    formula_ptr_less_than cmp;
+	    formula_ptr_less_than_bool_first cmp;
-	    if (cmp(second, first) > 0)
+	    if (cmp(second, first))
-	      std::swap(first, second);
+	      std::swap(second, first);
 	  }
 	  //   - (1 ^ Exp) = !Exp
 	  //   - (0 ^ Exp) = Exp
@@ -363,9 +363,9 @@ namespace spot
 	case Equiv:
 	  {
 	    // Equiv is commutative: sort operands.
-	    formula_ptr_less_than cmp;
+	    formula_ptr_less_than_bool_first cmp;
-	    if (cmp(second, first) > 0)
+	    if (cmp(second, first))
-	      std::swap(first, second);
+	      std::swap(second, first);
 	  }
 	  //   - (0 <=> Exp) = !Exp
 	  //   - (1 <=> Exp) = Exp

src/ltlast/formula.cc

@@ -120,8 +120,7 @@ namespace spot
       return out;
     }
 
-
+    const formula* get_literal(const formula* f)
-    const formula* is_literal(const formula* f)
     {
       const unop* g = is_Not(f);
       if (g)

src/ltlast/formula.hh

@@ -360,7 +360,22 @@ namespace spot
     ///
     /// Return 0 otherwise.
     SPOT_API
-    const formula* is_literal(const formula* f);
+    const formula* get_literal(const formula* f);
+
+    /// Return true iff f is a literal.
+    inline
+    bool
+    is_literal(const formula* f)
+    {
+      return (f->kind() == formula::AtomicProp
+	      // The only unary operator that is Boolean is Not,
+	      // and if f is in nenoform, Not can only occur in
+	      // front of an atomic proposition.  So with this
+	      // check we do not have to cast f to check what
+	      // operator it is and the type of its child.
+	      || (f->is_boolean() && f->is_in_nenoform()
+		  && f->kind() == formula::UnOp));
+    }
 
 
     /// Compare two atomic propositions.
@@ -419,7 +434,7 @@ namespace spot
     /// order to speed up implication checks.
     ///
     /// Also keep literal alphabetically ordered.
-    struct formula_ptr_less_than_multop:
+    struct formula_ptr_less_than_bool_first:
       public std::binary_function<const formula*, const formula*, bool>
     {
       bool
@@ -438,17 +453,24 @@ namespace spot
 	// We have two Boolean formulae
 	if (lib)
 	  {
-	    // Literals should come first
+	    bool lconst = left->kind() == formula::Constant;
-	    const formula* litl = is_literal(left);
+	    bool rconst = right->kind() == formula::Constant;
-	    const formula* litr = is_literal(right);
+	    if (lconst != rconst)
-	    if (!litl != !litr)
+	      return lconst;
-	      return litl;
+	    if (!lconst)
-	    if (litl)
 	      {
-		// And they should be sorted alphabetically
+		// Literals should come first
-		int cmp = atomic_prop_cmp(litl, litr);
+		const formula* litl = get_literal(left);
-		if (cmp)
+		const formula* litr = get_literal(right);
-		  return cmp < 0;
+		if (!litl != !litr)
+		  return litl;
+		if (litl)
+		  {
+		    // And they should be sorted alphabetically
+		    int cmp = atomic_prop_cmp(litl, litr);
+		    if (cmp)
+		      return cmp < 0;
+		  }
 	      }
 	  }
 

src/ltlast/multop.cc

@@ -167,6 +167,8 @@ namespace spot
 	*width = s;
       if (!s)
 	return 0;
+      if (s == 1)
+	return nth(0)->clone();
       vec* v = new vec(children_->begin(),
 		       children_->begin() + s);
       for (unsigned n = 0; n < s; ++n)
@@ -277,7 +279,7 @@ namespace spot
 		i = v->erase(i);
 		continue;
 	      }
-	    // All operator except "Concat" and "Fusion" are
+	    // All operators except "Concat" and "Fusion" are
 	    // commutative, so we just keep a list of the inlined
 	    // arguments that should later be added to the vector.
 	    // For concat we have to keep track of the order of
@@ -293,7 +295,7 @@ namespace spot
       }
 
       if (op != Concat && op != Fusion)
-	std::sort(v->begin(), v->end(), formula_ptr_less_than_multop());
+	std::sort(v->begin(), v->end(), formula_ptr_less_than_bool_first());
 
       unsigned orig_size = v->size();