representative_generator.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// 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_REPRESENTATIVE_GENERATOR_H
#define MCRL2_DATA_REPRESENTATIVE_GENERATOR_H
 
#include "mcrl2/data/data_specification.h"
 
namespace mcrl2
{
 
namespace data
{
 
class representative_generator
{
 
  protected:
 
    const data_specification& m_specification;
 
    std::map< sort_expression, data_expression > m_representatives_cache;
 
  protected:
 
    void set_representative(const sort_expression& sort, const data_expression& representative)
    {
      assert(sort==representative.sort());
      m_representatives_cache[sort] = representative;
    }
 
    //                           an infinite circular search through the sorts.
    bool find_representative(
                       const function_symbol& symbol, 
                       std::set < sort_expression >& visited_sorts,
                       data_expression& result) 
    {
      assert(is_function_sort(symbol.sort()));
 
      data_expression_vector arguments;
 
      for (const sort_expression& s: static_cast<const function_sort&>(symbol.sort()).domain())
      {
        data_expression representative;
        if (find_representative(s, visited_sorts, representative))
        {
          arguments.push_back(representative);
        }
        else
        {
          // a representative for this argument could not be found.
          return false;
        }
      }
 
      // a suitable set of arguments is found
      result=application(symbol, arguments);
      return true;
    }
 
    bool search_for_lexicographically_minimal_symbol(function_symbol& f_result, 
                                                   const sort_expression& sort,
                                                   const std::vector<function_symbol>& function_symbols)
    {
      bool function_symbol_found=false;
      for (const function_symbol& f: function_symbols)
      {
        if (f.sort()==sort)
        {
          if (function_symbol_found) 
          {
            if (static_cast<const std::string&>(f.name())<static_cast<const std::string&>(f_result.name()))
            {
              f_result=f;
            }
          }
          else
          {
            f_result=f;
            function_symbol_found=true;
          }
        }
      }
      return function_symbol_found;
    }
 
    //                           an infinite circular search through the sorts.
    bool find_representative(
                    const sort_expression& sort, 
                    std::set < sort_expression >& visited_sorts, 
                    data_expression& result)
    {
      if (visited_sorts.count(sort)>0)
      {
        // This sort is already visited. We are looking to find a representative term of this sort
        // within the scope of finding a term of this sort. If this is to be succesful, a more compact
        // term can be found. Hence, stop searching further.
        return false;
      }
 
      const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
      if (i!=m_representatives_cache.end())
      {
        assert(i->second.sort()==sort);
        result=i->second;
        return true;
      }
      
      if (is_function_sort(sort))
      {
        // s is a function sort. 
        // First search for a lexicographically minimal mapping with sort s (constructors with sort s cannot exist).
        function_symbol minimal_f;
        const function_sort& fs=atermpp::down_cast<function_sort>(sort);
        if (search_for_lexicographically_minimal_symbol(minimal_f, sort, m_specification.mappings(fs.codomain())))
        {
           result=minimal_f;
           set_representative(sort, result);
           return true;
        }
 
        // If no explicit constant is found of this sort, we know that its shape is "s0#..#sn -> s". 
        // We search a term t of sort s and if found, construct a lambda term of the shape 
        // lambda x0:s0,...,xn:sn.t. Note that this can be strengthened slightly by incorporating
        // the variables xi in generating t, e.g. generating for D->D  the reprentant lambd d:D.d. 
        // Incorporating the variables in the generation of terms requires adapting all algorithms,
        // and is not done. Until now the need for such representant generators has not been felt. 
 
        const sort_expression& s2=fs.codomain();
        data_expression t;
        if (find_representative(s2, visited_sorts, t))
        {
          variable_vector bound_variables;
          std::size_t variable_index=0;
          for(const sort_expression& s: fs.domain())
          {
            bound_variables.emplace_back("x" + std::to_string(variable_index), s);
            variable_index++;
          }
          result=abstraction(lambda_binder(),variable_list(bound_variables.begin(),bound_variables.end()),t);
          return true;
        }
      }
      else
      {
        // s is a constant (not a function sort).
        // check if there is a constant constructor for s
 
        function_symbol minimal_c;
        if (search_for_lexicographically_minimal_symbol(minimal_c, sort, m_specification.constructors(sort)))
        {
          result=minimal_c;
          set_representative(sort, result);
          return true;
        }
 
        visited_sorts.insert(sort);
 
        // Check whether there is a representative f(t1,...,tn) for s, where f is a constructor function. 
        // We prefer this over a constant mapping, as a constant mapping generally does not have appropriate
        // rewrite rules.
        
        // recursively traverse constructor functions of the form f:s1#...#sn -> sort.
        // operators with f:s1#...#sn->G where G is a complex sort expression are ignored
 
        for (const function_symbol& f: m_specification.constructors(sort))
        {
          if (find_representative(f, visited_sorts, result))
          {
            set_representative(sort, result);
            visited_sorts.erase(sort);
            return true;
          }
        }
 
        // check if there is a constant mapping for s
        for (const function_symbol& f: m_specification.mappings(sort))
        {
          if (f.sort()==sort)
          {
            result=f;
            set_representative(sort, result);
            visited_sorts.erase(sort);
            return true;
          }
        }
 
        // Try to check whether there is a representative f(t1,...,tn) where f is a mapping. 
        for (const function_symbol& f: m_specification.mappings(sort))
        {
          if (find_representative(f, visited_sorts, result))
          {
            set_representative(sort, result);
            visited_sorts.erase(sort);
            return true;
          }
        }
        
        visited_sorts.erase(sort);
 
      }
 
      // No representative has been found.
      return false;
    }
 
  public:
 
    representative_generator(const data_specification& specification) : m_specification(specification)
    {
    }
 
    data_expression operator()(const sort_expression& sort)
    {
      // First see whether a term of this sort has already been constructed and resides in the representatives_cache. If yes return it. 
      const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
      if (i!=m_representatives_cache.end())
      {
        return i->second;
      }
      
      data_expression result;
      std::set<sort_expression> visited_sorts;
      if (find_representative(sort, visited_sorts, result))
      {
        // A term of the requested sort is found. Return it. 
        return result;
      }
      else 
      {
        throw mcrl2::runtime_error("Cannot find a term of sort " + data::pp(sort));
      }
     
    }
};
 
} // namespace data
} // namespace mcrl2
#endif