ltlsynt: extract In/Out AP processing in separate file

We'd like to reuse the --ins/--outs matching in ltlfilt
as well, so let's put that code in a common file.

* bin/common_ioap.cc, bin/common_ioap.hh: New files.
* bin/ltlsynt.cc: Extracted from here.
* bin/Makefile.am: Add them.

bin/Makefile.am

@@ -43,6 +43,8 @@ libcommon_a_SOURCES =				\
   common_finput.hh				\
   common_hoaread.cc				\
   common_hoaread.hh				\
+  common_ioap.cc				\
+  common_ioap.hh				\
   common_output.cc				\
   common_output.hh				\
   common_post.cc				\

bin/common_ioap.cc

@@ -0,0 +1,166 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#include "common_ioap.hh"
+#include "error.h"
+#include <unordered_set>
+
+// --ins and --outs, as supplied on the command-line
+std::optional<std::vector<std::string>> all_output_aps;
+std::optional<std::vector<std::string>> all_input_aps;
+
+// Store refirst, separate the filters that are regular expressions from
+// the others.  Compile the regular expressions while we are at it.
+std::vector<std::regex> regex_in;
+std::vector<std::regex> regex_out;
+// map identifier to input/output (false=input, true=output)
+std::unordered_map<std::string, bool> identifier_map;
+
+static std::string
+str_tolower(std::string s)
+{
+  std::transform(s.begin(), s.end(), s.begin(),
+                 [](unsigned char c){ return std::tolower(c); });
+  return s;
+}
+
+void
+split_aps(const std::string& arg, std::vector<std::string>& where)
+{
+  std::istringstream aps(arg);
+  std::string ap;
+  while (std::getline(aps, ap, ','))
+    {
+      ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
+      where.push_back(str_tolower(ap));
+    }
+}
+
+void process_io_options()
+{
+  // Filter identifiers from regexes.
+  if (all_input_aps.has_value())
+    for (const std::string& f: *all_input_aps)
+      {
+        unsigned sz = f.size();
+        if (f[0] == '/' && f[sz - 1] == '/')
+          regex_in.push_back(std::regex(f.substr(1, sz - 2)));
+        else
+          identifier_map.emplace(f, false);
+      }
+  if (all_output_aps.has_value())
+    for (const std::string& f: *all_output_aps)
+      {
+        unsigned sz = f.size();
+        if (f[0] == '/' && f[sz - 1] == '/')
+          regex_out.push_back(std::regex(f.substr(1, sz - 2)));
+        else if (auto [it, is_new] = identifier_map.try_emplace(f, true);
+                 !is_new && !it->second)
+          error(2, 0, "'%s' appears in both --ins and --outs",
+                f.c_str());
+      }
+}
+
+static std::unordered_set<std::string>
+list_aps_in_formula(spot::formula f)
+{
+  std::unordered_set<std::string> aps;
+  f.traverse([&aps](spot::formula s) {
+    if (s.is(spot::op::ap))
+      aps.emplace(s.ap_name());
+    return false;
+  });
+  return aps;
+}
+
+// Takes a set of the atomic propositions appearing in the formula,
+// and separate them into two vectors: input APs and output APs.
+std::pair<std::vector<std::string>, std::vector<std::string>>
+filter_list_of_aps(spot::formula f, const char* filename, int linenum)
+{
+  std::unordered_set<std::string> aps = list_aps_in_formula(f);
+  // now iterate over the list of atomic propositions to filter them
+  std::vector<std::string> matched[2]; // 0 = input, 1 = output
+  for (const std::string& a: aps)
+    {
+      if (auto it = identifier_map.find(a); it != identifier_map.end())
+        {
+          matched[it->second].push_back(a);
+          continue;
+        }
+
+      bool found_in = false;
+      for (const std::regex& r: regex_in)
+        if (std::regex_search(a, r))
+          {
+            found_in = true;
+            break;
+          }
+      bool found_out = false;
+      for (const std::regex& r: regex_out)
+        if (std::regex_search(a, r))
+          {
+            found_out = true;
+            break;
+          }
+      if (all_input_aps.has_value() == all_output_aps.has_value())
+        {
+          if (!all_input_aps.has_value())
+            {
+              // If the atomic proposition hasn't been classified
+              // because neither --ins nor --out were specified,
+              // attempt to classify automatically using the first
+              // letter.
+              int fl = a[0];
+              if (fl == 'i' || fl == 'I')
+                found_in = true;
+              else if (fl == 'o' || fl == 'O')
+                found_out = true;
+            }
+          if (found_in && found_out)
+            error_at_line(2, 0, filename, linenum,
+                          "'%s' matches both --ins and --outs",
+                          a.c_str());
+          if (!found_in && !found_out)
+            {
+              if (all_input_aps.has_value() || all_output_aps.has_value())
+                error_at_line(2, 0, filename, linenum,
+                              "one of --ins or --outs should match '%s'",
+                              a.c_str());
+              else
+                error_at_line(2, 0, filename, linenum,
+                              "since '%s' does not start with 'i' or 'o', "
+                              "it is unclear if it is an input or "
+                              "an output;\n    use --ins or --outs",
+                              a.c_str());
+            }
+        }
+      else
+        {
+          // if we had only --ins or only --outs, anything not
+          // matching that was given is assumed to belong to the
+          // other one.
+          if (!all_input_aps.has_value() && !found_out)
+            found_in = true;
+          else if (!all_output_aps.has_value() && !found_in)
+            found_out = true;
+        }
+      matched[found_out].push_back(a);
+    }
+  return {matched[0], matched[1]};
+}

