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                 :            :  * Simple substitution utility.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "expr/subs.h"
      14                 :            : 
      15                 :            : #include <sstream>
      16                 :            : 
      17                 :            : #include "expr/skolem_manager.h"
      18                 :            : 
      19                 :            : namespace cvc5::internal {
      20                 :            : 
      21                 :      79263 : bool Subs::empty() const { return d_vars.empty(); }
      22                 :            : 
      23                 :     105565 : size_t Subs::size() const { return d_vars.size(); }
      24                 :            : 
      25                 :      14866 : bool Subs::contains(Node v) const
      26                 :            : {
      27                 :      14866 :   return std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end();
      28                 :            : }
      29                 :            : 
      30                 :          0 : Node Subs::getSubs(Node v) const
      31                 :            : {
      32                 :            :   std::vector<Node>::const_iterator it =
      33                 :          0 :       std::find(d_vars.begin(), d_vars.end(), v);
      34         [ -  - ]:          0 :   if (it == d_vars.end())
      35                 :            :   {
      36                 :          0 :     return Node::null();
      37                 :            :   }
      38                 :          0 :   size_t i = std::distance(d_vars.begin(), it);
      39                 :          0 :   Assert(i < d_subs.size());
      40                 :          0 :   return d_subs[i];
      41                 :            : }
      42                 :            : 
      43                 :    6248094 : std::optional<Node> Subs::find(TNode v) const
      44                 :            : {
      45                 :    6248094 :   auto it = std::find(d_vars.begin(), d_vars.end(), v);
      46         [ +  + ]:    6248094 :   if (it == d_vars.end())
      47                 :            :   {
      48                 :    4584037 :     return {};
      49                 :            :   }
      50                 :    1664057 :   return d_subs[std::distance(d_vars.begin(), it)];
      51                 :            : }
      52                 :            : 
      53                 :        426 : void Subs::add(Node v)
      54                 :            : {
      55                 :            :   // default, use a fresh skolem of the same type
      56                 :        852 :   Node s = NodeManager::mkDummySkolem("sk", v.getType());
      57                 :        426 :   add(v, s);
      58                 :        426 : }
      59                 :            : 
      60                 :         30 : void Subs::add(const std::vector<Node>& vs)
      61                 :            : {
      62         [ +  + ]:         67 :   for (const Node& v : vs)
      63                 :            :   {
      64                 :         37 :     add(v);
      65                 :            :   }
      66                 :         30 : }
      67                 :            : 
      68                 :    3299177 : void Subs::add(const Node& v, const Node& s)
      69                 :            : {
      70                 :    3299177 :   Assert(s.isNull() || v.getType().isComparableTo(s.getType()));
      71                 :    3299177 :   d_vars.push_back(v);
      72                 :    3299177 :   d_subs.push_back(s);
      73                 :    3299177 : }
      74                 :            : 
      75                 :       4859 : void Subs::add(const std::vector<Node>& vs, const std::vector<Node>& ss)
      76                 :            : {
      77 [ -  + ][ -  + ]:       4859 :   Assert(vs.size() == ss.size());
                 [ -  - ]
      78         [ +  + ]:      11319 :   for (size_t i = 0, nvs = vs.size(); i < nvs; i++)
      79                 :            :   {
      80                 :       6460 :     add(vs[i], ss[i]);
      81                 :            :   }
      82                 :       4859 : }
      83                 :            : 
      84                 :          0 : void Subs::addEquality(Node eq)
      85                 :            : {
      86                 :          0 :   Assert(eq.getKind() == Kind::EQUAL);
      87                 :          0 :   add(eq[0], eq[1]);
      88                 :          0 : }
      89                 :            : 
      90                 :       3481 : void Subs::append(Subs& s)
      91                 :            : {
      92                 :            :   // add the substitution list
      93                 :       3481 :   add(s.d_vars, s.d_subs);
      94                 :       3481 : }
      95                 :            : 
      96                 :      65272 : Node Subs::apply(const Node& n) const
      97                 :            : {
      98         [ +  + ]:      65272 :   if (d_vars.empty())
      99                 :            :   {
     100                 :       6508 :     return n;
     101                 :            :   }
     102                 :            :   Node ns =
     103                 :      58764 :       n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end());
     104                 :      58764 :   return ns;
     105                 :      58764 : }
     106                 :         30 : Node Subs::rapply(Node n) const
     107                 :            : {
     108         [ -  + ]:         30 :   if (d_vars.empty())
     109                 :            :   {
     110                 :          0 :     return n;
     111                 :            :   }
     112                 :            :   Node ns =
     113                 :         30 :       n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end());
     114                 :         30 :   return ns;
     115                 :         30 : }
     116                 :            : 
     117                 :          0 : void Subs::applyToRange(Subs& s) const
     118                 :            : {
     119         [ -  - ]:          0 :   if (d_vars.empty())
     120                 :            :   {
     121                 :          0 :     return;
     122                 :            :   }
     123         [ -  - ]:          0 :   for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
     124                 :            :   {
     125                 :          0 :     s.d_subs[i] = apply(s.d_subs[i]);
     126                 :            :   }
     127                 :            : }
     128                 :            : 
     129                 :          0 : void Subs::rapplyToRange(Subs& s) const
     130                 :            : {
     131         [ -  - ]:          0 :   if (d_vars.empty())
     132                 :            :   {
     133                 :          0 :     return;
     134                 :            :   }
     135         [ -  - ]:          0 :   for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
     136                 :            :   {
     137                 :          0 :     s.d_subs[i] = rapply(s.d_subs[i]);
     138                 :            :   }
     139                 :            : }
     140                 :            : 
     141                 :          0 : Node Subs::getEquality(size_t i) const
     142                 :            : {
     143                 :          0 :   Assert(i < d_vars.size());
     144                 :          0 :   return d_vars[i].eqNode(d_subs[i]);
     145                 :            : }
     146                 :            : 
     147                 :          0 : std::map<Node, Node> Subs::toMap() const
     148                 :            : {
     149                 :          0 :   std::map<Node, Node> ret;
     150         [ -  - ]:          0 :   for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++)
     151                 :            :   {
     152                 :          0 :     ret[d_vars[i]] = d_subs[i];
     153                 :            :   }
     154                 :          0 :   return ret;
     155                 :          0 : }
     156                 :            : 
     157                 :          0 : std::string Subs::toString() const
     158                 :            : {
     159                 :          0 :   std::stringstream ss;
     160                 :          0 :   ss << "[";
     161         [ -  - ]:          0 :   for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++)
     162                 :            :   {
     163         [ -  - ]:          0 :     if (i > 0)
     164                 :            :     {
     165                 :          0 :       ss << " ";
     166                 :            :     }
     167                 :          0 :     ss << d_vars[i] << " -> " << d_subs[i];
     168                 :            :   }
     169                 :          0 :   ss << "]";
     170                 :          0 :   return ss.str();
     171                 :          0 : }
     172                 :            : 
     173                 :     154695 : void Subs::clear()
     174                 :            : {
     175                 :     154695 :   d_vars.clear();
     176                 :     154695 :   d_subs.clear();
     177                 :     154695 : }
     178                 :            : 
     179                 :          0 : std::ostream& operator<<(std::ostream& out, const Subs& s)
     180                 :            : {
     181                 :          0 :   out << s.toString();
     182                 :          0 :   return out;
     183                 :            : }
     184                 :            : 
     185                 :            : }  // namespace cvc5::internal