Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implements conflict-based instantiation (Reynolds et al FMCAD 2014).
11 : : */
12 : :
13 : : #include "theory/quantifiers/quant_conflict_find.h"
14 : :
15 : : #include "base/configuration.h"
16 : : #include "expr/node_algorithm.h"
17 : : #include "options/quantifiers_options.h"
18 : : #include "options/theory_options.h"
19 : : #include "options/uf_options.h"
20 : : #include "theory/quantifiers/ematching/trigger_term_info.h"
21 : : #include "theory/quantifiers/first_order_model.h"
22 : : #include "theory/quantifiers/instantiate.h"
23 : : #include "theory/quantifiers/quant_util.h"
24 : : #include "theory/quantifiers/term_database.h"
25 : : #include "theory/quantifiers/term_util.h"
26 : : #include "theory/rewriter.h"
27 : : #include "util/rational.h"
28 : :
29 : : using namespace cvc5::internal::kind;
30 : : using namespace std;
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace quantifiers {
35 : :
36 : 47541 : QuantInfo::QuantInfo(Env& env,
37 : : QuantifiersState& qs,
38 : : TermRegistry& tr,
39 : : QuantConflictFind* p,
40 : 47541 : Node q)
41 : : : EnvObj(env),
42 : 47541 : d_qs(qs),
43 : 47541 : d_parent(p),
44 : 47541 : d_instMatch(env, qs, tr, q),
45 : 47541 : d_mg(nullptr),
46 : 47541 : d_q(q),
47 : 47541 : d_unassigned_nvar(0),
48 : 95082 : d_una_index(0)
49 : : {
50 : 47541 : Node qn = d_q[1];
51 : 47541 : d_extra_var.clear();
52 : :
53 : : // register the variables
54 [ + + ]: 154613 : for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++)
55 : : {
56 : 107072 : Node v = d_q[0][i];
57 : 107072 : d_match.push_back(TNode::null());
58 : 107072 : d_match_term.push_back(TNode::null());
59 : 107072 : d_var_num[v] = i;
60 : 107072 : d_vars.push_back(v);
61 : 107072 : d_var_types.push_back(v.getType());
62 : 107072 : }
63 : :
64 : 47541 : registerNode(qn, true, true);
65 : :
66 [ + - ]: 47541 : Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
67 : 47541 : d_mg = std::make_unique<MatchGen>(d_env, p, this, qn);
68 : :
69 [ + + ]: 47541 : if (d_mg->isValid())
70 : : {
71 [ + + ]: 215239 : for (size_t j = q[0].getNumChildren(), nvars = d_vars.size(); j < nvars;
72 : : j++)
73 : : {
74 [ + + ]: 178557 : if (d_vars[j].getKind() != Kind::BOUND_VARIABLE)
75 : : {
76 : 165904 : d_var_mg[j] = nullptr;
77 : 165904 : bool is_tsym = false;
78 [ + + ][ - - ]: 331808 : if (!MatchGen::isHandledUfTerm(d_vars[j])
79 [ + + ][ + + ]: 331808 : && d_vars[j].getKind() != Kind::ITE)
[ + - ]
80 : : {
81 : 1769 : is_tsym = true;
82 : 1769 : d_tsym_vars.push_back(j);
83 : : }
84 [ + + ][ + + ]: 165904 : if (!is_tsym || options().quantifiers.cbqiTConstraint)
[ + + ]
85 : : {
86 : 164856 : d_var_mg[j] =
87 : 329712 : std::make_unique<MatchGen>(d_env, p, this, d_vars[j], true);
88 : : }
89 [ + + ][ + + ]: 165904 : if (!d_var_mg[j] || !d_var_mg[j]->isValid())
[ + + ]
90 : : {
91 [ + - ]: 9870 : Trace("qcf-invalid")
92 : 4935 : << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
93 : 4935 : d_mg->setInvalid();
94 : 4935 : break;
95 : : }
96 : : else
97 : : {
98 : 160969 : std::vector<size_t> bvars;
99 : 160969 : d_var_mg[j]->determineVariableOrder(bvars);
100 : 160969 : }
101 : : }
102 : : }
103 [ + + ]: 41617 : if (d_mg->isValid())
104 : : {
105 : 36682 : std::vector<size_t> bvars;
106 : 36682 : d_mg->determineVariableOrder(bvars);
107 : 36682 : }
108 : : }
109 : : else
110 : : {
111 [ + - ]: 11848 : Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed."
112 : 5924 : << std::endl;
113 : : }
114 [ + - ]: 95082 : Trace("qcf-qregister-summary")
115 [ - - ]: 47541 : << "QCF register : " << (d_mg->isValid() ? "VALID " : "INVALID") << " : "
116 : 47541 : << q << std::endl;
117 : :
118 [ + + ]: 47541 : if (d_mg->isValid())
119 : : {
120 : : // optimization : record variable argument positions for terms that must be
121 : : // matched
122 : 36682 : std::vector<TNode> vars;
123 : : // TODO: revisit this, makes QCF faster, but misses conflicts due to caring
124 : : // about paths that may not be relevant (starExec jobs 14136/14137)
125 [ - + ]: 36682 : if (options().quantifiers.cbqiSkipRd)
126 : : {
127 [ - - ]: 0 : for (unsigned j = q[0].getNumChildren(); j < d_vars.size(); j++)
128 : : {
129 : 0 : vars.push_back(d_vars[j]);
130 : : }
131 : : }
132 : : else
133 : : {
134 : : // get all variables that are always relevant
135 : 36682 : std::map<TNode, bool> visited;
136 : 36682 : getPropagateVars(vars, q[1], false, visited);
137 : 36682 : }
138 [ + + ]: 199944 : for (TNode v : vars)
139 : : {
140 : 326524 : TNode f = p->getTermDatabase()->getMatchOperator(v);
141 [ + + ]: 163262 : if (!f.isNull())
142 : : {
143 [ + - ]: 197232 : Trace("qcf-opt") << "Record variable argument positions in " << v
144 : 98616 : << ", op=" << f << "..." << std::endl;
145 [ + + ]: 321512 : for (size_t k = 0, vnchild = v.getNumChildren(); k < vnchild; k++)
146 : : {
147 : 222896 : Node n = v[k];
148 : 222896 : std::map<TNode, size_t>::iterator itv = d_var_num.find(n);
149 [ + + ]: 222896 : if (itv != d_var_num.end())
150 : : {
151 : 191441 : std::vector<size_t>& vrd = d_var_rel_dom[itv->second][f];
152 [ + - ]: 382882 : Trace("qcf-opt")
153 : 191441 : << " arg " << k << " is var #" << itv->second << std::endl;
154 [ + + ]: 191441 : if (std::find(vrd.begin(), vrd.end(), k) == vrd.end())
155 : : {
156 : 179914 : vrd.push_back(k);
157 : : }
158 : : }
159 : 222896 : }
160 : : }
161 : 163262 : }
162 : 36682 : }
163 : 47541 : }
164 : :
165 : 95082 : QuantInfo::~QuantInfo() {}
166 : :
167 : 2850075 : Node QuantInfo::getQuantifiedFormula() const { return d_q; }
168 : :
169 : 0 : QuantifiersInferenceManager& QuantInfo::getInferenceManager()
170 : : {
171 : 0 : Assert(d_parent != nullptr);
172 : 0 : return d_parent->getInferenceManager();
173 : : }
174 : :
175 : 421483 : void QuantInfo::getPropagateVars(std::vector<TNode>& vars,
176 : : TNode n,
177 : : bool pol,
178 : : std::map<TNode, bool>& visited)
179 : : {
180 : 421483 : std::map<TNode, bool>::iterator itv = visited.find(n);
181 [ + + ]: 421483 : if (itv == visited.end())
182 : : {
183 : 310435 : visited[n] = true;
184 : 310435 : bool rec = true;
185 : 310435 : bool newPol = pol;
186 [ + + ]: 310435 : if (d_var_num.find(n) != d_var_num.end())
187 : : {
188 [ - + ][ - + ]: 163262 : Assert(std::find(vars.begin(), vars.end(), n) == vars.end());
[ - - ]
189 : 163262 : vars.push_back(n);
190 : 326524 : TNode f = d_parent->getTermDatabase()->getMatchOperator(n);
191 [ + + ]: 163262 : if (!f.isNull())
192 : : {
193 : 98616 : std::vector<Node>& rd = d_parent->d_func_rel_dom[f];
194 [ + + ]: 98616 : if (std::find(rd.begin(), rd.end(), d_q) == rd.end())
195 : : {
196 : 75384 : rd.push_back(d_q);
197 : : }
198 : : }
199 : 163262 : }
200 [ + + ]: 147173 : else if (MatchGen::isHandledBoolConnective(n))
201 : : {
202 [ - + ][ - + ]: 59777 : Assert(n.getKind() != Kind::IMPLIES);
[ - - ]
203 : 59777 : QuantPhaseReq::getEntailPolarity(n, 0, true, pol, rec, newPol);
204 : : }
205 [ + - ]: 620870 : Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol
206 : 310435 : << ", rec = " << rec << std::endl;
207 [ + + ]: 310435 : if (rec)
208 : : {
209 [ + + ]: 681340 : for (const Node& nc : n)
210 : : {
211 : 384801 : getPropagateVars(vars, nc, pol, visited);
212 : 384801 : }
213 : : }
214 : : }
215 : 421483 : }
216 : :
217 : 4244339 : bool QuantInfo::isBaseMatchComplete()
218 : : {
219 : 4244339 : return d_vars_set.size() == (d_q[0].getNumChildren() + d_extra_var.size());
220 : : }
221 : :
222 : 249132 : void QuantInfo::registerNode(Node n, bool hasPol, bool pol, bool beneathQuant)
223 : : {
224 [ + - ]: 249132 : Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
225 [ + + ]: 249132 : if (n.getKind() == Kind::FORALL)
226 : : {
227 : 11519 : registerNode(n[1], hasPol, pol, true);
228 : : }
229 : : else
230 : : {
231 [ + + ]: 237613 : if (!MatchGen::isHandledBoolConnective(n))
232 : : {
233 [ + + ]: 130551 : if (expr::hasBoundVar(n))
234 : : {
235 : : // literals
236 [ + + ]: 130202 : if (n.getKind() == Kind::EQUAL)
237 : : {
238 [ + + ]: 205203 : for (unsigned i = 0; i < n.getNumChildren(); i++)
239 : : {
240 : 136802 : flatten(n[i], beneathQuant);
241 : : }
242 : : }
243 [ + + ]: 61801 : else if (MatchGen::isHandledUfTerm(n))
244 : : {
245 : 43907 : flatten(n, beneathQuant);
246 : : }
247 [ + + ]: 17894 : else if (n.getKind() == Kind::ITE)
248 : : {
249 [ + + ]: 10488 : for (unsigned i = 1; i <= 2; i++)
250 : : {
251 : 6992 : flatten(n[i], beneathQuant);
252 : : }
253 : 3496 : registerNode(n[0], false, pol, beneathQuant);
254 : : }
255 [ + + ]: 14398 : else if (options().quantifiers.cbqiTConstraint)
256 : : {
257 : : // a theory-specific predicate
258 [ + + ]: 1944 : for (unsigned i = 0; i < n.getNumChildren(); i++)
259 : : {
260 : 1296 : flatten(n[i], beneathQuant);
261 : : }
262 : : }
263 : : }
264 : : }
265 : : else
266 : : {
267 [ + + ]: 290142 : for (unsigned i = 0; i < n.getNumChildren(); i++)
268 : : {
269 : : bool newHasPol;
270 : : bool newPol;
271 : 183080 : QuantPhaseReq::getPolarity(n, i, hasPol, pol, newHasPol, newPol);
272 : 183080 : registerNode(n[i], newHasPol, newPol, beneathQuant);
273 : : }
274 : : }
275 : : }
276 : 249132 : }
277 : :
278 : 597907 : void QuantInfo::flatten(Node n, bool beneathQuant)
279 : : {
280 [ + - ]: 597907 : Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
281 [ + + ]: 597907 : if (expr::hasBoundVar(n))
282 : : {
283 [ + + ]: 500677 : if (d_var_num.find(n) == d_var_num.end())
284 : : {
285 [ + - ]: 216792 : Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
286 : 216792 : d_var_num[n] = d_vars.size();
287 : 216792 : d_vars.push_back(n);
288 : 216792 : d_var_types.push_back(n.getType());
289 : 216792 : d_match.push_back(TNode::null());
290 : 216792 : d_match_term.push_back(TNode::null());
291 [ + + ]: 216792 : if (n.getKind() == Kind::ITE)
292 : : {
293 : 3496 : registerNode(n, false, false);
294 : : }
295 [ + + ]: 213296 : else if (n.getKind() == Kind::BOUND_VARIABLE)
296 : : {
297 : 14618 : d_extra_var.push_back(n);
298 : : }
299 : : else
300 : : {
301 [ + + ]: 607588 : for (unsigned i = 0; i < n.getNumChildren(); i++)
302 : : {
303 : 408910 : flatten(n[i], beneathQuant);
304 : : }
305 : : }
306 : : }
307 : : else
308 : : {
309 [ + - ]: 283885 : Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
310 : : }
311 : : }
312 : : else
313 : : {
314 [ + - ]: 97230 : Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
315 : : }
316 : 597907 : }
317 : :
318 : 2830517 : int QuantInfo::getVarNum(TNode v) const
319 : : {
320 : 2830517 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(v);
321 [ + + ]: 2830517 : return it != d_var_num.end() ? static_cast<int>(it->second) : -1;
322 : : }
323 : :
324 : 269046 : bool QuantInfo::reset_round()
325 : : {
326 [ + + ]: 2157224 : for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
327 : : {
328 : 1888178 : d_match[i] = TNode::null();
329 : 1888178 : d_match_term[i] = TNode::null();
330 : : }
331 : 269046 : d_instMatch.resetAll();
332 : 269046 : ieval::TermEvaluatorMode tev = d_parent->atConflictEffort()
333 [ + + ]: 269046 : ? ieval::TermEvaluatorMode::CONFLICT
334 : 269046 : : ieval::TermEvaluatorMode::PROP;
335 : 269046 : d_instMatch.setEvaluatorMode(tev);
336 : 269046 : d_vars_set.clear();
337 : 269046 : d_curr_var_deq.clear();
338 : 269046 : d_tconstraints.clear();
339 : :
340 : 269046 : d_mg->reset_round();
341 [ + + ]: 1399779 : for (const std::pair<const size_t, std::unique_ptr<MatchGen>>& vg : d_var_mg)
342 : : {
343 [ - + ]: 1130733 : if (!vg.second->reset_round())
344 : : {
345 : 0 : return false;
346 : : }
347 : : }
348 : : // now, reset for matching
349 : 269046 : d_mg->reset(false);
350 : 269046 : return true;
351 : : }
352 : :
353 : 14036250 : size_t QuantInfo::getCurrentRepVar(size_t v)
354 : : {
355 [ - + ][ - + ]: 14036250 : Assert(v < d_match.size());
[ - - ]
356 : 14036250 : TNode m = d_match[v];
357 [ + + ]: 14036250 : if (!m.isNull())
358 : : {
359 : 7695692 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(m);
360 [ + + ]: 7695692 : if (it != d_var_num.end())
361 : : {
362 : 40907 : return getCurrentRepVar(it->second);
363 : : }
364 : : }
365 : 13995343 : return v;
366 : 14036250 : }
367 : :
368 : 6531214 : TNode QuantInfo::getCurrentValue(TNode n)
369 : : {
370 : 6531214 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(n);
371 [ + + ]: 6531214 : if (it == d_var_num.end())
372 : : {
373 : 1936213 : return n;
374 : : }
375 : 4595001 : Node m = d_match[it->second];
376 [ + + ]: 4595001 : if (m.isNull())
377 : : {
378 : 4335571 : return n;
379 : : }
380 : 259430 : return getCurrentValue(m);
381 : 4595001 : }
382 : :
383 : 70 : TNode QuantInfo::getCurrentExpValue(TNode n)
384 : : {
385 : 70 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(n);
386 [ - + ]: 70 : if (it == d_var_num.end())
387 : : {
388 : 0 : return n;
389 : : }
390 : 70 : Node m = d_match[it->second];
391 [ - + ]: 70 : if (m.isNull())
392 : : {
393 : 0 : return n;
394 : : }
395 [ - + ][ - + ]: 70 : Assert(m != n);
[ - - ]
396 : 70 : Node mt = d_match_term[it->second];
397 [ - + ]: 70 : if (mt.isNull())
398 : : {
399 : 0 : return getCurrentValue(m);
400 : : }
401 : 70 : return mt;
402 : 70 : }
403 : :
404 : 12631392 : bool QuantInfo::getCurrentCanBeEqual(size_t v, TNode n, bool chDiseq)
405 : : {
406 : : // check disequalities
407 : : std::map<size_t, std::map<TNode, size_t>>::iterator itd =
408 : 12631392 : d_curr_var_deq.find(v);
409 [ + + ]: 12631392 : if (itd == d_curr_var_deq.end())
410 : : {
411 : 8135721 : return true;
412 : : }
413 [ + + ]: 8788237 : for (std::pair<const TNode, size_t>& dd : itd->second)
414 : : {
415 : 8831766 : Node cv = getCurrentValue(dd.first);
416 [ + - ]: 4415883 : Trace("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
417 [ + + ]: 4415883 : if (cv == n)
418 : : {
419 : 123242 : return false;
420 : : }
421 : 4292641 : else if (chDiseq && !isVar(n) && !isVar(cv))
422 : : {
423 : : // they must actually be disequal if we are looking for conflicts
424 [ + + ]: 1117 : if (!d_qs.areDisequal(n, cv))
425 : : {
426 : : // TODO : check for entailed disequal
427 : 75 : return false;
428 : : }
429 : : }
430 [ + + ]: 4415883 : }
431 : :
432 : 4372354 : return true;
433 : : }
434 : :
435 : 0 : int QuantInfo::addConstraint(size_t v, TNode n, bool polarity)
436 : : {
437 : 0 : v = getCurrentRepVar(v);
438 : 0 : int vn = getVarNum(n);
439 [ - - ]: 0 : if (vn != -1)
440 : : {
441 : 0 : vn = static_cast<int>(getCurrentRepVar(static_cast<size_t>(vn)));
442 : : }
443 : 0 : n = getCurrentValue(n);
444 : 0 : return addConstraint(v, n, vn, polarity, false);
445 : : }
446 : :
447 : 1430946 : int QuantInfo::addConstraint(
448 : : size_t v, TNode n, int vn, bool polarity, bool doRemove)
449 : : {
450 [ - + ][ - + ]: 1430946 : Assert(v < d_match.size());
[ - - ]
451 : : // for handling equalities between variables, and disequalities involving
452 : : // variables
453 [ + - ][ - - ]: 2861892 : Trace("qcf-match-debug") << "- " << (doRemove ? "un" : "")
454 : 0 : << "constrain : " << v << " -> " << n
455 : 1430946 : << " (cv=" << getCurrentValue(n) << ")";
456 [ + - ]: 2861892 : Trace("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity
457 : 1430946 : << std::endl;
458 : 1430946 : Assert(doRemove || n == getCurrentValue(n));
459 [ + + ][ + - ]: 1430946 : Assert(doRemove || v == getCurrentRepVar(v));
[ - + ][ - + ]
[ - - ]
460 : 1430946 : Assert(doRemove || (vn == -1 && getVarNum(n) == -1)
461 : : || (vn >= 0
462 : : && static_cast<size_t>(vn)
463 : : == getCurrentRepVar(static_cast<size_t>(getVarNum(n)))));
464 [ + + ]: 1430946 : if (polarity)
465 : : {
466 [ + - ]: 992779 : if (vn != static_cast<int>(v))
467 : : {
468 [ + + ]: 992779 : if (doRemove)
469 : : {
470 [ + + ]: 481392 : if (vn != -1)
471 : : {
472 : : // if set to this in the opposite direction, clean up opposite instead
473 : : // std::map< int, TNode >::iterator itmn = d_match.find( vn
474 : : // );
475 [ - + ]: 31070 : if (d_match[vn] == d_vars[v])
476 : : {
477 : 0 : return addConstraint(vn, d_vars[v], v, true, true);
478 : : }
479 : : else
480 : : {
481 : : // unsetting variables equal
482 : : std::map<size_t, std::map<TNode, size_t>>::iterator itd =
483 : 31070 : d_curr_var_deq.find(vn);
484 [ + + ]: 31070 : if (itd != d_curr_var_deq.end())
485 : : {
486 : : // remove disequalities owned by this
487 : 12079 : std::vector<TNode> remDeq;
488 [ + + ]: 12518 : for (const std::pair<const TNode, size_t>& dd : itd->second)
489 : : {
490 [ + - ]: 439 : if (dd.second == v)
491 : : {
492 : 439 : remDeq.push_back(dd.first);
493 : : }
494 : : }
495 [ + + ]: 12518 : for (TNode rd : remDeq)
496 : : {
497 : 439 : itd->second.erase(rd);
498 : 439 : }
499 : 12079 : }
500 : : }
501 : : }
502 : 481392 : unsetMatch(v);
503 : 481392 : return 1;
504 : : }
505 : : else
506 : : {
507 : 511387 : bool isGroundRep = false;
508 : 511387 : bool isGround = false;
509 [ + + ]: 511387 : if (vn != -1)
510 : : {
511 [ + - ]: 63044 : Trace("qcf-match-debug")
512 : 31522 : << " ...Variable bound to variable" << std::endl;
513 [ + - ]: 31522 : if (d_match[v].isNull())
514 : : {
515 : : // setting variables equal
516 : 31522 : bool alreadySet = false;
517 [ - + ]: 31522 : if (!d_match[vn].isNull())
518 : : {
519 : 0 : alreadySet = true;
520 : 0 : Assert(!isVar(d_match[vn]));
521 : : }
522 : :
523 : : // copy or check disequalities
524 : : std::map<size_t, std::map<TNode, size_t>>::iterator itd =
525 : 31522 : d_curr_var_deq.find(v);
526 [ + + ]: 31522 : if (itd != d_curr_var_deq.end())
527 : : {
528 : 12094 : std::map<TNode, size_t>& cvd = d_curr_var_deq[vn];
529 [ + + ]: 12533 : for (const std::pair<const TNode, size_t>& dd : itd->second)
530 : : {
531 : 878 : Node dv = getCurrentValue(dd.first);
532 [ + - ]: 439 : if (!alreadySet)
533 : : {
534 [ + - ]: 439 : if (cvd.find(dv) == cvd.end())
535 : : {
536 : 439 : cvd[dv] = v;
537 : : }
538 : : }
539 [ - - ]: 0 : else if (d_match[vn] == dv)
540 : : {
541 [ - - ]: 0 : Trace("qcf-match-debug")
542 : 0 : << " -> fail, conflicting disequality" << std::endl;
543 : 0 : return -1;
544 : : }
545 [ + - ]: 439 : }
546 : : }
547 [ - + ]: 31522 : if (alreadySet)
548 : : {
549 : 0 : n = getCurrentValue(n);
550 : : }
551 : : }
552 : : else
553 : : {
554 [ - - ]: 0 : if (d_match[vn].isNull())
555 : : {
556 [ - - ]: 0 : Trace("qcf-match-debug") << " ...Reverse direction" << std::endl;
557 : : // set the opposite direction
558 : 0 : return addConstraint(vn, d_vars[v], v, true, false);
559 : : }
560 : : else
561 : : {
562 [ - - ]: 0 : Trace("qcf-match-debug")
563 : 0 : << " -> Both variables bound, compare" << std::endl;
564 : : // are they currently equal
565 [ - - ]: 0 : return d_match[v] == d_match[vn] ? 0 : -1;
566 : : }
567 : : }
568 : : }
569 : : else
570 : : {
571 [ + - ]: 959730 : Trace("qcf-match-debug")
572 : 479865 : << " ...Variable bound to ground" << std::endl;
573 [ + - ]: 479865 : if (d_match[v].isNull())
574 : : {
575 : : // isGroundRep = true; ??
576 : 479865 : isGround = true;
577 : : }
578 : : else
579 : : {
580 : : // compare ground values
581 [ - - ]: 0 : Trace("qcf-match-debug") << " -> Ground value, compare "
582 : 0 : << d_match[v] << " " << n << std::endl;
583 [ - - ]: 0 : return d_match[v] == n ? 0 : -1;
584 : : }
585 : : }
586 [ + + ]: 511387 : if (setMatch(v, n, isGroundRep, isGround))
587 : : {
588 [ + - ]: 485990 : Trace("qcf-match-debug") << " -> success" << std::endl;
589 : 485990 : return 1;
590 : : }
591 : : else
592 : : {
593 [ + - ]: 50794 : Trace("qcf-match-debug")
594 : 25397 : << " -> fail, conflicting disequality" << std::endl;
595 : 25397 : return -1;
596 : : }
597 : : }
598 : : }
599 : : else
600 : : {
601 [ - - ]: 0 : Trace("qcf-match-debug")
602 : 0 : << " -> redundant, variable identity" << std::endl;
603 : 0 : return 0;
604 : : }
605 : : }
606 : : else
607 : : {
608 [ - + ]: 438167 : if (vn == static_cast<int>(v))
609 : : {
610 [ - - ]: 0 : Trace("qcf-match-debug") << " -> fail, variable identity" << std::endl;
611 : 0 : return -1;
612 : : }
613 : : else
614 : : {
615 [ + + ]: 438167 : if (doRemove)
616 : : {
617 [ - + ][ - + ]: 218115 : Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end());
[ - - ]
618 : 218115 : d_curr_var_deq[v].erase(n);
619 : 218115 : return 1;
620 : : }
621 : : else
622 : : {
623 [ + + ]: 220052 : if (d_curr_var_deq[v].find(n) == d_curr_var_deq[v].end())
624 : : {
625 : : // check if it respects equality
626 [ - + ]: 219590 : if (!d_match[v].isNull())
627 : : {
628 : 0 : TNode nv = getCurrentValue(n);
629 [ - - ]: 0 : if (nv == d_match[v])
630 : : {
631 [ - - ]: 0 : Trace("qcf-match-debug")
632 : 0 : << " -> fail, conflicting disequality" << std::endl;
633 : 0 : return -1;
634 : : }
635 [ - - ]: 0 : }
636 : 219590 : d_curr_var_deq[v][n] = v;
637 [ + - ]: 219590 : Trace("qcf-match-debug") << " -> success" << std::endl;
638 : 219590 : return 1;
639 : : }
640 : : else
641 : : {
642 [ + - ]: 462 : Trace("qcf-match-debug") << " -> redundant disequality" << std::endl;
643 : 462 : return 0;
644 : : }
645 : : }
646 : : }
647 : : }
648 : : }
649 : :
650 : 160 : bool QuantInfo::isConstrainedVar(size_t v)
651 : : {
652 : : std::map<size_t, std::map<TNode, size_t>>::const_iterator it =
653 : 160 : d_curr_var_deq.find(v);
654 [ + + ][ - + ]: 160 : if (it != d_curr_var_deq.end() && !it->second.empty())
[ - + ]
655 : : {
656 : 0 : return true;
657 : : }
658 : 160 : TNode vv = getVar(v);
659 [ - + ]: 160 : if (std::find(d_match.begin(), d_match.end(), vv) != d_match.end())
660 : : {
661 : 0 : return true;
662 : : }
663 : 160 : for (const std::pair<const size_t, std::map<TNode, size_t>>& d :
664 [ + + ]: 404 : d_curr_var_deq)
665 : : {
666 [ + + ]: 116 : for (const std::pair<const TNode, size_t>& dd : d.second)
667 : : {
668 [ - + ]: 32 : if (dd.first == vv)
669 : : {
670 : 0 : return true;
671 : : }
672 : : }
673 : : }
674 : 160 : return false;
675 : 160 : }
676 : :
677 : 12463363 : bool QuantInfo::setMatch(size_t v, TNode n, bool isGroundRep, bool isGround)
678 : : {
679 [ + + ]: 12463363 : if (!getCurrentCanBeEqual(v, n))
680 : : {
681 : 119037 : return false;
682 : : }
683 [ + + ]: 12344326 : if (isGroundRep)
684 : : {
685 : : // fail if n does not exist in the relevant domain of each of the argument
686 : : // positions
687 : : std::map<size_t, std::map<TNode, std::vector<size_t>>>::iterator it =
688 : 11830322 : d_var_rel_dom.find(v);
689 [ + + ]: 11830322 : if (it != d_var_rel_dom.end())
690 : : {
691 : 6065514 : TermDb* tdb = d_parent->getTermDatabase();
692 [ + + ]: 13619478 : for (std::pair<const TNode, std::vector<size_t>>& rd : it->second)
693 : : {
694 [ + + ]: 16131523 : for (size_t index : rd.second)
695 : : {
696 [ + - ]: 17155118 : Trace("qcf-match-debug2") << n << " in relevant domain " << rd.first
697 : 8577559 : << "." << index << "?" << std::endl;
698 [ + + ]: 8577559 : if (!tdb->inRelevantDomain(rd.first, index, n))
699 : : {
700 [ + - ]: 845422 : Trace("qcf-match-debug")
701 : 0 : << " -> fail, since " << n << " is not in relevant domain of "
702 : 422711 : << rd.first << "." << index << std::endl;
703 : 422711 : return false;
704 : : }
705 : : }
706 : : }
707 : : }
708 : : }
709 [ + - ]: 23843230 : Trace("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked "
710 : 11921615 : << d_curr_var_deq[v].size() << " disequalities"
711 : 11921615 : << std::endl;
712 [ + + ][ + + ]: 11921615 : if (isGround && d_vars[v].getKind() == Kind::BOUND_VARIABLE)
[ + + ]
713 : : {
714 : : // Set the inst match object if this corresponds to an original variable
715 [ + + ]: 4381977 : if (v < d_q[0].getNumChildren())
716 : : {
717 : : // we overwrite, so we must reset/set here
718 [ + + ]: 4378418 : if (!d_instMatch.get(v).isNull())
719 : : {
720 : 457571 : d_instMatch.reset(v);
721 : : }
722 [ + + ]: 4378418 : if (!d_instMatch.set(v, n))
723 : : {
724 : 2987894 : return false;
725 : : }
726 : : }
727 : 1394083 : d_vars_set.insert(v);
728 [ + - ]: 2788166 : Trace("qcf-match-debug")
729 : 0 : << "---- now bound " << d_vars_set.size() << " / "
730 [ - + ][ - - ]: 1394083 : << d_q[0].getNumChildren() << " base variables." << std::endl;
731 : : }
732 : : // Note that assigning to a variable that an original variable is equal to
733 : : // should trigger the match object. For example, if we have auxiliary
734 : : // variable k and original variable x where x <-> k currently, and we set
735 : : // k -> t, then we should notify the match object that x -> t. However,
736 : : // this is not done, as it would require more complex bookkeeping. Overall,
737 : : // this means that we may fail in some rare cases to eagerly recognize when a
738 : : // substitution is entailed.
739 : 8933721 : d_match[v] = n;
740 : 8933721 : return true;
741 : : }
742 : :
743 : 7451318 : void QuantInfo::unsetMatch(size_t v)
744 : : {
745 [ + - ]: 7451318 : Trace("qcf-match-debug") << "-- unbind : " << v << std::endl;
746 : 7451318 : if (d_vars[v].getKind() == Kind::BOUND_VARIABLE
747 [ + + ][ + + ]: 7451318 : && d_vars_set.find(v) != d_vars_set.end())
[ + + ]
748 : : {
749 : 934458 : d_vars_set.erase(v);
750 : : // Reset the inst match object if this corresponds to an original variable
751 [ + + ]: 934458 : if (v < d_q[0].getNumChildren())
752 : : {
753 [ + + ]: 931886 : if (!d_instMatch.get(v).isNull())
754 : : {
755 : 925174 : d_instMatch.reset(v);
756 : : }
757 : : }
758 : : }
759 : 7451318 : d_match[v] = TNode::null();
760 : 7451318 : }
761 : :
762 : 36101 : bool QuantInfo::isMatchSpurious()
763 : : {
764 [ + + ]: 259565 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
765 : : {
766 [ + + ]: 227744 : if (!d_match[i].isNull())
767 : : {
768 [ + + ]: 168029 : if (!getCurrentCanBeEqual(i, d_match[i], d_parent->atConflictEffort()))
769 : : {
770 : 4280 : return true;
771 : : }
772 : : }
773 : : }
774 : 31821 : return false;
775 : : }
776 : :
777 : 30580 : bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
778 : : {
779 [ + + ]: 30580 : if (options().quantifiers.ievalMode != options::IevalMode::OFF)
780 : : {
781 : : // We rely on the instantiation evaluator. When the instantiation evaluator
782 : : // is enabled, this method (almost) always returns false. The code may
783 : : // return true based on minor differences in the entailment tests, which
784 : : // would allow us in very rare cases to recognize when an instantiation
785 : : // is spurious.
786 : 6757 : return false;
787 : : }
788 : 23823 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
789 : : // check whether the instantiation evaluates as expected
790 : 23823 : std::map<TNode, TNode> subs;
791 [ + + ]: 94526 : for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
792 : : {
793 [ + - ]: 70703 : Trace("qcf-instance-check") << " " << terms[i] << std::endl;
794 : 70703 : subs[d_q[0][i]] = terms[i];
795 : : }
796 [ + + ]: 23893 : for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++)
797 : : {
798 : 140 : Node n = getCurrentExpValue(d_extra_var[i]);
799 [ + - ]: 140 : Trace("qcf-instance-check")
800 : 70 : << " " << d_extra_var[i] << " -> " << n << std::endl;
801 : 70 : subs[d_extra_var[i]] = n;
802 : 70 : }
803 [ + + ]: 23823 : if (d_parent->atConflictEffort())
804 : : {
805 [ + - ]: 33926 : Trace("qcf-instance-check")
806 : 16963 : << "Possible conflict instance for " << d_q << " : " << std::endl;
807 [ + + ]: 16963 : if (!echeck->isEntailed(d_q[1], subs, false, false))
808 : : {
809 [ + - ]: 33866 : Trace("qcf-instance-check")
810 : 16933 : << "...not entailed to be false." << std::endl;
811 : 16933 : return true;
812 : : }
813 : : }
814 : : else
815 : : {
816 : : // see if the body of the quantified formula evaluates to a Boolean
817 : : // combination of known terms under the current substitution. We use
818 : : // the helper method evaluateTerm from the entailment check utility.
819 : : Node inst_eval = echeck->evaluateTerm(
820 : 13720 : d_q[1], subs, false, options().quantifiers.cbqiTConstraint, true);
821 [ - + ]: 6860 : if (TraceIsOn("qcf-instance-check"))
822 : : {
823 [ - - ]: 0 : Trace("qcf-instance-check")
824 : 0 : << "Possible propagating instance for " << d_q << " : " << std::endl;
825 [ - - ]: 0 : Trace("qcf-instance-check") << " " << terms << std::endl;
826 [ - - ]: 0 : Trace("qcf-instance-check")
827 : 0 : << "...evaluates to " << inst_eval << std::endl;
828 : : }
829 : : // If it is the case that instantiation can be rewritten to a Boolean
830 : : // combination of terms that exist in the current context, then inst_eval
831 : : // is non-null. Moreover, we insist that inst_eval is not true, or else
832 : : // the instantiation is trivially entailed and hence is spurious.
833 : 6860 : if (inst_eval.isNull()
834 [ + + ][ + + ]: 6860 : || (inst_eval.isConst() && inst_eval.getConst<bool>()))
[ + + ][ + + ]
835 : : {
836 [ + - ]: 6753 : Trace("qcf-instance-check") << "...spurious." << std::endl;
837 : 6753 : return true;
838 : : }
839 : : else
840 : : {
841 [ + - ]: 107 : if (Configuration::isDebugBuild())
842 : : {
843 [ - + ]: 107 : if (!d_parent->isPropagatingInstance(inst_eval))
844 : : {
845 : : // Notice that this can happen in cases where:
846 : : // (1) x = -1*y is rewritten to y = -1*x, and
847 : : // (2) -1*y is a term in the master equality engine but -1*x is not.
848 : : // In other words, we determined that x = -1*y is a relevant
849 : : // equality to propagate since it involves two known terms, but
850 : : // after rewriting, the equality y = -1*x involves an unknown term
851 : : // -1*x. In this case, the equality is still relevant to propagate,
852 : : // despite the above function not being precise enough to realize
853 : : // it. We output a warning in debug for this. See #2993.
854 [ - - ]: 0 : Trace("qcf-instance-check")
855 : 0 : << "WARNING: not propagating." << std::endl;
856 : : }
857 : : }
858 [ + - ]: 107 : Trace("qcf-instance-check") << "...not spurious." << std::endl;
859 : : }
860 [ + + ]: 6860 : }
861 [ - + ]: 137 : if (!d_tconstraints.empty())
862 : : {
863 : : // check constraints
864 : 0 : QuantifiersRegistry& qr = d_parent->getQuantifiersRegistry();
865 : 0 : for (std::map<Node, bool>::iterator it = d_tconstraints.begin();
866 [ - - ]: 0 : it != d_tconstraints.end();
867 : 0 : ++it)
868 : : {
869 : : // apply substitution to the tconstraint
870 : 0 : Node cons = qr.substituteBoundVariables(it->first, d_q, terms);
871 [ - - ]: 0 : cons = it->second ? cons : cons.negate();
872 [ - - ]: 0 : if (!entailmentTest(cons, d_parent->atConflictEffort()))
873 : : {
874 : 0 : return true;
875 : : }
876 [ - - ]: 0 : }
877 : : }
878 : : // spurious if quantifiers engine is in conflict
879 : 137 : return d_parent->d_qstate.isInConflict();
880 : 23823 : }
881 : :
882 : 0 : bool QuantInfo::entailmentTest(Node lit, bool chEnt)
883 : : {
884 [ - - ]: 0 : Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
885 : 0 : Node rew = rewrite(lit);
886 [ - - ]: 0 : if (rew.isConst())
887 : : {
888 [ - - ]: 0 : Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to "
889 : 0 : << rew << "." << std::endl;
890 : 0 : return rew.getConst<bool>();
891 : : }
892 : : // if checking for conflicts, we must be sure that the (negation of)
893 : : // constraint is (not) entailed
894 [ - - ]: 0 : if (!chEnt)
895 : : {
896 : 0 : rew = rewrite(rew.negate());
897 : : }
898 : : // check if it is entailed
899 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
900 : 0 : << "Check entailment of " << rew << "..." << std::endl;
901 : : std::pair<bool, Node> et =
902 : 0 : d_parent->getState().getValuation().entailmentCheck(
903 : 0 : options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
904 : 0 : ++(d_parent->d_statistics.d_entailment_checks);
905 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
906 : 0 : << "ET result : " << et.first << " " << et.second << std::endl;
907 [ - - ]: 0 : if (!et.first)
908 : : {
909 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
910 : 0 : << "...cannot show entailment of " << rew << "." << std::endl;
911 : 0 : return !chEnt;
912 : : }
913 : 0 : return chEnt;
914 : 0 : }
915 : :
916 : 31587 : bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
917 : : {
918 : : // assign values for variables that were unassigned (usually not necessary,
919 : : // but handles corner cases)
920 : 31587 : bool doFail = false;
921 : 31587 : bool success = true;
922 [ - + ]: 31587 : if (doContinue)
923 : : {
924 : 0 : doFail = true;
925 : 0 : success = false;
926 : : }
927 : : else
928 : : {
929 [ + + ]: 31587 : if (isBaseMatchComplete())
930 : : {
931 : 30277 : return true;
932 : : }
933 : : // solve for interpreted symbol matches
934 : : // this breaks the invariant that all introduced constraints are over
935 : : // existing terms
936 [ + + ]: 1350 : for (int i = (int)(d_tsym_vars.size() - 1); i >= 0; i--)
937 : : {
938 : 66 : int index = d_tsym_vars[i];
939 : 66 : TNode v = getCurrentValue(d_vars[index]);
940 : 66 : int slv_v = -1;
941 [ + + ]: 66 : if (v == d_vars[index])
942 : : {
943 : 40 : slv_v = index;
944 : : }
945 [ + - ]: 132 : Trace("qcf-tconstraint-debug")
946 : 0 : << "Solve " << d_vars[index] << " = " << v << " "
947 : 66 : << d_vars[index].getKind() << std::endl;
948 : 66 : if (d_vars[index].getKind() == Kind::ADD
949 [ + + ][ + + ]: 66 : || d_vars[index].getKind() == Kind::MULT)
[ + + ]
950 : : {
951 : 40 : Kind k = d_vars[index].getKind();
952 : 40 : std::vector<TNode> children;
953 [ + + ]: 76 : for (const Node& vi : d_vars[index])
954 : : {
955 : 62 : int vn = getVarNum(vi);
956 [ + + ]: 62 : if (vn != -1)
957 : : {
958 : 47 : TNode vv = getCurrentValue(vi);
959 [ + + ]: 47 : if (vv == vi)
960 : : {
961 : : // we will assign this
962 [ - + ]: 40 : if (slv_v == -1)
963 : : {
964 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
965 : 0 : << "...will solve for var #" << vn << std::endl;
966 : 0 : slv_v = vn;
967 [ - - ]: 0 : if (!d_parent->atConflictEffort())
968 : : {
969 : 0 : break;
970 : : }
971 : : }
972 : : else
973 : : {
974 : 80 : Node z = d_parent->getZero(d_vars[index].getType(), k);
975 [ + + ]: 40 : if (!z.isNull())
976 : : {
977 : 33 : size_t vni = static_cast<size_t>(vn);
978 [ + - ]: 66 : Trace("qcf-tconstraint-debug")
979 : 33 : << "...set " << d_vars[vn] << " = " << z << std::endl;
980 : 33 : assigned.push_back(vni);
981 [ + + ]: 33 : if (!setMatch(vni, z, false, true))
982 : : {
983 : 26 : success = false;
984 : 26 : break;
985 : : }
986 : : }
987 [ + + ]: 40 : }
988 : : }
989 : : else
990 : : {
991 [ + - ]: 14 : Trace("qcf-tconstraint-debug")
992 : 7 : << "...sum value " << vv << std::endl;
993 : 7 : children.push_back(vv);
994 : : }
995 [ + + ]: 47 : }
996 : : else
997 : : {
998 [ + - ]: 15 : Trace("qcf-tconstraint-debug") << "...sum " << vi << std::endl;
999 : 15 : children.push_back(vi);
1000 : : }
1001 [ + + ]: 62 : }
1002 [ + + ]: 40 : if (success)
1003 : : {
1004 [ + - ]: 14 : if (slv_v != -1)
1005 : : {
1006 : 14 : Node lhs;
1007 [ - + ]: 14 : if (children.empty())
1008 : : {
1009 : 0 : lhs = d_parent->getZero(d_vars[index].getType(), k);
1010 : : }
1011 [ + - ]: 14 : else if (children.size() == 1)
1012 : : {
1013 : 14 : lhs = children[0];
1014 : : }
1015 : : else
1016 : : {
1017 : 0 : lhs = nodeManager()->mkNode(k, children);
1018 : : }
1019 : 14 : Node sum;
1020 [ + - ]: 14 : if (v == d_vars[index])
1021 : : {
1022 : 14 : sum = lhs;
1023 : : }
1024 : : else
1025 : : {
1026 [ - - ]: 0 : if (d_parent->atConflictEffort())
1027 : : {
1028 : 0 : Kind kn = k;
1029 [ - - ]: 0 : if (d_vars[index].getKind() == Kind::ADD)
1030 : : {
1031 : 0 : kn = Kind::SUB;
1032 : : }
1033 [ - - ]: 0 : if (kn != k)
1034 : : {
1035 : 0 : sum = nodeManager()->mkNode(kn, v, lhs);
1036 : : }
1037 : : }
1038 : : }
1039 [ + - ]: 14 : if (!sum.isNull())
1040 : : {
1041 : 14 : assigned.push_back(slv_v);
1042 [ + - ]: 28 : Trace("qcf-tconstraint-debug")
1043 : 14 : << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
1044 [ - + ]: 14 : if (!setMatch(slv_v, sum, false, true))
1045 : : {
1046 : 0 : success = false;
1047 : : }
1048 : 14 : d_parent->d_tempCache.push_back(sum);
1049 : : }
1050 : 14 : }
1051 : : else
1052 : : {
1053 : : // must show that constraint is met
1054 : 0 : Node sum = nodeManager()->mkNode(k, children);
1055 : 0 : Node eq = sum.eqNode(v);
1056 [ - - ]: 0 : if (!entailmentTest(eq))
1057 : : {
1058 : 0 : success = false;
1059 : : }
1060 : 0 : d_parent->d_tempCache.push_back(sum);
1061 : 0 : }
1062 : : }
1063 : 40 : }
1064 : :
1065 [ + + ]: 66 : if (!success)
1066 : : {
1067 : 26 : break;
1068 : : }
1069 [ + + ]: 66 : }
1070 [ + + ]: 1310 : if (success)
1071 : : {
1072 : : // check what is left to assign
1073 : 1284 : d_unassigned.clear();
1074 : 1284 : d_unassigned_tn.clear();
1075 [ + + ]: 7704 : std::vector<size_t> unassigned[2];
1076 [ + + ]: 6420 : std::vector<TypeNode> unassigned_tn[2];
1077 [ + + ]: 3551 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
1078 : : {
1079 [ + + ]: 2267 : if (d_match[i].isNull())
1080 : : {
1081 [ + + ]: 1803 : int rindex = d_var_mg.find(i) == d_var_mg.end() ? 1 : 0;
1082 : 1803 : unassigned[rindex].push_back(i);
1083 : 1803 : unassigned_tn[rindex].push_back(getVar(i).getType());
1084 : 1803 : assigned.push_back(i);
1085 : : }
1086 : : }
1087 : 1284 : d_unassigned_nvar = unassigned[0].size();
1088 [ + + ]: 3852 : for (unsigned i = 0; i < 2; i++)
1089 : : {
1090 : 5136 : d_unassigned.insert(
1091 : 2568 : d_unassigned.end(), unassigned[i].begin(), unassigned[i].end());
1092 : 2568 : d_unassigned_tn.insert(d_unassigned_tn.end(),
1093 : : unassigned_tn[i].begin(),
1094 : : unassigned_tn[i].end());
1095 : : }
1096 : 1284 : d_una_eqc_count.clear();
1097 : 1284 : d_una_index = 0;
1098 [ + + ][ + + ]: 7704 : }
[ - - ][ - - ]
1099 : : }
1100 : :
1101 [ + + ][ - + ]: 1310 : if (!d_unassigned.empty() && (success || doContinue))
[ - - ][ + + ]
1102 : : {
1103 [ + - ]: 2430 : Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size()
1104 : 1215 : << ")..." << std::endl;
1105 : : do
1106 : : {
1107 [ - + ]: 1215 : if (doFail)
1108 : : {
1109 [ - - ]: 0 : Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
1110 : : }
1111 : 1215 : bool invalidMatch = false;
1112 [ + + ][ + - ]: 8126 : while ((success && d_una_index < d_unassigned.size()) || invalidMatch
1113 [ + + ][ - + ]: 13822 : || doFail)
[ + + ]
1114 : : {
1115 : 5696 : invalidMatch = false;
1116 [ + - ][ + + ]: 5696 : if (!doFail && d_una_index == d_una_eqc_count.size())
[ + + ]
1117 : : {
1118 : : // check if it has now been assigned
1119 [ + + ]: 1703 : if (d_una_index < d_unassigned_nvar)
1120 : : {
1121 [ + - ]: 80 : if (!isConstrainedVar(d_unassigned[d_una_index]))
1122 : : {
1123 : 80 : d_una_eqc_count.push_back(-1);
1124 : : }
1125 : : else
1126 : : {
1127 : 0 : d_var_mg[d_unassigned[d_una_index]]->reset(true);
1128 : 0 : d_una_eqc_count.push_back(0);
1129 : : }
1130 : : }
1131 : : else
1132 : : {
1133 : 1623 : d_una_eqc_count.push_back(0);
1134 : : }
1135 : : }
1136 : : else
1137 : : {
1138 : 3993 : bool failed = false;
1139 [ + - ]: 3993 : if (!doFail)
1140 : : {
1141 [ + + ]: 3993 : if (d_una_index < d_unassigned_nvar)
1142 : : {
1143 [ + - ]: 80 : if (!isConstrainedVar(d_unassigned[d_una_index]))
1144 : : {
1145 [ + - ]: 160 : Trace("qcf-check-unassign")
1146 : 0 : << "Succeeded, variable unconstrained at " << d_una_index
1147 : 80 : << std::endl;
1148 : 80 : d_una_index++;
1149 : : }
1150 [ - - ]: 0 : else if (d_var_mg[d_unassigned[d_una_index]]->getNextMatch())
1151 : : {
1152 [ - - ]: 0 : Trace("qcf-check-unassign") << "Succeeded match with mg at "
1153 : 0 : << d_una_index << std::endl;
1154 : 0 : d_una_index++;
1155 : : }
1156 : : else
1157 : : {
1158 : 0 : failed = true;
1159 [ - - ]: 0 : Trace("qcf-check-unassign")
1160 : 0 : << "Failed match with mg at " << d_una_index << std::endl;
1161 : : }
1162 : : }
1163 : : else
1164 : : {
1165 [ + - ][ + - ]: 3913 : Assert(doFail || d_una_index + 1 == d_una_eqc_count.size());
[ - + ][ - + ]
[ - - ]
1166 : : const std::vector<TNode>& eqcs =
1167 : 3913 : d_parent->d_eqcs[d_unassigned_tn[d_una_index]];
1168 [ + + ]: 3913 : if (d_una_eqc_count[d_una_index] < static_cast<int>(eqcs.size()))
1169 : : {
1170 : 2581 : int currIndex = d_una_eqc_count[d_una_index];
1171 : 2581 : d_una_eqc_count[d_una_index]++;
1172 [ + - ]: 5162 : Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->"
1173 : 2581 : << eqcs[currIndex] << std::endl;
1174 [ + + ]: 5162 : if (setMatch(
1175 : 5162 : d_unassigned[d_una_index], eqcs[currIndex], true, true))
1176 : : {
1177 : 642 : d_match_term[d_unassigned[d_una_index]] = TNode::null();
1178 [ + - ]: 1284 : Trace("qcf-check-unassign")
1179 : 642 : << "Succeeded match " << d_una_index << std::endl;
1180 : 642 : d_una_index++;
1181 : : }
1182 : : else
1183 : : {
1184 [ + - ]: 3878 : Trace("qcf-check-unassign")
1185 : 1939 : << "Failed match " << d_una_index << std::endl;
1186 : 1939 : invalidMatch = true;
1187 : : }
1188 : : }
1189 : : else
1190 : : {
1191 : 1332 : failed = true;
1192 [ + - ]: 2664 : Trace("qcf-check-unassign")
1193 : 1332 : << "No more matches " << d_una_index << std::endl;
1194 : : }
1195 : : }
1196 : : }
1197 [ + - ][ + + ]: 3993 : if (doFail || failed)
1198 : : {
1199 : : do
1200 : : {
1201 [ + - ]: 1332 : if (!doFail)
1202 : : {
1203 : 1332 : d_una_eqc_count.pop_back();
1204 : : }
1205 : : else
1206 : : {
1207 : 0 : doFail = false;
1208 : : }
1209 [ + + ]: 1332 : if (d_una_index == 0)
1210 : : {
1211 : 981 : success = false;
1212 : 981 : break;
1213 : : }
1214 : 351 : d_una_index--;
1215 [ - + ]: 351 : } while (d_una_eqc_count[d_una_index] == -1);
1216 : : }
1217 : : }
1218 : : }
1219 [ + + ]: 1215 : if (success)
1220 : : {
1221 : 234 : doFail = true;
1222 [ + - ]: 234 : Trace("qcf-check-unassign") << " Try: " << std::endl;
1223 [ - + ]: 234 : if (TraceIsOn("qcf-check"))
1224 : : {
1225 [ - - ]: 0 : for (int ui : d_unassigned)
1226 : : {
1227 [ - - ]: 0 : if (!d_match[ui].isNull())
1228 : : {
1229 [ - - ]: 0 : Trace("qcf-check-unassign")
1230 : 0 : << " Assigned #" << ui << " : " << d_vars[ui] << " -> "
1231 : 0 : << d_match[ui] << std::endl;
1232 : : }
1233 : : }
1234 : : }
1235 : : }
1236 [ + + ][ - + ]: 1215 : } while (success && isMatchSpurious());
[ - + ]
1237 [ + - ]: 1215 : Trace("qcf-check") << "done assigning." << std::endl;
1238 : : }
1239 [ + + ]: 1310 : if (success)
1240 : : {
1241 [ - + ]: 303 : if (TraceIsOn("qcf-check"))
1242 : : {
1243 [ - - ]: 0 : for (int ui : d_unassigned)
1244 : : {
1245 [ - - ]: 0 : if (!d_match[ui].isNull())
1246 : : {
1247 [ - - ]: 0 : Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui]
1248 : 0 : << " -> " << d_match[ui] << std::endl;
1249 : : }
1250 : : }
1251 : : }
1252 : 303 : return true;
1253 : : }
1254 : 1007 : revertMatch(assigned);
1255 : 1007 : assigned.clear();
1256 : 1007 : return false;
1257 : : }
1258 : :
1259 : 30580 : void QuantInfo::getMatch(std::vector<Node>& terms)
1260 : : {
1261 [ + + ]: 118186 : for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++)
1262 : : {
1263 : 87606 : size_t repVar = getCurrentRepVar(i);
1264 : 87606 : Node cv;
1265 [ + + ]: 87606 : if (!d_match_term[repVar].isNull())
1266 : : {
1267 : 87209 : cv = d_match_term[repVar];
1268 : : }
1269 : : else
1270 : : {
1271 : 397 : cv = d_match[repVar];
1272 : : }
1273 [ + - ]: 175212 : Trace("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from "
1274 : 87606 : << d_match[i] << std::endl;
1275 : 87606 : terms.push_back(cv);
1276 : 87606 : }
1277 : 30580 : }
1278 : :
1279 : 28557 : void QuantInfo::revertMatch(const std::vector<size_t>& assigned)
1280 : : {
1281 [ + + ]: 30200 : for (size_t a : assigned)
1282 : : {
1283 : 1643 : unsetMatch(a);
1284 : : }
1285 : 28557 : }
1286 : :
1287 : 0 : void QuantInfo::debugPrintMatch(CVC5_UNUSED const char* c) const
1288 : : {
1289 [ - - ]: 0 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
1290 : : {
1291 [ - - ]: 0 : Trace(c) << " " << d_vars[i] << " -> ";
1292 [ - - ]: 0 : if (!d_match[i].isNull())
1293 : : {
1294 [ - - ]: 0 : Trace(c) << d_match[i];
1295 : : }
1296 : : else
1297 : : {
1298 [ - - ]: 0 : Trace(c) << "(unassigned) ";
1299 : : }
1300 : : std::map<size_t, std::map<TNode, size_t>>::const_iterator itc =
1301 : 0 : d_curr_var_deq.find(i);
1302 [ - - ]: 0 : if (!itc->second.empty())
1303 : : {
1304 [ - - ]: 0 : Trace(c) << ", DEQ{ ";
1305 [ - - ]: 0 : for (const std::pair<const TNode, size_t>& d : itc->second)
1306 : : {
1307 [ - - ]: 0 : Trace(c) << d.first << " ";
1308 : : }
1309 [ - - ]: 0 : Trace(c) << "}";
1310 : : }
1311 : 0 : if (!d_match_term[i].isNull() && d_match_term[i] != d_match[i])
1312 : : {
1313 [ - - ]: 0 : Trace(c) << ", EXP : " << d_match_term[i];
1314 : : }
1315 [ - - ]: 0 : Trace(c) << std::endl;
1316 : : }
1317 [ - - ]: 0 : if (!d_tconstraints.empty())
1318 : : {
1319 [ - - ]: 0 : Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
1320 [ - - ]: 0 : for (const std::pair<const Node, bool>& tc : d_tconstraints)
1321 : : {
1322 [ - - ]: 0 : Trace(c) << " " << tc.first << " -> " << tc.second << std::endl;
1323 : : }
1324 : : }
1325 : 0 : }
1326 : :
1327 : 331561 : MatchGen::MatchGen(
1328 : 331561 : Env& env, QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar)
1329 : : : EnvObj(env),
1330 : 331561 : d_tgt(),
1331 : 331561 : d_tgt_orig(),
1332 : 331561 : d_wasSet(),
1333 : 331561 : d_n(),
1334 : 331561 : d_type(),
1335 : 331561 : d_type_not(),
1336 : 331561 : d_parent(p),
1337 : 331561 : d_qi(qi),
1338 : 331561 : d_matched_basis(),
1339 : 331561 : d_binding()
1340 : : {
1341 : : // initialize temporary
1342 : 331561 : d_child_counter = -1;
1343 : 331561 : d_use_children = true;
1344 : :
1345 [ + - ]: 663122 : Trace("qcf-qregister-debug")
1346 : 331561 : << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
1347 : 331561 : std::vector<Node> qni_apps;
1348 : 331561 : d_qni_size = 0;
1349 [ + + ]: 331561 : if (isVar)
1350 : : {
1351 [ - + ][ - + ]: 164856 : Assert(qi->d_var_num.find(n) != qi->d_var_num.end());
[ - - ]
1352 : : // rare case where we have a free variable in an operator, we are invalid
1353 : 494568 : if (n.getKind() == Kind::ITE
1354 : 164856 : || (n.getKind() == Kind::APPLY_UF && expr::hasFreeVar(n.getOperator())))
1355 : : {
1356 : 3887 : d_type = typ_invalid;
1357 : : }
1358 : : else
1359 : : {
1360 [ + + ]: 160969 : d_type = isHandledUfTerm(n) ? typ_var : typ_tsym;
1361 : 160969 : int vn = qi->getVarNum(n);
1362 [ - + ][ - + ]: 160969 : Assert(vn >= 0);
[ - - ]
1363 : 160969 : d_qni_var_num[0] = static_cast<size_t>(vn);
1364 : 160969 : d_qni_size++;
1365 : 160969 : d_type_not = false;
1366 : 160969 : d_n = n;
1367 : : // Node f = getMatchOperator( n );
1368 [ + + ]: 503452 : for (unsigned j = 0; j < d_n.getNumChildren(); j++)
1369 : : {
1370 : 342483 : Node nn = d_n[j];
1371 [ + - ]: 342483 : Trace("qcf-qregister-debug") << " " << d_qni_size;
1372 [ + + ]: 342483 : if (qi->isVar(nn))
1373 : : {
1374 : 293305 : size_t v = qi->d_var_num[nn];
1375 [ + - ]: 293305 : Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
1376 : 293305 : d_qni_var_num[d_qni_size] = v;
1377 : : // qi->addFuncParent( v, f, j );
1378 : : }
1379 : : else
1380 : : {
1381 [ + - ]: 49178 : Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
1382 : 49178 : d_qni_gterm[d_qni_size] = nn;
1383 : : }
1384 : 342483 : d_qni_size++;
1385 : 342483 : }
1386 : : }
1387 : : }
1388 : : else
1389 : : {
1390 [ + + ]: 166705 : if (expr::hasBoundVar(n))
1391 : : {
1392 : 166448 : d_type_not = false;
1393 : 166448 : d_n = n;
1394 [ + + ]: 166448 : if (d_n.getKind() == Kind::NOT)
1395 : : {
1396 : 52921 : d_n = d_n[0];
1397 : 52921 : d_type_not = !d_type_not;
1398 : : }
1399 : :
1400 [ + + ]: 166448 : if (isHandledBoolConnective(d_n))
1401 : : {
1402 : : // non-literals
1403 : 57165 : d_type = typ_formula;
1404 [ + + ]: 179942 : for (unsigned i = 0; i < d_n.getNumChildren(); i++)
1405 : : {
1406 [ + + ][ + + ]: 130325 : if (d_n.getKind() != Kind::FORALL || i == 1)
[ + + ]
1407 : : {
1408 : : std::unique_ptr<MatchGen> mg =
1409 : 119164 : std::make_unique<MatchGen>(d_env, p, qi, d_n[i], false);
1410 [ + + ]: 119164 : if (!mg->isValid())
1411 : : {
1412 : 7548 : setInvalid();
1413 : 7548 : break;
1414 : : }
1415 : 111616 : d_children.push_back(std::move(mg));
1416 [ + + ]: 119164 : }
1417 : : }
1418 : : }
1419 : : else
1420 : : {
1421 : 109283 : d_type = typ_invalid;
1422 : : // literals
1423 [ + + ]: 109283 : if (isHandledUfTerm(d_n))
1424 : : {
1425 [ - + ][ - + ]: 42086 : Assert(qi->isVar(d_n));
[ - - ]
1426 : 42086 : d_type = typ_pred;
1427 : : }
1428 [ + + ]: 67197 : else if (d_n.getKind() == Kind::BOUND_VARIABLE)
1429 : : {
1430 [ - + ][ - + ]: 344 : Assert(d_n.getType().isBoolean());
[ - - ]
1431 : 344 : d_type = typ_bool_var;
1432 : : }
1433 : 66853 : else if (d_n.getKind() == Kind::EQUAL
1434 [ + + ][ + + ]: 66853 : || options().quantifiers.cbqiTConstraint)
[ + + ]
1435 : : {
1436 [ + + ]: 182787 : for (unsigned i = 0; i < d_n.getNumChildren(); i++)
1437 : : {
1438 [ + + ]: 121858 : if (expr::hasBoundVar(d_n[i]))
1439 : : {
1440 [ - + ]: 92124 : if (!qi->isVar(d_n[i]))
1441 : : {
1442 [ - - ]: 0 : Trace("qcf-qregister-debug")
1443 : 0 : << "ERROR : not var " << d_n[i] << std::endl;
1444 : : }
1445 [ - + ][ - + ]: 92124 : Assert(qi->isVar(d_n[i]));
[ - - ]
1446 : 92124 : if (d_n.getKind() != Kind::EQUAL && qi->isVar(d_n[i]))
1447 : : {
1448 : 648 : d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
1449 : : }
1450 : : }
1451 : : else
1452 : : {
1453 : 29734 : d_qni_gterm[i] = d_n[i];
1454 : : }
1455 : : }
1456 [ + + ]: 60929 : d_type = d_n.getKind() == Kind::EQUAL ? typ_eq : typ_tconstraint;
1457 [ + - ]: 60929 : Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
1458 : : }
1459 : : }
1460 : : }
1461 : : else
1462 : : {
1463 : : // we will just evaluate
1464 : 257 : d_n = n;
1465 : 257 : d_type = typ_ground;
1466 : : }
1467 : : }
1468 [ + - ]: 331561 : Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
1469 : 331561 : debugPrintType("qcf-qregister-debug", d_type);
1470 [ + - ]: 331561 : Trace("qcf-qregister-debug") << std::endl;
1471 : 331561 : }
1472 : :
1473 : 943438 : void MatchGen::collectBoundVar(Node n,
1474 : : std::vector<int>& cbvars,
1475 : : std::map<Node, bool>& visited,
1476 : : bool& hasNested)
1477 : : {
1478 [ + + ]: 943438 : if (visited.find(n) == visited.end())
1479 : : {
1480 : 814137 : visited[n] = true;
1481 [ + + ]: 814137 : if (n.getKind() == Kind::FORALL)
1482 : : {
1483 : 7790 : hasNested = true;
1484 : : }
1485 : 814137 : int v = d_qi->getVarNum(n);
1486 [ + + ][ + - ]: 814137 : if (v != -1 && std::find(cbvars.begin(), cbvars.end(), v) == cbvars.end())
[ + + ]
1487 : : {
1488 : 518746 : cbvars.push_back(v);
1489 : : }
1490 [ + + ]: 1663307 : for (const Node& nc : n)
1491 : : {
1492 : 849170 : collectBoundVar(nc, cbvars, visited, hasNested);
1493 : 849170 : }
1494 : : }
1495 : 943438 : }
1496 : :
1497 : 291919 : void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
1498 : : {
1499 [ + - ]: 583838 : Trace("qcf-qregister-debug") << "Determine variable order " << d_n
1500 : 291919 : << ", #bvars = " << bvars.size() << std::endl;
1501 : 291919 : bool isComm = d_type == typ_formula
1502 [ + + ][ + + ]: 307852 : && (d_n.getKind() == Kind::OR || d_n.getKind() == Kind::AND
[ + + ]
1503 [ + + ]: 15933 : || d_n.getKind() == Kind::EQUAL);
1504 [ + + ]: 291919 : if (isComm)
1505 : : {
1506 : 34230 : std::map<int, std::vector<int>> c_to_vars;
1507 : 34230 : std::map<int, std::vector<int>> vars_to_c;
1508 : 34230 : std::map<int, int> vb_count;
1509 : 34230 : std::map<int, int> vu_count;
1510 : 34230 : std::map<int, bool> has_nested;
1511 : 34230 : std::vector<bool> assigned;
1512 [ + - ]: 34230 : Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
1513 [ + + ]: 119473 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1514 : : {
1515 : 85243 : std::map<Node, bool> visited;
1516 : 85243 : has_nested[i] = false;
1517 : 85243 : collectBoundVar(
1518 : 170486 : d_children[i]->getNode(), c_to_vars[i], visited, has_nested[i]);
1519 : 85243 : assigned.push_back(false);
1520 : 85243 : vb_count[i] = 0;
1521 : 85243 : vu_count[i] = 0;
1522 [ + + ]: 500497 : for (unsigned j = 0; j < c_to_vars[i].size(); j++)
1523 : : {
1524 : 415254 : int v = c_to_vars[i][j];
1525 : 415254 : vars_to_c[v].push_back(i);
1526 [ + + ]: 415254 : if (std::find(bvars.begin(), bvars.end(), v) == bvars.end())
1527 : : {
1528 : 377114 : vu_count[i]++;
1529 : : }
1530 : : else
1531 : : {
1532 : 38140 : vb_count[i]++;
1533 : : }
1534 : : }
1535 : 85243 : }
1536 : : // children that bind no unbound variable, then the most number of bound,
1537 : : // unbound variables go first
1538 [ + - ]: 68460 : Trace("qcf-qregister-vo")
1539 : 34230 : << "Variable order for " << d_n << " : " << std::endl;
1540 : 34230 : size_t nqvars = d_qi->d_vars.size();
1541 : : do
1542 : : {
1543 : 85243 : int min_score0 = -1;
1544 : 85243 : int min_score = -1;
1545 : 85243 : int min_score_index = -1;
1546 [ + + ]: 1228658 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1547 : : {
1548 [ + + ]: 1143415 : if (!assigned[i])
1549 : : {
1550 [ + - ]: 1228658 : Trace("qcf-qregister-debug2")
1551 : 0 : << "Child " << i << " has b/ub : " << vb_count[i] << "/"
1552 : 614329 : << vu_count[i] << std::endl;
1553 : 614329 : int score0 = 0; // has_nested[i] ? 0 : 1;
1554 : : int score;
1555 [ + - ]: 614329 : if (!options().quantifiers.cbqiVoExp)
1556 : : {
1557 : 614329 : score = vu_count[i];
1558 : : }
1559 : : else
1560 : : {
1561 [ - - ]: 0 : score = vu_count[i] == 0 ? 0
1562 : 0 : : (1 + nqvars * (nqvars - vb_count[i])
1563 : 0 : + (nqvars - vu_count[i]));
1564 : : }
1565 [ + + ][ + - ]: 614329 : if (min_score == -1 || score0 < min_score0
1566 [ + - ][ + + ]: 529086 : || (score0 == min_score0 && score < min_score))
1567 : : {
1568 : 139769 : min_score0 = score0;
1569 : 139769 : min_score = score;
1570 : 139769 : min_score_index = i;
1571 : : }
1572 : : }
1573 : : }
1574 [ + - ]: 170486 : Trace("qcf-qregister-vo")
1575 : 0 : << " " << d_children_order.size() + 1 << ": "
1576 [ - + ][ - - ]: 85243 : << d_children[min_score_index]->getNode() << " : ";
1577 [ + - ]: 170486 : Trace("qcf-qregister-vo")
1578 : 0 : << vu_count[min_score_index] << " " << vb_count[min_score_index]
1579 : 85243 : << " " << has_nested[min_score_index] << std::endl;
1580 [ + - ]: 170486 : Trace("qcf-qregister-debug")
1581 : 85243 : << "...assign child " << min_score_index << std::endl;
1582 [ + - ]: 85243 : Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
1583 [ - + ][ - + ]: 85243 : Assert(min_score_index != -1);
[ - - ]
1584 : : // add to children order
1585 : 85243 : d_children_order.push_back(min_score_index);
1586 : 85243 : assigned[min_score_index] = true;
1587 : : // determine order internal to children
1588 : 85243 : d_children[min_score_index]->determineVariableOrder(bvars);
1589 [ + - ]: 85243 : Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
1590 : : // now, make it a bound variable
1591 [ + + ]: 85243 : if (vu_count[min_score_index] > 0)
1592 : : {
1593 [ + + ]: 467098 : for (unsigned i = 0; i < c_to_vars[min_score_index].size(); i++)
1594 : : {
1595 : 386596 : int v = c_to_vars[min_score_index][i];
1596 [ + + ]: 386596 : if (std::find(bvars.begin(), bvars.end(), v) == bvars.end())
1597 : : {
1598 [ + + ]: 483726 : for (unsigned j = 0; j < vars_to_c[v].size(); j++)
1599 : : {
1600 : 310653 : int vc = vars_to_c[v][j];
1601 : 310653 : vu_count[vc]--;
1602 : 310653 : vb_count[vc]++;
1603 : : }
1604 : 173073 : bvars.push_back(v);
1605 : : }
1606 : : }
1607 : : }
1608 [ + - ]: 170486 : Trace("qcf-qregister-debug")
1609 : 85243 : << "...done assign child " << min_score_index << std::endl;
1610 [ + + ]: 85243 : } while (d_children_order.size() != d_children.size());
1611 [ + - ]: 68460 : Trace("qcf-qregister-debug")
1612 : 34230 : << "Done assign variable ordering for " << d_n << std::endl;
1613 : 34230 : }
1614 : : else
1615 : : {
1616 [ + + ]: 266714 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1617 : : {
1618 : 9025 : d_children_order.push_back(i);
1619 : 9025 : d_children[i]->determineVariableOrder(bvars);
1620 : : // now add to bvars
1621 : 9025 : std::map<Node, bool> visited;
1622 : 9025 : std::vector<int> cvars;
1623 : 9025 : bool has_nested = false;
1624 : 9025 : collectBoundVar(d_children[i]->getNode(), cvars, visited, has_nested);
1625 [ + + ]: 112517 : for (unsigned j = 0; j < cvars.size(); j++)
1626 : : {
1627 [ + + ]: 103492 : if (std::find(bvars.begin(), bvars.end(), cvars[j]) == bvars.end())
1628 : : {
1629 : 13713 : bvars.push_back(cvars[j]);
1630 : : }
1631 : : }
1632 : 9025 : }
1633 : : }
1634 : 291919 : }
1635 : :
1636 : 2291094 : bool MatchGen::reset_round()
1637 : : {
1638 : 2291094 : d_wasSet = false;
1639 [ + + ]: 3182409 : for (std::unique_ptr<MatchGen>& mg : d_children)
1640 : : {
1641 [ - + ]: 891315 : if (!mg->reset_round())
1642 : : {
1643 : 0 : return false;
1644 : : }
1645 : : }
1646 [ + + ]: 2291094 : if (d_type == typ_ground)
1647 : : {
1648 : 2283 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
1649 : 2283 : QuantifiersState& qs = d_parent->getState();
1650 [ + + ]: 6849 : for (unsigned i = 0; i < 2; i++)
1651 : : {
1652 [ + + ]: 4566 : if (echeck->isEntailed(d_n, i == 0))
1653 : : {
1654 : 48 : d_ground_eval[0] = nodeManager()->mkConst(i == 0);
1655 : : }
1656 [ - + ]: 4566 : if (qs.isInConflict())
1657 : : {
1658 : 0 : return false;
1659 : : }
1660 : : }
1661 : : }
1662 [ + + ]: 2288811 : else if (d_type == typ_eq)
1663 : : {
1664 : 374791 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
1665 : 374791 : QuantifiersState& qs = d_parent->getState();
1666 [ + + ]: 1124373 : for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
1667 : : {
1668 [ + + ]: 749582 : if (!expr::hasBoundVar(d_n[i]))
1669 : : {
1670 : 410108 : TNode t = echeck->getEntailedTerm(d_n[i]);
1671 [ - + ]: 205054 : if (qs.isInConflict())
1672 : : {
1673 : 0 : return false;
1674 : : }
1675 [ + + ]: 205054 : if (t.isNull())
1676 : : {
1677 : 2995 : d_ground_eval[i] = d_n[i];
1678 : : }
1679 : : else
1680 : : {
1681 : 202059 : d_ground_eval[i] = t;
1682 : : }
1683 [ + - ]: 205054 : }
1684 : : }
1685 : : }
1686 : 2291094 : d_qni_bound_cons.clear();
1687 : 2291094 : d_qni_bound_cons_var.clear();
1688 : 2291094 : d_qni_bound.clear();
1689 : 2291094 : return true;
1690 : : }
1691 : :
1692 : 4213665 : void MatchGen::reset(bool tgt)
1693 : : {
1694 [ + + ]: 4213665 : d_tgt = d_type_not ? !tgt : tgt;
1695 [ + - ]: 4213665 : Trace("qcf-match") << " Reset for : " << d_n << ", type : ";
1696 : 4213665 : debugPrintType("qcf-match", d_type);
1697 [ + - ]: 8427330 : Trace("qcf-match") << ", tgt = " << d_tgt
1698 : 0 : << ", children = " << d_children.size() << " "
1699 : 4213665 : << d_children_order.size() << std::endl;
1700 : 4213665 : d_qn.clear();
1701 : 4213665 : d_qni.clear();
1702 : 4213665 : d_qni_bound.clear();
1703 : 4213665 : d_child_counter = -1;
1704 : 4213665 : d_use_children = true;
1705 : 4213665 : d_tgt_orig = d_tgt;
1706 : :
1707 : : // set up processing matches
1708 [ - + ]: 4213665 : if (d_type == typ_invalid)
1709 : : {
1710 : 0 : d_use_children = false;
1711 : : }
1712 [ + + ]: 4213665 : else if (d_type == typ_ground)
1713 : : {
1714 : 913 : d_use_children = false;
1715 : 913 : if (d_ground_eval[0].isConst()
1716 [ + + ][ + + ]: 913 : && d_ground_eval[0].getConst<bool>() == d_tgt)
[ + + ]
1717 : : {
1718 : 62 : d_child_counter = 0;
1719 : : }
1720 : : }
1721 [ + + ]: 4212752 : else if (d_qi->isBaseMatchComplete())
1722 : : {
1723 : 27636 : d_use_children = false;
1724 : 27636 : d_child_counter = 0;
1725 : : }
1726 [ + + ]: 4185116 : else if (d_type == typ_bool_var)
1727 : : {
1728 : : // get current value of the variable
1729 : 2645 : TNode n = d_qi->getCurrentValue(d_n);
1730 : 2645 : int vnn = d_qi->getVarNum(n);
1731 [ - + ]: 2645 : if (vnn == -1)
1732 : : {
1733 : : // evaluate the value, see if it is compatible
1734 : : EntailmentCheck* echeck =
1735 : 0 : d_parent->getTermRegistry().getEntailmentCheck();
1736 [ - - ]: 0 : if (echeck->isEntailed(n, d_tgt))
1737 : : {
1738 : 0 : d_child_counter = 0;
1739 : : }
1740 : : }
1741 : : else
1742 : : {
1743 : 2645 : size_t vn = d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1744 : : // unassigned, set match to true/false
1745 : 2645 : d_qni_bound[0] = vn;
1746 : 2645 : d_qi->setMatch(vn, nodeManager()->mkConst(d_tgt), false, true);
1747 : 2645 : d_child_counter = 0;
1748 : : }
1749 [ + - ]: 2645 : if (d_child_counter == 0)
1750 : : {
1751 : 2645 : d_qn.push_back(nullptr);
1752 : : }
1753 : 2645 : }
1754 [ + + ]: 4182471 : else if (d_type == typ_var)
1755 : : {
1756 [ - + ][ - + ]: 3151036 : Assert(isHandledUfTerm(d_n));
[ - - ]
1757 : 6302072 : TNode f = d_parent->getTermDatabase()->getMatchOperator(d_n);
1758 [ + - ]: 6302072 : Trace("qcf-match-debug")
1759 : 3151036 : << " reset: Var will match operators of " << f << std::endl;
1760 : : TNodeTrie* qni =
1761 : 3151036 : d_parent->getTermDatabase()->getTermArgTrie(Node::null(), f);
1762 [ + - ][ + + ]: 3151036 : if (qni == nullptr || qni->empty())
[ + + ]
1763 : : {
1764 : : // inform irrelevant quantifiers
1765 : 266356 : d_parent->setIrrelevantFunction(f);
1766 : : }
1767 : : else
1768 : : {
1769 : 2884680 : d_qn.push_back(qni);
1770 : : }
1771 : 3151036 : d_matched_basis = false;
1772 : 3151036 : }
1773 [ + + ][ + + ]: 1031435 : else if (d_type == typ_tsym || d_type == typ_tconstraint)
1774 : : {
1775 [ + + ]: 7060 : for (std::pair<const size_t, size_t>& qvn : d_qni_var_num)
1776 : : {
1777 : 4239 : size_t repVar = d_qi->getCurrentRepVar(qvn.second);
1778 [ + + ]: 4239 : if (d_qi->d_match[repVar].isNull())
1779 : : {
1780 [ + - ]: 8118 : Trace("qcf-match-debug") << "Force matching on child #" << qvn.first
1781 : 4059 : << ", which is var #" << repVar << std::endl;
1782 : 4059 : d_qni_bound[qvn.first] = repVar;
1783 : : }
1784 : : }
1785 : 2821 : d_qn.push_back(nullptr);
1786 : 2821 : }
1787 [ + + ][ + + ]: 1028614 : else if (d_type == typ_pred || d_type == typ_eq)
1788 : : {
1789 : : // add initial constraint
1790 [ + + ]: 4393326 : Node nn[2];
1791 : : int vn[2];
1792 [ + + ]: 732221 : if (d_type == typ_pred)
1793 : : {
1794 : 343177 : nn[0] = d_qi->getCurrentValue(d_n);
1795 : 343177 : int vnn = d_qi->getVarNum(nn[0]);
1796 [ + + ]: 343177 : vn[0] =
1797 : 342625 : vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1798 : 343177 : nn[1] = nodeManager()->mkConst(d_tgt);
1799 : 343177 : vn[1] = -1;
1800 : 343177 : d_tgt = true;
1801 : : }
1802 : : else
1803 : : {
1804 [ + + ]: 1167132 : for (unsigned i = 0; i < 2; i++)
1805 : : {
1806 : 778088 : TNode nc;
1807 : 778088 : std::map<size_t, TNode>::iterator it = d_qni_gterm.find(i);
1808 [ + + ]: 778088 : if (it != d_qni_gterm.end())
1809 : : {
1810 : 243286 : nc = it->second;
1811 : : }
1812 : : else
1813 : : {
1814 : 534802 : nc = d_n[i];
1815 : : }
1816 : 778088 : nn[i] = d_qi->getCurrentValue(nc);
1817 : 778088 : int vnn = d_qi->getVarNum(nn[i]);
1818 [ + + ]: 778088 : vn[i] =
1819 : 524928 : vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1820 : 778088 : }
1821 : : }
1822 : : bool success;
1823 [ + + ][ + + ]: 732221 : if (vn[0] == -1 && vn[1] == -1)
1824 : : {
1825 : : // Trace("qcf-explain") << " reset : " << d_n << " check ground values
1826 : : // " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
1827 [ + - ]: 1564 : Trace("qcf-match-debug")
1828 : 0 : << " reset: check ground values " << nn[0] << " " << nn[1]
1829 : 782 : << " (" << d_tgt << ")" << std::endl;
1830 : : // just compare values
1831 [ + + ]: 782 : if (d_tgt)
1832 : : {
1833 : 710 : success = nn[0] == nn[1];
1834 : : }
1835 : : else
1836 : : {
1837 [ + + ]: 72 : if (d_parent->atConflictEffort())
1838 : : {
1839 : 24 : success = d_parent->areDisequal(nn[0], nn[1]);
1840 : : }
1841 : : else
1842 : : {
1843 : 48 : success = (nn[0] != nn[1]);
1844 : : }
1845 : : }
1846 : : }
1847 : : else
1848 : : {
1849 : : // otherwise, add a constraint to a variable TODO: this may be over-eager
1850 : : // at effort > conflict, since equality may be a propagation
1851 [ + + ][ + + ]: 731439 : if (vn[1] != -1 && vn[0] == -1)
1852 : : {
1853 : : // swap
1854 : 103323 : Node t = nn[1];
1855 : 103323 : nn[1] = nn[0];
1856 : 103323 : nn[0] = t;
1857 : 103323 : vn[0] = vn[1];
1858 : 103323 : vn[1] = -1;
1859 : 103323 : }
1860 [ + - ]: 1462878 : Trace("qcf-match-debug")
1861 : 0 : << " reset: add constraint " << vn[0] << " -> " << nn[1]
1862 : 731439 : << " (vn=" << vn[1] << ")" << std::endl;
1863 : : // add some constraint
1864 : 731439 : int addc = d_qi->addConstraint(vn[0], nn[1], vn[1], d_tgt, false);
1865 : 731439 : success = addc != -1;
1866 : : // if successful and non-redundant, store that we need to cleanup this
1867 [ + + ]: 731439 : if (addc == 1)
1868 : : {
1869 [ + + ]: 2116740 : for (size_t i = 0; i < 2; i++)
1870 : : {
1871 : 2822320 : if (vn[i] != -1
1872 [ + + ][ + - ]: 3094548 : && std::find(
1873 : : d_qni_bound_except.begin(), d_qni_bound_except.end(), i)
1874 [ + + ]: 3094548 : == d_qni_bound_except.end())
1875 : : {
1876 : 841694 : d_qni_bound[vn[i]] = vn[i];
1877 : : }
1878 : : }
1879 : 705580 : d_qni_bound_cons[vn[0]] = nn[1];
1880 : 705580 : d_qni_bound_cons_var[vn[0]] = vn[1];
1881 : : }
1882 : : }
1883 : : // if successful, we will bind values to variables
1884 [ + + ]: 732221 : if (success)
1885 : : {
1886 : 706263 : d_qn.push_back(nullptr);
1887 : : }
1888 [ + + ][ - - ]: 2928884 : }
1889 : : else
1890 : : {
1891 [ - + ]: 296393 : if (d_children.empty())
1892 : : {
1893 : : // add dummy
1894 : 0 : d_qn.push_back(nullptr);
1895 : : }
1896 : : else
1897 : : {
1898 [ + + ][ + + ]: 296393 : if (d_tgt && d_n.getKind() == Kind::FORALL)
[ + + ]
1899 : : {
1900 : : // fail
1901 : : }
1902 [ + + ][ + + ]: 263156 : else if (d_n.getKind() == Kind::FORALL && d_parent->atConflictEffort())
[ + + ]
1903 : : {
1904 : : // fail
1905 : : }
1906 : : else
1907 : : {
1908 : : // reset the first child to d_tgt
1909 : 261631 : d_child_counter = 0;
1910 : 261631 : getChild(d_child_counter)->reset(d_tgt);
1911 : : }
1912 : : }
1913 : : }
1914 : 4213665 : d_binding = false;
1915 : 4213665 : d_wasSet = true;
1916 [ + - ]: 8427330 : Trace("qcf-match") << " reset: Finished reset for " << d_n
1917 : 0 : << ", success = "
1918 [ - - ][ - - ]: 4213665 : << (!d_qn.empty() || d_child_counter != -1) << std::endl;
1919 : 8065571 : }
1920 : :
1921 : 5091817 : bool MatchGen::getNextMatch()
1922 : : {
1923 [ + - ]: 5091817 : Trace("qcf-match") << " Get next match for : " << d_n << ", type = ";
1924 : 5091817 : debugPrintType("qcf-match", d_type);
1925 [ + - ]: 10183634 : Trace("qcf-match") << ", children = " << d_children.size()
1926 : 5091817 : << ", binding = " << d_binding << std::endl;
1927 [ + + ]: 5091817 : if (!d_use_children)
1928 : : {
1929 [ + + ]: 54734 : if (d_child_counter == 0)
1930 : : {
1931 : 27698 : d_child_counter = -1;
1932 : 27698 : return true;
1933 : : }
1934 : : else
1935 : : {
1936 : 27036 : d_wasSet = false;
1937 : 27036 : return false;
1938 : : }
1939 : : }
1940 [ + + ][ + + ]: 5037083 : else if (d_type == typ_var || d_type == typ_eq || d_type == typ_pred
[ + + ]
1941 [ + + ][ + + ]: 336840 : || d_type == typ_bool_var || d_type == typ_tconstraint
1942 [ + + ]: 328537 : || d_type == typ_tsym)
1943 : : {
1944 : 4709655 : bool success = false;
1945 : 4709655 : bool terminate = false;
1946 : : do
1947 : : {
1948 : 8250237 : bool doReset = false;
1949 : 8250237 : bool doFail = false;
1950 [ + + ]: 8250237 : if (!d_binding)
1951 : : {
1952 [ + + ]: 7437376 : if (doMatching())
1953 : : {
1954 [ + - ]: 3561804 : Trace("qcf-match-debug") << " - Matching succeeded" << std::endl;
1955 : 3561804 : d_binding = true;
1956 : 3561804 : d_binding_it = d_qni_bound.begin();
1957 : 3561804 : doReset = true;
1958 : : // for tconstraint, add constraint
1959 [ + + ]: 3561804 : if (d_type == typ_tconstraint)
1960 : : {
1961 : 1868 : std::map<Node, bool>::iterator it = d_qi->d_tconstraints.find(d_n);
1962 [ + - ]: 1868 : if (it == d_qi->d_tconstraints.end())
1963 : : {
1964 : 1868 : d_qi->d_tconstraints[d_n] = d_tgt;
1965 : : // store that we added this constraint
1966 : 1868 : d_qni_bound_cons[0] = d_n;
1967 : : }
1968 [ - - ]: 0 : else if (d_tgt != it->second)
1969 : : {
1970 : 0 : success = false;
1971 : 0 : terminate = true;
1972 : : }
1973 : : }
1974 : : }
1975 : : else
1976 : : {
1977 [ + - ]: 3875572 : Trace("qcf-match-debug") << " - Matching failed" << std::endl;
1978 : 3875572 : success = false;
1979 : 3875572 : terminate = true;
1980 : : }
1981 : : }
1982 : : else
1983 : : {
1984 : 812861 : doFail = true;
1985 : : }
1986 [ + + ]: 8250237 : if (d_binding)
1987 : : {
1988 : : // also need to create match for each variable we bound
1989 : 4374665 : success = true;
1990 [ + - ]: 8749330 : Trace("qcf-match-debug")
1991 : 0 : << " Produce matches for bound variables by " << d_n
1992 : 4374665 : << ", type = ";
1993 : 4374665 : debugPrintType("qcf-match-debug", d_type);
1994 [ + - ]: 4374665 : Trace("qcf-match-debug") << "..." << std::endl;
1995 : :
1996 [ + + ][ + + ]: 11871945 : while ((success && d_binding_it != d_qni_bound.end()) || doFail)
[ + + ][ + + ]
1997 : : {
1998 : 7497280 : QuantInfo::VarMgMap::const_iterator itm;
1999 [ + + ]: 7497280 : if (!doFail)
2000 : : {
2001 [ + - ]: 13368838 : Trace("qcf-match-debug") << " check variable "
2002 : 6684419 : << d_binding_it->second << std::endl;
2003 : 6684419 : itm = d_qi->var_mg_find(d_binding_it->second);
2004 : : }
2005 [ + + ][ + + ]: 7497280 : if (doFail || (d_binding_it->first != 0 && itm != d_qi->var_mg_end()))
[ + + ][ + + ]
2006 : : {
2007 [ + - ]: 8865570 : Trace("qcf-match-debug")
2008 : 0 : << " we had bound variable " << d_binding_it->second
2009 : 4432785 : << ", reset = " << doReset << std::endl;
2010 [ + + ]: 4432785 : if (doReset)
2011 : : {
2012 : 3177543 : itm->second->reset(true);
2013 : : }
2014 [ + + ][ + + ]: 4432785 : if (doFail || !itm->second->getNextMatch())
[ + + ]
2015 : : {
2016 : : do
2017 : : {
2018 [ + + ]: 7036831 : if (d_binding_it == d_qni_bound.begin())
2019 : : {
2020 [ + - ]: 3540582 : Trace("qcf-match-debug") << " failed." << std::endl;
2021 : 3540582 : success = false;
2022 : : }
2023 : : else
2024 : : {
2025 : 3496249 : --d_binding_it;
2026 [ + - ]: 6992498 : Trace("qcf-match-debug")
2027 : 3496249 : << " decrement..." << std::endl;
2028 : : }
2029 : : } while (success
2030 [ + + ][ + + ]: 8259672 : && (d_binding_it->first == 0
[ + + ]
2031 [ + + ]: 1222841 : || (!d_qi->containsVarMg(d_binding_it->second))));
2032 : 3982963 : doReset = false;
2033 : 3982963 : doFail = false;
2034 : : }
2035 : : else
2036 : : {
2037 [ + - ]: 449822 : Trace("qcf-match-debug") << " increment..." << std::endl;
2038 : 449822 : ++d_binding_it;
2039 : 449822 : doReset = true;
2040 : : }
2041 : : }
2042 : : else
2043 : : {
2044 [ + - ]: 6128990 : Trace("qcf-match-debug")
2045 : 3064495 : << " skip..." << d_binding_it->second << std::endl;
2046 : 3064495 : ++d_binding_it;
2047 : 3064495 : doReset = true;
2048 : : }
2049 : : }
2050 [ + + ]: 4374665 : if (!success)
2051 : : {
2052 : 3540582 : d_binding = false;
2053 : : }
2054 : : else
2055 : : {
2056 : 834083 : terminate = true;
2057 [ + + ]: 834083 : if (d_binding_it == d_qni_bound.begin())
2058 : : {
2059 : 8249 : d_binding = false;
2060 : : }
2061 : : }
2062 : : }
2063 [ + + ]: 8250237 : } while (!terminate);
2064 : : // if not successful, clean up the variables you bound
2065 [ + + ]: 4709655 : if (!success)
2066 : : {
2067 [ + + ][ + + ]: 3875572 : if (d_type == typ_eq || d_type == typ_pred)
2068 : : {
2069 : : // clean up the constraints you added
2070 : 726125 : std::map<size_t, size_t>::iterator itb;
2071 [ + + ]: 1425632 : for (const std::pair<const size_t, TNode>& qb : d_qni_bound_cons)
2072 : : {
2073 [ + - ]: 699507 : if (!qb.second.isNull())
2074 : : {
2075 [ + - ]: 1399014 : Trace("qcf-match")
2076 : 0 : << " Clean up bound var " << qb.first
2077 [ - - ]: 699507 : << (d_tgt ? "!" : "") << " = " << qb.second << std::endl;
2078 : 699507 : itb = d_qni_bound_cons_var.find(qb.first);
2079 [ + - ]: 699507 : int vn = itb != d_qni_bound_cons_var.end() ? itb->second : -1;
2080 : 699507 : d_qi->addConstraint(qb.first, qb.second, vn, d_tgt, true);
2081 : : }
2082 : : }
2083 : 726125 : d_qni_bound_cons.clear();
2084 : 726125 : d_qni_bound_cons_var.clear();
2085 : 726125 : d_qni_bound.clear();
2086 : 726125 : }
2087 : : else
2088 : : {
2089 : : // clean up the matches you set
2090 [ + + ]: 5529597 : for (const std::pair<const size_t, size_t>& qb : d_qni_bound)
2091 : : {
2092 [ + - ]: 4760300 : Trace("qcf-match")
2093 : 2380150 : << " Clean up bound var " << qb.second << std::endl;
2094 [ - + ][ - + ]: 2380150 : Assert(qb.second < d_qi->getNumVars());
[ - - ]
2095 : 2380150 : d_qi->unsetMatch(qb.second);
2096 : 2380150 : d_qi->d_match_term[qb.second] = TNode::null();
2097 : : }
2098 : 3149447 : d_qni_bound.clear();
2099 : : }
2100 [ + + ]: 3875572 : if (d_type == typ_tconstraint)
2101 : : {
2102 : : // remove constraint if applicable
2103 [ + - ]: 1854 : if (d_qni_bound_cons.find(0) != d_qni_bound_cons.end())
2104 : : {
2105 : 1854 : d_qi->d_tconstraints.erase(d_n);
2106 : 1854 : d_qni_bound_cons.clear();
2107 : : }
2108 : : }
2109 : : }
2110 [ + - ]: 9419310 : Trace("qcf-match") << " ...finished matching for " << d_n
2111 : 4709655 : << ", success = " << success << std::endl;
2112 : 4709655 : d_wasSet = success;
2113 : 4709655 : return success;
2114 : : }
2115 [ + - ]: 327428 : else if (d_type == typ_formula)
2116 : : {
2117 : 327428 : bool success = false;
2118 [ + + ]: 327428 : if (d_child_counter < 0)
2119 : : {
2120 [ - + ]: 34762 : if (d_child_counter < -1)
2121 : : {
2122 : 0 : d_child_counter = -1;
2123 : : }
2124 : : }
2125 : : else
2126 : : {
2127 [ + + ][ + + ]: 1394830 : while (!success && d_child_counter >= 0)
2128 : : {
2129 : : // transition system based on d_child_counter
2130 [ + + ][ + + ]: 1102164 : if (d_n.getKind() == Kind::OR || d_n.getKind() == Kind::AND)
[ + + ]
2131 : : {
2132 [ + + ]: 843646 : if ((d_n.getKind() == Kind::AND) == d_tgt)
2133 : : {
2134 : : // all children must match simultaneously
2135 [ + + ]: 756466 : if (getChild(d_child_counter)->getNextMatch())
2136 : : {
2137 [ + + ]: 316082 : if (d_child_counter < (int)(getNumChildren() - 1))
2138 : : {
2139 : 308246 : d_child_counter++;
2140 [ + - ]: 616492 : Trace("qcf-match-debug")
2141 : 0 : << " Reset child " << d_child_counter << " of " << d_n
2142 : 308246 : << std::endl;
2143 : 308246 : getChild(d_child_counter)->reset(d_tgt);
2144 : : }
2145 : : else
2146 : : {
2147 : 7836 : success = true;
2148 : : }
2149 : : }
2150 : : else
2151 : : {
2152 : 440384 : d_child_counter--;
2153 : : }
2154 : : }
2155 : : else
2156 : : {
2157 : : // one child must match
2158 [ + + ]: 87180 : if (!getChild(d_child_counter)->getNextMatch())
2159 : : {
2160 [ + + ]: 68249 : if (d_child_counter < (int)(getNumChildren() - 1))
2161 : : {
2162 : 36306 : d_child_counter++;
2163 [ + - ]: 72612 : Trace("qcf-match-debug")
2164 : 0 : << " Reset child " << d_child_counter << " of " << d_n
2165 : 36306 : << ", one match" << std::endl;
2166 : 36306 : getChild(d_child_counter)->reset(d_tgt);
2167 : : }
2168 : : else
2169 : : {
2170 : 31943 : d_child_counter = -1;
2171 : : }
2172 : : }
2173 : : else
2174 : : {
2175 : 18931 : success = true;
2176 : : }
2177 : : }
2178 : : }
2179 [ + + ]: 258518 : else if (d_n.getKind() == Kind::EQUAL)
2180 : : {
2181 : : // construct match based on both children
2182 [ + + ]: 226531 : if (d_child_counter % 2 == 0)
2183 : : {
2184 [ + + ]: 221479 : if (getChild(0)->getNextMatch())
2185 : : {
2186 : 49404 : d_child_counter++;
2187 : 49404 : getChild(1)->reset(d_child_counter == 1);
2188 : : }
2189 : : else
2190 : : {
2191 [ + + ]: 172075 : if (d_child_counter == 0)
2192 : : {
2193 : 86225 : d_child_counter = 2;
2194 : 86225 : getChild(0)->reset(!d_tgt);
2195 : : }
2196 : : else
2197 : : {
2198 : 85850 : d_child_counter = -1;
2199 : : }
2200 : : }
2201 : : }
2202 [ + + ][ + + ]: 226531 : if (d_child_counter >= 0 && d_child_counter % 2 == 1)
2203 : : {
2204 [ + + ]: 54456 : if (getChild(1)->getNextMatch())
2205 : : {
2206 : 5828 : success = true;
2207 : : }
2208 : : else
2209 : : {
2210 : 48628 : d_child_counter--;
2211 : : }
2212 : : }
2213 : : }
2214 [ + + ]: 31987 : else if (d_n.getKind() == Kind::ITE)
2215 : : {
2216 [ + + ]: 28686 : if (d_child_counter % 2 == 0)
2217 : : {
2218 [ + + ]: 28657 : int index1 = d_child_counter == 4 ? 1 : 0;
2219 [ + + ]: 28657 : if (getChild(index1)->getNextMatch())
2220 : : {
2221 : 18442 : d_child_counter++;
2222 : 18442 : getChild(d_child_counter == 5
2223 : 18431 : ? 2
2224 [ + + ]: 18431 : : (d_tgt == (d_child_counter == 1) ? 1 : 2))
2225 [ + + ]: 36873 : ->reset(d_tgt);
2226 : : }
2227 : : else
2228 : : {
2229 [ + + ]: 10215 : if (d_child_counter == 4)
2230 : : {
2231 : 3393 : d_child_counter = -1;
2232 : : }
2233 : : else
2234 : : {
2235 : 6822 : d_child_counter += 2;
2236 : 6822 : getChild(d_child_counter == 2 ? 0 : 1)
2237 [ + + ]: 6822 : ->reset(d_child_counter == 2 ? !d_tgt : d_tgt);
2238 : : }
2239 : : }
2240 : : }
2241 [ + + ][ + + ]: 28686 : if (d_child_counter >= 0 && d_child_counter % 2 == 1)
2242 : : {
2243 : 36942 : int index2 = d_child_counter == 5
2244 [ + + ]: 36931 : ? 2
2245 [ + + ]: 18460 : : (d_tgt == (d_child_counter == 1) ? 1 : 2);
2246 [ + + ]: 18471 : if (getChild(index2)->getNextMatch())
2247 : : {
2248 : 243 : success = true;
2249 : : }
2250 : : else
2251 : : {
2252 : 18228 : d_child_counter--;
2253 : : }
2254 : : }
2255 : : }
2256 [ + - ]: 3301 : else if (d_n.getKind() == Kind::FORALL)
2257 : : {
2258 [ + + ]: 3301 : if (getChild(d_child_counter)->getNextMatch())
2259 : : {
2260 : 975 : success = true;
2261 : : }
2262 : : else
2263 : : {
2264 : 2326 : d_child_counter = -1;
2265 : : }
2266 : : }
2267 : : }
2268 : 292666 : d_wasSet = success;
2269 [ + - ]: 585332 : Trace("qcf-match") << " ...finished construct match for " << d_n
2270 : 292666 : << ", success = " << success << std::endl;
2271 : 292666 : return success;
2272 : : }
2273 : : }
2274 [ + - ]: 34762 : Trace("qcf-match") << " ...already finished for " << d_n << std::endl;
2275 : 34762 : return false;
2276 : : }
2277 : :
2278 : 7437376 : bool MatchGen::doMatching()
2279 : : {
2280 [ + + ]: 7437376 : if (d_qn.empty())
2281 : : {
2282 : 997902 : return false;
2283 : : }
2284 [ + + ]: 6439474 : if (d_qn[0] == nullptr)
2285 : : {
2286 : 711729 : d_qn.clear();
2287 : 711729 : return true;
2288 : : }
2289 [ - + ][ - + ]: 5727745 : Assert(d_type == typ_var);
[ - - ]
2290 [ - + ][ - + ]: 5727745 : Assert(d_qni_size > 0);
[ - - ]
2291 : : bool invalidMatch;
2292 : : do
2293 : : {
2294 : 28603075 : invalidMatch = false;
2295 [ + - ]: 57206150 : Trace("qcf-match-debug") << " Do matching " << d_n << " "
2296 : 28603075 : << d_qn.size() << " " << d_qni.size() << std::endl;
2297 [ + + ]: 28603075 : if (d_qn.size() == d_qni.size() + 1)
2298 : : {
2299 : 12585068 : size_t index = d_qni.size();
2300 : : // initialize
2301 : 12585068 : TNode val;
2302 : 12585068 : std::map<size_t, size_t>::iterator itv = d_qni_var_num.find(index);
2303 [ + + ]: 12585068 : if (itv != d_qni_var_num.end())
2304 : : {
2305 : : // get the representative variable this variable is equal to
2306 : 12165747 : size_t repVar = d_qi->getCurrentRepVar(itv->second);
2307 [ + - ]: 24331494 : Trace("qcf-match-debug")
2308 : 0 : << " Match " << index << " is a variable " << itv->second
2309 : 12165747 : << ", which is repVar " << repVar << std::endl;
2310 : : // get the value the rep variable
2311 [ + + ]: 12165747 : if (!d_qi->d_match[repVar].isNull())
2312 : : {
2313 : 7566999 : val = d_qi->d_match[repVar];
2314 [ + - ]: 15133998 : Trace("qcf-match-debug")
2315 : 7566999 : << " Variable is already bound to " << val << std::endl;
2316 : : }
2317 : : else
2318 : : {
2319 : : // binding a variable
2320 : 4598748 : d_qni_bound[index] = repVar;
2321 : 4598748 : std::map<TNode, TNodeTrie>::iterator it = d_qn[index]->d_data.begin();
2322 [ + - ]: 4598748 : if (it != d_qn[index]->d_data.end())
2323 : : {
2324 : 4598748 : d_qni.push_back(it);
2325 : : // set the match
2326 [ + + ][ - - ]: 9197496 : if (it->first.getType() == d_qi->d_var_types[repVar]
2327 [ + - ][ + + ]: 9197496 : && d_qi->setMatch(d_qni_bound[index], it->first, true, true))
[ + - ][ + - ]
[ - - ]
2328 : : {
2329 [ + - ]: 4689614 : Trace("qcf-match-debug")
2330 : 2344807 : << " Binding variable" << std::endl;
2331 [ + + ]: 2344807 : if (d_qn.size() < d_qni_size)
2332 : : {
2333 : 752536 : d_qn.push_back(&it->second);
2334 : : }
2335 : : }
2336 : : else
2337 : : {
2338 [ + - ]: 4507882 : Trace("qcf-match")
2339 : 2253941 : << " Binding variable, currently fail." << std::endl;
2340 : 2253941 : invalidMatch = true;
2341 : : }
2342 : : }
2343 : : else
2344 : : {
2345 [ - - ]: 0 : Trace("qcf-match-debug")
2346 : 0 : << " Binding variable, fail, no more variables to bind"
2347 : 0 : << std::endl;
2348 : 0 : d_qn.pop_back();
2349 : : }
2350 : : }
2351 : : }
2352 : : else
2353 : : {
2354 [ + - ]: 838642 : Trace("qcf-match-debug")
2355 : 419321 : << " Match " << index << " is ground term" << std::endl;
2356 [ - + ][ - + ]: 419321 : Assert(d_qni_gterm.find(index) != d_qni_gterm.end());
[ - - ]
2357 : 419321 : val = d_qni_gterm[index];
2358 [ - + ][ - + ]: 419321 : Assert(!val.isNull());
[ - - ]
2359 : : }
2360 [ + + ]: 12585068 : if (!val.isNull())
2361 : : {
2362 : 15972640 : Node valr = d_parent->getRepresentative(val);
2363 : : // constrained by val
2364 : : std::map<TNode, TNodeTrie>::iterator it =
2365 : 7986320 : d_qn[index]->d_data.find(valr);
2366 [ + + ]: 7986320 : if (it != d_qn[index]->d_data.end())
2367 : : {
2368 [ + - ]: 4103534 : Trace("qcf-match-debug") << " Match" << std::endl;
2369 : 4103534 : d_qni.push_back(it);
2370 [ + + ]: 4103534 : if (d_qn.size() < d_qni_size)
2371 : : {
2372 : 3989850 : d_qn.push_back(&it->second);
2373 : : }
2374 : : }
2375 : : else
2376 : : {
2377 [ + - ]: 3882786 : Trace("qcf-match-debug") << " Failed to match" << std::endl;
2378 : 3882786 : d_qn.pop_back();
2379 : : }
2380 : 7986320 : }
2381 : 12585068 : }
2382 : : else
2383 : : {
2384 [ - + ][ - + ]: 16018007 : Assert(d_qn.size() == d_qni.size());
[ - - ]
2385 : 16018007 : size_t index = d_qni.size() - 1;
2386 : : // increment if binding this variable
2387 : 16018007 : bool success = false;
2388 : 16018007 : std::map<size_t, size_t>::iterator itb = d_qni_bound.find(index);
2389 [ + + ]: 16018007 : if (itb != d_qni_bound.end())
2390 : : {
2391 : 11936088 : d_qni[index]++;
2392 [ + + ]: 11936088 : if (d_qni[index] != d_qn[index]->d_data.end())
2393 : : {
2394 : 7347955 : success = true;
2395 [ + + ]: 7347955 : if (d_qi->setMatch(itb->second, d_qni[index]->first, true, true))
2396 : : {
2397 [ + - ]: 12204244 : Trace("qcf-match-debug")
2398 : 6102122 : << " Bind next variable" << std::endl;
2399 [ + + ]: 6102122 : if (d_qn.size() < d_qni_size)
2400 : : {
2401 : 4958002 : d_qn.push_back(&d_qni[index]->second);
2402 : : }
2403 : : }
2404 : : else
2405 : : {
2406 [ + - ]: 2491666 : Trace("qcf-match-debug")
2407 : 1245833 : << " Bind next variable, currently fail" << std::endl;
2408 : 1245833 : invalidMatch = true;
2409 : : }
2410 : : }
2411 : : else
2412 : : {
2413 : 4588133 : d_qi->unsetMatch(itb->second);
2414 : 4588133 : d_qi->d_match_term[itb->second] = TNode::null();
2415 [ + - ]: 9176266 : Trace("qcf-match-debug")
2416 : 0 : << " Bind next variable, no more variables to bind"
2417 : 4588133 : << std::endl;
2418 : : }
2419 : : }
2420 : : else
2421 : : {
2422 : : // TODO : if it equal to something else, also try that
2423 : : }
2424 : : // if not incrementing, move to next
2425 [ + + ]: 16018007 : if (!success)
2426 : : {
2427 : 8670052 : d_qn.pop_back();
2428 : 8670052 : d_qni.pop_back();
2429 : : }
2430 : : }
2431 [ + + ][ + + ]: 28603075 : } while ((!d_qn.empty() && d_qni.size() != d_qni_size) || invalidMatch);
[ + + ][ + + ]
2432 [ + + ]: 5727745 : if (d_qni.size() == d_qni_size)
2433 : : {
2434 [ - + ][ - + ]: 2850075 : Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty());
[ - - ]
2435 : 2850075 : TNode t = d_qni[d_qni.size() - 1]->second.d_data.begin()->first;
2436 [ + - ]: 5700150 : Trace("qcf-match-debug")
2437 : 2850075 : << " " << d_n << " matched " << t << std::endl;
2438 : 2850075 : d_qi->d_match_term[d_qni_var_num[0]] = t;
2439 : : // set the match terms
2440 : 2850075 : Node q = d_qi->getQuantifiedFormula();
2441 [ + + ]: 8654416 : for (const std::pair<const size_t, size_t>& qb : d_qni_bound)
2442 : : {
2443 [ + - ]: 11608682 : Trace("qcf-match-debug")
2444 : 0 : << " position " << qb.first << " bounded " << qb.second << " / "
2445 [ - + ][ - - ]: 5804341 : << q[0].getNumChildren() << std::endl;
2446 [ + + ]: 5804341 : if (qb.first > 0)
2447 : : {
2448 [ - + ][ - + ]: 3625411 : Assert(!d_qi->d_match[qb.second].isNull());
[ - - ]
2449 [ - + ][ - + ]: 3625411 : Assert(d_parent->areEqual(t[qb.first - 1], d_qi->d_match[qb.second]));
[ - - ]
2450 : 3625411 : d_qi->d_match_term[qb.second] = t[qb.first - 1];
2451 : : }
2452 : : }
2453 : 2850075 : }
2454 : 5727745 : return !d_qn.empty();
2455 : : }
2456 : :
2457 : 14011708 : void MatchGen::debugPrintType(CVC5_UNUSED const char* c, short typ)
2458 : : {
2459 [ + + ][ + + ]: 14011708 : switch (typ)
[ + + ][ + + ]
2460 : : {
2461 [ + - ]: 17359 : case typ_invalid: Trace(c) << "invalid"; break;
2462 [ + - ]: 2140 : case typ_ground: Trace(c) << "ground"; break;
2463 [ + - ]: 1599705 : case typ_eq: Trace(c) << "eq"; break;
2464 [ + - ]: 1476379 : case typ_pred: Trace(c) << "pred"; break;
2465 [ + - ]: 674675 : case typ_formula: Trace(c) << "formula"; break;
2466 [ + - ]: 10215419 : case typ_var: Trace(c) << "var"; break;
2467 [ + - ]: 13507 : case typ_bool_var: Trace(c) << "bool_var"; break;
2468 : : }
2469 : 14011708 : }
2470 : :
2471 : 12483 : void MatchGen::setInvalid()
2472 : : {
2473 : 12483 : d_type = typ_invalid;
2474 : 12483 : d_children.clear();
2475 : 12483 : }
2476 : :
2477 : 551234 : bool MatchGen::isHandledBoolConnective(TNode n)
2478 : : {
2479 [ + + ][ + + ]: 551234 : return TermUtil::isBoolConnectiveTerm(n) && n.getKind() != Kind::SEP_STAR;
[ + - ][ - - ]
2480 : : }
2481 : :
2482 : 3648993 : bool MatchGen::isHandledUfTerm(TNode n)
2483 : : {
2484 : 3648993 : return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
2485 : : }
2486 : :
2487 : 0 : bool MatchGen::isHandled(TNode n)
2488 : : {
2489 : 0 : if (n.getKind() != Kind::BOUND_VARIABLE && expr::hasBoundVar(n))
2490 : : {
2491 : 0 : if (!isHandledBoolConnective(n) && !isHandledUfTerm(n)
2492 : 0 : && n.getKind() != Kind::EQUAL && n.getKind() != Kind::ITE)
2493 : : {
2494 : 0 : return false;
2495 : : }
2496 [ - - ]: 0 : for (unsigned i = 0; i < n.getNumChildren(); i++)
2497 : : {
2498 [ - - ]: 0 : if (!isHandled(n[i]))
2499 : : {
2500 : 0 : return false;
2501 : : }
2502 : : }
2503 : : }
2504 : 0 : return true;
2505 : : }
2506 : :
2507 : 13099 : QuantConflictFind::QuantConflictFind(Env& env,
2508 : : QuantifiersState& qs,
2509 : : QuantifiersInferenceManager& qim,
2510 : : QuantifiersRegistry& qr,
2511 : 13099 : TermRegistry& tr)
2512 : : : QuantifiersModule(env, qs, qim, qr, tr),
2513 : 13099 : d_statistics(statisticsRegistry()),
2514 : 26198 : d_effort(EFFORT_INVALID)
2515 : : {
2516 : 13099 : }
2517 : :
2518 : : //-------------------------------------------------- registration
2519 : :
2520 : 49047 : void QuantConflictFind::registerQuantifier(Node q)
2521 : : {
2522 [ + + ]: 49047 : if (!d_qreg.hasOwnership(q, this))
2523 : : {
2524 : 1506 : return;
2525 : : }
2526 : 47541 : d_quants.push_back(q);
2527 : 47541 : d_quant_id[q] = d_quants.size();
2528 [ - + ]: 47541 : if (TraceIsOn("qcf-qregister"))
2529 : : {
2530 [ - - ]: 0 : Trace("qcf-qregister") << "Register ";
2531 : 0 : debugPrintQuant("qcf-qregister", q);
2532 [ - - ]: 0 : Trace("qcf-qregister") << " : " << q << std::endl;
2533 : : }
2534 : : // make QcfNode structure
2535 [ + - ]: 95082 : Trace("qcf-qregister")
2536 : 0 : << "- Get relevant equality/disequality pairs, calculate flattening..."
2537 : 47541 : << std::endl;
2538 : 47541 : d_qinfo[q].reset(new QuantInfo(d_env, d_qstate, d_treg, this, q));
2539 : :
2540 : : // debug print
2541 [ - + ]: 47541 : if (TraceIsOn("qcf-qregister"))
2542 : : {
2543 : 0 : QuantInfo* qi = d_qinfo[q].get();
2544 [ - - ]: 0 : Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
2545 [ - - ]: 0 : Trace("qcf-qregister") << " ";
2546 : 0 : debugPrintQuantBody("qcf-qregister", q, q[1]);
2547 [ - - ]: 0 : Trace("qcf-qregister") << std::endl;
2548 [ - - ]: 0 : if (qi->d_vars.size() > q[0].getNumChildren())
2549 : : {
2550 [ - - ]: 0 : Trace("qcf-qregister") << " with additional constraints : " << std::endl;
2551 : 0 : for (size_t j = q[0].getNumChildren(), nvars = qi->d_vars.size();
2552 [ - - ]: 0 : j < nvars;
2553 : : j++)
2554 : : {
2555 [ - - ]: 0 : Trace("qcf-qregister") << " ?x" << j << " = ";
2556 : 0 : debugPrintQuantBody("qcf-qregister", q, qi->d_vars[j], false);
2557 [ - - ]: 0 : Trace("qcf-qregister") << std::endl;
2558 : : }
2559 : : }
2560 [ - - ]: 0 : Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
2561 : : }
2562 : : }
2563 : :
2564 : : //-------------------------------------------------- check function
2565 : :
2566 : 101420 : bool QuantConflictFind::needsCheck(Theory::Effort level)
2567 : : {
2568 [ + + ][ + + ]: 101420 : return !d_qstate.isConflictingInst() && (level == Theory::EFFORT_FULL);
2569 : : }
2570 : :
2571 : 39835 : void QuantConflictFind::reset_round(CVC5_UNUSED Theory::Effort level)
2572 : : {
2573 [ + - ]: 39835 : Trace("qcf-check") << "QuantConflictFind::reset_round" << std::endl;
2574 [ + - ]: 39835 : Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
2575 : 39835 : d_eqcs.clear();
2576 : :
2577 : 39835 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine());
2578 : 39835 : TermDb* tdb = getTermDatabase();
2579 [ + + ]: 2635213 : while (!eqcs_i.isFinished())
2580 : : {
2581 : 2595378 : Node r = (*eqcs_i);
2582 [ + + ]: 2595378 : if (tdb->hasTermCurrent(r))
2583 : : {
2584 : 1791793 : TypeNode rtn = r.getType();
2585 : : // check regardless of options
2586 [ + + ]: 1791793 : if (!TermUtil::hasInstConstAttr(r))
2587 : : {
2588 : 1654118 : d_eqcs[rtn].push_back(r);
2589 : : }
2590 : 1791793 : }
2591 : 2595378 : ++eqcs_i;
2592 : 2595378 : }
2593 : 39835 : }
2594 : :
2595 : 266356 : void QuantConflictFind::setIrrelevantFunction(TNode f)
2596 : : {
2597 [ + + ]: 266356 : if (d_irr_func.find(f) == d_irr_func.end())
2598 : : {
2599 : 34996 : d_irr_func[f] = true;
2600 : 34996 : std::map<TNode, std::vector<Node>>::iterator it = d_func_rel_dom.find(f);
2601 [ + + ]: 34996 : if (it != d_func_rel_dom.end())
2602 : : {
2603 [ + + ]: 125267 : for (unsigned j = 0; j < it->second.size(); j++)
2604 : : {
2605 : 100077 : d_irr_quant[it->second[j]] = true;
2606 : : }
2607 : : }
2608 : : }
2609 : 266356 : }
2610 : :
2611 : : namespace {
2612 : :
2613 : : // Returns the beginning of a range of efforts. The range can be iterated
2614 : : // through as unsigned using operator++.
2615 : 31345 : inline QuantConflictFind::Effort QcfEffortStart()
2616 : : {
2617 : 31345 : return QuantConflictFind::EFFORT_CONFLICT;
2618 : : }
2619 : :
2620 : : // Returns the beginning of a range of efforts. The value returned is included
2621 : : // in the range.
2622 : 31345 : inline QuantConflictFind::Effort QcfEffortEnd(options::QcfMode m)
2623 : : {
2624 [ + - ]: 31345 : return m == options::QcfMode::PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ
2625 : 31345 : : QuantConflictFind::EFFORT_CONFLICT;
2626 : : }
2627 : :
2628 : : } // namespace
2629 : :
2630 : : /** check */
2631 : 111063 : void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
2632 : : {
2633 : 111063 : CodeTimer codeTimer(d_qstate.getStats().d_cbqi_time);
2634 [ + + ]: 111063 : if (quant_e != QEFFORT_CONFLICT)
2635 : : {
2636 : 79718 : return;
2637 : : }
2638 [ + - ]: 31345 : Trace("qcf-check") << "QCF : check : " << level << std::endl;
2639 [ - + ]: 31345 : if (d_qstate.isConflictingInst())
2640 : : {
2641 [ - - ]: 0 : Trace("qcf-check2") << "QCF : finished check : already in conflict."
2642 : 0 : << std::endl;
2643 [ - - ]: 0 : if (level >= Theory::EFFORT_FULL)
2644 : : {
2645 [ - - ]: 0 : Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
2646 : : }
2647 : 0 : return;
2648 : : }
2649 : 31345 : unsigned addedLemmas = 0;
2650 : 31345 : ++(d_statistics.d_inst_rounds);
2651 : 31345 : beginCallDebug();
2652 : 31345 : int prevEt = 0;
2653 [ - + ]: 31345 : if (TraceIsOn("qcf-engine"))
2654 : : {
2655 : 0 : prevEt = d_statistics.d_entailment_checks.get();
2656 [ - - ]: 0 : Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
2657 : 0 : << "---" << std::endl;
2658 : : }
2659 : :
2660 : : // reset the round-specific information
2661 : 31345 : d_irr_func.clear();
2662 : 31345 : d_irr_quant.clear();
2663 : :
2664 [ - + ]: 31345 : if (TraceIsOn("qcf-debug"))
2665 : : {
2666 [ - - ]: 0 : Trace("qcf-debug") << std::endl;
2667 : 0 : debugPrint("qcf-debug");
2668 [ - - ]: 0 : Trace("qcf-debug") << std::endl;
2669 : : }
2670 : 31345 : bool isConflict = false;
2671 : 31345 : FirstOrderModel* fm = d_treg.getModel();
2672 : 31345 : size_t nquant = fm->getNumAssertedQuantifiers();
2673 : : // for each effort level (find conflict, find propagating)
2674 : 31345 : unsigned end = QcfEffortEnd(options().quantifiers.cbqiMode);
2675 [ + + ]: 87618 : for (unsigned e = QcfEffortStart(); e <= end; ++e)
2676 : : {
2677 : : // set the effort (data member for convienence of access)
2678 : 60016 : d_effort = static_cast<Effort>(e);
2679 [ + - ]: 120032 : Trace("qcf-check") << "Checking quantified formulas at effort " << e
2680 : 60016 : << "..." << std::endl;
2681 : : // for each quantified formula
2682 [ + + ]: 613015 : for (size_t i = 0; i < nquant; i++)
2683 : : {
2684 : 555673 : Node q = fm->getAssertedQuantifier(i, true);
2685 [ + + ][ - - ]: 555673 : if (d_qreg.hasOwnership(q, this)
2686 [ + + ]: 543646 : && d_irr_quant.find(q) == d_irr_quant.end()
2687 [ + + ][ + + ]: 1099319 : && fm->isQuantifierActive(q))
[ + + ][ + - ]
[ - - ]
2688 : : {
2689 : : // check this quantified formula
2690 : 434161 : checkQuantifiedFormula(q, isConflict, addedLemmas);
2691 [ + + ][ + + ]: 434161 : if (d_qstate.isConflictingInst() || d_qstate.isInConflict())
[ + + ]
2692 : : {
2693 : 2674 : break;
2694 : : }
2695 : : }
2696 [ + + ]: 555673 : }
2697 : : // We are done if we added a lemma, or discovered a conflict in another
2698 : : // way. An example of the latter case is when two disequal congruent terms
2699 : : // are discovered during term indexing.
2700 [ + + ][ + + ]: 60016 : if (addedLemmas > 0 || d_qstate.isInConflict())
[ + + ]
2701 : : {
2702 : 3743 : break;
2703 : : }
2704 : : }
2705 [ - + ]: 31345 : if (isConflict)
2706 : : {
2707 : 0 : d_qstate.notifyConflictingInst();
2708 : : }
2709 [ - + ]: 31345 : if (TraceIsOn("qcf-engine"))
2710 : : {
2711 [ - - ]: 0 : Trace("qcf-engine") << "Finished conflict find engine";
2712 [ - - ]: 0 : if (addedLemmas > 0)
2713 : : {
2714 [ - - ]: 0 : Trace("qcf-engine") << ", effort = "
2715 : 0 : << (d_effort == EFFORT_CONFLICT
2716 [ - - ]: 0 : ? "conflict"
2717 [ - - ]: 0 : : (d_effort == EFFORT_PROP_EQ ? "prop_eq"
2718 : 0 : : "mc"));
2719 [ - - ]: 0 : Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
2720 : : }
2721 [ - - ]: 0 : Trace("qcf-engine") << std::endl;
2722 : 0 : int currEt = d_statistics.d_entailment_checks.get();
2723 [ - - ]: 0 : if (currEt != prevEt)
2724 : : {
2725 [ - - ]: 0 : Trace("qcf-engine") << " Entailment checks = " << (currEt - prevEt)
2726 : 0 : << std::endl;
2727 : : }
2728 : : }
2729 [ + - ]: 31345 : Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
2730 : 31345 : endCallDebug();
2731 [ + + ]: 111063 : }
2732 : :
2733 : 0 : std::string QuantConflictFind::identify() const { return "cbqi"; }
2734 : :
2735 : 434161 : void QuantConflictFind::checkQuantifiedFormula(Node q,
2736 : : bool& isConflict,
2737 : : unsigned& addedLemmas)
2738 : : {
2739 [ - + ][ - + ]: 434161 : Assert(d_qinfo.find(q) != d_qinfo.end());
[ - - ]
2740 : 434161 : QuantInfo* qi = d_qinfo[q].get();
2741 [ + + ]: 434161 : if (!qi->matchGeneratorIsValid())
2742 : : {
2743 : : // quantified formula is not properly set up for matching
2744 : 165115 : return;
2745 : : }
2746 [ - + ]: 269046 : if (TraceIsOn("qcf-check"))
2747 : : {
2748 [ - - ]: 0 : Trace("qcf-check") << "Check quantified formula ";
2749 : 0 : debugPrintQuant("qcf-check", q);
2750 [ - - ]: 0 : Trace("qcf-check") << " : " << q << "..." << std::endl;
2751 : : }
2752 : :
2753 [ + - ]: 269046 : Trace("qcf-check-debug") << "Reset round..." << std::endl;
2754 [ - + ]: 269046 : if (!qi->reset_round())
2755 : : {
2756 : : // it is typically the case that another conflict (e.g. in the term
2757 : : // database) was discovered if we fail here.
2758 : 0 : return;
2759 : : }
2760 : : // try to make a matches making the body false or propagating
2761 [ + - ]: 269046 : Trace("qcf-check-debug") << "Get next match..." << std::endl;
2762 : 269046 : Instantiate* qinst = d_qim.getInstantiate();
2763 [ + + ]: 301883 : while (qi->getNextMatch())
2764 : : {
2765 [ - + ]: 35867 : if (d_qstate.isInConflict())
2766 : : {
2767 [ - - ]: 0 : Trace("qcf-check") << " ... Quantifiers engine discovered conflict, ";
2768 [ - - ]: 0 : Trace("qcf-check") << "probably related to disequal congruent terms in "
2769 : 0 : "master equality engine"
2770 : 0 : << std::endl;
2771 : 3030 : return;
2772 : : }
2773 [ - + ]: 35867 : if (TraceIsOn("qcf-inst"))
2774 : : {
2775 [ - - ]: 0 : Trace("qcf-inst") << "*** Produced match at effort " << d_effort << " : "
2776 : 0 : << std::endl;
2777 : 0 : qi->debugPrintMatch("qcf-inst");
2778 [ - - ]: 0 : Trace("qcf-inst") << std::endl;
2779 : : }
2780 : : // check whether internal match constraints are satisfied
2781 [ + + ]: 35867 : if (qi->isMatchSpurious())
2782 : : {
2783 [ + - ]: 8560 : Trace("qcf-inst") << " ... Spurious (match is inconsistent)"
2784 : 4280 : << std::endl;
2785 : 5287 : continue;
2786 : : }
2787 : : // check whether match can be completed
2788 : 31587 : std::vector<size_t> assigned;
2789 [ + + ]: 31587 : if (!qi->completeMatch(assigned))
2790 : : {
2791 [ + - ]: 2014 : Trace("qcf-inst") << " ... Spurious (cannot assign unassigned vars)"
2792 : 1007 : << std::endl;
2793 : 1007 : continue;
2794 : : }
2795 : : // check whether the match is spurious according to (T-)entailment checks
2796 : 30580 : std::vector<Node> terms;
2797 : 30580 : qi->getMatch(terms);
2798 : 30580 : bool tcs = qi->isTConstraintSpurious(terms);
2799 [ + + ]: 30580 : if (tcs)
2800 : : {
2801 [ + - ]: 47372 : Trace("qcf-inst") << " ... Spurious (match is T-inconsistent)"
2802 : 23686 : << std::endl;
2803 : : }
2804 : : else
2805 : : {
2806 : : // otherwise, we have a conflict/propagating instance
2807 : : // for debugging
2808 [ - + ]: 6894 : if (TraceIsOn("qcf-check-inst"))
2809 : : {
2810 : 0 : Node inst = qinst->getInstantiation(q, terms);
2811 [ - - ]: 0 : Trace("qcf-check-inst")
2812 : 0 : << "Check instantiation " << inst << "..." << std::endl;
2813 : 0 : Assert(!d_treg.getEntailmentCheck()->isEntailed(inst, true));
2814 : 0 : Assert(d_treg.getEntailmentCheck()->isEntailed(inst, false)
2815 : : || d_effort > EFFORT_CONFLICT);
2816 : 0 : }
2817 : : // Process the lemma: either add an instantiation or specific lemmas
2818 : : // constructed during the isTConstraintSpurious call, or both.
2819 : 13788 : InferenceId id = (d_effort == EFFORT_CONFLICT
2820 [ + + ]: 6894 : ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT
2821 : : : InferenceId::QUANTIFIERS_INST_CBQI_PROP);
2822 [ + + ]: 6894 : if (!qinst->addInstantiation(q, terms, id))
2823 : : {
2824 [ + - ]: 405 : Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
2825 : : // This should only happen if the algorithm generates the same
2826 : : // propagating instance twice this round. In this case, return
2827 : : // to avoid exponential behavior.
2828 : 405 : return;
2829 : : }
2830 [ + - ]: 6489 : Trace("qcf-check") << " ... Added instantiation" << std::endl;
2831 [ - + ]: 6489 : if (TraceIsOn("qcf-instantiate"))
2832 : : {
2833 [ - - ]: 0 : Trace("qcf-instantiate") << "QCF instantiation: " << q << std::endl;
2834 [ - - ]: 0 : for (const Node& t : terms)
2835 : : {
2836 [ - - ]: 0 : Trace("qcf-instantiate") << " " << t << std::endl;
2837 : : }
2838 : : }
2839 [ - + ]: 6489 : if (TraceIsOn("qcf-inst"))
2840 : : {
2841 [ - - ]: 0 : Trace("qcf-inst") << "*** Was from effort " << d_effort << " : "
2842 : 0 : << std::endl;
2843 : 0 : qi->debugPrintMatch("qcf-inst");
2844 [ - - ]: 0 : Trace("qcf-inst") << std::endl;
2845 : : }
2846 : 6489 : ++addedLemmas;
2847 [ + + ]: 6489 : if (d_effort == EFFORT_CONFLICT)
2848 : : {
2849 : : // mark relevant: this ensures that quantified formula q is
2850 : : // checked first on the next round. This is an optimization to
2851 : : // ensure that quantified formulas that are more likely to have
2852 : : // conflicting instances are checked earlier.
2853 : 2625 : d_treg.getModel()->markRelevant(q);
2854 [ - + ]: 2625 : if (options().quantifiers.cbqiAllConflict)
2855 : : {
2856 : 0 : isConflict = true;
2857 : : }
2858 : : else
2859 : : {
2860 : 2625 : d_qstate.notifyConflictingInst();
2861 : : }
2862 : 2625 : return;
2863 : : }
2864 [ + - ]: 3864 : else if (d_effort == EFFORT_PROP_EQ)
2865 : : {
2866 : 3864 : d_treg.getModel()->markRelevant(q);
2867 : : }
2868 : : }
2869 : : // clean up assigned
2870 : 27550 : qi->revertMatch(assigned);
2871 : 27550 : d_tempCache.clear();
2872 [ + + ][ + + ]: 34617 : }
[ + ]
2873 [ + - ]: 532032 : Trace("qcf-check") << "Done, conflict = " << d_qstate.isConflictingInst()
2874 : 266016 : << std::endl;
2875 : : }
2876 : :
2877 : : //-------------------------------------------------- debugging
2878 : :
2879 : 0 : void QuantConflictFind::debugPrint(CVC5_UNUSED const char* c) const
2880 : : {
2881 : : // print the equivalance classes
2882 [ - - ]: 0 : Trace(c) << "----------EQ classes" << std::endl;
2883 : 0 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine());
2884 [ - - ]: 0 : while (!eqcs_i.isFinished())
2885 : : {
2886 : 0 : Node n = (*eqcs_i);
2887 : : // if( !n.getType().isInteger() ){
2888 [ - - ]: 0 : Trace(c) << " - " << n << " : {";
2889 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator(n, getEqualityEngine());
2890 : 0 : bool pr = false;
2891 [ - - ]: 0 : while (!eqc_i.isFinished())
2892 : : {
2893 : 0 : Node nn = (*eqc_i);
2894 : 0 : if (nn.getKind() != Kind::EQUAL && nn != n)
2895 : : {
2896 : 0 : Trace(c) << (pr ? "," : "") << " " << nn;
2897 : 0 : pr = true;
2898 : : }
2899 : 0 : ++eqc_i;
2900 : 0 : }
2901 : 0 : Trace(c) << (pr ? " " : "") << "}" << std::endl;
2902 : 0 : ++eqcs_i;
2903 : 0 : }
2904 : 0 : }
2905 : :
2906 : 0 : void QuantConflictFind::debugPrintQuant(CVC5_UNUSED const char* c, Node q) const
2907 : : {
2908 : 0 : std::map<Node, size_t>::const_iterator it = d_quant_id.find(q);
2909 [ - - ]: 0 : if (it == d_quant_id.end())
2910 : : {
2911 [ - - ]: 0 : Trace(c) << q;
2912 : 0 : return;
2913 : : }
2914 [ - - ]: 0 : Trace(c) << "Q" << it->second;
2915 : : }
2916 : :
2917 : 0 : void QuantConflictFind::debugPrintQuantBody(const char* c,
2918 : : Node q,
2919 : : Node n,
2920 : : bool doVarNum) const
2921 : : {
2922 [ - - ]: 0 : if (n.getNumChildren() == 0)
2923 : : {
2924 [ - - ]: 0 : Trace(c) << n;
2925 : 0 : return;
2926 : : }
2927 : : std::map<Node, std::unique_ptr<QuantInfo>>::const_iterator itq =
2928 : 0 : d_qinfo.find(q);
2929 [ - - ]: 0 : if (itq != d_qinfo.end())
2930 : : {
2931 : 0 : const QuantInfo* qi = itq->second.get();
2932 : 0 : std::map<TNode, size_t>::const_iterator itv = qi->d_var_num.find(n);
2933 [ - - ][ - - ]: 0 : if (doVarNum && itv != qi->d_var_num.end())
[ - - ]
2934 : : {
2935 [ - - ]: 0 : Trace(c) << "?x" << itv->second;
2936 : 0 : return;
2937 : : }
2938 : : }
2939 [ - - ]: 0 : Trace(c) << "(";
2940 [ - - ]: 0 : if (n.getKind() == Kind::APPLY_UF)
2941 : : {
2942 : 0 : Trace(c) << n.getOperator();
2943 : : }
2944 : : else
2945 : : {
2946 [ - - ]: 0 : Trace(c) << n.getKind();
2947 : : }
2948 [ - - ]: 0 : for (const Node& nc : n)
2949 : : {
2950 [ - - ]: 0 : Trace(c) << " ";
2951 : 0 : debugPrintQuantBody(c, q, nc);
2952 : 0 : }
2953 [ - - ]: 0 : Trace(c) << ")";
2954 : : }
2955 : :
2956 : 13099 : QuantConflictFind::Statistics::Statistics(StatisticsRegistry& sr)
2957 : 13099 : : d_inst_rounds(sr.registerInt("QuantConflictFind::Inst_Rounds")),
2958 : : d_entailment_checks(
2959 : 13099 : sr.registerInt("QuantConflictFind::Entailment_Checks"))
2960 : : {
2961 : 13099 : }
2962 : :
2963 : 40 : TNode QuantConflictFind::getZero(TypeNode tn, Kind k)
2964 : : {
2965 : 40 : std::pair<TypeNode, Kind> key(tn, k);
2966 : 40 : std::map<std::pair<TypeNode, Kind>, Node>::iterator it = d_zero.find(key);
2967 [ + + ]: 40 : if (it == d_zero.end())
2968 : : {
2969 : 16 : Node nn;
2970 [ + + ]: 16 : if (k == Kind::ADD)
2971 : : {
2972 : 9 : nn = nodeManager()->mkConstRealOrInt(tn, Rational(0));
2973 : : }
2974 : 16 : d_zero[key] = nn;
2975 : 16 : return nn;
2976 : 16 : }
2977 : 24 : return it->second;
2978 : 40 : }
2979 : :
2980 : 0 : std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e)
2981 : : {
2982 [ - - ][ - - ]: 0 : switch (e)
2983 : : {
2984 : 0 : case QuantConflictFind::EFFORT_INVALID: os << "Invalid"; break;
2985 : 0 : case QuantConflictFind::EFFORT_CONFLICT: os << "Conflict"; break;
2986 : 0 : case QuantConflictFind::EFFORT_PROP_EQ: os << "PropEq"; break;
2987 : : }
2988 : 0 : return os;
2989 : : }
2990 : :
2991 : 107 : bool QuantConflictFind::isPropagatingInstance(Node n) const
2992 : : {
2993 : 107 : std::unordered_set<TNode> visited;
2994 : 107 : std::vector<TNode> visit;
2995 : 107 : TNode cur;
2996 : 107 : visit.push_back(n);
2997 : : do
2998 : : {
2999 : 229 : cur = visit.back();
3000 : 229 : visit.pop_back();
3001 [ + - ]: 229 : if (visited.find(cur) == visited.end())
3002 : : {
3003 : 229 : visited.insert(cur);
3004 : 229 : Kind ck = cur.getKind();
3005 [ + + ]: 229 : if (ck == Kind::FORALL)
3006 : : {
3007 : : // do nothing
3008 : : }
3009 [ + + ]: 189 : else if (TermUtil::isBoolConnective(ck))
3010 : : {
3011 [ + + ]: 183 : for (TNode cc : cur)
3012 : : {
3013 : 122 : visit.push_back(cc);
3014 : 122 : }
3015 : : }
3016 [ - + ]: 128 : else if (!getEqualityEngine()->hasTerm(cur))
3017 : : {
3018 [ - - ]: 0 : Trace("qcf-instance-check-debug")
3019 : 0 : << "...not propagating instance because of " << cur << " " << ck
3020 : 0 : << std::endl;
3021 : 0 : return false;
3022 : : }
3023 : : }
3024 [ + + ]: 229 : } while (!visit.empty());
3025 : 107 : return true;
3026 : 107 : }
3027 : :
3028 : : } // namespace quantifiers
3029 : : } // namespace theory
3030 : : } // namespace cvc5::internal
|
