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 replace_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE replace_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/atermpp/algorithm.h"
16 : #include "mcrl2/atermpp/aterm_io.h"
17 :
18 : using namespace atermpp;
19 :
20 : // function object to test if it is an aterm_appl with function symbol "f"
21 : struct is_f
22 : {
23 24 : bool operator()(const aterm_appl& t) const
24 : {
25 24 : return t.function().name() == "f";
26 : }
27 : };
28 :
29 : // function object to test if it is an aterm_appl with function symbol "g"
30 : struct is_g
31 : {
32 3 : bool operator()(const aterm_appl& t) const
33 : {
34 3 : return t.function().name() == "g";
35 : }
36 : };
37 :
38 : // function object to test if it is an aterm_appl with function symbol "z"
39 : struct is_z
40 : {
41 4 : bool operator()(const aterm_appl& t) const
42 : {
43 4 : return t.function().name() == "z";
44 : }
45 : };
46 :
47 : // function object to test if it is an aterm_appl with function symbol "a" or "b"
48 : struct is_a_or_b
49 : {
50 : bool operator()(const aterm_appl& t) const
51 : {
52 : return t.function().name() == "a" || t.function().name() == "b";
53 : }
54 : };
55 :
56 : // replaces function names f by g and vice versa
57 : struct fg_replacer
58 : {
59 5 : aterm_appl operator()(const aterm_appl& t) const
60 : {
61 5 : if (t.function().name() == "f")
62 : {
63 2 : return aterm_appl(function_symbol("g", t.function().arity()), t.begin(), t.end());
64 : }
65 4 : else if (t.function().name() == "g")
66 : {
67 4 : return aterm_appl(function_symbol("f", t.function().arity()), t.begin(), t.end());
68 : }
69 : else
70 : {
71 2 : return t;
72 : }
73 : }
74 : };
75 :
76 : // replaces function names f by g and vice versa, but stops the recursion once an f or g term is found
77 : struct fg_partial_replacer
78 : {
79 1 : std::pair< aterm_appl, bool> operator()(aterm_appl t) const
80 : {
81 1 : if (t.function().name() == "f")
82 : {
83 0 : return std::make_pair(aterm_appl(function_symbol("g", t.function().arity()), t.begin(), t.end()), false);
84 : }
85 1 : else if (t.function().name() == "g")
86 : {
87 2 : return std::make_pair(aterm_appl(function_symbol("f", t.function().arity()), t.begin(), t.end()), false);
88 : }
89 : else
90 : {
91 0 : return std::make_pair(t, true);
92 : }
93 : }
94 : };
95 :
96 2 : BOOST_AUTO_TEST_CASE(find_test)
97 : {
98 2 : aterm_appl a(read_appl_from_string("h(g(x),f(y),p(a(x,y),q(f(z))))"));
99 :
100 1 : aterm_appl t = find_if(a, is_f());
101 1 : BOOST_CHECK(t == read_appl_from_string("f(y)"));
102 :
103 2 : aterm_appl a1(read_appl_from_string("h(g(x),g(f(y)))"));
104 1 : t = partial_find_if(a1, is_f(), is_g());
105 1 : BOOST_CHECK(t == aterm_appl());
106 1 : t = partial_find_if(a1, is_f(), is_z());
107 1 : BOOST_CHECK(t == read_appl_from_string("f(y)"));
108 :
109 1 : std::vector< aterm_appl> v;
110 1 : find_all_if(a, is_f(), back_inserter(v));
111 1 : BOOST_CHECK(v.front() == read_appl_from_string("f(y)"));
112 1 : BOOST_CHECK(v.back() == read_appl_from_string("f(z)"));
113 1 : }
114 :
115 2 : BOOST_AUTO_TEST_CASE(replace_test1)
116 : {
117 1 : BOOST_CHECK(replace(read_appl_from_string("x"), read_appl_from_string("x"), read_appl_from_string("f(a)")) == read_term_from_string("f(a)"));
118 1 : BOOST_CHECK(replace(read_appl_from_string("x"), read_appl_from_string("x"), read_appl_from_string("f(x)")) == read_term_from_string("f(x)"));
119 1 : BOOST_CHECK(replace(read_list_from_string("[x]"), read_term_from_string("x"), read_appl_from_string("f(x)")) == read_term_from_string("[f(x)]"));
120 :
121 2 : aterm_appl a(read_appl_from_string("f(f(x))"));
122 2 : aterm_appl b(replace(a, read_appl_from_string("f(x)"), read_appl_from_string("x")));
123 1 : BOOST_CHECK(b == read_appl_from_string("f(x)"));
124 1 : b = bottom_up_replace(a, read_appl_from_string("f(x)"), read_appl_from_string("x"));
125 1 : BOOST_CHECK(b == read_term_from_string("x"));
126 :
127 2 : atermpp::aterm f = read_term_from_string("[]");
128 1 : atermpp::aterm g = replace(f, a, b);
129 1 : BOOST_CHECK(f == read_term_from_string("[]"));
130 1 : BOOST_CHECK(g == read_term_from_string("[]"));
131 :
132 2 : atermpp::aterm x = read_term_from_string("g(f(x),f(y),h(f(x)))");
133 1 : atermpp::aterm y = replace(x, fg_replacer());
134 2 : atermpp::aterm z = partial_replace(x, fg_partial_replacer());
135 :
136 1 : BOOST_CHECK(y == read_term_from_string("f(f(x),f(y),h(f(x)))"));
137 1 : BOOST_CHECK(z == read_term_from_string("f(f(x),f(y),h(f(x)))"));
138 1 : }
139 :
140 : inline
141 2 : const atermpp::function_symbol& f2()
142 : {
143 2 : static atermpp::function_symbol f = atermpp::function_symbol("f", 2);
144 2 : return f;
145 : }
146 :
147 : inline
148 9 : const atermpp::function_symbol& f3()
149 : {
150 9 : static atermpp::function_symbol f = atermpp::function_symbol("f", 3);
151 9 : return f;
152 : }
153 :
154 : struct replace_f
155 : {
156 9 : atermpp::aterm_appl operator()(const atermpp::aterm_appl& x) const
157 : {
158 9 : if (x.function() == f3())
159 : {
160 4 : return atermpp::aterm_appl(f2(), x.begin(), --x.end());
161 : }
162 7 : return x;
163 : }
164 : };
165 :
166 : // DataVarId
167 : inline
168 11 : const atermpp::function_symbol& function_symbol_DataVarId()
169 : {
170 11 : static atermpp::function_symbol function_symbol_DataVarId = atermpp::function_symbol("DataVarId", 3);
171 11 : return function_symbol_DataVarId;
172 : }
173 :
174 : // DataVarIdNoIndex
175 : inline
176 0 : const atermpp::function_symbol& function_symbol_DataVarIdNoIndex()
177 : {
178 0 : static atermpp::function_symbol f = atermpp::function_symbol("DataVarIdNoIndex", 2);
179 0 : return f;
180 : }
181 :
182 : // OpId
183 : inline
184 11 : const atermpp::function_symbol& function_symbol_OpId()
185 : {
186 11 : static atermpp::function_symbol function_symbol_OpId = atermpp::function_symbol("OpId", 3);
187 11 : return function_symbol_OpId;
188 : }
189 :
190 : // OpIdIndex
191 : inline
192 1 : const atermpp::function_symbol& function_symbol_OpIdNoIndex()
193 : {
194 1 : static atermpp::function_symbol f = atermpp::function_symbol("OpIdNoIndex", 2);
195 1 : return f;
196 : }
197 :
198 : // PropVarInst
199 : inline
200 10 : const atermpp::function_symbol& function_symbol_PropVarInst()
201 : {
202 10 : static atermpp::function_symbol function_symbol_PropVarInst = atermpp::function_symbol("PropVarInst", 3);
203 10 : return function_symbol_PropVarInst;
204 : }
205 :
206 : // PropVarInstNoIndex
207 : inline
208 2 : const atermpp::function_symbol& function_symbol_PropVarInstNoIndex()
209 : {
210 2 : static atermpp::function_symbol f = atermpp::function_symbol("PropVarInstNoIndex", 2);
211 2 : return f;
212 : }
213 :
214 : struct index_remover
215 : {
216 11 : atermpp::aterm_appl operator()(const atermpp::aterm_appl& x) const
217 : {
218 11 : if (x.function() == function_symbol_DataVarId())
219 : {
220 0 : return atermpp::aterm_appl(function_symbol_DataVarIdNoIndex(), x.begin(), --x.end());
221 : }
222 11 : else if (x.function() == function_symbol_OpId())
223 : {
224 2 : return atermpp::aterm_appl(function_symbol_OpIdNoIndex(), x.begin(), --x.end());
225 : }
226 10 : else if (x.function() == function_symbol_PropVarInst())
227 : {
228 4 : return atermpp::aterm_appl(function_symbol_PropVarInstNoIndex(), x.begin(), --x.end());
229 : }
230 8 : return x;
231 : }
232 : };
233 :
234 2 : BOOST_AUTO_TEST_CASE(replace_test2)
235 : {
236 2 : atermpp::aterm t = atermpp::read_term_from_string("g(h(x,[f(y,p(q),1)]))");
237 1 : t = atermpp::replace(t, replace_f());
238 1 : BOOST_CHECK(t == atermpp::read_term_from_string("g(h(x,[f(y,p(q))]))"));
239 1 : }
240 :
241 2 : BOOST_AUTO_TEST_CASE(replace_test3)
242 : {
243 2 : atermpp::aterm t = atermpp::read_term_from_string("g(h(z(x,[f(y,p(q),1)],0)))");
244 1 : atermpp::aterm t1 = atermpp::replace(t, replace_f());
245 2 : atermpp::aterm t2 = atermpp::read_term_from_string("g(h(z(x,[f(y,p(q))],0)))");
246 1 : BOOST_CHECK(t1 == t2);
247 1 : }
248 :
249 2 : BOOST_AUTO_TEST_CASE(bottom_up_replace_test)
250 : {
251 2 : atermpp::aterm t = atermpp::read_term_from_string("PBES(PBInit(PropVarInst(X,[OpId(@c0,SortId(Nat),131)],0)))");
252 1 : atermpp::aterm t1 = atermpp::replace(t, index_remover());
253 2 : atermpp::aterm t2 = atermpp::read_term_from_string("PBES(PBInit(PropVarInstNoIndex(X,[OpId(@c0,SortId(Nat),131)])))");
254 1 : atermpp::aterm t3 = atermpp::bottom_up_replace(t, index_remover());
255 2 : atermpp::aterm t4 = atermpp::read_term_from_string("PBES(PBInit(PropVarInstNoIndex(X,[OpIdNoIndex(@c0,SortId(Nat))])))");
256 1 : BOOST_CHECK(t1 == t2);
257 1 : BOOST_CHECK(t3 == t4);
258 1 : }
259 :
260 2 : BOOST_AUTO_TEST_CASE(cached_bottom_up_replace_test)
261 : {
262 1 : std::unordered_map<aterm_appl, aterm> cache;
263 2 : atermpp::aterm t = atermpp::read_term_from_string("h(g(f(x),f(x)),g(f(x),f(x)))");
264 1 : atermpp::aterm t1 = atermpp::bottom_up_replace(t, fg_replacer(), cache);
265 2 : atermpp::aterm t2 = atermpp::read_term_from_string("h(f(g(x),g(x)),f(g(x),g(x)))");
266 1 : BOOST_CHECK(t1 == t2);
267 1 : BOOST_CHECK(cache.size() == 4);
268 1 : }
269 :
|
