Move the remaining reduce() logic into ltl_simplifier.

* src/ltlvisit/simplify.hh
(ltl_simplifier::negative_normal_form): Allow logical
unabbreviations during the NNF pass.
* src/ltlvisit/simplify.cc
(ltl_simplifier::negative_normal_form)
(negative_normal_form_visitor): Adjust.
(ltl_simplifier::simplify): Request unabbreviations.
* src/ltlvisit/reduce.cc (reduce): Remove most
of the code, leaving only a call ltl_simplifier
and some wrapper code to convert options.
* src/ltltest/reduccmp.test: Add more test cases.

src/ltltest/reduccmp.test

@@ -66,6 +66,11 @@ for x in ../reduccmp ../reductaustr; do
   run 0 $x 'a | (b U a) | a' '(b U a)'
   run 0 $x 'a U (b U a)' '(b U a)'
 
+  run 0 $x 'a <-> !a' '0'
+  run 0 $x 'a <-> a' '1'
+  run 0 $x 'a ^ a' '0'
+  run 0 $x 'a ^ !a' '1'
+
   # Basic reductions
   run 0 $x 'X(true)' 'true'
   run 0 $x 'X(false)' 'false'
@@ -121,6 +126,8 @@ for x in ../reduccmp ../reductaustr; do
      run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
      run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
 
+     run 0 $x 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)'
+
      run 0 $x 'Gb W a' 'Gb|a'
      run 0 $x 'Fb M Fa' 'Fa & Fb'
 

src/ltlvisit/reduce.cc

@@ -22,25 +22,16 @@
 // 02111-1307, USA.
 
 #include "reduce.hh"
-#include "ltlast/allnodes.hh"
 #include <cassert>
