GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_enumeration.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_enumeration.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 utilities for term enumeration
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
18
#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
19
20
#include <unordered_map>
21
#include <vector>
22
23
#include "expr/node.h"
24
#include "expr/type_node.h"
25
#include "theory/type_enumerator.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace quantifiers {
30
31
class QuantifiersBoundInference;
32
33
/** Term enumeration
34
 *
35
 * This class has utilities for enumerating terms. It stores
36
 * a cache of terms enumerated per each type.
37
 * It also has various utility functions regarding type
38
 * enumeration.
39
 */
40
class TermEnumeration
41
{
42
 public:
43
  TermEnumeration(QuantifiersBoundInference* qbi = nullptr);
44
15963
  ~TermEnumeration() {}
45
  /** get i^th term for type tn */
46
  Node getEnumerateTerm(TypeNode tn, unsigned i);
47
48
  /** get domain
49
   *
50
   * If tn is a type such that d_qbi.mayComplete(tn) returns true, this method
51
   * adds all domain elements of tn to dom and returns true. Otherwise, this
52
   * method returns false.
53
   */
54
  bool getDomain(TypeNode tn, std::vector<Node>& dom);
55
56
 private:
57
  /**
58
   * Reference to quantifiers bound inference, which determines when it is
59
   * possible to enumerate the entire domain of a type. If this is not provided,
60
   * getDomain above always returns false.
61
   */
62
  QuantifiersBoundInference* d_qbi;
63
  /** ground terms enumerated for types */
64
  std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
65
      d_enum_terms;
66
  /** map from type to the index of its type enumerator in d_typ_enum. */
67
  std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
68
  /** type enumerators */
69
  std::vector<TypeEnumerator> d_typ_enum;
70
};
71
72
} /* CVC4::theory::quantifiers namespace */
73
} /* CVC4::theory namespace */
74
} /* CVC4 namespace */
75
76
#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */