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