Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/detail/pbes_context.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_PBES_CONTEXT_H
      13             : #define MCRL2_PBES_DETAIL_PBES_CONTEXT_H
      14             : 
      15             : #include "mcrl2/data/detail/data_utility.h"
      16             : #include "mcrl2/pbes/propositional_variable.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : class pbes_context
      25             : {
      26             :   private:
      27             :     std::map<core::identifier_string, propositional_variable> m_propositional_variables;
      28             : 
      29             :   public:
      30        1254 :     bool is_declared(const core::identifier_string& name) const
      31             :     {
      32        1254 :       return m_propositional_variables.find(name) != m_propositional_variables.end();
      33             :     }
      34             : 
      35        1254 :     data::sort_expression_list propositional_variable_sorts(const core::identifier_string& name) const
      36             :     {
      37        1254 :       auto i = m_propositional_variables.find(name);
      38        1254 :       assert(i != m_propositional_variables.end());
      39        2508 :       return data::detail::parameter_sorts(i->second.parameters());
      40             :     }
      41             : 
      42             :     template <typename PropositionalVariableContainer>
      43         468 :     void add_propositional_variables(const PropositionalVariableContainer& propositional_variables, const data::sort_type_checker& sort_typechecker)
      44             :     {
      45        3333 :       for (const propositional_variable& p: propositional_variables)
      46             :       {
      47       11156 :         for (const data::variable& v: p.parameters())
      48             :         {
      49        5426 :           sort_typechecker(v.sort());
      50             :         }
      51             : 
      52        2865 :         auto i = m_propositional_variables.find(p.name());
      53        2865 :         if (i == m_propositional_variables.end())
      54             :         {
      55        2865 :           m_propositional_variables[p.name()] = p;
      56             :         }
      57             :         else
      58             :         {
      59           0 :           throw mcrl2::runtime_error("attempt to overload propositional variable " + core::pp(p.name()));
      60             :         }
      61             :       }
      62         468 :     }
      63             : 
      64         467 :     void clear()
      65             :     {
      66         467 :       m_propositional_variables.clear();
      67         467 :     }
      68             : };
      69             : 
      70             : } // namespace detail
      71             : 
      72             : } // namespace pbes_system
      73             : 
      74             : } // namespace mcrl2
      75             : 
      76             : #endif // MCRL2_PBES_DETAIL_PBES_CONTEXT_H