1 /*********************                                                        */
2 /*! \file term_enumeration.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 /** Term enumeration
32  *
33  * This class has utilities for enumerating terms. It stores
34  * a cache of terms enumerated per each type.
35  * It also has various utility functions regarding type
36  * enumeration.
37  */
38 class TermEnumeration
39 {
40  public:
TermEnumeration()41   TermEnumeration() {}
~TermEnumeration()42   ~TermEnumeration() {}
43   /** get i^th term for type tn */
44   Node getEnumerateTerm(TypeNode tn, unsigned i);
45   /** may complete type
46    *
47    * Returns true if the type tn is closed enumerable, is interpreted as a
48    * finite type, and has cardinality less than some reasonable value
49    * (currently < 1000). This method caches the results of whether each type
50    * may be completed.
51    */
52   bool mayComplete(TypeNode tn);
53   /**
54    * Static version of the above method where maximum cardinality is
55    * configurable.
56    */
57   static bool mayComplete(TypeNode tn, unsigned cardMax);
58 
59  private:
60   /** ground terms enumerated for types */
61   std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction>
62       d_enum_terms;
63   /** map from type to the index of its type enumerator in d_typ_enum. */
64   std::unordered_map<TypeNode, size_t, TypeNodeHashFunction> d_typ_enum_map;
65   /** type enumerators */
66   std::vector<TypeEnumerator> d_typ_enum;
67   /** closed enumerable type cache */
68   std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_typ_closed_enum;
69   /** may complete */
70   std::unordered_map<TypeNode, bool, TypeNodeHashFunction> d_may_complete;
71 };
72 
73 } /* CVC4::theory::quantifiers namespace */
74 } /* CVC4::theory namespace */
75 } /* CVC4 namespace */
76 
77 #endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
78