randltl: add option to simplify formulas

* src/bin/common_r.cc, src/bin/common_r.hh: New files, extracted from...
* src/bin/ltlfilt.cc: Here.
* src/bin/randltl.cc: Use them.
* src/bin/Makefile.am: Adjust.

src/bin/Makefile.am

@@ -28,8 +28,8 @@ LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a
 
 bin_PROGRAMS = ltlfilt genltl randltl
 
-noinst_HEADERS = common_output.hh common_range.hh
+noinst_HEADERS = common_output.hh common_range.hh common_r.hh
 
-ltlfilt_SOURCES = ltlfilt.cc common_output.cc
+ltlfilt_SOURCES = ltlfilt.cc common_output.cc common_r.cc
 genltl_SOURCES = genltl.cc common_output.cc common_range.cc
-randltl_SOURCES = randltl.cc common_output.cc common_range.cc
+randltl_SOURCES = randltl.cc common_output.cc common_range.cc common_r.cc

src/bin/common_r.cc

@@ -0,0 +1,69 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifdef HAVE_CONFIG_H
+# include "config.h"
+#endif
+
+#include "error.h"
+
+#include "common_r.hh"
+
+int simplification_level = 0;
+
+void
+parse_r(const char* arg)
+{
+  if (!arg)
+    {
+      simplification_level = 3;
+      return;
+    }
+  if (arg[1] == 0 && arg[0] >= '0' && arg[0] <= '3')
+    {
+      simplification_level = arg[0] - '0';
+      return;
+    }
+  error(2, 0, "invalid simplification level '%s'",  arg);
+}
+
+spot::ltl::ltl_simplifier_options
+simplifier_options()
+{
+  spot::ltl::ltl_simplifier_options options;
+  switch (simplification_level)
+    {
+    case 3:
+      options.containment_checks = true;
+      options.containment_checks_stronger = true;
+      // fall through
+    case 2:
+      options.synt_impl = true;
+      // fall through
+    case 1:
+      options.reduce_basics = true;
+      options.event_univ = true;
+      // fall through
+    default:
+      break;
+    }
+  return options;
+}

src/bin/common_r.hh

@@ -0,0 +1,50 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012 Laboratoire de Recherche et Développement de
+// l'Epita (LRDE).
+//
+// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_BIN_COMMON_R_HH
+#define SPOT_BIN_COMMON_R_HH
+
+#include "ltlvisit/simplify.hh"
+
+#define OPT_R 'r'
+
+#define DECLARE_OPT_R							\
+    { "simplify", OPT_R, "LEVEL", OPTION_ARG_OPTIONAL,			\
+      "simplify formulas according to LEVEL (see below); LEVEL is "	\
+      "set to 3 if omitted", 0 }
+
+#define LEVEL_DOC(g)							\
+    { 0, 0, 0, 0, "The simplification LEVEL may be set as follows.", g }, \
+    { "  0", 0, 0, OPTION_DOC | OPTION_NO_USAGE,			\
+      "No rewriting", 0 },						\
+    { "  1", 0, 0, OPTION_DOC | OPTION_NO_USAGE,			\
+      "basic rewritings and eventual/universal rules", 0 },		\
+    { "  2", 0, 0, OPTION_DOC | OPTION_NO_USAGE,			\
+      "additional syntactic implication rules", 0 },			\
+    { "  3", 0, 0, OPTION_DOC | OPTION_NO_USAGE,			\
+      "better implications using containment", 0 }
+
+extern int simplification_level;
+
+void parse_r(const char* arg);
+spot::ltl::ltl_simplifier_options simplifier_options();
+
+#endif // SPOT_BIN_COMMON_RANGE_HH

src/bin/ltlfilt.cc

@@ -33,6 +33,7 @@
 #include "error.h"
 
 #include "common_output.hh"
+#include "common_r.hh"
 
 #include "misc/_config.h"
 #include "misc/hash.hh"
@@ -104,17 +105,8 @@ static const argp_option options[] =
     { 0, 0, 0, 0, "Transformation options:", 3 },
     { "negate", 'n', 0, 0, "negate each formula", 0 },
     { "nnf", OPT_NNF, 0, 0, "rewrite formulas in negative normal form", 0 },