bin/common_ioap.hh

@@ -0,0 +1,51 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) by the Spot authors, see the AUTHORS file for details.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#pragma once
+
+#include "common_sys.hh"
+#include <optional>
+#include <regex>
+#include <string>
+#include <vector>
+#include <unordered_map>
+#include <spot/tl/formula.hh>
+
+// --ins and --outs, as supplied on the command-line
+extern std::optional<std::vector<std::string>> all_output_aps;
+extern std::optional<std::vector<std::string>> all_input_aps;
+
+// Comma-separated list of strings, such as those passed to --ins/--outs
+void split_aps(const std::string& arg, std::vector<std::string>& where);
+
+// process the all_output_aps and all_input_aps above to
+// fill regex_in, regex_out, and identifier_map.
+void process_io_options();
+
+// Store refirst, separate the filters that are regular expressions from
+// the others.  Compile the regular expressions while we are at it.
+extern std::vector<std::regex> regex_in;
+extern std::vector<std::regex> regex_out;
+// map identifier to input/output (false=input, true=output)
+extern std::unordered_map<std::string, bool> identifier_map;
+
+// Separate the set of the atomic propositions appearing in f, into
+// two vectors: input APs and output APs, becased on regex_in,
+// regex_out, and identifier_map.
+std::pair<std::vector<std::string>, std::vector<std::string>>
+filter_list_of_aps(spot::formula f, const char* filename, int linenum);

bin/ltlsynt.cc

@@ -26,6 +26,7 @@
 #include "common_setup.hh"
 #include "common_sys.hh"
 #include "common_trans.hh"
+#include "common_ioap.hh"
 
 #include <spot/misc/bddlt.hh>
 #include <spot/misc/escape.hh>
@@ -43,7 +44,6 @@
 #include <spot/twaalgos/product.hh>
 #include <spot/twaalgos/synthesis.hh>
 #include <spot/twaalgos/translate.hh>
-#include <regex>
 
 enum
 {
@@ -178,17 +178,6 @@ Exit status:\n\
   1   if at least one input problem was not realizable\n\
   2   if any error has been reported";
 
-// --ins and --outs, as supplied on the command-line
-static std::optional<std::vector<std::string>> all_output_aps;
-static std::optional<std::vector<std::string>> all_input_aps;
-
-// first, separate the filters that are regular expressions from
-// the others.  Compile the regular expressions while we are at it.
-static std::vector<std::regex> regex_in;
-static std::vector<std::regex> regex_out;
-// map identifier to input/output (false=input, true=output)
-static std::unordered_map<std::string, bool> identifier_map;
-
 static const char* opt_csv = nullptr;
 static bool opt_print_pg = false;
 static bool opt_print_hoa = false;
@@ -323,14 +312,6 @@ namespace
     return opt_print_pg || opt_print_hoa;
   }
 
-  auto str_tolower = [] (std::string s)
-    {
-      std::transform(s.begin(), s.end(), s.begin(),
-                     [](unsigned char c){ return std::tolower(c); });
-      return s;
-    };
-
-
   static void
   dispatch_print_hoa(spot::twa_graph_ptr& game,
                      const spot::realizability_simplifier* rs = nullptr)
@@ -753,108 +734,6 @@ namespace
     return 0;
   }
 
