// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Developpement 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 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 <iostream>
//#define TRACE
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif

#include "simplify.hh"
#include <unordered_map>
#include "ltlvisit/contain.hh"
#include "ltlvisit/print.hh"
#include "ltlvisit/snf.hh"
#include "twa/formula2bdd.hh"
#include <cassert>
#include <memory>

namespace spot
{
  namespace ltl
  {
    typedef std::vector<formula> vec;

    // The name of this class is public, but not its contents.
    class ltl_simplifier_cache
    {
      typedef std::unordered_map<formula, formula> f2f_map;
      typedef std::unordered_map<formula, bdd> f2b_map;
      typedef std::pair<formula, formula> pairf;
      typedef std::map<pairf, bool> syntimpl_cache_t;
    public:
      bdd_dict_ptr dict;
      ltl_simplifier_options options;
      language_containment_checker lcc;

      ~ltl_simplifier_cache()
      {
	dict->unregister_all_my_variables(this);
      }

      ltl_simplifier_cache(const bdd_dict_ptr& d)
	: dict(d), lcc(d, true, true, false, false)
      {
      }

      ltl_simplifier_cache(const bdd_dict_ptr& d,
			   const ltl_simplifier_options& opt)
	: dict(d), options(opt), lcc(d, true, true, false, false)
      {
	options.containment_checks |= options.containment_checks_stronger;
	options.event_univ |= options.favor_event_univ;
      }

      void
      print_stats(std::ostream& os) const
      {
	os << "simplified formulae:    " << simplified_.size() << " entries\n"
	   << "negative normal form:   " << nenoform_.size() << " entries\n"
	   << "syntactic implications: " << syntimpl_.size() << " entries\n"
	   << "boolean to bdd:         " << as_bdd_.size() << " entries\n"
	   << "star normal form:       " << snf_cache_.size() << " entries\n"
	   << "boolean isop:           " << bool_isop_.size() << " entries\n";
      }

      void
      clear_as_bdd_cache()
      {
	as_bdd_.clear();
      }

      // Convert a Boolean formula into a BDD for easier comparison.
      bdd
      as_bdd(formula f)
      {
	// Lookup the result in case it has already been computed.
	f2b_map::const_iterator it = as_bdd_.find(f);
	if (it != as_bdd_.end())
	  return it->second;

	bdd result = bddfalse;

	switch (f.kind())
	  {
	  case op::True:
	    result = bddtrue;
	    break;
	  case op::False:
	    result = bddfalse;
	    break;
	  case op::AP:
	    result = bdd_ithvar(dict->register_proposition(f, this));
	    break;
	  case op::Not:
	    result = !as_bdd(f.nth(0));
	    break;
	  case op::Xor:
	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_xor);
	    break;
	  case op::Implies:
	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_imp);
	    break;
	  case op::Equiv:
	    result = bdd_apply(as_bdd(f.nth(0)), as_bdd(f.nth(1)), bddop_biimp);
	    break;
	  case op::And:
	    {
	      result = bddtrue;
	      for (auto c: f)
		result &= as_bdd(c);
	      break;
	    }
	  case op::Or:
	    {
	      result = bddfalse;
	      for (auto c: f)
		result |= as_bdd(c);
	      break;
	    }
	  default:
	    SPOT_UNIMPLEMENTED();
	  }

	// Cache the result before returning.
	as_bdd_[f] = result;
	return result;
      }

      formula
      lookup_nenoform(formula f)
      {
	f2f_map::const_iterator i = nenoform_.find(f);
	if (i == nenoform_.end())
	  return nullptr;
	return i->second;
      }

      void
      cache_nenoform(formula orig, formula nenoform)
      {
	nenoform_[orig] = nenoform;
      }

      // Return true iff the option set (syntactic implication
      // or containment checks) allow to prove that f1 => f2.
      bool
      implication(formula f1, formula f2)
      {
	trace << "[->] does " << str_psl(f1) << " implies "
	      << str_psl(f2) << " ?" << std::endl;
	if ((options.synt_impl && syntactic_implication(f1, f2))
	    || (options.containment_checks && contained(f1, f2)))
	  {
	    trace << "[->] Yes" << std::endl;
	    return true;
	  }
	trace << "[->] No" << std::endl;
	return false;
      }

      // Return true if f1 => f2 syntactically
      bool
      syntactic_implication(formula f1, formula f2);
      bool
      syntactic_implication_aux(formula f1, formula f2);

      // Return true if f1 => f2
      bool
      contained(formula f1, formula f2)
      {
	if (!f1.is_psl_formula() || !f2.is_psl_formula())
	  return false;
	return lcc.contained(f1, f2);
      }

      // If right==false, true if !f1 => f2, false otherwise.
      // If right==true, true if f1 => !f2, false otherwise.
      bool
      syntactic_implication_neg(formula f1, formula f2,
				bool right);

      // Return true if f1 => !f2
      bool contained_neg(formula f1, formula f2)
      {
	if (!f1.is_psl_formula() || !f2.is_psl_formula())
	  return false;
	trace << "[CN] Does (" << str_psl(f1) << ") implies !("
	      << str_psl(f2) << ") ?" << std::endl;
	if (lcc.contained_neg(f1, f2))
	  {
	    trace << "[CN] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[CN] No" << std::endl;
	    return false;
	  }
      }

      // Return true if f1 => !f2
      bool neg_contained(formula f1, formula f2)
      {
	if (!f1.is_psl_formula() || !f2.is_psl_formula())
	  return false;
	trace << "[NC] Does (" << str_psl(f1) << ") implies !("
	      << str_psl(f2) << ") ?" << std::endl;
	if (lcc.neg_contained(f1, f2))
	  {
	    trace << "[NC] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[NC] No" << std::endl;
	    return false;
	  }
      }

      // Return true iff the option set (syntactic implication
      // or containment checks) allow to prove that
      //   - !f1 => f2   (case where right=false)
      //   - f1 => !f2   (case where right=true)
      bool
      implication_neg(formula f1, formula f2, bool right)
      {
	trace << "[IN] Does " << (right ? "(" : "!(")
	      << str_psl(f1) << ") implies "
	      << (right ? "!(" : "(") << str_psl(f2) << ") ?"
	      << std::endl;
	if ((options.synt_impl && syntactic_implication_neg(f1, f2, right))
	    || (options.containment_checks && right && contained_neg(f1, f2))
	    || (options.containment_checks && !right && neg_contained(f1, f2)))
	  {
	    trace << "[IN] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[IN] No" << std::endl;
	    return false;
	  }
      }

      formula
      lookup_simplified(formula f)
      {
	f2f_map::const_iterator i = simplified_.find(f);
	if (i == simplified_.end())
	  return nullptr;
	return i->second;
      }

      void
      cache_simplified(formula orig, formula simplified)
      {
	simplified_[orig] = simplified;
      }

      formula
      star_normal_form(formula f)
      {
	return ltl::star_normal_form(f, &snf_cache_);
      }

      formula
      star_normal_form_bounded(formula f)
      {
	return ltl::star_normal_form_bounded(f, &snfb_cache_);
      }


      formula
      boolean_to_isop(formula f)
      {
	f2f_map::const_iterator it = bool_isop_.find(f);
	if (it != bool_isop_.end())
	  return it->second;

	assert(f.is_boolean());
	formula res = bdd_to_formula(as_bdd(f), dict);
	bool_isop_[f] = res;
	return res;
      }

