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/base_options.h" |
20 |
|
#include "options/quantifiers_options.h" |
21 |
|
#include "smt/env.h" |
22 |
|
#include "theory/quantifiers/ematching/candidate_generator.h" |
23 |
|
#include "theory/quantifiers/ematching/inst_match_generator.h" |
24 |
|
#include "theory/quantifiers/ematching/inst_match_generator_multi.h" |
25 |
|
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" |
26 |
|
#include "theory/quantifiers/ematching/inst_match_generator_simple.h" |
27 |
|
#include "theory/quantifiers/ematching/pattern_term_selector.h" |
28 |
|
#include "theory/quantifiers/ematching/trigger_trie.h" |
29 |
|
#include "theory/quantifiers/inst_match.h" |
30 |
|
#include "theory/quantifiers/instantiate.h" |
31 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
32 |
|
#include "theory/quantifiers/quantifiers_inference_manager.h" |
33 |
|
#include "theory/quantifiers/quantifiers_registry.h" |
34 |
|
#include "theory/quantifiers/quantifiers_state.h" |
35 |
|
#include "theory/quantifiers/term_util.h" |
36 |
|
#include "theory/valuation.h" |
37 |
|
|
38 |
|
using namespace cvc5::kind; |
39 |
|
|
40 |
|
namespace cvc5 { |
41 |
|
namespace theory { |
42 |
|
namespace quantifiers { |
43 |
|
namespace inst { |
44 |
|
|
45 |
|
/** trigger class constructor */ |
46 |
17703 |
Trigger::Trigger(Env& env, |
47 |
|
QuantifiersState& qs, |
48 |
|
QuantifiersInferenceManager& qim, |
49 |
|
QuantifiersRegistry& qr, |
50 |
|
TermRegistry& tr, |
51 |
|
Node q, |
52 |
17703 |
std::vector<Node>& nodes) |
53 |
17703 |
: EnvObj(env), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) |
54 |
|
{ |
55 |
|
// We must ensure that the ground subterms of the trigger have been |
56 |
|
// preprocessed. |
57 |
17703 |
Valuation& val = d_qstate.getValuation(); |
58 |
37057 |
for (const Node& n : nodes) |
59 |
|
{ |
60 |
38708 |
Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); |
61 |
19354 |
d_nodes.push_back(np); |
62 |
|
} |
63 |
17703 |
if (Trace.isOn("trigger")) |
64 |
|
{ |
65 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
66 |
|
Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": " |
67 |
|
<< std::endl; |
68 |
|
for (const Node& n : d_nodes) |
69 |
|
{ |
70 |
|
Trace("trigger") << " " << n << std::endl; |
71 |
|
} |
72 |
|
} |
73 |
35406 |
std::vector<Node> extNodes; |
74 |
37057 |
for (const Node& nt : d_nodes) |
75 |
|
{ |
76 |
|
// note we must display the original form, so we go back to bound vars |
77 |
38708 |
Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q); |
78 |
19354 |
extNodes.push_back(ns); |
79 |
|
} |
80 |
17703 |
d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); |
81 |
17703 |
if (isOutputOn(OutputTag::TRIGGER)) |
82 |
|
{ |
83 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
84 |
|
output(OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) << " " |
85 |
|
<< d_trNode << ")" << std::endl; |
86 |
|
} |
87 |
17703 |
QuantifiersStatistics& stats = qs.getStats(); |
88 |
17703 |
if( d_nodes.size()==1 ){ |
89 |
16363 |
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) |
90 |
|
{ |
91 |
8131 |
d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); |
92 |
8131 |
++(stats.d_triggers); |
93 |
|
}else{ |
94 |
8232 |
d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); |
95 |
8232 |
++(stats.d_simple_triggers); |
96 |
|
} |
97 |
|
}else{ |
98 |
1340 |
if (options().quantifiers.multiTriggerCache) |
99 |
|
{ |
100 |
10 |
d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); |
101 |
|
} |
102 |
|
else |
103 |
|
{ |
104 |
1330 |
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); |
105 |
|
} |
106 |
1340 |
if (Trace.isOn("multi-trigger")) |
107 |
|
{ |
108 |
|
Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; |
109 |
|
for (const Node& nc : d_nodes) |
110 |
|
{ |
111 |
|
Trace("multi-trigger") << " " << nc << std::endl; |
112 |
|
} |
113 |
|
} |
114 |
1340 |
++(stats.d_multi_triggers); |
115 |
|
} |
116 |
|
|
117 |
17703 |
Trace("trigger-debug") << "Finished making trigger." << std::endl; |
118 |
17703 |
} |
119 |
|
|
120 |
53073 |
Trigger::~Trigger() { |
121 |
17703 |
delete d_mg; |
122 |
35370 |
} |
123 |
|
|
124 |
150882 |
void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); } |
125 |
|
|
126 |
150882 |
void Trigger::reset(Node eqc) { d_mg->reset(eqc); } |
127 |
|
|
128 |
24125 |
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } |
129 |
|
|
130 |
|
Node Trigger::getInstPattern() const |
131 |
|
{ |
132 |
|
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); |
133 |
|
} |
134 |
|
|
135 |
50445 |
uint64_t Trigger::addInstantiations() |
136 |
|
{ |
137 |
50445 |
uint64_t gtAddedLemmas = 0; |
138 |
50445 |
if (!d_groundTerms.empty()) |
139 |
|
{ |
140 |
|
// for each ground term t that does not exist in the equality engine, we |
141 |
|
// add a purification lemma of the form (k = t). |
142 |
3745 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
143 |
7627 |
for (const Node& gt : d_groundTerms) |
144 |
|
{ |
145 |
3882 |
if (!ee->hasTerm(gt)) |
146 |
|
{ |
147 |
412 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
148 |
824 |
Node k = sm->mkPurifySkolem(gt, "gt"); |
149 |
824 |
Node eq = k.eqNode(gt); |
150 |
824 |
Trace("trigger-gt-lemma") |
151 |
412 |
<< "Trigger: ground term purify lemma: " << eq << std::endl; |
152 |
412 |
d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY); |
153 |
412 |
gtAddedLemmas++; |
154 |
|
} |
155 |
|
} |
156 |
|
} |
157 |
50445 |
uint64_t addedLemmas = d_mg->addInstantiations(d_quant); |
158 |
50445 |
if (Debug.isOn("inst-trigger")) |
159 |
|
{ |
160 |
|
if (addedLemmas > 0) |
161 |
|
{ |
162 |
|
Debug("inst-trigger") << "Added " << addedLemmas |
163 |
|
<< " lemmas, trigger was " << d_nodes << std::endl; |
164 |
|
} |
165 |
|
} |
166 |
50445 |
return gtAddedLemmas + addedLemmas; |
167 |
|
} |
168 |
|
|
169 |
136454 |
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) |
170 |
|
{ |
171 |
136454 |
return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode); |
172 |
|
} |
173 |
|
|
174 |
136646 |
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) |
175 |
|
{ |
176 |
136646 |
return sendInstantiation(m.d_vals, id); |
177 |
|
} |
178 |
|
|
179 |
|
int Trigger::getActiveScore() { return d_mg->getActiveScore(); } |
180 |
|
|
181 |
19354 |
Node Trigger::ensureGroundTermPreprocessed(Valuation& val, |
182 |
|
Node n, |
183 |
|
std::vector<Node>& gts) |
184 |
|
{ |
185 |
19354 |
NodeManager* nm = NodeManager::currentNM(); |
186 |
38708 |
std::unordered_map<TNode, Node> visited; |
187 |
19354 |
std::unordered_map<TNode, Node>::iterator it; |
188 |
38708 |
std::vector<TNode> visit; |
189 |
38708 |
TNode cur; |
190 |
19354 |
visit.push_back(n); |
191 |
143110 |
do |
192 |
|
{ |
193 |
162464 |
cur = visit.back(); |
194 |
162464 |
visit.pop_back(); |
195 |
162464 |
it = visited.find(cur); |
196 |
162464 |
if (it == visited.end()) |
197 |
|
{ |
198 |
110336 |
if (cur.getNumChildren() == 0) |
199 |
|
{ |
200 |
58776 |
visited[cur] = cur; |
201 |
|
} |
202 |
51560 |
else if (!TermUtil::hasInstConstAttr(cur)) |
203 |
|
{ |
204 |
|
// cur has no INST_CONSTANT, thus is ground. |
205 |
3038 |
Node vcur = val.getPreprocessedTerm(cur); |
206 |
1519 |
gts.push_back(vcur); |
207 |
1519 |
visited[cur] = vcur; |
208 |
|
} |
209 |
|
else |
210 |
|
{ |
211 |
50041 |
visited[cur] = Node::null(); |
212 |
50041 |
visit.push_back(cur); |
213 |
50041 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
214 |
|
} |
215 |
|
} |
216 |
52128 |
else if (it->second.isNull()) |
217 |
|
{ |
218 |
100082 |
Node ret = cur; |
219 |
50041 |
bool childChanged = false; |
220 |
100082 |
std::vector<Node> children; |
221 |
50041 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
222 |
|
{ |
223 |
42210 |
children.push_back(cur.getOperator()); |
224 |
|
} |
225 |
143110 |
for (const Node& cn : cur) |
226 |
|
{ |
227 |
93069 |
it = visited.find(cn); |
228 |
93069 |
Assert(it != visited.end()); |
229 |
93069 |
Assert(!it->second.isNull()); |
230 |
93069 |
childChanged = childChanged || cn != it->second; |
231 |
93069 |
children.push_back(it->second); |
232 |
|
} |
233 |
50041 |
if (childChanged) |
234 |
|
{ |
235 |
305 |
ret = nm->mkNode(cur.getKind(), children); |
236 |
|
} |
237 |
50041 |
visited[cur] = ret; |
238 |
|
} |
239 |
162464 |
} while (!visit.empty()); |
240 |
19354 |
Assert(visited.find(n) != visited.end()); |
241 |
19354 |
Assert(!visited.find(n)->second.isNull()); |
242 |
38708 |
return visited[n]; |
243 |
|
} |
244 |
|
|
245 |
36984 |
void Trigger::debugPrint(const char* c) const |
246 |
|
{ |
247 |
36984 |
Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; |
248 |
36984 |
} |
249 |
|
|
250 |
|
} // namespace inst |
251 |
|
} // namespace quantifiers |
252 |
|
} // namespace theory |
253 |
31137 |
} // namespace cvc5 |