LCOV - code coverage report
Current view: top level - smt/include/mcrl2/smt - utilities.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 79 0.0 %
Date: 2020-09-22 00:46:14 Functions: 0 19 0.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Thomas Neele, Ruud Koolen
       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             : #ifndef MCRL2_SMT_UTILITIES_H
      10             : #define MCRL2_SMT_UTILITIES_H
      11             : 
      12             : #include <queue>
      13             : 
      14             : #include "mcrl2/smt/native_translation.h"
      15             : #include "mcrl2/smt/translation_error.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace smt
      20             : {
      21             : 
      22             : inline
      23           0 : std::string translate_identifier(const std::string& id)
      24             : {
      25           0 :   std::string result = id;
      26           0 :   for(std::size_t i = 0; i < result.size(); i++)
      27             :   {
      28           0 :     if(result[i] == '\'')
      29             :     {
      30           0 :       result[i] = '!';
      31             :     }
      32             :   }
      33           0 :   return result;
      34             : }
      35             : 
      36             : inline
      37           0 : std::string translate_identifier(const core::identifier_string& id)
      38             : {
      39           0 :   return translate_identifier(core::pp(id));
      40             : }
      41             : 
      42             : inline
      43           0 : std::string translate_symbol(const data::function_symbol& f, const native_translations& nt)
      44             : {
      45           0 :   auto find_result = nt.symbols.find(f);
      46           0 :   return find_result != nt.symbols.end() ? find_result->second : translate_identifier(f.name());
      47             : }
      48             : 
      49             : inline
      50           0 : std::string make_projection_name(const data::function_symbol& cons, std::size_t i, const native_translations& nt)
      51             : {
      52             :   // Projections for natively defined sort List
      53           0 :   if(data::pp(cons) == "|>")
      54             :   {
      55           0 :     return i == 0 ? "head" : "tail";
      56             :   }
      57             :   // Projection for all constructors that are mapped to @id, such as @cNat and @cInt
      58           0 :   if(translate_symbol(cons, nt) == "@id")
      59             :   {
      60           0 :     return "@id";
      61             :   }
      62           0 :   return "@proj-" + translate_symbol(cons, nt) + "-" + std::to_string(i);
      63             : }
      64             : 
      65             : inline
      66           0 : data::function_symbol make_projection_func(const data::function_symbol& cons, const data::sort_expression& arg_sort, std::size_t i, const native_translations& nt)
      67             : {
      68           0 :   data::function_sort sort(data::sort_expression_list({ cons.sort().target_sort() }), arg_sort);
      69           0 :   return data::function_symbol(make_projection_name(cons, i, nt), sort);
      70             : }
      71             : 
      72             : inline
      73           0 : std::string make_recogniser_name(const data::function_symbol& cons, const native_translations& nt)
      74             : {
      75           0 :   auto find_result = nt.special_recogniser.find(cons);
      76           0 :   if(find_result != nt.special_recogniser.end())
      77             :   {
      78           0 :     return find_result->second;
      79             :   }
      80             :   // Z3 automatically generates recognisers "is-constructorname"
      81           0 :   return "is-" + translate_symbol(cons, nt);
      82             : }
      83             : 
      84             : inline
      85           0 : data::function_symbol make_recogniser_func(const data::function_symbol& cons, const native_translations& nt)
      86             : {
      87           0 :   data::function_sort sort(data::sort_expression_list({ cons.sort().target_sort() }), data::sort_bool::bool_());
      88           0 :   return data::function_symbol(make_recogniser_name(cons, nt), sort);
      89             : }
      90             : 
      91             : template<class T>
      92           0 : std::vector<T> topological_sort(std::map<T, std::set<T>> dependencies)
      93             : {
      94           0 :   std::queue<T> vertices_without_dependencies;
      95           0 :   std::map<T, std::set<T> > reverse_dependencies;
      96           0 :   for (const auto& p: dependencies)
      97             :   {
      98           0 :     const T& node = p.first;
      99           0 :     const std::set<T>& successors = p.second;
     100           0 :     for (const T& succ: successors)
     101             :     {
     102           0 :       reverse_dependencies[succ].insert(node);
     103             :     }
     104             : 
     105           0 :     if (successors.empty())
     106             :     {
     107           0 :       vertices_without_dependencies.push(node);
     108             :     }
     109             :   }
     110             : 
     111           0 :   std::vector<T> output;
     112           0 :   output.reserve(dependencies.size());
     113             : 
     114           0 :   while (!vertices_without_dependencies.empty())
     115             :   {
     116           0 :     T vertex = vertices_without_dependencies.front();
     117           0 :     vertices_without_dependencies.pop();
     118           0 :     output.push_back(vertex);
     119             : 
     120           0 :     const std::set<T>& successors = reverse_dependencies[vertex];
     121           0 :     for (const T& succ: successors)
     122             :     {
     123           0 :       dependencies[succ].erase(vertex);
     124           0 :       if (dependencies[succ].empty())
     125             :       {
     126           0 :         vertices_without_dependencies.push(succ);
     127             :       }
     128             :     }
     129             :   }
     130             : 
     131           0 :   if (output.size() != dependencies.size())
     132             :   {
     133           0 :     for (const T& node: output)
     134             :     {
     135           0 :       dependencies.erase(node);
     136             :     }
     137           0 :     assert(!dependencies.empty());
     138             :     //TODO: SMT2.5 format supports mutually recursive data types
     139           0 :     std::ostringstream out;
     140           0 :     for(const auto& p: dependencies)
     141             :     {
     142           0 :       out << p.first << ", ";
     143             :     }
     144           0 :     throw translation_error("Dependency loop trying to resolve dependencies: {" + out.str() + "}");
     145             :   }
     146             :   else
     147             :   {
     148           0 :     return output;
     149             :   }
     150             : }
     151             : 
     152             : template <typename OutStream>
     153             : class stack_outstream
     154             : {
     155             : protected:
     156             :   std::stack<typename OutStream::pos_type> m_stack;
     157             :   std::ostringstream buf;
     158             :   OutStream& m_out;
     159             : 
     160             : public:
     161           0 :   stack_outstream(OutStream& out)
     162           0 :   : m_out(out)
     163           0 :   {}
     164             : 
     165           0 :   ~stack_outstream()
     166             :   {
     167           0 :     m_out << buf.str();
     168           0 :   }
     169             : 
     170           0 :   void push()
     171             :   {
     172           0 :     m_stack.push(buf.tellp());
     173           0 :   }
     174             : 
     175           0 :   void pop()
     176             :   {
     177           0 :     m_stack.pop();
     178           0 :   }
     179             : 
     180           0 :   typename OutStream::pos_type top_size()
     181             :   {
     182           0 :     assert(!m_stack.empty());
     183           0 :     return buf.tellp() - m_stack.top();
     184             :   }
     185             : 
     186           0 :   void copy_top(std::string& dest)
     187             :   {
     188           0 :     dest = buf.str().substr(m_stack.top(), std::string::npos);
     189           0 :   }
     190             : 
     191             :   template <typename T>
     192           0 :   stack_outstream& operator<<(const T& s)
     193             :   {
     194           0 :     buf << s;
     195           0 :     return *this;
     196             :   }
     197             : };
     198             : 
     199             : } // namespace smt
     200             : } // namespace mcrl2
     201             : 
     202             : #endif

Generated by: LCOV version 1.13