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 |
6172 |
Trigger::Trigger(Env& env, |
47 |
|
QuantifiersState& qs, |
48 |
|
QuantifiersInferenceManager& qim, |
49 |
|
QuantifiersRegistry& qr, |
50 |
|
TermRegistry& tr, |
51 |
|
Node q, |
52 |
6172 |
std::vector<Node>& nodes) |
53 |
6172 |
: 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 |
6172 |
Valuation& val = d_qstate.getValuation(); |
58 |
12918 |
for (const Node& n : nodes) |
59 |
|
{ |
60 |
13492 |
Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); |
61 |
6746 |
d_nodes.push_back(np); |
62 |
|
} |
63 |
6172 |
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 |
12344 |
std::vector<Node> extNodes; |
74 |
12918 |
for (const Node& nt : d_nodes) |
75 |
|
{ |
76 |
|
// note we must display the original form, so we go back to bound vars |
77 |
13492 |
Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q); |
78 |
6746 |
extNodes.push_back(ns); |
79 |
|
} |
80 |
6172 |
d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); |
81 |
6172 |
if (d_env.isOutputOn(options::OutputTag::TRIGGER)) |
82 |
|
{ |
83 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
84 |
|
d_env.getOutput(options::OutputTag::TRIGGER) |
85 |
|
<< "(trigger " << qa.quantToString(q) << " " << d_trNode << ")" |
86 |
|
<< std::endl; |
87 |
|
} |
88 |
6172 |
QuantifiersStatistics& stats = qs.getStats(); |
89 |
6172 |
if( d_nodes.size()==1 ){ |
90 |
5702 |
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) |
91 |
|
{ |
92 |
2619 |
d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); |
93 |
2619 |
++(stats.d_triggers); |
94 |
|
}else{ |
95 |
3083 |
d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); |
96 |
3083 |
++(stats.d_simple_triggers); |
97 |
|
} |
98 |
|
}else{ |
99 |
470 |
if( options::multiTriggerCache() ){ |
100 |
3 |
d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); |
101 |
|
}else{ |
102 |
467 |
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); |
103 |
|
} |
104 |
470 |
if (Trace.isOn("multi-trigger")) |
105 |
|
{ |
106 |
|
Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; |
107 |
|
for (const Node& nc : d_nodes) |
108 |
|
{ |
109 |
|
Trace("multi-trigger") << " " << nc << std::endl; |
110 |
|
} |
111 |
|
} |
112 |
470 |
++(stats.d_multi_triggers); |
113 |
|
} |
114 |
|
|
115 |
6172 |
Trace("trigger-debug") << "Finished making trigger." << std::endl; |
116 |
6172 |
} |
117 |
|
|
118 |
18508 |
Trigger::~Trigger() { |
119 |
6172 |
delete d_mg; |
120 |
12336 |
} |
121 |
|
|
122 |
47216 |
void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); } |
123 |
|
|
124 |
47216 |
void Trigger::reset(Node eqc) { d_mg->reset(eqc); } |
125 |
|
|
126 |
8695 |
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } |
127 |
|
|
128 |
|
Node Trigger::getInstPattern() const |
129 |
|
{ |
130 |
|
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); |
131 |
|
} |
132 |
|
|
133 |
16443 |
uint64_t Trigger::addInstantiations() |
134 |
|
{ |
135 |
16443 |
uint64_t gtAddedLemmas = 0; |
136 |
16443 |
if (!d_groundTerms.empty()) |
137 |
|
{ |
138 |
|
// for each ground term t that does not exist in the equality engine, we |
139 |
|
// add a purification lemma of the form (k = t). |
140 |
1372 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
141 |
2789 |
for (const Node& gt : d_groundTerms) |
142 |
|
{ |
143 |
1417 |
if (!ee->hasTerm(gt)) |
144 |
|
{ |
145 |
170 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
146 |
340 |
Node k = sm->mkPurifySkolem(gt, "gt"); |
147 |
340 |
Node eq = k.eqNode(gt); |
148 |
340 |
Trace("trigger-gt-lemma") |
149 |
170 |
<< "Trigger: ground term purify lemma: " << eq << std::endl; |
150 |
170 |
d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY); |
151 |
170 |
gtAddedLemmas++; |
152 |
|
} |
153 |
|
} |
154 |
|
} |
155 |
16443 |
uint64_t addedLemmas = d_mg->addInstantiations(d_quant); |
156 |
16443 |
if (Debug.isOn("inst-trigger")) |
157 |
|
{ |
158 |
|
if (addedLemmas > 0) |
159 |
|
{ |
160 |
|
Debug("inst-trigger") << "Added " << addedLemmas |
161 |
|
<< " lemmas, trigger was " << d_nodes << std::endl; |
162 |
|
} |
163 |
|
} |
164 |
16443 |
return gtAddedLemmas + addedLemmas; |
165 |
|
} |
166 |
|
|
167 |
36778 |
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) |
168 |
|
{ |
169 |
36778 |
return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode); |
170 |
|
} |
171 |
|
|
172 |
36819 |
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) |
173 |
|
{ |
174 |
36819 |
return sendInstantiation(m.d_vals, id); |
175 |
|
} |
176 |
|
|
177 |
|
int Trigger::getActiveScore() { return d_mg->getActiveScore(); } |
178 |
|
|
179 |
6746 |
Node Trigger::ensureGroundTermPreprocessed(Valuation& val, |
180 |
|
Node n, |
181 |
|
std::vector<Node>& gts) |
182 |
|
{ |
183 |
6746 |
NodeManager* nm = NodeManager::currentNM(); |
184 |
13492 |
std::unordered_map<TNode, Node> visited; |
185 |
6746 |
std::unordered_map<TNode, Node>::iterator it; |
186 |
13492 |
std::vector<TNode> visit; |
187 |
13492 |
TNode cur; |
188 |
6746 |
visit.push_back(n); |
189 |
51848 |
do |
190 |
|
{ |
191 |
58594 |
cur = visit.back(); |
192 |
58594 |
visit.pop_back(); |
193 |
58594 |
it = visited.find(cur); |
194 |
58594 |
if (it == visited.end()) |
195 |
|
{ |
196 |
39638 |
if (cur.getNumChildren() == 0) |
197 |
|
{ |
198 |
20847 |
visited[cur] = cur; |
199 |
|
} |
200 |
18791 |
else if (!TermUtil::hasInstConstAttr(cur)) |
201 |
|
{ |
202 |
|
// cur has no INST_CONSTANT, thus is ground. |
203 |
1212 |
Node vcur = val.getPreprocessedTerm(cur); |
204 |
606 |
gts.push_back(vcur); |
205 |
606 |
visited[cur] = vcur; |
206 |
|
} |
207 |
|
else |
208 |
|
{ |
209 |
18185 |
visited[cur] = Node::null(); |
210 |
18185 |
visit.push_back(cur); |
211 |
18185 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
212 |
|
} |
213 |
|
} |
214 |
18956 |
else if (it->second.isNull()) |
215 |
|
{ |
216 |
36370 |
Node ret = cur; |
217 |
18185 |
bool childChanged = false; |
218 |
36370 |
std::vector<Node> children; |
219 |
18185 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
220 |
|
{ |
221 |
15344 |
children.push_back(cur.getOperator()); |
222 |
|
} |
223 |
51848 |
for (const Node& cn : cur) |
224 |
|
{ |
225 |
33663 |
it = visited.find(cn); |
226 |
33663 |
Assert(it != visited.end()); |
227 |
33663 |
Assert(!it->second.isNull()); |
228 |
33663 |
childChanged = childChanged || cn != it->second; |
229 |
33663 |
children.push_back(it->second); |
230 |
|
} |
231 |
18185 |
if (childChanged) |
232 |
|
{ |
233 |
87 |
ret = nm->mkNode(cur.getKind(), children); |
234 |
|
} |
235 |
18185 |
visited[cur] = ret; |
236 |
|
} |
237 |
58594 |
} while (!visit.empty()); |
238 |
6746 |
Assert(visited.find(n) != visited.end()); |
239 |
6746 |
Assert(!visited.find(n)->second.isNull()); |
240 |
13492 |
return visited[n]; |
241 |
|
} |
242 |
|
|
243 |
12718 |
void Trigger::debugPrint(const char* c) const |
244 |
|
{ |
245 |
12718 |
Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; |
246 |
12718 |
} |
247 |
|
|
248 |
|
} // namespace inst |
249 |
|
} // namespace quantifiers |
250 |
|
} // namespace theory |
251 |
22746 |
} // namespace cvc5 |