-
-#include "lunabbrev.hh"
-#include "simpfg.hh"
 #include "simplify.hh"
 
 namespace spot
 {
   namespace ltl
   {
-
     formula*
     reduce(const formula* f, int opt)
     {
-      formula* f1;
-      formula* f2;
-      formula* prev = 0;
-
       ltl_simplifier_options o;
       o.reduce_basics = opt & Reduce_Basics;
       o.synt_impl = opt & Reduce_Syntactic_Implications;
@@ -48,31 +39,7 @@ namespace spot
       o.containment_checks = opt & Reduce_Containment_Checks;
       o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger;
       ltl_simplifier simplifier(o);
-
+      return const_cast<formula*>(simplifier.simplify(f));
-      int n = 0;
-
-      while (f != prev)
-	{
-	  ++n;
-	  assert(n < 100);
-	  if (prev)
-	    {
-	      prev->destroy();
-	      prev = const_cast<formula*>(f);
-	    }
-	  else
-	    {
-	      prev = f->clone();
-	    }
-	  f1 = unabbreviate_logic(f);
-	  f2 = simplify_f_g(f1);
-	  f1->destroy();
-	  f = simplifier.simplify(f2);
-	  f2->destroy();
-	}
-      prev->destroy();
-
-      return const_cast<formula*>(f);
     }
 
     bool

src/ltlvisit/simplify.cc

@@ -365,13 +365,15 @@ namespace spot
       const formula*
       nenoform_recursively(const formula* f,
 			   bool negated,
+			   bool lunabbrev,
 			   ltl_simplifier_cache* c);
 
       class negative_normal_form_visitor: public visitor
       {
       public:
-	negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c)
+	negative_normal_form_visitor(bool negated, bool lunabbrev,
-	  : negated_(negated), cache_(c)
+				     ltl_simplifier_cache* c)
+	  : negated_(negated), lunabbrev_(lunabbrev), cache_(c)
 	{
 	}
 
@@ -455,13 +457,41 @@ namespace spot
 	void
 	visit(bunop* bo)
 	{
-	  // !(a*) is not simplified
+	  // !(a*) is not simplified, whatever that means
 	  result_ = bunop::instance(bo->op(), recurse_(bo->child(), false),
 				    bo->min(), bo->max());
 	  if (negated_)
 	    result_ = unop::instance(unop::Not, result_);
 	}
 
+	formula* equiv_or_xor(bool equiv, formula* f1, formula* f2)
+	{
+	  if (!lunabbrev_)
+	    return binop::instance(equiv ? binop::Equiv : binop::Xor,
+				   recurse_(f1, false),
+				   recurse_(f2, false));
+	  // Rewrite a<=>b as (a&b)|(!a&!b)
+	  if (equiv)
+	    return
+	      multop::instance(multop::Or,
+			       multop::instance(multop::And,
+						recurse_(f1, false),
+						recurse_(f2, false)),
+			       multop::instance(multop::And,
+						recurse_(f1, true),
+						recurse_(f2, true)));
+	  else
+	    // Rewrite a^b as (a&!b)|(!a&b)
+	    return
+	      multop::instance(multop::Or,
+			       multop::instance(multop::And,
+						recurse_(f1, false),
+						recurse_(f2, true)),
+			       multop::instance(multop::And,
+						recurse_(f1, true),
+						recurse_(f2, false)));
+	}
+
 	void
 	visit(binop* bo)
 	{
@@ -470,68 +500,69 @@ namespace spot
 	  switch (bo->op())
 	    {
 	    case binop::Xor:
-	      /* !(a ^ b) == a <=> b */
+	      // !(a ^ b) == a <=> b
-	      result_ = binop::instance(negated_ ? binop::Equiv : binop::Xor,
+	      result_ = equiv_or_xor(negated_, f1, f2);
-					recurse_(f1, false),
-					recurse_(f2, false));
 	      return;
 	    case binop::Equiv:
-	      /* !(a <=> b) == a ^ b */
+	      // !(a <=> b) == a ^ b
-	      result_ = binop::instance(negated_ ? binop::Xor : binop::Equiv,
+	      result_ = equiv_or_xor(!negated_, f1, f2);
-					recurse_(f1, false),
-					recurse_(f2, false));
 	      return;
 	    case binop::Implies:
 	      if (negated_)
-		/* !(a => b) == a & !b */
+		// !(a => b) == a & !b
 		result_ = multop::instance(multop::And,
 					   recurse_(f1, false),
 					   recurse_(f2, true));
-	      else
+	      else if (!lunabbrev_)
 		result_ = binop::instance(binop::Implies,
-					  recurse(f1), recurse(f2));
+					  recurse_(f1, false),
+					  recurse_(f2, false));
+	      else // a => b == !a | b
+		result_ = multop::instance(multop::Or,
+					   recurse_(f1, true),
+					   recurse_(f2, false));
 	      return;
 	    case binop::U:
-	      /* !(a U b) == !a R !b */
+	      // !(a U b) == !a R !b
 	      result_ = binop::instance(negated_ ? binop::R : binop::U,
 					recurse(f1), recurse(f2));
 	      return;
 	    case binop::R:
-	      /* !(a R b) == !a U !b */
+	      // !(a R b) == !a U !b
 	      result_ = binop::instance(negated_ ? binop::U : binop::R,
 					recurse(f1), recurse(f2));
 	      return;
 	    case binop::W:
-	      /* !(a W b) == !a M !b */
+	      // !(a W b) == !a M !b
 	      result_ = binop::instance(negated_ ? binop::M : binop::W,
 					recurse(f1), recurse(f2));
 	      return;
 	    case binop::M:
-	      /* !(a M b) == !a W !b */
+	      // !(a M b) == !a W !b
 	      result_ = binop::instance(negated_ ? binop::W : binop::M,
 					recurse(f1), recurse(f2));
 	      return;
 	    case binop::UConcat:
-	      /* !(a []-> b) == a<>-> !b */
+	      // !(a []-> b) == a<>-> !b
 	      result_ = binop::instance(negated_ ?
 					binop::EConcat : binop::UConcat,
 					recurse_(f1, false), recurse(f2));
 	      return;
 	    case binop::EConcat:
-	      /* !(a <>-> b) == a[]-> !b */
+	      // !(a <>-> b) == a[]-> !b
 	      result_ = binop::instance(negated_ ?
 					binop::UConcat : binop::EConcat,
 					recurse_(f1, false), recurse(f2));
 	      return;
 	    case binop::EConcatMarked:
-	      /* !(a <>-> b) == a[]-> !b */
+	      // !(a <>-> b) == a[]-> !b
 	      result_ = binop::instance(negated_ ?
 					binop::UConcat :
 					binop::EConcatMarked,
 					recurse_(f1, false), recurse(f2));
 	      return;
 	    }
-	  /* Unreachable code.  */
+	  // Unreachable code.
 	  assert(0);
 	}
 
@@ -594,7 +625,9 @@ namespace spot
 	formula*
 	recurse_(formula* f, bool negated)
 	{
-	  return const_cast<formula*>(nenoform_recursively(f, negated, cache_));
+	  return
+	    const_cast<formula*>(nenoform_recursively(f, negated,
+						      lunabbrev_, cache_));
 	}
 
 	formula*
@@ -606,6 +639,7 @@ namespace spot
       protected:
 	formula* result_;
 	bool negated_;
+	bool lunabbrev_;
 	ltl_simplifier_cache* cache_;
       };
 
