Arrange multops so that Boolean arguments come first.

This helps recursive implication checks.  Also order
atomic propositions with strverscmp().

* src/ltlast/formula.hh (formula_ptr_less_than_multop,
is_literal, atomic_prop_cmp): New.
* src/ltlast/formula.cc (is_literal, atomic_prop_cmp): Implement them.
* src/ltlast/multop.cc: Use formula_ptr_less_than_multop.
* src/ltltest/isop.test, src/ltltest/ltlfilt.test,
src/tgbatest/det.test, src/tgbatest/dstar.test,
src/tgbatest/explicit.test, src/tgbatest/explpro2.test,
src/tgbatest/explpro3.test, src/tgbatest/explprod.test,
src/tgbatest/nondet.test, src/tgbatest/tripprod.test: Adjust tests.
* NEWS: Mention the new order.

NEWS

@@ -158,6 +158,11 @@ New in spot 1.1.4a (not relased)
       Small or Deterministic.  These can now be combined with Complete
       as Any|Complete, Small|Complete, or Deterministic|Complete.
 
+    - operands of n-ary operators (like & and |) are now ordered so
+      that Boolean terms come first.  This speeds up syntactic
+      implication checks slightly.  Also, literals are now sorted
+      using strverscmp(), so that p5 comes before p12.
+
     - All the parsers implemented in Spot now use the same type to
       store locations.
 

src/ltlast/formula.cc

@@ -20,9 +20,14 @@
 // You should have received a copy of the GNU General Public License
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+#include "config.h"
 #include "formula.hh"
 #include "misc/hash.hh"
+#include "misc/casts.hh"
 #include <iostream>
+#include "unop.hh"
+#include "atomic_prop.hh"
+#include <string.h>
 
 namespace spot
 {
@@ -114,5 +119,22 @@ namespace spot
 
       return out;
     }
+
+
+    const formula* is_literal(const formula* f)
+    {
+      const unop* g = is_Not(f);
+      if (g)
+	f = g->child();
+      return is_atomic_prop(f);
+    }
+
+    int atomic_prop_cmp(const formula* f, const formula* g)
+    {
+      const atomic_prop* a = down_cast<const atomic_prop*>(f);
+      const atomic_prop* b = down_cast<const atomic_prop*>(g);
+      return strverscmp(a->name().c_str(), b->name().c_str());
+    }
+
   }
 }

src/ltlast/formula.hh

@@ -354,6 +354,20 @@ namespace spot
       opkind kind_;
     };
 
+
+    /// \brief Change \a f into <code>a</code> if it is equal to
+    /// <code>!a</code> or <code>a</code>.
+    ///
+    /// Return 0 otherwise.
+    SPOT_API
+    const formula* is_literal(const formula* f);
+
+
+    /// Compare two atomic propositions.
+    SPOT_API
+    int atomic_prop_cmp(const formula* f, const formula* g);
+
+
     /// \ingroup ltl_essentials
     /// \brief Strict Weak Ordering for <code>const formula*</code>.
     ///
@@ -377,6 +391,67 @@ namespace spot
 	assert(right);
 	if (left == right)
 	  return false;
+
+	size_t l = left->hash();
+	size_t r = right->hash();
+	if (l != r)
+	  return l < r;
+	// Because the hash code assigned to each formula is the
+	// number of formulae constructed so far, it is very unlikely
+	// that we will ever reach a case were two different formulae
+	// have the same hash.  This will happen only ever with have
+	// produced 256**sizeof(size_t) formulae (i.e. max_count has
+	// looped back to 0 and started over).  In that case we can
+	// order two formulae by looking at their text representation.
+	// We could be more efficient and look at their AST, but it's
+	// not worth the burden.  (Also ordering pointers is ruled out
+	// because it breaks the determinism of the implementation.)
+	return left->dump() < right->dump();
+      }
+    };
+
+    /// \brief Strict Weak Ordering for <code>const formula*</code>
+    ///        inside ltl::multop.
+    /// \ingroup ltl_essentials
+    ///
+    /// This is the comparison functor used by to order the
+    /// ltl::multop operands.  It keeps Boolean formulae first in
+    /// order to speed up implication checks.
+    ///
+    /// Also keep literal alphabetically ordered.
+    struct formula_ptr_less_than_multop:
+      public std::binary_function<const formula*, const formula*, bool>
+    {
+      bool
+      operator()(const formula* left, const formula* right) const
+      {
+	assert(left);
+	assert(right);
+	if (left == right)
+	  return false;
+
+	// We want Boolean formulae first.
+	bool lib = left->is_boolean();
+	if (lib != right->is_boolean())
+	  return lib;
+
+	// We have two Boolean formulae
+	if (lib)
+	  {
+	    // Literals should come first
+	    const formula* litl = is_literal(left);
+	    const formula* litr = is_literal(right);
+	    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;
+	      }
+	  }
+
 	size_t l = left->hash();
 	size_t r = right->hash();
 	if (l != r)

src/ltlast/multop.cc

@@ -199,13 +199,13 @@ namespace spot
 	      }
 	  }
 	// - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
