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