Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of shadow elimination node conversion
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "expr/elim_shadow_converter.h"
      14                 :            : 
      15                 :            : #include "expr/bound_var_manager.h"
      16                 :            : #include "expr/subtype_elim_node_converter.h"
      17                 :            : #include "util/rational.h"
      18                 :            : 
      19                 :            : using namespace cvc5::internal::kind;
      20                 :            : 
      21                 :            : namespace cvc5::internal {
      22                 :            : 
      23                 :     636726 : ElimShadowNodeConverter::ElimShadowNodeConverter(NodeManager* nm, const Node& q)
      24                 :     636726 :     : NodeConverter(nm), d_closure(q)
      25                 :            : {
      26 [ -  + ][ -  + ]:     636726 :   Assert(q.isClosure());
                 [ -  - ]
      27                 :     636726 :   d_vars.insert(d_vars.end(), q[0].begin(), q[0].end());
      28                 :     636726 : }
      29                 :            : 
      30                 :      66435 : ElimShadowNodeConverter::ElimShadowNodeConverter(
      31                 :      66435 :     NodeManager* nm, const Node& n, const std::unordered_set<Node>& vars)
      32                 :      66435 :     : NodeConverter(nm)
      33                 :            : {
      34                 :      66435 :   d_closure = n;
      35                 :      66435 :   d_vars.insert(d_vars.end(), vars.begin(), vars.end());
      36                 :      66435 : }
      37                 :            : 
      38                 :   13163250 : Node ElimShadowNodeConverter::postConvert(Node n)
      39                 :            : {
      40         [ +  + ]:   13163250 :   if (!n.isClosure())
      41                 :            :   {
      42                 :   13012730 :     return n;
      43                 :            :   }
      44                 :     150520 :   std::vector<Node> oldVars;
      45                 :     150520 :   std::vector<Node> newVars;
      46         [ +  + ]:     352580 :   for (size_t i = 0, nvars = n[0].getNumChildren(); i < nvars; i++)
      47                 :            :   {
      48                 :     202060 :     const Node& v = n[0][i];
      49         [ +  + ]:     202060 :     if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end())
      50                 :            :     {
      51                 :        402 :       Node nv = getElimShadowVar(d_closure, n, i);
      52                 :        402 :       oldVars.push_back(v);
      53                 :        402 :       newVars.push_back(nv);
      54                 :        402 :     }
      55                 :     202060 :   }
      56         [ +  + ]:     150520 :   if (!newVars.empty())
      57                 :            :   {
      58                 :            :     return n.substitute(
      59                 :        396 :         oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end());
      60                 :            :   }
      61                 :     150124 :   return n;
      62                 :     150520 : }
      63                 :            : 
      64                 :        408 : Node ElimShadowNodeConverter::getElimShadowVar(const Node& q,
      65                 :            :                                                const Node& n,
      66                 :            :                                                size_t i)
      67                 :            : {
      68                 :        408 :   NodeManager* nm = n.getNodeManager();
      69                 :        408 :   BoundVarManager* bvm = nm->getBoundVarManager();
      70                 :        408 :   Node ii = nm->mkConstInt(Rational(i));
      71                 :        816 :   Node cacheVal = BoundVarManager::getCacheValue(q, n, ii);
      72                 :            :   // must be robust to subtype elimination
      73                 :        408 :   SubtypeElimNodeConverter senc(nm);
      74                 :        408 :   cacheVal = senc.convert(cacheVal);
      75                 :        816 :   return bvm->mkBoundVar(BoundVarId::ELIM_SHADOW, cacheVal, n[0][i].getType());
      76                 :        408 : }
      77                 :            : 
      78                 :     636726 : Node ElimShadowNodeConverter::eliminateShadow(const Node& q)
      79                 :            : {
      80 [ -  + ][ -  + ]:     636726 :   Assert(q.isClosure());
                 [ -  - ]
      81                 :     636726 :   NodeManager* nm = q.getNodeManager();
      82                 :     636726 :   ElimShadowNodeConverter esnc(nm, q);
      83                 :            :   // eliminate shadowing in all children
      84                 :     636726 :   std::vector<Node> children;
      85                 :            :   // drop duplicate variables
      86                 :     636726 :   std::vector<Node> vars;
      87                 :     636726 :   bool childChanged = false;
      88         [ +  + ]:    2084226 :   for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
      89                 :            :   {
      90                 :    1447500 :     const Node& v = q[0][i];
      91         [ +  + ]:    1447500 :     if (std::find(vars.begin(), vars.end(), v) == vars.end())
      92                 :            :     {
      93                 :    1447494 :       vars.push_back(v);
      94                 :            :     }
      95                 :            :     else
      96                 :            :     {
      97                 :            :       // should not eliminate shadowing from lambda, since order of variables
      98                 :            :       // matters.
      99 [ -  + ][ -  + ]:          6 :       Assert(q.getKind() != Kind::LAMBDA);
                 [ -  - ]
     100                 :          6 :       Node vn = getElimShadowVar(q, q, i);
     101                 :          6 :       vars.push_back(vn);
     102                 :          6 :       childChanged = true;
     103                 :          6 :     }
     104                 :    1447500 :   }
     105         [ +  + ]:     636726 :   if (childChanged)
     106                 :            :   {
     107                 :          6 :     children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, vars));
     108                 :            :   }
     109                 :            :   else
     110                 :            :   {
     111                 :     636720 :     children.push_back(q[0]);
     112                 :            :   }
     113         [ +  + ]:    1338594 :   for (size_t i = 1, nchild = q.getNumChildren(); i < nchild; i++)
     114                 :            :   {
     115                 :     701868 :     children.push_back(esnc.convert(q[i]));
     116                 :            :   }
     117                 :    1273452 :   return nm->mkNode(q.getKind(), children);
     118                 :     636726 : }
     119                 :            : 
     120                 :            : }  // namespace cvc5::internal