* src/ltlparse/ltlparse.yy: Fix precedence OP_OR < OP_XOR < OP_AND.

* src/ltlast/binop.cc (binop::instance): Order operands for
associative operators, so that e.g. "a xor b" and "b xor a" are
mapped to the same formula.
* src/ltltest/equals.test: Check this.

ChangeLog

@@ -1,5 +1,11 @@
 2003-08-06  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/ltlparse/ltlparse.yy: Fix precedence OP_OR < OP_XOR < OP_AND.
+	* src/ltlast/binop.cc (binop::instance): Order operands for
+	associative operators, so that e.g. "a xor b" and "b xor a" are
+	mapped to the same formula.
+	* src/ltltest/equals.test: Check this.
+
 	* src/ltlvisit/dotty.cc (draw_node_): s/shabe/shape/.
 	(visit): Draw rectangular node for atomic propositions and
 	constant.  This is an attempt to mimic BuDDy's output.

src/ltlast/binop.cc

@@ -1,4 +1,5 @@
 #include <cassert>
+#include <utility>
 #include "binop.hh"
 #include "visitor.hh"
 
@@ -89,6 +90,23 @@ namespace spot
     binop*
     binop::instance(type op, formula* first, formula* second)
     {
+      // Sort the operands of associative operators, so that for
+      // example the formula instance for 'a xor b' is the same as
+      // that for 'b xor a'.
+      switch (op)
+	{
+	case Xor:
+	case Equiv:
+	  if (second < first)
+	    std::swap(first, second);
+	  break;
+	case Implies:
+	case U:
+	case R:
+	  // Non associative operators.
+	  break;
+	}
+
       pairf pf(first, second);
       pair p(op, pf);
       map::iterator i = instances.find(p);

src/ltlparse/ltlparse.yy

@@ -32,7 +32,9 @@ using namespace spot::ltl;
 %}
 
 /* Logical operators.  */
-%left <token> OP_AND OP_XOR OP_OR
+%left <token> OP_OR
+%left <token> OP_XOR
+%left <token> OP_AND
 %left <token> OP_IMPLIES OP_EQUIV
 
 /* LTL operators.  */

src/ltltest/equals.test

@@ -37,5 +37,8 @@ check 1 'a & b & c' 'c & a'
 check 1 'b & c' 'c & a & b'
 check 1 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
 
+# Precedence
+check 0 'a & b ^ c | d' 'd | c ^ b & a'
+
 # Success.
 :