1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Aina Niemetz |
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 theory uf candidate generator class. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/ematching/candidate_generator.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "options/quantifiers_options.h" |
21 |
|
#include "smt/solver_engine.h" |
22 |
|
#include "smt/solver_engine_scope.h" |
23 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
24 |
|
#include "theory/quantifiers/first_order_model.h" |
25 |
|
#include "theory/quantifiers/quantifiers_state.h" |
26 |
|
#include "theory/quantifiers/term_database.h" |
27 |
|
#include "theory/quantifiers/term_registry.h" |
28 |
|
#include "theory/quantifiers/term_util.h" |
29 |
|
|
30 |
|
using namespace cvc5::kind; |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
namespace theory { |
34 |
|
namespace quantifiers { |
35 |
|
namespace inst { |
36 |
|
|
37 |
35688 |
CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr) |
38 |
35688 |
: d_qs(qs), d_treg(tr) |
39 |
|
{ |
40 |
35688 |
} |
41 |
|
|
42 |
3494709 |
bool CandidateGenerator::isLegalCandidate( Node n ){ |
43 |
10484127 |
return d_treg.getTermDatabase()->isTermActive(n) |
44 |
13978836 |
&& (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n)); |
45 |
|
} |
46 |
|
|
47 |
35606 |
CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs, |
48 |
|
TermRegistry& tr, |
49 |
35606 |
Node pat) |
50 |
|
: CandidateGenerator(qs, tr), |
51 |
|
d_term_iter(-1), |
52 |
|
d_term_iter_limit(0), |
53 |
35606 |
d_mode(cand_term_none) |
54 |
|
{ |
55 |
35606 |
d_op = d_treg.getTermDatabase()->getMatchOperator(pat); |
56 |
35606 |
Assert(!d_op.isNull()); |
57 |
35606 |
} |
58 |
|
|
59 |
504585 |
void CandidateGeneratorQE::reset(Node eqc) { resetForOperator(eqc, d_op); } |
60 |
|
|
61 |
515362 |
void CandidateGeneratorQE::resetForOperator(Node eqc, Node op) |
62 |
|
{ |
63 |
515362 |
d_term_iter = 0; |
64 |
515362 |
d_eqc = eqc; |
65 |
515362 |
d_op = op; |
66 |
515362 |
d_term_iter_limit = d_treg.getTermDatabase()->getNumGroundTerms(d_op); |
67 |
515362 |
if( eqc.isNull() ){ |
68 |
120131 |
d_mode = cand_term_db; |
69 |
|
}else{ |
70 |
395231 |
if( isExcludedEqc( eqc ) ){ |
71 |
|
d_mode = cand_term_none; |
72 |
|
}else{ |
73 |
395231 |
eq::EqualityEngine* ee = d_qs.getEqualityEngine(); |
74 |
395231 |
if( ee->hasTerm( eqc ) ){ |
75 |
395231 |
TNodeTrie* tat = d_treg.getTermDatabase()->getTermArgTrie(eqc, op); |
76 |
395231 |
if( tat ){ |
77 |
|
//create an equivalence class iterator in eq class eqc |
78 |
357130 |
Node rep = ee->getRepresentative( eqc ); |
79 |
178565 |
d_eqc_iter = eq::EqClassIterator( rep, ee ); |
80 |
178565 |
d_mode = cand_term_eqc; |
81 |
|
}else{ |
82 |
216666 |
d_mode = cand_term_none; |
83 |
|
} |
84 |
|
}else{ |
85 |
|
//the only match is this term itself |
86 |
|
d_mode = cand_term_ident; |
87 |
|
} |
88 |
|
} |
89 |
|
} |
90 |
515362 |
} |
91 |
579195 |
bool CandidateGeneratorQE::isLegalOpCandidate( Node n ) { |
92 |
579195 |
if( n.hasOperator() ){ |
93 |
461676 |
if( isLegalCandidate( n ) ){ |
94 |
310329 |
return d_treg.getTermDatabase()->getMatchOperator(n) == d_op; |
95 |
|
} |
96 |
|
} |
97 |
268866 |
return false; |
98 |
|
} |
99 |
|
|
100 |
3194755 |
Node CandidateGeneratorQE::getNextCandidate(){ |
101 |
3194755 |
return getNextCandidateInternal(); |
102 |
|
} |
103 |
|
|
104 |
3214845 |
Node CandidateGeneratorQE::getNextCandidateInternal() |
105 |
|
{ |
106 |
3214845 |
if( d_mode==cand_term_db ){ |
107 |
2680910 |
Debug("cand-gen-qe") << "...get next candidate in tbd" << std::endl; |
108 |
|
//get next candidate term in the uf term database |
109 |
3547016 |
while( d_term_iter<d_term_iter_limit ){ |
110 |
3464016 |
Node n = d_treg.getTermDatabase()->getGroundTerm(d_op, d_term_iter); |
111 |
3030963 |
d_term_iter++; |
112 |
3030963 |
if( isLegalCandidate( n ) ){ |
113 |
2621827 |
if (d_treg.getTermDatabase()->hasTermCurrent(n)) |
114 |
|
{ |
115 |
2621827 |
if( d_exclude_eqc.empty() ){ |
116 |
2527172 |
return n; |
117 |
|
}else{ |
118 |
118572 |
Node r = d_qs.getRepresentative(n); |
119 |
94655 |
if( d_exclude_eqc.find( r )==d_exclude_eqc.end() ){ |
120 |
70738 |
Debug("cand-gen-qe") << "...returning " << n << std::endl; |
121 |
70738 |
return n; |
122 |
|
} |
123 |
|
} |
124 |
|
} |
125 |
|
} |
126 |
|
} |
127 |
533935 |
}else if( d_mode==cand_term_eqc ){ |
128 |
314234 |
Debug("cand-gen-qe") << "...get next candidate in eqc" << std::endl; |
129 |
1029492 |
while( !d_eqc_iter.isFinished() ){ |
130 |
936824 |
Node n = *d_eqc_iter; |
131 |
579195 |
++d_eqc_iter; |
132 |
579195 |
if( isLegalOpCandidate( n ) ){ |
133 |
221566 |
Debug("cand-gen-qe") << "...returning " << n << std::endl; |
134 |
221566 |
return n; |
135 |
|
} |
136 |
|
} |
137 |
219701 |
}else if( d_mode==cand_term_ident ){ |
138 |
3035 |
Debug("cand-gen-qe") << "...get next candidate identity" << std::endl; |
139 |
3035 |
if (!d_eqc.isNull()) |
140 |
|
{ |
141 |
2121 |
Node n = d_eqc; |
142 |
2030 |
d_eqc = Node::null(); |
143 |
2030 |
if( isLegalOpCandidate( n ) ){ |
144 |
1939 |
return n; |
145 |
|
} |
146 |
|
} |
147 |
|
} |
148 |
393430 |
return Node::null(); |
149 |
|
} |
150 |
|
|
151 |
7 |
CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq(QuantifiersState& qs, |
152 |
|
TermRegistry& tr, |
153 |
7 |
Node mpat) |
154 |
7 |
: CandidateGenerator(qs, tr), d_match_pattern(mpat) |
155 |
|
{ |
156 |
7 |
Assert(d_match_pattern.getKind() == EQUAL); |
157 |
7 |
d_match_pattern_type = d_match_pattern[0].getType(); |
158 |
7 |
} |
159 |
|
|
160 |
34 |
void CandidateGeneratorQELitDeq::reset( Node eqc ){ |
161 |
34 |
eq::EqualityEngine* ee = d_qs.getEqualityEngine(); |
162 |
68 |
Node falset = NodeManager::currentNM()->mkConst(false); |
163 |
34 |
d_eqc_false = eq::EqClassIterator(falset, ee); |
164 |
34 |
} |
165 |
|
|
166 |
112 |
Node CandidateGeneratorQELitDeq::getNextCandidate(){ |
167 |
|
//get next candidate term in equivalence class |
168 |
169 |
while( !d_eqc_false.isFinished() ){ |
169 |
154 |
Node n = (*d_eqc_false); |
170 |
97 |
++d_eqc_false; |
171 |
97 |
if( n.getKind()==d_match_pattern.getKind() ){ |
172 |
252 |
if (n[0].getType().isComparableTo(d_match_pattern_type) |
173 |
252 |
&& isLegalCandidate(n)) |
174 |
|
{ |
175 |
|
//found an iff or equality, try to match it |
176 |
|
//DO_THIS: cache to avoid redundancies? |
177 |
|
//DO_THIS: do we need to try the symmetric equality for n? or will it also exist in the eq class of false? |
178 |
40 |
return n; |
179 |
|
} |
180 |
|
} |
181 |
|
} |
182 |
15 |
return Node::null(); |
183 |
|
} |
184 |
|
|
185 |
75 |
CandidateGeneratorQEAll::CandidateGeneratorQEAll(QuantifiersState& qs, |
186 |
|
TermRegistry& tr, |
187 |
75 |
Node mpat) |
188 |
75 |
: CandidateGenerator(qs, tr), d_match_pattern(mpat) |
189 |
|
{ |
190 |
75 |
d_match_pattern_type = mpat.getType(); |
191 |
75 |
Assert(mpat.getKind() == INST_CONSTANT); |
192 |
75 |
d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); |
193 |
75 |
d_index = mpat.getAttribute(InstVarNumAttribute()); |
194 |
75 |
d_firstTime = false; |
195 |
75 |
} |
196 |
|
|
197 |
185 |
void CandidateGeneratorQEAll::reset( Node eqc ) { |
198 |
185 |
d_eq = eq::EqClassesIterator(d_qs.getEqualityEngine()); |
199 |
185 |
d_firstTime = true; |
200 |
185 |
} |
201 |
|
|
202 |
295 |
Node CandidateGeneratorQEAll::getNextCandidate() { |
203 |
295 |
quantifiers::TermDb* tdb = d_treg.getTermDatabase(); |
204 |
4707 |
while( !d_eq.isFinished() ){ |
205 |
4600 |
TNode n = (*d_eq); |
206 |
2394 |
++d_eq; |
207 |
2394 |
if( n.getType().isComparableTo( d_match_pattern_type ) ){ |
208 |
188 |
TNode nh = tdb->getEligibleTermInEqc(n); |
209 |
188 |
if( !nh.isNull() ){ |
210 |
188 |
if (options::instMaxLevel() != -1) |
211 |
|
{ |
212 |
|
nh = d_treg.getModel()->getInternalRepresentative(nh, d_f, d_index); |
213 |
|
//don't consider this if already the instantiation is ineligible |
214 |
|
if (!nh.isNull() && !tdb->isTermEligibleForInstantiation(nh, d_f)) |
215 |
|
{ |
216 |
|
nh = Node::null(); |
217 |
|
} |
218 |
|
} |
219 |
188 |
if( !nh.isNull() ){ |
220 |
188 |
d_firstTime = false; |
221 |
|
//an equivalence class with the same type as the pattern, return it |
222 |
188 |
return nh; |
223 |
|
} |
224 |
|
} |
225 |
|
} |
226 |
|
} |
227 |
107 |
if( d_firstTime ){ |
228 |
|
//must return something |
229 |
24 |
d_firstTime = false; |
230 |
24 |
return d_treg.getTermForType(d_match_pattern_type); |
231 |
|
} |
232 |
83 |
return Node::null(); |
233 |
|
} |
234 |
|
|
235 |
3017 |
CandidateGeneratorConsExpand::CandidateGeneratorConsExpand(QuantifiersState& qs, |
236 |
|
TermRegistry& tr, |
237 |
3017 |
Node mpat) |
238 |
3017 |
: CandidateGeneratorQE(qs, tr, mpat) |
239 |
|
{ |
240 |
3017 |
Assert(mpat.getKind() == APPLY_CONSTRUCTOR); |
241 |
3017 |
d_mpat_type = mpat.getType(); |
242 |
3017 |
} |
243 |
|
|
244 |
4095 |
void CandidateGeneratorConsExpand::reset(Node eqc) |
245 |
|
{ |
246 |
4095 |
d_term_iter = 0; |
247 |
4095 |
if (eqc.isNull()) |
248 |
|
{ |
249 |
2065 |
d_mode = cand_term_db; |
250 |
|
} |
251 |
|
else |
252 |
|
{ |
253 |
2030 |
d_eqc = eqc; |
254 |
2030 |
d_mode = cand_term_ident; |
255 |
2030 |
Assert(d_eqc.getType() == d_mpat_type); |
256 |
|
} |
257 |
4095 |
} |
258 |
|
|
259 |
5100 |
Node CandidateGeneratorConsExpand::getNextCandidate() |
260 |
|
{ |
261 |
|
// get the next term from the base class |
262 |
10200 |
Node curr = getNextCandidateInternal(); |
263 |
5100 |
if (curr.isNull() || (curr.hasOperator() && curr.getOperator() == d_op)) |
264 |
|
{ |
265 |
3766 |
return curr; |
266 |
|
} |
267 |
|
// expand it |
268 |
1334 |
NodeManager* nm = NodeManager::currentNM(); |
269 |
2668 |
std::vector<Node> children; |
270 |
1334 |
const DType& dt = d_mpat_type.getDType(); |
271 |
1334 |
Assert(dt.getNumConstructors() == 1); |
272 |
1334 |
children.push_back(d_op); |
273 |
4034 |
for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++) |
274 |
|
{ |
275 |
|
Node sel = nm->mkNode( |
276 |
5400 |
APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr); |
277 |
2700 |
children.push_back(sel); |
278 |
|
} |
279 |
1334 |
return nm->mkNode(APPLY_CONSTRUCTOR, children); |
280 |
|
} |
281 |
|
|
282 |
2030 |
bool CandidateGeneratorConsExpand::isLegalOpCandidate(Node n) |
283 |
|
{ |
284 |
2030 |
return isLegalCandidate(n); |
285 |
|
} |
286 |
|
|
287 |
313 |
CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs, |
288 |
|
TermRegistry& tr, |
289 |
313 |
Node mpat) |
290 |
313 |
: CandidateGeneratorQE(qs, tr, mpat) |
291 |
|
{ |
292 |
313 |
Trace("sel-trigger") << "Selector trigger: " << mpat << std::endl; |
293 |
313 |
Assert(mpat.getKind() == APPLY_SELECTOR); |
294 |
|
// NOTE: could use qs.getValuation().getPreprocessedTerm(mpat); when |
295 |
|
// expand definitions is eliminated, however, this also requires avoiding |
296 |
|
// term formula removal. |
297 |
626 |
Node mpatExp = datatypes::DatatypesRewriter::expandApplySelector(mpat); |
298 |
313 |
Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl; |
299 |
313 |
if (mpatExp.getKind() == ITE) |
300 |
|
{ |
301 |
313 |
Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL); |
302 |
313 |
Assert(mpatExp[2].getKind() == APPLY_UF); |
303 |
313 |
d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]); |
304 |
313 |
d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]); |
305 |
|
} |
306 |
|
else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL) |
307 |
|
{ |
308 |
|
// corner case of datatype with one constructor |
309 |
|
d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp); |
310 |
|
} |
311 |
|
else |
312 |
|
{ |
313 |
|
// corner case of a wrongly applied selector as a trigger |
314 |
|
Assert(mpatExp.getKind() == APPLY_UF); |
315 |
|
d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp); |
316 |
|
} |
317 |
313 |
Assert(d_selOp != d_ufOp); |
318 |
313 |
} |
319 |
|
|
320 |
6574 |
void CandidateGeneratorSelector::reset(Node eqc) |
321 |
|
{ |
322 |
6574 |
Trace("sel-trigger-debug") << "Reset in eqc=" << eqc << std::endl; |
323 |
|
// start with d_selOp, if it exists |
324 |
6574 |
resetForOperator(eqc, !d_selOp.isNull()? d_selOp : d_ufOp); |
325 |
6574 |
} |
326 |
|
|
327 |
14990 |
Node CandidateGeneratorSelector::getNextCandidate() |
328 |
|
{ |
329 |
29980 |
Node nextc = getNextCandidateInternal(); |
330 |
14990 |
if (!nextc.isNull()) |
331 |
|
{ |
332 |
6721 |
Trace("sel-trigger-debug") << "...next candidate is " << nextc << std::endl; |
333 |
6721 |
return nextc; |
334 |
|
} |
335 |
8269 |
else if (d_op == d_selOp) |
336 |
|
{ |
337 |
4203 |
if (d_ufOp.isNull()) |
338 |
|
{ |
339 |
|
// corner case: selector cannot be wrongly applied (1-cons case) |
340 |
|
d_op = Node::null(); |
341 |
|
} |
342 |
|
else |
343 |
|
{ |
344 |
|
// finished correctly applied selectors, now try incorrectly applied ones |
345 |
4203 |
resetForOperator(d_eqc, d_ufOp); |
346 |
4203 |
return getNextCandidate(); |
347 |
|
} |
348 |
|
} |
349 |
4066 |
Trace("sel-trigger-debug") << "...finished" << std::endl; |
350 |
|
// no more candidates |
351 |
4066 |
return Node::null(); |
352 |
|
} |
353 |
|
|
354 |
|
} // namespace inst |
355 |
|
} // namespace quantifiers |
356 |
|
} // namespace theory |
357 |
31137 |
} // namespace cvc5 |