Branch data     Line data    Source code

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