Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/consistency.h
      10             : /// \brief This file contains some functions that are present in all libraries
      11             : /// except the data library. In the data library they have different names, or
      12             : /// are located in different namespaces. Note that this file can not be used
      13             : /// everywhere, in particular not when people expose the sort_bool namespace.
      14             : 
      15             : #ifndef MCRL2_DATA_CONSISTENCY_H
      16             : #define MCRL2_DATA_CONSISTENCY_H
      17             : 
      18             : #include "mcrl2/data/bool.h"
      19             : #include "mcrl2/data/exists.h"
      20             : #include "mcrl2/data/forall.h"
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace data {
      25             : 
      26             : /// \brief Test if x is true
      27             : /// \param x a data expression
      28             : inline
      29          20 : bool is_true(const data_expression& x)
      30             : {
      31          20 :   return sort_bool::is_true_function_symbol(x);
      32             : }
      33             : 
      34             : /// \brief Test if x is false
      35             : /// \param x a data expression
      36             : inline
      37       16381 : bool is_false(const data_expression& x)
      38             : {
      39       16381 :   return sort_bool::is_false_function_symbol(x);
      40             : }
      41             : 
      42             : /// \brief Test if x is a negation
      43             : /// \param x a data expression
      44             : inline
      45          15 : bool is_not(const data_expression& x)
      46             : {
      47          15 :   return sort_bool::is_not_application(x);
      48             : }
      49             : 
      50             : /// \brief Test if x is a disjunction
      51             : /// \param x a data expression
      52             : inline
      53           5 : bool is_or(const data_expression& x)
      54             : {
      55           5 :   return sort_bool::is_or_application(x);
      56             : }
      57             : 
      58             : /// \brief Test if x is a conjunction
      59             : /// \param x a data expression
      60             : inline
      61           7 : bool is_and(const data_expression& x)
      62             : {
      63           7 :   return sort_bool::is_and_application(x);
      64             : }
      65             : 
      66             : /// \brief Test if x is an implication
      67             : /// \param x a data expression
      68             : inline
      69           5 : bool is_imp(const data_expression& x)
      70             : {
      71           5 :   return sort_bool::is_implies_application(x);
      72             : }
      73             : 
      74             : /// \brief Test if x is an equality
      75             : /// \param x a data expression
      76             : inline
      77           0 : bool is_equal_to(const data_expression& x)
      78             : {
      79           0 :   return is_equal_to_application(x);
      80             : }
      81             : 
      82             : /// \brief Test if x is an inequality
      83             : /// \param x a data expression
      84             : inline
      85           0 : bool is_not_equal_to(const data_expression& x)
      86             : {
      87           0 :   return is_not_equal_to_application(x);
      88             : }
      89             : 
      90             : /// \return The expression true
      91             : inline
      92         101 : const data_expression& true_()
      93             : {
      94         101 :   return sort_bool::true_();
      95             : }
      96             : 
      97             : /// \return The expression false
      98             : inline
      99           6 : const data_expression& false_()
     100             : {
     101           6 :   return sort_bool::false_();
     102             : }
     103             : 
     104             : /// \return The negation of x
     105             : inline
     106         736 : data_expression not_(const data_expression& x)
     107             : {
     108         736 :   return sort_bool::not_(x);
     109             : }
     110             : 
     111             : /// \return The disjunction of x and y
     112             : inline
     113           0 : data_expression or_(const data_expression& x, const data_expression& y)
     114             : {
     115           0 :   return sort_bool::or_(x, y);
     116             : }
     117             : 
     118             : /// \return The conjunction of x and y
     119             : inline
     120           5 : data_expression and_(const data_expression& x, const data_expression& y)
     121             : {
     122           5 :   return sort_bool::and_(x, y);
     123             : }
     124             : 
     125             : /// \return The implication of x and y
     126             : inline
     127           0 : data_expression imp(const data_expression& x, const data_expression& y)
     128             : {
     129           0 :   return sort_bool::implies(x, y);
     130             : }
     131             : 
     132             : /// \return Test if x is the boolean sort
     133             : inline
     134           0 : bool is_bool(const sort_expression& x)
     135             : {
     136           0 :   return sort_bool::is_bool(x);
     137             : }
     138             : 
     139             : /// \return The boolean sort
     140             : inline
     141        3114 : sort_expression bool_()
     142             : {
     143        3114 :   return sort_bool::bool_();
     144             : }
     145             : 
     146             : /// \brief Make a universal quantification. It checks for an empty variable list,
     147             : /// which is not allowed.
     148             : /// \param v A sequence of data variables
     149             : /// \param x A data expression
     150             : /// \return The value <tt>forall v.x</tt>
     151             : inline
     152             : data_expression make_forall_(const data::variable_list& v, const data_expression& x)
     153             : {
     154             :   if (v.empty())
     155             :   {
     156             :     return x;
     157             :   }
     158             :   return forall(v, x);
     159             : }
     160             : 
     161             : /// \brief Make an existential quantification. It checks for an empty variable list,
     162             : /// which is not allowed.
     163             : /// \param v A sequence of data variables
     164             : /// \param x A data expression
     165             : /// \return The value <tt>exists v.x</tt>
     166             : inline
     167             : data_expression make_exists_(const data::variable_list& v, const data_expression& x)
     168             : {
     169             :   if (v.empty())
     170             :   {
     171             :     return x;
     172             :   }
     173             :   return exists(v, x);
     174             : }
     175             : 
     176             : } // namespace data
     177             : 
     178             : } // namespace mcrl2
     179             : 
     180             : #endif // MCRL2_DATA_CONSISTENCY_H