src/theory/type_set.cpp

   1 /*********************                                                        */
   2 /*! \file type_set.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Clark Barrett
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 Implementation of type set class
  13  **/
  14 #include "theory/type_set.h"
  15
  16 using namespace std;
  17 using namespace CVC5::kind;
  18
  19 namespace CVC5 {
  20 namespace theory {
  21
  22 TypeSet::~TypeSet()
  23 {
  24   iterator it;
  25   for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
  26   {
  27     delete (*it).second;
  28   }
  29   TypeToTypeEnumMap::iterator it2;
  30   for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
  31   {
  32     delete (*it2).second;
  33   }
  34 }
  35
  36 void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
  37 {
  38   d_tep = tep;
  39 }
  40
  41 void TypeSet::add(TypeNode t, TNode n)
  42 {
  43   iterator it = d_typeSet.find(t);
  44   std::set<Node>* s;
  45   if (it == d_typeSet.end())
  46   {
  47     s = new std::set<Node>;
  48     d_typeSet[t] = s;
  49   }
  50   else
  51   {
  52     s = (*it).second;
  53   }
  54   s->insert(n);
  55 }
  56
  57 std::set<Node>* TypeSet::getSet(TypeNode t) const
  58 {
  59   const_iterator it = d_typeSet.find(t);
  60   if (it == d_typeSet.end())
  61   {
  62     return NULL;
  63   }
  64   return (*it).second;
  65 }
  66
  67 Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
  68 {
  69   TypeEnumerator* te;
  70   TypeToTypeEnumMap::iterator it = d_teMap.find(t);
  71   if (it == d_teMap.end())
  72   {
  73     te = new TypeEnumerator(t, d_tep);
  74     d_teMap[t] = te;
  75   }
  76   else
  77   {
  78     te = (*it).second;
  79   }
  80   if (te->isFinished())
  81   {
  82     return Node();
  83   }
  84
  85   if (useBaseType)
  86   {
  87     t = t.getBaseType();
  88   }
  89   iterator itSet = d_typeSet.find(t);
  90   std::set<Node>* s;
  91   if (itSet == d_typeSet.end())
  92   {
  93     s = new std::set<Node>;
  94     d_typeSet[t] = s;
  95   }
  96   else
  97   {
  98     s = (*itSet).second;
  99   }
 100   Node n = **te;
 101   while (s->find(n) != s->end())
 102   {
 103     ++(*te);
 104     if (te->isFinished())
 105     {
 106       return Node();
 107     }
 108     n = **te;
 109   }
 110   s->insert(n);
 111   // add all subterms of n to this set as well
 112   // this is necessary for parametric types whose values are constructed from
 113   // other types to ensure that we do not enumerate subterms of other
 114   // previously enumerated values
 115   std::unordered_set<TNode, TNodeHashFunction> visited;
 116   addSubTerms(n, visited);
 117   ++(*te);
 118   return n;
 119 }
 120
 121 void TypeSet::addSubTerms(TNode n,
 122                           std::unordered_set<TNode, TNodeHashFunction>& visited,
 123                           bool topLevel)
 124 {
 125   if (visited.find(n) == visited.end())
 126   {
 127     visited.insert(n);
 128     if (!topLevel)
 129     {
 130       add(n.getType(), n);
 131     }
 132     for (unsigned i = 0; i < n.getNumChildren(); i++)
 133     {
 134       addSubTerms(n[i], visited, false);
 135     }
 136   }
 137 }
 138
 139 }  // namespace theory
 140 } // namespace CVC5