Line data    Source code

       1             : // Author(s): Jeroen van der Wulp
       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/standard_utility.h
      10             : /// \brief Provides utilities for working with data expressions of standard sorts
      11             : 
      12             : #ifndef MCRL2_DATA_STANDARD_UTILITY_H
      13             : #define MCRL2_DATA_STANDARD_UTILITY_H
      14             : 
      15             : #include "mcrl2/utilities/detail/join.h"
      16             : #include "mcrl2/data/real.h"
      17             : 
      18             : #include <queue>
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace data
      24             : {
      25             : 
      26             : namespace sort_bool
      27             : {
      28             : /// \brief Constructs expression of type Bool from an integral type
      29             : /// \param b A Boolean
      30       11917 : inline data_expression bool_(bool b)
      31             : {
      32       11917 :   return (b) ? sort_bool::true_() : sort_bool::false_();
      33             : }
      34             : 
      35             : /// \brief Determines whether b is a Boolean constant
      36             : /// \param b A data expression
      37        5056 : inline bool is_boolean_constant(data_expression const& b)
      38             : {
      39        9102 :   return sort_bool::is_true_function_symbol(b) ||
      40        9102 :          sort_bool::is_false_function_symbol(b);
      41             : }
      42             : } // namespace sort_bool
      43             : 
      44             : /// \brief Returns true iff the expression represents a standard sort.
      45             : /// \param[in] s a sort expression.
      46             : inline
      47             : bool
      48      182388 : is_system_defined(const sort_expression& s)
      49             : {
      50      357023 :   return sort_bool::is_bool(s) || sort_real::is_real(s)
      51      174632 :          || sort_int::is_int(s) || sort_nat::is_nat(s) || sort_pos::is_pos(s)
      52      357023 :          || is_container_sort(s) || is_structured_sort(s);
      53             : }
      54             : 
      55             : /** \brief A collection of utilities for lazy expression construction
      56             :  *
      57             :  * The basic idea is to keep expressions that result from application of
      58             :  * any of the container operations by applying the usual rules of logic.
      59             :  *
      60             :  * For example and(true, x) as in `and' applied to `true' and `x' yields x.
      61             :  **/
      62             : namespace lazy
      63             : {
      64             : /// \brief Returns an expression equivalent to not p
      65             : /// \param p A data expression
      66             : /// \return The value <tt>!p</tt>
      67       14507 : inline data_expression not_(data_expression const& p)
      68             : {
      69       14507 :   if (p == sort_bool::true_())
      70             :   {
      71        1075 :     return sort_bool::false_();
      72             :   }
      73       13432 :   else if (p == sort_bool::false_())
      74             :   {
      75       11388 :     return sort_bool::true_();
      76             :   }
      77             : 
      78        2044 :   return sort_bool::not_(p);
      79             : }
      80             : 
      81             : /// \brief Returns an expression equivalent to p and q
      82             : /// \param p A data expression
      83             : /// \param q A data expression
      84             : /// \return The value <tt>p && q</tt>
      85        7418 : inline data_expression or_(data_expression const& p, data_expression const& q)
      86             : {
      87        7418 :   if ((p == sort_bool::true_()) || (q == sort_bool::true_()))
      88             :   {
      89        1245 :     return sort_bool::true_();
      90             :   }
      91        6173 :   else if ((p == q) || (p == sort_bool::false_()))
      92             :   {
      93        4501 :     return q;
      94             :   }
      95        1672 :   else if (q == sort_bool::false_())
      96             :   {
      97          36 :     return p;
      98             :   }
      99             : 
     100        1636 :   return sort_bool::or_(p, q);
     101             : }
     102             : 
     103             : /// \brief Returns an expression equivalent to p or q
     104             : /// \param p A data expression
     105             : /// \param q A data expression
     106             : /// \return The value p || q
     107       90698 : inline data_expression and_(data_expression const& p, data_expression const& q)
     108             : {
     109       90698 :   if ((p == sort_bool::false_()) || (q == sort_bool::false_()))
     110             :   {
     111        5069 :     return sort_bool::false_();
     112             :   }
     113       85629 :   else if ((p == q) || (p == sort_bool::true_()))
     114             :   {
     115       44394 :     return q;
     116             :   }
     117       41235 :   else if (q == sort_bool::true_())
     118             :   {
     119       22014 :     return p;
     120             :   }
     121             : 
     122       19221 :   return sort_bool::and_(p, q);
     123             : }
     124             : 
     125             : /// \brief Returns an expression equivalent to p implies q
     126             : /// \param p A data expression
     127             : /// \param q A data expression
     128             : /// \return The value p || q
     129           0 : inline data_expression implies(data_expression const& p, data_expression const& q)
     130             : {
     131           0 :   if ((p == sort_bool::false_()) || (q == sort_bool::true_()) || (p == q))
     132             :   {
     133           0 :     return sort_bool::true_();
     134             :   }
     135           0 :   else if (p == sort_bool::true_())
     136             :   {
     137           0 :     return q;
     138             :   }
     139           0 :   else if (q == sort_bool::false_())
     140             :   {
     141           0 :     return sort_bool::not_(p);
     142             :   }
     143             : 
     144           0 :   return sort_bool::implies(p, q);
     145             : }
     146             : 
     147             : /// \brief Returns an expression equivalent to p == q
     148             : /// \param p A data expression
     149             : /// \param q A data expression
     150             : /// \return The value p == q
     151         323 : inline data_expression equal_to(data_expression const& p, data_expression const& q)
     152             : {
     153         323 :   if (p == q)
     154             :   {
     155          23 :     return sort_bool::true_();
     156             :   }
     157             : 
     158         300 :   return data::equal_to(p, q);
     159             : }
     160             : 
     161             : /// \brief Returns an expression equivalent to p == q
     162             : /// \param p A data expression
     163             : /// \param q A data expression
     164             : /// \return The value ! p == q
     165             : inline data_expression not_equal_to(data_expression const& p, data_expression const& q)
     166             : {
     167             :   if (p == q)
     168             :   {
     169             :     return sort_bool::false_();
     170             :   }
     171             : 
     172             :   return data::not_equal_to(p, q);
     173             : }
     174             : 
     175             : /// @brief Returns an expression equivalent to if(cond,then,else_)
     176             : /// @return The value if(cond,then,else_)
     177           0 : inline data_expression if_(const data_expression& cond, const data_expression& then, const data_expression& else_)
     178             : {
     179           0 :   if (cond == sort_bool::true_() || then == else_)
     180             :   {
     181           0 :     return then;
     182             :   }
     183           0 :   else if (cond == sort_bool::false_())
     184             :   {
     185           0 :     return else_;
     186             :   }
     187             : 
     188           0 :   return data::if_(cond, then, else_);
     189             : }
     190             : 
     191             : /// \brief Returns or applied to the sequence of data expressions [first, last)
     192             : /// \param first Start of a sequence of data expressions
     193             : /// \param last End of a sequence of data expressions
     194             : /// \return Or applied to the sequence of data expressions [first, last)
     195             : template < typename ForwardTraversalIterator >
     196         731 : inline data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
     197             : {
     198         731 :   return utilities::detail::join(first, last, lazy::or_, static_cast< data_expression const& >(sort_bool::false_()));
     199             : }
     200             : 
     201             : /// \brief Returns and applied to the sequence of data expressions [first, last)
     202             : /// \param first Start of a sequence of data expressions
     203             : /// \param last End of a sequence of data expressions
     204             : /// \return And applied to the sequence of data expressions [first, last)
     205             : template < typename ForwardTraversalIterator >
     206         715 : inline data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
     207             : {
     208         715 :   return utilities::detail::join(first, last, lazy::and_, static_cast< data_expression const& >(sort_bool::true_()));
     209             : }
     210             : } // namespace lazy
     211             : 
     212             : 
     213             : /// \brief Split a disjunctive expression into a set of clauses.
     214             : inline std::list<data_expression> split_disjunction(const data_expression& condition)
     215             : {
     216             :   std::list<data_expression> clauses;
     217             : 
     218             :   std::queue<data_expression> todo;
     219             :   todo.push(condition);
     220             : 
     221             :   while (!todo.empty())
     222             :   {
     223             :     const data::data_expression& expr = todo.front();
     224             :     todo.pop();
     225             : 
     226             :     if (sort_bool::is_or_application(expr))
     227             :     {
     228             :       const auto& appl = static_cast<application>(expr);
     229             :       todo.push(appl[0]);
     230             :       todo.push(appl[1]);
     231             :     }
     232             :     else
     233             :     {
     234             :       clauses.push_front(expr);
     235             :     }
     236             :   }
     237             : 
     238             :   return clauses;
     239             : }
     240             : 
     241             : /// \brief Split a disjunctive expression into a set of clauses.
     242             : inline std::list<data_expression> split_conjunction(const data_expression& condition)
     243             : {
     244             :   std::list<data_expression> clauses;
     245             : 
     246             :   std::queue<data_expression> todo;
     247             :   todo.push(condition);
     248             : 
     249             :   while (!todo.empty())
     250             :   {
     251             :     const data_expression& expr = todo.front();
     252             :     todo.pop();
     253             : 
     254             :     if (sort_bool::is_and_application(expr))
     255             :     {
     256             :       const auto& appl = static_cast<application>(expr);
     257             :       todo.push(appl[0]);
     258             :       todo.push(appl[1]);
     259             :     }
     260             :     else
     261             :     {
     262             :       clauses.push_front(expr);
     263             :     }
     264             :   }
     265             : 
     266             :   return clauses;
     267             : }
     268             : 
     269             : } // namespace data
     270             : 
     271             : } // namespace mcrl2
     272             : 
     273             : #endif
     274             :