From b67852a5ff524c05aca1e22fd134e2dcd5dd0bf4 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 11 Nov 2011 15:53:05 +0100
Subject: [PATCH] Reuse Boolean->BDD translations performed during
 simplification.

* src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::ltl_to_bdd):
Use boolean_to_bdd()
---
 src/tgbaalgos/ltl2tgba_fm.cc | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc
index fbd6bdcb7..18e106038 100644
--- a/src/tgbaalgos/ltl2tgba_fm.cc
+++ b/src/tgbaalgos/ltl2tgba_fm.cc
@@ -1542,9 +1542,21 @@ namespace spot
       if (i != m->end())
 	return i->second;
 
-      ltl_trad_visitor v(*this, mark_all, exprop);
-      f->accept(v);
-      translated t = { v.result(), v.has_rational(), v.has_marked() };
+      translated t;
+      if (f->is_boolean())
+	{
+	  t.symbolic = boolean_to_bdd(f);
+	  t.has_rational = false;
+	  t.has_marked = false;
+	}
+      else
+	{
+	  ltl_trad_visitor v(*this, mark_all, exprop);
+	  f->accept(v);
+	  t.symbolic = v.result();
+	  t.has_rational = v.has_rational();
+	  t.has_marked = v.has_marked();
+	}
 
       return m->insert(std::make_pair(f->clone(), t)).first->second;
     }