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/outputc.h" |
21 |
|
#include "options/quantifiers_options.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 |
17033 |
Trigger::Trigger(QuantifiersState& qs, |
47 |
|
QuantifiersInferenceManager& qim, |
48 |
|
QuantifiersRegistry& qr, |
49 |
|
TermRegistry& tr, |
50 |
|
Node q, |
51 |
17033 |
std::vector<Node>& nodes) |
52 |
17033 |
: d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q) |
53 |
|
{ |
54 |
|
// We must ensure that the ground subterms of the trigger have been |
55 |
|
// preprocessed. |
56 |
17033 |
Valuation& val = d_qstate.getValuation(); |
57 |
35657 |
for (const Node& n : nodes) |
58 |
|
{ |
59 |
37248 |
Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); |
60 |
18624 |
d_nodes.push_back(np); |
61 |
|
} |
62 |
17033 |
if (Trace.isOn("trigger")) |
63 |
|
{ |
64 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
65 |
|
Trace("trigger") << "Trigger for " << qa.quantToString(q) << ": " |
66 |
|
<< std::endl; |
67 |
|
for (const Node& n : d_nodes) |
68 |
|
{ |
69 |
|
Trace("trigger") << " " << n << std::endl; |
70 |
|
} |
71 |
|
} |
72 |
34066 |
std::vector<Node> extNodes; |
73 |
35657 |
for (const Node& nt : d_nodes) |
74 |
|
{ |
75 |
|
// note we must display the original form, so we go back to bound vars |
76 |
37248 |
Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q); |
77 |
18624 |
extNodes.push_back(ns); |
78 |
|
} |
79 |
17033 |
d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); |
80 |
17033 |
if (Output.isOn(options::OutputTag::TRIGGER)) |
81 |
|
{ |
82 |
|
QuantAttributes& qa = d_qreg.getQuantAttributes(); |
83 |
|
Output(options::OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) |
84 |
|
<< " " << d_trNode << ")" << std::endl; |
85 |
|
} |
86 |
17033 |
QuantifiersStatistics& stats = qs.getStats(); |
87 |
17033 |
if( d_nodes.size()==1 ){ |
88 |
15723 |
if (TriggerTermInfo::isSimpleTrigger(d_nodes[0])) |
89 |
|
{ |
90 |
7717 |
d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]); |
91 |
7717 |
++(stats.d_triggers); |
92 |
|
}else{ |
93 |
8006 |
d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]); |
94 |
8006 |
++(stats.d_simple_triggers); |
95 |
|
} |
96 |
|
}else{ |
97 |
1310 |
if( options::multiTriggerCache() ){ |
98 |
10 |
d_mg = new InstMatchGeneratorMulti(this, q, d_nodes); |
99 |
|
}else{ |
100 |
1300 |
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes); |
101 |
|
} |
102 |
1310 |
if (Trace.isOn("multi-trigger")) |
103 |
|
{ |
104 |
|
Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl; |
105 |
|
for (const Node& nc : d_nodes) |
106 |
|
{ |
107 |
|
Trace("multi-trigger") << " " << nc << std::endl; |
108 |
|
} |
109 |
|
} |
110 |
1310 |
++(stats.d_multi_triggers); |
111 |
|
} |
112 |
|
|
113 |
17033 |
Trace("trigger-debug") << "Finished making trigger." << std::endl; |
114 |
17033 |
} |
115 |
|
|
116 |
51063 |
Trigger::~Trigger() { |
117 |
17033 |
delete d_mg; |
118 |
34030 |
} |
119 |
|
|
120 |
147295 |
void Trigger::resetInstantiationRound() { d_mg->resetInstantiationRound(); } |
121 |
|
|
122 |
147295 |
void Trigger::reset(Node eqc) { d_mg->reset(eqc); } |
123 |
|
|
124 |
23050 |
bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } |
125 |
|
|
126 |
|
Node Trigger::getInstPattern() const |
127 |
|
{ |
128 |
|
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes ); |
129 |
|
} |
130 |
|
|
131 |
48391 |
uint64_t Trigger::addInstantiations() |
132 |
|
{ |
133 |
48391 |
uint64_t gtAddedLemmas = 0; |
134 |
48391 |
if (!d_groundTerms.empty()) |
135 |
|
{ |
136 |
|
// for each ground term t that does not exist in the equality engine, we |
137 |
|
// add a purification lemma of the form (k = t). |
138 |
3597 |
eq::EqualityEngine* ee = d_qstate.getEqualityEngine(); |
139 |
7338 |
for (const Node& gt : d_groundTerms) |
140 |
|
{ |
141 |
3741 |
if (!ee->hasTerm(gt)) |
142 |
|
{ |
143 |
400 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
144 |
800 |
Node k = sm->mkPurifySkolem(gt, "gt"); |
145 |
800 |
Node eq = k.eqNode(gt); |
146 |
800 |
Trace("trigger-gt-lemma") |
147 |
400 |
<< "Trigger: ground term purify lemma: " << eq << std::endl; |
148 |
400 |
d_qim.addPendingLemma(eq, InferenceId::QUANTIFIERS_GT_PURIFY); |
149 |
400 |
gtAddedLemmas++; |
150 |
|
} |
151 |
|
} |
152 |
|
} |
153 |
48391 |
uint64_t addedLemmas = d_mg->addInstantiations(d_quant); |
154 |
48391 |
if (Debug.isOn("inst-trigger")) |
155 |
|
{ |
156 |
|
if (addedLemmas > 0) |
157 |
|
{ |
158 |
|
Debug("inst-trigger") << "Added " << addedLemmas |
159 |
|
<< " lemmas, trigger was " << d_nodes << std::endl; |
160 |
|
} |
161 |
|
} |
162 |
48391 |
return gtAddedLemmas + addedLemmas; |
163 |
|
} |
164 |
|
|
165 |
123367 |
bool Trigger::sendInstantiation(std::vector<Node>& m, InferenceId id) |
166 |
|
{ |
167 |
123367 |
return d_qim.getInstantiate()->addInstantiation(d_quant, m, id, d_trNode); |
168 |
|
} |
169 |
|
|
170 |
123559 |
bool Trigger::sendInstantiation(InstMatch& m, InferenceId id) |
171 |
|
{ |
172 |
123559 |
return sendInstantiation(m.d_vals, id); |
173 |
|
} |
174 |
|
|
175 |
|
int Trigger::getActiveScore() { return d_mg->getActiveScore(); } |
176 |
|
|
177 |
18624 |
Node Trigger::ensureGroundTermPreprocessed(Valuation& val, |
178 |
|
Node n, |
179 |
|
std::vector<Node>& gts) |
180 |
|
{ |
181 |
18624 |
NodeManager* nm = NodeManager::currentNM(); |
182 |
37248 |
std::unordered_map<TNode, Node> visited; |
183 |
18624 |
std::unordered_map<TNode, Node>::iterator it; |
184 |
37248 |
std::vector<TNode> visit; |
185 |
37248 |
TNode cur; |
186 |
18624 |
visit.push_back(n); |
187 |
139537 |
do |
188 |
|
{ |
189 |
158161 |
cur = visit.back(); |
190 |
158161 |
visit.pop_back(); |
191 |
158161 |
it = visited.find(cur); |
192 |
158161 |
if (it == visited.end()) |
193 |
|
{ |
194 |
107193 |
if (cur.getNumChildren() == 0) |
195 |
|
{ |
196 |
56818 |
visited[cur] = cur; |
197 |
|
} |
198 |
50375 |
else if (!TermUtil::hasInstConstAttr(cur)) |
199 |
|
{ |
200 |
|
// cur has no INST_CONSTANT, thus is ground. |
201 |
2970 |
Node vcur = val.getPreprocessedTerm(cur); |
202 |
1485 |
gts.push_back(vcur); |
203 |
1485 |
visited[cur] = vcur; |
204 |
|
} |
205 |
|
else |
206 |
|
{ |
207 |
48890 |
visited[cur] = Node::null(); |
208 |
48890 |
visit.push_back(cur); |
209 |
48890 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
210 |
|
} |
211 |
|
} |
212 |
50968 |
else if (it->second.isNull()) |
213 |
|
{ |
214 |
97780 |
Node ret = cur; |
215 |
48890 |
bool childChanged = false; |
216 |
97780 |
std::vector<Node> children; |
217 |
48890 |
if (cur.getMetaKind() == metakind::PARAMETERIZED) |
218 |
|
{ |
219 |
41219 |
children.push_back(cur.getOperator()); |
220 |
|
} |
221 |
139537 |
for (const Node& cn : cur) |
222 |
|
{ |
223 |
90647 |
it = visited.find(cn); |
224 |
90647 |
Assert(it != visited.end()); |
225 |
90647 |
Assert(!it->second.isNull()); |
226 |
90647 |
childChanged = childChanged || cn != it->second; |
227 |
90647 |
children.push_back(it->second); |
228 |
|
} |
229 |
48890 |
if (childChanged) |
230 |
|
{ |
231 |
299 |
ret = nm->mkNode(cur.getKind(), children); |
232 |
|
} |
233 |
48890 |
visited[cur] = ret; |
234 |
|
} |
235 |
158161 |
} while (!visit.empty()); |
236 |
18624 |
Assert(visited.find(n) != visited.end()); |
237 |
18624 |
Assert(!visited.find(n)->second.isNull()); |
238 |
37248 |
return visited[n]; |
239 |
|
} |
240 |
|
|
241 |
35093 |
void Trigger::debugPrint(const char* c) const |
242 |
|
{ |
243 |
35093 |
Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; |
244 |
35093 |
} |
245 |
|
|
246 |
|
} // namespace inst |
247 |
|
} // namespace quantifiers |
248 |
|
} // namespace theory |
249 |
29577 |
} // namespace cvc5 |