Line data Source code
1 : // Author(s): Luc Engelen
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 : /// \file mcrl2/data/detail/prover/induction.h
10 : /// \brief Proving with induction on lists
11 :
12 : #ifndef MCRL2_DATA_DETAIL_PROVER_INDUCTION_H
13 : #define MCRL2_DATA_DETAIL_PROVER_INDUCTION_H
14 :
15 : #include "mcrl2/data/list.h"
16 : #include "mcrl2/data/replace.h"
17 : #include "mcrl2/data/representative_generator.h"
18 : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
19 :
20 : namespace mcrl2
21 : {
22 : namespace data
23 : {
24 : namespace detail
25 : {
26 : /// The class Induction generates statements corresponding to
27 :
28 : class Induction
29 : {
30 : private:
31 : set_identifier_generator fresh_identifier_generator;
32 :
33 : /// \brief The number of variables used during the last application of induction.
34 : std::size_t f_count;
35 :
36 : /// \brief An expression of sort Bool in mCRL2 format.
37 : data_expression f_formula;
38 :
39 : /// \brief
40 : variable_vector f_list_variables;
41 :
42 : /// \brief
43 : // BDD_Info f_bdd_info;
44 :
45 : /// \brief
46 0 : variable_vector recurse_expression_for_lists(const data_expression& a_expression) const
47 : {
48 0 : variable_vector result;
49 0 : for(const variable& v: find_free_variables(a_expression))
50 : {
51 0 : if(sort_list::is_list(v.sort()))
52 : {
53 0 : result.push_back(v);
54 : }
55 0 : }
56 0 : return result;
57 0 : }
58 :
59 : /// \brief
60 0 : sort_expression get_sort_of_list_elements(const variable& a_list_variable) const
61 : {
62 0 : assert(sort_list::is_list(a_list_variable.sort()));
63 0 : return atermpp::down_cast<container_sort>(a_list_variable.sort()).element_sort();
64 : }
65 :
66 : /// \brief
67 0 : variable get_fresh_dummy(const sort_expression& a_sort)
68 : {
69 0 : return variable(fresh_identifier_generator("dummy$"),a_sort);
70 : }
71 :
72 :
73 : //TODO check if this special case can be integrated into create_clauses
74 0 : data_expression apply_induction_one(const core::identifier_string& fresh_name) const
75 : {
76 0 : const variable v_induction_variable = f_list_variables.front();
77 0 : assert(sort_list::is_list(v_induction_variable.sort()));
78 :
79 0 : const sort_expression v_dummy_sort = get_sort_of_list_elements(v_induction_variable);
80 0 : const variable v_dummy_variable(fresh_name, v_dummy_sort);
81 :
82 0 : mutable_map_substitution<> v_substitution1;
83 0 : v_substitution1[v_induction_variable] = sort_list::empty(v_dummy_sort);
84 0 : const data_expression v_base_case = replace_variables_capture_avoiding(f_formula, v_substitution1);
85 :
86 0 : mutable_map_substitution<> v_substitution2;
87 0 : v_substitution2[v_induction_variable] = sort_list::cons_(v_dummy_sort, v_dummy_variable, v_induction_variable);
88 0 : const data_expression v_induction_step = sort_bool::implies(f_formula, replace_variables_capture_avoiding(f_formula, v_substitution2));
89 :
90 0 : return sort_bool::and_(v_base_case, v_induction_step);
91 0 : }
92 :
93 : /// \brief
94 0 : data_expression create_hypotheses(
95 : const data_expression& a_hypothesis,
96 : variable_list a_list_of_variables,
97 : variable_list a_list_of_dummies) const
98 : {
99 0 : if (a_list_of_variables.empty())
100 : {
101 0 : return sort_bool::true_();
102 : }
103 : else
104 : {
105 0 : data_expression v_clause = a_hypothesis;
106 0 : if (a_list_of_variables.size() > 1)
107 : {
108 0 : for (const variable& v_variable: a_list_of_variables)
109 : {
110 0 : const variable v_dummy(a_list_of_dummies.front());
111 0 : a_list_of_dummies.pop_front();
112 :
113 0 : mutable_map_substitution<> v_substitution;
114 0 : v_substitution[v_variable] = sort_list::cons_(v_dummy.sort(), v_dummy, v_variable);
115 0 : v_clause = sort_bool::and_(v_clause, replace_variables_capture_avoiding(a_hypothesis, v_substitution));
116 0 : }
117 : }
118 :
119 0 : return v_clause;
120 0 : }
121 : }
122 :
123 : /// \brief
124 0 : data_expression_list create_clauses(const data_expression& a_formula,
125 : const data_expression& a_hypothesis,
126 : const std::size_t a_variable_number,
127 : const std::size_t a_number_of_variables,
128 : const variable_list& a_list_of_variables,
129 : const variable_list& a_list_of_dummies)
130 : {
131 0 : const variable v_variable = f_list_variables[a_variable_number];
132 0 : variable_list v_list_of_variables = a_list_of_variables;
133 0 : v_list_of_variables.push_front(v_variable);
134 0 : const sort_expression v_dummy_sort = get_sort_of_list_elements(v_variable);
135 0 : const variable v_dummy = get_fresh_dummy(v_dummy_sort);
136 0 : variable_list v_list_of_dummies = a_list_of_dummies;
137 0 : v_list_of_dummies.push_front(v_dummy);
138 :
139 0 : mutable_map_substitution<> v_substitution1;
140 0 : v_substitution1[v_variable] = sort_list::cons_(v_dummy_sort, v_dummy, v_variable);
141 0 : const data_expression v_formula_1 = replace_variables_capture_avoiding(a_formula, v_substitution1);
142 :
143 0 : mutable_map_substitution<> v_substitution2;
144 0 : assert(sort_list::is_list(v_variable.sort()));
145 0 : v_substitution2[v_variable] = sort_list::empty(v_dummy_sort);
146 0 : const data_expression v_formula_2 = replace_variables_capture_avoiding(a_formula, v_substitution2);
147 0 : const data_expression v_hypothesis = replace_variables_capture_avoiding(a_hypothesis, v_substitution2);
148 :
149 0 : if (a_variable_number < a_number_of_variables - 1)
150 : {
151 0 : const data_expression_list v_list_1 = create_clauses(v_formula_1, a_hypothesis, a_variable_number + 1, a_number_of_variables, v_list_of_variables, v_list_of_dummies);
152 0 : const data_expression_list v_list_2 = create_clauses(v_formula_2, v_hypothesis, a_variable_number + 1, a_number_of_variables, a_list_of_variables, a_list_of_dummies);
153 0 : return v_list_1 + v_list_2;
154 0 : }
155 : else
156 : {
157 0 : data_expression v_hypotheses_1 = create_hypotheses(a_hypothesis, v_list_of_variables, v_list_of_dummies);
158 0 : data_expression v_hypotheses_2 = create_hypotheses(v_hypothesis, a_list_of_variables, a_list_of_dummies);
159 0 : data_expression_list result;
160 0 : result.push_front(sort_bool::implies(v_hypotheses_2, v_formula_2));
161 0 : result.push_front(sort_bool::implies(v_hypotheses_1, v_formula_1));
162 0 : return result;
163 0 : }
164 0 : }
165 :
166 : public:
167 0 : void initialize(const data_expression& a_formula)
168 : {
169 0 : f_formula = a_formula;
170 0 : f_list_variables = recurse_expression_for_lists(a_formula);
171 0 : f_count = 0;
172 0 : }
173 :
174 0 : bool can_apply_induction() const
175 : {
176 0 : return f_list_variables.size() != f_count;
177 : }
178 :
179 : /// \requires can_apply_induction()
180 0 : data_expression apply_induction()
181 : {
182 0 : assert(can_apply_induction());
183 0 : data_expression v_result;
184 :
185 0 : f_count++;
186 0 : if (f_count == 1)
187 : {
188 0 : mCRL2log(log::verbose) << "Induction on one variable." << std::endl;
189 0 : v_result = apply_induction_one(fresh_identifier_generator("dummy$"));
190 : }
191 : else
192 : {
193 0 : mCRL2log(log::verbose) << "Induction on " << f_count << " variables." << std::endl;
194 0 : data_expression_list v_list_of_clauses = create_clauses(f_formula, f_formula, 0, f_count, variable_list(), variable_list());
195 0 : v_result = v_list_of_clauses.front();
196 0 : v_list_of_clauses.pop_front();
197 0 : while (!v_list_of_clauses.empty())
198 : {
199 0 : data_expression v_clause(v_list_of_clauses.front());
200 0 : v_list_of_clauses.pop_front();
201 0 : v_result = sort_bool::and_(v_result, v_clause);
202 0 : }
203 0 : }
204 0 : return v_result;
205 0 : }
206 : };
207 :
208 : } // namespace detail
209 : } // namespace data
210 : } // namespace mcrl2
211 :
212 : #endif
|