standard_utility.h

Go to the documentation of this file.

// Author(s): Jeroen van der Wulp
// 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_STANDARD_UTILITY_H
#define MCRL2_DATA_STANDARD_UTILITY_H
 
#include <queue>
 
#include "mcrl2/data/real.h"
#include "mcrl2/utilities/detail/join.h"
 
namespace mcrl2
{
 
namespace data
{
 
namespace sort_bool
{
inline data_expression bool_(bool b)
{
  return (b) ? sort_bool::true_() : sort_bool::false_();
}
 
inline bool is_boolean_constant(data_expression const& b)
{
  return sort_bool::is_true_function_symbol(b) ||
         sort_bool::is_false_function_symbol(b);
}
} // namespace sort_bool
 
inline
bool
is_system_defined(const sort_expression& s)
{
  return sort_bool::is_bool(s) || sort_real::is_real(s)
         || sort_int::is_int(s) || sort_nat::is_nat(s) || sort_pos::is_pos(s)
         || is_container_sort(s) || is_structured_sort(s);
}
 
namespace lazy
{
inline data_expression not_(data_expression const& p)
{
  if (p == sort_bool::true_())
  {
    return sort_bool::false_();
  }
  else if (p == sort_bool::false_())
  {
    return sort_bool::true_();
  }
 
  return sort_bool::not_(p);
}
 
inline data_expression or_(data_expression const& p, data_expression const& q)
{
  if ((p == sort_bool::true_()) || (q == sort_bool::true_()))
  {
    return sort_bool::true_();
  }
  else if ((p == q) || (p == sort_bool::false_()))
  {
    return q;
  }
  else if (q == sort_bool::false_())
  {
    return p;
  }
 
  return sort_bool::or_(p, q);
}
 
inline data_expression and_(data_expression const& p, data_expression const& q)
{
  if ((p == sort_bool::false_()) || (q == sort_bool::false_()))
  {
    return sort_bool::false_();
  }
  else if ((p == q) || (p == sort_bool::true_()))
  {
    return q;
  }
  else if (q == sort_bool::true_())
  {
    return p;
  }
 
  return sort_bool::and_(p, q);
}
 
inline data_expression implies(data_expression const& p, data_expression const& q)
{
  if ((p == sort_bool::false_()) || (q == sort_bool::true_()) || (p == q))
  {
    return sort_bool::true_();
  }
  else if (p == sort_bool::true_())
  {
    return q;
  }
  else if (q == sort_bool::false_())
  {
    return sort_bool::not_(p);
  }
 
  return sort_bool::implies(p, q);
}
 
inline data_expression equal_to(data_expression const& p, data_expression const& q)
{
  if (p == q)
  {
    return sort_bool::true_();
  }
 
  return data::equal_to(p, q);
}
 
inline data_expression not_equal_to(data_expression const& p, data_expression const& q)
{
  if (p == q)
  {
    return sort_bool::false_();
  }
 
  return data::not_equal_to(p, q);
}
 
inline data_expression if_(const data_expression& cond, const data_expression& then, const data_expression& else_)
{
  if (cond == sort_bool::true_() || then == else_)
  {
    return then;
  }
  else if (cond == sort_bool::false_())
  {
    return else_;
  }
 
  return data::if_(cond, then, else_);
}
 
template < typename ForwardTraversalIterator >
inline data_expression join_or(ForwardTraversalIterator first, ForwardTraversalIterator last)
{
  return utilities::detail::join(first, last, lazy::or_, static_cast< data_expression const& >(sort_bool::false_()));
}
 
template < typename ForwardTraversalIterator >
inline data_expression join_and(ForwardTraversalIterator first, ForwardTraversalIterator last)
{
  return utilities::detail::join(first, last, lazy::and_, static_cast< data_expression const& >(sort_bool::true_()));
}
} // namespace lazy
 
 
inline std::list<data_expression> split_disjunction(const data_expression& condition)
{
  std::list<data_expression> clauses;
 
  std::queue<data_expression> todo;
  todo.push(condition);
 
  while (!todo.empty())
  {
    data::data_expression expr = todo.front();
    todo.pop();
 
    if (sort_bool::is_or_application(expr))
    {
      const auto& appl = static_cast<application>(expr);
      todo.push(appl[0]);
      todo.push(appl[1]);
    }
    else
    {
      clauses.push_front(expr);
    }
  }
 
  return clauses;
}
 
inline std::list<data_expression> split_conjunction(const data_expression& condition)
{
  std::list<data_expression> clauses;
 
  std::queue<data_expression> todo;
  todo.push(condition);
 
  while (!todo.empty())
  {
    data_expression expr = todo.front();
    todo.pop();
 
    if (sort_bool::is_and_application(expr))
    {
      const auto& appl = static_cast<application>(expr);
      todo.push(appl[0]);
      todo.push(appl[1]);
    }
    else
    {
      clauses.push_front(expr);
    }
  }
 
  return clauses;
}
 
} // namespace data
 
} // namespace mcrl2
 
#endif