-	//    AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2))
+	//    AndNLM(And(Bool1,Bool2),Exps1...,Exps2...,Exps3...)
 	// - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
-	//    AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2))
+	//    AndRat(And(Bool1,Bool2),Exps1...,Exps2...,Exps3...)
 	// - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
-	//    AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2))
+	//    AndRat(Or(Bool1,Bool2),Exps1...,Exps2...,Exps3...)
 	if (!b->empty())
-	  v->push_back(multop::instance(op, b));
+	  v->insert(v->begin(), multop::instance(op, b));
 	else
 	  delete b;
       }
@@ -240,18 +240,15 @@ namespace spot
 		i = v->erase(i);
 		continue;
 	      }
-	    if (const multop* p = is_multop(*i))
+	    if (const multop* p = is_multop(*i, op))
 	      {
-		if (p->op() == op)
-		  {
-		    unsigned ps = p->size();
-		    for (unsigned n = 0; n < ps; ++n)
-		      inlined.push_back(p->nth(n)->clone());
-		    (*i)->destroy();
-		    // FIXME: Do not use erase.  See previous FIXME.
-		    i = v->erase(i);
-		    continue;
-		  }
+		unsigned ps = p->size();
+		for (unsigned n = 0; n < ps; ++n)
+		  inlined.push_back(p->nth(n)->clone());
+		(*i)->destroy();
+		// FIXME: Do not use erase.  See previous FIXME.
+		i = v->erase(i);
+		continue;
 	      }
 	    // All operator except "Concat" and "Fusion" are
 	    // commutative, so we just keep a list of the inlined
@@ -263,13 +260,13 @@ namespace spot
 	    ++i;
 	  }
 	if (op == Concat || op == Fusion)
-	  *v = inlined;
+	  v->swap(inlined);
 	else
 	  v->insert(v->end(), inlined.begin(), inlined.end());
       }
 
       if (op != Concat && op != Fusion)
-	std::sort(v->begin(), v->end(), formula_ptr_less_than());
+	std::sort(v->begin(), v->end(), formula_ptr_less_than_multop());
 
       unsigned orig_size = v->size();
 

src/ltltest/isop.test

@@ -33,9 +33,9 @@ run 0 ../../bin/ltlfilt --boolean-to-isop input > output
 
 cat> expected<<EOF
 (!a & !b) | (b & d)
-(b | !a) & (d | !b) & Xc
+(!a | b) & (!b | d) & Xc
 GF(b | (a & d))
-{{{{!a && !b} | {b && d}}}[*];a[*]}<>-> ((a & !b) | (b & !a))
+{{{{!a && !b} | {b && d}}}[*];a[*]}<>-> ((!a & b) | (a & !b))
 EOF
 
 cat output
@@ -46,9 +46,9 @@ run 0 ../../bin/ltlfilt input > output
 
 cat> expected<<EOF
 (a -> b) & (b -> d)
-(a -> b) & Xc & (b -> d)
+(a -> b) & (b -> d) & Xc
 GF((a | b) & (b | d))
-{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!b | !a))
+{{{{a -> b} && {b -> d}}}[*];a[*]}<>-> ((a | b) & (!a | !b))
 EOF
 
 cat output

src/ltltest/ltlfilt.test

@@ -90,7 +90,7 @@ b W GFa
 Fb
 G(a & Xb)
 Xa
-F(a & X(b & !a))
+F(a & X(!a & b))
 a & (b | c)
 EOF
 
@@ -98,7 +98,7 @@ checkopt --simplify --eventual --unique <<EOF
 F(GFa | Gb)
 F(b W GFa)
 Fb
-F(a & X(b & !a))
+F(a & X(!a & b))
 EOF
 
 checkopt --safety <<EOF

src/tgbatest/det.test

@@ -24,13 +24,13 @@ set -e
 ltl2tgba=../../bin/ltl2tgba
 
 cat >formulas <<'EOF'
-1,14,X((a M F((!c & !b) | (c & b))) W (G!c U b))
+1,14,X((a M F((!b & !c) | (b & c))) W (G!c U b))
 1,5,X(((a & b) R (!a U !c)) R b)
 1,10,XXG(Fa U Xb)
 1,5,(!a M !b) W F!c
 1,3,(b & Fa & GFc) R a
-1,2,(a R (b W a)) W G(!a M (c | b))
-1,11,(Fa W b) R (Fc | !a)
+1,2,(a R (b W a)) W G(!a M (b | c))
+1,11,(Fa W b) R (!a | Fc)
 1,7,X(G(!a M !b) | G(a | G!a))
 1,2,Fa W Gb
 1,3,Ga | GFb
@@ -49,7 +49,7 @@ cat >formulas <<'EOF'
 1,4,X(Gb | GFa)
 1,9,X(Gc | XG((b & Ga) | (!b & F!a)))
 1,2,Ga R Fb
-1,3,G(a U (b | X((!c & !a) | (a & c))))
+1,3,G(a U (b | X((!a & !c) | (a & c))))
 1,5,XG((G!a & F!b) | (Fa & (a | Gb)))
 1,10,(a U X!a) | XG(!b & XFc)
 1,4,X(G!a | GFa)

