mutable_map_substitution.h

Go to the documentation of this file.

// Author(s): Jeroen van der Wulp, 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_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
#define MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H
 
#include "mcrl2/data/is_simple_substitution.h"
#include "mcrl2/data/undefined.h"
 
namespace mcrl2 {
 
namespace data {
 
template <typename AssociativeContainer = std::map<variable,data_expression> >
class mutable_map_substitution
{
protected:
  AssociativeContainer m_map;
 
public:
  typedef typename AssociativeContainer::key_type variable_type;
  typedef typename AssociativeContainer::mapped_type expression_type;
  typedef typename AssociativeContainer::const_iterator const_iterator;
  typedef typename AssociativeContainer::iterator iterator;
  using argument_type = variable_type;
  using result_type = expression_type;
 
  struct assignment
  {
    typename AssociativeContainer::key_type m_variable;
    AssociativeContainer&                   m_map;
 
    assignment(typename AssociativeContainer::key_type v, AssociativeContainer& m) :
      m_variable(v), m_map(m)
    { }
 
    template <typename AssignableToExpression>
    assignment& operator=(AssignableToExpression const& e)
    {
      mCRL2log(log::trace) << "Setting " << m_variable << " := " << e << std::endl;
      if (e != m_variable)
      {
        m_map[m_variable] = e;
      }
      else
      {
        m_map.erase(m_variable);
      }
      return *this;
    }
  };
 
  mutable_map_substitution() = default;
 
  explicit mutable_map_substitution(const AssociativeContainer& m)
    : m_map(m)
  {}
 
  template <typename VariableContainer, typename ExpressionContainer>
  mutable_map_substitution(VariableContainer const& variables, ExpressionContainer const& expressions)
  {
    assert(variables.size() == expressions.size());
    auto j = expressions.begin();
    for (auto i = variables.begin(); i != variables.end(); ++i, ++j)
    {
      m_map[*i] = *j;
    }
  }
 
  expression_type operator()(const variable_type& v) const
  {
    auto i = m_map.find(v);
    if (i == m_map.end())
    {
      return v;
    }
    else
    {
      return i->second;
    }
  }
 
  assignment operator[](variable_type const& v)
  {
    return assignment(v, this->m_map);
  }
 
  void clear()
  {
    m_map.clear();
  }
 
  template <typename Substitution>
  bool operator==(const Substitution&) const
  {
    return false;
  }
 
  const_iterator begin() const
  {
    return m_map.begin();
  }
 
  const_iterator end() const
  {
    return m_map.end();
  }
 
  iterator begin()
  {
    return this->m_map.begin();
  }
 
  iterator end()
  {
    return this->m_map.end();
  }
 
  bool empty() const
  {
    return m_map.empty();
  }
 
  std::string to_string() const
  {
    std::stringstream result;
    result << "[";
    for (auto i = begin(); i != end(); ++i)
    {
      result << (i == begin() ? "" : "; ") << i->first << ":" << i->first.sort() << " := " << i->second;
    }
    result << "]";
    return result.str();
  }
 
  iterator find(variable_type const& v)
  {
    return this->m_map.find(v);
  }
 
  const_iterator find(variable_type const& v) const
  {
    return m_map.find(v);
  }
};
 
template <typename VariableContainer, typename ExpressionContainer, typename MapContainer>
mutable_map_substitution<MapContainer>
make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
{
  return mutable_map_substitution<MapContainer>(vc, ec);
}
 
template <typename VariableContainer, typename ExpressionContainer>
mutable_map_substitution<std::map<typename VariableContainer::value_type, typename ExpressionContainer::value_type> >
make_mutable_map_substitution(const VariableContainer& vc, const ExpressionContainer& ec)
{
  return mutable_map_substitution<std::map<typename VariableContainer::value_type, typename ExpressionContainer::value_type> >(vc, ec);
}
 
template <typename AssociativeContainer>
std::ostream& operator<<(std::ostream& out, const mutable_map_substitution<AssociativeContainer>& sigma)
{
  return out << sigma.to_string();
}
 
std::set<data::variable> substitution_variables(const mutable_map_substitution<>& sigma);
 
template <typename AssociativeContainer>
bool is_simple_substitution(const mutable_map_substitution<AssociativeContainer>& sigma)
{
  for (auto i = sigma.begin(); i != sigma.end(); ++i)
  {
    if (!is_simple_substitution(i->first, i->second))
    {
      return false;
    }
  }
  return true;
}
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_SUBSTITUTIONS_MUTABLE_MAP_SUBSTITUTION_H