mCRL2
Loading...
Searching...
No Matches
strategy.cpp
Go to the documentation of this file.
1// Author(s): Muck van Weerdenburg, 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
13
14namespace mcrl2
15{
16namespace data
17{
18namespace detail
19{
20
21class dependencies_rewrite_rule_pair
22{
23 protected:
24 std::set<std::size_t> m_dependencies;
25 data_equation m_equation;
26
27 public:
30 {}
31
32 const std::set<std::size_t>& dependencies() const
33 {
34 return m_dependencies;
35 }
36
37 const data_equation equation() const
38 {
39 return m_equation;
40 }
41};
42
43// Create a strategy for the rewrite rules belonging to one particular symbol.
44// It is a prerequisite for this function to that all rewrite rules in rules1 have
45// the same main function symbol in the lhs.
47{
48 static_cast<void>(f); // Avoid an unused variable warning.
49 data_equation_list rules=rules1;
50 std::vector<strategy_rule> strat;
51
52 std::vector <bool> used;
53
54 std::size_t arity = 0;
55 std::size_t max_number_of_variables = 0;
56 while (!rules.empty())
57 {
59 std::vector<dependencies_rewrite_rule_pair> m;
60
61 std::vector<int> args(arity,-1);
62
63 for (const data_equation& this_rule: rules)
64 {
65 max_number_of_variables=std::max(this_rule.variables().size(),max_number_of_variables);
66 const data_expression& this_rule_lhs = this_rule.lhs();
67 if ((is_function_symbol(this_rule_lhs)?1:detail::recursive_number_of_args(this_rule_lhs)+1) == arity + 1)
68 {
69 const data_expression& cond = this_rule.condition();
71
72 std::vector < bool> bs(arity,false);
73
74 for (std::size_t i = 0; i < arity; i++)
75 {
76 const data_expression this_rule_lhs_iplus1_arg=detail::get_argument_of_higher_order_term(atermpp::down_cast<application>(this_rule_lhs),i);
77 if (!is_variable(this_rule_lhs_iplus1_arg))
78 {
79 bs[i] = true;
80 const variable_list evars = get_free_vars(this_rule_lhs_iplus1_arg);
81 for (variable_list::const_iterator v=evars.begin(); v!=evars.end(); ++v)
82 {
83 int j=0;
84 const atermpp::term_list <variable_list>& next_vars=vars.tail();
85 for (atermpp::term_list <variable_list>::const_iterator o=next_vars.begin(); o!=next_vars.end(); ++o)
86 {
87 if (std::find(o->begin(),o->end(),*v) != o->end())
88 {
89 bs[j] = true;
90 }
91 j++;
92 }
93 }
94 vars=push_back(vars,get_free_vars(this_rule_lhs_iplus1_arg));
95 }
96 else
97 {
98 int j = -1;
99 bool b = false;
101 {
102 if (std::find(o->begin(),o->end(),variable(this_rule_lhs_iplus1_arg)) != o->end())
103 {
104 if (j >= 0)
105 {
106 bs[j] = true;
107 }
108 b = true;
109 }
110 j++;
111 }
112 if (b)
113 {
114 bs[i] = true;
115 }
116 vars=push_back(vars,get_free_vars(this_rule_lhs_iplus1_arg));
117 }
118 }
119
122 std::set<variable> condition_vars = find_free_variables(this_rule.condition());
123 lhs_doubles.apply(this_rule.lhs());
124 rhs_doubles.apply(this_rule.rhs());
125
126 std::set<std::size_t> deps;
127 for (std::size_t i = 0; i < arity; i++)
128 {
129 if (i>=used.size())
130 {
131 used.resize(i+1,false);
132 }
133 // Check whether argument i is a variable that occurs more than once in
134 // the left or right hand side, or occurs in the condition. It is not clear whether it is
135 // useful to check that it occurs in the condition, but this is what the jittyc rewriter also does.
136 const data_expression& arg_i = get_argument_of_higher_order_term(atermpp::down_cast<application>(this_rule.lhs()), i);
137 if ((bs[i] ||
138 (is_variable(arg_i) && (lhs_doubles.result().count(atermpp::down_cast<variable>(arg_i)) > 0 ||
139 condition_vars.count(atermpp::down_cast<variable>(arg_i)) > 0 ||
140 rhs_doubles.result().count(atermpp::down_cast<variable>(arg_i)) > 0))
141 ) && !used[i])
142 {
143 deps.insert(i);
144 args[i] += 1;
145 }
146 }
147
148 m.push_back(dependencies_rewrite_rule_pair(deps,this_rule));
149 }
150 else
151 {
152 l.push_front(this_rule);
153 }
154 }
155
156 while (!m.empty())
157 {
158 std::vector<dependencies_rewrite_rule_pair> m2;
159 for (const dependencies_rewrite_rule_pair& p: m)
160 {
161 if (p.dependencies().empty())
162 {
163 const data_equation rule = p.equation();
164 strat.push_back(strategy_rule(rule));
165 }
166 else
167 {
168 m2.push_back(p);
169 }
170 }
171 m = m2;
172
173 if (m.empty())
174 {
175 break;
176 }
177
178 int max = -1;
179 std::size_t maxidx = 0;
180
181 for (std::size_t i = 0; i < arity; i++)
182 {
183 assert(i<((std::size_t)1)<<(8*sizeof(int)-1));
184 if (args[i] > max)
185 {
186 maxidx = i+1;
187 max = args[i];
188 }
189 }
190
191 if (maxidx > 0)
192 {
193 args[maxidx-1] = -1;
194 if (maxidx>used.size())
195 {
196 used.resize(maxidx,false);
197 }
198 used[maxidx-1] = true;
199
200 const std::size_t k(maxidx-1);
201 strat.push_back(strategy_rule(k));
202 m2.clear();
203 for (const dependencies_rewrite_rule_pair& p: m)
204 {
205 const data_equation eq=p.equation();
206 std::set<std::size_t> dependencies=p.dependencies();
207 dependencies.erase(k);
208 m2.push_back(dependencies_rewrite_rule_pair(dependencies,eq));
209 }
210 m = m2;
211 }
212 }
213
214 rules = reverse(l);
215 arity++;
216 }
217 return strategy(max_number_of_variables,strat);
218}
219
220// Create an explicit rewrite strategy when rewriting using an explicitly given
221// C++ function. First rewrite all the arguments, then apply the function.
223{
224 size_t number_of_arguments=0;
225 if (is_function_sort(f.sort()))
226 {
227 number_of_arguments=atermpp::down_cast<function_sort>(f.sort()).domain().size();
228 }
229 // Indicate that all arguments must be rewritten first.
230 std::vector<strategy_rule> result;
231 for(size_t i=0; i<number_of_arguments; ++i)
232 {
233 result.push_back(strategy_rule(i));
234 }
235 result.push_back(strategy_rule(data_spec.cpp_implemented_functions().find(f)->second.first));
236
237 return strategy(0,result);
238}
239
240// Create a strategy to rewrite terms. This can either be a strategy that is based on rewrite
241// rules or it can be a strategy based on an explicitly given c++ function for this function symbol.
243{
244 if (data_spec.cpp_implemented_functions().count(f)==0) // There is no explicit implementation.
245 {
246 return create_a_rewriting_based_strategy(f, rules1);
247 }
248 else
249 {
250 assert(rules1.size()==0); // There should be no explicit rewrite rules, as this function is implemented by
251 // an explicit C++ function.
252 return create_a_cpp_function_based_strategy(f, data_spec);
253 }
254}
255
256} // namespace detail
257} // namespace data
258} // namespace mcrl2
Iterator for term_list.
A list of aterm objects.
Definition aterm_list.h:24
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const term_list< Term > & tail() const
Returns the tail of the list.
Definition aterm_list.h:225
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
term_list_iterator< Term > const_iterator
Const iterator used to iterate through an term_list.
Definition aterm_list.h:55
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief A data equation
const implementation_map & cpp_implemented_functions() const
Gets all equations in this specification including those that are system defined.
strategy create_a_rewriting_based_strategy(const function_symbol &f, const data_equation_list &rules1)
Definition strategy.cpp:46
strategy create_a_cpp_function_based_strategy(const function_symbol &f, const data_specification &data_spec)
Definition strategy.cpp:222
strategy create_strategy(const function_symbol &f, const data_equation_list &rules1, const data_specification &data_spec)
Definition strategy.cpp:242
const std::set< std::size_t > & dependencies() const
Definition jitty.cpp:121
dependencies_rewrite_rule_pair(std::set< std::size_t > &dependencies, const data_equation &eq)
Definition strategy.cpp:28
Is either a rewrite rule to be matched or an index that should be rewritten.
A strategy is a list of rules and the number of variables that occur in it.
\brief A function symbol
const sort_expression & sort() const
\brief A data variable
Definition variable.h:28
std::size_t recursive_number_of_args(const data_expression &t)
const data_expression & get_argument_of_higher_order_term(const application &t, std::size_t i)
variable_list get_free_vars(const data_expression &a)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
data_expression max(const data_expression &e1, const data_expression &e2, const rewriter &)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
const std::set< variable > & result()
A rule describes a partially pattern-matched rewrite rule.