Line data    Source code

       1             : // Author(s): Jeroen Keiren
       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 data_expression_test.cpp
      10             : /// \brief Basic regression test for data expressions.
      11             : 
      12             : #define BOOST_TEST_MODULE data_expression_test
      13             : #include <boost/test/included/unit_test.hpp>
      14             : 
      15             : #include "mcrl2/atermpp/aterm_io.h"
      16             : #include "mcrl2/data/bag.h"
      17             : #include "mcrl2/data/exists.h"
      18             : #include "mcrl2/data/lambda.h"
      19             : #include "mcrl2/data/list.h"
      20             : #include "mcrl2/data/where_clause.h"
      21             : 
      22             : using namespace mcrl2;
      23             : using namespace mcrl2::data;
      24             : 
      25           2 : BOOST_AUTO_TEST_CASE(variable_test)
      26             : {
      27           2 :   basic_sort s("S");
      28           2 :   variable x("x", s);
      29           1 :   BOOST_CHECK(pp(x.name()) == "x");
      30           1 :   BOOST_CHECK(x.sort() == s);
      31             : 
      32           2 :   core::identifier_string y_name("y");
      33           1 :   variable y(y_name, s);
      34           1 :   BOOST_CHECK(pp(y.name()) == "y");
      35           1 :   BOOST_CHECK(y.sort() == s);
      36             : 
      37           2 :   variable y_("y", s);
      38           1 :   BOOST_CHECK(pp(y_.name()) == "y");
      39           1 :   BOOST_CHECK(y.sort() == s);
      40             : 
      41           1 :   BOOST_CHECK(x != y);
      42           1 :   BOOST_CHECK(x != y_);
      43           1 :   BOOST_CHECK(y == y_);
      44             : 
      45           1 :   const data_expression& y_e(y);
      46           1 :   variable y_e_(y_e);
      47           1 :   BOOST_CHECK(y_e_ == y);
      48           1 :   BOOST_CHECK(y_e_.name() == y.name());
      49           1 :   BOOST_CHECK(y_e_.sort() == y.sort());
      50           1 : }
      51             : 
      52           2 : BOOST_AUTO_TEST_CASE(function_symbol_test)
      53             : {
      54           2 :   basic_sort s0("S0");
      55           2 :   basic_sort s1("S1");
      56           2 :   basic_sort s("S");
      57             : 
      58           1 :   sort_expression_vector s01;
      59           1 :   s01.push_back(s0);
      60           1 :   s01.push_back(s1);
      61           1 :   function_sort fs(s01, s);
      62             : 
      63             : 
      64           2 :   data::function_symbol f("f", fs);
      65           1 :   BOOST_CHECK(pp(f.name()) == "f");
      66           1 :   BOOST_CHECK(f.sort() == fs);
      67             : 
      68           2 :   data::function_symbol g("g", s0);
      69           1 :   BOOST_CHECK(pp(g.name()) == "g");
      70           1 :   BOOST_CHECK(g.sort() == s0);
      71             : 
      72           2 :   core::identifier_string g_name("g");
      73           1 :   data::function_symbol g_(g_name, s0);
      74           1 :   BOOST_CHECK(pp(g_.name()) == "g");
      75           1 :   BOOST_CHECK(g_.sort() == s0);
      76             : 
      77           1 :   BOOST_CHECK(f != g);
      78           1 :   BOOST_CHECK(f != g_);
      79           1 :   BOOST_CHECK(g == g_);
      80             : 
      81           1 :   const data_expression& f_e(f);
      82           1 :   data::function_symbol f_e_(f_e);
      83           1 :   BOOST_CHECK(f_e == f);
      84           1 :   BOOST_CHECK(f_e_.name() == f.name());
      85           1 :   BOOST_CHECK(f_e_.sort() == f.sort());
      86           1 : }
      87             : 
      88           2 : BOOST_AUTO_TEST_CASE(application_test)
      89             : {
      90           2 :   basic_sort s0("S0");
      91           2 :   basic_sort s1("S1");
      92           2 :   basic_sort s("S");
      93           1 :   sort_expression_vector s01;
      94           1 :   s01.push_back(sort_expression(s0));
      95           1 :   s01.push_back(sort_expression(s1));
      96           1 :   function_sort s01s(s01, s);
      97             : 
      98           2 :   data::function_symbol f("f", s01s);
      99           2 :   data_expression x(variable("x", s0));
     100           2 :   data_expression y(variable("y", s1));
     101           3 :   data_expression_list xy = { x, y };
     102           1 :   application fxy(f, xy);
     103           1 :   BOOST_CHECK(fxy.sort() == s);
     104           1 :   BOOST_CHECK(fxy.head() == f);
     105           1 :   BOOST_CHECK(data_expression_list(fxy.begin(), fxy.end()) == xy);
     106           1 :   BOOST_CHECK(*(fxy.begin()) == x);
     107           1 :   BOOST_CHECK(*(++fxy.begin()) == y);
     108             : 
     109           1 :   const data_expression& fxy_e(fxy);
     110           1 :   application fxy_e_(fxy_e);
     111           1 :   BOOST_CHECK(fxy == fxy_e_);
     112           1 :   BOOST_CHECK(fxy.sort() == fxy_e_.sort());
     113           1 :   BOOST_CHECK(fxy.head() == fxy_e_.head());
     114           1 :   BOOST_CHECK(fxy == f(x,y));
     115           1 : }
     116             : 
     117           2 : BOOST_AUTO_TEST_CASE(abstraction_test)
     118             : {
     119           2 :   basic_sort s("S");
     120             : 
     121           2 :   variable x("x", s);
     122           2 :   variable_list xl = { x };
     123           2 :   abstraction I(lambda_binder(), xl, x);
     124           1 :   BOOST_CHECK(I.binding_operator() == lambda_binder());
     125           1 :   BOOST_CHECK(I.variables() == xl);
     126           1 :   BOOST_CHECK(I.body() == x);
     127             : 
     128           1 :   const data_expression& I_e(I);
     129           1 :   abstraction I_e_(I_e);
     130           1 :   BOOST_CHECK(I_e_ == I);
     131           1 :   BOOST_CHECK(I_e_.binding_operator() == I.binding_operator());
     132           1 :   BOOST_CHECK(I_e_.variables() == I.variables());
     133           1 :   BOOST_CHECK(I_e_.body() == I.body());
     134           1 : }
     135             : 
     136           2 : BOOST_AUTO_TEST_CASE(lambda_test)
     137             : {
     138           2 :   basic_sort s("S");
     139             : 
     140           2 :   variable x("x", s);
     141           2 :   variable_list xl = { x };
     142           1 :   lambda I(xl, x);
     143           1 :   BOOST_CHECK(I.binding_operator() == lambda_binder());
     144           1 :   BOOST_CHECK(is_lambda(I));
     145           1 :   BOOST_CHECK(I.variables() == xl);
     146           1 :   BOOST_CHECK(I.body() == x);
     147           1 :   const sort_expression& s_(s);
     148           4 :   sort_expression_vector s_l {s_};
     149           1 :   BOOST_CHECK(!s_l.empty());
     150           1 :   function_sort fs(s_l, s);
     151           1 :   BOOST_CHECK(I.sort() == fs);
     152             : 
     153           1 :   const data_expression& I_e(I);
     154           1 :   lambda I_e_(I_e);
     155           1 :   BOOST_CHECK(I_e_ == I);
     156           1 :   BOOST_CHECK(I_e_.binding_operator() == I.binding_operator());
     157           1 :   BOOST_CHECK(I_e_.variables() == I.variables());
     158           1 :   BOOST_CHECK(I_e_.body() == I.body());
     159           2 :   abstraction I_(lambda_binder(), xl, x);
     160           1 :   BOOST_CHECK(I_ == I);
     161           1 :   BOOST_CHECK(I_.binding_operator() == I.binding_operator());
     162           1 :   BOOST_CHECK(I_.variables() == I.variables());
     163           1 :   BOOST_CHECK(I_.body() == I.body()) ;
     164           1 : }
     165             : 
     166           2 : BOOST_AUTO_TEST_CASE(forall_test)
     167             : {
     168           2 :   basic_sort s("S");
     169             : 
     170           2 :   variable x("x", s);
     171           2 :   variable_list xl = { x };
     172           1 :   forall I(xl, x);
     173           1 :   BOOST_CHECK(I.binding_operator() == forall_binder());
     174           1 :   BOOST_CHECK(is_forall(I));
     175           1 :   BOOST_CHECK(I.variables() == xl);
     176           1 :   BOOST_CHECK(I.body() == x);
     177           1 :   const sort_expression& s_(s);
     178           3 :   sort_expression_vector s_l {s_};
     179             : 
     180             :   // TODO Check sort
     181             : 
     182           1 :   const data_expression& I_e(I);
     183           1 :   forall I_e_(I_e);
     184           1 :   BOOST_CHECK(I_e_ == I);
     185           1 :   BOOST_CHECK(I_e_.binding_operator() == I.binding_operator());
     186           1 :   BOOST_CHECK(I_e_.variables() == I.variables());
     187           1 :   BOOST_CHECK(I_e_.body() == I.body());
     188           2 :   abstraction I_(forall_binder(), xl, x);
     189           1 :   BOOST_CHECK(I_ == I);
     190           1 :   BOOST_CHECK(I_.binding_operator() == I.binding_operator());
     191           1 :   BOOST_CHECK(I_.variables() == I.variables());
     192           1 :   BOOST_CHECK(I_.body() == I.body()) ;
     193           1 : }
     194             : 
     195           2 : BOOST_AUTO_TEST_CASE(exists_test)
     196             : {
     197           2 :   basic_sort s("S");
     198             : 
     199           2 :   variable x("x", s);
     200           2 :   variable_list xl = { x };
     201           1 :   exists I(xl, x);
     202           1 :   BOOST_CHECK(I.binding_operator() == exists_binder());
     203           1 :   BOOST_CHECK(is_exists(I));
     204           1 :   BOOST_CHECK(I.variables() == xl);
     205           1 :   BOOST_CHECK(I.body() == x);
     206           1 :   const sort_expression& s_(s);
     207           3 :   sort_expression_vector s_l {s_};
     208             : 
     209             :   // TODO Check sort
     210             : 
     211           1 :   const data_expression& I_e(I);
     212           1 :   exists I_e_(I_e);
     213           1 :   BOOST_CHECK(I_e_ == I);
     214           1 :   BOOST_CHECK(I_e_.binding_operator() == I.binding_operator());
     215           1 :   BOOST_CHECK(I_e_.variables() == I.variables());
     216           1 :   BOOST_CHECK(I_e_.body() == I.body());
     217           2 :   abstraction I_(exists_binder(), xl, x);
     218           1 :   BOOST_CHECK(I_ == I);
     219           1 :   BOOST_CHECK(I_.binding_operator() == I.binding_operator());
     220           1 :   BOOST_CHECK(I_.variables() == I.variables());
     221           1 :   BOOST_CHECK(I_.body() == I.body()) ;
     222           1 : }
     223             : 
     224           2 : BOOST_AUTO_TEST_CASE(set_comprehension_test)
     225             : {
     226           2 :   basic_sort s("S");
     227           2 :   variable x("x", make_function_sort_(s,sort_bool::bool_()));
     228           2 :   data::function_symbol f("f", make_function_sort_(s, sort_bool::bool_()));
     229           2 :   data_expression e(sort_set::set_comprehension(s, x));
     230           1 :   BOOST_CHECK(e.sort() == sort_set::set_(s));
     231           1 : }
     232             : 
     233           2 : BOOST_AUTO_TEST_CASE(bag_comprehension_test)
     234             : {
     235           2 :   basic_sort s("S");
     236           2 :   data::function_symbol f("f", make_function_sort_(s, sort_nat::nat()));
     237           2 :   data_expression e(sort_bag::bag_comprehension(s, f));
     238           1 :   BOOST_CHECK(e.sort() == sort_bag::bag(s));
     239           1 : }
     240             : 
     241           2 : BOOST_AUTO_TEST_CASE(where_declaration_test)
     242             : {
     243           2 :   basic_sort s("S");
     244           2 :   variable x("x", s);
     245           2 :   variable y("y", s);
     246             : 
     247           1 :   assignment xy(x,y);
     248           2 :   assignment_expression_list xyl = { xy };
     249           1 :   where_clause wxy(x, xyl);
     250           1 :   BOOST_CHECK(wxy.body() == x);
     251           1 :   BOOST_CHECK(wxy.declarations() == xyl);
     252             : 
     253           1 :   const data_expression& wxy_e(wxy);
     254           1 :   where_clause wxy_e_(wxy_e);
     255           1 :   BOOST_CHECK(wxy_e_ == wxy);
     256           1 :   BOOST_CHECK(wxy_e_.body() == wxy.body());
     257           1 :   BOOST_CHECK(wxy_e_.declarations() == wxy.declarations());
     258           1 :   BOOST_CHECK(wxy.sort() == x.sort());
     259           1 : }
     260             : 
     261           2 : BOOST_AUTO_TEST_CASE(assignment_test)
     262             : {
     263           2 :   basic_sort s("S");
     264           2 :   variable x("x", s);
     265           2 :   variable y("y", s);
     266             : 
     267           1 :   assignment xy(x, y);
     268           1 :   BOOST_CHECK(xy.lhs() == x);
     269           1 :   BOOST_CHECK(xy.rhs() == y);
     270           1 : }
     271             : 
     272           2 : BOOST_AUTO_TEST_CASE(system_defined_check)
     273             : {
     274           1 :   BOOST_CHECK(sort_list::empty(sort_pos::pos()) != sort_list::empty(sort_nat::nat()));
     275           1 : }