@@ -613,6 +647,7 @@ namespace spot
       const formula*
       nenoform_recursively(const formula* f,
 			   bool negated,
+			   bool lunabbrev,
 			   ltl_simplifier_cache* c)
       {
 	if (f->kind() == formula::UnOp)
@@ -639,7 +674,7 @@ namespace spot
 	  }
 	else
 	  {
-	    negative_normal_form_visitor v(negated, c);
+	    negative_normal_form_visitor v(negated, lunabbrev, c);
 	    const_cast<formula*>(f)->accept(v);
 	    result = v.result();
 	  }
@@ -2242,7 +2277,7 @@ namespace spot
     {
       formula* neno = 0;
       if (!f->is_in_nenoform())
-	f = neno = negative_normal_form(f);
+	f = neno = negative_normal_form(f, false, true);
       formula* res = const_cast<formula*>(simplify_recursively(f, cache_));
       if (neno)
 	neno->destroy();
@@ -2250,9 +2285,11 @@ namespace spot
     }
 
     formula*
-    ltl_simplifier::negative_normal_form(const formula* f, bool negated)
+    ltl_simplifier::negative_normal_form(const formula* f, bool negated,
+					 bool lunabbrev)
     {
-      return const_cast<formula*>(nenoform_recursively(f, negated, cache_));
+      return const_cast<formula*>(nenoform_recursively(f, negated, lunabbrev,
+						       cache_));
     }
 
 

src/ltlvisit/simplify.hh

@@ -80,13 +80,11 @@ namespace spot
       /// \param f The formula to normalize.
       /// \param negated If \c true, return the negative normal form of
       ///        \c !f
-      ///
+      /// \param lunabbrev If \c true, also remove Xor, Equiv, and Implies
-      /// Note that this will not remove abbreviated operators.  If you
+      ///        operators.  (It is faster than calling
-      /// want to remove abbreviations, call spot::ltl::unabbreviate_logic
+      ///        spot::ltl::unabbreviate_ltl first.)
-      /// or spot::ltl::unabbreviate_ltl first.  (Calling these functions
+      formula* negative_normal_form(const formula* f, bool negated = false,
-      /// after spot::ltl::negative_normal_form would likely produce a
+				    bool lunabbrev = false);
-      /// formula which is not in negative normal form.)
-      formula* negative_normal_form(const formula* f, bool negated = false);
 
 
     private: