mCRL2
Loading...
Searching...
No Matches
one_point_rule_rewriter.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
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//
11
12#ifndef MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H
13#define MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H
14
19#include "mcrl2/data/replace.h"
21
22namespace mcrl2::data
23{
24
25namespace detail
26{
27
28template <typename Derived>
30{
31 public:
33
34 using super::apply;
35
36 Derived& derived()
37 {
38 return static_cast<Derived&>(*this);
39 }
40
41 template <class T>
42 void apply(T& result, const forall& x)
43 {
44 data_expression body;
45 derived().apply(body, x.body());
46 std::vector<variable> variables;
47
48 std::map<variable, std::set<data_expression> > inequalities = find_inequalities(body);
49 if (!inequalities.empty())
50 {
51 auto [sigma, remaining_variables] = make_one_point_rule_substitution(inequalities, x.variables());
52 if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
53 {
54 mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
56 mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
57 if (remaining_variables.empty())
58 {
59 mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
60 result = body;
61 return;
62 }
63 data::variable_list v(remaining_variables.begin(), remaining_variables.end());
64 mCRL2log(log::debug) << "Replaced " << x << "\nwith " << forall(v, body) << std::endl;
65 make_forall(result, v, body);
66 return;
67 }
68 }
69 make_forall(result, x.variables(), body);
70 }
71
72 template <class T>
73 void apply(T& result, const exists& x)
74 {
75 data_expression body;
76 derived().apply(body, x.body());
77 std::vector<variable> variables;
78
79 std::map<variable, std::set<data_expression> > equalities = find_equalities(body);
80 if (!equalities.empty())
81 {
82 auto [sigma, remaining_variables] = make_one_point_rule_substitution(equalities, x.variables());
83 if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
84 {
85 mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
87 mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
88 if (remaining_variables.empty())
89 {
90 mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
91 result = body;
92 return;
93 }
94 data::variable_list v(remaining_variables.begin(), remaining_variables.end());
95 mCRL2log(log::debug) << "Replaced " << x << "\nwith " << exists(v, body) << std::endl;
96 make_exists(result, v, body);
97 return;
98 }
99 }
100 make_exists(result, x.variables(), body);
101 }
102};
103
104} // namespace detail
105
107{
110
112 {
113 data_expression result;
114 core::make_apply_builder<detail::one_point_rule_rewrite_builder>().apply(result, x);
115 return result;
116 }
117};
118
119template <typename T>
120void one_point_rule_rewrite(T& x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
121{
122 core::make_update_apply_builder<data::data_expression_builder>(one_point_rule_rewriter()).update(x);
123}
124
125template <typename T>
126T one_point_rule_rewrite(const T& x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
127{
128 T result;
129 core::make_update_apply_builder<data::data_expression_builder>(one_point_rule_rewriter()).apply(result, x);
130 return result;
131}
132
133} // namespace mcrl2::data
134
135#endif // MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
existential quantification.
Definition exists.h:26
universal quantification.
Definition forall.h:26
add your file description here.
add your file description here.
Contains term traits for data_expression.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
add your file description here.
Namespace for all data library functionality.
Definition abstraction.h:22
std::map< variable, std::set< data_expression > > find_inequalities(const data_expression &x)
std::map< variable, std::set< data_expression > > find_equalities(const data_expression &x)
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
void make_forall(atermpp::aterm &result, ARGUMENTS... arguments)
Definition forall.h:64
void one_point_rule_rewrite(T &x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value >::type *=0)
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)
void make_exists(atermpp::aterm &result, ARGUMENTS... arguments)
Definition exists.h:64
add your file description here.
void apply(T &result, const data::variable &x)
Definition builder.h:443
data_expression operator()(const data_expression &x) const