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 representative set.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/rep_set.h"
      14                 :            : 
      15                 :            : #include <unordered_set>
      16                 :            : 
      17                 :            : #include "theory/type_enumerator.h"
      18                 :            : 
      19                 :            : using namespace std;
      20                 :            : using namespace cvc5::internal::kind;
      21                 :            : 
      22                 :            : namespace cvc5::internal {
      23                 :            : namespace theory {
      24                 :            : 
      25                 :      58349 : void RepSet::clear()
      26                 :            : {
      27                 :      58349 :   d_type_reps.clear();
      28                 :      58349 :   d_type_complete.clear();
      29                 :      58349 :   d_tmap.clear();
      30                 :      58349 :   d_values_to_terms.clear();
      31                 :      58349 : }
      32                 :            : 
      33                 :          0 : bool RepSet::hasRep(TypeNode tn, Node n) const
      34                 :            : {
      35                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
      36                 :          0 :       d_type_reps.find(tn);
      37         [ -  - ]:          0 :   if (it == d_type_reps.end())
      38                 :            :   {
      39                 :          0 :     return false;
      40                 :            :   }
      41                 :            :   else
      42                 :            :   {
      43                 :          0 :     return std::find(it->second.begin(), it->second.end(), n)
      44                 :          0 :            != it->second.end();
      45                 :            :   }
      46                 :            : }
      47                 :            : 
      48                 :     191993 : size_t RepSet::getNumRepresentatives(TypeNode tn) const
      49                 :            : {
      50                 :     191993 :   const std::vector<Node>* reps = getTypeRepsOrNull(tn);
      51         [ +  + ]:     191993 :   return (reps != nullptr) ? reps->size() : 0;
      52                 :            : }
      53                 :            : 
      54                 :       4894 : Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
      55                 :            : {
      56                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
      57                 :       4894 :       d_type_reps.find(tn);
      58 [ -  + ][ -  + ]:       4894 :   Assert(it != d_type_reps.end());
                 [ -  - ]
      59 [ -  + ][ -  + ]:       4894 :   Assert(i < it->second.size());
                 [ -  - ]
      60                 :       9788 :   return it->second[i];
      61                 :            : }
      62                 :            : 
      63                 :     197772 : const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
      64                 :            : {
      65                 :     197772 :   auto it = d_type_reps.find(tn);
      66         [ +  + ]:     197772 :   if (it == d_type_reps.end())
      67                 :            :   {
      68                 :         73 :     return nullptr;
      69                 :            :   }
      70                 :     197699 :   return &(it->second);
      71                 :            : }
      72                 :            : 
      73                 :            : namespace {
      74                 :            : 
      75                 :       2783 : bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
      76                 :            : {
      77         [ +  - ]:       2783 :   if (std::find(cache.begin(), cache.end(), n) == cache.end())
      78                 :            :   {
      79                 :       2783 :     cache.insert(n);
      80         [ +  + ]:       2783 :     if (n.getKind() == Kind::STORE_ALL)
      81                 :            :     {
      82                 :       1224 :       return true;
      83                 :            :     }
      84                 :            :     else
      85                 :            :     {
      86         [ +  + ]:       1559 :       for (unsigned i = 0; i < n.getNumChildren(); i++)
      87                 :            :       {
      88         [ +  - ]:       1555 :         if (containsStoreAll(n[i], cache))
      89                 :            :         {
      90                 :       1555 :           return true;
      91                 :            :         }
      92                 :            :       }
      93                 :            :     }
      94                 :            :   }
      95                 :          4 :   return false;
      96                 :            : }
      97                 :            : 
      98                 :            : }  // namespace
      99                 :            : 
     100                 :    1245203 : void RepSet::add(TypeNode tn, Node n)
     101                 :            : {
     102                 :            :   // for now, do not add array constants FIXME
     103         [ +  + ]:    1245203 :   if (tn.isArray())
     104                 :            :   {
     105                 :       1228 :     std::unordered_set<Node> cache;
     106         [ +  + ]:       1228 :     if (containsStoreAll(n, cache))
     107                 :            :     {
     108                 :       1224 :       return;
     109                 :            :     }
     110         [ +  + ]:       1228 :   }
     111         [ +  - ]:    2487958 :   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn
     112                 :    1243979 :                      << " : " << n << std::endl;
     113 [ -  + ][ -  + ]:    1243979 :   Assert(n.getType() == tn);
                 [ -  - ]
     114                 :    1243979 :   d_tmap[n] = (int)d_type_reps[tn].size();
     115                 :    1243979 :   d_type_reps[tn].push_back(n);
     116                 :            : }
     117                 :            : 
     118                 :          0 : int RepSet::getIndexFor(Node n) const
     119                 :            : {
     120                 :          0 :   std::map<Node, int>::const_iterator it = d_tmap.find(n);
     121         [ -  - ]:          0 :   if (it != d_tmap.end())
     122                 :            :   {
     123                 :          0 :     return it->second;
     124                 :            :   }
     125                 :            :   else
     126                 :            :   {
     127                 :          0 :     return -1;
     128                 :            :   }
     129                 :            : }
     130                 :            : 
     131                 :       2407 : bool RepSet::complete(TypeNode t)
     132                 :            : {
     133                 :       2407 :   std::map<TypeNode, bool>::iterator it = d_type_complete.find(t);
     134         [ +  + ]:       2407 :   if (it == d_type_complete.end())
     135                 :            :   {
     136                 :            :     // remove all previous
     137         [ +  + ]:       1047 :     for (unsigned i = 0; i < d_type_reps[t].size(); i++)
     138                 :            :     {
     139                 :        763 :       d_tmap.erase(d_type_reps[t][i]);
     140                 :            :     }
     141                 :        284 :     d_type_reps[t].clear();
     142                 :            :     // now complete the type
     143                 :        284 :     d_type_complete[t] = true;
     144                 :        284 :     TypeEnumerator te(t);
     145         [ +  + ]:       1118 :     while (!te.isFinished())
     146                 :            :     {
     147                 :        834 :       Node n = *te;
     148                 :        834 :       if (std::find(d_type_reps[t].begin(), d_type_reps[t].end(), n)
     149         [ +  - ]:       1668 :           == d_type_reps[t].end())
     150                 :            :       {
     151                 :        834 :         add(t, n);
     152                 :            :       }
     153                 :        834 :       ++te;
     154                 :        834 :     }
     155         [ +  + ]:       1118 :     for (size_t i = 0; i < d_type_reps[t].size(); i++)
     156                 :            :     {
     157         [ +  - ]:        834 :       Trace("reps-complete") << d_type_reps[t][i] << " ";
     158                 :            :     }
     159         [ +  - ]:        284 :     Trace("reps-complete") << std::endl;
     160                 :        284 :     return true;
     161                 :        284 :   }
     162                 :            :   else
     163                 :            :   {
     164                 :       2123 :     return it->second;
     165                 :            :   }
     166                 :            : }
     167                 :            : 
     168                 :      62068 : Node RepSet::getTermForRepresentative(Node n) const
     169                 :            : {
     170                 :      62068 :   std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
     171         [ +  + ]:      62068 :   if (it != d_values_to_terms.end())
     172                 :            :   {
     173                 :      59825 :     return it->second;
     174                 :            :   }
     175                 :            :   else
     176                 :            :   {
     177                 :       2243 :     return Node::null();
     178                 :            :   }
     179                 :            : }
     180                 :            : 
     181                 :    1238479 : void RepSet::setTermForRepresentative(Node n, Node t)
     182                 :            : {
     183                 :    1238479 :   d_values_to_terms[n] = t;
     184                 :    1238479 : }
     185                 :            : 
     186                 :          0 : Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
     187                 :            : {
     188                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
     189                 :          0 :       d_type_reps.find(tn);
     190         [ -  - ]:          0 :   if (it != d_type_reps.end())
     191                 :            :   {
     192                 :            :     // try to find a pre-existing arbitrary element
     193         [ -  - ]:          0 :     for (size_t i = 0; i < it->second.size(); i++)
     194                 :            :     {
     195                 :          0 :       if (std::find(exclude.begin(), exclude.end(), it->second[i])
     196         [ -  - ]:          0 :           == exclude.end())
     197                 :            :       {
     198                 :          0 :         return it->second[i];
     199                 :            :       }
     200                 :            :     }
     201                 :            :   }
     202                 :          0 :   return Node::null();
     203                 :            : }
     204                 :            : 
     205                 :          0 : void RepSet::toStream(std::ostream& out)
     206                 :            : {
     207                 :          0 :   for (std::map<TypeNode, std::vector<Node> >::iterator it =
     208                 :          0 :            d_type_reps.begin();
     209         [ -  - ]:          0 :        it != d_type_reps.end();
     210                 :          0 :        ++it)
     211                 :            :   {
     212                 :          0 :     if (!it->first.isFunction() && !it->first.isPredicate())
     213                 :            :     {
     214                 :          0 :       out << "(" << it->first << " " << it->second.size();
     215                 :          0 :       out << " (";
     216         [ -  - ]:          0 :       for (unsigned i = 0; i < it->second.size(); i++)
     217                 :            :       {
     218         [ -  - ]:          0 :         if (i > 0)
     219                 :            :         {
     220                 :          0 :           out << " ";
     221                 :            :         }
     222                 :          0 :         out << it->second[i];
     223                 :            :       }
     224                 :          0 :       out << ")";
     225                 :          0 :       out << ")" << std::endl;
     226                 :            :     }
     227                 :            :   }
     228                 :          0 : }
     229                 :            : 
     230                 :            : }  // namespace theory
     231                 :            : }  // namespace cvc5::internal