From 473af5bb1d8fb388237f158a1b4868898845b339 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 22 Jun 2004 22:48:34 +0000
Subject: [PATCH] * src/ltlvisit/basicreduce.cc
 (basic_reduce_visitor::visit(binop*)): Factorize.

---
 ChangeLog                   |  3 +++
 src/ltlvisit/basicreduce.cc | 52 +++++--------------------------------
 2 files changed, 10 insertions(+), 45 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 8fb459f42..93c988df2 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,5 +1,8 @@
 2004-06-23  Alexandre Duret-Lutz  <adl@gnu.org>
 
+	* src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)):
+	Factorize.
+
 	* src/ltlvisit/basicreduce.hh: New file, extracted from ...
 	* src/ltlvisit/reducform.hh: ... here.
 	* src/ltlvisit/basereduc.cc: Rename as ...
diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc
index 50881d3d1..291995643 100644
--- a/src/ltlvisit/basicreduce.cc
+++ b/src/ltlvisit/basicreduce.cc
@@ -232,56 +232,18 @@ namespace spot
 	switch (bo->op())
 	  {
 	  case binop::Xor:
-	    result_ = binop::instance(binop::Xor,
-				      basic_reduce(f1),
-				      basic_reduce(f2));
-	    return;
 	  case binop::Equiv:
-	    result_ = binop::instance(binop::Equiv,
-				      basic_reduce(f1),
-				      basic_reduce(f2));
-	    return;
 	  case binop::Implies:
-	    result_ = binop::instance(binop::Implies,
+	    result_ = binop::instance(bo->op(),
 				      basic_reduce(f1),
 				      basic_reduce(f2));
 	    return;
 	  case binop::U:
+	  case binop::R:
 	    f2 = basic_reduce(f2);
 
 	    // a U false = false
 	    // a U true = true
-	    if (dynamic_cast<constant*>(f2))
-	      {
-		result_ = f2;
-		return;
-	      }
-
-	    f1 = basic_reduce(f1);
-
-	    // X(a) U X(b) = X(a U b)
-	    fu1 = dynamic_cast<unop*>(f1);
-	    fu2 = dynamic_cast<unop*>(f2);
-	    if ((fu1 && fu2) &&
-		(fu1->op() == unop::X) &&
-		(fu2->op() == unop::X))
-	      {
-		formula* ftmp = binop::instance(binop::U,
-						basic_reduce(fu1->child()),
-						basic_reduce(fu2->child()));
-		result_ = unop::instance(unop::X, basic_reduce(ftmp));
-		destroy(f1);
-		destroy(f2);
-		destroy(ftmp);
-		return;
-	      }
-
-	    result_ = binop::instance(binop::U, f1, f2);
-	    return;
-
-	  case binop::R:
-	    f2 = basic_reduce(f2);
-
 	    // a R false = false
 	    // a R true = true
 	    if (dynamic_cast<constant*>(f2))
@@ -292,12 +254,13 @@ namespace spot
 
 	    f1 = basic_reduce(f1);
 
+	    // X(a) U X(b) = X(a U b)
 	    // X(a) R X(b) = X(a R b)
 	    fu1 = dynamic_cast<unop*>(f1);
 	    fu2 = dynamic_cast<unop*>(f2);
-	    if ((fu1 && fu2) &&
-		(fu1->op() == unop::X) &&
-		(fu2->op() == unop::X))
+	    if (fu1 && fu2
+		&& fu1->op() == unop::X
+		&& fu2->op() == unop::X)
 	      {
 		formula* ftmp = binop::instance(bo->op(),
 						basic_reduce(fu1->child()),
@@ -309,8 +272,7 @@ namespace spot
 		return;
 	    }
 
-	    result_ = binop::instance(bo->op(),
-				      f1, f2);
+	    result_ = binop::instance(bo->op(), f1, f2);
 	    return;
 	  }
 	/* Unreachable code.  */