-    { "simplify", 'r', "LEVEL", OPTION_ARG_OPTIONAL,
+    DECLARE_OPT_R,
-      "simplify formulas according to LEVEL (see below)", 0 },
+    LEVEL_DOC(4),
-    { 0, 0, 0, 0, "  The simplification LEVEL might be one of:", 4 },
-    { "  0", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
-      "No rewriting", 0 },
-    { "  1", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
-      "basic rewritings and eventual/universal rules", 0 },
-    { "  2", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
-      "additional syntactic implication rules", 0 },
-    { "  3", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
-      "better implications using containment (default)", 0 },
     /**************************************************/
     { 0, 0, 0, 0,
       "Filtering options (matching is done after transformation):", 5 },
@@ -190,7 +182,6 @@ static error_style_t error_style = drop_errors;
 static bool quiet = false;
 static bool nnf = false;
 static bool negate = false;
-static int level = 0;
 static bool unique = false;
 static bool psl = false;
 static bool ltl = false;
@@ -257,26 +248,8 @@ parse_opt(int key, char* arg, struct argp_state*)
     case 'q':
       quiet = true;
       break;
-    case 'r':
+    case OPT_R:
-      if (!arg)
+      parse_r(arg);
-	{
-	  level = 3;
-	  break;
-	}
-      else
-	{
-	  if (arg[1] == 0)
-	    switch (arg[0])
-	      {
-	      case '0':
-	      case '1':
-	      case '2':
-	      case '3':
-		level = arg[0] = '0';
-		return 0;
-	      }
-	  error(2, 0, "invalid simplification level '%s'",  arg);
-	}
       break;
     case 'u':
       unique = true;
@@ -419,7 +392,7 @@ namespace
       if (negate)
 	f = spot::ltl::unop::instance(spot::ltl::unop::Not, f);
 
-      if (level)
+      if (simplification_level)
 	{
 	  const spot::ltl::formula* res = simpl.simplify(f);
 	  f->destroy();
@@ -538,26 +511,7 @@ namespace
 static int
 run_jobs()
 {
-  spot::ltl::ltl_simplifier_options options;
+  spot::ltl::ltl_simplifier simpl(simplifier_options());
-
-  switch (level)
-    {
-    case 3:
-      options.containment_checks = true;
-      options.containment_checks_stronger = true;
-      // fall through
-    case 2:
-      options.synt_impl = true;
-      // fall through
-    case 1:
-      options.reduce_basics = true;
-      options.event_univ = true;
-      // fall through
-    default:
-      break;
-    }
-
-  spot::ltl::ltl_simplifier simpl(options);
   ltl_processor processor(simpl);
 
   int error = 0;

src/bin/randltl.cc

@@ -32,6 +32,7 @@
 
 #include "common_output.hh"
 #include "common_range.hh"
+#include "common_r.hh"
 
 #include "misc/_config.h"
 #include <sstream>
@@ -95,9 +96,11 @@ static const argp_option options[] =
       "tree size of the formulas generated, before mandatory "\
       "trivial simplifications (15)", 0 },
     { "unique", 'u', 0, 0, "do not generate duplicate formulas", 0 },
+    DECLARE_OPT_R,
     RANGE_DOC,
+    LEVEL_DOC(3),
     /**************************************************/
-    { 0, 0, 0, 0, "Adjusting probabilities:", 3 },
+    { 0, 0, 0, 0, "Adjusting probabilities:", 4 },
     { "dump-priorities", OPT_DUMP_PRIORITIES, 0, 0,
       "show current priorities, do not generate any formula", 0 },
     { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0,
@@ -162,6 +165,9 @@ parse_opt(int key, char* arg, struct argp_state*)
     case 'P':
       output = OutputPSL;
       break;
+    case OPT_R:
+      parse_r(arg);
+      break;
     case 'S':
       output = OutputSERE;
       break;
@@ -304,6 +310,8 @@ main(int argc, char** argv)
 
   fset_t unique_set;
 
+  spot::ltl::ltl_simplifier simpl(simplifier_options());
+
   while (opt_formulas < 0 || opt_formulas--)
     {
 #define MAX_TRIALS 100000
@@ -318,6 +326,12 @@ main(int argc, char** argv)
 	  if (size != opt_tree_size.max)
 	    size = spot::rrand(size, opt_tree_size.max);
 	  f = rf->generate(size);
+	  if (simplification_level)
+	    {
+	      const spot::ltl::formula* tmp = simpl.simplify(f);
+	      f->destroy();
+	      f = tmp;
+	    }
 	  if (opt_unique)
 	    {
 	      if (unique_set.insert(f).second)