From 0d32884d2044c32de7d3e564e508949ddcc13299 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 6 Aug 2003 10:47:42 +0000
Subject: [PATCH] * 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                |  6 ++++++
 src/ltlast/binop.cc      | 18 ++++++++++++++++++
 src/ltlparse/ltlparse.yy |  4 +++-
 src/ltltest/equals.test  |  5 ++++-
 4 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 88785dd67..84824819e 100644
--- a/ChangeLog
+++ b/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.
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index 6129556ad..c874dd7c3 100644
--- a/src/ltlast/binop.cc
+++ b/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);
diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy
index 9c6391870..72fa09af6 100644
--- a/src/ltlparse/ltlparse.yy
+++ b/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.  */
diff --git a/src/ltltest/equals.test b/src/ltltest/equals.test
index 27a1f505d..d84cec858 100755
--- a/src/ltltest/equals.test
+++ b/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.
-:
\ No newline at end of file
+: