invelm_algorithm.h

Go to the documentation of this file.

// Author(s): Luc Engelen, Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_LPS_INVELM_ALGORITHM_H
#define MCRL2_LPS_INVELM_ALGORITHM_H
 
#include "mcrl2/data/parse.h"
#include "mcrl2/lps/detail/lps_algorithm.h"
#include "mcrl2/lps/invariant_checker.h"
 
namespace mcrl2
{
 
namespace lps
{
 
 
template <class Specification>
class invelm_algorithm: public detail::lps_algorithm<Specification>
{
  typedef typename detail::lps_algorithm<Specification> super;
  typedef typename Specification::process_type process_type;
  typedef typename process_type::action_summand_type action_summand_type;
  using super::m_spec;
 
  private:
    data::detail::BDD_Prover f_bdd_prover;
    bool f_simplify_all;
 
    void simplify_summand(summand_base& s, const data::data_expression& invariant, bool apply_prover)
    {
      data::data_expression new_condition = data::lazy::and_(invariant, s.condition());
 
      if (apply_prover)
      {
        f_bdd_prover.set_formula(new_condition);
        new_condition = f_bdd_prover.get_bdd();
      }
      if (f_simplify_all || data::sort_bool::is_false_function_symbol(new_condition))
      {
        s.condition() = new_condition;
      }
    }
 
    template <typename SummandSequence>
    void simplify_summands(SummandSequence& summands, const data::data_expression& invariant, bool apply_prover)
    {
      for (summand_base& s: summands)
      {
        simplify_summand(s, invariant, apply_prover);
      }
    }
 
  public:
    invelm_algorithm(
      Specification& a_lps,
      const data::rewriter::strategy a_rewrite_strategy = data::jitty,
      const int a_time_limit = 0,
      const bool a_path_eliminator = false,
      const data::detail::smt_solver_type a_solver_type = data::detail::solver_type_cvc,
      const bool a_apply_induction = false,
      const bool a_simplify_all = false
    )
      : detail::lps_algorithm<Specification>(a_lps),
        f_bdd_prover(a_lps.data(), data::used_data_equation_selector(a_lps.data()),a_rewrite_strategy, a_time_limit, a_path_eliminator, a_solver_type, a_apply_induction),
        f_simplify_all(a_simplify_all)
    {}
 
    void run(const data::data_expression& invariant, bool apply_prover)
    {
      simplify_summands(m_spec.process().action_summands(), invariant, apply_prover);
      simplify_summands(m_spec.process().deadlock_summands(), invariant, apply_prover);
      super::remove_trivial_summands();
    }
};
 
} // namespace lps
 
} // namespace mcrl2
 
#endif // MCRL2_LPS_INVELM_ALGORITHM_H