pres_equation.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote. Based on pbes_equation.h by 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_PRES_PRES_EQUATION_H
#define MCRL2_PRES_PRES_EQUATION_H
 
#include "mcrl2/data/detail/sequence_algorithm.h"
#include "mcrl2/pbes/fixpoint_symbol.h"
#include "mcrl2/pres/pres_expression.h"
 
namespace mcrl2
{
 
namespace pres_system
{
 
typedef pbes_system::fixpoint_symbol fixpoint_symbol;
 
class pres_equation;
atermpp::aterm pres_equation_to_aterm(const pres_equation& eqn);
bool is_well_typed(const pres_equation& eqn);
bool has_propositional_variables(const pres_expression& x);
 
class pres_equation
{
  protected:
    fixpoint_symbol m_symbol;
 
    propositional_variable m_variable;
 
    pres_expression m_formula;
 
  public:
    typedef pres_expression term_type;
 
    typedef propositional_variable variable_type;
 
    typedef fixpoint_symbol symbol_type;
 
    pres_equation() = default;
 
    pres_equation(const fixpoint_symbol& symbol, const propositional_variable& variable, const pres_expression& expr)
      :
      m_symbol(symbol),
      m_variable(variable),
      m_formula(expr)
    {
    }
 
    const fixpoint_symbol& symbol() const
    {
      return m_symbol;
    }
 
    fixpoint_symbol& symbol()
    {
      return m_symbol;
    }
 
    const propositional_variable& variable() const
    {
      return m_variable;
    }
 
    propositional_variable& variable()
    {
      return m_variable;
    }
 
    const pres_expression& formula() const
    {
      return m_formula;
    }
 
    pres_expression& formula()
    {
      return m_formula;
    }
 
    // (Comment Wieger: is_const would be a better name)
    bool is_solved() const;
 
    void swap(pres_equation& other)
    {
      using std::swap;
      swap(m_symbol, other.m_symbol);
      swap(m_variable, other.m_variable);
      swap(m_formula, other.m_formula);
    }
   
    void mark(std::stack<std::reference_wrapper<atermpp::detail::_aterm>>& todo) const
    {
      mark_term(m_symbol, todo);
    }
};
 
//--- start generated class pres_equation ---//
typedef atermpp::term_list<pres_equation> pres_equation_list;
 
typedef std::vector<pres_equation>    pres_equation_vector;
 
// prototype declaration
std::string pp(const pres_equation& x);
 
inline
std::ostream& operator<<(std::ostream& out, const pres_equation& x)
{
  return out << pres_system::pp(x);
}
 
inline void swap(pres_equation& t1, pres_equation& t2)
{
  t1.swap(t2);
}
//--- end generated class pres_equation ---//
 
inline bool
operator==(const pres_equation& x, const pres_equation& y)
{
  return x.symbol() == y.symbol() &&
         x.variable() == y.variable() &&
         x.formula() == y.formula();
}
 
inline bool
operator!=(const pres_equation& x, const pres_equation& y)
{
  return !(x == y);
}
 
inline
atermpp::aterm pres_equation_to_aterm(const pres_equation& eqn)
{
  return atermpp::aterm(core::detail::function_symbol_PREqn(), eqn.symbol(), eqn.variable(), eqn.formula());
}
 
// Overload for pp for propositional variables.
std::string pp(const propositional_variable& v);
 
// template function overloads
std::string pp(const pres_equation_vector& x);
void normalize_sorts(pres_equation_vector& x, const data::sort_specification& sortspec);
std::set<data::variable> find_free_variables(const pres_system::pres_equation& x);
 
} // namespace pres_system
 
} // namespace mcrl2
 
#endif // MCRL2_PRES_PRES_EQUATION_H