src/tgbatest/dstar.test

@@ -216,7 +216,7 @@ digraph G {
   1 [label="1"]
   1 -> 2 [label="!a & !b\n"]
   1 -> 3 [label="a & !b\n"]
-  1 -> 4 [label="b & !a\n"]
+  1 -> 4 [label="!a & b\n"]
   1 -> 5 [label="a & b\n"]
   2 [label="2"]
   2 -> 2 [label="!b\n"]
@@ -224,7 +224,7 @@ digraph G {
   3 [label="4", peripheries=2]
   3 -> 2 [label="!a & !b\n{Acc[1]}"]
   3 -> 3 [label="a & !b\n{Acc[1]}"]
-  3 -> 4 [label="b & !a\n{Acc[1]}"]
+  3 -> 4 [label="!a & b\n{Acc[1]}"]
   3 -> 5 [label="a & b\n{Acc[1]}"]
   4 [label="3", peripheries=2]
   4 -> 4 [label="1\n{Acc[1]}"]

src/tgbatest/explicit.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -25,7 +25,7 @@
 
 set -e
 
-run 0 ../explicit | sed 's/c & b/b \& c/' > stdout
+run 0 ../explicit > stdout
 
 cat >expected <<EOF
 digraph G {

src/tgbatest/explpro2.test

@@ -1,4 +1,6 @@
 #!/bin/sh
+# Copyright (C) 2013 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2005, 2006, 2008, 2009 Laboratoire
 # d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
 # Coopératifs (SRC), Université Pierre et Marie Curie.
@@ -37,13 +39,10 @@ EOF
 
 cat >expected <<'EOF'
 acc = "p2$1" "p3" "p2" "p1";
-"s1 * s1", "s2 * s2", "b & !a", "p2$1" "p1";
+"s1 * s1", "s2 * s2", "!a & b", "p2$1" "p1";
 "s1 * s1", "s3 * s3", "a & !b", "p3" "p2";
 EOF
 
-run 0 ../explprod input1 input2 |
-  sed 's/!a & b/b \& !a/;s/!b & a/a \& !b/'> stdout
-
-cat stdout
+run 0 ../explprod input1 input2 | tee stdout
 diff stdout expected
 rm input1 input2 stdout expected

src/tgbatest/explpro3.test

@@ -43,13 +43,7 @@ acc = "p2" "p3";
 "s1 * s1", "s3 * s3", "a & !b", "p3";
 EOF
 
-run 0 ../explprod input1 input2 > stdout
-
-# Sort out some possible inversions in the output.
-# (The order is not guaranteed by SPOT.)
-sed 's/"p3" "p2"/"p2" "p3"/g;s/!b & a/a \& !b/g;
-     s/b & !a/!a \& b/g' stdout > tmp_ && mv tmp_ stdout
-
-cat stdout
+run 0 ../explprod input1 input2 |
+sed 's/"p3" "p2"/"p2" "p3"/g' | tee stdout
 diff stdout expected
 rm input1 input2 stdout expected

src/tgbatest/explprod.test

@@ -1,6 +1,6 @@
 #!/bin/sh
-# Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
-# de l'Epita (LRDE).
+# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et
+# Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 # Université Pierre et Marie Curie.
@@ -46,9 +46,6 @@ acc = "p3" "p2" "p1";
 "s2 * s2", "s3 * s1", "a & c", "p3" "p1";
 EOF
 
-run 0 ../explprod input1 input2 |
-  sed 's/b & a/a \& b/;s/c & a/a \& c/' > stdout
-
-cat stdout
+run 0 ../explprod input1 input2 | tee stdout
 diff stdout expected
 rm input1 input2 stdout expected

src/tgbatest/nondet.test

@@ -25,7 +25,7 @@ cat >expected.1<<EOF
 FGa, 0 0
 GFa, 1 1
 a U b, 1 0
-G(Fa | !r) | Fx, 0 1
+G(!r | Fa) | Fx, 0 1
 EOF
 
 cut -d, -f1 expected.1 |
@@ -36,7 +36,7 @@ cat >expected.2<<EOF
 FGa, 0 1
 GFa, 1 1
 a U b, 1 1
-G(Fa | !r) | Fx, 0 1
+G(!r | Fa) | Fx, 0 1
 EOF
 
 cut -d, -f1 expected.2 |

src/tgbatest/tripprod.test

@@ -1,5 +1,5 @@
 #!/bin/sh
-# Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement
+# Copyright (C) 2008, 2009, 2013 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 # Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
 # Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -57,9 +57,6 @@ acc = "p4" "p3" "p2" "p1";
 "s2 * s2 * s3", "s3 * s1 * s2", "a & c", "p4" "p3";
 EOF
 
-run 0 ../tripprod input1 input2 input3 |
-  sed 's/b & a/a \& b/;s/c & a/a \& c/'> stdout
-
-cat stdout
+run 0 ../tripprod input1 input2 input3 | tee stdout
 diff stdout expected
 rm input1 input2 input3 stdout expected