Check that reductions are legitimates with containment.

* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh
(are_equivalent): Export this function from the cache.
* src/ltltest/reduc.cc, src/ltltest/equals.cc: Use
are_equivalent() to check that the reductions are legitimate.

src/ltltest/equals.cc

@@ -68,78 +68,92 @@ main(int argc, char** argv)
   if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
     return 2;
 
+  int exit_code;
+
+  {
 #if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM)
-  spot::ltl::formula* tmp;
+    spot::ltl::formula* tmp;
 #endif
 #ifdef LUNABBREV
-  tmp = f1;
+    tmp = f1;
-  f1 = spot::ltl::unabbreviate_logic(f1);
+    f1 = spot::ltl::unabbreviate_logic(f1);
-  tmp->destroy();
+    tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    spot::ltl::dump(std::cout, f1);
-  std::cout << std::endl;
+    std::cout << std::endl;
 #endif
 #ifdef TUNABBREV
-  tmp = f1;
+    tmp = f1;
-  f1 = spot::ltl::unabbreviate_ltl(f1);
+    f1 = spot::ltl::unabbreviate_ltl(f1);
-  tmp->destroy();
+    tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    spot::ltl::dump(std::cout, f1);
-  std::cout << std::endl;
+    std::cout << std::endl;
 #endif
 #ifdef NENOFORM
-  tmp = f1;
+    tmp = f1;
-  f1 = spot::ltl::negative_normal_form(f1);
+    f1 = spot::ltl::negative_normal_form(f1);
-  tmp->destroy();
+    tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    spot::ltl::dump(std::cout, f1);
-  std::cout << std::endl;
+    std::cout << std::endl;
 #endif
 #ifdef REDUC
-  {
     spot::ltl::ltl_simplifier_options opt(true, true, true, false, false);
     spot::ltl::ltl_simplifier simp(opt);
-    spot::ltl::formula* tmp;
+    {
-    tmp = f1;
+      spot::ltl::formula* tmp;
-    f1 = simp.simplify(f1);
+      tmp = f1;
-    tmp->destroy();
+      f1 = simp.simplify(f1);
-  }
+      tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    }
-  std::cout << std::endl;
+    spot::ltl::dump(std::cout, f1);
+    std::cout << std::endl;
 #endif
 #ifdef REDUC_TAU
-  {
     spot::ltl::ltl_simplifier_options opt(false, false, false, true, false);
     spot::ltl::ltl_simplifier simp(opt);
-    spot::ltl::formula* tmp;
+    {
-    tmp = f1;
+      spot::ltl::formula* tmp;
-    f1 = simp.simplify(f1);
+      tmp = f1;
-    tmp->destroy();
+      f1 = simp.simplify(f1);
-  }
+      tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    }
-  std::cout << std::endl;
+    spot::ltl::dump(std::cout, f1);
+    std::cout << std::endl;
 #endif
 #ifdef REDUC_TAUSTR
-  {
     spot::ltl::ltl_simplifier_options opt(false, false, false, true, true);
     spot::ltl::ltl_simplifier simp(opt);
-    spot::ltl::formula* tmp;
+    {
-    tmp = f1;
+      spot::ltl::formula* tmp;
-    f1 = simp.simplify(f1);
+      tmp = f1;
-    tmp->destroy();
+      f1 = simp.simplify(f1);
-  }
+      tmp->destroy();
-  spot::ltl::dump(std::cout, f1);
+    }
-  std::cout << std::endl;
+    spot::ltl::dump(std::cout, f1);
+    std::cout << std::endl;
 #endif
 
-  int exit_code = f1 != f2;
+    exit_code = f1 != f2;
 
-  if (exit_code)
+#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
-    {
+    spot::ltl::ltl_simplifier simp;
-      spot::ltl::dump(std::cerr, f1) << std::endl;
+#endif
-      spot::ltl::dump(std::cerr, f2) << std::endl;
-    }
 
-  f1->destroy();
+    if (!simp.are_equivalent(f1, f2))
-  f2->destroy();
+      {
+	std::cerr << "Source and destination formulae are not equivalent!"
+		  << std::endl;
+	exit_code = 1;
+      }
 
+    if (exit_code)
+      {
+	spot::ltl::dump(std::cerr, f1) << std::endl;
+	spot::ltl::dump(std::cerr, f2) << std::endl;
+      }
+
+    f1->destroy();
+    f2->destroy();
+  }
   spot::ltl::atomic_prop::dump_instances(std::cerr);
   spot::ltl::unop::dump_instances(std::cerr);
   spot::ltl::binop::dump_instances(std::cerr);

