src/theory/datatypes/type_enumerator.cpp

   1 /*********************                                                        */
   2 /*! \file type_enumerator.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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.\endverbatim
  11  **
  12  ** \brief Enumerators for datatypes
  13  **
  14  ** Enumerators for datatypes.
  15  **/
  16
  17 #include "theory/datatypes/type_enumerator.h"
  18 #include "theory/datatypes/datatypes_rewriter.h"
  19 #include "theory/datatypes/theory_datatypes_utils.h"
  20
  21 using namespace CVC4;
  22 using namespace theory;
  23 using namespace datatypes;
  24
  25 Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
  26    Node ret;
  27    if( i<d_terms[tn].size() ){
  28      ret = d_terms[tn][i];
  29    }else{
  30      Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl;
  31      std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn );
  32      unsigned tei;
  33      if( it==d_te_index.end() ){
  34        //initialize child enumerator for type
  35        tei = d_children.size();
  36        d_te_index[tn] = tei;
  37        if( tn.isDatatype() && d_has_debruijn ){
  38          //must indicate that this is a child enumerator (do not normalize constants for it)
  39          DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep );
  40          d_children.push_back( TypeEnumerator( dte ) );
  41        }else{
  42          d_children.push_back( TypeEnumerator( tn, d_tep ) );
  43        }
  44        d_terms[tn].push_back( *d_children[tei] );
  45      }else{
  46        tei = it->second;
  47      }
  48      //enumerate terms until index is reached
  49      while( i>=d_terms[tn].size() ){
  50        ++d_children[tei];
  51        if( d_children[tei].isFinished() ){
  52          Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl;
  53          return Node::null();
  54        }
  55        d_terms[tn].push_back( *d_children[tei] );
  56      }
  57      Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl;
  58      ret = d_terms[tn][i];
  59    }
  60    return ret;
  61  }
  62
  63  bool DatatypesEnumerator::increment( unsigned index ){
  64    Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl;
  65    if( d_sel_sum[index]==-1 ){
  66      //first time
  67      d_sel_sum[index] = 0;
  68      //special case: no children to iterate
  69      if( index>=d_has_debruijn && d_sel_types[index].empty() ){
  70        Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl;
  71        return d_size_limit==0;
  72      }else{
  73        Debug("dt-enum") << "...success" << std::endl;
  74        return true;
  75      }
  76    }else{
  77      unsigned i = 0;
  78      while( i < d_sel_index[index].size() ){
  79        //increment if the sum of iterations on arguments is less than the limit
  80        if( d_sel_sum[index]<(int)d_size_limit ){
  81          //also check if child enumerator has enough terms
  82          if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){
  83            Debug("dt-enum") << "...success increment child " << i << std::endl;
  84            d_sel_index[index][i]++;
  85            d_sel_sum[index]++;
  86            return true;
  87          }
  88        }
  89        Debug("dt-enum") << "......failed increment child " << i << std::endl;
  90        //reset child, iterate next
  91        d_sel_sum[index] -= d_sel_index[index][i];
  92        d_sel_index[index][i] = 0;
  93        i++;
  94      }
  95      Debug("dt-enum") << "...failure." << std::endl;
  96      return false;
  97    }
  98  }
  99
 100  Node DatatypesEnumerator::getCurrentTerm(unsigned index)
 101  {
 102    Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type
 103                           << std::endl;
 104    Node ret;
 105    if (index < d_has_debruijn)
 106    {
 107      if (d_child_enum)
 108      {
 109        ret = NodeManager::currentNM()->mkConst(
 110            UninterpretedConstant(d_type, d_size_limit));
 111      }
 112      else
 113      {
 114        // no top-level variables
 115        return Node::null();
 116      }
 117    }
 118    else
 119    {
 120      Debug("dt-enum-debug")
 121          << "Look at constructor " << (index - d_has_debruijn) << std::endl;
 122      const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn];
 123      Debug("dt-enum-debug") << "Check last term..." << std::endl;
 124      // we first check if the last argument (which is forced to make sum of
 125      // iterated arguments equal to d_size_limit) is defined
 126      Node lc;
 127      if (ctor.getNumArgs() > 0)
 128      {
 129        Assert(index < d_sel_types.size());
 130        Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size());
 131        lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1],
 132                         d_size_limit - d_sel_sum[index]);
 133        if (lc.isNull())
 134        {
 135          Debug("dt-enum-debug") << "Current infeasible." << std::endl;
 136          return Node::null();
 137        }
 138      }
 139      Debug("dt-enum-debug") << "Get constructor..." << std::endl;
 140      NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 141      if (d_datatype.isParametric())
 142      {
 143        NodeManager* nm = NodeManager::currentNM();
 144        TypeNode typ = ctor.getSpecializedConstructorType(d_type);
 145        b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
 146                        nm->mkConst(AscriptionType(typ)),
 147                        ctor.getConstructor());
 148      }
 149      else
 150      {
 151        b << ctor.getConstructor();
 152      }
 153      Debug("dt-enum-debug") << "Get arguments..." << std::endl;
 154      if (ctor.getNumArgs() > 0)
 155      {
 156        Assert(index < d_sel_types.size());
 157        Assert(index < d_sel_index.size());
 158        Assert(d_sel_types[index].size() == ctor.getNumArgs());
 159        Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1);
 160        for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++)
 161        {
 162          Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]);
 163          Assert(!c.isNull());
 164          b << c;
 165        }
 166        b << lc;
 167      }
 168      Node nnn = Node(b);
 169      Debug("dt-enum-debug") << "Return... " << nnn << std::endl;
 170      ret = nnn;
 171    }
 172
 173    if (!d_child_enum && d_has_debruijn)
 174    {
 175      Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret);
 176      if (nret != ret)
 177      {
 178        if (nret.isNull())
 179        {
 180          Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl;
 181        }
 182        else
 183        {
 184          Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl;
 185          Trace("dt-enum-nn") << "  ...normal form is : " << nret << std::endl;
 186        }
 187        return Node::null();
 188      }
 189    }
 190
 191    return ret;
 192  }
 193
 194  void DatatypesEnumerator::init()
 195  {
 196    Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype()
 197                     << std::endl;
 198    Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
 199    Debug("dt-enum") << "datatype is " << d_type << std::endl;
 200    Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " "
 201                     << d_datatype.isRecursiveSingleton(d_type);
 202    Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type)
 203                     << std::endl;
 204    // Start with the ground term constructed via mkGroundValue, which does
 205    // a traversal over the structure of the datatype to find a finite term.
 206    // Notice that mkGroundValue may be dependent upon extracting the first
 207    // value of type enumerators for *other non-datatype* subfield types of
 208    // this datatype. Since datatypes can not be embedded in non-datatype
 209    // types (e.g. (Array D D) cannot be a subfield type of datatype D), this
 210    // call is guaranteed to avoid infinite recursion. It is important that we
 211    // start with this term, since it has the same shape as the one returned by
 212    // TypeNode::mkGroundTerm for d_type, which avoids debug check model
 213    // failures.
 214    d_zeroTerm = d_datatype.mkGroundValue(d_type);
 215    // Only use the zero term if it was successfully constructed. This may
 216    // fail for codatatype types whose only values are infinite.
 217    d_zeroTermActive = !d_zeroTerm.isNull();
 218    if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype))
 219    {
 220      // start with uninterpreted constant
 221      d_has_debruijn = 1;
 222      d_sel_types.push_back(std::vector<TypeNode>());
 223      d_sel_index.push_back(std::vector<unsigned>());
 224      d_sel_sum.push_back(-1);
 225    }
 226    else
 227    {
 228      // find the "zero" term via mkGroundTerm
 229      Debug("dt-enum-debug") << "make ground term..." << std::endl;
 230      Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl;
 231      Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR);
 232      d_has_debruijn = 0;
 233    }
 234    Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl;
 235    d_ctor = 0;
 236    for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i)
 237    {
 238      d_sel_types.push_back(std::vector<TypeNode>());
 239      d_sel_index.push_back(std::vector<unsigned>());
 240      d_sel_sum.push_back(-1);
 241      const DTypeConstructor& ctor = d_datatype[i];
 242      TypeNode typ;
 243      if (d_datatype.isParametric())
 244      {
 245        typ = ctor.getSpecializedConstructorType(d_type);
 246      }
 247      for (unsigned a = 0; a < ctor.getNumArgs(); ++a)
 248      {
 249        TypeNode tn;
 250        if (d_datatype.isParametric())
 251        {
 252          tn = typ[a];
 253        }
 254        else
 255        {
 256          tn = ctor[a].getSelector().getType()[1];
 257        }
 258        d_sel_types.back().push_back(tn);
 259        d_sel_index.back().push_back(0);
 260      }
 261      if (!d_sel_index.back().empty())
 262      {
 263        d_sel_index.back().pop_back();
 264      }
 265    }
 266    d_size_limit = 0;
 267    if (!d_zeroTermActive)
 268    {
 269      // Set up initial conditions (should always succeed). Here, we are calling
 270      // the increment function of this class, which ensures a term is ready to
 271      // read via a dereference of this class. We use the same method for
 272      // setting up the first term, if it is not already set up
 273      // (d_zeroTermActive) using the increment function, for uniformity.
 274      ++*this;
 275    }
 276    AlwaysAssert(!isFinished());
 277  }
 278
 279  DatatypesEnumerator& DatatypesEnumerator::operator++()
 280  {
 281    Debug("dt-enum-debug") << ": increment " << this << std::endl;
 282    if (d_zeroTermActive)
 283    {
 284      d_zeroTermActive = false;
 285    }
 286    unsigned prevSize = d_size_limit;
 287    while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors())
 288    {
 289      // increment at index
 290      while (increment(d_ctor))
 291      {
 292        Node n = getCurrentTerm(d_ctor);
 293        if (!n.isNull())
 294        {
 295          if (n == d_zeroTerm)
 296          {
 297            d_zeroTerm = Node::null();
 298          }
 299          else
 300          {
 301            return *this;
 302          }
 303        }
 304      }
 305      // Here, we need to step from the current constructor to the next one
 306
 307      // Go to the next constructor
 308      d_ctor = d_ctor + 1;
 309      if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors())
 310      {
 311        // try next size limit as long as new terms were generated at last size,
 312        // or other cases
 313        if (prevSize == d_size_limit
 314            || (d_size_limit == 0 && d_datatype.isCodatatype())
 315            || !d_datatype.isInterpretedFinite(d_type))
 316        {
 317          d_size_limit++;
 318          d_ctor = 0;
 319          for (unsigned i = 0; i < d_sel_sum.size(); i++)
 320          {
 321            d_sel_sum[i] = -1;
 322          }
 323        }
 324      }
 325    }
 326    return *this;
 327  }