-  static void
-  split_aps(const std::string& arg, std::vector<std::string>& where)
-  {
-    std::istringstream aps(arg);
-    std::string ap;
-    while (std::getline(aps, ap, ','))
-      {
-        ap.erase(remove_if(ap.begin(), ap.end(), isspace), ap.end());
-        where.push_back(str_tolower(ap));
-      }
-  }
-
-  static std::unordered_set<std::string>
-  list_aps_in_formula(spot::formula f)
-  {
-    std::unordered_set<std::string> aps;
-    f.traverse([&aps](spot::formula s) {
-      if (s.is(spot::op::ap))
-        aps.emplace(s.ap_name());
-      return false;
-    });
-    return aps;
-  }
-
-  // Takes a set of the atomic propositions appearing in the formula,
-  // and separate them into two vectors: input APs and output APs.
-  static std::pair<std::vector<std::string>, std::vector<std::string>>
-  filter_list_of_aps(const std::unordered_set<std::string>& aps,
-                     const char* filename, int linenum)
-  {
-    // now iterate over the list of atomic propositions to filter them
-    std::vector<std::string> matched[2]; // 0 = input, 1 = output
-    for (const std::string& a: aps)
-      {
-        if (auto it = identifier_map.find(a); it != identifier_map.end())
-          {
-            matched[it->second].push_back(a);
-            continue;
-          }
-
-        bool found_in = false;
-        for (const std::regex& r: regex_in)
-          if (std::regex_search(a, r))
-            {
-              found_in = true;
-              break;
-            }
-        bool found_out = false;
-        for (const std::regex& r: regex_out)
-          if (std::regex_search(a, r))
-            {
-              found_out = true;
-              break;
-            }
-        if (all_input_aps.has_value() == all_output_aps.has_value())
-          {
-            if (!all_input_aps.has_value())
-              {
-                // If the atomic proposition hasn't been classified
-                // because neither --ins nor --out were specified,
-                // attempt to classify automatically using the first
-                // letter.
-                int fl = a[0];
-                if (fl == 'i' || fl == 'I')
-                  found_in = true;
-                else if (fl == 'o' || fl == 'O')
-                  found_out = true;
-              }
-            if (found_in && found_out)
-              error_at_line(2, 0, filename, linenum,
-                            "'%s' matches both --ins and --outs",
-                            a.c_str());
-            if (!found_in && !found_out)
-              {
-                if (all_input_aps.has_value() || all_output_aps.has_value())
-                  error_at_line(2, 0, filename, linenum,
-                                "one of --ins or --outs should match '%s'",
-                                a.c_str());
-                else
-                  error_at_line(2, 0, filename, linenum,
-                                "since '%s' does not start with 'i' or 'o', "
-                                "it is unclear if it is an input or "
-                                "an output;\n    use --ins or --outs",
-                                a.c_str());
-              }
-          }
-        else
-          {
-            // if we had only --ins or only --outs, anything not
-            // matching was was given is assumed to belong to the
-            // other one.
-            if (!all_input_aps.has_value() && !found_out)
-              found_in = true;
-            else if (!all_output_aps.has_value() && !found_in)
-              found_out = true;
-          }
-        matched[found_out].push_back(a);
-      }
-    return {matched[0], matched[1]};
-  }
-
-
 
   class ltl_processor final : public job_processor
   {
@@ -866,9 +745,8 @@ namespace
     int process_formula(spot::formula f,
                         const char* filename, int linenum) override
     {
-      std::unordered_set<std::string> aps = list_aps_in_formula(f);
       auto [input_aps, output_aps] =
-        filter_list_of_aps(aps, filename, linenum);
+        filter_list_of_aps(f, filename, linenum);
       int res = solve_formula(f, input_aps, output_aps);
       if (opt_csv)
         print_csv(f);
@@ -1193,28 +1071,7 @@ main(int argc, char **argv)
       exit(err);
 
     check_no_formula();
-
+    process_io_options();
-    // Filter identifiers from regexes.
-    if (all_input_aps.has_value())
-      for (const std::string& f: *all_input_aps)
-        {
-          unsigned sz = f.size();
-          if (f[0] == '/' && f[sz - 1] == '/')
-            regex_in.push_back(std::regex(f.substr(1, sz - 2)));
-          else
-            identifier_map.emplace(f, false);
-        }
-    if (all_output_aps.has_value())
-      for (const std::string& f: *all_output_aps)
-        {
-          unsigned sz = f.size();
-          if (f[0] == '/' && f[sz - 1] == '/')
-            regex_out.push_back(std::regex(f.substr(1, sz - 2)));
-          else if (auto [it, is_new] = identifier_map.try_emplace(f, true);
-                   !is_new && !it->second)
-            error(2, 0, "'%s' appears in both --ins and --outs",
-                  f.c_str());
-        }
 
     ltl_processor processor;
     if (int res = processor.run(); res == 0 || res == 1)