Line data    Source code

       1             : // Author(s): Maurice Laveaux
       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             : 
      10             : #ifdef MCRL2_ENABLE_SYLVAN
      11             : 
      12             : #include "mcrl2/symbolic/ldd_stream.h"
      13             : 
      14             : #include "mcrl2/utilities/exception.h"
      15             : 
      16             : #include <stack>
      17             : #include <optional>
      18             : 
      19             : using namespace sylvan::ldds;
      20             : using namespace mcrl2::symbolic;
      21             : 
      22             : /// Iterates over all nodes in the given LDD. The LDDs in nodes will not be traversed.
      23             : struct node_iterator
      24             : {
      25             : public:
      26           2 :   node_iterator(const ldd& U, mcrl2::utilities::indexed_set<sylvan::ldds::ldd>& nodes)
      27           2 :    : m_nodes(nodes)
      28             :   {    
      29           2 :     m_stack.emplace(std::make_pair(U, false));
      30           2 :     this->operator++();
      31           2 :   }
      32             : 
      33           4 :   void operator++()
      34             :   {
      35           6 :     while (!m_stack.empty())
      36             :     {    
      37           4 :       auto& current = m_stack.top();
      38             : 
      39           4 :       if (current.second)
      40             :       {
      41           2 :         m_current = current.first;
      42           2 :         m_stack.pop();
      43           2 :         return; // Top of the stack is the current item.        
      44             :       }
      45             :       else
      46             :       {
      47             :         // Add children and continue.        
      48           2 :         if (m_nodes.find(current.first.down()) == m_nodes.end())
      49             :         {
      50           0 :           m_stack.push(std::make_pair(current.first.down(), false));
      51             :         }
      52           2 :         if (m_nodes.find(current.first.right()) == m_nodes.end())
      53             :         {
      54           0 :           m_stack.push(std::make_pair(current.first.right(), false));
      55             :         }
      56           2 :         current.second = true; // Next time, we can actually process current.
      57             :       }
      58             :     }
      59             : 
      60           2 :     m_current.reset();
      61             :   }
      62             : 
      63           0 :   ldd* operator->()
      64             :   {
      65           0 :     assert(m_current);
      66           0 :     return &m_current.value();
      67             :   }
      68             : 
      69             :   const ldd* operator->() const
      70             :   {
      71             :     assert(m_current);
      72             :     return &m_current.value();
      73             :   }
      74             : 
      75           4 :   ldd& operator*()
      76             :   {
      77           4 :     assert(m_current);
      78           4 :     return m_current.value();
      79             :   }
      80             : 
      81             :   const ldd& operator*() const
      82             :   {
      83             :     assert(m_current);
      84             :     return m_current.value();
      85             :   }
      86             : 
      87           4 :   operator bool() const
      88             :   {
      89           4 :     return m_current.has_value();
      90             :   }
      91             : 
      92             : private:
      93             :   // Traverse the ldd bottom up, where the boolean indicates all children have been returned.
      94             :   std::stack<std::pair<ldd, bool>> m_stack;
      95             :   
      96             :   mcrl2::utilities::indexed_set<sylvan::ldds::ldd>& m_nodes;
      97             : 
      98             :   std::optional<ldd> m_current;
      99             : };
     100             : 
     101             : /// \brief The magic value for a binary LDD format stream.
     102             : static constexpr std::uint16_t BLF_MAGIC = 0x8baf;
     103             : static constexpr std::uint16_t BLF_VERSION = 0x8306;
     104             : 
     105           1 : binary_ldd_ostream::binary_ldd_ostream(std::shared_ptr<mcrl2::utilities::obitstream> stream)
     106           1 :   : m_stream(stream)
     107             : {
     108             :   // Write the header of the binary LDD format.
     109           1 :   m_stream->write_bits(BLF_MAGIC, 16);
     110           1 :   m_stream->write_bits(BLF_VERSION, 16);
     111             : 
     112             :   // Add the true and false constants.
     113           1 :   m_nodes.insert(false_());
     114           1 :   m_nodes.insert(true_());
     115           1 : }
     116             : 
     117           1 : binary_ldd_ostream::binary_ldd_ostream(std::ostream& is)
     118           1 :   : binary_ldd_ostream(std::make_shared<mcrl2::utilities::obitstream>(is))
     119           1 : {}
     120             : 
     121           1 : binary_ldd_ostream::~binary_ldd_ostream()
     122           1 : {}
     123             : 
     124           2 : void binary_ldd_ostream::put(const ldd& U)
     125             : {
     126             :   // Write all children of U.
     127           2 :   node_iterator it(U, m_nodes);
     128             : 
     129           4 :   while (it)
     130             :   {
     131           2 :     const auto& [index, inserted] = m_nodes.insert(*it);
     132           2 :     if (inserted)
     133             :     {
     134             :       // New LDD that must be written to stream.
     135           0 :       m_stream->write_bits(0, 1);
     136           0 :       m_stream->write_integer(it->value());
     137           0 :       m_stream->write_bits(m_nodes.index(it->down()), ldd_index_width());
     138           0 :       m_stream->write_bits(m_nodes.index(it->right()), ldd_index_width());
     139             :     }
     140             : 
     141           2 :     if (*it == U)
     142             :     {       
     143           2 :       m_stream->write_bits(1, 1); // Is output.
     144           2 :       m_stream->write_bits(index, ldd_index_width());
     145             :     }
     146             : 
     147           2 :     ++it;
     148             :   }
     149           2 : }
     150             : 
     151           2 : unsigned int binary_ldd_ostream::ldd_index_width()
     152             : {
     153           2 :   return std::log2(m_nodes.size()) + 1;
     154             : }
     155             : 
     156           1 : binary_ldd_istream::binary_ldd_istream(std::shared_ptr<mcrl2::utilities::ibitstream> stream)
     157           1 :   : m_stream(stream)
     158             : {  
     159             :   // The term with function symbol index 0 indicates the end of the stream.
     160           1 :   m_nodes.emplace_back(false_());
     161           1 :   m_nodes.emplace_back(true_());
     162             : 
     163             :   // Read the binary aterm format header.
     164           1 :   if (m_stream->read_bits(16) != BLF_MAGIC)
     165             :   {
     166           0 :     throw mcrl2::runtime_error("Error while reading: missing the BLF_MAGIC control sequence.");
     167             :   }
     168             : 
     169           1 :   std::size_t version = m_stream->read_bits(16);
     170           1 :   if (version != BLF_VERSION)
     171             :   {
     172           0 :     throw mcrl2::runtime_error("The BLF version (" + std::to_string(version) + ") of the input file is incompatible with the version (" + std::to_string(BLF_VERSION) +
     173           0 :                                ") of this tool. The input file must be regenerated. ");
     174             :   }
     175           1 : }
     176             : 
     177           1 : binary_ldd_istream::binary_ldd_istream(std::istream& is)
     178           1 :   : binary_ldd_istream(std::make_shared<mcrl2::utilities::ibitstream>(is))
     179           1 : {}
     180             : 
     181           2 : ldd binary_ldd_istream::get()
     182             : {
     183             :   while (true)
     184             :   {
     185           2 :     bool is_output = m_stream->read_bits(1);
     186             : 
     187           2 :     if (is_output)
     188             :     {
     189             :       // The output is simply an index of the LDD.
     190           2 :       std::size_t index = m_stream->read_bits(ldd_index_width());
     191           2 :       return m_nodes[index];
     192             :     }
     193             :     else
     194             :     {
     195           0 :       std::size_t value = m_stream->read_integer();
     196           0 :       std::size_t down_index = m_stream->read_bits(ldd_index_width(true));
     197           0 :       std::size_t right_index = m_stream->read_bits(ldd_index_width(true));
     198             : 
     199           0 :       ldd down = m_nodes[down_index];
     200           0 :       ldd right = m_nodes[right_index];
     201             : 
     202           0 :       ldd result = ldd(sylvan::lddmc_makenode(value, down.get(), right.get()));
     203           0 :       m_nodes.emplace_back(result);
     204           0 :     }
     205           0 :   }
     206             : }
     207             : 
     208           2 : unsigned int binary_ldd_istream::ldd_index_width(bool input)
     209             : {
     210           2 :   return std::log2(m_nodes.size() + input) + 1; // Assume that size is one larger to contain the input ldd.
     211             : }
     212             : 
     213             : #endif // MCRL2_ENABLE_SYLVAN