LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - constelm.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 312 463 67.4 %
Date: 2024-03-08 02:52:28 Functions: 38 91 41.8 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       2             : //
       3             : // Distributed under the Boost Software License, Version 1.0.
       4             : // (See accompanying file LICENSE_1_0.txt or copy at
       5             : // http://www.boost.org/LICENSE_1_0.txt)
       6             : //
       7             : /// \file mcrl2/pbes/constelm.h
       8             : /// \brief The constelm algorithm.
       9             : 
      10             : #ifndef MCRL2_PBES_CONSTELM_H
      11             : #define MCRL2_PBES_CONSTELM_H
      12             : 
      13             : #include "mcrl2/pbes/algorithms.h"
      14             : #include "mcrl2/pbes/pbes_rewriter_type.h"
      15             : #include "mcrl2/pbes/print.h"
      16             : #include "mcrl2/pbes/replace.h"
      17             : #include "mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : inline
      29         145 : void make_constelm_substitution(const std::map<data::variable, data::data_expression>& m, data::rewriter::substitution_type& result)
      30             : {
      31         287 :   for (const auto& i : m)
      32             :   {
      33         142 :     result[i.first] = i.second;
      34             :   }
      35         145 : }
      36             : 
      37             : class quantified_variable
      38             : {
      39             : protected:
      40             :   bool m_is_forall;
      41             :   data::variable m_var;
      42             : 
      43             : public:
      44           1 :   quantified_variable(bool is_forall, const data::variable& var)
      45           1 :   : m_is_forall(is_forall)
      46           1 :   , m_var(var)
      47           1 :   {}
      48             : 
      49           0 :   bool is_forall() const
      50             :   {
      51           0 :     return m_is_forall;
      52             :   }
      53             : 
      54           0 :   const data::variable& variable() const
      55             :   {
      56           0 :     return m_var;
      57             :   }
      58             : 
      59           0 :   bool operator==(const quantified_variable& other) const
      60             :   {
      61           0 :     return m_is_forall == other.m_is_forall && m_var == other.m_var;
      62             :   }
      63             : 
      64             :   bool operator!=(const quantified_variable& other) const
      65             :   {
      66             :     return !(*this == other);
      67             :   }
      68             : 
      69           0 :   bool operator<(const quantified_variable& other) const
      70             :   {
      71           0 :     return m_is_forall < other.m_is_forall || (m_is_forall == other.m_is_forall && m_var < other.m_var);
      72             :   }
      73             : 
      74           0 :   pbes_expression make_expr(const pbes_expression& expr) const
      75             :   {
      76           0 :     return m_is_forall ? pbes_expression(forall(data::variable_list({m_var}), expr)) : pbes_expression(exists(data::variable_list({m_var}), expr));
      77             :   }
      78             : 
      79           0 :   std::string to_string() const
      80             :   {
      81           0 :     std::ostringstream out;
      82           0 :     out << (is_forall() ? "forall " : "exists ") << variable() << ". ";
      83           0 :     return out.str();
      84           0 :   }
      85             : };
      86             : 
      87             : /// \brief A quantified predicate variable instantiation
      88             : struct QPVI
      89             : {
      90             :   std::list<quantified_variable> Q;
      91             :   propositional_variable_instantiation X_e;
      92             : 
      93          42 :   bool operator<(const QPVI& other) const
      94             :   {
      95          42 :     return std::tie(Q, X_e) < std::tie(other.Q, other.X_e);
      96             :   }
      97             : };
      98             : 
      99             : struct edge_details
     100             : {
     101             :   /// \brief Contains expressions that characterise when an edge is enabled.
     102             :   /// The conjunction of these expressions is a guard for some PVI.
     103             :   std::set<data::data_expression> conditions;
     104             :   /// \brief The set of free variables that occur on the other side of the conjunctions this
     105             :   /// PVI occurs in. Can be used to determine whether the quantifier inside rewriter
     106             :   /// can manage to push an existential quantifier all the way to this PVI.
     107             :   std::set<data::variable> conjunctive_context_FV;
     108             :   /// \brief The set of free variables that occur on the other side of the conjunctions this
     109             :   /// PVI occurs in. Can be used to determine whether the quantifier inside rewriter
     110             :   /// can manage to push a universal quantifier all the way to this PVI.
     111             :   std::set<data::variable> disjunctive_context_FV;
     112             : };
     113             : 
     114             : struct edge_traverser_stack_elem
     115             : {
     116             :   typedef std::multimap<QPVI, edge_details> edge_map;
     117             : 
     118             :   data::data_expression Cpos;
     119             :   data::data_expression Cneg;
     120             :   std::set<data::variable> FV;
     121             :   edge_map edges;
     122             : 
     123          87 :   edge_traverser_stack_elem(const data::data_expression& cond_pos, const data::data_expression& cond_neg, std::set<data::variable>&& free_vars)
     124          87 :     : Cpos(cond_pos), Cneg(cond_neg)
     125             :   {
     126          87 :     std::swap(FV, free_vars);
     127          87 :   }
     128             : };
     129             : 
     130             : struct edge_condition_traverser: public pbes_expression_traverser<edge_condition_traverser>
     131             : {
     132             :   typedef pbes_expression_traverser<edge_condition_traverser> super;
     133             :   using super::enter;
     134             :   using super::leave;
     135             :   using super::apply;
     136             : 
     137             :   typedef edge_traverser_stack_elem stack_elem;
     138             :   typedef stack_elem::edge_map edge_map;
     139             :   typedef std::list<detail::quantified_variable> qvar_list;
     140             : 
     141             :   std::vector<stack_elem> condition_fv_stack;
     142             :   std::list<pbes_expression> quantified_context;
     143             : 
     144          93 :   void push(const stack_elem& x)
     145             :   {
     146          93 :     condition_fv_stack.push_back(x);
     147          93 :   }
     148             : 
     149          64 :   stack_elem& top()
     150             :   {
     151          64 :     return condition_fv_stack.back();
     152             :   }
     153             : 
     154          29 :   const stack_elem& top() const
     155             :   {
     156          29 :     return condition_fv_stack.back();
     157             :   }
     158             : 
     159          64 :   stack_elem pop()
     160             :   {
     161          64 :     stack_elem result = top();
     162          64 :     condition_fv_stack.pop_back();
     163          64 :     return result;
     164             :   }
     165             : 
     166             :   // N.B. As a side effect ec1 and ec2 are changed!!!
     167          29 :   void merge_conditions(stack_elem& ec1, bool negate1,
     168             :                         stack_elem& ec2, bool negate2,
     169             :                         stack_elem& ec, bool is_conjunctive
     170             :                        )
     171             :   {
     172          39 :     for (auto& i: ec1.edges)
     173             :     {
     174          10 :       auto& [Q_X_e, details] = i;
     175          10 :       details.conditions.insert(negate2 ? ec2.Cneg : ec2.Cpos);
     176             :       (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
     177          10 :         .insert(ec2.FV.begin(), ec2.FV.end());
     178          10 :       ec.edges.insert(i);
     179             :     }
     180          66 :     for (auto& i: ec2.edges)
     181             :     {
     182          37 :       auto& [Q_X_e, details] = i;
     183          37 :       details.conditions.insert(negate1 ? ec1.Cneg : ec1.Cpos);
     184             :       (is_conjunctive ? details.conjunctive_context_FV : details.disjunctive_context_FV)
     185          37 :         .insert(ec1.FV.begin(), ec1.FV.end());
     186          37 :       ec.edges.insert(i);
     187             :     }
     188          29 :   }
     189             : 
     190             :   // enter functions related to maintaining the quantfier scope
     191           0 :   void enter(const not_&)
     192             :   {
     193           0 :     quantified_context.clear();
     194           0 :   }
     195             : 
     196          14 :   void enter(const and_&)
     197             :   {
     198          14 :     quantified_context.clear();
     199          14 :   }
     200             : 
     201          15 :   void enter(const or_&)
     202             :   {
     203          15 :     quantified_context.clear();
     204          15 :   }
     205             : 
     206           0 :   void enter(const imp&)
     207             :   {
     208           0 :     quantified_context.clear();
     209           0 :   }
     210             : 
     211           4 :   void enter(const forall& x)
     212             :   {
     213           4 :     quantified_context.push_back(x);
     214           4 :   }
     215             : 
     216           2 :   void enter(const exists& x)
     217             :   {
     218           2 :     quantified_context.push_back(x);
     219           2 :   }
     220             : 
     221             :   // leave functions, mostly used to build conditions and gather free variables
     222          19 :   void leave(const data::data_expression& x)
     223             :   {
     224          19 :     data::data_expression cond_not;
     225          19 :     data::optimized_not(cond_not, x);
     226             : 
     227          19 :     push(stack_elem(x, cond_not, data::find_free_variables(x)));
     228          19 :   }
     229             : 
     230           0 :   void leave(const not_&)
     231             :   {
     232           0 :     std::swap(top().Cpos, top().Cneg);
     233           0 :   }
     234             : 
     235          14 :   void leave(const and_&)
     236             :   {
     237          14 :     stack_elem ec_right = pop();
     238          14 :     stack_elem ec_left = pop();
     239          14 :     data::data_expression cond_and;
     240          14 :     data::data_expression cond_or;
     241          14 :     data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cpos);
     242          14 :     data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cneg);
     243             : 
     244             :     stack_elem ec(cond_and, cond_or,
     245          14 :       utilities::detail::set_union(ec_left.FV, ec_right.FV));
     246          14 :     merge_conditions(ec_left, false, ec_right, false, ec, true);
     247          14 :     push(ec);
     248          14 :   }
     249             : 
     250          15 :   void leave(const or_&)
     251             :   {
     252          15 :     stack_elem ec_right = pop();
     253          15 :     stack_elem ec_left = pop();
     254          15 :     data::data_expression cond_and;
     255          15 :     data::data_expression cond_or;
     256             : 
     257          15 :     data::optimized_and(cond_and, ec_left.Cneg, ec_right.Cneg);
     258          15 :     data::optimized_or(cond_or, ec_left.Cpos, ec_right.Cpos);
     259             : 
     260             :     stack_elem ec(cond_or, cond_and,
     261          15 :       utilities::detail::set_union(ec_left.FV, ec_right.FV));
     262          15 :     merge_conditions(ec_left, true, ec_right, true, ec, false);
     263          15 :     push(ec);
     264          15 :   }
     265             : 
     266           0 :   void leave(const imp&)
     267             :   {
     268           0 :     stack_elem ec_right = pop();
     269           0 :     stack_elem ec_left = pop();
     270           0 :     data::data_expression cond_or;
     271           0 :     data::data_expression cond_and;
     272             : 
     273           0 :     data::optimized_or(cond_or, ec_left.Cneg, ec_right.Cpos);
     274           0 :     data::optimized_and(cond_and, ec_left.Cpos, ec_right.Cneg);
     275             : 
     276             :     stack_elem ec(cond_or, cond_and,
     277           0 :       utilities::detail::set_union(ec_left.FV, ec_right.FV));;
     278           0 :     merge_conditions(ec_left, false, ec_right, true, ec, false);
     279           0 :     push(ec);
     280           0 :   }
     281             : 
     282           4 :   void leave(const forall& x)
     283             :   {
     284             :     // build conditions and free variable sets
     285           4 :     stack_elem ec = pop();
     286           8 :     for (auto& [X_e, details]: ec.edges)
     287             :     {
     288           4 :       auto& [cond_set, conj_FV, disj_FV] = details;
     289             : 
     290             :       // Update the conditions
     291           4 :       std::set<data::data_expression> new_conditions;
     292          11 :       for(const data::data_expression& e: cond_set)
     293             :       {        
     294           7 :         data::data_expression t;
     295           7 :         data::optimized_exists(t, x.variables(), e, true);
     296           7 :         new_conditions.insert(t);
     297           7 :       }
     298           4 :       cond_set = std::move(new_conditions);
     299           4 :       data::data_expression forall;
     300           4 :       data::optimized_forall(forall, x.variables(), ec.Cpos, true);
     301             : 
     302           4 :       cond_set.insert(forall);
     303             : 
     304             :       // Update FV
     305           4 :       conj_FV = ec.FV;
     306           4 :     }
     307           4 :     data::optimized_forall(ec.Cpos, x.variables(), ec.Cpos, true);
     308           4 :     data::optimized_exists(ec.Cneg, x.variables(), ec.Cneg, true);
     309           4 :     std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
     310           4 :     ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
     311           4 :     push(ec);
     312             : 
     313             :     // maintain quantifier scope
     314           4 :     if(!quantified_context.empty() && quantified_context.back() == x)
     315             :     {
     316           1 :       quantified_context.pop_back();
     317             :     }
     318           4 :   }
     319             : 
     320           2 :   void leave(const exists& x)
     321             :   {
     322             :     // build conditions and free variable sets
     323           2 :     stack_elem ec = pop();
     324           4 :     for (auto& [X_e, details]: ec.edges)
     325             :     {
     326           2 :       auto& [cond_set, conj_FV, disj_FV] = details;
     327             : 
     328             :       // Update the conditions
     329           2 :       std::set<data::data_expression> new_conditions;
     330           6 :       for(const data::data_expression& e: cond_set)
     331             :       {
     332           4 :         data::data_expression t;
     333           4 :         data::optimized_exists(t, x.variables(), e, true);
     334           4 :         new_conditions.insert(t);
     335           4 :       }
     336           2 :       cond_set = std::move(new_conditions);
     337             : 
     338           2 :       data::data_expression forall;
     339           2 :       data::optimized_forall(forall, x.variables(), ec.Cneg, true);
     340           2 :       cond_set.insert(forall);
     341             : 
     342             :       // Update FV
     343           2 :       disj_FV = ec.FV;
     344           2 :     }
     345           2 :     data::optimized_exists(ec.Cpos, x.variables(), ec.Cpos, true);
     346           2 :     data::optimized_forall(ec.Cneg, x.variables(), ec.Cneg, true);
     347           2 :     std::set<data::variable> bound_vars{x.variables().begin(), x.variables().end()};
     348           2 :     ec.FV = utilities::detail::set_difference(ec.FV, bound_vars);
     349           2 :     push(ec);
     350             : 
     351             :     // maintain quantifier scope
     352           2 :     if(!quantified_context.empty() && quantified_context.back() == x)
     353             :     {
     354           0 :       quantified_context.pop_back();
     355             :     }
     356           2 :   }
     357             : 
     358          39 :   void leave(const propositional_variable_instantiation& x)
     359             :   {
     360             :     // Build list of qvars from quantifier scope
     361          39 :     qvar_list qvars;
     362          40 :     for(const pbes_expression& expr: quantified_context)
     363             :     {
     364           1 :       assert(is_forall(expr) || is_exists(expr));
     365           1 :       data::variable_list vars(is_forall(expr) ? atermpp::down_cast<forall>(expr).variables() : atermpp::down_cast<exists>(expr).variables());
     366           2 :       for(const data::variable& v: vars)
     367             :       {
     368           1 :         qvars.emplace_back(is_forall(expr), v);
     369             :       }
     370           1 :     }
     371          39 :     QPVI Q_X_e{qvars, x};
     372             : 
     373             :     // Store the QPVI and the condition true
     374          39 :     stack_elem ec(data::sort_bool::true_(), data::sort_bool::true_(), data::find_free_variables(x.parameters()));
     375          39 :     ec.edges.insert(std::make_pair(Q_X_e,
     376         117 :       edge_details{std::set<data::data_expression>{data::sort_bool::true_()},
     377             :         std::set<data::variable>{}, std::set<data::variable>{}}));
     378          39 :     push(ec);
     379          39 :   }
     380             : 
     381          29 :   const edge_map& result() const
     382             :   {
     383          29 :     assert(condition_fv_stack.size() == 1);
     384          29 :     return top().edges;
     385             :   }
     386             : };
     387             : 
     388             : } // namespace detail
     389             : /// \endcond
     390             : 
     391             : 
     392             : /// \brief Algorithm class for the constelm algorithm
     393             : template <typename DataRewriter, typename PbesRewriter>
     394             : class pbes_constelm_algorithm
     395             : {
     396             :   protected:
     397             :     /// \brief A map with constraints on the vertices of the graph
     398             :     typedef std::map<data::variable, data::data_expression> constraint_map;
     399             :     typedef std::list<detail::quantified_variable> qvar_list;
     400             : 
     401             :     /// \brief Compares data expressions for equality.
     402             :     const DataRewriter& m_data_rewriter;
     403             : 
     404             :     /// \brief Compares data expressions for equality.
     405             :     const PbesRewriter& m_pbes_rewriter;
     406             : 
     407             :     /// \brief Represents an edge of the dependency graph. The assignments are stored
     408             :     /// implicitly using the 'right' parameter. The condition determines under
     409             :     /// what circumstances the influence of the edge is propagated to its target
     410             :     /// vertex.
     411             :     //
     412             :     // N.B. The attribute condition "pbes_expression condition;" needs to be protected.
     413             :     // This is achieved by deriving from pbes_expression. This is very ugly, but AFAIK
     414             :     // this is the least destructive solution to garbage collection problems.
     415             :     // Note that source and target are protected elsewhere.
     416             :     class edge: public data::data_expression
     417             :     {
     418             :       protected:
     419             :         /// \brief The propositional variable at the source of the edge
     420             :         const propositional_variable m_source;
     421             : 
     422             :         /// \brief The quantifiers in whose direct context the target PVI occurs
     423             :         const qvar_list m_qvars;
     424             : 
     425             :         /// \brief The propositional variable instantiation that determines the target of the edge
     426             :         const propositional_variable_instantiation m_target;
     427             : 
     428             :         const std::set<data::variable> m_conj_context;
     429             :         const std::set<data::variable> m_disj_context;
     430             : 
     431             :       public:
     432             :         /// \brief Constructor
     433             :         edge() = default;
     434             : 
     435             :         /// \brief Constructor
     436             :         /// \param src A propositional variable declaration
     437             :         /// \param tgt A propositional variable
     438             :         /// \param c A term
     439          39 :         edge(
     440             :           const propositional_variable& src,
     441             :           const qvar_list& qvars,
     442             :           const propositional_variable_instantiation& tgt,
     443             :           const std::set<data::variable>& conj_context,
     444             :           const std::set<data::variable>& disj_context,
     445             :           data::data_expression c = data::sort_bool::true_()
     446             :         )
     447             :         : data::data_expression(c)
     448          39 :         , m_source(src)
     449          39 :         , m_qvars(qvars)
     450          39 :         , m_target(tgt)
     451          39 :         , m_conj_context(conj_context)
     452          78 :         , m_disj_context(disj_context)
     453          39 :         {}
     454             : 
     455             :         /// \brief Returns a string representation of the edge.
     456             :         /// \return A string representation of the edge.
     457           0 :         std::string to_string() const
     458             :         {
     459           0 :           std::ostringstream out;
     460           0 :           out << "(" << m_source.name() << ", " << m_target.name() << ")  label = ";
     461           0 :           for(const detail::quantified_variable& qv: m_qvars)
     462             :           {
     463           0 :             out << qv.to_string();
     464             :           }
     465           0 :           out << m_target << "  condition = " << condition();
     466           0 :           return out.str();
     467           0 :         }
     468             : 
     469             :         /// \brief The propositional variable at the source of the edge
     470             :         const propositional_variable& source() const
     471             :         {
     472             :           return m_source;
     473             :         }
     474             : 
     475          55 :         const qvar_list& quantified_variables() const
     476             :         {
     477          55 :           return m_qvars;
     478             :         }
     479             : 
     480             :         /// \brief The propositional variable instantiation that determines the target of the edge
     481         114 :         const propositional_variable_instantiation& target() const
     482             :         {
     483         114 :           return m_target;
     484             :         }
     485             : 
     486             :         /// \brief The condition of the edge
     487          59 :         const data::data_expression& condition() const
     488             :         {
     489          59 :           return *this;
     490             :         }
     491             : 
     492             :         /// \brief Try to guess which quantifiers of Q can end up directly
     493             :         /// before target, when the quantifier inside rewriter is applied.
     494          55 :         qvar_list quantifier_inside_approximation(const qvar_list& Q) const
     495             :         {
     496          55 :           qvar_list result;
     497          55 :           for (auto it = Q.crbegin(); it != Q.crend(); ++it)
     498             :           {
     499             :             // Variable of a universal quantifier cannot occur in the disjunctive context
     500             :             // Variable of an existential quantifier cannot occur in the conjunctive context
     501           0 :             if (( it->is_forall() && m_disj_context.find(it->variable()) == m_disj_context.end()) ||
     502           0 :                 (!it->is_forall() && m_conj_context.find(it->variable()) == m_conj_context.end()))
     503             :             {
     504           0 :               result.push_front(*it);
     505             :             }
     506             :             else
     507             :             {
     508           0 :               break;
     509             :             }
     510             :           }
     511          55 :           return result;
     512           0 :         }
     513             :     };
     514             : 
     515             :     /// \brief Represents a vertex of the dependency graph.
     516             :     class vertex
     517             :     {
     518             :       protected:
     519             :         /// \brief The propositional variable that corresponds to the vertex
     520             :         propositional_variable m_variable;
     521             : 
     522             :         /// \brief The list of quantified variables that occur in the constraints
     523             :         qvar_list m_qvars;
     524             : 
     525             :         /// \brief Maps data variables to data expressions. If a parameter is not
     526             :         // present in this map, it means that it represents NaC ("not a constant").
     527             :         constraint_map m_constraints;
     528             : 
     529             :         /// \brief Indicates whether this vertex has been visited at least once.
     530             :         bool m_visited = false;
     531             : 
     532             :         /// \brief Returns true if the parameter v has been assigned a constant expression.
     533             :         /// \param v A parameter of this->variable()
     534             :         /// \return True if the data parameter v has been assigned a constant expression.
     535          26 :         bool is_constant(const data::variable& v) const
     536             :         {
     537          26 :           auto i = m_constraints.find(v);
     538          26 :           return i != m_constraints.end();
     539             :         }
     540             : 
     541             :         /// \brief Returns true iff all free variables in e are bound in qvars
     542          71 :         bool bound_in_quantifiers(const qvar_list& qvars, const data::data_expression& e)
     543             :         {
     544          71 :           std::set<data::variable> free_vars = data::find_free_variables(e);
     545          71 :           return std::all_of(free_vars.begin(), free_vars.end(), [&](const data::variable& v)
     546             :             {
     547           0 :               return std::find_if(qvars.begin(), qvars.end(), [&](const detail::quantified_variable& qvar){ return qvar.variable() == v; }) != qvars.end();
     548         142 :             });
     549          71 :         }
     550             : 
     551             :         /// \brief Weaken the constraints so they satisfy
     552             :         /// - vars(m_constraints[d]) subset vars(m_qvars); and
     553             :         /// - vars(deleted_constraints) intersection vars(m_qvars) = {}
     554          73 :         void fix_constraints(std::vector<data::data_expression> deleted_constraints)
     555             :         {
     556         103 :           while (!deleted_constraints.empty())
     557             :           {
     558          15 :             std::set<data::variable> vars_deleted;
     559          55 :             for (const data::data_expression& fi: deleted_constraints)
     560             :             {
     561          40 :               data::find_free_variables(fi, std::inserter(vars_deleted, vars_deleted.end()));
     562             :             }
     563          15 :             deleted_constraints.clear();
     564             : 
     565          15 :             auto del_i = std::find_if(m_qvars.rbegin(), m_qvars.rend(), [&](const detail::quantified_variable& qv)
     566             :             {
     567           0 :               return vars_deleted.find(qv.variable()) != vars_deleted.end();
     568             :             });
     569             :             // Remove quantified variables up to and including del_i
     570          15 :             m_qvars.erase(m_qvars.begin(), del_i.base());
     571             : 
     572          58 :             for (const data::variable& par: m_variable.parameters())
     573             :             {
     574          28 :               auto k = m_constraints.find(par);
     575          28 :               if(k == m_constraints.end())
     576             :               {
     577          20 :                 continue;
     578             :               }
     579           8 :               if(!bound_in_quantifiers(m_qvars, k->second))
     580             :               {
     581           0 :                 deleted_constraints.push_back(k->second);
     582           0 :                 m_constraints.erase(k);
     583             :               }
     584             :             }
     585             :           }
     586          73 :         }
     587             : 
     588             :       public:
     589             :         /// \brief Constructor
     590          29 :         vertex() = default;
     591             : 
     592             :         /// \brief Constructor
     593             :         /// \param x A propositional variable declaration
     594          29 :         vertex(propositional_variable x)
     595          29 :           : m_variable(x)
     596          29 :         {}
     597             : 
     598             :         /// \brief The propositional variable that corresponds to the vertex
     599          43 :         const propositional_variable& variable() const
     600             :         {
     601          43 :           return m_variable;
     602             :         }
     603             : 
     604          81 :         const qvar_list& quantified_variables() const
     605             :         {
     606          81 :           return m_qvars;
     607             :         }
     608             : 
     609             :         /// \brief Maps data variables to data expressions. If the right hand side is a data
     610             :         /// variable, it means that it represents NaC ("not a constant").
     611         185 :         const constraint_map& constraints() const
     612             :         {
     613         185 :           return m_constraints;
     614             :         }
     615             : 
     616             :         /// \brief Returns the indices of the constant parameters of this vertex.
     617             :         /// \return The indices of the constant parameters of this vertex.
     618          13 :         std::vector<std::size_t> constant_parameter_indices() const
     619             :         {
     620          13 :           std::vector<std::size_t> result;
     621          13 :           std::size_t index = 0;
     622          52 :           for (const data::variable& parameter: m_variable.parameters())
     623             :           {
     624          26 :             if (is_constant(parameter))
     625             :             {
     626          19 :               result.push_back(index);
     627             :             }
     628          26 :             index++;
     629             :           }
     630          26 :           return result;
     631           0 :         }
     632             : 
     633             :         /// \brief Returns a string representation of the vertex.
     634             :         /// \return A string representation of the vertex.
     635           0 :         std::string to_string() const
     636             :         {
     637           0 :           std::ostringstream out;
     638           0 :           out << m_variable << "  assertions = ";
     639           0 :           for(const detail::quantified_variable& v: quantified_variables())
     640             :           {
     641           0 :             out << v.to_string();
     642             :           }
     643           0 :           for (const auto& constraint: m_constraints)
     644             :           {
     645           0 :             out << "{" << constraint.first << " := " << constraint.second << "} ";
     646             :           }
     647           0 :           return out.str();
     648           0 :         }
     649             : 
     650             :         /// \brief Assign new values to the parameters of this vertex, and update the constraints accordingly.
     651             :         /// The new values have a number of constraints.
     652          73 :         bool update(const qvar_list& qvars, const data::data_expression_list& e, const constraint_map& e_constraints, const DataRewriter& datar)
     653             :         {
     654          73 :           bool changed = false;
     655             : 
     656          73 :           data::variable_list params = m_variable.parameters();
     657          73 :           data::rewriter::substitution_type sigma;
     658          73 :           detail::make_constelm_substitution(e_constraints, sigma);
     659             : 
     660          73 :           if (!m_visited)
     661             :           {
     662          28 :             m_visited = true;
     663          28 :             changed = true;
     664             : 
     665          28 :             m_qvars = qvars;
     666             :             // Partition expressions in e based on whether their free variables
     667             :             // are bound in m_qvars.
     668          28 :             std::vector<data::data_expression> deleted_constraints;
     669          28 :             auto par = params.begin();
     670          67 :             for (auto i = e.begin(); i != e.end(); ++i, ++par)
     671             :             {
     672          39 :               data::data_expression e1 = datar(*i, sigma);
     673          39 :               if (bound_in_quantifiers(m_qvars, e1))
     674             :               {
     675          39 :                 m_constraints[*par] = e1;
     676             :               }
     677             :               else
     678             :               {
     679           0 :                 deleted_constraints.push_back(e1);
     680             :               }
     681             :             }
     682          28 :             fix_constraints(deleted_constraints);
     683          28 :           }
     684             :           else
     685             :           {
     686             :             // Find longest common suffix of qvars
     687          45 :             auto mismatch_it = std::mismatch(m_qvars.rbegin(), m_qvars.rend(), qvars.rbegin(), qvars.rend()).first;
     688          45 :             changed |= mismatch_it != m_qvars.rend();
     689             :             // Remove the outer quantifiers, up to and including mismatch_it
     690          45 :             m_qvars.erase(m_qvars.begin(), mismatch_it.base());
     691             : 
     692             :             // Find constraints for which f[i] = e[i] and for which all free
     693             :             // variables are bound in m_qvars (which may have changed).
     694          45 :             std::vector<data::data_expression> deleted_constraints;
     695          45 :             auto i = e.begin();
     696         159 :             for (auto par = params.begin(); i != e.end(); ++i, ++par)
     697             :             {
     698          70 :               auto k = m_constraints.find(*par);
     699          70 :               if(k == m_constraints.end())
     700             :               {
     701          26 :                 continue;
     702             :               }
     703          44 :               const data::data_expression& fi = k->second;
     704          44 :               data::data_expression ei = datar(*i, sigma);
     705          44 :               if (fi != ei || !bound_in_quantifiers(m_qvars, fi))
     706             :               {
     707          20 :                 changed = true;
     708          20 :                 deleted_constraints.push_back(fi);
     709          20 :                 deleted_constraints.push_back(ei);
     710          20 :                 m_constraints.erase(k);
     711             :               }
     712             :             }
     713          45 :             fix_constraints(deleted_constraints);
     714          45 :           }
     715          73 :           return changed;
     716          73 :         }
     717             :     };
     718             : 
     719             :     /// \brief The storage type for vertices
     720             :     typedef std::map<core::identifier_string, vertex> vertex_map;
     721             : 
     722             :     /// \brief The storage type for edges
     723             :     typedef std::map<core::identifier_string, std::vector<edge> > edge_map;
     724             : 
     725             :     /// \brief The vertices of the dependency graph. They are stored in a map, to
     726             :     /// support searching for a vertex.
     727             :     vertex_map m_vertices;
     728             : 
     729             :     /// \brief The edges of the dependency graph. They are stored in a map, to
     730             :     /// easily access all out-edges corresponding to a particular vertex.
     731             :     edge_map m_edges;
     732             : 
     733             :     /// \brief The redundant parameters.
     734             :     std::map<core::identifier_string, std::vector<std::size_t> > m_redundant_parameters;
     735             : 
     736             :     /// \brief Logs the vertices of the dependency graph.
     737           0 :     std::string print_vertices() const
     738             :     {
     739           0 :       std::ostringstream out;
     740           0 :       for (const auto& v: m_vertices)
     741             :       {
     742           0 :         out << v.second.to_string() << std::endl;
     743             :       }
     744           0 :       return out.str();
     745           0 :     }
     746             : 
     747             :     /// \brief Logs the edges of the dependency graph.
     748           0 :     std::string print_edges()
     749             :     {
     750           0 :       std::ostringstream out;
     751           0 :       for (const auto& source: m_edges)
     752             :       {
     753           0 :         for (const auto& e: source.second)
     754             :         {
     755           0 :           out << e.to_string() << std::endl;
     756             :         }
     757             :       }
     758           0 :       return out.str();
     759           0 :     }
     760             : 
     761           0 :     std::string print_todo_list(const std::deque<propositional_variable>& todo)
     762             :     {
     763           0 :       std::ostringstream out;
     764           0 :       out << "\n<todo list> [";
     765           0 :       for (auto i = todo.begin(); i != todo.end(); ++i)
     766             :       {
     767           0 :         if (i != todo.begin())
     768             :         {
     769           0 :           out << ", ";
     770             :         }
     771           0 :         out << core::pp(i->name());
     772             :       }
     773           0 :       out << "]" << std::endl;
     774           0 :       return out.str();
     775           0 :     }
     776             : 
     777           0 :     std::string print_edge_update(const edge& e, const vertex& u, const vertex& v)
     778             :     {
     779           0 :       std::ostringstream out;
     780           0 :       out << "\n<updating edge> " << e.to_string() << std::endl;
     781           0 :       out << "  <source vertex       > " << u.to_string() << std::endl;
     782           0 :       out << "  <target vertex before> " << v.to_string() << std::endl;
     783           0 :       return out.str();
     784           0 :     }
     785             : 
     786           0 :     std::string print_condition(const edge& e, const vertex& u, const pbes_expression& value)
     787             :     {
     788           0 :       std::ostringstream out;
     789           0 :       data::rewriter::substitution_type sigma;
     790           0 :       detail::make_constelm_substitution(u.constraints(), sigma);
     791           0 :       out << "  <condition           > " << e.condition() << sigma << " to " << value << std::endl;
     792           0 :       return out.str();
     793           0 :     }
     794             : 
     795           0 :     std::string print_evaluation_failure(const edge& e, const vertex& u)
     796             :     {
     797           0 :       std::ostringstream out;
     798           0 :       data::rewriter::substitution_type sigma;
     799           0 :       detail::make_constelm_substitution(u.constraints(), sigma);
     800           0 :       out << "\nCould not evaluate condition " << e.condition() << sigma << " to true or false";
     801           0 :       return out.str();
     802           0 :     }
     803             : 
     804             :     template <typename E>
     805          55 :     std::list<E> concat(const std::list<E> a, const std::list<E> b)
     806             :     {
     807          55 :       std::list<E> result(a);
     808          55 :       result.insert(result.end(), b.begin(), b.end());
     809          55 :       return result;
     810           0 :     }
     811             : 
     812             :   public:
     813             : 
     814             :     /// \brief Constructor.
     815             :     /// \param datar A data rewriter
     816             :     /// \param pbesr A PBES rewriter
     817          18 :     pbes_constelm_algorithm(const DataRewriter& datar, const PbesRewriter& pbesr)
     818          18 :       : m_data_rewriter(datar), m_pbes_rewriter(pbesr)
     819          18 :     {}
     820             : 
     821             :     /// \brief Returns the parameters that have been removed by the constelm algorithm
     822             :     /// \return The removed parameters
     823           0 :     std::map<propositional_variable, std::vector<data::variable> > redundant_parameters() const
     824             :     {
     825           0 :       std::map<propositional_variable, std::vector<data::variable> > result;
     826           0 :       for (const std::pair<const core::identifier_string, std::vector<std::size_t>>& red_pair: m_redundant_parameters)
     827             :       {
     828           0 :         const vertex& v = m_vertices.find(red_pair.first)->second;
     829           0 :         std::vector<data::variable>& variables = result[v.variable()];
     830           0 :         for (const std::size_t par: red_pair.second)
     831             :         {
     832           0 :           typename data::variable_list::iterator k = v.variable().parameters().begin();
     833           0 :           std::advance(k, par);
     834           0 :           variables.push_back(*k);
     835             :         }
     836             :       }
     837           0 :       return result;
     838           0 :     }
     839             : 
     840             :     /// \brief Runs the constelm algorithm
     841             :     /// \param p A pbes
     842             :     /// \param compute_conditions If true, propagation conditions are computed. Note
     843             :     /// that the currently implementation has exponential behavior.
     844          18 :     void run(pbes& p, bool compute_conditions = false, bool check_quantifiers = true)
     845             :     {
     846          18 :       m_vertices.clear();
     847          18 :       m_edges.clear();
     848          18 :       m_redundant_parameters.clear();
     849             : 
     850             :       // compute the vertices and edges of the dependency graph
     851          47 :       for (pbes_equation& eqn: p.equations())
     852             :       {
     853          29 :         core::identifier_string name = eqn.variable().name();
     854          29 :         m_vertices[name] = vertex(eqn.variable());
     855             : 
     856             :         // use an edge_condition_traverser to compute the edges
     857          29 :         detail::edge_condition_traverser f;
     858          29 :         f.apply(eqn.formula());
     859             : 
     860          29 :         std::vector<edge>& edges = m_edges[name];
     861          68 :         for (const auto& [Q_X_e, details]: f.result())
     862             :         {
     863          39 :           const auto& [Q, X_e] = Q_X_e;
     864          39 :           const auto& [conditions, conj_FV, disj_FV] = details;
     865             : 
     866             :           // check options for quantifiers and conditions.
     867          39 :           qvar_list quantifier_list = check_quantifiers ? Q : qvar_list();
     868          39 :           data::data_expression condition = compute_conditions
     869             :             ? data::lazy::join_and(conditions.begin(), conditions.end())
     870          28 :             : data::data_expression(data::sort_bool::true_());
     871             : 
     872          39 :           edges.emplace_back(eqn.variable(), quantifier_list, X_e, conj_FV, disj_FV, condition);
     873             :         }
     874             :       }
     875             : 
     876             :       // initialize the todo list of vertices that need to be processed
     877          18 :       propositional_variable_instantiation init = p.initial_state();
     878          18 :       std::deque<propositional_variable> todo;
     879          18 :       const data::data_expression_list& e_init = init.parameters();
     880          18 :       vertex& u_init = m_vertices[init.name()];
     881          18 :       u_init.update(qvar_list(), e_init, constraint_map(), m_data_rewriter);
     882          18 :       todo.push_back(u_init.variable());
     883             : 
     884          18 :       mCRL2log(log::debug) << "\n--- initial vertices ---\n" << print_vertices();
     885          18 :       mCRL2log(log::debug) << "\n--- edges ---\n" << print_edges();
     886             : 
     887             :       // propagate constraints over the edges until the todo list is empty
     888         100 :       while (!todo.empty())
     889             :       {
     890          41 :         mCRL2log(log::debug) << print_todo_list(todo);
     891          41 :         propositional_variable var = todo.front();
     892             : 
     893             :         // remove all occurrences of var from todo
     894          41 :         todo.erase(std::remove(todo.begin(), todo.end(), var), todo.end());
     895             : 
     896          41 :         const vertex& u = m_vertices[var.name()];
     897          41 :         const std::vector<edge>& u_edges = m_edges[var.name()];
     898             : 
     899         100 :         for (const edge& e: u_edges)
     900             :         {
     901          59 :           vertex& v = m_vertices[e.target().name()];
     902          59 :           mCRL2log(log::debug) << print_edge_update(e, u, v);
     903             : 
     904          59 :           data::rewriter::substitution_type sigma;
     905          59 :           detail::make_constelm_substitution(u.constraints(), sigma);
     906          59 :           pbes_expression needs_update = m_pbes_rewriter(e.condition(), sigma);
     907          59 :           mCRL2log(log::debug) << print_condition(e, u, needs_update);
     908             : 
     909          59 :           if (!is_false(needs_update) && !is_true(needs_update))
     910             :           {
     911           4 :             mCRL2log(log::debug) << print_evaluation_failure(e, u);
     912             :           }
     913          59 :           if (!is_false(needs_update))
     914             :           {
     915         165 :             bool changed = v.update(
     916          55 :                               concat(e.quantifier_inside_approximation(u.quantified_variables()), e.quantified_variables()),
     917          55 :                               e.target().parameters(),
     918             :                               u.constraints(),
     919             :                               m_data_rewriter);
     920          55 :             if (changed)
     921             :             {
     922          25 :               todo.push_back(v.variable());
     923             :             }
     924             :           }
     925          59 :           mCRL2log(log::debug) << "  <target vertex after > " << v.to_string() << "\n";
     926             :         }
     927             :       }
     928             : 
     929          18 :       mCRL2log(log::debug) << "\n--- final vertices ---\n" << print_vertices();
     930             : 
     931             :       // compute the redundant parameters and the redundant equations
     932          47 :       for (const pbes_equation& eqn: p.equations())
     933             :       {
     934          29 :         core::identifier_string name = eqn.variable().name();
     935          29 :         const vertex& v = m_vertices[name];
     936          29 :         if (!v.constraints().empty())
     937             :         {
     938          13 :           std::vector<std::size_t> r = v.constant_parameter_indices();
     939          13 :           if (!r.empty())
     940             :           {
     941          13 :             m_redundant_parameters[name] = r;
     942             :           }
     943          13 :         }
     944             :       }
     945             : 
     946             :       // Apply the constraints to the equations.
     947          47 :       for (pbes_equation& eqn: p.equations())
     948             :       {
     949          29 :         core::identifier_string name = eqn.variable().name();
     950          29 :         const vertex& v = m_vertices[name];
     951             : 
     952          29 :         if (!v.constraints().empty())
     953             :         {
     954          13 :           data::rewriter::substitution_type sigma;
     955          13 :           detail::make_constelm_substitution(v.constraints(), sigma);
     956          13 :           pbes_expression body = pbes_system::replace_free_variables(eqn.formula(), sigma);
     957          13 :           for (auto i = v.quantified_variables().crbegin(); i != v.quantified_variables().crend(); ++i)
     958             :           {
     959           0 :             body = i->make_expr(body);
     960             :           }
     961          13 :           eqn = pbes_equation(
     962          13 :                    eqn.symbol(),
     963          13 :                    eqn.variable(),
     964             :                    body
     965             :                  );
     966          13 :         }
     967             :       }
     968             : 
     969             :       // remove the redundant parameters
     970          18 :       pbes_system::algorithms::remove_parameters(p, m_redundant_parameters);
     971             : 
     972             :       // print the parameters and equation that are removed
     973          18 :       if (mCRL2logEnabled(log::verbose))
     974             :       {
     975           0 :         mCRL2log(log::verbose) << "\nremoved the following constant parameters:" << std::endl;
     976           0 :         for (const std::pair<const propositional_variable, std::vector<data::variable>>& i: redundant_parameters())
     977             :         {
     978           0 :           for (const data::variable& var: i.second)
     979             :           {
     980           0 :             mCRL2log(log::verbose) << "  (" << mcrl2::core::pp(i.first.name()) << ", " << data::pp(var) << ")" << std::endl;
     981             :           }
     982             :         }
     983             :       }
     984          18 :     }
     985             : };
     986             : 
     987             : /// \brief Apply the constelm algorithm
     988             : /// \param p A PBES to which the algorithm is applied
     989             : /// \param rewrite_strategy A data rewrite strategy
     990             : /// \param rewriter_type A PBES rewriter type
     991             : /// \param compute_conditions If true, conditions for the edges of the dependency graph are used N.B. Very inefficient!
     992             : /// \param remove_redundant_equations If true, unreachable equations will be removed.
     993             : inline
     994           0 : void constelm(pbes& p,
     995             :               data::rewrite_strategy rewrite_strategy,
     996             :               pbes_rewriter_type rewriter_type,
     997             :               bool compute_conditions = false,
     998             :               bool remove_redundant_equations = true,
     999             :               bool check_quantifiers = true
    1000             :              )
    1001             : {
    1002             :   // data rewriter
    1003           0 :   data::rewriter datar(p.data(), rewrite_strategy);
    1004             : 
    1005             :   // pbes rewriter
    1006           0 :   switch (rewriter_type)
    1007             :   {
    1008           0 :     case simplify:
    1009             :     {
    1010             :       typedef simplify_data_rewriter<data::rewriter> pbes_rewriter;
    1011           0 :       pbes_rewriter pbesr(datar);
    1012           0 :       pbes_constelm_algorithm<data::rewriter, pbes_rewriter> algorithm(datar, pbesr);
    1013           0 :       algorithm.run(p, compute_conditions, check_quantifiers);
    1014           0 :       if (remove_redundant_equations)
    1015             :       {
    1016           0 :         std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
    1017           0 :         mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
    1018           0 :       }
    1019           0 :       break;
    1020           0 :     }
    1021           0 :     case quantifier_all:
    1022             :     case quantifier_finite:
    1023             :     {
    1024           0 :       bool enumerate_infinite_sorts = (rewriter_type == quantifier_all);
    1025           0 :       enumerate_quantifiers_rewriter pbesr(datar, p.data(), enumerate_infinite_sorts);
    1026           0 :       pbes_constelm_algorithm<data::rewriter, enumerate_quantifiers_rewriter> algorithm(datar, pbesr);
    1027           0 :       algorithm.run(p, compute_conditions, check_quantifiers);
    1028           0 :       if (remove_redundant_equations)
    1029             :       {
    1030           0 :         std::vector<propositional_variable> V = algorithms::remove_unreachable_variables(p);
    1031           0 :         mCRL2log(log::verbose) << algorithms::print_removed_equations(V);
    1032           0 :       }
    1033           0 :       break;
    1034           0 :     }
    1035           0 :     default:
    1036             :     { }
    1037             :   }
    1038           0 : }
    1039             : 
    1040             : } // namespace pbes_system
    1041             : 
    1042             : } // namespace mcrl2
    1043             : 
    1044             : #endif // MCRL2_PBES_CONSTELM_H

Generated by: LCOV version 1.14