1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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_POOLS_H |
19 |
|
#define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H |
20 |
|
|
21 |
|
#include <unordered_set> |
22 |
|
#include <vector> |
23 |
|
|
24 |
|
#include "expr/node.h" |
25 |
|
#include "theory/quantifiers/quant_util.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace theory { |
29 |
|
namespace quantifiers { |
30 |
|
|
31 |
|
class QuantifiersState; |
32 |
|
|
33 |
|
/** |
34 |
|
* Information concerning a pool variable. |
35 |
|
*/ |
36 |
12 |
class TermPoolDomain |
37 |
|
{ |
38 |
|
public: |
39 |
|
/** initialize, which clears the data below */ |
40 |
|
void initialize(); |
41 |
|
/** add node to this pool */ |
42 |
|
void add(Node n); |
43 |
|
/** The list in this pool */ |
44 |
|
std::vector<Node> d_terms; |
45 |
|
/** |
46 |
|
* The list of terms on this round. This is cleared at the beginning of an |
47 |
|
* instantiation round. The members are unique modulo equality. |
48 |
|
*/ |
49 |
|
std::vector<Node> d_currTerms; |
50 |
|
}; |
51 |
|
|
52 |
|
/** |
53 |
|
* Contains all annotations that pertain to pools for a given quantified |
54 |
|
* formula. |
55 |
|
*/ |
56 |
10974 |
class TermPoolQuantInfo |
57 |
|
{ |
58 |
|
public: |
59 |
|
/** initialize, which clears the data below */ |
60 |
|
void initialize(); |
61 |
|
/** Annotations of kind INST_ADD_TO_POOL */ |
62 |
|
std::vector<Node> d_instAddToPool; |
63 |
|
/** Annotations of kind SKOLEM_ADD_TO_POOL */ |
64 |
|
std::vector<Node> d_skolemAddToPool; |
65 |
|
}; |
66 |
|
|
67 |
|
/** |
68 |
|
* Term pools, which tracks the values of "pools", which are used for |
69 |
|
* pool-based instantiation. |
70 |
|
*/ |
71 |
|
class TermPools : public QuantifiersUtil |
72 |
|
{ |
73 |
|
public: |
74 |
|
TermPools(QuantifiersState& qs); |
75 |
19700 |
~TermPools() {} |
76 |
|
/** reset, which resets the current values of pools */ |
77 |
|
bool reset(Theory::Effort e) override; |
78 |
|
/** Called for new quantifiers, which computes TermPoolQuantInfo above */ |
79 |
|
void registerQuantifier(Node q) override; |
80 |
|
/** Identify this module (for debugging, dynamic configuration, etc..) */ |
81 |
|
std::string identify() const override; |
82 |
|
/** Register pool p with initial value initValue. */ |
83 |
|
void registerPool(Node p, const std::vector<Node>& initValue); |
84 |
|
/** Get terms for pool p, adds them to the vector terms. */ |
85 |
|
void getTermsForPool(Node p, std::vector<Node>& terms); |
86 |
|
/** |
87 |
|
* Process instantiation, called at the moment we successfully instantiate |
88 |
|
* q with terms. This adds terms to pools based on INST_ADD_TO_POOL |
89 |
|
* annotations. |
90 |
|
*/ |
91 |
|
void processInstantiation(Node q, const std::vector<Node>& terms); |
92 |
|
/** Same as above, for SKOLEM_ADD_TO_POOL. */ |
93 |
|
void processSkolemization(Node q, const std::vector<Node>& skolems); |
94 |
|
private: |
95 |
|
void processInternal(Node q, const std::vector<Node>& ts, bool isInst); |
96 |
|
/** reference to the quantifiers state */ |
97 |
|
QuantifiersState& d_qs; |
98 |
|
/** Maps pools to a domain */ |
99 |
|
std::map<Node, TermPoolDomain> d_pools; |
100 |
|
/** Maps quantifiers to info */ |
101 |
|
std::map<Node, TermPoolQuantInfo> d_qinfo; |
102 |
|
}; |
103 |
|
|
104 |
|
} // namespace quantifiers |
105 |
|
} // namespace theory |
106 |
|
} // namespace cvc5 |
107 |
|
|
108 |
|
#endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */ |