From 929ffc417670886227493310dd2c6ef640131ff1 Mon Sep 17 00:00:00 2001
From: Philipp Schlehuber <philipp@lrde.epita.fr>
Date: Mon, 22 Nov 2021 17:15:03 +0100
Subject: [PATCH] Adapt ltlsynt

Using the new flexibility for solving and converting
of mealy machines and aiger circuits

* bin/ltlsynt.cc: here
---
 bin/ltlsynt.cc | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 57b67bcc0..45fd3b159 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -408,8 +408,14 @@ namespace
               spot::mealy_like ml;
               ml.success =
                 spot::mealy_like::realizability_code::REALIZABLE_REGULAR;
-              ml.mealy_like =
-                  spot::solved_game_to_separated_mealy(arena, *gi);
+              if (opt_print_aiger)
+                // we do not care about the type,
+                // machine to aiger can handle it
+                ml.mealy_like =
+                    spot::solved_game_to_mealy(arena, *gi);
+              else
+                ml.mealy_like =
+                    spot::solved_game_to_separated_mealy(arena, *gi);
               ml.glob_cond = bddfalse;
               mealy_machines.push_back(ml);
             }
@@ -452,8 +458,11 @@ namespace
                   delta = sw_direct.stop();
                 }
 
-              // Unsplit to have separated mealy
-              m_like.mealy_like = unsplit_mealy(m_like.mealy_like);
+              // If our goal is to have an aiger,
+              // we can use split or separated machines
+              if (!opt_print_aiger)
+                // Unsplit to have separated mealy
+                m_like.mealy_like = unsplit_mealy(m_like.mealy_like);
 
               if (gi->bv)
                 gi->bv->strat2aut_time += delta;