Line data    Source code

       1             : // Author(s): Luc Engelen
       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/data/detail/prover/bdd_simplifier.h
      10             : /// \brief Abstract interface for BDD simplifiers
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PROVER_BDD_SIMPLIFIER_H
      13             : #define MCRL2_DATA_DETAIL_PROVER_BDD_SIMPLIFIER_H
      14             : 
      15             : #include "mcrl2/data/data_expression.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : /** \brief A base class for simplifying binary decision diagrams.
      25             :  *
      26             :  * \detail
      27             :  * These classes take a BDD as input and try to simplify this BDD.
      28             :  * The method BDD_Simplifier::simplify receives a BDD as parameter
      29             :  * a_bdd and tries to find an equivalent BDD that is smaller. It
      30             :  * returns the reduced BDD if such a BDD is found. If a reduced BDD is
      31             :  * not found, the original BDD is returned.
      32             : */
      33             : 
      34             : class BDD_Simplifier
      35             : {
      36             :   protected:
      37             :     /// \brief An integer representing the moment in time when the maximal amount of seconds has been spent on simplifying
      38             :     /// \brief the BDD.
      39             :     time_t f_deadline;
      40             :   public:
      41             :     /// \brief Destructor without any additional functionality.
      42          36 :     virtual ~BDD_Simplifier()
      43          18 :     {
      44          36 :     }
      45             : 
      46             :     /// \brief Sets the attribute BDD_Simplifier::f_deadline.
      47          81 :     void set_time_limit(time_t a_time_limit)
      48             :     {
      49          81 :       if (a_time_limit == 0)
      50             :       {
      51           0 :         f_deadline = 0;
      52             :       }
      53             :       else
      54             :       {
      55          81 :         f_deadline = time(nullptr) + a_time_limit;
      56             :       }
      57          81 :     }
      58             : 
      59             :     /// \brief Returns a simplified BDD, equivalent to the bdd a_bdd.
      60             :     /// precondition: The argument passed as parameter a_bdd is a data expression in internal mCRL2 format with the
      61             :     /// following restrictions: It either represents the constant true or the constant false, or it is an if-then-else
      62             :     /// expression with an expression of sort Bool  as guard, and a then-branch and an else-branch that again follow these
      63             :     /// restrictions
      64          81 :     virtual data_expression simplify(const data_expression& a_bdd)
      65             :     {
      66          81 :       return a_bdd;
      67             :     }
      68             : };
      69             : } // namespace detail
      70             : } // namespace data
      71             : } // namespace mcrl2
      72             : 
      73             : #endif