Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Tim King, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Implementation of representative set.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include <unordered_set>
      17                 :            : 
      18                 :            : #include "theory/rep_set.h"
      19                 :            : #include "theory/type_enumerator.h"
      20                 :            : 
      21                 :            : using namespace std;
      22                 :            : using namespace cvc5::internal::kind;
      23                 :            : 
      24                 :            : namespace cvc5::internal {
      25                 :            : namespace theory {
      26                 :            : 
      27                 :      56914 : void RepSet::clear(){
      28                 :      56914 :   d_type_reps.clear();
      29                 :      56914 :   d_type_complete.clear();
      30                 :      56914 :   d_tmap.clear();
      31                 :      56914 :   d_values_to_terms.clear();
      32                 :      56914 : }
      33                 :            : 
      34                 :          0 : bool RepSet::hasRep(TypeNode tn, Node n) const
      35                 :            : {
      36                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
      37                 :          0 :       d_type_reps.find(tn);
      38         [ -  - ]:          0 :   if( it==d_type_reps.end() ){
      39                 :          0 :     return false;
      40                 :            :   }else{
      41                 :          0 :     return std::find( it->second.begin(), it->second.end(), n )!=it->second.end();
      42                 :            :   }
      43                 :            : }
      44                 :            : 
      45                 :     200136 : size_t RepSet::getNumRepresentatives(TypeNode tn) const
      46                 :            : {
      47                 :     200136 :   const std::vector<Node>* reps = getTypeRepsOrNull(tn);
      48         [ +  + ]:     200136 :   return (reps != nullptr) ? reps->size() : 0;
      49                 :            : }
      50                 :            : 
      51                 :       7487 : Node RepSet::getRepresentative(TypeNode tn, unsigned i) const
      52                 :            : {
      53                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
      54                 :       7487 :       d_type_reps.find(tn);
      55 [ -  + ][ -  + ]:       7487 :   Assert(it != d_type_reps.end());
                 [ -  - ]
      56 [ -  + ][ -  + ]:       7487 :   Assert(i < it->second.size());
                 [ -  - ]
      57                 :      14974 :   return it->second[i];
      58                 :            : }
      59                 :            : 
      60                 :     205090 : const std::vector<Node>* RepSet::getTypeRepsOrNull(TypeNode tn) const
      61                 :            : {
      62                 :     205090 :   auto it = d_type_reps.find(tn);
      63         [ +  + ]:     205090 :   if (it == d_type_reps.end())
      64                 :            :   {
      65                 :        194 :     return nullptr;
      66                 :            :   }
      67                 :     204896 :   return &(it->second);
      68                 :            : }
      69                 :            : 
      70                 :            : namespace {
      71                 :            : 
      72                 :       2817 : bool containsStoreAll(Node n, std::unordered_set<Node>& cache)
      73                 :            : {
      74         [ +  - ]:       2817 :   if( std::find( cache.begin(), cache.end(), n )==cache.end() ){
      75                 :       2817 :     cache.insert(n);
      76         [ +  + ]:       2817 :     if (n.getKind() == Kind::STORE_ALL)
      77                 :            :     {
      78                 :       1222 :       return true;
      79                 :            :     }
      80                 :            :     else
      81                 :            :     {
      82         [ +  + ]:       1595 :       for( unsigned i=0; i<n.getNumChildren(); i++ ){
      83         [ +  - ]:       1591 :         if( containsStoreAll( n[i], cache ) ){
      84                 :       1591 :           return true;
      85                 :            :         }
      86                 :            :       }
      87                 :            :     }
      88                 :            :   }
      89                 :          4 :   return false;
      90                 :            : }
      91                 :            : 
      92                 :            : }  // namespace
      93                 :            : 
      94                 :    1227210 : void RepSet::add( TypeNode tn, Node n ){
      95                 :            :   //for now, do not add array constants FIXME
      96         [ +  + ]:    1227210 :   if( tn.isArray() ){
      97                 :       1226 :     std::unordered_set<Node> cache;
      98         [ +  + ]:       1226 :     if( containsStoreAll( n, cache ) ){
      99                 :       1222 :       return;
     100                 :            :     }
     101                 :            :   }
     102         [ +  - ]:    1225980 :   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
     103 [ -  + ][ -  + ]:    1225980 :   Assert(n.getType() == tn);
                 [ -  - ]
     104                 :    1225980 :   d_tmap[ n ] = (int)d_type_reps[tn].size();
     105                 :    1225980 :   d_type_reps[tn].push_back( n );
     106                 :            : }
     107                 :            : 
     108                 :          0 : int RepSet::getIndexFor( Node n ) const {
     109                 :          0 :   std::map< Node, int >::const_iterator it = d_tmap.find( n );
     110         [ -  - ]:          0 :   if( it!=d_tmap.end() ){
     111                 :          0 :     return it->second;
     112                 :            :   }else{
     113                 :          0 :     return -1;
     114                 :            :   }
     115                 :            : }
     116                 :            : 
     117                 :       2196 : bool RepSet::complete( TypeNode t ){
     118                 :       2196 :   std::map< TypeNode, bool >::iterator it = d_type_complete.find( t );
     119         [ +  + ]:       2196 :   if( it==d_type_complete.end() ){
     120                 :            :     //remove all previous
     121         [ +  + ]:        841 :     for( unsigned i=0; i<d_type_reps[t].size(); i++ ){
     122                 :        620 :       d_tmap.erase( d_type_reps[t][i] );
     123                 :            :     }
     124                 :        221 :     d_type_reps[t].clear();
     125                 :            :     //now complete the type
     126                 :        221 :     d_type_complete[t] = true;
     127                 :        442 :     TypeEnumerator te(t);
     128         [ +  + ]:        911 :     while( !te.isFinished() ){
     129                 :       1380 :       Node n = *te;
     130         [ +  - ]:        690 :       if( std::find( d_type_reps[t].begin(), d_type_reps[t].end(), n )==d_type_reps[t].end() ){
     131                 :        690 :         add( t, n );
     132                 :            :       }
     133                 :        690 :       ++te;
     134                 :            :     }
     135         [ +  + ]:        911 :     for( size_t i=0; i<d_type_reps[t].size(); i++ ){
     136         [ +  - ]:        690 :       Trace("reps-complete") << d_type_reps[t][i] << " ";
     137                 :            :     }
     138         [ +  - ]:        221 :     Trace("reps-complete") << std::endl;
     139                 :        221 :     return true;
     140                 :            :   }else{
     141                 :       1975 :     return it->second;
     142                 :            :   }
     143                 :            : }
     144                 :            : 
     145                 :      62467 : Node RepSet::getTermForRepresentative(Node n) const
     146                 :            : {
     147                 :      62467 :   std::map<Node, Node>::const_iterator it = d_values_to_terms.find(n);
     148         [ +  + ]:      62467 :   if (it != d_values_to_terms.end())
     149                 :            :   {
     150                 :      60055 :     return it->second;
     151                 :            :   }
     152                 :            :   else
     153                 :            :   {
     154                 :       2412 :     return Node::null();
     155                 :            :   }
     156                 :            : }
     157                 :            : 
     158                 :    1224010 : void RepSet::setTermForRepresentative(Node n, Node t)
     159                 :            : {
     160                 :    1224010 :   d_values_to_terms[n] = t;
     161                 :    1224010 : }
     162                 :            : 
     163                 :          0 : Node RepSet::getDomainValue(TypeNode tn, const std::vector<Node>& exclude) const
     164                 :            : {
     165                 :            :   std::map<TypeNode, std::vector<Node> >::const_iterator it =
     166                 :          0 :       d_type_reps.find(tn);
     167         [ -  - ]:          0 :   if (it != d_type_reps.end())
     168                 :            :   {
     169                 :            :     // try to find a pre-existing arbitrary element
     170         [ -  - ]:          0 :     for (size_t i = 0; i < it->second.size(); i++)
     171                 :            :     {
     172                 :          0 :       if (std::find(exclude.begin(), exclude.end(), it->second[i])
     173         [ -  - ]:          0 :           == exclude.end())
     174                 :            :       {
     175                 :          0 :         return it->second[i];
     176                 :            :       }
     177                 :            :     }
     178                 :            :   }
     179                 :          0 :   return Node::null();
     180                 :            : }
     181                 :            : 
     182                 :          0 : void RepSet::toStream(std::ostream& out){
     183         [ -  - ]:          0 :   for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){
     184                 :          0 :     if( !it->first.isFunction() && !it->first.isPredicate() ){
     185                 :          0 :       out << "(" << it->first << " " << it->second.size();
     186                 :          0 :       out << " (";
     187         [ -  - ]:          0 :       for( unsigned i=0; i<it->second.size(); i++ ){
     188         [ -  - ]:          0 :         if( i>0 ){ out << " "; }
     189                 :          0 :         out << it->second[i];
     190                 :            :       }
     191                 :          0 :       out << ")";
     192                 :          0 :       out << ")" << std::endl;
     193                 :            :     }
     194                 :            :   }
     195                 :          0 : }
     196                 :            : 
     197                 :            : }  // namespace theory
     198                 :            : }  // namespace cvc5::internal