1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Tim King |
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 |
|
* Implementation of trigger class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/ematching/trigger.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "options/quantifiers_options.h" |
20 |
|
#include "theory/quantifiers/ematching/candidate_generator.h" |
21 |
|
#include "theory/quantifiers/ematching/inst_match_generator.h" |
22 |
|
#include "theory/quantifiers/ematching/inst_match_generator_multi.h" |
23 |
|
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" |
24 |
|
#include "theory/quantifiers/ematching/inst_match_generator_simple.h" |
25 |
|
#include "theory/quantifiers/ematching/pattern_term_selector.h" |
26 |
|
#include "theory/quantifiers/ematching/trigger_trie.h" |
27 |
|
#include "theory/quantifiers/inst_match.h" |
28 |
|
#include "theory/quantifiers/instantiate.h" |
29 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
30 |
|
#include "theory/quantifiers/quantifiers_inference_manager.h" |
31 |
|
#include "theory/quantifiers/quantifiers_registry.h" |
32 |
|
#include "theory/quantifiers/quantifiers_state.h" |
33 |
|
#include "theory/quantifiers/term_util.h" |
34 |
|
#include "theory/valuation.h" |
35 |
|
|
36 |
|
using namespace cvc5::kind; |
37 |
|
|
38 |
|
namespace cvc5 { |
39 |
|
namespace theory { |
40 |
|
namespace quantifiers { |
41 |
|
namespace inst { |
42 |
|
|
43 |
|
/** trigger class constructor */ |
44 |
17261 |
Trigger::Trigger(QuantifiersState& qs, |
45 |
|
QuantifiersInferenceManager& qim, |
46 |
|
QuantifiersRegistry& qr, |
47 |
|
TermRegistry& tr, |
48 |
|
Node q, |
49 |
17261 |
std::vector<Node>& nodes) |
50 |
17261 |
: d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) |
51 |
|
{ |
52 |
|
// We must ensure that the ground subterms of the trigger have been |
53 |
|
// preprocessed. |
54 |
17261 |
Valuation& val = d_qstate.getValuation(); |
55 |
36107 |
for (const Node& n : nodes) |
56 |
|
{ |
57 |
37692 |
Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); |
58 |
18846 |
d_nodes.push_back(np); |
59 |
|
} |
60 |
17261 |
if (Trace.isOn("trigger")) |
61 |
|
{ |
62 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
63 |
|
Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": " |
64 |
|
<< std::endl; |
65 |
|
for (const Node& n : d_nodes) |
66 |
|
{ |
67 |
|
Trace("trigger") << " " << n << std::endl; |
68 |
|
} |
69 |
|
} |
70 |
17261 |
QuantifiersStatistics& stats = qs.getStats(); |
71 |
17261 |
if( d_nodes.size()==1 ){ |
72 |
15985 |
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) |
73 |
|
{ |
74 |
7694 |
d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); |
75 |
7694 |
++(stats.d_triggers); |
76 |
|
}else{ |
77 |
8291 |
d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); |
78 |
8291 |
++(stats.d_simple_triggers); |
79 |
|
} |
80 |
|
}else{ |
81 |
2555 |
if( options::multiTriggerCache() ){ |
82 |
10 |
d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); |
83 |
|
}else{ |
84 |
1266 |
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); |
85 |
|
} |
86 |
1276 |
if (Trace.isOn("multi-trigger")) |
87 |
|
{ |
88 |
|
Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; |
89 |
|
for (const Node& nc : d_nodes) |
90 |
|
{ |
91 |
|
Trace("multi-trigger") << " " << nc << std::endl; |
92 |
|
} |
93 |
|
} |
94 |
1276 |
++(stats.d_multi_triggers); |
95 |
|
} |
96 |
|
|
97 |
17261 |
Trace("trigger-debug") << "Finished making trigger." << std::endl; |
98 |
17261 |
} |
99 |
|
|
100 |
51747 |
Trigger::~Trigger() { |
101 |
17261 |
delete d_mg; |
102 |
34486 |
} |
103 |
|
|
104 |
151624 |
void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); } |
105 |
|
|
106 |
151624 |
void Trigger::reset(Node eqc) { d_mg->reset(eqc); } |
107 |
|
|
108 |
22982 |
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } |
109 |
|
|
110 |
|
Node Trigger::getInstPattern() const |
111 |
|
{ |
112 |
|
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); |
113 |
|
} |
114 |
|
|
115 |
48013 |
uint64_t Trigger::addInstantiations() |
116 |
|
{ |
117 |
48013 |
uint64_t gtAddedLemmas = 0; |
118 |
48013 |
if (!d_groundTerms.empty()) |
119 |
|
{ |
120 |
|
// for each ground term t that does not exist in the equality engine, we |
121 |
|
// add a purification lemma of the form (k = t). |
122 |
3493 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
123 |
7067 |
for (const Node& gt : d_groundTerms) |
124 |
|
{ |
125 |
3574 |
if (!ee->hasTerm(gt)) |
126 |
|
{ |
127 |
430 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
128 |
860 |
Node k = sm->mkPurifySkolem(gt, "gt"); |
129 |
860 |
Node eq = k.eqNode(gt); |
130 |
860 |
Trace("trigger-gt-lemma") |
131 |
430 |
<< "Trigger: ground term purify lemma: " << eq << std::endl; |
132 |
430 |
d_qim.addPendingLemma(eq, InferenceId::UNKNOWN); |
133 |
430 |
gtAddedLemmas++; |
134 |
|
} |
135 |
|
} |
136 |
|
} |
137 |
48013 |
uint64_t addedLemmas = d_mg->addInstantiations(d_quant); |
138 |
48013 |
if (Debug.isOn("inst-trigger")) |
139 |
|
{ |
140 |
|
if (addedLemmas > 0) |
141 |
|
{ |
142 |
|
Debug("inst-trigger") << "Added " << addedLemmas |
143 |
|
<< " lemmas, trigger was " << d_nodes << std::endl; |
144 |
|
} |
145 |
|
} |
146 |
48013 |
return gtAddedLemmas + addedLemmas; |
147 |
|
} |
148 |
|
|
149 |
137371 |
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) |
150 |
|
{ |
151 |
137371 |
return d_qim.getInstantiate()->addInstantiation(d_quant, m, id); |
152 |
|
} |
153 |
|
|
154 |
137563 |
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) |
155 |
|
{ |
156 |
137563 |
return sendInstantiation(m.d_vals, id); |
157 |
|
} |
158 |
|
|
159 |
|
int Trigger::getActiveScore() { return d_mg->getActiveScore(); } |
160 |
|
|
161 |
18846 |
Node Trigger::ensureGroundTermPreprocessed(Valuation& val, |
162 |
|
Node n, |
163 |
|
std::vector<Node>& gts) |
164 |
|
{ |
165 |
18846 |
NodeManager* nm = NodeManager::currentNM(); |
166 |
37692 |
std::unordered_map<TNode, Node> visited; |
167 |
18846 |
std::unordered_map<TNode, Node>::iterator it; |
168 |
37692 |
std::vector<TNode> visit; |
169 |
37692 |
TNode cur; |
170 |
18846 |
visit.push_back(n); |
171 |
142594 |
do |
172 |
|
{ |
173 |
161440 |
cur = visit.back(); |
174 |
161440 |
visit.pop_back(); |
175 |
161440 |
it = visited.find(cur); |
176 |
161440 |
if (it == visited.end()) |
177 |
|
{ |
178 |
109238 |
if (cur.getNumChildren() == 0) |
179 |
|
{ |
180 |
57851 |
visited[cur] = cur; |
181 |
|
} |
182 |
51387 |
else if (!TermUtil::hasInstConstAttr(cur)) |
183 |
|
{ |
184 |
|
// cur has no INST_CONSTANT, thus is ground. |
185 |
2872 |
Node vcur = val.getPreprocessedTerm(cur); |
186 |
1436 |
gts.push_back(vcur); |
187 |
1436 |
visited[cur] = vcur; |
188 |
|
} |
189 |
|
else |
190 |
|
{ |
191 |
49951 |
visited[cur] = Node::null(); |
192 |
49951 |
visit.push_back(cur); |
193 |
49951 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
194 |
|
} |
195 |
|
} |
196 |
52202 |
else if (it->second.isNull()) |
197 |
|
{ |
198 |
99902 |
Node ret = cur; |
199 |
49951 |
bool childChanged = false; |
200 |
99902 |
std::vector<Node> children; |
201 |
49951 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
202 |
|
{ |
203 |
42267 |
children.push_back(cur.getOperator()); |
204 |
|
} |
205 |
142594 |
for (const Node& cn : cur) |
206 |
|
{ |
207 |
92643 |
it = visited.find(cn); |
208 |
92643 |
Assert(it != visited.end()); |
209 |
92643 |
Assert(!it->second.isNull()); |
210 |
92643 |
childChanged = childChanged || cn != it->second; |
211 |
92643 |
children.push_back(it->second); |
212 |
|
} |
213 |
49951 |
if (childChanged) |
214 |
|
{ |
215 |
182 |
ret = nm->mkNode(cur.getKind(), children); |
216 |
|
} |
217 |
49951 |
visited[cur] = ret; |
218 |
|
} |
219 |
161440 |
} while (!visit.empty()); |
220 |
18846 |
Assert(visited.find(n) != visited.end()); |
221 |
18846 |
Assert(!visited.find(n)->second.isNull()); |
222 |
37692 |
return visited[n]; |
223 |
|
} |
224 |
|
|
225 |
34297 |
void Trigger::debugPrint(const char* c) const |
226 |
|
{ |
227 |
34297 |
Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; |
228 |
34297 |
} |
229 |
|
|
230 |
|
} // namespace inst |
231 |
|
} // namespace quantifiers |
232 |
|
} // namespace theory |
233 |
29473 |
} // namespace cvc5 |