    private:
      f2b_map as_bdd_;
      f2f_map simplified_;
      f2f_map nenoform_;
      syntimpl_cache_t syntimpl_;
      snf_cache snf_cache_;
      snf_cache snfb_cache_;
      f2f_map bool_isop_;
    };


    namespace
    {
      //////////////////////////////////////////////////////////////////////
      //
      //  NEGATIVE_NORMAL_FORM
      //
      //////////////////////////////////////////////////////////////////////

      formula
      nenoform_rec(formula f, bool negated, ltl_simplifier_cache* c);

      formula equiv_or_xor(bool equiv, formula f1, formula f2,
			   ltl_simplifier_cache* c)
      {
	auto rec = [c](formula f, bool negated)
	  {
	    return nenoform_rec(f, negated, c);
	  };

	if (equiv)
	  {
	    // Rewrite a<=>b as (a&b)|(!a&!b)
	    auto recurse_f1_true = rec(f1, true);
	    auto recurse_f1_false = rec(f1, false);
	    auto recurse_f2_true = rec(f2, true);
	    auto recurse_f2_false = rec(f2, false);
	    auto left = formula::And({recurse_f1_false, recurse_f2_false});
	    auto right = formula::And({recurse_f1_true, recurse_f2_true});
	    return formula::Or({left, right});
	  }
	else
	  {
	    // Rewrite a^b as (a&!b)|(!a&b)
	    auto recurse_f1_true = rec(f1, true);
	    auto recurse_f1_false = rec(f1, false);
	    auto recurse_f2_true = rec(f2, true);
	    auto recurse_f2_false = rec(f2, false);
	    auto left = formula::And({recurse_f1_false, recurse_f2_true});
	    auto right = formula::And({recurse_f1_true, recurse_f2_false});
	    return formula::Or({left, right});
	  }
      }

      formula
      nenoform_rec(formula f, bool negated, ltl_simplifier_cache* c)
      {
	if (f.is(op::Not))
	  {
	    negated = !negated;
	    f = f.nth(0);
	  }

	formula key = f;
	if (negated)
	  key = formula::Not(f);
	formula result = c->lookup_nenoform(key);
	if (result)
	  return result;

	if (key.is_in_nenoform()
	    || (c->options.nenoform_stop_on_boolean && key.is_boolean()))
	  {
	    result = key;
	  }
	else
	  {
	    auto rec = [c](formula f, bool neg)
	      {
		return nenoform_rec(f, neg, c);
	      };

	    switch (op o = f.kind())
	      {
	      case op::False:
	      case op::True:
		// Negation of constants is taken care of in the
		// constructor of unop::Not, so these cases should be
		// caught by nenoform_recursively().
		assert(!negated);
		result = f;
		break;
	      case op::AP:
		result = negated ? formula::Not(f) : f;
		break;
	      case op::X:
		// !Xa == X!a
		result = formula::X(rec(f.nth(0), negated));
		break;
	      case op::F:
		// !Fa == G!a
		result = formula::unop(negated ? op::G : op::F,
				       rec(f.nth(0), negated));
		break;
	      case op::G:
		// !Ga == F!a
		result = formula::unop(negated ? op::F : op::G,
				       rec(f.nth(0), negated));
		break;
	      case op::Closure:
		result = formula::unop(negated ?
				       op::NegClosure : op::Closure,
				       rec(f.nth(0), false));
		break;
	      case op::NegClosure:
	      case op::NegClosureMarked:
		result = formula::unop(negated ? op::Closure : o,
				       rec(f.nth(0), false));
		break;

	      case op::Implies:
		if (negated)
		  // !(a => b) == a & !b
		  {
		    auto f2 = rec(f.nth(1), true);
		    result = formula::And({rec(f.nth(0), false), f2});
		  }
		else // a => b == !a | b
		  {
		    auto f2 = rec(f.nth(1), false);
		    result = formula::Or({rec(f.nth(0), true), f2});
		  }
		break;
	      case op::Xor:
		{
		  // !(a ^ b) == a <=> b
		  result = equiv_or_xor(negated, f.nth(0), f.nth(1), c);
		  break;
		}
	      case op::Equiv:
		{
		  // !(a <=> b) == a ^ b
		  result = equiv_or_xor(!negated, f.nth(0), f.nth(1), c);
		  break;
		}
	      case op::U:
		{
		  // !(a U b) == !a R !b
		  auto f1 = rec(f.nth(0), negated);
		  auto f2 = rec(f.nth(1), negated);
		  result = formula::binop(negated ? op::R : op::U, f1, f2);
		  break;
		}
	      case op::R:
		{
		  // !(a R b) == !a U !b
		  auto f1 = rec(f.nth(0), negated);
		  auto f2 = rec(f.nth(1), negated);
		  result = formula::binop(negated ? op::U : op::R, f1, f2);
		  break;
		}
	      case op::W:
		{
		  // !(a W b) == !a M !b
		  auto f1 = rec(f.nth(0), negated);
		  auto f2 = rec(f.nth(1), negated);
		  result = formula::binop(negated ? op::M : op::W, f1, f2);
		  break;
		}
	      case op::M:
		{
		  // !(a M b) == !a W !b
		  auto f1 = rec(f.nth(0), negated);
		  auto f2 = rec(f.nth(1), negated);
		  result = formula::binop(negated ? op::W : op::M, f1, f2);
		  break;
		}
	      case op::Or:
	      case op::And:
		{
		  unsigned mos = f.size();
		  vec v;
		  for (unsigned i = 0; i < mos; ++i)
		    v.push_back(rec(f.nth(i), negated));
		  op on = o;
		  if (negated)
		    on = o == op::Or ? op::And : op::Or;
		  result = formula::multop(on, v);
		  break;
		}
	      case op::OrRat:
	      case op::AndRat:
	      case op::AndNLM:
	      case op::Concat:
	      case op::Fusion:
	      case op::Star:
	      case op::FStar:
		// !(a*) etc. should never occur.
		{
		  assert(!negated);
		  result = f.map([c](formula f)
				 {
				   return nenoform_rec(f, false, c);
				 });
		  break;
		}
	      case op::EConcat:
	      case op::EConcatMarked:
		{
		  // !(a <>-> b) == a[]-> !b
		  auto f1 = f.nth(0);
		  auto f2 = f.nth(1);
		  result = formula::binop(negated ? op::UConcat : o,
					  rec(f1, false), rec(f2, negated));
		  break;
		}
	      case op::UConcat:
		{
		  // !(a []-> b) == a<>-> !b
		  auto f1 = f.nth(0);
		  auto f2 = f.nth(1);
		  result = formula::binop(negated ? op::EConcat : op::UConcat,
					  rec(f1, false), rec(f2, negated));
		  break;
		}
	      case op::EmptyWord:
	      case op::Not:
		SPOT_UNREACHABLE();
	      }
	  }

	c->cache_nenoform(key, result);
	return result;
      }

      //////////////////////////////////////////////////////////////////////
      //
      //  SIMPLIFY_VISITOR
      //
      //////////////////////////////////////////////////////////////////////

      // Forward declaration.
      formula
      simplify_recursively(formula f, ltl_simplifier_cache* c);

      // X(a) R b   or   X(a) M b
      // This returns a.
      formula
      is_XRM(formula f)
      {
	if (!f.is(op::R, op::M))
	  return nullptr;
	auto left = f.nth(0);
	if (!left.is(op::X))
	  return nullptr;
	return left.nth(0);
      }

      // X(a) W b   or   X(a) U b
      // This returns a.
      formula
      is_XWU(formula f)
      {
	if (!f.is(op::W, op::U))
	  return nullptr;
	auto left = f.nth(0);
	if (!left.is(op::X))
	  return nullptr;
	return left.nth(0);
      }

      // b & X(b W a)  or   b & X(b U a)
      // This returns (b W a) or (b U a).
      formula
      is_bXbWU(formula f)
      {
	if (!f.is(op::And))
	  return nullptr;
	unsigned s = f.size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
	    auto p = f.nth(pos);
	    if (!(p.is(op::X)))
	      continue;
	    auto c = p.nth(0);
	    if (!c.is(op::U, op::W))
	      continue;
	    formula b = f.all_but(pos);
	    if (b == c.nth(0))
	      return c;
	  }
	return nullptr;
      }

      // b | X(b R a)  or   b | X(b M a)
      // This returns (b R a) or (b M a).
      formula
      is_bXbRM(formula f)
      {
	if (!f.is(op::Or))
	  return nullptr;
	unsigned s = f.size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
	    auto p = f.nth(pos);
	    if (!(p.is(op::X)))
	      continue;
	    auto c = p.nth(0);
	    if (!c.is(op::R, op::M))
	      continue;
	    formula b = f.all_but(pos);
	    if (b == c.nth(0))
	      return c;
	  }
	return nullptr;
      }

      formula
      unop_multop(op uop, op mop, vec v)
      {
	return formula::unop(uop, formula::multop(mop, v));
      }

      formula
      unop_unop_multop(op uop1, op uop2, op mop, vec v)
      {
	return formula::unop(uop1, unop_multop(uop2, mop, v));
      }

      formula
      unop_unop(op uop1, op uop2, formula f)
      {
	return formula::unop(uop1, formula::unop(uop2, f));
      }

      struct mospliter
      {
	enum what { Split_GF = (1 << 0),
		    Strip_GF = (1 << 1) | (1 << 0),
		    Split_FG = (1 << 2),
		    Strip_FG = (1 << 3) | (1 << 2),
		    Split_F = (1 << 4),
		    Strip_F = (1 << 5) | (1 << 4),
		    Split_G = (1 << 6),
		    Strip_G = (1 << 7) | (1 << 6),
		    Strip_X = (1 << 8),
		    Split_U_or_W = (1 << 9),
		    Split_R_or_M = (1 << 10),
		    Split_EventUniv = (1 << 11),
		    Split_Event = (1 << 12),
		    Split_Univ = (1 << 13),
		    Split_Bool = (1 << 14)
	};

      private:
	mospliter(unsigned split, ltl_simplifier_cache* cache)
	  : split_(split), c_(cache),
	    res_GF{(split_ & Split_GF) ? new vec : nullptr},
	    res_FG{(split_ & Split_FG) ? new vec : nullptr},
	    res_F{(split_ & Split_F) ? new vec : nullptr},
	    res_G{(split_ & Split_G) ? new vec : nullptr},
	    res_X{(split_ & Strip_X) ? new vec : nullptr},
	    res_U_or_W{(split_ & Split_U_or_W) ? new vec : nullptr},
	    res_R_or_M{(split_ & Split_R_or_M) ? new vec : nullptr},
	    res_Event{(split_ & Split_Event) ? new vec : nullptr},
	    res_Univ{(split_ & Split_Univ) ? new vec : nullptr},
	    res_EventUniv{(split_ & Split_EventUniv) ? new vec : nullptr},
	    res_Bool{(split_ & Split_Bool) ? new vec : nullptr},
	    res_other{new vec}
	{
	}

      public:
	mospliter(unsigned split, vec v, ltl_simplifier_cache* cache)
	  : mospliter(split, cache)
	{
	  for (auto f: v)
	    {
	      if (f) // skip null pointers left by previous simplifications
		process(f);
	    }
	}

	mospliter(unsigned split, formula mo,
		  ltl_simplifier_cache* cache)
	  : mospliter(split, cache)
	{
	  unsigned mos = mo.size();
	  for (unsigned i = 0; i < mos; ++i)
	    {
	      formula f = simplify_recursively(mo.nth(i), cache);
	      process(f);
	    }
	}

	void process(formula f)
	{
	  bool e = f.is_eventual();
	  bool u = f.is_universal();
	  bool eu = res_EventUniv && e & u && c_->options.favor_event_univ;
	  switch (f.kind())
	    {
	    case op::X:
	      if (res_X && !eu)
		{
		  res_X->push_back(f.nth(0));
		  return;
		}
	      break;
	    case op::F:
	      {
		formula c = f.nth(0);
		if (res_FG && u && c.is(op::G))
		  {
		    res_FG->push_back(((split_ & Strip_FG) == Strip_FG
				       ? c.nth(0) : f));
		    return;
		  }
		if (res_F && !eu)
		  {
		    res_F->push_back(((split_ & Strip_F) == Strip_F
				      ? c : f));
		    return;
		  }
		break;
	      }
	    case op::G:
	      {
		formula c = f.nth(0);
		if (res_GF && e && c.is(op::F))
		  {
		    res_GF->push_back(((split_ & Strip_GF) == Strip_GF
				       ? c.nth(0) : f));
		    return;
		  }
		if (res_G && !eu)
		  {
		    res_G->push_back(((split_ & Strip_G) == Strip_G
				      ? c : f));
		    return;
		  }
		break;
	      }
	    case op::U:
	    case op::W:
	      if (res_U_or_W)
		{
		  res_U_or_W->push_back(f);
		  return;
		}
	      break;
	    case op::R:
	    case op::M:
	      if (res_R_or_M)
		{
		  res_R_or_M->push_back(f);
		  return;
		}
	      break;
	    default:
	      if (res_Bool && f.is_boolean())
		{
		  res_Bool->push_back(f);
		  return;
		}
	      break;
	    }
	  if (c_->options.event_univ)
	    {
	      if (res_EventUniv && e && u)
		{
		  res_EventUniv->push_back(f);
		  return;
		}
	      if (res_Event && e)
		{
		  res_Event->push_back(f);
		  return;
		}
	      if (res_Univ && u)
		{
		  res_Univ->push_back(f);
		  return;
		}
	    }
	  res_other->push_back(f);
	}

	unsigned split_;
	ltl_simplifier_cache* c_;
	std::unique_ptr<vec> res_GF;
	std::unique_ptr<vec> res_FG;
	std::unique_ptr<vec> res_F;
	std::unique_ptr<vec> res_G;
	std::unique_ptr<vec> res_X;
	std::unique_ptr<vec> res_U_or_W;
	std::unique_ptr<vec> res_R_or_M;
	std::unique_ptr<vec> res_Event;
	std::unique_ptr<vec> res_Univ;
	std::unique_ptr<vec> res_EventUniv;
	std::unique_ptr<vec> res_Bool;
	std::unique_ptr<vec> res_other;
      };

      class simplify_visitor final
      {
      public:

	simplify_visitor(ltl_simplifier_cache* cache)
	  : c_(cache), opt_(cache->options)
	{
	}

	// if !neg build c&X(c&X(...&X(tail))) with n occurences of c
	// if neg build !c|X(!c|X(...|X(tail))).
	formula
	dup_b_x_tail(bool neg, formula c, formula tail, unsigned n)
	{
	  op mop;
	  if (neg)
	    {
	      c = formula::Not(c);
	      mop = op::Or;
	    }
	  else
	    {
	      mop = op::And;
	    }
	  while (n--)
	    tail = // b&X(tail) or !b|X(tail)
	      formula::multop(mop, {c, formula::X(tail)});
	  return tail;
	}

	formula
	visit(formula f)
	{
	  formula result = f;

	  auto recurse = [this](formula f)
	    {
	      return simplify_recursively(f, c_);
	    };

	  f = f.map(recurse);

	  switch (op o = f.kind())
	    {
	      case op::False:
	      case op::True:
	      case op::EmptyWord:
	      case op::AP:
	      case op::Not:
	      case op::FStar:
		return f;
	      case op::X:
		{
		  formula c = f.nth(0);
		  // Xf = f if f is both eventual and universal.
		  if (c.is_universal() && c.is_eventual())
		    {
		      if (opt_.event_univ)
			return c;
		      // If EventUniv simplification is disabled, use
		      // only the following basic rewriting rules:
		      //   XGF(f) = GF(f) and XFG(f) = FG(f)
		      // The former comes from Somenzi&Bloem (CAV'00).
		      // It's not clear why they do not list the second.
		      if (opt_.reduce_basics &&
			  (c.is({op::G, op::F}) || c.is({op::F, op::G})))
			return c;
		    }

		  // If Xa = a, keep only a.
		  if (opt_.containment_checks_stronger
		      && c_->lcc.equal(f, c))
		    return c;

		  // X(f1 & GF(f2)) = X(f1) & GF(f2)
		  // X(f1 | GF(f2)) = X(f1) | GF(f2)
		  // X(f1 & FG(f2)) = X(f1) & FG(f2)
		  // X(f1 | FG(f2)) = X(f1) | FG(f2)
		  //
		  // The above usually make more sense when reversed (see
		  // them in the And and Or rewritings), except when we
		  // try to maximaze the size of subformula that do not
		  // have EventUniv formulae.
		  if (opt_.favor_event_univ)
		    if (c.is(op::Or, op::And))
		      {
			mospliter s(mospliter::Split_EventUniv, c, c_);
			op oc = c.kind();
			s.res_EventUniv->
			  push_back(unop_multop(op::X, oc,
						std::move(*s.res_other)));
			formula result =
			  formula::multop(oc,
					  std::move(*s.res_EventUniv));
			if (result != f)
			  result = recurse(result);
			return result;
		      }
		  return f;
		}
	      case op::F:
		{
		  formula c = f.nth(0);
		  // If f is a pure eventuality formula then F(f)=f.
		  if (opt_.event_univ && c.is_eventual())
		    return c;

		  if (opt_.reduce_basics)
		    {
		      // F(a U b) = F(b)
		      if (c.is(op::U))
			return recurse(formula::F(c.nth(1)));

		      // F(a M b) = F(a & b)
		      if (c.is(op::M))
			return recurse(unop_multop(op::F, op::And,
						   {c.nth(0), c.nth(1)}));

		      // FX(a) = XF(a)
		      // FXX(a) = XXF(a) ...
		      // FXG(a) = XFG(a) = FG(a) ...
		      if (c.is(op::X))
			return recurse(unop_unop(op::X, op::F, c.nth(0)));

		      // FG(a & Xb) = FG(a & b)
		      // FG(a & Gb) = FG(a & b)
		      if (c.is({op::G, op::And}))
			{
			  formula m = c.nth(0);
			  if (!m.is_boolean())
			    {
			      formula out = m.map([](formula f)
						  {
						    if (f.is(op::X, op::G))
						      return f.nth(0);
						    return f;
						  });
			      if (out != m)
				return recurse(unop_unop(op::F, op::G, out));
			    }
			}
		    }
		  // if Fa => a, keep a.
		  if (opt_.containment_checks_stronger
		      && c_->lcc.contained(f, c))
		    return c;

		  // Disabled by default:
		  //     F(f1 & GF(f2)) = F(f1) & GF(f2)
		  //
		  // As is, these two formulae are translated into
		  // equivalent Büchi automata so the rewriting is
		  // useless.
		  //
		  // However when taken in a larger formula such
		  // as F(f1 & GF(f2)) | F(a & GF(b)), this
		  // rewriting used to produce (F(f1) & GF(f2)) |
		  // (F(a) & GF(b)), missing the opportunity to
		  // apply the F(E1)|F(E2) = F(E1|E2) rule which
		  // really helps the translation. F((f1 & GF(f2))
		  // | (a & GF(b))) is indeed easier to translate.
		  //
		  // So we do not consider this rewriting rule by
		  // default.  However if favor_event_univ is set,
		  // we want to move the GF out of the F.
		  if (opt_.favor_event_univ)
		    // F(f1&f2&FG(f3)&FG(f4)&f5&f6) =
		    //                     F(f1&f2) & FG(f3&f4) & f5 & f6
		    // if f5 and f6 are both eventual and universal.
		    if (c.is(op::And))
		      {
			mospliter s(mospliter::Strip_FG |
				    mospliter::Split_EventUniv,
				    c, c_);
			s.res_EventUniv->
			  push_back(unop_multop(op::F, op::And,
						std::move(*s.res_other)));
			s.res_EventUniv->
			  push_back(unop_unop_multop(op::F, op::G, op::And,
						     std::move(*s.res_FG)));
			formula res =
			  formula::And(std::move(*s.res_EventUniv));
			if (res != f)
			  return recurse(res);
		      }
		  // If u3 and u4 are universal formulae and h is not:
		  // F(f1 | f2 | Fu3 | u4 | FGg | Fh)
		  //    = F(f1 | f2 | u3 | u4 | Gg | h)
		  // or
		  // F(f1 | f2 | Fu3 | u4 | FGg | Fh)
		  //    = F(f1 | f2 | h) | F(u3 | u4 | Gg)
		  // depending on whether favor_event_univ is set.
		  if (c.is(op::Or))
		    {
		      int w = mospliter::Strip_F;
		      if (opt_.favor_event_univ)
			w |= mospliter::Split_Univ;
		      mospliter s(w, c, c_);
		      s.res_other->insert(s.res_other->end(),
					  s.res_F->begin(), s.res_F->end());
		      formula res = unop_multop(op::F, op::Or,
						std::move(*s.res_other));
		      if (s.res_Univ)
			{
			  // Strip any F.
			  for (auto& g: *s.res_Univ)
			    if (g.is(op::F))
			      g = g.nth(0);
			  formula fu = unop_multop(op::F, op::Or,
						   std::move(*s.res_Univ));
			  res = formula::Or({res, fu});
			}
		      if (res != f)
			return recurse(res);
		    }
		}
		return f;
	      case op::G:
		{
		  formula c = f.nth(0);
		  // If f is a pure universality formula then G(f)=f.
		  if (opt_.event_univ && c.is_universal())
		    return c;

		  if (opt_.reduce_basics)
		    {
		      // G(a R b) = G(b)
		      if (c.is(op::R))
			return recurse(formula::G(c.nth(1)));

		      // G(a W b) = G(a | b)
		      if (c.is(op::W))
			return recurse(unop_multop(op::G, op::Or,
						   {c.nth(0), c.nth(1)}));

		      // GX(a) = XG(a)
		      // GXX(a) = XXG(a) ...
		      // GXF(a) = XGF(a) = GF(a) ...
		      if (c.is(op::X))
			return recurse(unop_unop(op::X, op::G, c.nth(0)));

		      // G(f1|f2|GF(f3)|GF(f4)|f5|f6) =
		      //                        G(f1|f2) | GF(f3|f4) | f5 | f6
		      // if f5 and f6 are both eventual and universal.
		      if (c.is(op::Or))
			{
			  mospliter s(mospliter::Strip_GF |
				      mospliter::Split_EventUniv,
				      c, c_);
			  s.res_EventUniv->
			    push_back(unop_multop(op::G, op::Or,
						  std::move(*s.res_other)));
			  s.res_EventUniv->
			    push_back(unop_unop_multop(op::G, op::F, op::Or,
						       std::move(*s.res_GF)));
			  formula res =
			    formula::Or(std::move(*s.res_EventUniv));

			  if (res != f)
			    return recurse(res);
			}
		      // If e3 and e4 are eventual formulae and h is not:
		      // G(f1 & f2 & Ge3 & e4 & GFg & Gh)
		      //    = G(f1 & f2 & e3 & e4 & Fg & h)
		      // or
		      // G(f1 & f2 & Ge3 & e4 & GFg & Gh)
		      //    = G(f1 & f2 & h) & G(e3 & e4 & Fg)
		      // depending on whether favor_event_univ is set.
		      else if (c.is(op::And))
			{
			  int w = mospliter::Strip_G;
			  if (opt_.favor_event_univ)
			    w |= mospliter::Split_Event;
			  mospliter s(w, c, c_);
			  s.res_other->insert(s.res_other->end(),
					      s.res_G->begin(), s.res_G->end());
			  formula res = unop_multop(op::G, op::And,
						    std::move(*s.res_other));

			  if (s.res_Event)
			    {
			      // Strip any G.
			      for (auto& g: *s.res_Event)
				if (g.is(op::G))
				  g = g.nth(0);
			      formula ge =
				unop_multop(op::G, op::And,
					    std::move(*s.res_Event));
			      res = formula::And({res, ge});
			    }
			  if (res != f)
			    return recurse(res);
			}

		      // GF(a | Xb) = GF(a | b)
		      // GF(a | Fb) = GF(a | b)
		      if (c.is({op::F, op::Or}))
			{
			  formula m = c.nth(0);
			  if (!m.is_boolean())
			    {
			      formula out = m.map([](formula f)
						  {
						    if (f.is(op::X, op::F))
						      return f.nth(0);
						    return f;
						  });
			      if (out != m)
				return recurse(unop_unop(op::G, op::F, out));
			    }
			}
		    }
		  // if a => Ga, keep a.
		  if (opt_.containment_checks_stronger
		      && c_->lcc.contained(c, f))
		    return c;
		}
		return f;
	      case op::Closure:
	      case op::NegClosure:
	      case op::NegClosureMarked:
		{
		  formula c = f.nth(0);
		  // {e[*]} = {e}
		  // !{e[*]} = !{e}
		  if (c.accepts_eword() && c.is(op::Star))
		    return recurse(formula::unop(o, c.nth(0)));

		  if (!opt_.reduce_size_strictly)
		    if (c.is(op::OrRat))
		      {
			//  {a₁|a₂} =  {a₁}| {a₂}
			// !{a₁|a₂} = !{a₁}&!{a₂}
			unsigned s = c.size();
			vec v;
			for (unsigned n = 0; n < s; ++n)
			  v.push_back(formula::unop(o, c.nth(n)));
			return recurse(formula::multop(o == op::Closure
						       ? op::Or : op::And, v));
		      }
		  if (c.is(op::Concat))
		    {
		      if (c.accepts_eword())
			{
			  if (opt_.reduce_size_strictly)
			    return f;
			  // If all terms accept the empty word, we have
			  // {e₁;e₂;e₃} =  {e₁}|{e₂}|{e₃}
			  // !{e₁;e₂;e₃} = !{e₁}&!{e₂}&!{e₃}
			  vec v;
			  unsigned end = c.size();
			  v.reserve(end);
			  for (unsigned i = 0; i < end; ++i)
			    v.push_back(formula::unop(o, c.nth(i)));
			  return recurse(formula::multop(o == op::Closure ?
							 op::Or : op::And, v));
			}

		      // Some term does not accept the empty word.
		      unsigned end = c.size() - 1;
		      // {b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
		      //    = b₁&X(b₂&X({e₁;f₁;e₂;f₂}))
		      // !{b₁;b₂;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
		      //    = !b₁|X(!b₂|X(!{e₁;f₁;e₂;f₂}))
		      // if e denotes a term that accepts [*0]
		      // and b denotes a Boolean formula.
		      while (c.nth(end).accepts_eword())
			--end;
		      unsigned start = 0;
		      while (start <= end)
			{
			  formula r = c.nth(start);
			  if (r.is_boolean() && !opt_.reduce_size_strictly)
			    ++start;
			  else
			    break;
			}
		      unsigned s = end + 1 - start;
		      if (s != c.size())
			{
			  bool doneg = o != op::Closure;
			  formula tail;
			  if (s > 0)
			    {
			      vec v;
			      v.reserve(s);
			      for (unsigned n = start; n <= end; ++n)
				v.push_back(c.nth(n));
			      tail = formula::Concat(v);
			      tail = formula::unop(o, tail);
			    }
			  else
			    {
			      tail = doneg ? formula::ff() : formula::tt();
			    }

			  for (unsigned n = start; n > 0;)
			    {
			      --n;
			      formula e = c.nth(n);
			      // {b;f} = b & X{f}
			      // !{b;f} = !b | X!{f}
			      if (e.is_boolean())
				{
				  tail = formula::X(tail);
				  if (doneg)
				    tail = formula::Or({formula::Not(e), tail});
				  else
				    tail = formula::And({e, tail});
				}
			    }
			  return recurse(tail);
			}

		      // {b[*i..j];c} = b&X(b&X(... b&X{b[*0..j-i];c}))
		      // !{b[*i..j];c} = !b&X(!b&X(... !b&X!{b[*0..j-i];c}))
		      if (!opt_.reduce_size_strictly)
			if (c.nth(0).is(op::Star))
			  {
			    formula s = c.nth(0);
			    formula sc = s.nth(0);
			    unsigned min = s.min();
			    if (sc.is_boolean() && min > 0)
			      {
				unsigned max = s.max();
				if (max != formula::unbounded())
				  max -= min;
				unsigned ss = c.size();
				vec v;
				v.reserve(ss);
				v.push_back(formula::Star(sc, 0, max));
				for (unsigned n = 1; n < ss; ++n)
				  v.push_back(c.nth(n));
				formula tail = formula::Concat(v);
				tail = // {b[*0..j-i]} or !{b[*0..j-i]}
				  formula::unop(o, tail);
				tail =
				  dup_b_x_tail(o != op::Closure,
					       sc, tail, min);
				return recurse(tail);
			      }
			  }
		    }
		  // {b[*i..j]} = b&X(b&X(... b))  with i occurences of b
		  // !{b[*i..j]} = !b&X(!b&X(... !b))
		  if (!opt_.reduce_size_strictly)
		    if (c.is(op::Star))
		      {
			formula cs = c.nth(0);
			if (cs.is_boolean())
			  {
			    unsigned min = c.min();
			    assert(min > 0);
			    formula tail;
			    if (o == op::Closure)
			      tail = dup_b_x_tail(false, cs,
						  formula::tt(), min);
			    else
			      tail = dup_b_x_tail(true, cs,
						  formula::ff(), min);
			    return recurse(tail);
			  }
		      }
		  return f;
		}
	      case op::Xor:
	      case op::Implies:
	      case op::Equiv:
	      case op::U:
	      case op::R:
	      case op::W:
	      case op::M:
	      case op::EConcat:
	      case op::EConcatMarked:
	      case op::UConcat:
		return visit_binop(f);
	      case op::Or:
	      case op::OrRat:
	      case op::And:
	      case op::AndRat:
	      case op::AndNLM:
	      case op::Concat:
		return visit_multop(f);
	      case op::Fusion:
		return f;
	      case op::Star:
		{
		  formula h = f.nth(0);
		  auto min = f.min();
		  if (h.accepts_eword())
		    min = 0;
		  if (min == 0)
		    h = f.max() == formula::unbounded()
		      ? c_->star_normal_form(h)
		      : c_->star_normal_form_bounded(h);
		  return formula::Star(h, min, f.max());
		}
	    }
	  SPOT_UNREACHABLE();
	}

	formula reduce_sere_ltl(formula orig)
	{
	  op bindop = orig.kind();
	  formula a = orig.nth(0);
	  formula b = orig.nth(1);

	  auto recurse = [this](formula f)
	    {
	      return simplify_recursively(f, c_);
	    };

	  // All this function is documented assuming bindop ==
	  // UConcat, but by changing the following variables it can
	  // perform the rules for EConcat as well.
	  op op_g;
	  op op_w;
	  op op_r;
	  op op_and;
	  bool doneg;
	  if (bindop == op::UConcat)
	    {
	      op_g = op::G;
	      op_w = op::W;
	      op_r = op::R;
	      op_and = op::And;
	      doneg = true;
	    }
	  else // EConcat & EConcatMarked
	    {
	      op_g = op::F;
	      op_w = op::M;
	      op_r = op::U;
	      op_and = op::Or;
	      doneg = false;
	    }

	  if (!opt_.reduce_basics)
	    return orig;
	  if (a.is(op::Star))
	    {
	      // {[*]}[]->b = Gb
	      if (a == formula::one_star())
		return recurse(formula::unop(op_g, b));

	      formula s = a.nth(0);
	      unsigned min = a.min();
	      unsigned max = a.max();
	      // {s[*]}[]->b = b W !s   if s is Boolean.
	      // {s[+]}[]->b = b W !s   if s is Boolean.
	      if (s.is_boolean() && max == formula::unbounded() && min <= 1)
		{
		  formula ns = doneg ? formula::Not(s) : s;
		  // b W !s
		  return recurse(formula::binop(op_w, b, ns));
		}
	      if (opt_.reduce_size_strictly)
		return orig;
	      // {s[*i..j]}[]->b = {s;s;...;s[*1..j-i+1]}[]->b
	      // = {s}[]->X({s}[]->X(...[]->X({s[*1..j-i+1]}[]->b)))
	      // if i>0 and s does not accept the empty word
	      if (min == 0 || s.accepts_eword())
		return orig;
	      --min;
	      if (max != formula::unbounded())
		max -= min; // j-i+1
	      // Don't rewrite s[1..].
	      if (min == 0)
		return orig;
	      formula tail = // {s[*1..j-i]}[]->b
		formula::binop(bindop, formula::Star(s, 1, max), b);
	      for (unsigned n = 0; n < min; ++n)
		tail = // {s}[]->X(tail)
		  formula::binop(bindop, s, formula::X(tail));
	      return recurse(tail);
	    }
	  else if (a.is(op::Concat))
	    {
	      unsigned s = a.size() - 1;
	      formula last = a.nth(s);
	      // {r;[*]}[]->b = {r}[]->Gb
	      if (last == formula::one_star())
		  return recurse(formula::binop(bindop, a.all_but(s),
						formula::unop(op_g, b)));

	      formula first = a.nth(0);
	      // {[*];r}[]->b = G({r}[]->b)
	      if (first == formula::one_star())
		return recurse(formula::unop(op_g,
					     formula::binop(bindop,
							    a.all_but(0), b)));

	      if (opt_.reduce_size_strictly)
		return orig;

	      // {r;s[*]}[]->b = {r}[]->(b & X(b W !s))
	      // if s is Boolean and r does not accept [*0];
	      if (last.is_Kleene_star()) // l = s[*]
		if (last.nth(0).is_boolean())
		  {
		    formula r = a.all_but(s);
		    if (!r.accepts_eword())
		      {
			formula ns = // !s
			  doneg ? formula::Not(last.nth(0)) : last.nth(0);
			formula w = // b W !s
			  formula::binop(op_w, b, ns);
			formula x = // X(b W !s)
			  formula::X(w);
			formula d = // b & X(b W !s)
			  formula::multop(op_and, {b, x});
			// {r}[]->(b & X(b W !s))
			return recurse(formula::binop(bindop, r, d));
		      }
		  }
	      // {s[*];r}[]->b = !s R ({r}[]->b)
	      // if s is Boolean and r does not accept [*0];
	      if (first.is_Kleene_star())
		if (first.nth(0).is_boolean())
		  {
		    formula r = a.all_but(0);
		    if (!r.accepts_eword())
		      {
			formula ns = // !s
			  doneg
			  ? formula::Not(first.nth(0))
			  : first.nth(0);
			formula u = // {r}[]->b
			  formula::binop(bindop, r, b);
			// !s R ({r}[]->b)
			return recurse(formula::binop(op_r, ns, u));
		      }
		  }

	      // {r₁;r₂;r₃}[]->b = {r₁}[]->X({r₂}[]->X({r₃}[]->b))
	      // if r₁, r₂, r₃ do not accept [*0].
	      if (!a.accepts_eword())
		{
		  unsigned count = 0;
		  for (unsigned n = 0; n <= s; ++n)
		    count += !a.nth(n).accepts_eword();
		  assert(count > 0);
		  if (count == 1)
		    return orig;
		  // Let e denote a term that accepts [*0]
		  // and let f denote a term that do not.
		  // A formula such as {e₁;f₁;e₂;e₃;f₂;e₄}[]->b
		  // in which count==2 will be grouped
		  // as follows:  r₁ = e₁;f₁;e₂;e₃
		  //              r₂ = f₂;e₄
		  // this way we have
		  // {e₁;f₁;e₂;e₃;f₂;e₄}[]->b = {r₁;r₂;r₃}[]->b
		  // where r₁ and r₂ do not accept [*0].
		  unsigned pos = s + 1;

		  // We compute the r formulas from the right
		  // (i.e., r₂ before r₁.)
		  vec r;
		  do
		    r.insert(r.begin(), a.nth(--pos));
		  while (r.front().accepts_eword());
		  formula tail = // {r₂}[]->b
		    formula::binop(bindop, formula::Concat(r), b);
		  while (--count)
		    {
		      vec r;
		      do
			r.insert(r.begin(), a.nth(--pos));
		      while (r.front().accepts_eword());
		      // If it's the last block, take all leading
		      // formulae as well.
		      if (count == 1)
			while (pos > 0)
			  {
			    r.insert(r.begin(), a.nth(--pos));
			    assert(r.front().accepts_eword());
			  }

		      tail = // X({r₂}[]->b)
			formula::X(tail);
		      tail = // {r₁}[]->X({r₂}[]->b)
			formula::binop(bindop, formula::Concat(r), tail);
		    }
		  return recurse(tail);
		}
	    }
	  else if (opt_.reduce_size_strictly)
	    {
	      return orig;
	    }
	  else if (a.is(op::Fusion))
	    {
	      // {r₁:r₂:r₃}[]->b = {r₁}[]->({r₂}[]->({r₃}[]->b))
	      unsigned s = a.size();
	      formula tail = b;
	      do
		{
		  --s;
		  tail = formula::binop(bindop, a.nth(s), tail);
		}
	      while (s != 0);
	      return recurse(tail);
	    }
	  else if (a.is(op::OrRat))
	    {
	      // {r₁|r₂|r₃}[]->b = ({r₁}[]->b)&({r₂}[]->b)&({r₃}[]->b)
	      unsigned s = a.size();
	      vec v;
	      for (unsigned n = 0; n < s; ++n)
		// {r₁}[]->b
		v.push_back(formula::binop(bindop, a.nth(n), b));
	      return recurse(formula::multop(op_and, v));
	    }
	  return orig;
	}

	formula
	visit_binop(formula bo)
	{
	  auto recurse = [this](formula f)
	    {
	      return simplify_recursively(f, c_);
	    };
	  op o = bo.kind();
	  formula b = bo.nth(1);
	  if (opt_.event_univ)
	    {
	      trace << "bo: trying eventuniv rules" << std::endl;
	      /* If b is a pure eventuality formula then a U b = b.
		 If b is a pure universality formula a R b = b. */
	      if ((b.is_eventual() && bo.is(op::U))
		  || (b.is_universal() && bo.is(op::R)))
		return b;
	    }

	  formula a = bo.nth(0);
	  if (opt_.event_univ)
	    {
	      /* If a is a pure eventuality formula then a M b = a & b.
		 If a is a pure universality formula a W b = a | b. */
	      if (a.is_eventual() && bo.is(op::M))
		return recurse(formula::And({a, b}));
	      if (a.is_universal() && bo.is(op::W))
		return recurse(formula::Or({a, b}));

	      // e₁ W e₂ = Ge₁ | e₂
	      // u₁ M u₂ = Fu₁ & u₂
	      if (!opt_.reduce_size_strictly)
		{
		  if (bo.is(op::W) && a.is_eventual() && b.is_eventual())
		    return recurse(formula::Or({formula::G(a), b}));
		  if (bo.is(op::M) && a.is_universal() && b.is_universal())
		    return recurse(formula::And({formula::F(a), b}));
		}

	      // In the following rewritings we assume that
	      // - e is a pure eventuality
	      // - u is purely universal
	      // - q is purely universal pure eventuality
	      // (a U (b|e)) = (a U b)|e
	      // (a W (b|e)) = (a W b)|e
	      // (a U (b&q)) = (a U b)&q
	      // ((a&q) M b) = (a M b)&q
	      // (a R (b&u)) = (a R b)&u
	      // (a M (b&u)) = (a M b)&u
	      if (opt_.favor_event_univ)
		{
		  if (bo.is(op::U, op::W))
		    if (b.is(op::Or))
		      {
			mospliter s(mospliter::Split_Event, b, c_);
			formula b2 = formula::Or(std::move(*s.res_other));
			if (b2 != b)
			  {
			    s.res_Event->push_back(formula::binop(o, a, b2));
			    return recurse
			      (formula::Or(std::move(*s.res_Event)));
			  }
		      }
		  if (bo.is(op::U))
		    if (b.is(op::And))
		      {
			mospliter s(mospliter::Split_EventUniv, b, c_);
			formula b2 = formula::And(std::move(*s.res_other));
			if (b2 != b)
			  {
			    s.res_EventUniv->push_back(formula::binop(o,
								      a, b2));
			    return recurse
			      (formula::And(std::move(*s.res_EventUniv)));
			  }
		      }
		  if (bo.is(op::M))
		    if (a.is(op::And))
		      {
			mospliter s(mospliter::Split_EventUniv, a, c_);
			formula a2 = formula::And(std::move(*s.res_other));
			if (a2 != a)
			  {
			    s.res_EventUniv->push_back(formula::binop(o,
								      a2, b));
			    return recurse
			      (formula::And(std::move(*s.res_EventUniv)));
			  }
		      }
		  if (bo.is(op::R, op::M))
		    if (b.is(op::And))
		      {
			mospliter s(mospliter::Split_Univ, b, c_);
			formula b2 = formula::And(std::move(*s.res_other));
			if (b2 != b)
			  {
			    s.res_Univ->push_back(formula::binop(o, a, b2));
			    return recurse
			      (formula::And(std::move(*s.res_Univ)));
			  }
		      }
		}
	      trace << "bo: no eventuniv rule matched" << std::endl;
	    }

	  // Inclusion-based rules
	  if (opt_.synt_impl | opt_.containment_checks)
	    {
	      trace << "bo: trying inclusion-based rules" << std::endl;
	      switch (o)
		{
		case op::Xor:
		case op::Equiv:
		case op::Implies:
		  SPOT_UNIMPLEMENTED();
		  break;

		case op::U:
		  // if a => b, then a U b = b
		  // if (a U b) => b, then a U b = b (for stronger containment)
		  if (c_->implication(a, b)
		      || (opt_.containment_checks_stronger
			  && c_->contained(bo, b)))
		    return b;
		  // if !a => b, then a U b = Fb
		  if (c_->implication_neg(a, b, false))
		    return formula::F(b);
		  // if a => b, then a U (b U c) = (b U c)
		  // if a => b, then a U (b W c) = (b W c)
		  if (b.is(op::U, op::W) && c_->implication(a, b.nth(0)))
		    return b;
		  // if b => a, then a U (b U c) = (a U c)
		  if (b.is(op::U) && c_->implication(b.nth(0), a))
		    return recurse(formula::U(a, b.nth(1)));
		  // if a => c, then a U (b R (c U d)) = (b R (c U d))
		  // if a => c, then a U (b R (c W d)) = (b R (c W d))
		  // if a => c, then a U (b M (c U d)) = (b M (c U d))
		  // if a => c, then a U (b M (c W d)) = (b M (c W d))
		  if (b.is(op::R, op::M) && b.nth(1).is(op::U, op::W)
		      && c_->implication(a, b.nth(1).nth(0)))
		    return b;
		  // if a => b, then (a U c) U b = c U b
		  // if a => b, then (a W c) U b = c U b
		  if (a.is(op::U, op::W) && c_->implication(a.nth(0), b))
		    return recurse(formula::U(a.nth(1), b));
		  // if c => b, then (a U c) U b = (a U c) | b
		  if (a.is(op::U) && c_->implication(a.nth(1), b))
		    return recurse(formula::Or({a, b}));
		  break;

		case op::R:
		  // if b => a, then a R b = b
		  if (c_->implication(b, a))
		    return b;
		  // if b => !a, then a R b = Gb
		  if (c_->implication_neg(b, a, true))
		    return recurse(formula::G(b));
		  // if b => a, then a R (b R c) = b R c
		  // if b => a, then a R (b M c) = b M c
		  if (b.is(op::R, op::M) && c_->implication(b.nth(0), a))
		    return b;
		  // if a => b, then a R (b R c) = a R c
		  if (b.is(op::R) && c_->implication(a, b.nth(0)))
		    return recurse(formula::R(a, b.nth(1)));
		  // if b => a, then (a R c) R b = c R b
		  // if b => a, then (a M c) R b = c R b
		  // if c => b, then (a R c) R b = (a & c) R b
		  // if c => b, then (a M c) R b = (a & c) R b
		  if (a.is(op::R, op::M))
		    {
		      if (c_->implication(b, a.nth(0)))
			return recurse(formula::R(a.nth(1), b));
		      if (c_->implication(a.nth(1), b))
			{
			  formula ac = formula::And({a.nth(0), a.nth(1)});
			  return recurse(formula::R(ac, b));
			}
		    }
		  break;

		case op::W:
		  // if a => b, then a W b = b
		  // if a W b => b, then a W b = b (for stronger containment)
		  if (c_->implication(a, b)
		      || (opt_.containment_checks_stronger
			  && c_->contained(bo, b)))
		    return b;
		  // if !a => b then a W b = 1
		  if (c_->implication_neg(a, b, false))
		    return formula::tt();
		  // if a => b, then a W (b W c) = b W c
		  // (Beware: even if a => b we do not have a W (b U c) = b U c)
		  if (b.is(op::W) && c_->implication(a, b.nth(0)))
		    return b;
		  // if b => a, then a W (b U c) = a W c
		  // if b => a, then a W (b W c) = a W c
		  if (b.is(op::U, op::W) && c_->implication(b.nth(0), a))
		    return recurse(formula::W(a, b.nth(1)));
		  // if a => b, then (a U c) W b = c W b
		  // if a => b, then (a W c) W b = c W b
		  if (a.is(op::U, op::W) && c_->implication(a.nth(0), b))
		    return recurse(formula::W(a.nth(1), b));
		  // if c => b, then (a W c) W b = (a W c) | b
		  // if c => b, then (a U c) W b = (a U c) | b
		  if (a.is(op::U, op::W) && c_->implication(a.nth(1), b))
		    return recurse(formula::Or({a, b}));
		  break;

		case op::M:
		  // if b => a, then a M b = b
		  if (c_->implication(b, a))
		    return b;
		  // if b => !a, then a M b = 0
		  if (c_->implication_neg(b, a, true))
		    return formula::ff();
		  // if b => a, then a M (b M c) = b M c
		  if (b.is(op::M) && c_->implication(b.nth(0), a))
		    return b;
		  // if a => b, then a M (b M c) = a M c
		  // if a => b, then a M (b R c) = a M c
		  if (b.is(op::M, op::R) && c_->implication(a, b.nth(0)))
		    return recurse(formula::M(a, b.nth(1)));
		  // if b => a, then (a R c) M b = c M b
		  // if b => a, then (a M c) M b = c M b
		  if (a.is(op::R, op::M) && c_->implication(b, a.nth(0)))
		    return recurse(formula::M(a.nth(1), b));
		  // if c => b, then (a M c) M b = (a & c) M b
		  if (a.is(op::M) && c_->implication(a.nth(1), b))
		    return
		      recurse(formula::M(formula::And({a.nth(0), a.nth(1)}),
					 b));
		  break;

		default:
		  break;
		}
	      trace << "bo: no inclusion-based rules matched" << std::endl;
	    }

	  if (!opt_.reduce_basics)
	    {
	      trace << "bo: basic reductions disabled" << std::endl;
	      return bo;
	    }

	  trace << "bo: trying basic reductions" << std::endl;
	  // Rewrite U,R,W,M as F or G when possible.
	  // true U b == F(b)
	  if (bo.is(op::U) && a.is(op::True))
	    return recurse(formula::F(b));
	  // false R b == G(b)
	  if (bo.is(op::R) && a.is(op::False))
	    return recurse(formula::G(b));
	  // a W false == G(a)
	  if (bo.is(op::W) && b.is(op::False))
	    return recurse(formula::G(a));
	  // a M true == F(a)
	  if (bo.is(op::M) && b.is(op::True))
	    return recurse(formula::F(a));

	  if (bo.is(op::W, op::M) || bo.is(op::U, op::R))
	    {
	      // X(a) U X(b) = X(a U b)
	      // X(a) R X(b) = X(a R b)
	      // X(a) W X(b) = X(a W b)
	      // X(a) M X(b) = X(a M b)
	      if (a.is(op::X) && b.is(op::X))
		return recurse(formula::X(formula::binop(o,
							 a.nth(0), b.nth(0))));

	      if (bo.is(op::U, op::W))
		{
		  // a U Ga = Ga
		  // a W Ga = Ga
		  if (b.is(op::G) && a == b.nth(0))
		    return b;
		  // a U (b | c | G(a)) = a W (b | c)
		  // a W (b | c | G(a)) = a W (b | c)
		  if (b.is(op::Or))
		    for (int i = 0, s = b.size(); i < s; ++i)
		      {
			formula c = b.nth(i);
			if (c.is(op::G) && c.nth(0) == a)
			  return recurse(formula::W(a, b.all_but(i)));
		      }
		  // a U (b & a & c) == (b & c) M a
		  // a W (b & a & c) == (b & c) R a
		  if (b.is(op::And))
		    for (int i = 0, s = b.size(); i < s; ++i)
		      if (b.nth(i) == a)
			return recurse(formula::binop(o == op::U ?
						      op::M : op::R,
						      b.all_but(i), a));
		  // If b is Boolean:
		  // (Xc) U b = b | X(b M c)
		  // (Xc) W b = b | X(b R c)
		  if (!opt_.reduce_size_strictly
		      && a.is(op::X) && b.is_boolean())
		    {
		      formula x = formula::X(formula::binop(o == op::U ?
							    op::M : op::R,
							    b, a.nth(0)));
		      return recurse(formula::Or({b, x}));
		    }
		}
	      else if (bo.is(op::M, op::R))
		{
		  // a R Fa = Fa
		  // a M Fa = Fa
		  if (b.is(op::F) && b.nth(0) == a)
		    return b;

		  // a R (b & c & F(a)) = a M (b & c)
		  // a M (b & c & F(a)) = a M (b & c)
		  if (b.is(op::And))
		    for (int i = 0, s = b.size(); i < s; ++i)
		      {
			formula c = b.nth(i);
			if (c.is(op::F) && c.nth(0) == a)
			  return recurse(formula::M(a, b.all_but(i)));
		      }
		  // a M (b | a | c) == (b | c) U a
		  // a R (b | a | c) == (b | c) W a
		  if (b.is(op::Or))
		    for (int i = 0, s = b.size(); i < s; ++i)
		      if (b.nth(i) == a)
			return recurse(formula::binop(o == op::M ?
						      op::U : op::W,
						      b.all_but(i), a));
		  // If b is Boolean:
		  // (Xc) R b = b & X(b W c)
		  // (Xc) M b = b & X(b U c)
		  if (!opt_.reduce_size_strictly
		      && a.is(op::X) && b.is_boolean())
		    {
		      formula x =
			formula::X(formula::binop(o == op::M ? op::U : op::W,
						  b, a.nth(0)));
		      return recurse(formula::And({b, x}));
		    }
		}
	    }
	  if (bo.is(op::UConcat) || bo.is(op::EConcat, op::EConcatMarked))
	    return reduce_sere_ltl(bo);
	  return bo;
	}

	formula
	visit_multop(formula mo)
	{
	  auto recurse = [this](formula f)
	    {
	      return simplify_recursively(f, c_);
	    };

	  unsigned mos = mo.size();

	  if ((opt_.synt_impl | opt_.containment_checks)
	      && mo.is(op::Or, op::And))
	    for (unsigned i = 0; i < mos; ++i)
	      {
		formula fi = mo.nth(i);
		formula fo = mo.all_but(i);
		// if fi => fo, then fi | fo = fo
		// if fo => fi, then fi & fo = fo
		if ((mo.is(op::Or) && c_->implication(fi, fo))
		    || (mo.is(op::And) && c_->implication(fo, fi)))
		  return recurse(fo);
		// if fi => !fo, then fi & fo = false
		// if fo => !fi, then fi & fo = false
		// if !fi => fo, then fi | fo = true
		// if !fo => fi, then fi | fo = true
		bool is_and = mo.is(op::And);
		if (c_->implication_neg(fi, fo, is_and)
		    || c_->implication_neg(fo, fi, is_and))
		  return recurse(is_and ? formula::ff() : formula::tt());
	      }

	  vec res;
	  res.reserve(mos);
	  for (auto f: mo)
	    res.push_back(f);
	  op o = mo.kind();

	  // basics reduction do not concern Boolean formulas,
	  // so don't waste time trying to apply them.
	  if (opt_.reduce_basics && !mo.is_boolean())
	    {
	      switch (o)
		{
		case op::And:
		  assert(!mo.is_sere_formula());
		  {
		    // a & X(G(a&b...) & c...) = Ga & X(G(b...) & c...)
		    // a & (Xa W b) = b R a
		    // a & (Xa U b) = b M a
		    // a & (b | X(b R a)) = b R a
		    // a & (b | X(b M a)) = b M a
		    if (!mo.is_syntactic_stutter_invariant()) // Skip if no X.
		      {
			typedef std::unordered_set<formula> fset_t;
			typedef std::unordered_map<formula,
						   std::set<unsigned>> fmap_t;
			fset_t xgset; // XG(...)
			fset_t xset;  // X(...)
			fmap_t wuset; // (X...)W(...) or (X...)U(...)

			std::vector<bool> tokill(mos);

			// Make a pass to search for subterms
			// of the form XGa or  X(... & G(...&a&...) & ...)
			for (unsigned n = 0; n < mos; ++n)
			  {
			    if (!res[n])
			      continue;
			    if (res[n].is_syntactic_stutter_invariant())
			      continue;

			    if (formula xarg = is_XWU(res[n]))
			      {
				wuset[xarg].insert(n);
				continue;
			      }

			    // Now we are looking for
			    // - X(...)
			    // - b | X(b R ...)
			    // - b | X(b M ...)
			    if (formula barg = is_bXbRM(res[n]))
			      {
				wuset[barg.nth(1)].insert(n);
				continue;
			      }

			    if (!res[n].is(op::X))
			      continue;

			    formula c = res[n].nth(0);
			    auto handle_G = [&xgset](formula c)
			      {
				formula a2 = c.nth(0);
				if (a2.is(op::And))
				  for (auto c: a2)
				    xgset.insert(c);
				else
				  xgset.insert(a2);
			      };

			    if (c.is(op::G))
			      {
				handle_G(c);
			      }
			    else if (c.is(op::And))
			      {
				for (auto cc: c)
				  if (cc.is(op::G))
				    handle_G(cc);
				  else
				    xset.insert(cc);
			      }
			    else
			      {
				xset.insert(c);
			      }
			    res[n] = nullptr;
			  }
			// Make a second pass to check if the "a"
			// terms can be used to simplify "Xa W b",
			// "Xa U b", "b | X(b R a)", or "b | X(b M a)".
			vec resorig(res);
			for (unsigned n = 0; n < mos; ++n)
			  {
			    formula x = resorig[n];
			    if (!x)
			      continue;
			    fmap_t::const_iterator gs = wuset.find(x);
			    if (gs == wuset.end())
			      continue;

			    for (unsigned pos: gs->second)
			      {
				formula wu = resorig[pos];
				if (wu.is(op::W, op::U))
				  {
				    // a & (Xa W b) = b R a
				    // a & (Xa U b) = b M a
				    op t = wu.is(op::U) ? op::M : op::R;
				    assert(wu.nth(0).is(op::X));
				    formula a = wu.nth(0).nth(0);
				    formula b = wu.nth(1);
				    res[pos] = formula::binop(t, b, a);
				  }
				else
				  {
				    // a & (b | X(b R a)) = b R a
				    // a & (b | X(b M a)) = b M a
				    wu = is_bXbRM(resorig[pos]);
				    assert(wu);
				    res[pos] = wu;
				  }
				// Remember to kill "a".
				tokill[n] = true;
			      }
			  }

			// Make third pass to search for terms 'a'
			// that also appears as 'XGa'.  Replace them
			// by 'Ga' and delete XGa.
			for (unsigned n = 0; n < mos; ++n)
			  {
			    formula x = res[n];
			    if (!x)
			      continue;
			    fset_t::const_iterator g = xgset.find(x);
			    if (g != xgset.end())
			      {
				// x can appear only once.
				formula gf = *g;
				xgset.erase(g);
				res[n] = formula::G(x);
			      }
			    else if (tokill[n])
			      {
				res[n] = nullptr;
			      }
			  }

			vec xv;
			unsigned xgs = xgset.size();
			xv.reserve(xset.size() + 1);
			if (xgs > 0)
			  {
			    vec xgv;
			    xgv.reserve(xgs);
			    for (auto f: xgset)
			      xgv.push_back(f);
			    xv.emplace_back(unop_multop(op::G, op::And, xgv));
			  }
			for (auto f: xset)
			  xv.emplace_back(f);
			res.push_back(unop_multop(op::X, op::And, xv));
		      }

		    // Gather all operands by type.
		    mospliter s(mospliter::Strip_X |
				mospliter::Strip_FG |
				mospliter::Strip_G |
				mospliter::Split_F |
				mospliter::Split_U_or_W |
				mospliter::Split_R_or_M |
				mospliter::Split_EventUniv,
				res, c_);

		    // FG(a) & FG(b) = FG(a & b)
		    formula allFG = unop_unop_multop(op::F, op::G, op::And,
						     std::move(*s.res_FG));
		    // Xa & Xb = X(a & b)
		    // Xa & Xb & FG(c) = X(a & b & FG(c))
		    // For Universal&Eventual formulae f1...fn we also have:
		    // Xa & Xb & f1...fn = X(a & b & f1...fn)
		    if (!s.res_X->empty() && !opt_.favor_event_univ)
		      {
			s.res_X->push_back(allFG);
			allFG = nullptr;
			s.res_X->insert(s.res_X->begin(),
					s.res_EventUniv->begin(),
					s.res_EventUniv->end());
		      }
		    else
		      // If f1...fn are event&univ formulae, with at least
		      // one formula of the form G(...),
		      // Rewrite  g & f1...fn  as  g & G(f1..fn) while
		      // stripping any leading G from f1...fn.
		      // This gathers eventual&universal formulae
		      // under the same term.
		      {
			vec eu;
			bool seen_g = false;
			for (auto f: *s.res_EventUniv)
			  {
			    if (f.is_eventual() && f.is_universal())
			      {
				if (f.is(op::G))
				  {
				    seen_g = true;
				    eu.push_back(f.nth(0));
				  }
				else
				  {
				    eu.push_back(f);
				  }
			      }
			    else
			      {
				s.res_other->push_back(f);
			      }
			  }
			if (seen_g)
			  {
			    eu.push_back(allFG);
			    allFG = nullptr;
			    s.res_other->push_back(unop_multop(op::G, op::And,
							       eu));
			  }
			else
			  {
			    s.res_other->insert(s.res_other->end(),
						eu.begin(), eu.end());
			  }
		      }

		    // Xa & Xb & f1...fn = X(a & b & f1...fn)
		    // is built at the end of this op::And case.
		    // G(a) & G(b) = G(a & b)
		    // is built at the end of this op::And case.

		    // The following three loops perform these rewritings:
		    // (a U b) & (c U b) = (a & c) U b
		    // (a U b) & (c W b) = (a & c) U b
		    // (a W b) & (c W b) = (a & c) W b
		    // (a R b) & (a R c) = a R (b & c)
		    // (a R b) & (a M c) = a M (b & c)
		    // (a M b) & (a M c) = a M (b & c)
		    // F(a) & (a R b) = a M b
		    // F(a) & (a M b) = a M b
		    // F(b) & (a W b) = a U b
		    // F(b) & (a U b) = a U b
		    typedef std::unordered_map<formula, vec::iterator> fmap_t;
		    fmap_t uwmap; // associates "b" to "a U b" or "a W b"
		    fmap_t rmmap; // associates "a" to "a R b" or "a M b"
		    // (a U b) & (c U b) = (a & c) U b
		    // (a U b) & (c W b) = (a & c) U b
		    // (a W b) & (c W b) = (a & c) W b
		    for (auto i = s.res_U_or_W->begin();
			 i != s.res_U_or_W->end(); ++i)
		      {
			formula b = i->nth(1);
			auto j = uwmap.find(b);
			if (j == uwmap.end())
			  {
			    // First occurrence.
			    uwmap[b] = i;
			    continue;
			  }
			// We already have one occurrence.  Merge them.
			formula old = *j->second;
			op o = op::W;
			if (i->is(op::U) || old.is(op::U))
			  o = op::U;
			formula fst_arg = formula::And({old.nth(0), i->nth(0)});
			*j->second = formula::binop(o, fst_arg, b);
			assert(j->second->is(o));
			*i = nullptr;
		      }
		    // (a R b) & (a R c) = a R (b & c)
		    // (a R b) & (a M c) = a M (b & c)
		    // (a M b) & (a M c) = a M (b & c)
		    for (auto i = s.res_R_or_M->begin();
			 i != s.res_R_or_M->end(); ++i)
		      {
			formula a = i->nth(0);
			auto j = rmmap.find(a);
			if (j == rmmap.end())
			  {
			    // First occurrence.
			    rmmap[a] = i;
			    continue;
			  }
			// We already have one occurrence.  Merge them.
			formula old = *j->second;
			op o = op::R;
			if (i->is(op::M) || old.is(op::M))
			  o = op::M;
			formula snd_arg = formula::And({old.nth(1), i->nth(1)});
			*j->second = formula::binop(o, a, snd_arg);
			assert(j->second->is(o));
			*i = nullptr;
		      }
		    // F(b) & (a W b) = a U b
		    // F(b) & (a U b) = a U b
		    // F(a) & (a R b) = a M b
		    // F(a) & (a M b) = a M b
		    for (auto& f: *s.res_F)
		      {
			bool superfluous = false;
			formula c = f.nth(0);

			fmap_t::iterator j = uwmap.find(c);
			if (j != uwmap.end())
			  {
			    superfluous = true;
			    formula bo = *j->second;
			    if (bo.is(op::W))
			      {
				*j->second = formula::U(bo.nth(0), bo.nth(1));
				assert(j->second->is(op::U));
			      }
			  }
			j = rmmap.find(c);
			if (j != rmmap.end())
			  {
			    superfluous = true;
			    formula bo = *j->second;
			    if (bo.is(op::R))
			      {
				*j->second = formula::M(bo.nth(0), bo.nth(1));
				assert(j->second->is(op::M));
			      }
			  }
			if (superfluous)
			  f = nullptr;
		      }

		    s.res_other->reserve(s.res_other->size()
					 + s.res_F->size()
					 + s.res_U_or_W->size()
					 + s.res_R_or_M->size()
					 + 3);
		    s.res_other->insert(s.res_other->end(),
					s.res_F->begin(),
					s.res_F->end());
		    s.res_other->insert(s.res_other->end(),
					s.res_U_or_W->begin(),
					s.res_U_or_W->end());
		    s.res_other->insert(s.res_other->end(),
					s.res_R_or_M->begin(),
					s.res_R_or_M->end());

		    // Those "G" formulae that are eventual can be
		    // postponed inside the X term if there is one.
		    //
		    // In effect we rewrite
		    //   Xa&Xb&GFc&GFd&Ge as X(a&b&G(Fc&Fd))&Ge
		    if (!s.res_X->empty() && !opt_.favor_event_univ)
		      {
			vec event;
			for (auto& f: *s.res_G)
			  if (f.is_eventual())
			    {
			      event.push_back(f);
			      f = nullptr; // Remove it from res_G.
			    }
			s.res_X->push_back(unop_multop(op::G, op::And,
						       std::move(event)));
		      }

		    // G(a) & G(b) & ... = G(a & b & ...)
		    formula allG = unop_multop(op::G, op::And,
					       std::move(*s.res_G));
		    // Xa & Xb & ... = X(a & b & ...)
		    formula allX = unop_multop(op::X, op::And,
					       std::move(*s.res_X));
		    s.res_other->push_back(allX);
		    s.res_other->push_back(allG);
		    s.res_other->push_back(allFG);
		    formula r = formula::And(std::move(*s.res_other));
		    // If we altered the formula in some way, process
		    // it another time.
		    if (r != mo)
		      return recurse(r);
		    return r;
		  }
		case op::AndRat:
		  {
		    mospliter s(mospliter::Split_Bool, res, c_);
		    if (!s.res_Bool->empty())
		      {
			// b1 & b2 & b3 = b1 ∧ b2 ∧ b3
			formula b = formula::And(std::move(*s.res_Bool));

			vec ares;
			for (auto& f: *s.res_other)
			  switch (f.kind())
			    {
			    case op::Star:
			      // b && r[*i..j] = b & r  if i<=1<=j
			      //               = 0      otherwise
			      if (f.min() > 1 || f.max() < 1)
				return formula::ff();
			      ares.push_back(f.nth(0));
			      f = nullptr;
			      break;
			    case op::Fusion:
			      // b && {r1:..:rn} = b && r1 && .. && rn
			      for (auto ri: f)
				ares.push_back(ri);
			      f = nullptr;
			      break;
			    case op::Concat:
			      // b && {r1;...;rn} =
			      // - b && ri if there is only one ri
			      //           that does not accept [*0]
			      // - b && (r1|...|rn) if all ri
			      //           do not accept [*0]
			      // - 0 if more than one ri accept [*0]
			      {
				formula ri = nullptr;
				unsigned nonempty = 0;
				unsigned rs = f.size();
				for (unsigned j = 0; j < rs; ++j)
				  {
				    formula jf = f.nth(j);
				    if (!jf.accepts_eword())
				      {
					ri = jf;
					++nonempty;
				      }
				  }
				if (nonempty == 1)
				  {
				    ares.push_back(ri);
				  }
				else if (nonempty == 0)
				  {
				    vec sum;
				    for (auto j: f)
				      sum.push_back(j);
				    ares.emplace_back(formula::OrRat(sum));
				  }
				else
				  {
				    return formula::ff();
				  }
				f = nullptr;
				break;
			      }
			    default:
			      ares.push_back(f);
			      f = nullptr;
			      break;
			    }
			ares.push_back(b);
			auto r = formula::AndRat(std::move(ares));
			// If we altered the formula in some way, process
			// it another time.
			if (r != mo)
			  return recurse(r);
			return r;
		      }
		    // No Boolean as argument of &&.

		    // Look for occurrences of {b;r} or {b:r}.  We have
		    // {b1;r1}&&{b2;r2} = {b1&&b2};{r1&&r2}
		    //                     head1    tail1
		    // {b1:r1}&&{b2:r2} = {b1&&b2}:{r1&&r2}
		    //                     head2    tail2
		    vec head1;
		    vec tail1;
		    vec head2;
		    vec tail2;
		    for (auto& i: *s.res_other)
		      {
			if (!i)
			  continue;
			if (!i.is(op::Concat, op::Fusion))
			  continue;
			formula h = i.nth(0);
			if (!h.is_boolean())
			  continue;
			if (i.is(op::Concat))
			  {
			    head1.push_back(h);
			    tail1.push_back(i.all_but(0));
			  }
			else // op::Fusion
			  {
			    head2.push_back(h);
			    tail2.push_back(i.all_but(0));
			  }
			i = nullptr;
		      }
		    if (!head1.empty())
		      {
			formula h = formula::And(std::move(head1));
			formula t = formula::AndRat(std::move(tail1));
			s.res_other->push_back(formula::Concat({h, t}));
		      }
		    if (!head2.empty())
		      {
			formula h = formula::And(std::move(head2));
			formula t = formula::AndRat(std::move(tail2));
			s.res_other->push_back(formula::Fusion({h, t}));
		      }

		    // {r1;b1}&&{r2;b2} = {r1&&r2};{b1∧b2}
		    //                     head3    tail3
		    // {r1:b1}&&{r2:b2} = {r1&&r2}:{b1∧b2}
		    //                     head4    tail4
		    vec head3;
		    vec tail3;
		    vec head4;
		    vec tail4;
		    for (auto& i: *s.res_other)
		      {
			if (!i)
			  continue;
			if (!i.is(op::Concat, op::Fusion))
			  continue;
			unsigned s = i.size() - 1;
			formula t = i.nth(s);
			if (!t.is_boolean())
			  continue;
			if (i.is(op::Concat))
			  {
			    tail3.push_back(t);
			    head3.push_back(i.all_but(s));
			  }
			else // op::Fusion
			  {
			    tail4.push_back(t);
			    head4.push_back(i.all_but(s));
			  }
			i = nullptr;
		      }
		    if (!head3.empty())
		      {
			formula h = formula::AndRat(std::move(head3));
			formula t = formula::And(std::move(tail3));
			s.res_other->push_back(formula::Concat({h, t}));
		      }
		    if (!head4.empty())
		      {
			formula h = formula::AndRat(std::move(head4));
			formula t = formula::And(std::move(tail4));
			s.res_other->push_back(formula::Fusion({h, t}));
		      }

		    auto r = formula::AndRat(std::move(*s.res_other));
		    // If we altered the formula in some way, process
		    // it another time.
		    if (r != mo)
		      return recurse(r);
		    return r;
		  }
		case op::Or:
		  {
		    // a | X(F(a) | c...) = Fa | X(c...)
		    // a | (Xa R b) = b W a
		    // a | (Xa M b) = b U a
		    // a | (b & X(b W a)) = b W a
		    // a | (b & X(b U a)) = b U a
		    if (!mo.is_syntactic_stutter_invariant()) // Skip if no X
		      {
			typedef std::unordered_set<formula> fset_t;
			typedef std::unordered_map<formula,
						   std::set<unsigned>> fmap_t;
			fset_t xfset; // XF(...)
			fset_t xset;  // X(...)
			fmap_t rmset; // (X...)R(...) or (X...)M(...) or
				      // b & X(b W ...) or b & X(b U ...)

			std::vector<bool> tokill(mos);

			// Make a pass to search for subterms
			// of the form XFa or  X(... | F(...|a|...) | ...)
			for (unsigned n = 0; n < mos; ++n)
			  {
			    if (!res[n])
			      continue;
			    if (res[n].is_syntactic_stutter_invariant())
			      continue;

			    if (formula xarg = is_XRM(res[n]))
			      {
				rmset[xarg].insert(n);
				continue;
			      }

			    // Now we are looking for
			    // - X(...)
			    // - b & X(b W ...)
			    // - b & X(b U ...)
			    if (formula barg = is_bXbWU(res[n]))
			      {
				rmset[barg.nth(1)].insert(n);
				continue;
			      }

			    if (!res[n].is(op::X))
			      continue;

			    formula c = res[n].nth(0);

			    auto handle_F = [&xfset](formula c)
			      {
				formula a2 = c.nth(0);
				if (a2.is(op::Or))
				  for (auto c: a2)
				    xfset.insert(c);
				else
				  xfset.insert(a2);
			      };

			    if (c.is(op::F))
			      {
				handle_F(c);
			      }
			    else if (c.is(op::Or))
			      {
				for (auto cc: c)
				  if (cc.is(op::F))
				    handle_F(cc);
				  else
				    xset.insert(cc);
			      }
			    else
			      {
				xset.insert(c);
			      }
			    res[n] = nullptr;
			  }
			// Make a second pass to check if we can
			// remove all instance of XF(a).
			unsigned allofthem = xfset.size();
			vec resorig(res);
			for (unsigned n = 0; n < mos; ++n)
 			  {
			    formula x = resorig[n];
			    if (!x)
			      continue;
			    fset_t::const_iterator f = xfset.find(x);
			    if (f != xfset.end())
			      --allofthem;
			    assert(allofthem != -1U);
			    // At the same time, check if "a" can also
			    // be used to simplify "Xa R b", "Xa M b".
			    // "b & X(b W a)", or "b & X(b U a)".
			    fmap_t::const_iterator gs = rmset.find(x);
			    if (gs == rmset.end())
			      continue;
			    for (unsigned pos: gs->second)
			      {
				formula rm = resorig[pos];
				if (rm.is(op::M, op::R))
				  {
				    // a | (Xa R b) = b W a
				    // a | (Xa M b) = b U a
				    op t = rm.is(op::M) ? op::U : op::W;
				    assert(rm.nth(0).is(op::X));
				    formula a = rm.nth(0).nth(0);
				    formula b = rm.nth(1);
				    res[pos] = formula::binop(t, b, a);
				  }
				else
				  {
				    // a | (b & X(b W a)) = b W a
				    // a | (b & X(b U a)) = b U a
				    rm = is_bXbWU(resorig[pos]);
				    assert(rm);
				    res[pos] = rm;
				  }
				// Remember to kill "a".
				tokill[n] = true;
			      }
			  }

			// If we can remove all of them...
			if (allofthem == 0)
			  // Make third pass to search for terms 'a'
			  // that also appears as 'XFa'.  Replace them
			  // by 'Fa' and delete XFa.
			  for (unsigned n = 0; n < mos; ++n)
			    {
			      formula x = res[n];
			      if (!x)
				continue;
			      fset_t::const_iterator f = xfset.find(x);
			      if (f != xfset.end())
				{
				  // x can appear only once.
				  formula ff = *f;
				  xfset.erase(f);
				  res[n] = formula::F(x);
				  // We don't need to kill "a" anymore.
				  tokill[n] = false;
				}
			    }
			// Kill any remaining "a", used to simplify Xa R b
			// or Xa M b.
			for (unsigned n = 0; n < mos; ++n)
			  if (tokill[n] && res[n])
			    res[n] = nullptr;

			// Now rebuild the formula that remains.
			vec xv;
			size_t xfs = xfset.size();
			xv.reserve(xset.size() + 1);
			if (xfs > 0)
			  {
			    // Group all XF(a)|XF(b|c|...)|... as XF(a|b|c|...)
			    vec xfv;
			    xfv.reserve(xfs);
			    for (auto f: xfset)
			      xfv.push_back(f);
			    xv.push_back(unop_multop(op::F, op::Or, xfv));
			  }
			// Also gather the remaining Xa | X(b|c) as X(b|c).
			for (auto f: xset)
			  xv.push_back(f);
			res.push_back(unop_multop(op::X, op::Or, xv));
		      }

		    // Gather all operand by type.
		    mospliter s(mospliter::Strip_X |
				mospliter::Strip_GF |
				mospliter::Strip_F |
				mospliter::Split_G |
				mospliter::Split_U_or_W |
				mospliter::Split_R_or_M |
				mospliter::Split_EventUniv,
				res, c_);
		    // GF(a) | GF(b) = GF(a | b)
		    formula allGF = unop_unop_multop(op::G, op::F, op::Or,
						     std::move(*s.res_GF));

		    // Xa | Xb = X(a | b)
		    // Xa | Xb | GF(c) = X(a | b | GF(c))
		    // For Universal&Eventual formula f1...fn we also have:
		    // Xa | Xb | f1...fn = X(a | b | f1...fn)
		    if (!s.res_X->empty() && !opt_.favor_event_univ)
		      {
			s.res_X->push_back(allGF);
			allGF = nullptr;
			s.res_X->insert(s.res_X->end(),
					s.res_EventUniv->begin(),
					s.res_EventUniv->end());
		      }
		    else if (!opt_.favor_event_univ
			     && !s.res_F->empty()
			     && s.res_G->empty()
			     && s.res_U_or_W->empty()
			     && s.res_R_or_M->empty()
			     && s.res_other->empty())
		      {
			// If there is no X but some F and only
			// eventual&universal formulae f1...fn|GF(c), do:
			// Fa|Fb|f1...fn|GF(c) = F(a|b|f1...fn|GF(c))
			//
			// The reasoning here is that if we should
			// move f1...fn|GF(c) inside the "F" only
			// if it allows us to move all terms under F,
			// allowing a nice initial self-loop.
			//
			// For instance:
			//   F(a|GFb)  3st.6tr. with initial self-loop
			//   Fa|GFb    4st.8tr. without initial self-loop
			//
			// However, if other terms are presents they will
			// prevent the formation of a self-loop, and the
			// rewriting is unwelcome:
			//   F(a|GFb)|Gc  5st.11tr.  without initial self-loop
			//   Fa|GFb|Gc    5st.10tr.  without initial self-loop
			// (counting the number of "subtransitions"
			// or, degeneralizing the automaton amplifies
			// these differences)
			s.res_F->push_back(allGF);
			allGF = nullptr;
			s.res_F->insert(s.res_F->end(),
					s.res_EventUniv->begin(),
					s.res_EventUniv->end());
		      }
		    else if (opt_.favor_event_univ)
		      {
			s.res_EventUniv->push_back(allGF);
			allGF = nullptr;
			bool seen_f = false;
			if (s.res_EventUniv->size() > 1)
			  {
			    // If some of the EventUniv formulae start
			    // with an F, Gather them all under the
			    // same F.  Striping any leading F.
			    for (auto& f: *s.res_EventUniv)
			      if (f.is(op::F))
				{
				  seen_f = true;
				  f = f.nth(0);
				}
			    if (seen_f)
			      {
				formula eu =
				  unop_multop(op::F, op::Or,
					      std::move(*s.res_EventUniv));
				s.res_other->push_back(eu);
			      }
			  }
			if (!seen_f)
			  s.res_other->insert(s.res_other->end(),
					      s.res_EventUniv->begin(),
					      s.res_EventUniv->end());
		      }
		    else
		      {
			s.res_other->insert(s.res_other->end(),
					    s.res_EventUniv->begin(),
					    s.res_EventUniv->end());
		      }
		    // Xa | Xb | f1...fn = X(a | b | f1...fn)
		    // is built at the end of this multop::Or case.
		    // F(a) | F(b) = F(a | b)
		    // is built at the end of this multop::Or case.

		    // The following three loops perform these rewritings:
		    // (a U b) | (a U c) = a U (b | c)
		    // (a W b) | (a U c) = a W (b | c)
		    // (a W b) | (a W c) = a W (b | c)
		    // (a R b) | (c R b) = (a | c) R b
		    // (a R b) | (c M b) = (a | c) R b
		    // (a M b) | (c M b) = (a | c) M b
		    // G(a) | (a U b) = a W b
		    // G(a) | (a W b) = a W b
		    // G(b) | (a R b) = a R b.
		    // G(b) | (a M b) = a R b.
		    typedef std::unordered_map<formula, vec::iterator> fmap_t;
		    fmap_t uwmap; // associates "a" to "a U b" or "a W b"
		    fmap_t rmmap; // associates "b" to "a R b" or "a M b"
		    // (a U b) | (a U c) = a U (b | c)
		    // (a W b) | (a U c) = a W (b | c)
		    // (a W b) | (a W c) = a W (b | c)
		    for (auto i = s.res_U_or_W->begin();
			 i != s.res_U_or_W->end(); ++i)
		      {
			formula a = i->nth(0);
			auto j = uwmap.find(a);
			if (j == uwmap.end())
			  {
			    // First occurrence.
			    uwmap[a] = i;
			    continue;
			  }
			// We already have one occurrence.  Merge them.
			formula old = *j->second;
			op o = op::U;
			if (i->is(op::W) || old.is(op::W))
			  o = op::W;
			formula snd_arg = formula::Or({old.nth(1), i->nth(1)});
			*j->second = formula::binop(o, a, snd_arg);
			assert(j->second->is(o));
			*i = nullptr;
		      }
		    // (a R b) | (c R b) = (a | c) R b
		    // (a R b) | (c M b) = (a | c) R b
		    // (a M b) | (c M b) = (a | c) M b
		    for (auto i = s.res_R_or_M->begin();
			 i != s.res_R_or_M->end(); ++i)
		      {
			formula b = i->nth(1);
			auto j = rmmap.find(b);
			if (j == rmmap.end())
			  {
			    // First occurrence.
			    rmmap[b] = i;
			    continue;
			  }
			// We already have one occurrence.  Merge them.
			formula old = *j->second;
			op o = op::M;
			if (i->is(op::R) || old.is(op::R))
			  o = op::R;
			formula fst_arg = formula::Or({old.nth(0), i->nth(0)});
			*j->second = formula::binop(o, fst_arg, b);
			assert(j->second->is(o));
			*i = nullptr;
		      }
		    // G(a) | (a U b) = a W b
		    // G(a) | (a W b) = a W b
		    // G(b) | (a R b) = a R b.
		    // G(b) | (a M b) = a R b.
		    for (auto& f: *s.res_G)
		      {
			bool superfluous = false;
			formula c = f.nth(0);

			fmap_t::iterator j = uwmap.find(c);
			if (j != uwmap.end())
			  {
			    superfluous = true;
			    formula bo = *j->second;
			    if (bo.is(op::U))
			      {
				*j->second = formula::W(bo.nth(0), bo.nth(1));
				assert(j->second->is(op::W));
			      }
			  }
			j = rmmap.find(c);
			if (j != rmmap.end())
			  {
			    superfluous = true;
			    formula bo = *j->second;
			    if (bo.is(op::M))
			      {
				*j->second = formula::R(bo.nth(0), bo.nth(1));
				assert(j->second->is(op::R));
			      }
			  }
			if (superfluous)
			  f = nullptr;
		      }

		    s.res_other->reserve(s.res_other->size()
					 + s.res_G->size()
					 + s.res_U_or_W->size()
					 + s.res_R_or_M->size()
					 + 3);
		    s.res_other->insert(s.res_other->end(),
					s.res_G->begin(),
					s.res_G->end());
		    s.res_other->insert(s.res_other->end(),
					s.res_U_or_W->begin(),
					s.res_U_or_W->end());
		    s.res_other->insert(s.res_other->end(),
					s.res_R_or_M->begin(),
					s.res_R_or_M->end());

		    // Those "F" formulae that are universal can be
		    // postponed inside the X term if there is one.
		    //
		    // In effect we rewrite
		    //   Xa|Xb|FGc|FGd|Fe as X(a|b|F(Gc|Gd))|Fe
		    if (!s.res_X->empty())
		      {
			vec univ;
			for (auto& f: *s.res_F)
			  if (f.is_universal())
			    {
			      univ.push_back(f);
			      f = nullptr; // Remove it from res_F.
			    }
			s.res_X->push_back(unop_multop(op::F, op::Or,
						       std::move(univ)));
		      }

		    // F(a) | F(b) | ... = F(a | b | ...)
		    formula allF = unop_multop(op::F, op::Or,
					       std::move(*s.res_F));
		    // Xa | Xb | ... = X(a | b | ...)
		    formula allX = unop_multop(op::X, op::Or,
					       std::move(*s.res_X));
		    s.res_other->push_back(allX);
		    s.res_other->push_back(allF);
		    s.res_other->push_back(allGF);
		    formula r = formula::Or(std::move(*s.res_other));
		    // If we altered the formula in some way, process
		    // it another time.
		    if (r != mo)
		      return recurse(r);
		    return r;
		  }
		case op::AndNLM:
		  {
		    mospliter s(mospliter::Split_Bool, res, c_);
		    if (!s.res_Bool->empty())
		      {
			// b1 & b2 & b3 = b1 ∧ b2 ∧ b3
			formula b = formula::And(std::move(*s.res_Bool));

			// now we just consider  b & rest
			formula rest = formula::AndNLM(std::move(*s.res_other));

			// We have  b & rest = b : rest  if rest does not
			// accept [*0]. Otherwise  b & rest = b | (b : rest)
			// FIXME: It would be nice to remove [*0] from rest.
			formula r = nullptr;
			if (rest.accepts_eword())
			  {
			    // The b & rest = b | (b : rest) rewriting
			    // augment the size, so do that only when
			    // explicitly requested.
			    if (!opt_.reduce_size_strictly)
			      return recurse(formula::OrRat
					     ({b, formula::Fusion({b, rest})}));
			    else
			      return mo;
			  }
			else
			  {
			    return recurse(formula::Fusion({b, rest}));
			  }
		      }
		    // No Boolean as argument of &&.

		    // Look for occurrences of {b;r} or {b:r}.  We have
		    // {b1;r1}&{b2;r2} = {b1∧b2};{r1&r2}
		    //                    head1   tail1
		    // {b1:r1}&{b2:r2} = {b1∧b2}:{r1&r2}
		    //                    head2   tail2
		    // BEWARE: The second rule is correct only when
		    // both r1 and r2 do not accept [*0].

		    vec head1;
		    vec tail1;
		    vec head2;
		    vec tail2;
		    for (auto& i: *s.res_other)
		      {
			if (!i)
			  continue;
			if (!i.is(op::Concat, op::Fusion))
			  continue;
			formula h = i.nth(0);
			if (!h.is_boolean())
			  continue;
			if (i.is(op::Concat))
			  {
			    head1.push_back(h);
			    tail1.push_back(i.all_but(0));
			  }
			else // op::Fusion
			  {
			    formula t = i.all_but(0);
			    if (t.accepts_eword())
			      continue;
			    head2.push_back(h);
			    tail2.push_back(t);
			  }
			i = nullptr;
		      }
		    if (!head1.empty())
		      {
			formula h = formula::And(std::move(head1));
			formula t = formula::AndNLM(std::move(tail1));
			s.res_other->push_back(formula::Concat({h, t}));
		      }
		    if (!head2.empty())
		      {
			formula h = formula::And(std::move(head2));
			formula t = formula::AndNLM(std::move(tail2));
			s.res_other->push_back(formula::Fusion({h, t}));
		      }

		    formula r = formula::AndNLM(std::move(*s.res_other));
		    // If we altered the formula in some way, process
		    // it another time.
		    if (r != mo)
		      return recurse(r);
		    return r;
		  }
		case op::OrRat:
		case op::Concat:
		case op::Fusion:
		  // FIXME: No simplifications yet.
		  return mo;
		default:
		  SPOT_UNIMPLEMENTED();
		  return nullptr;
		}
	      SPOT_UNREACHABLE();
	    }
	  return mo;
	}

      protected:
	ltl_simplifier_cache* c_;
	const ltl_simplifier_options& opt_;
      };


      formula
      simplify_recursively(formula f,
			   ltl_simplifier_cache* c)
      {
#ifdef TRACE
	static int srec = 0;
	for (int i = srec; i; --i)
	  trace << ' ';
	trace << "** simplify_recursively(" << str_psl(f) << ')';
#endif

	formula result = c->lookup_simplified(f);
	if (result)
	  {
	    trace << " cached: " << str_psl(result) << std::endl;
	    return result;
	  }
	else
	  {
	    trace << " miss" << std::endl;
	  }

#ifdef TRACE
	++srec;
#endif

	if (f.is_boolean() && c->options.boolean_to_isop)
	  {
	    result = c->boolean_to_isop(f);
	  }
	else
	  {
	    simplify_visitor v(c);
	    result = v.visit(f);
	  }

#ifdef TRACE
	--srec;
	for (int i = srec; i; --i)
	  trace << ' ';
        trace << "** simplify_recursively(" << str_psl(f) << ") result: "
	      << str_psl(result) << std::endl;
#endif

	c->cache_simplified(f, result);
	return result;
      }

    } // anonymous namespace

    //////////////////////////////////////////////////////////////////////
    // ltl_simplifier_cache


    // This implements the recursive rules for syntactic implication.
    // (To follow this code please look at the table given as an
    // appendix in the documentation for temporal logic operators.)
    inline
    bool
    ltl_simplifier_cache::syntactic_implication_aux(formula f, formula g)
    {
      // We first process all lines from the table except the
      // first two, and then we process the first two as a fallback.
      //
      // However for Boolean formulas we skip the bottom lines
      // (keeping only the first one) to prevent them from being
      // further split.
      if (!f.is_boolean())
	// Deal with all lines of the table except the first two.
	switch (f.kind())
	  {
	  case op::X:
	    if (g.is_eventual() && syntactic_implication(f.nth(0), g))
	      return true;
	    if (g.is(op::X) && syntactic_implication(f.nth(0), g.nth(0)))
	      return true;
	    break;

	  case op::F:
	    if (g.is_eventual() && syntactic_implication(f.nth(0), g))
	      return true;
	    break;

	  case op::G:
	    if (g.is(op::U, op::R) && syntactic_implication(f.nth(0), g.nth(1)))
	      return true;
	    if (g.is(op::W) && (syntactic_implication(f.nth(0), g.nth(0))
				|| syntactic_implication(f.nth(0), g.nth(1))))
	      return true;
	    if (g.is(op::M) && (syntactic_implication(f.nth(0), g.nth(0))
				&& syntactic_implication(f.nth(0), g.nth(1))))
	      return true;
	    // First column.
	    if (syntactic_implication(f.nth(0), g))
	      return true;
	    break;

	  case op::U:
	    {
	      formula f1 = f.nth(0);
	      formula f2 = f.nth(1);
	      if (g.is(op::U, op::W)
		  && syntactic_implication(f1, g.nth(0))
		  && syntactic_implication(f2, g.nth(1)))
		return true;
	      if (g.is(op::M, op::R)
		  && syntactic_implication(f1, g.nth(1))
		  && syntactic_implication(f2, g.nth(0))
		  && syntactic_implication(f2, g.nth(1)))
		return true;
	      if (g.is(op::F) && syntactic_implication(f2, g.nth(0)))
		return true;
	      // First column.
	      if (syntactic_implication(f1, g) && syntactic_implication(f2, g))
		return true;
	      break;
	    }
	  case op::W:
	    {
	      formula f1 = f.nth(0);
	      formula f2 = f.nth(1);
	      if (g.is(op::U) && (syntactic_implication(f1, g.nth(1))
				  && syntactic_implication(f2, g.nth(1))))
		return true;
	      if (g.is(op::W) && (syntactic_implication(f1, g.nth(0))
				  && syntactic_implication(f2, g.nth(1))))
		return true;
	      if (g.is(op::R) && (syntactic_implication(f1, g.nth(1))
				  && syntactic_implication(f2, g.nth(0))
				  && syntactic_implication(f2, g.nth(1))))
		return true;
	      if (g.is(op::F) && (syntactic_implication(f1, g.nth(0))
				  && syntactic_implication(f2, g.nth(0))))
		return true;
	      // First column.
	      if (syntactic_implication(f1, g) && syntactic_implication(f2, g))
		return true;
	      break;
	    }
	  case op::R:
	    {
	      formula f1 = f.nth(0);
	      formula f2 = f.nth(1);
	      if (g.is(op::W) && (syntactic_implication(f1, g.nth(1))
				  && syntactic_implication(f2, g.nth(0))))
		return true;
	      if (g.is(op::R) && (syntactic_implication(f1, g.nth(0))
				  && syntactic_implication(f2, g.nth(1))))
		return true;
	      if (g.is(op::M) && (syntactic_implication(f2, g.nth(0))
				  && syntactic_implication(f2, g.nth(1))))
		return true;
	      if (g.is(op::F) && syntactic_implication(f2, g.nth(0)))
		return true;
	      // First column.
	      if (syntactic_implication(f2, g))
		return true;
	      break;
	    }
	  case op::M:
	    {
	      formula f1 = f.nth(0);
	      formula f2 = f.nth(1);
	      if (g.is(op::U, op::W) && (syntactic_implication(f1, g.nth(1))
					 && syntactic_implication(f2,
								  g.nth(0))))
		return true;
	      if (g.is(op::R, op::M) && (syntactic_implication(f1, g.nth(0))
					 && syntactic_implication(f2,
								  g.nth(1))))
		return true;
	      if (g.is(op::F) && (syntactic_implication(f1, g.nth(0))
				  || syntactic_implication(f2, g.nth(0))))
		return true;
	      // First column.
	      if (syntactic_implication(f2, g))
		return true;
	      break;
	    }
	  case op::Or:
	    {
	      // If we are checking something like
	      //   (a | b | Xc) => g,
	      // split it into
	      //   (a | b) => g
	      //   Xc      => g
	      unsigned i = 0;
	      if (formula bops = f.boolean_operands(&i))
		if (!syntactic_implication(bops, g))
		  break;
	      bool b = true;
	      unsigned fs = f.size();
	      for (; i < fs; ++i)
		if (!syntactic_implication(f.nth(i), g))
		  {
		    b = false;
		    break;
		  }
	      if (b)
		return true;
	      break;
	    }
	  case op::And:
	    {
	      // If we are checking something like
	      //   (a & b & Xc) => g,
	      // split it into
	      //   (a & b) => g
	      //   Xc      => g
	      unsigned i = 0;
	      if (formula bops = f.boolean_operands(&i))
		if (syntactic_implication(bops, g))
		  return true;
	      unsigned fs = f.size();
	      for (; i < fs; ++i)
		if (syntactic_implication(f.nth(i), g))
		  return true;
	      break;
	    }
	  default:
	    break;
	  }
      // First two lines of the table.
      // (Don't check equality, it has already be done.)
      if (!g.is_boolean())
	switch (g.kind())
	  {
	  case op::F:
	    if (syntactic_implication(f, g.nth(0)))
	      return true;
	    break;

	  case op::G:
	  case op::X:
	    if (f.is_universal() && syntactic_implication(f, g.nth(0)))
	      return true;
	    break;

	  case op::U:
	  case op::W:
	    if (syntactic_implication(f, g.nth(1)))
	      return true;
	    break;

	  case op::M:
	  case op::R:
	    if (syntactic_implication(f, g.nth(0))
		&& syntactic_implication(f, g.nth(1)))
	      return true;
	    break;

	  case op::And:
	    {
	      // If we are checking something like
	      //   f => (a & b & Xc),
	      // split it into
	      //   f => (a & b)
	      //   f => Xc
	      unsigned i = 0;
	      if (formula bops = g.boolean_operands(&i))
		if (!syntactic_implication(f, bops))
		  break;
	      bool b = true;
	      unsigned gs = g.size();
	      for (; i < gs; ++i)
		if (!syntactic_implication(f, g.nth(i)))
		  {
		    b = false;
		    break;
		  }
	      if (b)
		return true;
	      break;
	    }

	  case op::Or:
	    {
	      // If we are checking something like
	      //   f => (a | b | Xc),
	      // split it into
	      //   f => (a | b)
	      //   f => Xc
	      unsigned i = 0;
	      if (formula bops = g.boolean_operands(&i))
		if (syntactic_implication(f, bops))
		  return true;
	      unsigned gs = g.size();
	      for (; i < gs; ++i)
		if (syntactic_implication(f, g.nth(i)))
		  return true;
	      break;
	    }
	  default:
	    break;
	  }
      return false;
    }

    // Return true if f => g syntactically
    bool
    ltl_simplifier_cache::syntactic_implication(formula f,
						formula g)
    {
      // We cannot run syntactic_implication on SERE formulae,
      // except on Boolean formulae.
      if (f.is_sere_formula() && !f.is_boolean())
	return false;
      if (g.is_sere_formula() && !g.is_boolean())
	return false;

      if (f == g)
	return true;
      if (g.is(op::True) || f.is(op::False))
	return true;
      if (g.is(op::False) || f.is(op::True))
	return false;

      // Often we compare a literal (an atomic_prop or its negation)
      // to another literal.  The result is necessarily false. To be
      // true, the two literals would have to be equal, but we have
      // already checked that.
      if (f.is_literal() && g.is_literal())
	return false;

      // Cache lookup
      {
	pairf p(f, g);
	syntimpl_cache_t::const_iterator i = syntimpl_.find(p);
	if (i != syntimpl_.end())
	  return i->second;
      }

      bool result;

      if (f.is_boolean() && g.is_boolean())
	result = bdd_implies(as_bdd(f), as_bdd(g));
      else
	result = syntactic_implication_aux(f, g);

      // Cache result
      {
	pairf p(f, g);
	syntimpl_[p] = result;
	// std::cerr << str_psl(f) << (result ? " ==> " : " =/=> ")
	//           << str_psl(g) << std::endl;
      }

      return result;
    }

    // If right==false, true if !f1 => f2, false otherwise.
    // If right==true, true if f1 => !f2, false otherwise.
    bool
    ltl_simplifier_cache::syntactic_implication_neg(formula f1,
						    formula f2,
						    bool right)
    {
      // We cannot run syntactic_implication_neg on SERE formulae,
      // except on Boolean formulae.
      if (f1.is_sere_formula() && !f1.is_boolean())
	return false;
      if (f2.is_sere_formula() && !f2.is_boolean())
	return false;
      if (right)
	f2 = nenoform_rec(f2, true, this);
      else
	f1 = nenoform_rec(f1, true, this);
      return syntactic_implication(f1, f2);
    }


    /////////////////////////////////////////////////////////////////////
    // ltl_simplifier

    ltl_simplifier::ltl_simplifier(const bdd_dict_ptr& d)
    {
      cache_ = new ltl_simplifier_cache(d);
    }

    ltl_simplifier::ltl_simplifier(const ltl_simplifier_options& opt,
				   bdd_dict_ptr d)
    {
      cache_ = new ltl_simplifier_cache(d, opt);
    }

    ltl_simplifier::~ltl_simplifier()
    {
      delete cache_;
    }

    formula
    ltl_simplifier::simplify(formula f)
    {
      if (!f.is_in_nenoform())
	f = negative_normal_form(f, false);
      return simplify_recursively(f, cache_);
    }

    formula
    ltl_simplifier::negative_normal_form(formula f, bool negated)
    {
      return nenoform_rec(f, negated, cache_);
    }

    bool
    ltl_simplifier::syntactic_implication(formula f1, formula f2)
    {
      return cache_->syntactic_implication(f1, f2);
    }

    bool
    ltl_simplifier::syntactic_implication_neg(formula f1,
					      formula f2, bool right)
    {
      return cache_->syntactic_implication_neg(f1, f2, right);
    }

    bool
    ltl_simplifier::are_equivalent(formula f, formula g)
    {
      return cache_->lcc.equal(f, g);
    }

    bool
    ltl_simplifier::implication(formula f, formula g)
    {
      return cache_->lcc.contained(f, g);
    }

    bdd
    ltl_simplifier::as_bdd(formula f)
    {
      return cache_->as_bdd(f);
    }

    formula
    ltl_simplifier::star_normal_form(formula f)
    {
      return cache_->star_normal_form(f);
    }

    formula
    ltl_simplifier::boolean_to_isop(formula f)
    {
      return cache_->boolean_to_isop(f);
    }

    bdd_dict_ptr
    ltl_simplifier::get_dict() const
    {
      return cache_->dict;
    }

    void
    ltl_simplifier::print_stats(std::ostream& os) const
    {
      cache_->print_stats(os);
    }

    void
    ltl_simplifier::clear_as_bdd_cache()
    {
      cache_->clear_as_bdd_cache();
      cache_->lcc.clear();
    }
  }
}