LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/prover - induction.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 1 85 1.2 %
Date: 2020-09-22 00:46:14 Functions: 2 11 18.2 %
Legend: Lines: hit not hit

          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          36 : 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             :       }
      56           0 :       return result;
      57             :     }
      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             :     }
      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             :           }
     117             :         }
     118             : 
     119           0 :         return v_clause;
     120             :       }
     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             :       }
     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             :       }
     164             :     }
     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             :         }
     203             :       }
     204           0 :       return v_result;
     205             :     }
     206             : };
     207             : 
     208             : } // namespace detail
     209             : } // namespace data
     210             : } // namespace mcrl2
     211             : 
     212             : #endif

Generated by: LCOV version 1.13