LCOV - code coverage report
Current view: top level - data/test - enumerator_test.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 253 266 95.1 %
Date: 2024-03-08 02:52:28 Functions: 36 37 97.3 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jeroen van der Wulp, 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             : #define BOOST_TEST_MODULE enumerator_test
      10             : #include <boost/test/included/unit_test.hpp>
      11             : 
      12             : #include "mcrl2/data/consistency.h"
      13             : #include "mcrl2/data/detail/concepts.h"
      14             : #include "mcrl2/data/enumerator_with_iterator.h"
      15             : #include "mcrl2/data/optimized_boolean_operators.h"
      16             : #include "mcrl2/data/parse.h"
      17             : #include "mcrl2/data/print.h"
      18             : #include "mcrl2/data/replace.h"
      19             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      20             : 
      21             : using namespace mcrl2;
      22             : using namespace mcrl2::data;
      23             : 
      24             : // Example: parse_variable_list("x:Nat; y:Pos");
      25          27 : variable_list parse_variable_list(const std::string& text, const data_specification& dataspec = detail::default_specification())
      26             : {
      27          27 :   variable_vector result;
      28          27 :   parse_variables(text, std::back_inserter(result), dataspec);
      29          54 :   return variable_list(result.begin(), result.end());
      30          27 : }
      31             : 
      32          13 : void enumerate(const data_specification& dataspec,
      33             :                const variable_list& variables,
      34             :                const data_expression& expression,
      35             :                std::size_t expected_no_of_solutions,
      36             :                bool more_solutions_possible)
      37             : {
      38             :   typedef enumerator_list_element_with_substitution<> enumerator_element;
      39             :   typedef enumerator_algorithm_with_iterator<> enumerator_type;
      40             : 
      41          26 :   data::enumerator_identifier_generator id_generator;
      42          13 :   rewriter rewr(dataspec);
      43          13 :   enumerator_type enumerator(rewr, dataspec, rewr, id_generator);
      44          13 :   std::size_t number_of_solutions = 0;
      45          13 :   mutable_indexed_substitution<> sigma;
      46          13 :   data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, expression));
      47          13 :   auto i = enumerator.begin(sigma, enumerator_deque);
      48         124 :   for ( ; number_of_solutions < expected_no_of_solutions && i != enumerator.end(); ++i)
      49             :   {
      50         111 :     mutable_map_substitution<> rho;
      51         111 :     i->add_assignments(variables, rho, rewr);
      52         111 :     std::cout << "solution = " << rho << std::endl;
      53         111 :     number_of_solutions++;
      54         111 :   }
      55          13 :   BOOST_CHECK(number_of_solutions == expected_no_of_solutions && (more_solutions_possible || i == enumerator.end()));
      56          13 : }
      57             : 
      58          13 : void enumerate(const std::string& dataspec_text,
      59             :                const std::string& variable_text,
      60             :                const std::string& expression_text,
      61             :                const std::string& free_variable_text,
      62             :                std::size_t number_of_solutions,
      63             :                bool more_solutions_possible)
      64             : {
      65          13 :   data_specification dataspec = parse_data_specification(dataspec_text);
      66          13 :   variable_list variables = parse_variable_list(variable_text, dataspec);
      67          13 :   variable_list free_variables = parse_variable_list(free_variable_text, dataspec);
      68          13 :   data_expression expression = parse_data_expression(expression_text, free_variables, dataspec);
      69          13 :   enumerate(dataspec, variables, expression, number_of_solutions, more_solutions_possible);
      70          13 : }
      71             : 
      72           2 : BOOST_AUTO_TEST_CASE(empty_test)
      73             : {
      74             :   typedef enumerator_list_element_with_substitution<> enumerator_element;
      75             :   typedef enumerator_algorithm_with_iterator<> enumerator_type;
      76             : 
      77             :   // test manual construction of rewr with rewriter
      78           1 :   data_specification dataspec;
      79           1 :   rewriter rewr(dataspec);
      80           1 :   variable_list variables;
      81             : 
      82           1 :   std::size_t count = 0;
      83           2 :   data::enumerator_identifier_generator id_generator;
      84             : 
      85             :   // explicit with condition rewr and condition
      86           1 :   enumerator_type enumerator(rewr, dataspec, rewr, id_generator);
      87             : 
      88           1 :   mutable_indexed_substitution<> sigma;
      89           1 :   data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, sort_bool::true_()));
      90           2 :   for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
      91             :   {
      92           1 :     count++;
      93             :   }
      94           1 :   BOOST_CHECK(count == 1);
      95             : 
      96             :   // explicit with condition but without condition rewr
      97           1 :   enumerator_deque.clear();
      98           1 :   enumerator_deque.push_back(enumerator_element(variables, sort_bool::true_()));
      99           2 :   for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
     100             :   {
     101           1 :     count++;
     102             :   }
     103           1 :   BOOST_CHECK(count == 2);
     104             : 
     105           1 :   variables = parse_variable_list("y: Nat;");
     106           1 :   enumerator_deque.clear();
     107           1 :   enumerator_deque.push_back(enumerator_element(variables, sort_bool::false_()));
     108           1 :   for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
     109             :   {
     110           0 :     BOOST_CHECK(false);
     111             :   }
     112           1 : }
     113             : 
     114           2 : BOOST_AUTO_TEST_CASE(list_test)
     115             : {
     116             :   std::string dataspec_text =
     117             :     "sort list_of_booleans;                                    \n"
     118             :     "cons empty : list_of_booleans;                            \n"
     119             :     "     lcons : Bool # list_of_booleans -> list_of_booleans; \n"
     120             :     "map  size   : list_of_booleans -> Nat;                    \n"
     121             :     "var  l : list_of_booleans;                                \n"
     122             :     "     b : Bool;                                            \n"
     123             :     "eqn  size(empty) = 0;                                     \n"
     124           1 :     "     size(lcons(b,l)) = 1 + size(l);                      \n"
     125             :     ;
     126           1 :   std::string variable_text = "x: list_of_booleans; y: Nat;";
     127           1 :   std::string expression_text = "y == size(x) && 0 < y && y < 2";
     128           1 :   std::string free_variable_text = "x : list_of_booleans; y : Nat;";
     129           1 :   std::size_t number_of_solutions = 0;
     130           1 :   bool more_solutions_possible = true; // Changed!
     131           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     132           1 : }
     133             : 
     134           2 : BOOST_AUTO_TEST_CASE(structured_sort_test)
     135             : {
     136             :   std::string dataspec_text =
     137             :     "sort D = struct d1(E) | d2(E); \n"
     138           1 :     "     E = struct e1 | e2;       \n"
     139             :     ;
     140           1 :   std::string variable_text = "d: D;";
     141           1 :   std::string expression_text = "forall d: D. d == e";
     142           1 :   std::string free_variable_text = "e: D;";
     143           1 :   std::size_t number_of_solutions = 4;
     144           1 :   bool more_solutions_possible = false;
     145           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     146           1 : }
     147             : 
     148           2 : BOOST_AUTO_TEST_CASE(equality_substitution_test)
     149             : {
     150           1 :   std::string dataspec_text = "sort L = Nat;";
     151           1 :   std::string variable_text = "";
     152           1 :   std::string expression_text = "x == 17 && x != 17";
     153           1 :   std::string free_variable_text = "x : Pos;";
     154           1 :   std::size_t number_of_solutions = 0;
     155           1 :   bool more_solutions_possible = true; // Changed!
     156             : 
     157           1 :   std::clog << "Test1 equality\n";
     158           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     159             : 
     160           1 :   std::clog << "Test2 equality\n";
     161           1 :   expression_text = "x == 17 && x == x";
     162           1 :   number_of_solutions = 1;
     163           1 :   more_solutions_possible = false;
     164           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     165             : 
     166           1 :   std::clog << "Test3 equality\n";
     167           1 :   expression_text = "x == 17 && 2*x == 34";
     168           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     169             : 
     170           1 :   std::clog << "Test4 equality\n";
     171           1 :   variable_text = "";
     172           1 :   number_of_solutions = 1;
     173           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     174             : 
     175           1 :   std::clog << "Test4 equality: return two non exact solutions\n";
     176           1 :   variable_text = "b: Bool;";
     177           1 :   number_of_solutions = 2;
     178           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     179           1 : }
     180             : 
     181           2 : BOOST_AUTO_TEST_CASE(test_ticket_1486)
     182             : {
     183           1 :   std::string dataspec_text = "sort L = Int;";
     184           1 :   std::string variable_text = "y : Nat;";
     185           1 :   std::string expression_text = "y + 20 == 25";
     186           1 :   std::string free_variable_text = "y : Nat;";
     187           1 :   std::size_t number_of_solutions = 1;
     188           1 :   bool more_solutions_possible = false;
     189           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     190           1 : }
     191             : 
     192           2 : BOOST_AUTO_TEST_CASE(tree_test)
     193             : {
     194             :   std::string dataspec_text =
     195             :     "sort tree_with_booleans;                                                   \n"
     196             :     "cons leaf : Bool -> tree_with_booleans;                                    \n"
     197           1 :     "cons node : tree_with_booleans # tree_with_booleans -> tree_with_booleans; \n"
     198             :     ;
     199           1 :   std::string variable_text = "x : tree_with_booleans;";
     200           1 :   std::string expression_text = "true";
     201           1 :   std::string free_variable_text = "";
     202           1 :   std::size_t number_of_solutions = 32;
     203           1 :   bool more_solutions_possible = true;
     204           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     205           1 : }
     206             : 
     207           2 : BOOST_AUTO_TEST_CASE(mutually_recursive_test)
     208             : {
     209             :   std::string dataspec_text =
     210             :     "sort this;                                              \n"
     211             :     "     that;                                              \n"
     212             :     "cons a : this;                                          \n"
     213             :     "     A : that -> this;                                  \n"
     214             :     "     b : that;                                          \n"
     215             :     "     B : this -> that;                                  \n"
     216             :     "map  maximum_a : Nat # this -> Bool;                    \n"
     217             :     "     maximum_a : Nat # that -> Bool;                    \n"
     218             :     "     maximum_b : Nat # this -> Bool;                    \n"
     219             :     "     maximum_b : Nat # that -> Bool;                    \n"
     220             :     "var  x : Nat;                                           \n"
     221             :     "     ax : this;                                         \n"
     222             :     "     bx : that;                                         \n"
     223             :     "eqn  maximum_a(x,A(bx)) = maximum_a(Int2Nat(x - 1),bx); \n"
     224             :     "     maximum_a(0,a) = true;                             \n"
     225             :     "     maximum_b(x,B(ax)) = maximum_b(Int2Nat(x - 1),ax); \n"
     226           1 :     "     maximum_b(0,b) = true;                             \n"
     227             :     ;
     228             : 
     229           1 :   std::string variable_text = "x : this;";
     230           1 :   std::string expression_text = "true";
     231           1 :   std::string free_variable_text = "";
     232           1 :   std::size_t number_of_solutions = 32;
     233           1 :   bool more_solutions_possible = true;
     234           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     235             : 
     236           1 :   variable_text = "x : that;";
     237           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     238           1 : }
     239             : 
     240           2 : BOOST_AUTO_TEST_CASE(set_test)
     241             : {
     242           1 :   std::string dataspec_text = "sort Dummy;\n";
     243           1 :   std::string variable_text = "f: Set(Bool);";
     244           1 :   std::string expression_text = "true in f";
     245           1 :   std::string free_variable_text = "f: Set(Bool);";
     246           1 :   std::size_t number_of_solutions = 4;
     247           1 :   bool more_solutions_possible = false;
     248           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     249           1 : }
     250             : 
     251             : inline
     252          23 : data_expression_vector generate_values(const data_specification& dataspec, const sort_expression& s, std::size_t max_size = 1000)
     253             : {
     254             :   typedef enumerator_list_element_with_substitution<> enumerator_element;
     255             :   typedef enumerator_algorithm_with_iterator<> enumerator_type;
     256             : 
     257          23 :   std::size_t max_internal_variables = 10000;
     258          23 :   data_expression_vector result;
     259          46 :   data::enumerator_identifier_generator id_generator;
     260             : 
     261          23 :   rewriter rewr(dataspec);
     262          23 :   enumerator_type enumerator(rewr, dataspec, rewr, id_generator, max_internal_variables);
     263          46 :   variable v("x", s);
     264          23 :   variable_list variables;
     265          23 :   variables.push_front(v);
     266          23 :   mutable_indexed_substitution<> sigma;
     267          23 :   data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, sort_bool::true_()));
     268         133 :   for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end() ; ++i)
     269             :   {
     270         116 :     i->add_assignments(variables, sigma, rewr);
     271         116 :     result.push_back(sigma(variables.front()));
     272         116 :     if (result.size() >= max_size)
     273             :     {
     274           6 :       break;
     275             :     }
     276             :   }
     277          46 :   return result;
     278          23 : }
     279             : 
     280          23 : bool no_duplicates(const data_expression_vector& v)
     281             : {
     282          23 :   std::set<data_expression> s;
     283          23 :   s.insert(v.begin(), v.end());
     284          46 :   return s.size() == v.size();
     285          23 : }
     286             : 
     287           2 : BOOST_AUTO_TEST_CASE(generate_values_test)
     288             : {
     289             :   std::string DATASPEC =
     290             :     "sort Identifiers = struct t1 | t2 | t3 | t4 | t5 | p1 | p2 | s1 | r1 | r2 | r3 | IL;                                                                                  \n"
     291             :     "     signal_Messages = struct ic_set_proceed_signal | ic_set_stop_signal;                                                                                             \n"
     292             :     "     track_Messages = struct dv_free_track | dv_occupied_track;                                                                                                       \n"
     293             :     "     point_Messages = struct ic_move_right_point | ic_move_left_point | dv_at_right_point | dv_at_left_point;                                                         \n"
     294             :     "     route_Messages = struct ic_cancel_route_route | ic_set_route_route;                                                                                              \n"
     295             :     "     Interlocking_Messages = struct c_set_stop | c_move_left | c_set_route | c_IL_off | c_cancel_route | tc_set_proceed | c_IL_on | c_move_right;                     \n"
     296             :     "     environment_Messages = struct i_signal_status_proceed_signal_environment | i_signal_status_stop_signal_environment | i_track_status_occupied_track_environment | \n"
     297             :     "       i_track_status_free_track_environment | i_point_at_right_point_environment | i_point_locked_point_environment | i_point_ok_point_environment |                 \n"
     298             :     "       i_point_broken_point_environment | i_point_at_left_point_environment | i_route_cancelled_route_environment | i_route_established_route_environment;            \n"
     299             :     "     rail_yard_Messages = struct sv_set_proceed_signal_railyard | sv_set_stop_signal_railyard | sv_move_right_point_railyard | sv_move_left_point_railyard;           \n"
     300             :     "     Enum3 = struct e2_3 | e1_3 | e0_3;                                                                                                                               \n"
     301             :     "     track__ready_States = struct track__ready_free_substate | track__ready_occupied_substate | track__ready_startup_substate | track__ready_nop;                     \n"
     302             :     "     Enum15 = struct e14_15 | e13_15 | e12_15 | e11_15 | e10_15 | e9_15 | e8_15 | e7_15 | e6_15 | e5_15 | e4_15 | e3_15 | e2_15 | e1_15 | e0_15;                      \n"
     303             :     "     point_States = struct point__broken_substate | point__startup_substate | point__working_substate;                                                                \n"
     304             :     "     point__working_States = struct point__working_right_substate | point__working_left_substate | point__working_moving_substate | point__working_nop;               \n"
     305             :     "     point__working_moving_States = struct point__working_moving_left_substate | point__working_moving_right_substate | point__working_moving_nop;                    \n"
     306             :     "     Enum7 = struct e6_7 | e5_7 | e4_7 | e3_7 | e2_7 | e1_7 | e0_7;                                                                                                   \n"
     307             :     "     signal_States = struct signal__stop_substate | signal__proceed_substate;                                                                                         \n"
     308             :     "     Enum10 = struct e9_10 | e8_10 | e7_10 | e6_10 | e5_10 | e4_10 | e3_10 | e2_10 | e1_10 | e0_10;                                                                   \n"
     309             :     "     route_States = struct route__idle_substate | route__established_substate | route__setting_up_substate;                                                           \n"
     310             :     "     route__established_States = struct route__established_in_use_substate | route__established_active_substate | route__established_nop;                             \n"
     311             :     "     Enum11 = struct e10_11 | e9_11 | e8_11 | e7_11 | e6_11 | e5_11 | e4_11 | e3_11 | e2_11 | e1_11 | e0_11;                                                          \n"
     312             :     "     Enum13 = struct e12_13 | e11_13 | e10_13 | e9_13 | e8_13 | e7_13 | e6_13 | e5_13 | e4_13 | e3_13 | e2_13 | e1_13 | e0_13;                                        \n"
     313             :     "     HAL_device_States = struct HAL_device__normal_substate;                                                                                                          \n"
     314           1 :     "     track_States = struct track__ready_substate;                                                                                                                     \n"
     315             :     ;
     316           1 :   data_specification dataspec = parse_data_specification(DATASPEC);
     317             : 
     318           1 :   for (const sort_expression& sort: dataspec.user_defined_sorts())
     319             :   {
     320           0 :     sort_expression s = normalize_sorts(sort, dataspec);
     321           0 :     std::clog << "--- sort " << data::pp(s) << std::endl;
     322           0 :     data_expression_vector v = generate_values(dataspec, s, 10);
     323           0 :     std::clog << " possible values: " << core::detail::print_set(v) << std::endl;
     324           0 :     BOOST_CHECK(v.size() <= 10);
     325           0 :     BOOST_CHECK(no_duplicates(v));
     326           0 :   }
     327             : 
     328          24 :   for (const alias& a: dataspec.user_defined_aliases())
     329             :   {
     330          23 :     sort_expression s = normalize_sorts(a.reference(),dataspec);
     331          23 :     std::clog << "--- sort " << data::pp(s) << std::endl;
     332          23 :     data_expression_vector v = generate_values(dataspec, s, 10);
     333          23 :     std::clog << " possible values: " << core::detail::print_set(v) << std::endl;
     334          23 :     BOOST_CHECK(v.size() <= 10);
     335          23 :     BOOST_CHECK(no_duplicates(v));
     336          23 :   }
     337           1 : }
     338             : 
     339           2 : BOOST_AUTO_TEST_CASE(constructors_that_are_not_a_normal_form_test)
     340             : {
     341             :   std::string dataspec_text =
     342             :     "sort FloorID     = struct F1 | F2;\n"
     343             :     " \n"
     344             :     "map  fSucc      : FloorID           -> FloorID;\n"
     345             :     "     equal      : FloorID # FloorID      -> Bool;\n"
     346             :     "\n"
     347             :     "var  f,g       : FloorID;\n"
     348             :     "eqn  F2               = fSucc(F1); \n"
     349             :     "     equal(fSucc(f),fSucc(g))  = equal(f,g);\n"
     350             :     "     equal(fSucc(f),F1)      = false;\n"
     351             :     "     equal(F1,fSucc(g))      = false;\n"
     352             :     "     equal(F1,F1)        = true;\n"
     353           1 :     "     f==g            = equal(f,g);\n"
     354             :     ;
     355           1 :   std::string variable_text = "f: FloorID;";
     356           1 :   std::string expression_text = "equal(f, F2)";
     357           1 :   const std::string& free_variable_text = variable_text;
     358           1 :   std::size_t number_of_solutions = 1;
     359           1 :   bool more_solutions_possible = false;
     360           1 :   enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
     361           1 : }
     362             : 
     363           2 : BOOST_AUTO_TEST_CASE(cannot_enumerate_real_default)
     364             : {
     365             :   typedef data::enumerator_list_element<data_expression> enumerator_element;
     366             : 
     367           1 :   data_expression result = data::sort_bool::true_();
     368           3 :   data::variable_list v  = { data::variable("r", data::sort_real::real_()) };
     369           2 :   data_expression phi = parse_data_expression("r == r", v);
     370           1 :   data::data_specification dataspec;
     371           1 :   dataspec.add_context_sort(data::sort_real::real_());
     372           1 :   data::rewriter R(dataspec);
     373           2 :   data::enumerator_identifier_generator id_generator("x");
     374           1 :   data::enumerator_algorithm<> E(R, dataspec, R, id_generator, (std::numeric_limits<std::size_t>::max)());
     375           1 :   data::rewriter::substitution_type sigma;
     376             : 
     377             :   try
     378             :   {
     379           3 :     E.enumerate(enumerator_element(v, phi),
     380             :                 sigma,
     381           0 :                 [&](const enumerator_element& p)
     382             :                 {
     383           0 :                   data::optimized_and(result, result, p.expression());
     384           0 :                   return result == data::sort_bool::false_();
     385             :                 },
     386             :                 is_true,
     387             :                 is_false
     388             :     );
     389             :   }
     390           1 :   catch (mcrl2::runtime_error& e)
     391             :   {
     392           1 :     std::cout << e.what() << std::endl;
     393           1 :     return;
     394           1 :   }
     395           0 :   BOOST_CHECK(false);
     396           8 : }
     397             : 
     398           2 : BOOST_AUTO_TEST_CASE(cannot_enumerate_real_with_substitution)
     399             : {
     400             :   typedef data::enumerator_list_element_with_substitution<data_expression> enumerator_element;
     401             : 
     402           1 :   data::data_specification dataspec;
     403           1 :   dataspec.add_context_sort(data::sort_real::real_());
     404           1 :   data::rewriter R(dataspec);
     405           1 :   data::variable_list v;
     406           1 :   v.push_front(data::variable("r", data::sort_real::real_()));
     407           2 :   data_expression phi = parse_data_expression("r == r", v);
     408           1 :   data::mutable_indexed_substitution<> sigma;
     409           1 :   std::size_t max_count = 1000;
     410           1 :   bool throw_exceptions = true;
     411           2 :   data::enumerator_identifier_generator id_generator;
     412           1 :   data::enumerator_algorithm_with_iterator<rewriter, enumerator_element> E(R, dataspec, R, id_generator, max_count, throw_exceptions);
     413           1 :   data::enumerator_queue<enumerator_element> P(enumerator_element(v, phi));
     414             :   try {
     415           1 :     for (auto i = E.begin(sigma, P); i != E.end() ; ++i)
     416             :     {
     417             :       // skip
     418             :     }
     419             :   }
     420           1 :   catch (mcrl2::runtime_error& e)
     421             :   {
     422           1 :     std::cout << e.what() << std::endl;
     423           1 :     return;
     424           1 :   }
     425           0 :   BOOST_CHECK(false);
     426           8 : }
     427             : 
     428           2 : BOOST_AUTO_TEST_CASE(enumerate_callback)
     429             : {
     430             :   typedef data::enumerator_list_element<data_expression> enumerator_element;
     431           2 :   enumerator_identifier_generator id_generator;
     432           1 :   data_specification dataspec;
     433           1 :   dataspec.add_context_sort(data::sort_int::int_());
     434           1 :   std::size_t max_count = 10;
     435           1 :   data::rewriter r(dataspec);
     436           1 :   data::enumerator_algorithm<rewriter> E(r, dataspec, r, id_generator, max_count);
     437             : 
     438           2 :   auto enumerate = [&](const data_expression& x)
     439             :   {
     440           2 :     data::mutable_indexed_substitution<> sigma;
     441           2 :     data_expression result;
     442           2 :     id_generator.clear();
     443           2 :     if (is_forall(x))
     444             :     {
     445           1 :       const auto& x_ = atermpp::down_cast<forall>(x);
     446           1 :       result = true_();
     447           1 :       E.enumerate(enumerator_element(x_.variables(), r(x_.body())),
     448             :                   sigma,
     449           1 :                   [&](const enumerator_element& p)
     450             :                   {
     451           1 :                     data::optimized_and(result, result, p.expression());
     452           1 :                     return is_false(result);
     453             :                   },
     454             :                   is_true,
     455             :                   is_false
     456             :       );
     457             :     }
     458           1 :     else if (is_exists(x))
     459             :     {
     460           1 :       const exists& x_ = atermpp::down_cast<exists>(x);
     461           1 :       result = false_();
     462           1 :       E.enumerate(enumerator_element(x_.variables(), r(x_.body())),
     463             :                   sigma,
     464           1 :                   [&](const enumerator_element& p)
     465             :                   {
     466           1 :                     data::optimized_or(result, result, p.expression());
     467           1 :                     return is_true(result);
     468             :                   },
     469             :                   is_false,
     470             :                   is_true
     471             :       );
     472             :     }
     473           4 :     return result;
     474           3 :   };
     475             : 
     476           1 :   BOOST_CHECK_EQUAL(enumerate(parse_data_expression("forall n: Nat. n < 2")), false_());
     477           1 :   BOOST_CHECK_EQUAL(enumerate(parse_data_expression("exists n: Nat. n < 2")), true_());
     478           1 : }
     479             : 
     480           2 : BOOST_AUTO_TEST_CASE(enumerate_expressions_test)
     481             : {
     482             :   const std::string dataspec_text =
     483             :           "sort D = struct d1(E) | d2(E);\n"
     484           1 :           "     E = struct e1 | e2;      \n"
     485             :           ;
     486           1 :   std::string variable_text = "d:D";
     487           1 :   data_specification dataspec = parse_data_specification(dataspec_text);
     488           1 :   data::variable v = parse_variable(variable_text, dataspec);
     489           1 :   rewriter r(dataspec);
     490             : 
     491           1 :   data::data_expression_vector result_as_vector = enumerate_expressions(v.sort(), dataspec, r);
     492             : 
     493           1 :   std::set<data::data_expression> result(result_as_vector.begin(), result_as_vector.end());
     494             :   std::set<data::data_expression> expected_result = {
     495             :       parse_data_expression("d1(e2)", dataspec),
     496             :       parse_data_expression("d1(e1)", dataspec),
     497             :       parse_data_expression("d2(e2)", dataspec),
     498             :       parse_data_expression("d2(e1)", dataspec)
     499           7 :   };
     500             : 
     501           1 :   BOOST_CHECK_EQUAL_COLLECTIONS(result.begin(), result.end(), expected_result.begin(), expected_result.end());
     502           1 : }

Generated by: LCOV version 1.14