src/ltltest/reduc.cc

@@ -210,6 +210,15 @@ main(int argc, char** argv)
 
     ftmp1 = f1;
     f1 = simp->simplify(f1);
+
+    if (!simp->are_equivalent(ftmp1, f1))
+      {
+	std::cerr << "Incorrect reduction from `" << f1s_before
+		  << "' to `" << spot::ltl::to_string(f1) << "'."
+		  << std::endl;
+	exit_code = 3;
+      }
+
     ftmp1->destroy();
 
     int length_f1_after = spot::ltl::length(f1);
@@ -229,11 +238,11 @@ main(int argc, char** argv)
 
     // If -h is set, we want to print only formulae that have become larger.
     if (!f2 && (!hidereduc || (length_f1_after > length_f1_before)))
-    {
+      {
 	std::cout << length_f1_before << " " << length_f1_after
 		  << " '" << f1s_before << "' reduce to '" << f1s_after << "'"
 		  << std::endl;
-    }
+      }
 
     if (f2)
       {
@@ -284,10 +293,16 @@ main(int argc, char** argv)
       delete fin;
     }
 
+  spot::ltl::atomic_prop::dump_instances(std::cerr);
+  spot::ltl::unop::dump_instances(std::cerr);
+  spot::ltl::binop::dump_instances(std::cerr);
+  spot::ltl::multop::dump_instances(std::cerr);
+  spot::ltl::automatop::dump_instances(std::cerr);
   assert(spot::ltl::atomic_prop::instance_count() == 0);
   assert(spot::ltl::unop::instance_count() == 0);
   assert(spot::ltl::binop::instance_count() == 0);
   assert(spot::ltl::multop::instance_count() == 0);
+  assert(spot::ltl::automatop::instance_count() == 0);
 
   return exit_code;
 }

src/ltlvisit/simplify.cc

@@ -244,7 +244,8 @@ namespace spot
       // If right==false, true if !f1 => f2, false otherwise.
       // If right==true, true if f1 => !f2, false otherwise.
       bool
-      syntactic_implication_neg(const formula* f1, const formula* f2, bool right);
+      syntactic_implication_neg(const formula* f1, const formula* f2,
+				bool right);
 
       // Return true if f1 => !f2
       bool contained_neg(const formula* f1, const formula* f2)
@@ -2862,11 +2863,17 @@ namespace spot
     }
 
     bool
-    ltl_simplifier::syntactic_implication_neg(const formula* f1, const formula* f2,
+    ltl_simplifier::syntactic_implication_neg(const formula* f1,
-					      bool right)
+					      const formula* f2, bool right)
     {
       return cache_->syntactic_implication_neg(f1, f2, right);
     }
 
+    bool
+    ltl_simplifier::are_equivalent(const formula* f, const formula* g)
+    {
+      return cache_->lcc.equal(f, g);
+    }
+
   }
 }

src/ltlvisit/simplify.hh

@@ -70,7 +70,8 @@ namespace spot
       ltl_simplifier(ltl_simplifier_options& opt);
       ~ltl_simplifier();
 
-      /// Simplify the formula \a f (using options supplied to the constructor).
+      /// Simplify the formula \a f (using options supplied to the
+      /// constructor).
       formula* simplify(const formula* f);
 
       /// Build the negative normal form of formula \a f.
@@ -108,7 +109,15 @@ namespace spot
       /// If \a right is true, this method returns whether
       /// \a f implies !\a g.  If \a right is false, this returns
       /// whether !\a g implies \a g.
-      bool syntactic_implication_neg(const formula* f, const formula* g, bool right);
+      bool syntactic_implication_neg(const formula* f, const formula* g,
+				     bool right);
+
+      /// \brief check whether two formulae are equivalent.
+      ///
+      /// This costly check performs up to four translations,
+      /// two products, and two emptiness checks.
+      bool are_equivalent(const formula* f, const formula* g);
+
 
     private:
       ltl_simplifier_cache* cache_;