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 utilities.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "theory/rep_set_iterator.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                 :       9370 : RepSetIterator::RepSetIterator(const RepSet* rs, RepBoundExt* rext)
      26                 :       9370 :     : d_rs(rs), d_rext(rext), d_incomplete(false)
      27                 :            : {
      28                 :       9370 : }
      29                 :            : 
      30                 :      53313 : size_t RepSetIterator::domainSize(size_t i) const
      31                 :            : {
      32                 :      53313 :   size_t v = d_var_order[i];
      33                 :      53313 :   return d_domain_elements[v].size();
      34                 :            : }
      35                 :            : 
      36                 :     106203 : TypeNode RepSetIterator::getTypeOf(size_t i) const { return d_types[i]; }
      37                 :            : 
      38                 :       9370 : bool RepSetIterator::setQuantifier(Node q)
      39                 :            : {
      40         [ +  - ]:       9370 :   Trace("rsi") << "Make rsi for quantified formula " << q << std::endl;
      41 [ -  + ][ -  + ]:       9370 :   Assert(d_types.empty());
                 [ -  - ]
      42                 :            :   // store indicies
      43         [ +  + ]:      22155 :   for (const Node& v : q[0])
      44                 :            :   {
      45                 :      12785 :     d_types.push_back(v.getType());
      46                 :      22155 :   }
      47                 :       9370 :   d_owner = q;
      48                 :       9370 :   return initialize();
      49                 :            : }
      50                 :            : 
      51                 :          0 : bool RepSetIterator::setFunctionDomain(Node op)
      52                 :            : {
      53         [ -  - ]:          0 :   Trace("rsi") << "Make rsi for function " << op << std::endl;
      54                 :          0 :   Assert(d_types.empty());
      55                 :          0 :   TypeNode tn = op.getType();
      56         [ -  - ]:          0 :   for (size_t i = 0; i < tn.getNumChildren() - 1; i++)
      57                 :            :   {
      58                 :          0 :     d_types.push_back(tn[i]);
      59                 :            :   }
      60                 :          0 :   d_owner = op;
      61                 :          0 :   return initialize();
      62                 :          0 : }
      63                 :            : 
      64                 :       9370 : bool RepSetIterator::initialize()
      65                 :            : {
      66         [ +  - ]:       9370 :   Trace("rsi") << "Initialize rep set iterator..." << std::endl;
      67                 :       9370 :   size_t ntypes = d_types.size();
      68                 :       9370 :   d_var_order.resize(ntypes);
      69         [ +  + ]:      22155 :   for (size_t v = 0; v < ntypes; v++)
      70                 :            :   {
      71                 :      12785 :     d_index.push_back(0);
      72                 :            :     // store default index order
      73                 :      12785 :     d_index_order.push_back(v);
      74                 :      12785 :     d_var_order[v] = v;
      75                 :            :     // store default domain
      76                 :            :     // d_domain.push_back( RepDomain() );
      77                 :      12785 :     d_domain_elements.push_back(std::vector<Node>());
      78                 :      12785 :     TypeNode tn = d_types[v];
      79         [ +  - ]:      12785 :     Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl;
      80                 :      12785 :     bool inc = true;
      81                 :      12785 :     bool setEnum = false;
      82                 :            :     // check if it is externally bound
      83         [ +  - ]:      12785 :     if (d_rext)
      84                 :            :     {
      85                 :      12785 :       inc = !d_rext->initializeRepresentativesForType(tn);
      86                 :      12785 :       RsiEnumType rsiet = d_rext->setBound(d_owner, v, d_domain_elements[v]);
      87         [ +  + ]:      12785 :       if (rsiet != ENUM_INVALID)
      88                 :            :       {
      89                 :       7326 :         d_enum_type.push_back(rsiet);
      90                 :       7326 :         inc = false;
      91                 :       7326 :         setEnum = true;
      92                 :            :       }
      93                 :            :     }
      94         [ -  + ]:      12785 :     if (inc)
      95                 :            :     {
      96         [ -  - ]:          0 :       Trace("fmf-incomplete")
      97                 :          0 :           << "Incomplete because of quantification of type " << tn << std::endl;
      98                 :          0 :       d_incomplete = true;
      99                 :            :     }
     100                 :            : 
     101                 :            :     // if we have yet to determine the type of enumeration
     102         [ +  + ]:      12785 :     if (!setEnum)
     103                 :            :     {
     104         [ +  - ]:       5459 :       if (d_rs->hasType(tn))
     105                 :            :       {
     106                 :       5459 :         d_enum_type.push_back(ENUM_DEFAULT);
     107         [ +  - ]:       5459 :         if (const auto* type_reps = d_rs->getTypeRepsOrNull(tn))
     108                 :            :         {
     109                 :       5459 :           std::vector<Node>& v_domain_elements = d_domain_elements[v];
     110                 :      10918 :           v_domain_elements.insert(
     111                 :      10918 :               v_domain_elements.end(), type_reps->begin(), type_reps->end());
     112                 :            :         }
     113                 :            :       }
     114                 :            :       else
     115                 :            :       {
     116                 :          0 :         Assert(d_incomplete);
     117                 :          0 :         return false;
     118                 :            :       }
     119                 :            :     }
     120         [ +  - ]:      12785 :   }
     121                 :            : 
     122         [ +  - ]:       9370 :   if (d_rext)
     123                 :            :   {
     124                 :       9370 :     std::vector<size_t> varOrder;
     125         [ +  - ]:       9370 :     if (d_rext->getVariableOrder(d_owner, varOrder))
     126                 :            :     {
     127         [ -  + ]:       9370 :       if (TraceIsOn("bound-int-rsi"))
     128                 :            :       {
     129         [ -  - ]:          0 :         Trace("bound-int-rsi") << "Variable order : ";
     130         [ -  - ]:          0 :         for (size_t v : varOrder)
     131                 :            :         {
     132         [ -  - ]:          0 :           Trace("bound-int-rsi") << v << " ";
     133                 :            :         }
     134         [ -  - ]:          0 :         Trace("bound-int-rsi") << std::endl;
     135                 :            :       }
     136                 :       9370 :       size_t nvars = varOrder.size();
     137                 :       9370 :       std::vector<size_t> indexOrder;
     138                 :       9370 :       indexOrder.resize(nvars);
     139         [ +  + ]:      22155 :       for (size_t i = 0; i < nvars; i++)
     140                 :            :       {
     141 [ -  + ][ -  + ]:      12785 :         Assert(varOrder[i] < indexOrder.size());
                 [ -  - ]
     142                 :      12785 :         indexOrder[varOrder[i]] = i;
     143                 :            :       }
     144         [ -  + ]:       9370 :       if (TraceIsOn("bound-int-rsi"))
     145                 :            :       {
     146         [ -  - ]:          0 :         Trace("bound-int-rsi") << "Will use index order : ";
     147         [ -  - ]:          0 :         for (size_t i = 0, isize = indexOrder.size(); i < isize; i++)
     148                 :            :         {
     149         [ -  - ]:          0 :           Trace("bound-int-rsi") << indexOrder[i] << " ";
     150                 :            :         }
     151         [ -  - ]:          0 :         Trace("bound-int-rsi") << std::endl;
     152                 :            :       }
     153                 :       9370 :       setIndexOrder(indexOrder);
     154                 :       9370 :     }
     155                 :       9370 :   }
     156                 :            :   // now reset the indices
     157                 :       9370 :   doResetIncrement(-1, true);
     158                 :       9370 :   return true;
     159                 :            : }
     160                 :            : 
     161                 :       9370 : void RepSetIterator::setIndexOrder(std::vector<size_t>& indexOrder)
     162                 :            : {
     163                 :       9370 :   d_index_order.clear();
     164                 :      18740 :   d_index_order.insert(
     165                 :       9370 :       d_index_order.begin(), indexOrder.begin(), indexOrder.end());
     166                 :            :   // make the d_var_order mapping
     167         [ +  + ]:      22155 :   for (size_t i = 0, isize = d_index_order.size(); i < isize; i++)
     168                 :            :   {
     169                 :      12785 :     d_var_order[d_index_order[i]] = i;
     170                 :            :   }
     171                 :       9370 : }
     172                 :            : 
     173                 :      22891 : int RepSetIterator::resetIndex(size_t i, bool initial)
     174                 :            : {
     175                 :      22891 :   d_index[i] = 0;
     176                 :      22891 :   size_t v = d_var_order[i];
     177         [ +  - ]:      45782 :   Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v
     178                 :      22891 :                          << ", initial = " << initial << std::endl;
     179         [ +  - ]:      22891 :   if (d_rext)
     180                 :            :   {
     181         [ +  + ]:      22891 :     if (!d_rext->resetIndex(this, d_owner, v, initial, d_domain_elements[v]))
     182                 :            :     {
     183                 :        298 :       return -1;
     184                 :            :     }
     185                 :            :   }
     186         [ +  + ]:      22593 :   return d_domain_elements[v].empty() ? 0 : 1;
     187                 :            : }
     188                 :            : 
     189                 :      41305 : int RepSetIterator::incrementAtIndex(int i)
     190                 :            : {
     191 [ -  + ][ -  + ]:      41305 :   Assert(!isFinished());
                 [ -  - ]
     192         [ +  - ]:      41305 :   Trace("rsi-debug") << "RepSetIterator::incrementAtIndex: " << i << std::endl;
     193                 :            :   // increment d_index
     194         [ +  + ]:      41305 :   if (i >= 0)
     195                 :            :   {
     196         [ +  - ]:      82016 :     Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i)
     197                 :      41008 :                        << std::endl;
     198                 :            :   }
     199 [ +  + ][ +  + ]:      62089 :   while (i >= 0 && d_index[i] >= (int)(domainSize(i) - 1))
                 [ +  + ]
     200                 :            :   {
     201                 :      20784 :     i--;
     202         [ +  + ]:      20784 :     if (i >= 0)
     203                 :            :     {
     204         [ +  - ]:      24610 :       Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i)
     205                 :      12305 :                          << std::endl;
     206                 :            :     }
     207                 :            :   }
     208         [ +  + ]:      41305 :   if (i == -1)
     209                 :            :   {
     210         [ +  - ]:       8776 :     Trace("rsi-debug") << "increment failed" << std::endl;
     211                 :       8776 :     d_index.clear();
     212                 :       8776 :     return -1;
     213                 :            :   }
     214                 :            :   else
     215                 :            :   {
     216         [ +  - ]:      32529 :     Trace("rsi-debug") << "increment " << i << std::endl;
     217                 :      32529 :     d_index[i]++;
     218                 :      32529 :     return doResetIncrement(i);
     219                 :            :   }
     220                 :            : }
     221                 :            : 
     222                 :      41899 : int RepSetIterator::doResetIncrement(int i, bool initial)
     223                 :            : {
     224         [ +  - ]:      83798 :   Trace("rsi-debug") << "RepSetIterator::doResetIncrement: " << i
     225                 :      41899 :                      << ", initial=" << initial << std::endl;
     226         [ +  + ]:      64154 :   for (size_t ii = (i + 1); ii < d_index.size(); ii++)
     227                 :            :   {
     228                 :      22891 :     bool emptyDomain = false;
     229                 :      22891 :     int ri_res = resetIndex(ii, initial);
     230         [ +  + ]:      22891 :     if (ri_res == -1)
     231                 :            :     {
     232                 :            :       // failed
     233                 :        298 :       d_index.clear();
     234         [ +  - ]:        596 :       Trace("fmf-incomplete")
     235                 :        298 :           << "Incomplete because of reset index " << ii << std::endl;
     236                 :        298 :       d_incomplete = true;
     237                 :        298 :       break;
     238                 :            :     }
     239         [ +  + ]:      22593 :     else if (ri_res == 0)
     240                 :            :     {
     241                 :        338 :       emptyDomain = true;
     242                 :            :     }
     243                 :            :     // force next iteration if currently an empty domain
     244         [ +  + ]:      22593 :     if (emptyDomain)
     245                 :            :     {
     246         [ +  - ]:        676 :       Trace("rsi-debug") << "This is an empty domain (index " << ii << ")."
     247                 :        338 :                          << std::endl;
     248         [ +  + ]:        338 :       if (ii > 0)
     249                 :            :       {
     250                 :            :         // increment at the previous index
     251                 :        338 :         return incrementAtIndex(ii - 1);
     252                 :            :       }
     253                 :            :       else
     254                 :            :       {
     255                 :            :         // this is the first index, we are done
     256                 :        296 :         d_index.clear();
     257                 :        296 :         return -1;
     258                 :            :       }
     259                 :            :     }
     260                 :            :   }
     261         [ +  - ]:      41561 :   Trace("rsi-debug") << "Finished, return " << i << std::endl;
     262                 :      41561 :   return i;
     263                 :            : }
     264                 :            : 
     265                 :      39944 : int RepSetIterator::increment()
     266                 :            : {
     267         [ +  - ]:      39944 :   if (!isFinished())
     268                 :            :   {
     269                 :      39944 :     return incrementAtIndex(d_index.size() - 1);
     270                 :            :   }
     271                 :            :   else
     272                 :            :   {
     273                 :          0 :     return -1;
     274                 :            :   }
     275                 :            : }
     276                 :            : 
     277                 :     170195 : bool RepSetIterator::isFinished() const { return d_index.empty(); }
     278                 :            : 
     279                 :     108420 : Node RepSetIterator::getCurrentTerm(size_t i, bool valTerm) const
     280                 :            : {
     281                 :     108420 :   size_t ii = d_index_order[i];
     282                 :     108420 :   size_t curr = d_index[ii];
     283         [ +  - ]:     216840 :   Trace("rsi-debug") << "rsi : get term " << i
     284                 :     108420 :                      << ", index order = " << d_index_order[i] << std::endl;
     285         [ +  - ]:     216840 :   Trace("rsi-debug") << "rsi : curr = " << curr << " / "
     286                 :     108420 :                      << d_domain_elements[i].size() << std::endl;
     287 [ -  + ][ -  + ]:     108420 :   Assert(curr < d_domain_elements[i].size());
                 [ -  - ]
     288                 :     108420 :   Node t = d_domain_elements[i][curr];
     289         [ +  - ]:     108420 :   Trace("rsi-debug") << "rsi : term = " << t << std::endl;
     290         [ +  + ]:     108420 :   if (valTerm)
     291                 :            :   {
     292                 :      66948 :     Node tt = d_rs->getTermForRepresentative(t);
     293         [ +  + ]:      66948 :     if (!tt.isNull())
     294                 :            :     {
     295         [ +  - ]:      64733 :       Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl;
     296                 :      64733 :       return tt;
     297                 :            :     }
     298         [ +  + ]:      66948 :   }
     299         [ +  - ]:      43687 :   Trace("rsi-debug") << "rsi : return" << std::endl;
     300                 :      43687 :   return t;
     301                 :     108420 : }
     302                 :            : 
     303                 :        206 : void RepSetIterator::getCurrentTerms(std::vector<Node>& terms) const
     304                 :            : {
     305         [ +  + ]:        650 :   for (size_t i = 0, size = d_index_order.size(); i < size; i++)
     306                 :            :   {
     307                 :        444 :     terms.push_back(getCurrentTerm(i));
     308                 :            :   }
     309                 :        206 : }
     310                 :            : 
     311                 :          0 : void RepSetIterator::debugPrint(CVC5_UNUSED const char* c)
     312                 :            : {
     313         [ -  - ]:          0 :   for (size_t v = 0, isize = d_index.size(); v < isize; v++)
     314                 :            :   {
     315                 :          0 :     Trace(c) << v << " : " << getCurrentTerm(v) << std::endl;
     316                 :            :   }
     317                 :          0 : }
     318                 :            : 
     319                 :          0 : void RepSetIterator::debugPrintSmall(CVC5_UNUSED const char* c)
     320                 :            : {
     321         [ -  - ]:          0 :   Trace(c) << "RI: ";
     322         [ -  - ]:          0 :   for (size_t v = 0, isize = d_index.size(); v < isize; v++)
     323                 :            :   {
     324                 :          0 :     Trace(c) << v << ": " << getCurrentTerm(v) << " ";
     325                 :            :   }
     326         [ -  - ]:          0 :   Trace(c) << std::endl;
     327                 :          0 : }
     328                 :            : 
     329                 :            : }  // namespace theory
     330                 :            : }  // namespace cvc5::internal