simplify.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <spot/tl/formula.hh>
#include <bddx.h>
#include <spot/twa/bdddict.hh>
#include <iosfwd>
 
namespace spot
{
  // forward declaration
  class option_map;
 
  class SPOT_API tl_simplifier_options
  {
  public:
    tl_simplifier_options(bool basics = true,
                          bool synt_impl = true,
                          bool event_univ = true,
                          bool containment_checks = false,
                          bool containment_checks_stronger = false,
                          bool nenoform_stop_on_boolean = false,
                          bool reduce_size_strictly = false,
                          bool boolean_to_isop = false,
                          bool favor_event_univ = false,
                          bool keep_top_xor = false,
                          bool unit_prop = false)
      : reduce_basics(basics),
        synt_impl(synt_impl),
        event_univ(event_univ),
        containment_checks(containment_checks),
        containment_checks_stronger(containment_checks_stronger),
        nenoform_stop_on_boolean(nenoform_stop_on_boolean),
        reduce_size_strictly(reduce_size_strictly),
        boolean_to_isop(boolean_to_isop),
        favor_event_univ(favor_event_univ),
        keep_top_xor(keep_top_xor),
        unit_prop(unit_prop)
    {
    }
 
    tl_simplifier_options(int level) :
      tl_simplifier_options(false, false, false)
    {
      switch (level)
        {
        case 3:
          containment_checks = true;
          containment_checks_stronger = true;
          SPOT_FALLTHROUGH;
        case 2:
          synt_impl = true;
          SPOT_FALLTHROUGH;
        case 1:
          reduce_basics = true;
          event_univ = true;
          SPOT_FALLTHROUGH;
        default:
          break;
        }
    }
 
    bool reduce_basics;      
    bool synt_impl;          
    bool event_univ;         
    bool containment_checks; 
    bool containment_checks_stronger; 
    bool nenoform_stop_on_boolean;
    bool reduce_size_strictly;
    bool boolean_to_isop;
    bool favor_event_univ;
    bool keep_top_xor;
    bool unit_prop;
    unsigned containment_max_states = 0;
    unsigned containment_max_ops = 16;
 
    bool is_enabled() const
    {
      return reduce_basics || synt_impl || event_univ
        || containment_checks || containment_checks_stronger
        || nenoform_stop_on_boolean || reduce_size_strictly
        || boolean_to_isop || favor_event_univ || keep_top_xor
        || unit_prop;
    }
 
    void save_to_option_map(option_map& om, const char* prefix) const;
 
    bool load_from_option_map(const option_map& om, const char* prefix);
  };
 
  // fwd declaration to hide technical details.
  class tl_simplifier_cache;
 
  class SPOT_API tl_simplifier
  {
  public:
    tl_simplifier(const bdd_dict_ptr& dict = make_bdd_dict());
    tl_simplifier(const tl_simplifier_options& opt,
                   bdd_dict_ptr dict = make_bdd_dict());
    ~tl_simplifier();
 
    formula simplify(formula f);
 
#ifndef SWIG
    tl_simplifier_options& options();
#endif
 
    formula
      negative_normal_form(formula f, bool negated = false);
 
    bool syntactic_implication(formula f, formula g);
    bool syntactic_implication_neg(formula f, formula g,
                                   bool right);
 
    bool are_equivalent(formula f, formula g);
 
 
    bool implication(formula f, formula g);
 
    bdd as_bdd(formula f);
 
    void clear_as_bdd_cache();
 
    void clear_caches();
 
    bdd_dict_ptr get_dict() const;
 
    formula star_normal_form(formula f);
 
    formula boolean_to_isop(formula f);
 
    void print_stats(std::ostream& os) const;
 
  private:
    tl_simplifier_cache* cache_;
    // Copy disallowed.
    tl_simplifier(const tl_simplifier&) = delete;
    void operator=(const tl_simplifier&) = delete;
  };
 
 
  SPOT_API formula normalize_quantifiers(formula);
}