12#ifndef MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
13#define MCRL2_DATA_EQUALITY_ONE_POINT_SUBSTITUTION_H
26 std::map<data::variable, std::vector<data::data_expression> >
equalities;
47 std::vector<data::variable> to_be_removed;
56 to_be_removed.push_back(lhs);
70 return !to_be_removed.empty();
77 std::set<data::variable> to_be_removed;
91 to_be_removed.insert(lhs);
92 to_be_removed.insert(FV.begin(), FV.end());
96 if (!to_be_removed.empty())
111 return !to_be_removed.empty();
117 for (
const auto& [lhs,exprs]: equalities_)
123 std::vector<data::data_expression> E;
151 while (find_all_assignments)
163 std::pair<data::mutable_map_substitution<>, std::vector<data::variable> >
run(
const data::variable_list& quantifier_variables,
bool find_all_assignments =
true)
167 run(find_all_assignments);
169 std::vector<data::variable> remaining_variables;
174 remaining_variables.push_back(v);
178 return std::make_pair(
sigma, remaining_variables);
191 const std::map<
data::variable, std::set<data::data_expression> >& equalities,
193 bool find_all_assignments =
true)
196 return algorithm.
run(quantifier_variables, find_all_assignments);
204 const std::map<
data::variable, std::set<data::data_expression> >& equalities,
205 bool find_all_assignments =
true)
208 return algorithm.
run(find_all_assignments);
Generic substitution function. The substitution is stored as a mapping of variables to expressions....
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
void add_identifier(const core::identifier_string &s) override
Adds the identifier s to the context.
add your file description here.
add your file description here.
static void check_vars(const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
Namespace for all data library functionality.
std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > make_one_point_rule_substitution(const std::map< data::variable, std::set< data::data_expression > > &equalities, const data::variable_list &quantifier_variables, bool find_all_assignments=true)
creates a substitution from a set of (in-)equalities for a given list of quantifier variables
std::set< data::variable > find_free_variables(const data::data_expression &x)
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
bool is_constant(const data_expression &x)
bool contains(const atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable > &c, const typename atermpp::indexed_set< Key, ThreadSafe, Hash, Equals, Allocator, KeyTable >::key_type &v, const std::size_t thread_index=0)
one_point_rule_substitution_algorithm(const std::map< data::variable, std::set< data::data_expression > > &equalities_, const data::variable_list &quantifier_variables)
data::mutable_map_substitution sigma
data::set_identifier_generator id_generator
std::pair< data::mutable_map_substitution<>, std::vector< data::variable > > run(const data::variable_list &quantifier_variables, bool find_all_assignments=true)
one_point_rule_substitution_algorithm(const std::map< data::variable, std::set< data::data_expression > > &equalities_)
data::mutable_map_substitution run(bool find_all_assignments=true)
std::map< data::variable, std::vector< data::data_expression > > equalities
bool find_constant_assignments()
void build_equality_map(const std::map< data::variable, std::set< data::data_expression > > &equalities_, bool check_vars, const data::variable_list &vars=data::variable_list())
std::set< data::variable > sigma_lhs_variables