Line data Source code
1 : // Author(s): Jan Friso Groote
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/representative_generator.h
10 : /// \brief Component for generating representatives of sorts
11 :
12 : #ifndef MCRL2_DATA_REPRESENTATIVE_GENERATOR_H
13 : #define MCRL2_DATA_REPRESENTATIVE_GENERATOR_H
14 :
15 : #include "mcrl2/data/data_specification.h"
16 :
17 : namespace mcrl2
18 : {
19 :
20 : namespace data
21 : {
22 : /// \brief Components for generating an arbitrary element of a sort
23 : /// \details This component is not deterministic. So, it is not guaranteed
24 : /// to deliver the same element each time it is run.
25 : ///
26 : /// A representative is an arbitrary element of a given sort. This
27 : /// component takes a specification and generates representatives for sorts
28 : /// defined by the specification. An important property is that for the
29 : /// same sort the same representative is returned. For this it assumes
30 : /// that the context -constructors and mappings for the sort- remain
31 : /// unchanged.
32 : ///
33 : /// The general aim is to keep the representative expression as simple. Use of
34 : /// constructors is preferred above mappings and constructors or
35 : /// mappings representing constants are preferred over those that have
36 : /// non-empty domain.
37 : ///
38 : /// Constructors and functions that have arrows in their target sorts
39 : /// (e.g. f:A->(B->C)) are not used to construct default terms. Once an
40 : /// element is generated it is kept for later requests, which is done for
41 : /// performance when used frequently on the same specification. At some
42 : /// point a sufficiently advanced enumerator may be used to replace the
43 : /// current implementation.
44 : ///
45 : /// This component will evolve through time, in the sense that more
46 : /// complex expressions will be generated over time to act as
47 : /// representative a certain sort, for instance containing function symbols
48 : /// with complex target sorts, containing explicit function constructors
49 : /// (lambda's). So, no reliance is possible on the particular shape of the
50 : /// terms that are generated.
51 :
52 : class representative_generator
53 : {
54 :
55 : protected:
56 :
57 : /// \brief Data specification context
58 : const data_specification& m_specification;
59 :
60 : /// \brief Serves as a cache for later find operations
61 : std::map< sort_expression, data_expression > m_representatives_cache;
62 :
63 : protected:
64 :
65 : /// \brief Sets a data expression as representative of the sort
66 : /// \param[in] sort the sort of which to set the representative
67 : /// \param[in] representative the data expression that serves as representative
68 696 : void set_representative(const sort_expression& sort, const data_expression& representative)
69 : {
70 696 : assert(sort==representative.sort());
71 696 : m_representatives_cache[sort] = representative;
72 696 : }
73 :
74 : /// \brief Finds a representative of the form f(t1,...,tn) where f is the function symbol.
75 : /// \param[in] symbol The function symbol f using which the representative is constructed.
76 : /// \param[in] visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent
77 : // an infinite circular search through the sorts.
78 : /// \param[out] result The representative of the shape f(t1,...,tn). This is only set if this function yields true.
79 : /// \return a boolean indicating whether a representative has successfully been found.
80 : /// \pre symbol.sort() is of type function_sort
81 39 : bool find_representative(
82 : const function_symbol& symbol,
83 : std::set < sort_expression >& visited_sorts,
84 : data_expression& result)
85 : {
86 39 : assert(is_function_sort(symbol.sort()));
87 :
88 39 : data_expression_vector arguments;
89 :
90 81 : for (const sort_expression& s: static_cast<const function_sort&>(symbol.sort()).domain())
91 : {
92 47 : data_expression representative;
93 47 : if (find_representative(s, visited_sorts, representative))
94 : {
95 42 : arguments.push_back(representative);
96 : }
97 : else
98 : {
99 : // a representative for this argument could not be found.
100 5 : return false;
101 : }
102 47 : }
103 :
104 : // a suitable set of arguments is found
105 34 : result=application(symbol, arguments);
106 34 : return true;
107 39 : }
108 :
109 : /// \brief Finds a representative element for an arbitrary sort expression
110 : /// \param[in] sort the sort for which to find the representative
111 : /// \param[in] visited_sorts A set of sorts for which no representative can be constructed. This is used to prevent
112 : // an infinite circular search through the sorts.
113 : /// \param[out] result The representative of the shape f(t1,...,tn). This is only set if this function yields true.
114 : /// \return a boolean indicating whether a representative has successfully been found.
115 710 : bool find_representative(
116 : const sort_expression& sort,
117 : std::set < sort_expression >& visited_sorts,
118 : data_expression& result)
119 : {
120 710 : if (visited_sorts.count(sort)>0)
121 : {
122 : // This sort is already visited. We are looking to find a representative term of this sort
123 : // within the scope of finding a term of this sort. If this is to be succesful, a more compact
124 : // term can be found. Hence, stop searching further.
125 5 : return false;
126 : }
127 :
128 705 : const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
129 705 : if (i!=m_representatives_cache.end())
130 : {
131 3 : assert(i->second.sort()==sort);
132 3 : result=i->second;
133 3 : return true;
134 : }
135 :
136 702 : if (is_function_sort(sort))
137 : {
138 : // s is a function sort.
139 : // First check if there is a mapping with sort s (constructors with sort s cannot exist).
140 9 : const function_sort& fs=atermpp::down_cast<function_sort>(sort);
141 188 : for (const function_symbol& f: m_specification.mappings(fs.codomain()))
142 : {
143 187 : if (f.sort()==sort)
144 : {
145 8 : result=f;
146 8 : set_representative(sort, result);
147 8 : return true;
148 : }
149 : }
150 : // If no explicit constant is found of this sort, we know that its shape is "s0#..#sn -> s".
151 : // We search a term t of sort s and if found, construct a lambda term of the shape
152 : // lambda x0:s0,...,xn:sn.t. Note that this can be strengthened slightly by incorporating
153 : // the variables xi in generating t, e.g. generating for D->D the reprentant lambd d:D.d.
154 : // Incorporating the variables in the generation of terms requires adapting all algorithms,
155 : // and is not done. Until now the need for such representant generators has not been felt.
156 :
157 1 : const sort_expression& s2=fs.codomain();
158 1 : data_expression t;
159 1 : if (find_representative(s2, visited_sorts, t))
160 : {
161 1 : variable_vector bound_variables;
162 1 : std::size_t variable_index=0;
163 3 : for(const sort_expression& s: fs.domain())
164 : {
165 2 : bound_variables.emplace_back("x" + std::to_string(variable_index), s);
166 2 : variable_index++;
167 : }
168 1 : result=abstraction(lambda_binder(),variable_list(bound_variables.begin(),bound_variables.end()),t);
169 1 : return true;
170 1 : }
171 1 : }
172 : else
173 : {
174 : // s is a constant (not a function sort).
175 : // check if there is a constant constructor for s
176 :
177 744 : for (const function_symbol& f: m_specification.constructors(sort))
178 : {
179 705 : if (f.sort()==sort)
180 : {
181 654 : result=f;
182 654 : set_representative(sort, result);
183 654 : return true;
184 : }
185 : }
186 :
187 39 : visited_sorts.insert(sort);
188 :
189 : // Check whether there is a representative f(t1,...,tn) for s, where f is a constructor function.
190 : // We prefer this over a constant mapping, as a constant mapping generally does not have appropriate
191 : // rewrite rules.
192 :
193 : // recursively traverse constructor functions of the form f:s1#...#sn -> sort.
194 : // operators with f:s1#...#sn->G where G is a complex sort expression are ignored
195 39 : for (const function_symbol& f: m_specification.constructors(sort))
196 : {
197 32 : if (find_representative(f, visited_sorts, result))
198 : {
199 32 : set_representative(sort, result);
200 32 : visited_sorts.erase(sort);
201 32 : return true;
202 : }
203 : }
204 :
205 : // check if there is a constant mapping for s
206 58 : for (const function_symbol& f: m_specification.mappings(sort))
207 : {
208 51 : if (f.sort()==sort)
209 : {
210 0 : result=f;
211 0 : set_representative(sort, result);
212 0 : visited_sorts.erase(sort);
213 0 : return true;
214 : }
215 : }
216 :
217 : // Try to check whether there is a representative f(t1,...,tn) where f is a mapping.
218 12 : for (const function_symbol& f: m_specification.mappings(sort))
219 : {
220 7 : if (find_representative(f, visited_sorts, result))
221 : {
222 2 : set_representative(sort, result);
223 2 : visited_sorts.erase(sort);
224 2 : return true;
225 : }
226 : }
227 :
228 5 : visited_sorts.erase(sort);
229 :
230 : }
231 :
232 : // No representative has been found.
233 5 : return false;
234 : }
235 :
236 : public:
237 :
238 : /// \brief Constructor with data specification as context
239 782 : representative_generator(const data_specification& specification) : m_specification(specification)
240 : {
241 782 : }
242 :
243 : /// \brief Returns a representative of a sort
244 : /// \param[in] sort sort of which to find a representatitive
245 1129 : data_expression operator()(const sort_expression& sort)
246 : {
247 : // First see whether a term of this sort has already been constructed and resides in the representatives_cache. If yes return it.
248 1129 : const std::map< sort_expression, data_expression >::iterator i=m_representatives_cache.find(sort);
249 1129 : if (i!=m_representatives_cache.end())
250 : {
251 467 : return i->second;
252 : }
253 :
254 662 : data_expression result;
255 662 : std::set<sort_expression> visited_sorts;
256 662 : if (find_representative(sort, visited_sorts, result))
257 : {
258 : // A term of the requested sort is found. Return it.
259 657 : return result;
260 : }
261 : else
262 : {
263 5 : throw mcrl2::runtime_error("Cannot find a term of sort " + data::pp(sort));
264 : }
265 :
266 667 : }
267 : };
268 :
269 : } // namespace data
270 : } // namespace mcrl2
271 : #endif
272 :
|