mcrl2/data/equality_one_point_substitution.h

Include file:

#include "mcrl2/data/equality_one_point_substitution.h"

Classes

  • mcrl2::data::detail::one_point_rule_substitution_algorithm

Functions

data::mutable_map_substitution mcrl2::data::make_one_point_rule_substitution(const std::map<data::variable, std::set<data::data_expression>> &equalities, bool find_all_assignments = true)

creates a substitution from a set of (in-)equalities

Parameters:

  • find_all_assignments True to find all assignments, false to find only constant assignments

Returns: the substitution

std::pair<data::mutable_map_substitution<>, std::vector<data::variable>> mcrl2::data::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

Parameters:

  • quantifier_variables Consider only these variables
  • find_all_assignments True to find all assignments, false to find only constant assignments

Returns: the substitution, and the subset of quantifier variables that are not used in the substitution