21class dependencies_rewrite_rule_pair
50 std::vector<strategy_rule> strat;
52 std::vector <bool> used;
54 std::size_t arity = 0;
55 std::size_t max_number_of_variables = 0;
56 while (!rules.
empty())
59 std::vector<dependencies_rewrite_rule_pair> m;
61 std::vector<int> args(arity,-1);
65 max_number_of_variables=std::max(this_rule.variables().size(),max_number_of_variables);
72 std::vector < bool> bs(arity,
false);
74 for (std::size_t i = 0; i < arity; i++)
84 const atermpp::term_list <variable_list>& next_vars=vars.
tail();
87 if (std::find(o->begin(),o->end(),*v) != o->end())
102 if (std::find(o->begin(),o->end(),
variable(this_rule_lhs_iplus1_arg)) != o->end())
116 vars=push_back(vars,
get_free_vars(this_rule_lhs_iplus1_arg));
123 lhs_doubles.
apply(this_rule.lhs());
124 rhs_doubles.
apply(this_rule.rhs());
126 std::set<std::size_t> deps;
127 for (std::size_t i = 0; i < arity; i++)
131 used.resize(i+1,
false);
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))
158 std::vector<dependencies_rewrite_rule_pair> m2;
161 if (p.dependencies().empty())
179 std::size_t maxidx = 0;
181 for (std::size_t i = 0; i < arity; i++)
183 assert(i<((std::size_t)1)<<(8*
sizeof(
int)-1));
194 if (maxidx>used.size())
196 used.resize(maxidx,
false);
198 used[maxidx-1] =
true;
200 const std::size_t k(maxidx-1);
206 std::set<std::size_t> dependencies=p.dependencies();
207 dependencies.erase(k);
217 return strategy(max_number_of_variables,strat);
224 size_t number_of_arguments=0;
227 number_of_arguments=atermpp::down_cast<function_sort>(f.
sort()).domain().size();
230 std::vector<strategy_rule> result;
231 for(
size_t i=0; i<number_of_arguments; ++i)
250 assert(rules1.
size()==0);
size_type size() const
Returns the size of the term_list.
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
const term_list< Term > & tail() const
Returns the tail of the list.
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
term_list_iterator< Term > const_iterator
Const iterator used to iterate through an term_list.
bool empty() const
Returns true if the list's size is 0.
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
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)
strategy create_a_cpp_function_based_strategy(const function_symbol &f, const data_specification &data_spec)
strategy create_strategy(const function_symbol &f, const data_equation_list &rules1, const data_specification &data_spec)
std::set< std::size_t > m_dependencies
const std::set< std::size_t > & dependencies() const
const data_equation equation() const
dependencies_rewrite_rule_pair(std::set< std::size_t > &dependencies, const data_equation &eq)
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.
const sort_expression & sort() const
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)
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...
void apply(const variable &v)
const std::set< variable > & result()
A rule describes a partially pattern-matched rewrite rule.