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 ticket_1300.cpp
10 : /// \brief Test for find functions.
11 :
12 : #define BOOST_TEST_MODULE ticket_1300
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/detail/io.h"
16 : #include "mcrl2/data/parse.h"
17 : #include "mcrl2/data/print.h"
18 :
19 :
20 : using namespace mcrl2;
21 :
22 1 : void test1()
23 : {
24 1 : std::string expression_text = "DataAppl(OpId(Four_in_a_row_diagonally_column,SortArrow([SortId(Piece),SortId(Pos),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortId(Bool)),88),OpId(Red,SortId(Piece),87),DataAppl(OpId(@cDub,SortArrow([SortId(Bool),SortId(Pos)],SortId(Pos)),89),OpId(false,SortId(Bool),43),OpId(@c1,SortId(Pos),90)),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(Red,SortId(Piece),87),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),DataAppl(OpId(|>,SortArrow([SortCons(SortList,SortId(Piece)),SortCons(SortList,SortCons(SortList,SortId(Piece)))],SortCons(SortList,SortCons(SortList,SortId(Piece)))),79),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),DataAppl(OpId(|>,SortArrow([SortId(Piece),SortCons(SortList,SortId(Piece))],SortCons(SortList,SortId(Piece))),84),OpId(None,SortId(Piece),86),OpId(\"[]\",SortCons(SortList,SortId(Piece)),83)))))))),OpId(\"[]\",SortCons(SortList,SortCons(SortList,SortId(Piece))),78))))))))";
25 :
26 : std::string dataspec_text =
27 : "sort Piece = struct Red | Yellow | None;\n"
28 : " Row = List(Piece);\n"
29 : " Board = List(Row);\n"
30 : " S1;\n"
31 : " S2;\n"
32 : "\n"
33 : "cons c_,c_1: S1;\n"
34 : " c_2,c_3: S2;\n"
35 : "\n"
36 : "map N,M,R: Pos;\n"
37 : " At: Nat # Nat # Board -> Piece;\n"
38 : " At: Nat # Row -> Piece;\n"
39 : " PutColumn: Piece # Pos # Board -> Board;\n"
40 : " PutColumn,Put: Piece # Pos # Pos # Board -> Board;\n"
41 : " Put: Piece # Pos # Row -> Row;\n"
42 : " Four_in_a_row,Four_in_a_row_horizontally: Piece # Board -> Bool;\n"
43 : " Four_in_a_row_horizontally: Piece # Pos # Board -> Bool;\n"
44 : " Count_rows_horizontally: Piece # Pos # Pos # Board # Nat -> Bool;\n"
45 : " Four_in_a_row_vertically: Piece # Board -> Bool;\n"
46 : " Four_in_a_row_vertically: Piece # Pos # Board -> Bool;\n"
47 : " Count_rows_vertically: Piece # Pos # Pos # Board # Nat -> Bool;\n"
48 : " Four_in_a_row_diagonally: Piece # Board -> Bool;\n"
49 : " Four_in_a_row_diagonally_column,Four_in_a_row_diagonally_row: Piece # Pos # Board -> Bool;\n"
50 : " Count_rows_diagonally,Count_rows_diagonally': Piece # Pos # Pos # Board # Nat -> Bool;\n"
51 : " initial_board: Board;\n"
52 : " pi_S1_: List(List(Piece)) -> List(Piece);\n"
53 : " pi_S1_1: List(List(Piece)) -> List(List(Piece));\n"
54 : " C_S1_: S1 # List(Piece) # List(Piece) -> List(Piece);\n"
55 : " C_S1_: S1 # List(List(Piece)) # List(List(Piece)) -> List(List(Piece));\n"
56 : " C_S1_: S1 # S1 # S1 -> S1;\n"
57 : " Det_S1_: List(List(Piece)) -> S1;\n"
58 : " pi_S2_: List(Piece) -> Piece;\n"
59 : " pi_S2_1: List(Piece) -> List(Piece);\n"
60 : " C_S2_: S2 # Piece # Piece -> Piece;\n"
61 : " C_S2_: S2 # List(Piece) # List(Piece) -> List(Piece);\n"
62 : " C_S2_: S2 # S2 # S2 -> S2;\n"
63 : " Det_S2_: List(Piece) -> S2;\n"
64 : "\n"
65 : "var b,b': Board;\n"
66 : " r: Row;\n"
67 : " p,p',p'': Piece;\n"
68 : " x,y: Nat;\n"
69 : " c: Bool;\n"
70 : " z: Pos;\n"
71 : "eqn N = 7;\n"
72 : " M = 1;\n"
73 : " R = 4;\n"
74 : " if(c, true, false) = c;\n"
75 : " if(c, false, true) = !c;\n"
76 : " if(c, p, p') == p'' = if(c, p == p'', p' == p'');\n"
77 : " y == 1 -> At(x, y, r |> b) = At(x, r);\n"
78 : " 1 < y && y <= M -> At(x, y, r |> b) = At(x, Int2Nat(y - 1), b);\n"
79 : " y == 0 || y > M || x == 0 || x > N -> At(x, y, b) = None;\n"
80 : " At(x, y, if(c, b, b')) = if(c, At(x, y, b), At(x, y, b'));\n"
81 : " x == 1 -> At(x, p |> r) = p;\n"
82 : " 1 < x && x <= N -> At(x, p |> r) = At(Int2Nat(x - 1), r);\n"
83 : " x == 0 || x > N -> At(x, p |> r) = None;\n"
84 : " At(x, Put(p, z, r)) = if(x == z, p, At(x, r));\n"
85 : "\n"
86 : "var b,b': Board;\n"
87 : " r: Row;\n"
88 : " p,p': Piece;\n"
89 : " x,y: Pos;\n"
90 : " dx,dy: Int;\n"
91 : " c,othercolorseen: Bool;\n"
92 : " counter: Nat;\n"
93 : " y3,y2,d1: List(List(Piece));\n"
94 : " y1: S1;\n"
95 : " d: List(Piece);\n"
96 : "eqn y == 1 -> Put(p, x, y, r |> b) = Put(p, x, r) |> b;\n"
97 : " y > 1 && y <= M -> Put(p, x, y, r |> b) = r |> Put(p, x, Int2Pos(y - 1), b);\n"
98 : " Put(p, x, y, if(c, b, b')) = if(c, Put(p, x, y, b), Put(p, x, y, b'));\n"
99 : " x == 1 -> Put(p, x, p' |> r) = p |> r;\n"
100 : " x > 1 && x <= N -> Put(p, x, p' |> r) = p' |> Put(p, Int2Pos(x - 1), r);\n"
101 : " PutColumn(p, x, b) = PutColumn(p, x, 1, b);\n"
102 : " y < M -> PutColumn(p, x, y, b) = if(At(x, y, b) == None, Put(p, x, y, b), PutColumn(p, x, y + 1, b));\n"
103 : " y == M -> PutColumn(p, x, y, b) = Put(p, x, M, b);\n"
104 : " Four_in_a_row(p, b) = Four_in_a_row_horizontally(p, b) || Four_in_a_row_vertically(p, b) || Four_in_a_row_diagonally(p, b);\n"
105 : " Four_in_a_row_horizontally(p, b) = Four_in_a_row_horizontally(p, 1, b);\n"
106 : " y < M -> Four_in_a_row_horizontally(p, y, b) = Count_rows_horizontally(p, 1, y, b, 0) || Four_in_a_row_horizontally(p, y + 1, b);\n"
107 : " y == M -> Four_in_a_row_horizontally(p, y, b) = Count_rows_horizontally(p, 1, M, b, 0);\n"
108 : " x < N -> Count_rows_horizontally(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1 || Count_rows_horizontally(p, x + 1, y, b, counter + 1), Count_rows_horizontally(p, x + 1, y, b, 0));\n"
109 : " x == N -> Count_rows_horizontally(p, x, y, b, counter) = if(At(N, y, b) == p, counter >= R - 1, false);\n"
110 : " Four_in_a_row_vertically(p, b) = Four_in_a_row_vertically(p, 1, b);\n"
111 : " x < N -> Four_in_a_row_vertically(p, x, b) = Count_rows_vertically(p, x, 1, b, 0) || Four_in_a_row_vertically(p, x + 1, b);\n"
112 : " x == N -> Four_in_a_row_vertically(p, x, b) = Count_rows_vertically(p, N, 1, b, 0);\n"
113 : " y < M -> Count_rows_vertically(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1 || Count_rows_vertically(p, x, y + 1, b, counter + 1), Count_rows_vertically(p, x, y + 1, b, 0));\n"
114 : " y == M -> Count_rows_vertically(p, x, y, b, counter) = if(At(x, M, b) == p, counter >= R - 1, false);\n"
115 : " Four_in_a_row_diagonally(p, b) = Four_in_a_row_diagonally_column(p, 2, b) || Four_in_a_row_diagonally_row(p, 1, b);\n"
116 : " x < N -> Four_in_a_row_diagonally_row(p, x, b) = Count_rows_diagonally(p, x, 1, b, 0) || Count_rows_diagonally'(p, x, 1, b, 0) || Four_in_a_row_diagonally_row(p, x + 1, b);\n"
117 : " x == N -> Four_in_a_row_diagonally_row(p, x, b) = Count_rows_diagonally'(p, N, 1, b, 0);\n"
118 : " y < M -> Four_in_a_row_diagonally_column(p, y, b) = Count_rows_diagonally(p, 1, y, b, 0) || Count_rows_diagonally'(p, N, y, b, 0) || Four_in_a_row_diagonally_column(p, y + 1, b);\n"
119 : " y == M -> Four_in_a_row_diagonally_column(p, y, b) = false;\n"
120 : " x < N && y < M -> Count_rows_diagonally(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1 || Count_rows_diagonally(p, x + 1, y + 1, b, counter + 1), Count_rows_diagonally(p, x + 1, y + 1, b, 0));\n"
121 : " x == N || y == M -> Count_rows_diagonally(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1, false);\n"
122 : " x > 1 && y < M -> Count_rows_diagonally'(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1 || Count_rows_diagonally'(p, max(1, x - 1), y + 1, b, counter + 1), Count_rows_diagonally'(p, max(1, x - 1), y + 1, b, 0));\n"
123 : " x == 1 || y == M -> Count_rows_diagonally'(p, x, y, b, counter) = if(At(x, y, b) == p, counter >= R - 1, false);\n"
124 : " initial_board = [[None, None, None, None, None, None, None], [None, None, None, None, None, None, None], [None, None, None, None, None, None, None], [None, None, None, None, None, None, None], [None, None, None, None, None, None, None], [None, None, None, None, None, None, None]];\n"
125 : " C_S1_(c_, y2, y3) = y2;\n"
126 : " C_S1_(c_1, y2, y3) = y3;\n"
127 : " C_S1_(y1, y3, y3) = y3;\n"
128 : " Det_S1_([]) = c_;\n"
129 : " Det_S1_(d |> d1) = c_1;\n"
130 : " pi_S1_(d |> d1) = d;\n"
131 : "\n"
132 : "var b,b2,b4: Bool;\n"
133 : " d2,d3,d4,d5,d1,d6,d7,y15,y14,d8,d9,y19,y18,d10,d11,d12,d13: List(List(Piece));\n"
134 : " y7,y6,y11,y10,d,y3,y2: List(Piece);\n"
135 : " y5,b1,y9,y13,b3,y17,y23,y22,y21,b5: S1;\n"
136 : " y1: S2;\n"
137 : "eqn pi_S1_(if(b, d2, d3)) = if(b, pi_S1_(d2), pi_S1_(d3));\n"
138 : " C_S1_(c_, y6, y7) = y6;\n"
139 : " C_S1_(c_1, y6, y7) = y7;\n"
140 : " C_S1_(y5, y7, y7) = y7;\n"
141 : " pi_S1_(C_S1_(b1, d4, d5)) = C_S1_(b1, pi_S1_(d4), pi_S1_(d5));\n"
142 : " C_S1_(c_, y10, y11) = y10;\n"
143 : " C_S1_(c_1, y10, y11) = y11;\n"
144 : " C_S1_(y9, y11, y11) = y11;\n"
145 : " pi_S1_1(d |> d1) = d1;\n"
146 : " pi_S1_1(if(b2, d6, d7)) = if(b2, pi_S1_1(d6), pi_S1_1(d7));\n"
147 : " C_S1_(c_, y14, y15) = y14;\n"
148 : " C_S1_(c_1, y14, y15) = y15;\n"
149 : " C_S1_(y13, y15, y15) = y15;\n"
150 : " pi_S1_1(C_S1_(b3, d8, d9)) = C_S1_(b3, pi_S1_1(d8), pi_S1_1(d9));\n"
151 : " C_S1_(c_, y18, y19) = y18;\n"
152 : " C_S1_(c_1, y18, y19) = y19;\n"
153 : " C_S1_(y17, y19, y19) = y19;\n"
154 : " Det_S1_(if(b4, d10, d11)) = if(b4, Det_S1_(d10), Det_S1_(d11));\n"
155 : " C_S1_(c_, y22, y23) = y22;\n"
156 : " C_S1_(c_1, y22, y23) = y23;\n"
157 : " C_S1_(y21, y23, y23) = y23;\n"
158 : " Det_S1_(C_S1_(b5, d12, d13)) = C_S1_(b5, Det_S1_(d12), Det_S1_(d13));\n"
159 : " C_S2_(c_2, y2, y3) = y2;\n"
160 : " C_S2_(c_3, y2, y3) = y3;\n"
161 : " C_S2_(y1, y3, y3) = y3;\n"
162 : " Det_S2_([]) = c_2;\n"
163 : "\n"
164 : "var d,y7,y6,y11,y10: Piece;\n"
165 : " d1,d2,d3,d4,d5,d6,d7,y15,y14,d8,d9,y19,y18,d10,d11,d12,d13: List(Piece);\n"
166 : " b,b2,b4: Bool;\n"
167 : " y5,b1,y9,y13,b3,y17,y23,y22,y21,b5: S2;\n"
168 : "eqn Det_S2_(d |> d1) = c_3;\n"
169 : " pi_S2_(d |> d1) = d;\n"
170 : " pi_S2_(if(b, d2, d3)) = if(b, pi_S2_(d2), pi_S2_(d3));\n"
171 : " C_S2_(c_2, y6, y7) = y6;\n"
172 : " C_S2_(c_3, y6, y7) = y7;\n"
173 : " C_S2_(y5, y7, y7) = y7;\n"
174 : " pi_S2_(C_S2_(b1, d4, d5)) = C_S2_(b1, pi_S2_(d4), pi_S2_(d5));\n"
175 : " C_S2_(c_2, y10, y11) = y10;\n"
176 : " C_S2_(c_3, y10, y11) = y11;\n"
177 : " C_S2_(y9, y11, y11) = y11;\n"
178 : " pi_S2_1(d |> d1) = d1;\n"
179 : " pi_S2_1(if(b2, d6, d7)) = if(b2, pi_S2_1(d6), pi_S2_1(d7));\n"
180 : " C_S2_(c_2, y14, y15) = y14;\n"
181 : " C_S2_(c_3, y14, y15) = y15;\n"
182 : " C_S2_(y13, y15, y15) = y15;\n"
183 : " pi_S2_1(C_S2_(b3, d8, d9)) = C_S2_(b3, pi_S2_1(d8), pi_S2_1(d9));\n"
184 : " C_S2_(c_2, y18, y19) = y18;\n"
185 : " C_S2_(c_3, y18, y19) = y19;\n"
186 : " C_S2_(y17, y19, y19) = y19;\n"
187 : " Det_S2_(if(b4, d10, d11)) = if(b4, Det_S2_(d10), Det_S2_(d11));\n"
188 : " C_S2_(c_2, y22, y23) = y22;\n"
189 : " C_S2_(c_3, y22, y23) = y23;\n"
190 : " C_S2_(y21, y23, y23) = y23;\n"
191 1 : " Det_S2_(C_S2_(b5, d12, d13)) = C_S2_(b5, Det_S2_(d12), Det_S2_(d13));\n"
192 : ;
193 :
194 1 : data::data_specification dataspec = data::parse_data_specification(dataspec_text);
195 :
196 1 : atermpp::aterm t = atermpp::read_term_from_string(expression_text);
197 1 : t = data::detail::remove_index(t);
198 1 : t = data::detail::add_index(t);
199 1 : const data::data_expression& d = atermpp::down_cast<data::data_expression>(t);
200 1 : std::string s = data::pp(d);
201 1 : std::cout << s << std::endl;
202 1 : }
203 :
204 2 : BOOST_AUTO_TEST_CASE(test_main)
205 : {
206 1 : test1();
207 1 : }
|