GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/type_set.h Lines: 4 4 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_set.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 Type set class
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__TYPE_SET_H
18
#define CVC4__THEORY__TYPE_SET_H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
23
#include "theory/type_enumerator.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
/* Type set
29
 *
30
 * This class encapsulates a map from types to sets of nodes.
31
 */
32
class TypeSet
33
{
34
 public:
35
  typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction>
36
      TypeSetMap;
37
  typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction>
38
      TypeToTypeEnumMap;
39
  typedef TypeSetMap::iterator iterator;
40
  typedef TypeSetMap::const_iterator const_iterator;
41
42
 public:
43
61755
  TypeSet() : d_tep(NULL) {}
44
  ~TypeSet();
45
  /** set the properties of the type set
46
   *
47
   * These indicate information such as finite bounds
48
   * on the number of unique uninterpreted constants that can be
49
   * enumerated by this class.
50
   */
51
  void setTypeEnumeratorProperties(TypeEnumeratorProperties* tep);
52
  /** add node n to the set of values of t */
53
  void add(TypeNode t, TNode n);
54
  /** get the set of values of type t */
55
  std::set<Node>* getSet(TypeNode t) const;
56
  /** get the next enumerated term of type t
57
   *
58
   * useBaseType is whether
59
   */
60
  Node nextTypeEnum(TypeNode t, bool useBaseType = false);
61
62
  bool empty() { return d_typeSet.empty(); }
63
37900
  iterator begin() { return d_typeSet.begin(); }
64
70127
  iterator end() { return d_typeSet.end(); }
65
  static TypeNode getType(iterator it) { return (*it).first; }
66
32227
  static std::set<Node>& getSet(iterator it) { return *(*it).second; }
67
 private:
68
  /** sets of values for each type */
69
  TypeSetMap d_typeSet;
70
  /** type enumerators for each type */
71
  TypeToTypeEnumMap d_teMap;
72
  /** pointer the type enumerator properties for this class. */
73
  TypeEnumeratorProperties* d_tep;
74
75
  /* add all sub-terms of n to the sets of this class
76
   *
77
   * If topLevel is true, then we add strict subterms only.
78
   *
79
   * Note that recursive traversal here is over enumerated expressions
80
   * (very low expression depth).
81
   */
82
  void addSubTerms(TNode n,
83
                   std::unordered_set<TNode, TNodeHashFunction>& visited,
84
                   bool topLevel = true);
85
}; /* class TypeSet */
86
87
} /* CVC4::theory namespace */
88
} /* CVC4 namespace */
89
90
#endif /* CVC4__THEORY__TYPE_SET_H */