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 : 47757 : QuantInfo::QuantInfo(Env& env,
37 : : QuantifiersState& qs,
38 : : TermRegistry& tr,
39 : : QuantConflictFind* p,
40 : 47757 : Node q)
41 : : : EnvObj(env),
42 : 47757 : d_qs(qs),
43 : 47757 : d_parent(p),
44 : 47757 : d_instMatch(env, qs, tr, q),
45 : 47757 : d_mg(nullptr),
46 : 47757 : d_q(q),
47 : 47757 : d_unassigned_nvar(0),
48 : 95514 : d_una_index(0)
49 : : {
50 : 47757 : Node qn = d_q[1];
51 : 47757 : d_extra_var.clear();
52 : :
53 : : //register the variables
54 [ + + ]: 155198 : for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++)
55 : : {
56 : 107441 : Node v = d_q[0][i];
57 : 107441 : d_match.push_back(TNode::null());
58 : 107441 : d_match_term.push_back(TNode::null());
59 : 107441 : d_var_num[v] = i;
60 : 107441 : d_vars.push_back(v);
61 : 107441 : d_var_types.push_back(v.getType());
62 : 107441 : }
63 : :
64 : 47757 : registerNode( qn, true, true );
65 : :
66 [ + - ]: 47757 : Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
67 : 47757 : d_mg = std::make_unique<MatchGen>(d_env, p, this, qn);
68 : :
69 [ + + ]: 47757 : if( d_mg->isValid() ){
70 [ + + ]: 215214 : for (size_t j = q[0].getNumChildren(), nvars = d_vars.size(); j < nvars;
71 : : j++)
72 : : {
73 [ + + ]: 177957 : if (d_vars[j].getKind() != Kind::BOUND_VARIABLE)
74 : : {
75 : 165467 : d_var_mg[j] = nullptr;
76 : 165467 : bool is_tsym = false;
77 [ + + ][ - - ]: 330934 : if (!MatchGen::isHandledUfTerm(d_vars[j])
78 [ + + ][ + + ]: 330934 : && d_vars[j].getKind() != Kind::ITE)
[ + - ]
79 : : {
80 : 1754 : is_tsym = true;
81 : 1754 : d_tsym_vars.push_back( j );
82 : : }
83 [ + + ][ + + ]: 165467 : if (!is_tsym || options().quantifiers.cbqiTConstraint)
[ + + ]
84 : : {
85 : 164434 : d_var_mg[j] = std::make_unique<MatchGen>(d_env, p, this, d_vars[j], true);
86 : : }
87 [ + + ][ + + ]: 165467 : if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
[ + + ]
88 [ + - ]: 9352 : Trace("qcf-invalid")
89 : 4676 : << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
90 : 4676 : d_mg->setInvalid();
91 : 4676 : break;
92 : : }else{
93 : 160791 : std::vector<size_t> bvars;
94 : 160791 : d_var_mg[j]->determineVariableOrder(bvars);
95 : 160791 : }
96 : : }
97 : : }
98 [ + + ]: 41933 : if( d_mg->isValid() ){
99 : 37257 : std::vector<size_t> bvars;
100 : 37257 : d_mg->determineVariableOrder(bvars);
101 : 37257 : }
102 : : }else{
103 [ + - ]: 11648 : Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed."
104 : 5824 : << std::endl;
105 : : }
106 [ + - ]: 95514 : Trace("qcf-qregister-summary")
107 [ - - ]: 47757 : << "QCF register : " << (d_mg->isValid() ? "VALID " : "INVALID") << " : "
108 : 47757 : << q << std::endl;
109 : :
110 [ + + ]: 47757 : if (d_mg->isValid())
111 : : {
112 : : //optimization : record variable argument positions for terms that must be matched
113 : 37257 : std::vector< TNode > vars;
114 : : //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
115 [ - + ]: 37257 : if (options().quantifiers.cbqiSkipRd)
116 : : {
117 [ - - ]: 0 : for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
118 : 0 : vars.push_back( d_vars[j] );
119 : : }
120 : : }
121 : : else
122 : : {
123 : : //get all variables that are always relevant
124 : 37257 : std::map< TNode, bool > visited;
125 : 37257 : getPropagateVars(vars, q[1], false, visited);
126 : 37257 : }
127 [ + + ]: 201196 : for (TNode v : vars)
128 : : {
129 : 327878 : TNode f = p->getTermDatabase()->getMatchOperator( v );
130 [ + + ]: 163939 : if( !f.isNull() ){
131 [ + - ]: 197654 : Trace("qcf-opt") << "Record variable argument positions in " << v
132 : 98827 : << ", op=" << f << "..." << std::endl;
133 [ + + ]: 321883 : for (size_t k = 0, vnchild = v.getNumChildren(); k < vnchild; k++)
134 : : {
135 : 223056 : Node n = v[k];
136 : 223056 : std::map<TNode, size_t>::iterator itv = d_var_num.find(n);
137 [ + + ]: 223056 : if( itv!=d_var_num.end() ){
138 : 191441 : std::vector<size_t>& vrd = d_var_rel_dom[itv->second][f];
139 [ + - ]: 382882 : Trace("qcf-opt")
140 : 191441 : << " arg " << k << " is var #" << itv->second << std::endl;
141 [ + + ]: 191441 : if (std::find(vrd.begin(), vrd.end(), k) == vrd.end())
142 : : {
143 : 179901 : vrd.push_back(k);
144 : : }
145 : : }
146 : 223056 : }
147 : : }
148 : 163939 : }
149 : 37257 : }
150 : 47757 : }
151 : :
152 : 95508 : QuantInfo::~QuantInfo() {}
153 : :
154 : 1899133 : Node QuantInfo::getQuantifiedFormula() const { return d_q; }
155 : :
156 : 0 : QuantifiersInferenceManager& QuantInfo::getInferenceManager()
157 : : {
158 : 0 : Assert(d_parent != nullptr);
159 : 0 : return d_parent->getInferenceManager();
160 : : }
161 : :
162 : 422229 : void QuantInfo::getPropagateVars(std::vector<TNode>& vars,
163 : : TNode n,
164 : : bool pol,
165 : : std::map<TNode, bool>& visited)
166 : : {
167 : 422229 : std::map< TNode, bool >::iterator itv = visited.find( n );
168 [ + + ]: 422229 : if( itv==visited.end() ){
169 : 311608 : visited[n] = true;
170 : 311608 : bool rec = true;
171 : 311608 : bool newPol = pol;
172 [ + + ]: 311608 : if( d_var_num.find( n )!=d_var_num.end() ){
173 [ - + ][ - + ]: 163939 : Assert(std::find(vars.begin(), vars.end(), n) == vars.end());
[ - - ]
174 : 163939 : vars.push_back( n );
175 : 327878 : TNode f = d_parent->getTermDatabase()->getMatchOperator(n);
176 [ + + ]: 163939 : if( !f.isNull() ){
177 : 98827 : std::vector<Node>& rd = d_parent->d_func_rel_dom[f];
178 [ + + ]: 98827 : if (std::find(rd.begin(), rd.end(), d_q) == rd.end())
179 : : {
180 : 75547 : rd.push_back(d_q);
181 : : }
182 : : }
183 [ + + ]: 311608 : }else if( MatchGen::isHandledBoolConnective( n ) ){
184 [ - + ][ - + ]: 59693 : Assert(n.getKind() != Kind::IMPLIES);
[ - - ]
185 : 59693 : QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
186 : : }
187 [ + - ]: 623216 : Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol
188 : 311608 : << ", rec = " << rec << std::endl;
189 [ + + ]: 311608 : if( rec ){
190 [ + + ]: 682401 : for (const Node& nc : n)
191 : : {
192 : 384972 : getPropagateVars(vars, nc, pol, visited);
193 : 384972 : }
194 : : }
195 : : }
196 : 422229 : }
197 : :
198 : 3226539 : bool QuantInfo::isBaseMatchComplete() {
199 : 3226539 : return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var.size());
200 : : }
201 : :
202 : 247952 : void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
203 [ + - ]: 247952 : Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
204 [ + + ]: 247952 : if (n.getKind() == Kind::FORALL)
205 : : {
206 : 11315 : registerNode( n[1], hasPol, pol, true );
207 : : }
208 : : else
209 : : {
210 [ + + ]: 236637 : if( !MatchGen::isHandledBoolConnective( n ) ){
211 [ + + ]: 130316 : if (expr::hasBoundVar(n))
212 : : {
213 : : // literals
214 [ + + ]: 129980 : if (n.getKind() == Kind::EQUAL)
215 : : {
216 [ + + ]: 204315 : for (unsigned i = 0; i < n.getNumChildren(); i++)
217 : : {
218 : 136210 : flatten(n[i], beneathQuant);
219 : : }
220 : : }
221 [ + + ]: 61875 : else if (MatchGen::isHandledUfTerm(n))
222 : : {
223 : 43703 : flatten(n, beneathQuant);
224 : : }
225 [ + + ]: 18172 : else if (n.getKind() == Kind::ITE)
226 : : {
227 [ + + ]: 10182 : for (unsigned i = 1; i <= 2; i++)
228 : : {
229 : 6788 : flatten(n[i], beneathQuant);
230 : : }
231 : 3394 : registerNode(n[0], false, pol, beneathQuant);
232 : : }
233 [ + + ]: 14778 : else if (options().quantifiers.cbqiTConstraint)
234 : : {
235 : : // a theory-specific predicate
236 [ + + ]: 1944 : for (unsigned i = 0; i < n.getNumChildren(); i++)
237 : : {
238 : 1296 : flatten(n[i], beneathQuant);
239 : : }
240 : : }
241 : : }
242 : : }else{
243 [ + + ]: 288413 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
244 : : bool newHasPol;
245 : : bool newPol;
246 : 182092 : QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
247 : 182092 : registerNode( n[i], newHasPol, newPol, beneathQuant );
248 : : }
249 : : }
250 : : }
251 : 247952 : }
252 : :
253 : 595030 : void QuantInfo::flatten( Node n, bool beneathQuant ) {
254 [ + - ]: 595030 : Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
255 [ + + ]: 595030 : if (expr::hasBoundVar(n))
256 : : {
257 [ + + ]: 499047 : if( d_var_num.find( n )==d_var_num.end() ){
258 [ + - ]: 215875 : Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
259 : 215875 : d_var_num[n] = d_vars.size();
260 : 215875 : d_vars.push_back( n );
261 : 215875 : d_var_types.push_back( n.getType() );
262 : 215875 : d_match.push_back( TNode::null() );
263 : 215875 : d_match_term.push_back( TNode::null() );
264 [ + + ]: 215875 : if (n.getKind() == Kind::ITE)
265 : : {
266 : 3394 : registerNode( n, false, false );
267 : : }
268 [ + + ]: 212481 : else if (n.getKind() == Kind::BOUND_VARIABLE)
269 : : {
270 : 14392 : d_extra_var.push_back( n );
271 : : }
272 : : else
273 : : {
274 [ + + ]: 605122 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
275 : 407033 : flatten( n[i], beneathQuant );
276 : : }
277 : : }
278 : : }else{
279 [ + - ]: 283172 : Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
280 : : }
281 : : }else{
282 [ + - ]: 95983 : Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
283 : : }
284 : 595030 : }
285 : :
286 : 2748219 : int QuantInfo::getVarNum(TNode v) const
287 : : {
288 : 2748219 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(v);
289 [ + + ]: 2748219 : return it != d_var_num.end() ? static_cast<int>(it->second) : -1;
290 : : }
291 : :
292 : 260284 : bool QuantInfo::reset_round()
293 : : {
294 [ + + ]: 2100903 : for (size_t i = 0, nmatch = d_match.size(); i < nmatch; i++)
295 : : {
296 : 1840619 : d_match[i] = TNode::null();
297 : 1840619 : d_match_term[i] = TNode::null();
298 : : }
299 : 260284 : d_instMatch.resetAll();
300 : 260284 : ieval::TermEvaluatorMode tev = d_parent->atConflictEffort()
301 [ + + ]: 260284 : ? ieval::TermEvaluatorMode::CONFLICT
302 : 260284 : : ieval::TermEvaluatorMode::PROP;
303 : 260284 : d_instMatch.setEvaluatorMode(tev);
304 : 260284 : d_vars_set.clear();
305 : 260284 : d_curr_var_deq.clear();
306 : 260284 : d_tconstraints.clear();
307 : :
308 : 260284 : d_mg->reset_round();
309 [ + + ]: 1361336 : for (const std::pair<const size_t, std::unique_ptr<MatchGen>>& vg : d_var_mg)
310 : : {
311 [ - + ]: 1101052 : if (!vg.second->reset_round())
312 : : {
313 : 0 : return false;
314 : : }
315 : : }
316 : : //now, reset for matching
317 : 260284 : d_mg->reset(false);
318 : 260284 : return true;
319 : : }
320 : :
321 : 12172022 : size_t QuantInfo::getCurrentRepVar(size_t v)
322 : : {
323 [ - + ][ - + ]: 12172022 : Assert(v < d_match.size());
[ - - ]
324 : 12172022 : TNode m = d_match[v];
325 [ + + ]: 12172022 : if (!m.isNull())
326 : : {
327 : 6787496 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(m);
328 [ + + ]: 6787496 : if (it != d_var_num.end())
329 : : {
330 : 38448 : return getCurrentRepVar(it->second);
331 : : }
332 : : }
333 : 12133574 : return v;
334 : 12172022 : }
335 : :
336 : 6624928 : TNode QuantInfo::getCurrentValue( TNode n ) {
337 : 6624928 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(n);
338 [ + + ]: 6624928 : if (it == d_var_num.end())
339 : : {
340 : 2001049 : return n;
341 : : }
342 : 4623879 : Node m = d_match[it->second];
343 [ + + ]: 4623879 : if (m.isNull())
344 : : {
345 : 4241789 : return n;
346 : : }
347 : 382090 : return getCurrentValue(m);
348 : 4623879 : }
349 : :
350 : 70 : TNode QuantInfo::getCurrentExpValue( TNode n ) {
351 : 70 : std::map<TNode, size_t>::const_iterator it = d_var_num.find(n);
352 [ - + ]: 70 : if (it == d_var_num.end())
353 : : {
354 : 0 : return n;
355 : : }
356 : 70 : Node m = d_match[it->second];
357 [ - + ]: 70 : if (m.isNull())
358 : : {
359 : 0 : return n;
360 : : }
361 [ - + ][ - + ]: 70 : Assert(m != n);
[ - - ]
362 : 70 : Node mt = d_match_term[it->second];
363 [ - + ]: 70 : if (mt.isNull())
364 : : {
365 : 0 : return getCurrentValue(m);
366 : : }
367 : 70 : return mt;
368 : 70 : }
369 : :
370 : 11117252 : bool QuantInfo::getCurrentCanBeEqual(size_t v, TNode n, bool chDiseq)
371 : : {
372 : : //check disequalities
373 : : std::map<size_t, std::map<TNode, size_t> >::iterator itd =
374 : 11117252 : d_curr_var_deq.find(v);
375 [ + + ]: 11117252 : if (itd == d_curr_var_deq.end())
376 : : {
377 : 6580404 : return true;
378 : : }
379 [ + + ]: 8646295 : for (std::pair<const TNode, size_t>& dd : itd->second)
380 : : {
381 : 8929160 : Node cv = getCurrentValue(dd.first);
382 [ + - ]: 4464580 : Trace("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
383 [ + + ]: 4464580 : if (cv == n)
384 : : {
385 : 355058 : return false;
386 : : }
387 : 4109522 : else if (chDiseq && !isVar(n) && !isVar(cv))
388 : : {
389 : : // they must actually be disequal if we are looking for conflicts
390 [ + + ]: 1057 : if (!d_qs.areDisequal(n, cv))
391 : : {
392 : : // TODO : check for entailed disequal
393 : 75 : return false;
394 : : }
395 : : }
396 [ + + ]: 4464580 : }
397 : :
398 : 4181715 : return true;
399 : : }
400 : :
401 : 0 : int QuantInfo::addConstraint(size_t v, TNode n, bool polarity)
402 : : {
403 : 0 : v = getCurrentRepVar( v );
404 : 0 : int vn = getVarNum( n );
405 [ - - ]: 0 : if (vn != -1)
406 : : {
407 : 0 : vn = static_cast<int>(getCurrentRepVar(static_cast<size_t>(vn)));
408 : : }
409 : 0 : n = getCurrentValue( n );
410 : 0 : return addConstraint(v, n, vn, polarity, false);
411 : : }
412 : :
413 : 1374759 : int QuantInfo::addConstraint(
414 : : size_t v, TNode n, int vn, bool polarity, bool doRemove)
415 : : {
416 [ - + ][ - + ]: 1374759 : Assert(v < d_match.size());
[ - - ]
417 : : //for handling equalities between variables, and disequalities involving variables
418 : 1374759 : Trace("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
419 [ + - ]: 1374759 : Trace("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
420 : 1374759 : Assert(doRemove || n == getCurrentValue(n));
421 [ + + ][ + - ]: 1374759 : Assert(doRemove || v == getCurrentRepVar(v));
[ - + ][ - + ]
[ - - ]
422 : 1374759 : Assert(doRemove || (vn == -1 && getVarNum(n) == -1)
423 : : || (vn >= 0
424 : : && static_cast<size_t>(vn)
425 : : == getCurrentRepVar(static_cast<size_t>(getVarNum(n)))));
426 [ + + ]: 1374759 : if( polarity ){
427 [ + - ]: 951558 : if (vn != static_cast<int>(v))
428 : : {
429 [ + + ]: 951558 : if( doRemove ){
430 [ + + ]: 464042 : if( vn!=-1 ){
431 : : //if set to this in the opposite direction, clean up opposite instead
432 : : // std::map< int, TNode >::iterator itmn = d_match.find( vn );
433 [ - + ]: 28515 : if( d_match[vn]==d_vars[v] ){
434 : 0 : return addConstraint(vn, d_vars[v], v, true, true);
435 : : }else{
436 : : //unsetting variables equal
437 : : std::map<size_t, std::map<TNode, size_t> >::iterator itd =
438 : 28515 : d_curr_var_deq.find(vn);
439 [ + + ]: 28515 : if( itd!=d_curr_var_deq.end() ){
440 : : //remove disequalities owned by this
441 : 11969 : std::vector< TNode > remDeq;
442 [ + + ]: 12298 : for (const std::pair<const TNode, size_t>& dd : itd->second)
443 : : {
444 [ + - ]: 329 : if (dd.second == v)
445 : : {
446 : 329 : remDeq.push_back(dd.first);
447 : : }
448 : : }
449 [ + + ]: 12298 : for (TNode rd : remDeq)
450 : : {
451 : 329 : itd->second.erase(rd);
452 : 329 : }
453 : 11969 : }
454 : : }
455 : : }
456 : 464042 : unsetMatch(v);
457 : 464042 : return 1;
458 : : }else{
459 : 487516 : bool isGroundRep = false;
460 : 487516 : bool isGround = false;
461 [ + + ]: 487516 : if( vn!=-1 ){
462 [ + - ]: 28887 : Trace("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
463 [ + - ]: 28887 : if( d_match[v].isNull() ){
464 : : //setting variables equal
465 : 28887 : bool alreadySet = false;
466 [ - + ]: 28887 : if( !d_match[vn].isNull() ){
467 : 0 : alreadySet = true;
468 : 0 : Assert(!isVar(d_match[vn]));
469 : : }
470 : :
471 : : //copy or check disequalities
472 : : std::map<size_t, std::map<TNode, size_t> >::iterator itd =
473 : 28887 : d_curr_var_deq.find(v);
474 [ + + ]: 28887 : if( itd!=d_curr_var_deq.end() ){
475 : 11984 : std::map<TNode, size_t>& cvd = d_curr_var_deq[vn];
476 [ + + ]: 12313 : for (const std::pair<const TNode, size_t>& dd : itd->second)
477 : : {
478 : 658 : Node dv = getCurrentValue(dd.first);
479 [ + - ]: 329 : if( !alreadySet ){
480 [ + - ]: 329 : if (cvd.find(dv) == cvd.end())
481 : : {
482 : 329 : cvd[dv] = v;
483 : : }
484 : : }
485 [ - - ]: 0 : else if (d_match[vn] == dv)
486 : : {
487 [ - - ]: 0 : Trace("qcf-match-debug")
488 : 0 : << " -> fail, conflicting disequality" << std::endl;
489 : 0 : return -1;
490 : : }
491 [ + - ]: 329 : }
492 : : }
493 [ - + ]: 28887 : if( alreadySet ){
494 : 0 : n = getCurrentValue( n );
495 : : }
496 : : }else{
497 [ - - ]: 0 : if( d_match[vn].isNull() ){
498 [ - - ]: 0 : Trace("qcf-match-debug") << " ...Reverse direction" << std::endl;
499 : : //set the opposite direction
500 : 0 : return addConstraint(vn, d_vars[v], v, true, false);
501 : : }else{
502 [ - - ]: 0 : Trace("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;
503 : : //are they currently equal
504 [ - - ]: 0 : return d_match[v] == d_match[vn] ? 0 : -1;
505 : : }
506 : : }
507 : : }else{
508 [ + - ]: 458629 : Trace("qcf-match-debug") << " ...Variable bound to ground" << std::endl;
509 [ + - ]: 458629 : if( d_match[v].isNull() ){
510 : : //isGroundRep = true; ??
511 : 458629 : isGround = true;
512 : : }else{
513 : : //compare ground values
514 [ - - ]: 0 : Trace("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
515 [ - - ]: 0 : return d_match[v] == n ? 0 : -1;
516 : : }
517 : : }
518 [ + + ]: 487516 : if (setMatch(v, n, isGroundRep, isGround))
519 : : {
520 [ + - ]: 468539 : Trace("qcf-match-debug") << " -> success" << std::endl;
521 : 468539 : return 1;
522 : : }
523 : : else
524 : : {
525 [ + - ]: 18977 : Trace("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
526 : 18977 : return -1;
527 : : }
528 : : }
529 : : }
530 : : else
531 : : {
532 [ - - ]: 0 : Trace("qcf-match-debug") << " -> redundant, variable identity" << std::endl;
533 : 0 : return 0;
534 : : }
535 : : }else{
536 [ - + ]: 423201 : if (vn == static_cast<int>(v))
537 : : {
538 [ - - ]: 0 : Trace("qcf-match-debug") << " -> fail, variable identity" << std::endl;
539 : 0 : return -1;
540 : : }
541 : : else
542 : : {
543 [ + + ]: 423201 : if( doRemove ){
544 [ - + ][ - + ]: 210653 : Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end());
[ - - ]
545 : 210653 : d_curr_var_deq[v].erase( n );
546 : 210653 : return 1;
547 : : }else{
548 [ + + ]: 212548 : if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
549 : : //check if it respects equality
550 [ - + ]: 212086 : if( !d_match[v].isNull() ){
551 : 0 : TNode nv = getCurrentValue( n );
552 [ - - ]: 0 : if (nv == d_match[v])
553 : : {
554 [ - - ]: 0 : Trace("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
555 : 0 : return -1;
556 : : }
557 [ - - ]: 0 : }
558 : 212086 : d_curr_var_deq[v][n] = v;
559 [ + - ]: 212086 : Trace("qcf-match-debug") << " -> success" << std::endl;
560 : 212086 : return 1;
561 : : }else{
562 [ + - ]: 462 : Trace("qcf-match-debug") << " -> redundant disequality" << std::endl;
563 : 462 : return 0;
564 : : }
565 : : }
566 : : }
567 : : }
568 : : }
569 : :
570 : 160 : bool QuantInfo::isConstrainedVar(size_t v)
571 : : {
572 : : std::map<size_t, std::map<TNode, size_t> >::const_iterator it =
573 : 160 : d_curr_var_deq.find(v);
574 [ + + ][ - + ]: 160 : if (it != d_curr_var_deq.end() && !it->second.empty())
[ - + ]
575 : : {
576 : 0 : return true;
577 : : }
578 : 160 : TNode vv = getVar(v);
579 [ - + ]: 160 : if (std::find(d_match.begin(), d_match.end(), vv) != d_match.end())
580 : : {
581 : 0 : return true;
582 : : }
583 : 160 : for (const std::pair<const size_t, std::map<TNode, size_t> >& d :
584 [ + + ]: 404 : d_curr_var_deq)
585 : : {
586 [ + + ]: 116 : for (const std::pair<const TNode, size_t>& dd : d.second)
587 : : {
588 [ - + ]: 32 : if (dd.first == vv)
589 : : {
590 : 0 : return true;
591 : : }
592 : : }
593 : : }
594 : 160 : return false;
595 : 160 : }
596 : :
597 : 10947916 : bool QuantInfo::setMatch(size_t v, TNode n, bool isGroundRep, bool isGround)
598 : : {
599 [ + + ]: 10947916 : if (!getCurrentCanBeEqual(v, n))
600 : : {
601 : 350853 : return false;
602 : : }
603 [ + + ]: 10597063 : if (isGroundRep)
604 : : {
605 : : // fail if n does not exist in the relevant domain of each of the argument
606 : : // positions
607 : : std::map<size_t, std::map<TNode, std::vector<size_t> > >::iterator it =
608 : 10104886 : d_var_rel_dom.find(v);
609 [ + + ]: 10104886 : if (it != d_var_rel_dom.end())
610 : : {
611 : 4394942 : TermDb* tdb = d_parent->getTermDatabase();
612 [ + + ]: 10093896 : for (std::pair<const TNode, std::vector<size_t> >& rd : it->second)
613 : : {
614 [ + + ]: 12021845 : for (size_t index : rd.second)
615 : : {
616 [ + - ]: 12645782 : Trace("qcf-match-debug2") << n << " in relevant domain " << rd.first
617 : 6322891 : << "." << index << "?" << std::endl;
618 [ + + ]: 6322891 : if (!tdb->inRelevantDomain(rd.first, index, n))
619 : : {
620 [ + - ]: 824360 : Trace("qcf-match-debug")
621 : 0 : << " -> fail, since " << n << " is not in relevant domain of "
622 : 412180 : << rd.first << "." << index << std::endl;
623 : 412180 : return false;
624 : : }
625 : : }
626 : : }
627 : : }
628 : : }
629 [ + - ]: 20369766 : Trace("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked "
630 : 10184883 : << d_curr_var_deq[v].size() << " disequalities"
631 : 10184883 : << std::endl;
632 [ + + ][ + + ]: 10184883 : if (isGround && d_vars[v].getKind() == Kind::BOUND_VARIABLE)
[ + + ]
633 : : {
634 : : // Set the inst match object if this corresponds to an original variable
635 [ + + ]: 3608738 : if (v < d_q[0].getNumChildren())
636 : : {
637 : : // we overwrite, so we must reset/set here
638 [ + + ]: 3605423 : if (!d_instMatch.get(v).isNull())
639 : : {
640 : 543654 : d_instMatch.reset(v);
641 : : }
642 [ + + ]: 3605423 : if (!d_instMatch.set(v, n))
643 : : {
644 : 2222240 : return false;
645 : : }
646 : : }
647 : 1386498 : d_vars_set.insert(v);
648 [ + - ]: 2772996 : Trace("qcf-match-debug")
649 : 0 : << "---- now bound " << d_vars_set.size() << " / "
650 [ - + ][ - - ]: 1386498 : << d_q[0].getNumChildren() << " base variables." << std::endl;
651 : : }
652 : : // Note that assigning to a variable that an original variable is equal to
653 : : // should trigger the match object. For example, if we have auxiliary
654 : : // variable k and original variable x where x <-> k currently, and we set
655 : : // k -> t, then we should notify the match object that x -> t. However,
656 : : // this is not done, as it would require more complex bookkeeping. Overall,
657 : : // this means that we may fail in some rare cases to eagerly recognize when a
658 : : // substitution is entailed.
659 : 7962643 : d_match[v] = n;
660 : 7962643 : return true;
661 : : }
662 : :
663 : 5664526 : void QuantInfo::unsetMatch(size_t v)
664 : : {
665 [ + - ]: 5664526 : Trace("qcf-match-debug") << "-- unbind : " << v << std::endl;
666 : 5664526 : if (d_vars[v].getKind() == Kind::BOUND_VARIABLE
667 [ + + ][ + + ]: 5664526 : && d_vars_set.find(v) != d_vars_set.end())
[ + + ]
668 : : {
669 : 838248 : d_vars_set.erase( v );
670 : : // Reset the inst match object if this corresponds to an original variable
671 [ + + ]: 838248 : if (v < d_q[0].getNumChildren())
672 : : {
673 [ + + ]: 835892 : if (!d_instMatch.get(v).isNull())
674 : : {
675 : 830950 : d_instMatch.reset(v);
676 : : }
677 : : }
678 : : }
679 : 5664526 : d_match[v] = TNode::null();
680 : 5664526 : }
681 : :
682 : 37602 : bool QuantInfo::isMatchSpurious()
683 : : {
684 [ + + ]: 263789 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
685 : : {
686 [ + + ]: 230467 : if( !d_match[i].isNull() ){
687 [ + + ]: 169336 : if (!getCurrentCanBeEqual(i, d_match[i], d_parent->atConflictEffort()))
688 : : {
689 : 4280 : return true;
690 : : }
691 : : }
692 : : }
693 : 33322 : return false;
694 : : }
695 : :
696 : 31906 : bool QuantInfo::isTConstraintSpurious(const std::vector<Node>& terms)
697 : : {
698 [ + + ]: 31906 : if (options().quantifiers.ievalMode != options::IevalMode::OFF)
699 : : {
700 : : // We rely on the instantiation evaluator. When the instantiation evaluator
701 : : // is enabled, this method (almost) always returns false. The code may
702 : : // return true based on minor differences in the entailment tests, which
703 : : // would allow us in very rare cases to recognize when an instantiation
704 : : // is spurious.
705 : 8405 : return false;
706 : : }
707 : 23501 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
708 : : // check whether the instantiation evaluates as expected
709 : 23501 : std::map<TNode, TNode> subs;
710 [ + + ]: 93238 : for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
711 : : {
712 [ + - ]: 69737 : Trace("qcf-instance-check") << " " << terms[i] << std::endl;
713 : 69737 : subs[d_q[0][i]] = terms[i];
714 : : }
715 [ + + ]: 23571 : for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++)
716 : : {
717 : 140 : Node n = getCurrentExpValue(d_extra_var[i]);
718 [ + - ]: 140 : Trace("qcf-instance-check")
719 : 70 : << " " << d_extra_var[i] << " -> " << n << std::endl;
720 : 70 : subs[d_extra_var[i]] = n;
721 : 70 : }
722 [ + + ]: 23501 : if (d_parent->atConflictEffort())
723 : : {
724 [ + - ]: 33216 : Trace("qcf-instance-check")
725 : 16608 : << "Possible conflict instance for " << d_q << " : " << std::endl;
726 [ + + ]: 16608 : if (!echeck->isEntailed(d_q[1], subs, false, false))
727 : : {
728 [ + - ]: 33154 : Trace("qcf-instance-check")
729 : 16577 : << "...not entailed to be false." << std::endl;
730 : 16577 : return true;
731 : : }
732 : : }
733 : : else
734 : : {
735 : : // see if the body of the quantified formula evaluates to a Boolean
736 : : // combination of known terms under the current substitution. We use
737 : : // the helper method evaluateTerm from the entailment check utility.
738 : : Node inst_eval = echeck->evaluateTerm(
739 : 13786 : d_q[1], subs, false, options().quantifiers.cbqiTConstraint, true);
740 [ - + ]: 6893 : if (TraceIsOn("qcf-instance-check"))
741 : : {
742 [ - - ]: 0 : Trace("qcf-instance-check")
743 : 0 : << "Possible propagating instance for " << d_q << " : " << std::endl;
744 [ - - ]: 0 : Trace("qcf-instance-check") << " " << terms << std::endl;
745 [ - - ]: 0 : Trace("qcf-instance-check")
746 : 0 : << "...evaluates to " << inst_eval << std::endl;
747 : : }
748 : : // If it is the case that instantiation can be rewritten to a Boolean
749 : : // combination of terms that exist in the current context, then inst_eval
750 : : // is non-null. Moreover, we insist that inst_eval is not true, or else
751 : : // the instantiation is trivially entailed and hence is spurious.
752 : 6893 : if (inst_eval.isNull()
753 [ + + ][ + + ]: 6893 : || (inst_eval.isConst() && inst_eval.getConst<bool>()))
[ + + ][ + + ]
754 : : {
755 [ + - ]: 6775 : Trace("qcf-instance-check") << "...spurious." << std::endl;
756 : 6775 : return true;
757 : : }
758 : : else
759 : : {
760 [ + - ]: 118 : if (Configuration::isDebugBuild())
761 : : {
762 [ - + ]: 118 : if (!d_parent->isPropagatingInstance(inst_eval))
763 : : {
764 : : // Notice that this can happen in cases where:
765 : : // (1) x = -1*y is rewritten to y = -1*x, and
766 : : // (2) -1*y is a term in the master equality engine but -1*x is not.
767 : : // In other words, we determined that x = -1*y is a relevant
768 : : // equality to propagate since it involves two known terms, but
769 : : // after rewriting, the equality y = -1*x involves an unknown term
770 : : // -1*x. In this case, the equality is still relevant to propagate,
771 : : // despite the above function not being precise enough to realize
772 : : // it. We output a warning in debug for this. See #2993.
773 [ - - ]: 0 : Trace("qcf-instance-check")
774 : 0 : << "WARNING: not propagating." << std::endl;
775 : : }
776 : : }
777 [ + - ]: 118 : Trace("qcf-instance-check") << "...not spurious." << std::endl;
778 : : }
779 [ + + ]: 6893 : }
780 [ - + ]: 149 : if( !d_tconstraints.empty() ){
781 : : //check constraints
782 : 0 : QuantifiersRegistry& qr = d_parent->getQuantifiersRegistry();
783 [ - - ]: 0 : for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
784 : : //apply substitution to the tconstraint
785 : 0 : Node cons = qr.substituteBoundVariables(it->first, d_q, terms);
786 [ - - ]: 0 : cons = it->second ? cons : cons.negate();
787 [ - - ]: 0 : if (!entailmentTest(cons, d_parent->atConflictEffort()))
788 : : {
789 : 0 : return true;
790 : : }
791 [ - - ]: 0 : }
792 : : }
793 : : // spurious if quantifiers engine is in conflict
794 : 149 : return d_parent->d_qstate.isInConflict();
795 : 23501 : }
796 : :
797 : 0 : bool QuantInfo::entailmentTest(Node lit, bool chEnt)
798 : : {
799 [ - - ]: 0 : Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
800 : 0 : Node rew = rewrite(lit);
801 [ - - ]: 0 : if (rew.isConst())
802 : : {
803 [ - - ]: 0 : Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to "
804 : 0 : << rew << "." << std::endl;
805 : 0 : return rew.getConst<bool>();
806 : : }
807 : : // if checking for conflicts, we must be sure that the (negation of)
808 : : // constraint is (not) entailed
809 [ - - ]: 0 : if (!chEnt)
810 : : {
811 : 0 : rew = rewrite(rew.negate());
812 : : }
813 : : // check if it is entailed
814 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
815 : 0 : << "Check entailment of " << rew << "..." << std::endl;
816 : : std::pair<bool, Node> et =
817 : 0 : d_parent->getState().getValuation().entailmentCheck(
818 : 0 : options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
819 : 0 : ++(d_parent->d_statistics.d_entailment_checks);
820 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
821 : 0 : << "ET result : " << et.first << " " << et.second << std::endl;
822 [ - - ]: 0 : if (!et.first)
823 : : {
824 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
825 : 0 : << "...cannot show entailment of " << rew << "." << std::endl;
826 : 0 : return !chEnt;
827 : : }
828 : 0 : return chEnt;
829 : 0 : }
830 : :
831 : 33149 : bool QuantInfo::completeMatch(std::vector<size_t>& assigned, bool doContinue)
832 : : {
833 : : //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
834 : 33149 : bool doFail = false;
835 : 33149 : bool success = true;
836 [ - + ]: 33149 : if( doContinue ){
837 : 0 : doFail = true;
838 : 0 : success = false;
839 : : }else{
840 [ + + ]: 33149 : if (isBaseMatchComplete())
841 : : {
842 : 31664 : return true;
843 : : }
844 : : //solve for interpreted symbol matches
845 : : // this breaks the invariant that all introduced constraints are over existing terms
846 [ + + ]: 1525 : for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
847 : 66 : int index = d_tsym_vars[i];
848 : 66 : TNode v = getCurrentValue( d_vars[index] );
849 : 66 : int slv_v = -1;
850 [ + + ]: 66 : if( v==d_vars[index] ){
851 : 40 : slv_v = index;
852 : : }
853 [ + - ]: 132 : Trace("qcf-tconstraint-debug")
854 : 0 : << "Solve " << d_vars[index] << " = " << v << " "
855 : 66 : << d_vars[index].getKind() << std::endl;
856 : 66 : if (d_vars[index].getKind() == Kind::ADD
857 [ + + ][ + + ]: 66 : || d_vars[index].getKind() == Kind::MULT)
[ + + ]
858 : : {
859 : 40 : Kind k = d_vars[index].getKind();
860 : 40 : std::vector< TNode > children;
861 [ + + ]: 76 : for (const Node& vi : d_vars[index]){
862 : 62 : int vn = getVarNum( vi );
863 [ + + ]: 62 : if( vn!=-1 ){
864 : 47 : TNode vv = getCurrentValue( vi );
865 [ + + ]: 47 : if( vv==vi ){
866 : : //we will assign this
867 [ - + ]: 40 : if( slv_v==-1 ){
868 [ - - ]: 0 : Trace("qcf-tconstraint-debug")
869 : 0 : << "...will solve for var #" << vn << std::endl;
870 : 0 : slv_v = vn;
871 [ - - ]: 0 : if (!d_parent->atConflictEffort())
872 : : {
873 : 0 : break;
874 : : }
875 : : }else{
876 : 80 : Node z = d_parent->getZero(d_vars[index].getType(), k);
877 [ + + ]: 40 : if( !z.isNull() ){
878 : 33 : size_t vni = static_cast<size_t>(vn);
879 [ + - ]: 66 : Trace("qcf-tconstraint-debug")
880 : 33 : << "...set " << d_vars[vn] << " = " << z << std::endl;
881 : 33 : assigned.push_back(vni);
882 [ + + ]: 33 : if (!setMatch(vni, z, false, true))
883 : : {
884 : 26 : success = false;
885 : 26 : break;
886 : : }
887 : : }
888 [ + + ]: 40 : }
889 : : }else{
890 [ + - ]: 14 : Trace("qcf-tconstraint-debug")
891 : 7 : << "...sum value " << vv << std::endl;
892 : 7 : children.push_back( vv );
893 : : }
894 [ + + ]: 47 : }else{
895 [ + - ]: 15 : Trace("qcf-tconstraint-debug") << "...sum " << vi << std::endl;
896 : 15 : children.push_back( vi );
897 : : }
898 [ + + ]: 62 : }
899 [ + + ]: 40 : if( success ){
900 [ + - ]: 14 : if( slv_v!=-1 ){
901 : 14 : Node lhs;
902 [ - + ]: 14 : if( children.empty() ){
903 : 0 : lhs = d_parent->getZero(d_vars[index].getType(), k);
904 [ + - ]: 14 : }else if( children.size()==1 ){
905 : 14 : lhs = children[0];
906 : : }else{
907 : 0 : lhs = nodeManager()->mkNode(k, children);
908 : : }
909 : 14 : Node sum;
910 [ + - ]: 14 : if( v==d_vars[index] ){
911 : 14 : sum = lhs;
912 : : }else{
913 [ - - ]: 0 : if (d_parent->atConflictEffort())
914 : : {
915 : 0 : Kind kn = k;
916 [ - - ]: 0 : if (d_vars[index].getKind() == Kind::ADD)
917 : : {
918 : 0 : kn = Kind::SUB;
919 : : }
920 [ - - ]: 0 : if( kn!=k ){
921 : 0 : sum = nodeManager()->mkNode(kn, v, lhs);
922 : : }
923 : : }
924 : : }
925 [ + - ]: 14 : if( !sum.isNull() ){
926 : 14 : assigned.push_back( slv_v );
927 [ + - ]: 28 : Trace("qcf-tconstraint-debug")
928 : 14 : << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
929 [ - + ]: 14 : if (!setMatch(slv_v, sum, false, true))
930 : : {
931 : 0 : success = false;
932 : : }
933 : 14 : d_parent->d_tempCache.push_back(sum);
934 : : }
935 : 14 : }else{
936 : : //must show that constraint is met
937 : 0 : Node sum = nodeManager()->mkNode(k, children);
938 : 0 : Node eq = sum.eqNode( v );
939 [ - - ]: 0 : if (!entailmentTest(eq))
940 : : {
941 : 0 : success = false;
942 : : }
943 : 0 : d_parent->d_tempCache.push_back(sum);
944 : 0 : }
945 : : }
946 : 40 : }
947 : :
948 [ + + ]: 66 : if( !success ){
949 : 26 : break;
950 : : }
951 [ + + ]: 66 : }
952 [ + + ]: 1485 : if( success ){
953 : : //check what is left to assign
954 : 1459 : d_unassigned.clear();
955 : 1459 : d_unassigned_tn.clear();
956 [ + + ]: 8754 : std::vector<size_t> unassigned[2];
957 [ + + ]: 7295 : std::vector< TypeNode > unassigned_tn[2];
958 [ + + ]: 4224 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
959 : : {
960 [ + + ]: 2765 : if( d_match[i].isNull() ){
961 [ + + ]: 2301 : int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
962 : 2301 : unassigned[rindex].push_back( i );
963 : 2301 : unassigned_tn[rindex].push_back( getVar( i ).getType() );
964 : 2301 : assigned.push_back( i );
965 : : }
966 : : }
967 : 1459 : d_unassigned_nvar = unassigned[0].size();
968 [ + + ]: 4377 : for( unsigned i=0; i<2; i++ ){
969 : 2918 : d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
970 : 2918 : d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
971 : : }
972 : 1459 : d_una_eqc_count.clear();
973 : 1459 : d_una_index = 0;
974 [ + + ][ + + ]: 8754 : }
[ - - ][ - - ]
975 : : }
976 : :
977 [ + + ][ - + ]: 1485 : if( !d_unassigned.empty() && ( success || doContinue ) ){
[ - - ][ + + ]
978 [ + - ]: 2780 : Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size()
979 : 1390 : << ")..." << std::endl;
980 : : do {
981 [ - + ]: 1390 : if( doFail ){
982 [ - - ]: 0 : Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
983 : : }
984 : 1390 : bool invalidMatch = false;
985 [ + + ][ + - ]: 8180 : while ((success && d_una_index < d_unassigned.size()) || invalidMatch
986 [ + + ][ - + ]: 13580 : || doFail)
[ + + ]
987 : : {
988 : 5400 : invalidMatch = false;
989 [ + - ][ + + ]: 5400 : if (!doFail && d_una_index == d_una_eqc_count.size())
[ + + ]
990 : : {
991 : : //check if it has now been assigned
992 [ + + ]: 1857 : if( d_una_index<d_unassigned_nvar ){
993 [ + - ]: 80 : if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
994 : 80 : d_una_eqc_count.push_back( -1 );
995 : : }else{
996 : 0 : d_var_mg[d_unassigned[d_una_index]]->reset(true);
997 : 0 : d_una_eqc_count.push_back( 0 );
998 : : }
999 : : }else{
1000 : 1777 : d_una_eqc_count.push_back( 0 );
1001 : : }
1002 : : }
1003 : : else
1004 : : {
1005 : 3543 : bool failed = false;
1006 [ + - ]: 3543 : if( !doFail ){
1007 [ + + ]: 3543 : if( d_una_index<d_unassigned_nvar ){
1008 [ + - ]: 80 : if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
1009 [ + - ]: 160 : Trace("qcf-check-unassign")
1010 : 0 : << "Succeeded, variable unconstrained at " << d_una_index
1011 : 80 : << std::endl;
1012 : 80 : d_una_index++;
1013 : : }
1014 [ - - ]: 0 : else if (d_var_mg[d_unassigned[d_una_index]]->getNextMatch())
1015 : : {
1016 [ - - ]: 0 : Trace("qcf-check-unassign") << "Succeeded match with mg at "
1017 : 0 : << d_una_index << std::endl;
1018 : 0 : d_una_index++;
1019 : : }
1020 : : else
1021 : : {
1022 : 0 : failed = true;
1023 [ - - ]: 0 : Trace("qcf-check-unassign")
1024 : 0 : << "Failed match with mg at " << d_una_index << std::endl;
1025 : : }
1026 : : }else{
1027 [ + - ][ + - ]: 3463 : Assert(doFail || d_una_index + 1 == d_una_eqc_count.size());
[ - + ][ - + ]
[ - - ]
1028 : : const std::vector<TNode>& eqcs =
1029 : 3463 : d_parent->d_eqcs[d_unassigned_tn[d_una_index]];
1030 [ + + ]: 3463 : if (d_una_eqc_count[d_una_index] < static_cast<int>(eqcs.size()))
1031 : : {
1032 : 1905 : int currIndex = d_una_eqc_count[d_una_index];
1033 : 1905 : d_una_eqc_count[d_una_index]++;
1034 [ + - ]: 3810 : Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->"
1035 : 1905 : << eqcs[currIndex] << std::endl;
1036 [ + + ]: 3810 : if (setMatch(
1037 : 3810 : d_unassigned[d_una_index], eqcs[currIndex], true, true))
1038 : : {
1039 : 560 : d_match_term[d_unassigned[d_una_index]] = TNode::null();
1040 [ + - ]: 1120 : Trace("qcf-check-unassign")
1041 : 560 : << "Succeeded match " << d_una_index << std::endl;
1042 : 560 : d_una_index++;
1043 : : }
1044 : : else
1045 : : {
1046 [ + - ]: 2690 : Trace("qcf-check-unassign")
1047 : 1345 : << "Failed match " << d_una_index << std::endl;
1048 : 1345 : invalidMatch = true;
1049 : : }
1050 : : }
1051 : : else
1052 : : {
1053 : 1558 : failed = true;
1054 [ + - ]: 3116 : Trace("qcf-check-unassign")
1055 : 1558 : << "No more matches " << d_una_index << std::endl;
1056 : : }
1057 : : }
1058 : : }
1059 [ + - ][ + + ]: 3543 : if( doFail || failed ){
1060 : : do{
1061 [ + - ]: 1558 : if( !doFail ){
1062 : 1558 : d_una_eqc_count.pop_back();
1063 : : }else{
1064 : 0 : doFail = false;
1065 : : }
1066 [ + + ]: 1558 : if (d_una_index == 0)
1067 : : {
1068 : 1217 : success = false;
1069 : 1217 : break;
1070 : : }
1071 : 341 : d_una_index--;
1072 [ - + ]: 341 : } while (d_una_eqc_count[d_una_index] == -1);
1073 : : }
1074 : : }
1075 : : }
1076 [ + + ]: 1390 : if( success ){
1077 : 173 : doFail = true;
1078 [ + - ]: 173 : Trace("qcf-check-unassign") << " Try: " << std::endl;
1079 [ - + ]: 173 : if (TraceIsOn("qcf-check"))
1080 : : {
1081 [ - - ]: 0 : for (int ui : d_unassigned)
1082 : : {
1083 [ - - ]: 0 : if (!d_match[ui].isNull())
1084 : : {
1085 [ - - ]: 0 : Trace("qcf-check-unassign")
1086 : 0 : << " Assigned #" << ui << " : " << d_vars[ui] << " -> "
1087 : 0 : << d_match[ui] << std::endl;
1088 : : }
1089 : : }
1090 : : }
1091 : : }
1092 [ + + ][ - + ]: 1390 : } while (success && isMatchSpurious());
[ - + ]
1093 [ + - ]: 1390 : Trace("qcf-check") << "done assigning." << std::endl;
1094 : : }
1095 [ + + ]: 1485 : if( success ){
1096 [ - + ]: 242 : if (TraceIsOn("qcf-check"))
1097 : : {
1098 [ - - ]: 0 : for (int ui : d_unassigned)
1099 : : {
1100 [ - - ]: 0 : if (!d_match[ui].isNull())
1101 : : {
1102 [ - - ]: 0 : Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui]
1103 : 0 : << " -> " << d_match[ui] << std::endl;
1104 : : }
1105 : : }
1106 : : }
1107 : 242 : return true;
1108 : : }
1109 : 1243 : revertMatch(assigned);
1110 : 1243 : assigned.clear();
1111 : 1243 : return false;
1112 : : }
1113 : :
1114 : 31906 : void QuantInfo::getMatch( std::vector< Node >& terms ){
1115 [ + + ]: 120721 : for (size_t i = 0, nvars = d_q[0].getNumChildren(); i < nvars; i++)
1116 : : {
1117 : 88815 : size_t repVar = getCurrentRepVar(i);
1118 : 88815 : Node cv;
1119 [ + + ]: 88815 : if( !d_match_term[repVar].isNull() ){
1120 : 87468 : cv = d_match_term[repVar];
1121 : : }else{
1122 : 1347 : cv = d_match[repVar];
1123 : : }
1124 [ + - ]: 88815 : Trace("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
1125 : 88815 : terms.push_back( cv );
1126 : 88815 : }
1127 : 31906 : }
1128 : :
1129 : 29137 : void QuantInfo::revertMatch(const std::vector<size_t>& assigned)
1130 : : {
1131 [ + + ]: 31320 : for (size_t a : assigned)
1132 : : {
1133 : 2183 : unsetMatch(a);
1134 : : }
1135 : 29137 : }
1136 : :
1137 : 0 : void QuantInfo::debugPrintMatch(const char* c) const
1138 : : {
1139 [ - - ]: 0 : for (size_t i = 0, nvars = getNumVars(); i < nvars; i++)
1140 : : {
1141 [ - - ]: 0 : Trace(c) << " " << d_vars[i] << " -> ";
1142 [ - - ]: 0 : if( !d_match[i].isNull() ){
1143 [ - - ]: 0 : Trace(c) << d_match[i];
1144 : : }else{
1145 [ - - ]: 0 : Trace(c) << "(unassigned) ";
1146 : : }
1147 : : std::map<size_t, std::map<TNode, size_t> >::const_iterator itc =
1148 : 0 : d_curr_var_deq.find(i);
1149 [ - - ]: 0 : if (!itc->second.empty())
1150 : : {
1151 [ - - ]: 0 : Trace(c) << ", DEQ{ ";
1152 [ - - ]: 0 : for (const std::pair<const TNode, size_t>& d : itc->second)
1153 : : {
1154 [ - - ]: 0 : Trace(c) << d.first << " ";
1155 : : }
1156 [ - - ]: 0 : Trace(c) << "}";
1157 : : }
1158 : 0 : if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
1159 [ - - ]: 0 : Trace(c) << ", EXP : " << d_match_term[i];
1160 : : }
1161 [ - - ]: 0 : Trace(c) << std::endl;
1162 : : }
1163 [ - - ]: 0 : if( !d_tconstraints.empty() ){
1164 [ - - ]: 0 : Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
1165 [ - - ]: 0 : for (const std::pair<const Node, bool>& tc : d_tconstraints)
1166 : : {
1167 [ - - ]: 0 : Trace(c) << " " << tc.first << " -> " << tc.second << std::endl;
1168 : : }
1169 : : }
1170 : 0 : }
1171 : :
1172 : 330901 : MatchGen::MatchGen(Env& env, QuantConflictFind* p, QuantInfo* qi, Node n, bool isVar)
1173 : : : EnvObj(env),
1174 : 330901 : d_tgt(),
1175 : 330901 : d_tgt_orig(),
1176 : 330901 : d_wasSet(),
1177 : 330901 : d_n(),
1178 : 330901 : d_type(),
1179 : 330901 : d_type_not(),
1180 : 330901 : d_parent(p),
1181 : 330901 : d_qi(qi),
1182 : 330901 : d_matched_basis(),
1183 : 330901 : d_binding()
1184 : : {
1185 : : //initialize temporary
1186 : 330901 : d_child_counter = -1;
1187 : 330901 : d_use_children = true;
1188 : :
1189 [ + - ]: 661802 : Trace("qcf-qregister-debug")
1190 : 330901 : << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
1191 : 330901 : std::vector< Node > qni_apps;
1192 : 330901 : d_qni_size = 0;
1193 [ + + ]: 330901 : if( isVar ){
1194 [ - + ][ - + ]: 164434 : Assert(qi->d_var_num.find(n) != qi->d_var_num.end());
[ - - ]
1195 : : // rare case where we have a free variable in an operator, we are invalid
1196 : 493302 : if (n.getKind() == Kind::ITE
1197 : 164434 : || (n.getKind() == Kind::APPLY_UF && expr::hasFreeVar(n.getOperator())))
1198 : : {
1199 : 3643 : d_type = typ_invalid;
1200 : : }else{
1201 [ + + ]: 160791 : d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
1202 : 160791 : int vn = qi->getVarNum(n);
1203 [ - + ][ - + ]: 160791 : Assert(vn >= 0);
[ - - ]
1204 : 160791 : d_qni_var_num[0] = static_cast<size_t>(vn);
1205 : 160791 : d_qni_size++;
1206 : 160791 : d_type_not = false;
1207 : 160791 : d_n = n;
1208 : : //Node f = getMatchOperator( n );
1209 [ + + ]: 501759 : for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
1210 : 340968 : Node nn = d_n[j];
1211 [ + - ]: 340968 : Trace("qcf-qregister-debug") << " " << d_qni_size;
1212 [ + + ]: 340968 : if( qi->isVar( nn ) ){
1213 : 292035 : size_t v = qi->d_var_num[nn];
1214 [ + - ]: 292035 : Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
1215 : 292035 : d_qni_var_num[d_qni_size] = v;
1216 : : //qi->addFuncParent( v, f, j );
1217 : : }else{
1218 [ + - ]: 48933 : Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
1219 : 48933 : d_qni_gterm[d_qni_size] = nn;
1220 : : }
1221 : 340968 : d_qni_size++;
1222 : 340968 : }
1223 : : }
1224 : : }else{
1225 [ + + ]: 166467 : if (expr::hasBoundVar(n))
1226 : : {
1227 : 166219 : d_type_not = false;
1228 : 166219 : d_n = n;
1229 [ + + ]: 166219 : if (d_n.getKind() == Kind::NOT)
1230 : : {
1231 : 52368 : d_n = d_n[0];
1232 : 52368 : d_type_not = !d_type_not;
1233 : : }
1234 : :
1235 [ + + ]: 166219 : if( isHandledBoolConnective( d_n ) ){
1236 : : //non-literals
1237 : 56857 : d_type = typ_formula;
1238 [ + + ]: 178999 : for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
1239 [ + + ][ + + ]: 129678 : if (d_n.getKind() != Kind::FORALL || i == 1)
[ + + ]
1240 : : {
1241 : : std::unique_ptr<MatchGen> mg =
1242 : 118710 : std::make_unique<MatchGen>(d_env, p, qi, d_n[i], false);
1243 [ + + ]: 118710 : if (!mg->isValid())
1244 : : {
1245 : 7536 : setInvalid();
1246 : 7536 : break;
1247 : : }
1248 : 111174 : d_children.push_back(std::move(mg));
1249 [ + + ]: 118710 : }
1250 : : }
1251 : : }else{
1252 : 109362 : d_type = typ_invalid;
1253 : : //literals
1254 [ + + ]: 109362 : if( isHandledUfTerm( d_n ) ){
1255 [ - + ][ - + ]: 41889 : Assert(qi->isVar(d_n));
[ - - ]
1256 : 41889 : d_type = typ_pred;
1257 : : }
1258 [ + + ]: 67473 : else if (d_n.getKind() == Kind::BOUND_VARIABLE)
1259 : : {
1260 [ - + ][ - + ]: 852 : Assert(d_n.getType().isBoolean());
[ - - ]
1261 : 852 : d_type = typ_bool_var;
1262 : : }
1263 : 66621 : else if (d_n.getKind() == Kind::EQUAL
1264 [ + + ][ + + ]: 66621 : || options().quantifiers.cbqiTConstraint)
[ + + ]
1265 : : {
1266 [ + + ]: 182391 : for (unsigned i = 0; i < d_n.getNumChildren(); i++)
1267 : : {
1268 [ + + ]: 121594 : if (expr::hasBoundVar(d_n[i]))
1269 : : {
1270 [ - + ]: 92114 : if (!qi->isVar(d_n[i]))
1271 : : {
1272 [ - - ]: 0 : Trace("qcf-qregister-debug")
1273 : 0 : << "ERROR : not var " << d_n[i] << std::endl;
1274 : : }
1275 [ - + ][ - + ]: 92114 : Assert(qi->isVar(d_n[i]));
[ - - ]
1276 : 92114 : if (d_n.getKind() != Kind::EQUAL && qi->isVar(d_n[i]))
1277 : : {
1278 : 648 : d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
1279 : : }
1280 : : }
1281 : : else
1282 : : {
1283 : 29480 : d_qni_gterm[i] = d_n[i];
1284 : : }
1285 : : }
1286 [ + + ]: 60797 : d_type = d_n.getKind() == Kind::EQUAL ? typ_eq : typ_tconstraint;
1287 [ + - ]: 60797 : Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
1288 : : }
1289 : : }
1290 : : }else{
1291 : : //we will just evaluate
1292 : 248 : d_n = n;
1293 : 248 : d_type = typ_ground;
1294 : : }
1295 : : }
1296 [ + - ]: 330901 : Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
1297 : 330901 : debugPrintType( "qcf-qregister-debug", d_type );
1298 [ + - ]: 330901 : Trace("qcf-qregister-debug") << std::endl;
1299 : 330901 : }
1300 : :
1301 : 937741 : void MatchGen::collectBoundVar(Node n,
1302 : : std::vector<int>& cbvars,
1303 : : std::map<Node, bool>& visited,
1304 : : bool& hasNested)
1305 : : {
1306 [ + + ]: 937741 : if( visited.find( n )==visited.end() ){
1307 : 809550 : visited[n] = true;
1308 [ + + ]: 809550 : if (n.getKind() == Kind::FORALL)
1309 : : {
1310 : 7752 : hasNested = true;
1311 : : }
1312 : 809550 : int v = d_qi->getVarNum(n);
1313 [ + + ][ + - ]: 809550 : if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
[ + + ]
1314 : 516632 : cbvars.push_back( v );
1315 : : }
1316 [ + + ]: 1653114 : for (const Node& nc : n)
1317 : : {
1318 : 843564 : collectBoundVar(nc, cbvars, visited, hasNested);
1319 : 843564 : }
1320 : : }
1321 : 937741 : }
1322 : :
1323 : 292225 : void MatchGen::determineVariableOrder(std::vector<size_t>& bvars)
1324 : : {
1325 [ + - ]: 584450 : Trace("qcf-qregister-debug") << "Determine variable order " << d_n
1326 : 292225 : << ", #bvars = " << bvars.size() << std::endl;
1327 : 292225 : bool isComm = d_type == typ_formula
1328 [ + + ][ + + ]: 308360 : && (d_n.getKind() == Kind::OR || d_n.getKind() == Kind::AND
[ + + ]
1329 [ + + ]: 16135 : || d_n.getKind() == Kind::EQUAL);
1330 [ + + ]: 292225 : if( isComm ){
1331 : 34291 : std::map< int, std::vector< int > > c_to_vars;
1332 : 34291 : std::map< int, std::vector< int > > vars_to_c;
1333 : 34291 : std::map< int, int > vb_count;
1334 : 34291 : std::map< int, int > vu_count;
1335 : 34291 : std::map< int, bool > has_nested;
1336 : 34291 : std::vector< bool > assigned;
1337 [ + - ]: 34291 : Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
1338 [ + + ]: 119579 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1339 : : {
1340 : 85288 : std::map< Node, bool > visited;
1341 : 85288 : has_nested[i] = false;
1342 : 85288 : collectBoundVar(
1343 : 170576 : d_children[i]->getNode(), c_to_vars[i], visited, has_nested[i]);
1344 : 85288 : assigned.push_back( false );
1345 : 85288 : vb_count[i] = 0;
1346 : 85288 : vu_count[i] = 0;
1347 [ + + ]: 499350 : for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
1348 : 414062 : int v = c_to_vars[i][j];
1349 : 414062 : vars_to_c[v].push_back( i );
1350 [ + + ]: 414062 : if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1351 : 376061 : vu_count[i]++;
1352 : : }else{
1353 : 38001 : vb_count[i]++;
1354 : : }
1355 : : }
1356 : 85288 : }
1357 : : //children that bind no unbound variable, then the most number of bound, unbound variables go first
1358 [ + - ]: 68582 : Trace("qcf-qregister-vo")
1359 : 34291 : << "Variable order for " << d_n << " : " << std::endl;
1360 : 34291 : size_t nqvars = d_qi->d_vars.size();
1361 : : do {
1362 : 85288 : int min_score0 = -1;
1363 : 85288 : int min_score = -1;
1364 : 85288 : int min_score_index = -1;
1365 [ + + ]: 1228128 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1366 : : {
1367 [ + + ]: 1142840 : if( !assigned[i] ){
1368 [ + - ]: 1228128 : Trace("qcf-qregister-debug2")
1369 : 0 : << "Child " << i << " has b/ub : " << vb_count[i] << "/"
1370 : 614064 : << vu_count[i] << std::endl;
1371 : 614064 : int score0 = 0;//has_nested[i] ? 0 : 1;
1372 : : int score;
1373 [ + - ]: 614064 : if (!options().quantifiers.cbqiVoExp)
1374 : : {
1375 : 614064 : score = vu_count[i];
1376 : : }
1377 : : else
1378 : : {
1379 [ - - ]: 0 : score = vu_count[i] == 0 ? 0
1380 : 0 : : (1 + nqvars * (nqvars - vb_count[i])
1381 : 0 : + (nqvars - vu_count[i]));
1382 : : }
1383 [ + + ][ + - ]: 614064 : if( min_score==-1 || score0<min_score0 || ( score0==min_score0 && score<min_score ) ){
[ + - ][ + + ]
1384 : 139675 : min_score0 = score0;
1385 : 139675 : min_score = score;
1386 : 139675 : min_score_index = i;
1387 : : }
1388 : : }
1389 : : }
1390 [ + - ]: 170576 : Trace("qcf-qregister-vo")
1391 : 0 : << " " << d_children_order.size() + 1 << ": "
1392 [ - + ][ - - ]: 85288 : << d_children[min_score_index]->getNode() << " : ";
1393 [ + - ]: 170576 : Trace("qcf-qregister-vo")
1394 : 0 : << vu_count[min_score_index] << " " << vb_count[min_score_index]
1395 : 85288 : << " " << has_nested[min_score_index] << std::endl;
1396 [ + - ]: 170576 : Trace("qcf-qregister-debug")
1397 : 85288 : << "...assign child " << min_score_index << std::endl;
1398 [ + - ]: 85288 : Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
1399 [ - + ][ - + ]: 85288 : Assert(min_score_index != -1);
[ - - ]
1400 : : //add to children order
1401 : 85288 : d_children_order.push_back( min_score_index );
1402 : 85288 : assigned[min_score_index] = true;
1403 : : //determine order internal to children
1404 : 85288 : d_children[min_score_index]->determineVariableOrder(bvars);
1405 [ + - ]: 85288 : Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
1406 : : //now, make it a bound variable
1407 [ + + ]: 85288 : if( vu_count[min_score_index]>0 ){
1408 [ + + ]: 466114 : for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
1409 : 385509 : int v = c_to_vars[min_score_index][i];
1410 [ + + ]: 385509 : if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1411 [ + + ]: 483104 : for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
1412 : 310285 : int vc = vars_to_c[v][j];
1413 : 310285 : vu_count[vc]--;
1414 : 310285 : vb_count[vc]++;
1415 : : }
1416 : 172819 : bvars.push_back( v );
1417 : : }
1418 : : }
1419 : : }
1420 [ + - ]: 170576 : Trace("qcf-qregister-debug")
1421 : 85288 : << "...done assign child " << min_score_index << std::endl;
1422 [ + + ]: 85288 : }while( d_children_order.size()!=d_children.size() );
1423 [ + - ]: 68582 : Trace("qcf-qregister-debug")
1424 : 34291 : << "Done assign variable ordering for " << d_n << std::endl;
1425 : 34291 : }else{
1426 [ + + ]: 266823 : for (size_t i = 0, nchild = d_children.size(); i < nchild; i++)
1427 : : {
1428 : 8889 : d_children_order.push_back( i );
1429 : 8889 : d_children[i]->determineVariableOrder(bvars);
1430 : : //now add to bvars
1431 : 8889 : std::map< Node, bool > visited;
1432 : 8889 : std::vector< int > cvars;
1433 : 8889 : bool has_nested = false;
1434 : 8889 : collectBoundVar(d_children[i]->getNode(), cvars, visited, has_nested);
1435 [ + + ]: 111459 : for( unsigned j=0; j<cvars.size(); j++ ){
1436 [ + + ]: 102570 : if( std::find( bvars.begin(), bvars.end(), cvars[j] )==bvars.end() ){
1437 : 13257 : bvars.push_back( cvars[j] );
1438 : : }
1439 : : }
1440 : 8889 : }
1441 : : }
1442 : 292225 : }
1443 : :
1444 : 2212330 : bool MatchGen::reset_round()
1445 : : {
1446 : 2212330 : d_wasSet = false;
1447 [ + + ]: 3063324 : for (std::unique_ptr<MatchGen>& mg : d_children)
1448 : : {
1449 [ - + ]: 850994 : if (!mg->reset_round())
1450 : : {
1451 : 0 : return false;
1452 : : }
1453 : : }
1454 [ + + ]: 2212330 : if( d_type==typ_ground ){
1455 : 2025 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
1456 : 2025 : QuantifiersState& qs = d_parent->getState();
1457 [ + + ]: 6075 : for (unsigned i = 0; i < 2; i++)
1458 : : {
1459 [ + + ]: 4050 : if (echeck->isEntailed(d_n, i == 0))
1460 : : {
1461 : 48 : d_ground_eval[0] = nodeManager()->mkConst(i == 0);
1462 : : }
1463 [ - + ]: 4050 : if (qs.isInConflict())
1464 : : {
1465 : 0 : return false;
1466 : : }
1467 : : }
1468 [ + + ]: 2210305 : }else if( d_type==typ_eq ){
1469 : 362891 : EntailmentCheck* echeck = d_parent->getTermRegistry().getEntailmentCheck();
1470 : 362891 : QuantifiersState& qs = d_parent->getState();
1471 [ + + ]: 1088673 : for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
1472 : : {
1473 [ + + ]: 725782 : if (!expr::hasBoundVar(d_n[i]))
1474 : : {
1475 : 397172 : TNode t = echeck->getEntailedTerm(d_n[i]);
1476 [ - + ]: 198586 : if (qs.isInConflict())
1477 : : {
1478 : 0 : return false;
1479 : : }
1480 [ + + ]: 198586 : if (t.isNull())
1481 : : {
1482 : 2995 : d_ground_eval[i] = d_n[i];
1483 : : }
1484 : : else
1485 : : {
1486 : 195591 : d_ground_eval[i] = t;
1487 : : }
1488 [ + - ]: 198586 : }
1489 : : }
1490 : : }
1491 : 2212330 : d_qni_bound_cons.clear();
1492 : 2212330 : d_qni_bound_cons_var.clear();
1493 : 2212330 : d_qni_bound.clear();
1494 : 2212330 : return true;
1495 : : }
1496 : :
1497 : 3194079 : void MatchGen::reset(bool tgt)
1498 : : {
1499 [ + + ]: 3194079 : d_tgt = d_type_not ? !tgt : tgt;
1500 [ + - ]: 3194079 : Trace("qcf-match") << " Reset for : " << d_n << ", type : ";
1501 : 3194079 : debugPrintType( "qcf-match", d_type );
1502 [ + - ]: 3194079 : Trace("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;
1503 : 3194079 : d_qn.clear();
1504 : 3194079 : d_qni.clear();
1505 : 3194079 : d_qni_bound.clear();
1506 : 3194079 : d_child_counter = -1;
1507 : 3194079 : d_use_children = true;
1508 : 3194079 : d_tgt_orig = d_tgt;
1509 : :
1510 : : //set up processing matches
1511 [ - + ]: 3194079 : if( d_type==typ_invalid ){
1512 : 0 : d_use_children = false;
1513 [ + + ]: 3194079 : }else if( d_type==typ_ground ){
1514 : 689 : d_use_children = false;
1515 : 689 : if (d_ground_eval[0].isConst()
1516 [ + + ][ + + ]: 689 : && d_ground_eval[0].getConst<bool>() == d_tgt)
[ + + ]
1517 : : {
1518 : 62 : d_child_counter = 0;
1519 : : }
1520 : : }
1521 [ + + ]: 3193390 : else if (d_qi->isBaseMatchComplete())
1522 : : {
1523 : 28573 : d_use_children = false;
1524 : 28573 : d_child_counter = 0;
1525 : : }
1526 [ + + ]: 3164817 : else if (d_type == typ_bool_var)
1527 : : {
1528 : : //get current value of the variable
1529 : 4689 : TNode n = d_qi->getCurrentValue(d_n);
1530 : 4689 : int vnn = d_qi->getVarNum(n);
1531 [ - + ]: 4689 : if (vnn == -1)
1532 : : {
1533 : : // evaluate the value, see if it is compatible
1534 : : EntailmentCheck* echeck =
1535 : 0 : d_parent->getTermRegistry().getEntailmentCheck();
1536 [ - - ]: 0 : if (echeck->isEntailed(n, d_tgt))
1537 : : {
1538 : 0 : d_child_counter = 0;
1539 : : }
1540 : : }
1541 : : else
1542 : : {
1543 : 4689 : size_t vn = d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1544 : : //unassigned, set match to true/false
1545 : 4689 : d_qni_bound[0] = vn;
1546 : 4689 : d_qi->setMatch(vn, nodeManager()->mkConst(d_tgt), false, true);
1547 : 4689 : d_child_counter = 0;
1548 : : }
1549 [ + - ]: 4689 : if( d_child_counter==0 ){
1550 : 4689 : d_qn.push_back( NULL );
1551 : : }
1552 : 4689 : }
1553 [ + + ]: 3160128 : else if (d_type == typ_var)
1554 : : {
1555 [ - + ][ - + ]: 2185470 : Assert(isHandledUfTerm(d_n));
[ - - ]
1556 : 4370940 : TNode f = d_parent->getTermDatabase()->getMatchOperator(d_n);
1557 [ + - ]: 2185470 : Trace("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
1558 : : TNodeTrie* qni =
1559 : 2185470 : d_parent->getTermDatabase()->getTermArgTrie(Node::null(), f);
1560 [ + - ][ + + ]: 2185470 : if (qni == nullptr || qni->empty())
[ + + ]
1561 : : {
1562 : : //inform irrelevant quantifiers
1563 : 265939 : d_parent->setIrrelevantFunction(f);
1564 : : }
1565 : : else
1566 : : {
1567 : 1919531 : d_qn.push_back(qni);
1568 : : }
1569 : 2185470 : d_matched_basis = false;
1570 : 2185470 : }
1571 [ + + ][ + + ]: 974658 : else if (d_type == typ_tsym || d_type == typ_tconstraint)
1572 : : {
1573 [ + + ]: 7060 : for (std::pair<const size_t, size_t>& qvn : d_qni_var_num)
1574 : : {
1575 : 4239 : size_t repVar = d_qi->getCurrentRepVar(qvn.second);
1576 [ + + ]: 4239 : if (d_qi->d_match[repVar].isNull())
1577 : : {
1578 [ + - ]: 8118 : Trace("qcf-match-debug") << "Force matching on child #" << qvn.first
1579 : 4059 : << ", which is var #" << repVar << std::endl;
1580 : 4059 : d_qni_bound[qvn.first] = repVar;
1581 : : }
1582 : : }
1583 : 2821 : d_qn.push_back( NULL );
1584 : 2821 : }
1585 [ + + ][ + + ]: 971837 : else if (d_type == typ_pred || d_type == typ_eq)
1586 : : {
1587 : : //add initial constraint
1588 [ + + ]: 4205016 : Node nn[2];
1589 : : int vn[2];
1590 [ + + ]: 700836 : if( d_type==typ_pred ){
1591 : 328609 : nn[0] = d_qi->getCurrentValue(d_n);
1592 : 328609 : int vnn = d_qi->getVarNum(nn[0]);
1593 [ + + ]: 328609 : vn[0] =
1594 : 328057 : vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1595 : 328609 : nn[1] = nodeManager()->mkConst(d_tgt);
1596 : 328609 : vn[1] = -1;
1597 : 328609 : d_tgt = true;
1598 : : }else{
1599 [ + + ]: 1116681 : for( unsigned i=0; i<2; i++ ){
1600 : 744454 : TNode nc;
1601 : 744454 : std::map<size_t, TNode>::iterator it = d_qni_gterm.find(i);
1602 [ + + ]: 744454 : if (it != d_qni_gterm.end())
1603 : : {
1604 : 230801 : nc = it->second;
1605 : : }else{
1606 : 513653 : nc = d_n[i];
1607 : : }
1608 : 744454 : nn[i] = d_qi->getCurrentValue(nc);
1609 : 744454 : int vnn = d_qi->getVarNum(nn[i]);
1610 [ + + ]: 744454 : vn[i] =
1611 : 504005 : vnn == -1 ? vnn : d_qi->getCurrentRepVar(static_cast<size_t>(vnn));
1612 : 744454 : }
1613 : : }
1614 : : bool success;
1615 [ + + ][ + + ]: 700836 : if( vn[0]==-1 && vn[1]==-1 ){
1616 : : //Trace("qcf-explain") << " reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
1617 [ + - ]: 772 : Trace("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
1618 : : //just compare values
1619 [ + + ]: 772 : if( d_tgt ){
1620 : 700 : success = nn[0] == nn[1];
1621 : : }else{
1622 [ + + ]: 72 : if (d_parent->atConflictEffort())
1623 : : {
1624 : 24 : success = d_parent->areDisequal(nn[0], nn[1]);
1625 : : }
1626 : : else
1627 : : {
1628 : 48 : success = (nn[0] != nn[1]);
1629 : : }
1630 : : }
1631 : : }else{
1632 : : //otherwise, add a constraint to a variable TODO: this may be over-eager at effort > conflict, since equality may be a propagation
1633 [ + + ][ + + ]: 700064 : if( vn[1]!=-1 && vn[0]==-1 ){
1634 : : //swap
1635 : 100833 : Node t = nn[1];
1636 : 100833 : nn[1] = nn[0];
1637 : 100833 : nn[0] = t;
1638 : 100833 : vn[0] = vn[1];
1639 : 100833 : vn[1] = -1;
1640 : 100833 : }
1641 [ + - ]: 700064 : Trace("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
1642 : : //add some constraint
1643 : 700064 : int addc = d_qi->addConstraint(vn[0], nn[1], vn[1], d_tgt, false);
1644 : 700064 : success = addc!=-1;
1645 : : //if successful and non-redundant, store that we need to cleanup this
1646 [ + + ]: 700064 : if( addc==1 ){
1647 [ + + ]: 2041875 : for (size_t i = 0; i < 2; i++)
1648 : : {
1649 [ + + ][ + - ]: 1361250 : if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
[ + + ]
1650 : 812623 : d_qni_bound[vn[i]] = vn[i];
1651 : : }
1652 : : }
1653 : 680625 : d_qni_bound_cons[vn[0]] = nn[1];
1654 : 680625 : d_qni_bound_cons_var[vn[0]] = vn[1];
1655 : : }
1656 : : }
1657 : : //if successful, we will bind values to variables
1658 [ + + ]: 700836 : if( success ){
1659 : 681308 : d_qn.push_back( NULL );
1660 : : }
1661 [ + + ][ - - ]: 2803344 : }
1662 : : else
1663 : : {
1664 [ - + ]: 271001 : if( d_children.empty() ){
1665 : : //add dummy
1666 : 0 : d_qn.push_back( NULL );
1667 : : }else{
1668 [ + + ][ + + ]: 271001 : if (d_tgt && d_n.getKind() == Kind::FORALL)
[ + + ]
1669 : : {
1670 : : //fail
1671 : : }
1672 [ + + ][ + + ]: 239517 : else if (d_n.getKind() == Kind::FORALL && d_parent->atConflictEffort())
[ + + ]
1673 : : {
1674 : : //fail
1675 : : }
1676 : : else
1677 : : {
1678 : : //reset the first child to d_tgt
1679 : 238141 : d_child_counter = 0;
1680 : 238141 : getChild(d_child_counter)->reset(d_tgt);
1681 : : }
1682 : : }
1683 : : }
1684 : 3194079 : d_binding = false;
1685 : 3194079 : d_wasSet = true;
1686 : 3194079 : Trace("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
1687 : 6038160 : }
1688 : :
1689 : 4045850 : bool MatchGen::getNextMatch()
1690 : : {
1691 [ + - ]: 4045850 : Trace("qcf-match") << " Get next match for : " << d_n << ", type = ";
1692 : 4045850 : debugPrintType( "qcf-match", d_type );
1693 [ + - ]: 4045850 : Trace("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
1694 [ + + ]: 4045850 : if( !d_use_children ){
1695 [ + + ]: 55369 : if( d_child_counter==0 ){
1696 : 28635 : d_child_counter = -1;
1697 : 28635 : return true;
1698 : : }else{
1699 : 26734 : d_wasSet = false;
1700 : 26734 : return false;
1701 : : }
1702 [ + + ][ + + ]: 3990481 : }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
[ + + ][ + + ]
[ + + ][ + + ]
1703 : 3689044 : bool success = false;
1704 : 3689044 : bool terminate = false;
1705 : : do {
1706 : 6255720 : bool doReset = false;
1707 : 6255720 : bool doFail = false;
1708 [ + + ]: 6255720 : if( !d_binding ){
1709 [ + + ]: 5468045 : if (doMatching())
1710 : : {
1711 [ + - ]: 2587951 : Trace("qcf-match-debug") << " - Matching succeeded" << std::endl;
1712 : 2587951 : d_binding = true;
1713 : 2587951 : d_binding_it = d_qni_bound.begin();
1714 : 2587951 : doReset = true;
1715 : : //for tconstraint, add constraint
1716 [ + + ]: 2587951 : if( d_type==typ_tconstraint ){
1717 : 1868 : std::map<Node, bool>::iterator it = d_qi->d_tconstraints.find(d_n);
1718 [ + - ]: 1868 : if (it == d_qi->d_tconstraints.end())
1719 : : {
1720 : 1868 : d_qi->d_tconstraints[d_n] = d_tgt;
1721 : : //store that we added this constraint
1722 : 1868 : d_qni_bound_cons[0] = d_n;
1723 : : }
1724 [ - - ]: 0 : else if (d_tgt != it->second)
1725 : : {
1726 : 0 : success = false;
1727 : 0 : terminate = true;
1728 : : }
1729 : : }
1730 : : }
1731 : : else
1732 : : {
1733 [ + - ]: 2880094 : Trace("qcf-match-debug") << " - Matching failed" << std::endl;
1734 : 2880094 : success = false;
1735 : 2880094 : terminate = true;
1736 : : }
1737 : : }else{
1738 : 787675 : doFail = true;
1739 : : }
1740 [ + + ]: 6255720 : if( d_binding ){
1741 : : //also need to create match for each variable we bound
1742 : 3375626 : success = true;
1743 [ + - ]: 3375626 : Trace("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = ";
1744 : 3375626 : debugPrintType( "qcf-match-debug", d_type );
1745 [ + - ]: 3375626 : Trace("qcf-match-debug") << "..." << std::endl;
1746 : :
1747 [ + + ][ + + ]: 8966968 : while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
[ + + ][ + + ]
1748 : 5591342 : QuantInfo::VarMgMap::const_iterator itm;
1749 [ + + ]: 5591342 : if( !doFail ){
1750 [ + - ]: 4803667 : Trace("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;
1751 : 4803667 : itm = d_qi->var_mg_find(d_binding_it->second);
1752 : : }
1753 [ + + ][ + + ]: 5591342 : if (doFail || (d_binding_it->first != 0 && itm != d_qi->var_mg_end()))
[ + + ][ + + ]
1754 : : {
1755 [ + - ]: 3425393 : Trace("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
1756 [ + + ]: 3425393 : if( doReset ){
1757 : 2211935 : itm->second->reset(true);
1758 : : }
1759 [ + + ][ + + ]: 3425393 : if (doFail || !itm->second->getNextMatch())
[ + + ]
1760 : : {
1761 : : do {
1762 [ + + ]: 5147127 : if( d_binding_it==d_qni_bound.begin() ){
1763 [ + - ]: 2566676 : Trace("qcf-match-debug") << " failed." << std::endl;
1764 : 2566676 : success = false;
1765 : : }else{
1766 : 2580451 : --d_binding_it;
1767 [ + - ]: 2580451 : Trace("qcf-match-debug") << " decrement..." << std::endl;
1768 : : }
1769 : : } while (success
1770 [ + + ][ + + ]: 6407745 : && (d_binding_it->first == 0
[ + + ]
1771 [ + + ]: 1260618 : || (!d_qi->containsVarMg(d_binding_it->second))));
1772 : 2992459 : doReset = false;
1773 : 2992459 : doFail = false;
1774 : : }
1775 : : else
1776 : : {
1777 [ + - ]: 432934 : Trace("qcf-match-debug") << " increment..." << std::endl;
1778 : 432934 : ++d_binding_it;
1779 : 432934 : doReset = true;
1780 : : }
1781 : : }
1782 : : else
1783 : : {
1784 [ + - ]: 2165949 : Trace("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl;
1785 : 2165949 : ++d_binding_it;
1786 : 2165949 : doReset = true;
1787 : : }
1788 : : }
1789 [ + + ]: 3375626 : if( !success ){
1790 : 2566676 : d_binding = false;
1791 : : }else{
1792 : 808950 : terminate = true;
1793 [ + + ]: 808950 : if( d_binding_it==d_qni_bound.begin() ){
1794 : 7724 : d_binding = false;
1795 : : }
1796 : : }
1797 : : }
1798 [ + + ]: 6255720 : }while( !terminate );
1799 : : //if not successful, clean up the variables you bound
1800 [ + + ]: 3689044 : if( !success ){
1801 [ + + ][ + + ]: 2880094 : if( d_type==typ_eq || d_type==typ_pred ){
1802 : : //clean up the constraints you added
1803 : 694883 : std::map<size_t, size_t>::iterator itb;
1804 [ + + ]: 1369578 : for (const std::pair<const size_t, TNode>& qb : d_qni_bound_cons)
1805 : : {
1806 [ + - ]: 674695 : if (!qb.second.isNull())
1807 : : {
1808 [ + - ]: 1349390 : Trace("qcf-match")
1809 : 0 : << " Clean up bound var " << qb.first
1810 [ - - ]: 674695 : << (d_tgt ? "!" : "") << " = " << qb.second << std::endl;
1811 : 674695 : itb = d_qni_bound_cons_var.find(qb.first);
1812 [ + - ]: 674695 : int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
1813 : 674695 : d_qi->addConstraint(qb.first, qb.second, vn, d_tgt, true);
1814 : : }
1815 : : }
1816 : 694883 : d_qni_bound_cons.clear();
1817 : 694883 : d_qni_bound_cons_var.clear();
1818 : 694883 : d_qni_bound.clear();
1819 : 694883 : }else{
1820 : : //clean up the matches you set
1821 [ + + ]: 3682051 : for (const std::pair<const size_t, size_t>& qb : d_qni_bound)
1822 : : {
1823 [ + - ]: 2993680 : Trace("qcf-match")
1824 : 1496840 : << " Clean up bound var " << qb.second << std::endl;
1825 [ - + ][ - + ]: 1496840 : Assert(qb.second < d_qi->getNumVars());
[ - - ]
1826 : 1496840 : d_qi->unsetMatch(qb.second);
1827 : 1496840 : d_qi->d_match_term[qb.second] = TNode::null();
1828 : : }
1829 : 2185211 : d_qni_bound.clear();
1830 : : }
1831 [ + + ]: 2880094 : if( d_type==typ_tconstraint ){
1832 : : //remove constraint if applicable
1833 [ + - ]: 1854 : if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
1834 : 1854 : d_qi->d_tconstraints.erase(d_n);
1835 : 1854 : d_qni_bound_cons.clear();
1836 : : }
1837 : : }
1838 : : }
1839 [ + - ]: 3689044 : Trace("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;
1840 : 3689044 : d_wasSet = success;
1841 : 3689044 : return success;
1842 : : }
1843 [ + - ]: 301437 : else if (d_type == typ_formula)
1844 : : {
1845 : 301437 : bool success = false;
1846 [ + + ]: 301437 : if( d_child_counter<0 ){
1847 [ - + ]: 32860 : if( d_child_counter<-1 ){
1848 : 0 : d_child_counter = -1;
1849 : : }
1850 : : }else{
1851 [ + + ][ + + ]: 1313567 : while( !success && d_child_counter>=0 ){
1852 : : //transition system based on d_child_counter
1853 [ + + ][ + + ]: 1044990 : if (d_n.getKind() == Kind::OR || d_n.getKind() == Kind::AND)
[ + + ]
1854 : : {
1855 [ + + ]: 799158 : if ((d_n.getKind() == Kind::AND) == d_tgt)
1856 : : {
1857 : : //all children must match simultaneously
1858 [ + + ]: 724950 : if (getChild(d_child_counter)->getNextMatch())
1859 : : {
1860 [ + + ]: 305433 : if( d_child_counter<(int)(getNumChildren()-1) ){
1861 : 297781 : d_child_counter++;
1862 [ + - ]: 297781 : Trace("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;
1863 : 297781 : getChild(d_child_counter)->reset(d_tgt);
1864 : : }else{
1865 : 7652 : success = true;
1866 : : }
1867 : : }
1868 : : else
1869 : : {
1870 : 419517 : d_child_counter--;
1871 : : }
1872 : : }
1873 : : else
1874 : : {
1875 : : //one child must match
1876 [ + + ]: 74208 : if (!getChild(d_child_counter)->getNextMatch())
1877 : : {
1878 [ + + ]: 55395 : if( d_child_counter<(int)(getNumChildren()-1) ){
1879 : 29880 : d_child_counter++;
1880 [ + - ]: 29880 : Trace("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;
1881 : 29880 : getChild(d_child_counter)->reset(d_tgt);
1882 : : }else{
1883 : 25515 : d_child_counter = -1;
1884 : : }
1885 : : }
1886 : : else
1887 : : {
1888 : 18813 : success = true;
1889 : : }
1890 : : }
1891 : : }
1892 [ + + ]: 245832 : else if (d_n.getKind() == Kind::EQUAL)
1893 : : {
1894 : : //construct match based on both children
1895 [ + + ]: 214781 : if( d_child_counter%2==0 ){
1896 [ + + ]: 209761 : if (getChild(0)->getNextMatch())
1897 : : {
1898 : 51037 : d_child_counter++;
1899 : 51037 : getChild(1)->reset(d_child_counter == 1);
1900 : : }
1901 : : else
1902 : : {
1903 [ + + ]: 158724 : if( d_child_counter==0 ){
1904 : 80040 : d_child_counter = 2;
1905 : 80040 : getChild(0)->reset(!d_tgt);
1906 : : }else{
1907 : 78684 : d_child_counter = -1;
1908 : : }
1909 : : }
1910 : : }
1911 [ + + ][ + + ]: 214781 : if( d_child_counter>=0 && d_child_counter%2==1 ){
1912 [ + + ]: 56057 : if (getChild(1)->getNextMatch())
1913 : : {
1914 : 6777 : success = true;
1915 : : }
1916 : : else
1917 : : {
1918 : 49280 : d_child_counter--;
1919 : : }
1920 : : }
1921 : : }
1922 [ + + ]: 31051 : else if (d_n.getKind() == Kind::ITE)
1923 : : {
1924 [ + + ]: 28277 : if( d_child_counter%2==0 ){
1925 [ + + ]: 28255 : int index1 = d_child_counter==4 ? 1 : 0;
1926 [ + + ]: 28255 : if (getChild(index1)->getNextMatch())
1927 : : {
1928 : 18404 : d_child_counter++;
1929 : 18404 : getChild(d_child_counter == 5
1930 : 18393 : ? 2
1931 [ + + ]: 18393 : : (d_tgt == (d_child_counter == 1) ? 1 : 2))
1932 [ + + ]: 36797 : ->reset(d_tgt);
1933 : : }
1934 : : else
1935 : : {
1936 [ + + ]: 9851 : if (d_child_counter == 4)
1937 : : {
1938 : 3274 : d_child_counter = -1;
1939 : : }else{
1940 : 6577 : d_child_counter +=2;
1941 : 6577 : getChild(d_child_counter == 2 ? 0 : 1)
1942 [ + + ]: 6577 : ->reset(d_child_counter == 2 ? !d_tgt : d_tgt);
1943 : : }
1944 : : }
1945 : : }
1946 [ + + ][ + + ]: 28277 : if( d_child_counter>=0 && d_child_counter%2==1 ){
1947 [ + + ][ + + ]: 18426 : int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
1948 [ + + ]: 18426 : if (getChild(index2)->getNextMatch())
1949 : : {
1950 : 229 : success = true;
1951 : : }
1952 : : else
1953 : : {
1954 : 18197 : d_child_counter--;
1955 : : }
1956 : : }
1957 : : }
1958 [ + - ]: 2774 : else if (d_n.getKind() == Kind::FORALL)
1959 : : {
1960 [ + + ]: 2774 : if (getChild(d_child_counter)->getNextMatch())
1961 : : {
1962 : 621 : success = true;
1963 : : }
1964 : : else
1965 : : {
1966 : 2153 : d_child_counter = -1;
1967 : : }
1968 : : }
1969 : : }
1970 : 268577 : d_wasSet = success;
1971 [ + - ]: 268577 : Trace("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;
1972 : 268577 : return success;
1973 : : }
1974 : : }
1975 [ + - ]: 32860 : Trace("qcf-match") << " ...already finished for " << d_n << std::endl;
1976 : 32860 : return false;
1977 : : }
1978 : :
1979 : 5468045 : bool MatchGen::doMatching()
1980 : : {
1981 [ + + ]: 5468045 : if (d_qn.empty())
1982 : : {
1983 : 967265 : return false;
1984 : : }
1985 [ + + ]: 4500780 : if (d_qn[0] == NULL)
1986 : : {
1987 : 688818 : d_qn.clear();
1988 : 688818 : return true;
1989 : : }
1990 [ - + ][ - + ]: 3811962 : Assert(d_type == typ_var);
[ - - ]
1991 [ - + ][ - + ]: 3811962 : Assert(d_qni_size > 0);
[ - - ]
1992 : : bool invalidMatch;
1993 : : do
1994 : : {
1995 : 24288505 : invalidMatch = false;
1996 [ + - ]: 48577010 : Trace("qcf-match-debug") << " Do matching " << d_n << " "
1997 : 24288505 : << d_qn.size() << " " << d_qni.size() << std::endl;
1998 [ + + ]: 24288505 : if (d_qn.size() == d_qni.size() + 1)
1999 : : {
2000 : 10689293 : size_t index = d_qni.size();
2001 : : // initialize
2002 : 10689293 : TNode val;
2003 : 10689293 : std::map<size_t, size_t>::iterator itv = d_qni_var_num.find(index);
2004 [ + + ]: 10689293 : if (itv != d_qni_var_num.end())
2005 : : {
2006 : : // get the representative variable this variable is equal to
2007 : 10371707 : size_t repVar = d_qi->getCurrentRepVar(itv->second);
2008 [ + - ]: 20743414 : Trace("qcf-match-debug")
2009 : 0 : << " Match " << index << " is a variable " << itv->second
2010 : 10371707 : << ", which is repVar " << repVar << std::endl;
2011 : : // get the value the rep variable
2012 [ + + ]: 10371707 : if (!d_qi->d_match[repVar].isNull())
2013 : : {
2014 : 6660053 : val = d_qi->d_match[repVar];
2015 [ + - ]: 13320106 : Trace("qcf-match-debug")
2016 : 6660053 : << " Variable is already bound to " << val << std::endl;
2017 : : }
2018 : : else
2019 : : {
2020 : : // binding a variable
2021 : 3711654 : d_qni_bound[index] = repVar;
2022 : 3711654 : std::map<TNode, TNodeTrie>::iterator it = d_qn[index]->d_data.begin();
2023 [ + - ]: 3711654 : if (it != d_qn[index]->d_data.end())
2024 : : {
2025 : 3711654 : d_qni.push_back(it);
2026 : : // set the match
2027 [ + + ][ - - ]: 7423308 : if (it->first.getType() == d_qi->d_var_types[repVar]
2028 [ + - ][ + + ]: 7423308 : && d_qi->setMatch(d_qni_bound[index], it->first, true, true))
[ + - ][ + - ]
[ - - ]
2029 : : {
2030 [ + - ]: 4200748 : Trace("qcf-match-debug")
2031 : 2100374 : << " Binding variable" << std::endl;
2032 [ + + ]: 2100374 : if( d_qn.size()<d_qni_size ){
2033 : 793342 : d_qn.push_back( &it->second );
2034 : : }
2035 : : }
2036 : : else
2037 : : {
2038 [ + - ]: 3222560 : Trace("qcf-match")
2039 : 1611280 : << " Binding variable, currently fail." << std::endl;
2040 : 1611280 : invalidMatch = true;
2041 : : }
2042 : : }
2043 : : else
2044 : : {
2045 [ - - ]: 0 : Trace("qcf-match-debug")
2046 : 0 : << " Binding variable, fail, no more variables to bind"
2047 : 0 : << std::endl;
2048 : 0 : d_qn.pop_back();
2049 : : }
2050 : : }
2051 : : }
2052 : : else
2053 : : {
2054 [ + - ]: 635172 : Trace("qcf-match-debug")
2055 : 317586 : << " Match " << index << " is ground term" << std::endl;
2056 [ - + ][ - + ]: 317586 : Assert(d_qni_gterm.find(index) != d_qni_gterm.end());
[ - - ]
2057 : 317586 : val = d_qni_gterm[index];
2058 [ - + ][ - + ]: 317586 : Assert(!val.isNull());
[ - - ]
2059 : : }
2060 [ + + ]: 10689293 : if (!val.isNull())
2061 : : {
2062 : 13955278 : Node valr = d_parent->getRepresentative(val);
2063 : : // constrained by val
2064 : : std::map<TNode, TNodeTrie>::iterator it =
2065 : 6977639 : d_qn[index]->d_data.find(valr);
2066 [ + + ]: 6977639 : if (it != d_qn[index]->d_data.end())
2067 : : {
2068 [ + - ]: 3176533 : Trace("qcf-match-debug") << " Match" << std::endl;
2069 : 3176533 : d_qni.push_back(it);
2070 [ + + ]: 3176533 : if (d_qn.size() < d_qni_size)
2071 : : {
2072 : 3078380 : d_qn.push_back(&it->second);
2073 : : }
2074 : : }
2075 : : else
2076 : : {
2077 [ + - ]: 3801106 : Trace("qcf-match-debug") << " Failed to match" << std::endl;
2078 : 3801106 : d_qn.pop_back();
2079 : : }
2080 : 6977639 : }
2081 : 10689293 : }
2082 : : else
2083 : : {
2084 [ - + ][ - + ]: 13599212 : Assert(d_qn.size() == d_qni.size());
[ - - ]
2085 : 13599212 : size_t index = d_qni.size() - 1;
2086 : : // increment if binding this variable
2087 : 13599212 : bool success = false;
2088 : 13599212 : std::map<size_t, size_t>::iterator itb = d_qni_bound.find(index);
2089 [ + + ]: 13599212 : if (itb != d_qni_bound.end())
2090 : : {
2091 : 10443566 : d_qni[index]++;
2092 [ + + ]: 10443566 : if (d_qni[index] != d_qn[index]->d_data.end())
2093 : : {
2094 : 6742105 : success = true;
2095 [ + + ]: 6742105 : if (d_qi->setMatch(itb->second, d_qni[index]->first, true, true))
2096 : : {
2097 [ + - ]: 10783976 : Trace("qcf-match-debug")
2098 : 5391988 : << " Bind next variable" << std::endl;
2099 [ + + ]: 5391988 : if (d_qn.size() < d_qni_size)
2100 : : {
2101 : 4898040 : d_qn.push_back(&d_qni[index]->second);
2102 : : }
2103 : : }
2104 : : else
2105 : : {
2106 [ + - ]: 2700234 : Trace("qcf-match-debug")
2107 : 1350117 : << " Bind next variable, currently fail" << std::endl;
2108 : 1350117 : invalidMatch = true;
2109 : : }
2110 : : }
2111 : : else
2112 : : {
2113 : 3701461 : d_qi->unsetMatch(itb->second);
2114 : 3701461 : d_qi->d_match_term[itb->second] = TNode::null();
2115 [ + - ]: 7402922 : Trace("qcf-match-debug")
2116 : 0 : << " Bind next variable, no more variables to bind"
2117 : 3701461 : << std::endl;
2118 : : }
2119 : : }
2120 : : else
2121 : : {
2122 : : // TODO : if it equal to something else, also try that
2123 : : }
2124 : : // if not incrementing, move to next
2125 [ + + ]: 13599212 : if (!success)
2126 : : {
2127 : 6857107 : d_qn.pop_back();
2128 : 6857107 : d_qni.pop_back();
2129 : : }
2130 : : }
2131 [ + + ][ + + ]: 24288505 : } while ((!d_qn.empty() && d_qni.size() != d_qni_size) || invalidMatch);
[ + + ][ + + ]
2132 [ + + ]: 3811962 : if (d_qni.size() == d_qni_size)
2133 : : {
2134 [ - + ][ - + ]: 1899133 : Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty());
[ - - ]
2135 : 1899133 : TNode t = d_qni[d_qni.size() - 1]->second.d_data.begin()->first;
2136 [ + - ]: 3798266 : Trace("qcf-match-debug")
2137 : 1899133 : << " " << d_n << " matched " << t << std::endl;
2138 : 1899133 : d_qi->d_match_term[d_qni_var_num[0]] = t;
2139 : : // set the match terms
2140 : 1899133 : Node q = d_qi->getQuantifiedFormula();
2141 [ + + ]: 5745329 : for (const std::pair<const size_t, size_t>& qb : d_qni_bound)
2142 : : {
2143 [ + - ]: 7692392 : Trace("qcf-match-debug")
2144 : 0 : << " position " << qb.first << " bounded " << qb.second << " / "
2145 [ - + ][ - - ]: 3846196 : << q[0].getNumChildren() << std::endl;
2146 [ + + ]: 3846196 : if (qb.first > 0)
2147 : : {
2148 [ - + ][ - + ]: 2612804 : Assert(!d_qi->d_match[qb.second].isNull());
[ - - ]
2149 [ - + ][ - + ]: 2612804 : Assert(d_parent->areEqual(t[qb.first - 1], d_qi->d_match[qb.second]));
[ - - ]
2150 : 2612804 : d_qi->d_match_term[qb.second] = t[qb.first - 1];
2151 : : }
2152 : : }
2153 : 1899133 : }
2154 : 3811962 : return !d_qn.empty();
2155 : : }
2156 : :
2157 : 10946456 : void MatchGen::debugPrintType(const char* c, short typ)
2158 : : {
2159 [ + + ][ + + ]: 10946456 : switch (typ)
[ + + ][ + + ]
2160 : : {
2161 [ + - ]: 17003 : case typ_invalid: Trace(c) << "invalid"; break;
2162 [ + - ]: 1683 : case typ_ground: Trace(c) << "ground"; break;
2163 [ + - ]: 1535642 : case typ_eq: Trace(c) << "eq"; break;
2164 [ + - ]: 1433978 : case typ_pred: Trace(c) << "pred"; break;
2165 [ + - ]: 622970 : case typ_formula: Trace(c) << "formula"; break;
2166 [ + - ]: 7300465 : case typ_var: Trace(c) << "var"; break;
2167 [ + - ]: 22191 : case typ_bool_var: Trace(c) << "bool_var"; break;
2168 : : }
2169 : 10946456 : }
2170 : :
2171 : 12212 : void MatchGen::setInvalid() {
2172 : 12212 : d_type = typ_invalid;
2173 : 12212 : d_children.clear();
2174 : 12212 : }
2175 : :
2176 : 550525 : bool MatchGen::isHandledBoolConnective( TNode n ) {
2177 [ + + ][ + + ]: 550525 : return TermUtil::isBoolConnectiveTerm(n) && n.getKind() != Kind::SEP_STAR;
[ + - ][ - - ]
2178 : : }
2179 : :
2180 : 2682965 : bool MatchGen::isHandledUfTerm( TNode n ) {
2181 : 2682965 : return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
2182 : : }
2183 : :
2184 : 0 : bool MatchGen::isHandled( TNode n ) {
2185 : 0 : if (n.getKind() != Kind::BOUND_VARIABLE && expr::hasBoundVar(n))
2186 : : {
2187 : 0 : if (!isHandledBoolConnective(n) && !isHandledUfTerm(n)
2188 : 0 : && n.getKind() != Kind::EQUAL && n.getKind() != Kind::ITE)
2189 : : {
2190 : 0 : return false;
2191 : : }
2192 [ - - ]: 0 : for( unsigned i=0; i<n.getNumChildren(); i++ ){
2193 [ - - ]: 0 : if( !isHandled( n[i] ) ){
2194 : 0 : return false;
2195 : : }
2196 : : }
2197 : : }
2198 : 0 : return true;
2199 : : }
2200 : :
2201 : 29815 : QuantConflictFind::QuantConflictFind(Env& env,
2202 : : QuantifiersState& qs,
2203 : : QuantifiersInferenceManager& qim,
2204 : : QuantifiersRegistry& qr,
2205 : 29815 : TermRegistry& tr)
2206 : : : QuantifiersModule(env, qs, qim, qr, tr),
2207 : 29815 : d_statistics(statisticsRegistry()),
2208 : 59630 : d_effort(EFFORT_INVALID)
2209 : : {
2210 : 29815 : }
2211 : :
2212 : : //-------------------------------------------------- registration
2213 : :
2214 : 49610 : void QuantConflictFind::registerQuantifier( Node q ) {
2215 [ + + ]: 49610 : if (!d_qreg.hasOwnership(q, this))
2216 : : {
2217 : 1853 : return;
2218 : : }
2219 : 47757 : d_quants.push_back(q);
2220 : 47757 : d_quant_id[q] = d_quants.size();
2221 [ - + ]: 47757 : if (TraceIsOn("qcf-qregister"))
2222 : : {
2223 [ - - ]: 0 : Trace("qcf-qregister") << "Register ";
2224 : 0 : debugPrintQuant("qcf-qregister", q);
2225 [ - - ]: 0 : Trace("qcf-qregister") << " : " << q << std::endl;
2226 : : }
2227 : : // make QcfNode structure
2228 [ + - ]: 95514 : Trace("qcf-qregister")
2229 : 0 : << "- Get relevant equality/disequality pairs, calculate flattening..."
2230 : 47757 : << std::endl;
2231 : 47757 : d_qinfo[q].reset(new QuantInfo(d_env, d_qstate, d_treg, this, q));
2232 : :
2233 : : // debug print
2234 [ - + ]: 47757 : if (TraceIsOn("qcf-qregister"))
2235 : : {
2236 : 0 : QuantInfo* qi = d_qinfo[q].get();
2237 [ - - ]: 0 : Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
2238 [ - - ]: 0 : Trace("qcf-qregister") << " ";
2239 : 0 : debugPrintQuantBody("qcf-qregister", q, q[1]);
2240 [ - - ]: 0 : Trace("qcf-qregister") << std::endl;
2241 [ - - ]: 0 : if (qi->d_vars.size() > q[0].getNumChildren())
2242 : : {
2243 [ - - ]: 0 : Trace("qcf-qregister") << " with additional constraints : " << std::endl;
2244 : 0 : for (size_t j = q[0].getNumChildren(), nvars = qi->d_vars.size();
2245 [ - - ]: 0 : j < nvars;
2246 : : j++)
2247 : : {
2248 [ - - ]: 0 : Trace("qcf-qregister") << " ?x" << j << " = ";
2249 : 0 : debugPrintQuantBody("qcf-qregister", q, qi->d_vars[j], false);
2250 [ - - ]: 0 : Trace("qcf-qregister") << std::endl;
2251 : : }
2252 : : }
2253 [ - - ]: 0 : Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
2254 : : }
2255 : : }
2256 : :
2257 : : //-------------------------------------------------- check function
2258 : :
2259 : 102606 : bool QuantConflictFind::needsCheck( Theory::Effort level ) {
2260 [ + + ][ + + ]: 102606 : return !d_qstate.isConflictingInst() && (level == Theory::EFFORT_FULL);
2261 : : }
2262 : :
2263 : 40526 : void QuantConflictFind::reset_round(CVC5_UNUSED Theory::Effort level)
2264 : : {
2265 [ + - ]: 40526 : Trace("qcf-check") << "QuantConflictFind::reset_round" << std::endl;
2266 [ + - ]: 40526 : Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
2267 : 40526 : d_eqcs.clear();
2268 : :
2269 : 40526 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine());
2270 : 40526 : TermDb* tdb = getTermDatabase();
2271 [ + + ]: 2357243 : while (!eqcs_i.isFinished())
2272 : : {
2273 : 2316717 : Node r = (*eqcs_i);
2274 [ + + ]: 2316717 : if (tdb->hasTermCurrent(r))
2275 : : {
2276 : 1655932 : TypeNode rtn = r.getType();
2277 : : // check regardless of options
2278 [ + + ]: 1655932 : if (!TermUtil::hasInstConstAttr(r))
2279 : : {
2280 : 1556736 : d_eqcs[rtn].push_back(r);
2281 : : }
2282 : 1655932 : }
2283 : 2316717 : ++eqcs_i;
2284 : 2316717 : }
2285 : 40526 : }
2286 : :
2287 : 265939 : void QuantConflictFind::setIrrelevantFunction( TNode f ) {
2288 [ + + ]: 265939 : if( d_irr_func.find( f )==d_irr_func.end() ){
2289 : 34670 : d_irr_func[f] = true;
2290 : 34670 : std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f );
2291 [ + + ]: 34670 : if( it != d_func_rel_dom.end()){
2292 [ + + ]: 124597 : for( unsigned j=0; j<it->second.size(); j++ ){
2293 : 99712 : d_irr_quant[it->second[j]] = true;
2294 : : }
2295 : : }
2296 : : }
2297 : 265939 : }
2298 : :
2299 : : namespace {
2300 : :
2301 : : // Returns the beginning of a range of efforts. The range can be iterated
2302 : : // through as unsigned using operator++.
2303 : 31490 : inline QuantConflictFind::Effort QcfEffortStart() {
2304 : 31490 : return QuantConflictFind::EFFORT_CONFLICT;
2305 : : }
2306 : :
2307 : : // Returns the beginning of a range of efforts. The value returned is included
2308 : : // in the range.
2309 : 31490 : inline QuantConflictFind::Effort QcfEffortEnd(options::QcfMode m) {
2310 : : return m == options::QcfMode::PROP_EQ
2311 [ + - ]: 31490 : ? QuantConflictFind::EFFORT_PROP_EQ
2312 : 31490 : : QuantConflictFind::EFFORT_CONFLICT;
2313 : : }
2314 : :
2315 : : } // namespace
2316 : :
2317 : : /** check */
2318 : 109025 : void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
2319 : : {
2320 : 109025 : CodeTimer codeTimer(d_qstate.getStats().d_cbqi_time);
2321 [ + + ]: 109025 : if (quant_e != QEFFORT_CONFLICT)
2322 : : {
2323 : 77535 : return;
2324 : : }
2325 [ + - ]: 31490 : Trace("qcf-check") << "QCF : check : " << level << std::endl;
2326 [ - + ]: 31490 : if (d_qstate.isConflictingInst())
2327 : : {
2328 [ - - ]: 0 : Trace("qcf-check2") << "QCF : finished check : already in conflict."
2329 : 0 : << std::endl;
2330 [ - - ]: 0 : if (level >= Theory::EFFORT_FULL)
2331 : : {
2332 [ - - ]: 0 : Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
2333 : : }
2334 : 0 : return;
2335 : : }
2336 : 31490 : unsigned addedLemmas = 0;
2337 : 31490 : ++(d_statistics.d_inst_rounds);
2338 : 31490 : beginCallDebug();
2339 : 31490 : int prevEt = 0;
2340 [ - + ]: 31490 : if (TraceIsOn("qcf-engine"))
2341 : : {
2342 : 0 : prevEt = d_statistics.d_entailment_checks.get();
2343 [ - - ]: 0 : Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
2344 : 0 : << "---" << std::endl;
2345 : : }
2346 : :
2347 : : // reset the round-specific information
2348 : 31490 : d_irr_func.clear();
2349 : 31490 : d_irr_quant.clear();
2350 : :
2351 [ - + ]: 31490 : if (TraceIsOn("qcf-debug"))
2352 : : {
2353 [ - - ]: 0 : Trace("qcf-debug") << std::endl;
2354 : 0 : debugPrint("qcf-debug");
2355 [ - - ]: 0 : Trace("qcf-debug") << std::endl;
2356 : : }
2357 : 31490 : bool isConflict = false;
2358 : 31490 : FirstOrderModel* fm = d_treg.getModel();
2359 : 31490 : size_t nquant = fm->getNumAssertedQuantifiers();
2360 : : // for each effort level (find conflict, find propagating)
2361 : 31490 : unsigned end = QcfEffortEnd(options().quantifiers.cbqiMode);
2362 [ + + ]: 86025 : for (unsigned e = QcfEffortStart(); e <= end; ++e)
2363 : : {
2364 : : // set the effort (data member for convienence of access)
2365 : 59289 : d_effort = static_cast<Effort>(e);
2366 [ + - ]: 118578 : Trace("qcf-check") << "Checking quantified formulas at effort " << e
2367 : 59289 : << "..." << std::endl;
2368 : : // for each quantified formula
2369 [ + + ]: 593972 : for (size_t i = 0; i < nquant; i++)
2370 : : {
2371 : 538374 : Node q = fm->getAssertedQuantifier(i, true);
2372 [ + + ][ - - ]: 538374 : if (d_qreg.hasOwnership(q, this)
2373 [ + + ]: 523839 : && d_irr_quant.find(q) == d_irr_quant.end()
2374 [ + + ][ + + ]: 1062213 : && fm->isQuantifierActive(q))
[ + + ][ + - ]
[ - - ]
2375 : : {
2376 : : // check this quantified formula
2377 : 414744 : checkQuantifiedFormula(q, isConflict, addedLemmas);
2378 [ + + ][ + + ]: 414744 : if (d_qstate.isConflictingInst() || d_qstate.isInConflict())
[ + + ]
2379 : : {
2380 : 3691 : break;
2381 : : }
2382 : : }
2383 [ + + ]: 538374 : }
2384 : : // We are done if we added a lemma, or discovered a conflict in another
2385 : : // way. An example of the latter case is when two disequal congruent terms
2386 : : // are discovered during term indexing.
2387 [ + + ][ + + ]: 59289 : if (addedLemmas > 0 || d_qstate.isInConflict())
[ + + ]
2388 : : {
2389 : 4754 : break;
2390 : : }
2391 : : }
2392 [ - + ]: 31490 : if (isConflict)
2393 : : {
2394 : 0 : d_qstate.notifyConflictingInst();
2395 : : }
2396 [ - + ]: 31490 : if (TraceIsOn("qcf-engine"))
2397 : : {
2398 [ - - ]: 0 : Trace("qcf-engine") << "Finished conflict find engine";
2399 [ - - ]: 0 : if (addedLemmas > 0)
2400 : : {
2401 [ - - ]: 0 : Trace("qcf-engine") << ", effort = "
2402 : 0 : << (d_effort == EFFORT_CONFLICT
2403 [ - - ]: 0 : ? "conflict"
2404 [ - - ]: 0 : : (d_effort == EFFORT_PROP_EQ ? "prop_eq"
2405 : 0 : : "mc"));
2406 [ - - ]: 0 : Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
2407 : : }
2408 [ - - ]: 0 : Trace("qcf-engine") << std::endl;
2409 : 0 : int currEt = d_statistics.d_entailment_checks.get();
2410 [ - - ]: 0 : if (currEt != prevEt)
2411 : : {
2412 [ - - ]: 0 : Trace("qcf-engine") << " Entailment checks = " << (currEt - prevEt)
2413 : 0 : << std::endl;
2414 : : }
2415 : : }
2416 [ + - ]: 31490 : Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
2417 : 31490 : endCallDebug();
2418 [ + + ]: 109025 : }
2419 : :
2420 : 0 : std::string QuantConflictFind::identify() const { return "cbqi"; }
2421 : :
2422 : 414744 : void QuantConflictFind::checkQuantifiedFormula(Node q,
2423 : : bool& isConflict,
2424 : : unsigned& addedLemmas)
2425 : : {
2426 [ - + ][ - + ]: 414744 : Assert(d_qinfo.find(q) != d_qinfo.end());
[ - - ]
2427 : 414744 : QuantInfo* qi = d_qinfo[q].get();
2428 [ + + ]: 414744 : if (!qi->matchGeneratorIsValid())
2429 : : {
2430 : : // quantified formula is not properly set up for matching
2431 : 154460 : return;
2432 : : }
2433 [ - + ]: 260284 : if (TraceIsOn("qcf-check"))
2434 : : {
2435 [ - - ]: 0 : Trace("qcf-check") << "Check quantified formula ";
2436 : 0 : debugPrintQuant("qcf-check", q);
2437 [ - - ]: 0 : Trace("qcf-check") << " : " << q << "..." << std::endl;
2438 : : }
2439 : :
2440 [ + - ]: 260284 : Trace("qcf-check-debug") << "Reset round..." << std::endl;
2441 [ - + ]: 260284 : if (!qi->reset_round())
2442 : : {
2443 : : // it is typically the case that another conflict (e.g. in the term
2444 : : // database) was discovered if we fail here.
2445 : 0 : return;
2446 : : }
2447 : : // try to make a matches making the body false or propagating
2448 [ + - ]: 260284 : Trace("qcf-check-debug") << "Get next match..." << std::endl;
2449 : 260284 : Instantiate* qinst = d_qim.getInstantiate();
2450 [ + + ]: 293701 : while (qi->getNextMatch())
2451 : : {
2452 [ - + ]: 37429 : if (d_qstate.isInConflict())
2453 : : {
2454 [ - - ]: 0 : Trace("qcf-check") << " ... Quantifiers engine discovered conflict, ";
2455 [ - - ]: 0 : Trace("qcf-check") << "probably related to disequal congruent terms in "
2456 : 0 : "master equality engine"
2457 : 0 : << std::endl;
2458 : 4012 : return;
2459 : : }
2460 [ - + ]: 37429 : if (TraceIsOn("qcf-inst"))
2461 : : {
2462 [ - - ]: 0 : Trace("qcf-inst") << "*** Produced match at effort " << d_effort << " : "
2463 : 0 : << std::endl;
2464 : 0 : qi->debugPrintMatch("qcf-inst");
2465 [ - - ]: 0 : Trace("qcf-inst") << std::endl;
2466 : : }
2467 : : // check whether internal match constraints are satisfied
2468 [ + + ]: 37429 : if (qi->isMatchSpurious())
2469 : : {
2470 [ + - ]: 8560 : Trace("qcf-inst") << " ... Spurious (match is inconsistent)"
2471 : 4280 : << std::endl;
2472 : 5523 : continue;
2473 : : }
2474 : : // check whether match can be completed
2475 : 33149 : std::vector<size_t> assigned;
2476 [ + + ]: 33149 : if (!qi->completeMatch(assigned))
2477 : : {
2478 [ + - ]: 2486 : Trace("qcf-inst") << " ... Spurious (cannot assign unassigned vars)"
2479 : 1243 : << std::endl;
2480 : 1243 : continue;
2481 : : }
2482 : : // check whether the match is spurious according to (T-)entailment checks
2483 : 31906 : std::vector<Node> terms;
2484 : 31906 : qi->getMatch(terms);
2485 : 31906 : bool tcs = qi->isTConstraintSpurious(terms);
2486 [ + + ]: 31906 : if (tcs)
2487 : : {
2488 [ + - ]: 46704 : Trace("qcf-inst") << " ... Spurious (match is T-inconsistent)"
2489 : 23352 : << std::endl;
2490 : : }
2491 : : else
2492 : : {
2493 : : // otherwise, we have a conflict/propagating instance
2494 : : // for debugging
2495 [ - + ]: 8554 : if (TraceIsOn("qcf-check-inst"))
2496 : : {
2497 : 0 : Node inst = qinst->getInstantiation(q, terms);
2498 [ - - ]: 0 : Trace("qcf-check-inst")
2499 : 0 : << "Check instantiation " << inst << "..." << std::endl;
2500 : 0 : Assert(!d_treg.getEntailmentCheck()->isEntailed(inst, true));
2501 : 0 : Assert(d_treg.getEntailmentCheck()->isEntailed(inst, false)
2502 : : || d_effort > EFFORT_CONFLICT);
2503 : 0 : }
2504 : : // Process the lemma: either add an instantiation or specific lemmas
2505 : : // constructed during the isTConstraintSpurious call, or both.
2506 : 17108 : InferenceId id = (d_effort == EFFORT_CONFLICT
2507 [ + + ]: 8554 : ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT
2508 : : : InferenceId::QUANTIFIERS_INST_CBQI_PROP);
2509 [ + + ]: 8554 : if (!qinst->addInstantiation(q, terms, id))
2510 : : {
2511 [ + - ]: 370 : Trace("qcf-inst") << " ... Failed to add instantiation" << std::endl;
2512 : : // This should only happen if the algorithm generates the same
2513 : : // propagating instance twice this round. In this case, return
2514 : : // to avoid exponential behavior.
2515 : 370 : return;
2516 : : }
2517 [ + - ]: 8184 : Trace("qcf-check") << " ... Added instantiation" << std::endl;
2518 [ - + ]: 8184 : if (TraceIsOn("qcf-instantiate"))
2519 : : {
2520 [ - - ]: 0 : Trace("qcf-instantiate") << "QCF instantiation: " << q << std::endl;
2521 [ - - ]: 0 : for (const Node& t : terms)
2522 : : {
2523 [ - - ]: 0 : Trace("qcf-instantiate") << " " << t << std::endl;
2524 : : }
2525 : : }
2526 [ - + ]: 8184 : if (TraceIsOn("qcf-inst"))
2527 : : {
2528 [ - - ]: 0 : Trace("qcf-inst") << "*** Was from effort " << d_effort << " : "
2529 : 0 : << std::endl;
2530 : 0 : qi->debugPrintMatch("qcf-inst");
2531 [ - - ]: 0 : Trace("qcf-inst") << std::endl;
2532 : : }
2533 : 8184 : ++addedLemmas;
2534 [ + + ]: 8184 : if (d_effort == EFFORT_CONFLICT)
2535 : : {
2536 : : // mark relevant: this ensures that quantified formula q is
2537 : : // checked first on the next round. This is an optimization to
2538 : : // ensure that quantified formulas that are more likely to have
2539 : : // conflicting instances are checked earlier.
2540 : 3642 : d_treg.getModel()->markRelevant(q);
2541 [ - + ]: 3642 : if (options().quantifiers.cbqiAllConflict)
2542 : : {
2543 : 0 : isConflict = true;
2544 : : }
2545 : : else
2546 : : {
2547 : 3642 : d_qstate.notifyConflictingInst();
2548 : : }
2549 : 3642 : return;
2550 : : }
2551 [ + - ]: 4542 : else if (d_effort == EFFORT_PROP_EQ)
2552 : : {
2553 : 4542 : d_treg.getModel()->markRelevant(q);
2554 : : }
2555 : : }
2556 : : // clean up assigned
2557 : 27894 : qi->revertMatch(assigned);
2558 : 27894 : d_tempCache.clear();
2559 [ + + ][ + + ]: 37161 : }
[ + ]
2560 [ + - ]: 512544 : Trace("qcf-check") << "Done, conflict = " << d_qstate.isConflictingInst()
2561 : 256272 : << std::endl;
2562 : : }
2563 : :
2564 : : //-------------------------------------------------- debugging
2565 : :
2566 : 0 : void QuantConflictFind::debugPrint(const char* c) const
2567 : : {
2568 : : //print the equivalance classes
2569 [ - - ]: 0 : Trace(c) << "----------EQ classes" << std::endl;
2570 : 0 : eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2571 [ - - ]: 0 : while( !eqcs_i.isFinished() ){
2572 : 0 : Node n = (*eqcs_i);
2573 : : //if( !n.getType().isInteger() ){
2574 [ - - ]: 0 : Trace(c) << " - " << n << " : {";
2575 : 0 : eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
2576 : 0 : bool pr = false;
2577 [ - - ]: 0 : while( !eqc_i.isFinished() ){
2578 : 0 : Node nn = (*eqc_i);
2579 : 0 : if (nn.getKind() != Kind::EQUAL && nn != n)
2580 : : {
2581 : 0 : Trace(c) << (pr ? "," : "" ) << " " << nn;
2582 : 0 : pr = true;
2583 : : }
2584 : 0 : ++eqc_i;
2585 : 0 : }
2586 : 0 : Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2587 : 0 : ++eqcs_i;
2588 : 0 : }
2589 : 0 : }
2590 : :
2591 : 0 : void QuantConflictFind::debugPrintQuant(const char* c, Node q) const
2592 : : {
2593 : 0 : std::map<Node, size_t>::const_iterator it = d_quant_id.find(q);
2594 [ - - ]: 0 : if (it == d_quant_id.end())
2595 : : {
2596 [ - - ]: 0 : Trace(c) << q;
2597 : 0 : return;
2598 : : }
2599 [ - - ]: 0 : Trace(c) << "Q" << it->second;
2600 : : }
2601 : :
2602 : 0 : void QuantConflictFind::debugPrintQuantBody(const char* c,
2603 : : Node q,
2604 : : Node n,
2605 : : bool doVarNum) const
2606 : : {
2607 [ - - ]: 0 : if( n.getNumChildren()==0 ){
2608 [ - - ]: 0 : Trace(c) << n;
2609 : 0 : return;
2610 : : }
2611 : : std::map<Node, std::unique_ptr<QuantInfo> >::const_iterator itq =
2612 : 0 : d_qinfo.find(q);
2613 [ - - ]: 0 : if (itq != d_qinfo.end())
2614 : : {
2615 : 0 : const QuantInfo* qi = itq->second.get();
2616 : 0 : std::map<TNode, size_t>::const_iterator itv = qi->d_var_num.find(n);
2617 [ - - ][ - - ]: 0 : if (doVarNum && itv != qi->d_var_num.end())
[ - - ]
2618 : : {
2619 [ - - ]: 0 : Trace(c) << "?x" << itv->second;
2620 : 0 : return;
2621 : : }
2622 : : }
2623 [ - - ]: 0 : Trace(c) << "(";
2624 [ - - ]: 0 : if (n.getKind() == Kind::APPLY_UF)
2625 : : {
2626 : 0 : Trace(c) << n.getOperator();
2627 : : }
2628 : : else
2629 : : {
2630 [ - - ]: 0 : Trace(c) << n.getKind();
2631 : : }
2632 [ - - ]: 0 : for (const Node& nc : n)
2633 : : {
2634 [ - - ]: 0 : Trace(c) << " ";
2635 : 0 : debugPrintQuantBody(c, q, nc);
2636 : 0 : }
2637 [ - - ]: 0 : Trace(c) << ")";
2638 : : }
2639 : :
2640 : 29815 : QuantConflictFind::Statistics::Statistics(StatisticsRegistry& sr)
2641 : 29815 : : d_inst_rounds(sr.registerInt("QuantConflictFind::Inst_Rounds")),
2642 : : d_entailment_checks(
2643 : 29815 : sr.registerInt("QuantConflictFind::Entailment_Checks"))
2644 : : {
2645 : 29815 : }
2646 : :
2647 : 40 : TNode QuantConflictFind::getZero(TypeNode tn, Kind k)
2648 : : {
2649 : 40 : std::pair<TypeNode, Kind> key(tn, k);
2650 : 40 : std::map<std::pair<TypeNode, Kind>, Node>::iterator it = d_zero.find(key);
2651 [ + + ]: 40 : if (it == d_zero.end())
2652 : : {
2653 : 16 : Node nn;
2654 [ + + ]: 16 : if (k == Kind::ADD)
2655 : : {
2656 : 9 : nn = nodeManager()->mkConstRealOrInt(tn, Rational(0));
2657 : : }
2658 : 16 : d_zero[key] = nn;
2659 : 16 : return nn;
2660 : 16 : }
2661 : 24 : return it->second;
2662 : 40 : }
2663 : :
2664 : 0 : std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) {
2665 [ - - ][ - - ]: 0 : switch (e) {
2666 : 0 : case QuantConflictFind::EFFORT_INVALID:
2667 : 0 : os << "Invalid";
2668 : 0 : break;
2669 : 0 : case QuantConflictFind::EFFORT_CONFLICT:
2670 : 0 : os << "Conflict";
2671 : 0 : break;
2672 : 0 : case QuantConflictFind::EFFORT_PROP_EQ:
2673 : 0 : os << "PropEq";
2674 : 0 : break;
2675 : : }
2676 : 0 : return os;
2677 : : }
2678 : :
2679 : 118 : bool QuantConflictFind::isPropagatingInstance(Node n) const
2680 : : {
2681 : 118 : std::unordered_set<TNode> visited;
2682 : 118 : std::vector<TNode> visit;
2683 : 118 : TNode cur;
2684 : 118 : visit.push_back(n);
2685 : : do
2686 : : {
2687 : 262 : cur = visit.back();
2688 : 262 : visit.pop_back();
2689 [ + - ]: 262 : if (visited.find(cur) == visited.end())
2690 : : {
2691 : 262 : visited.insert(cur);
2692 : 262 : Kind ck = cur.getKind();
2693 [ + + ]: 262 : if (ck == Kind::FORALL)
2694 : : {
2695 : : // do nothing
2696 : : }
2697 [ + + ]: 222 : else if (TermUtil::isBoolConnective(ck))
2698 : : {
2699 [ + + ]: 216 : for (TNode cc : cur)
2700 : : {
2701 : 144 : visit.push_back(cc);
2702 : 144 : }
2703 : : }
2704 [ - + ]: 150 : else if (!getEqualityEngine()->hasTerm(cur))
2705 : : {
2706 [ - - ]: 0 : Trace("qcf-instance-check-debug")
2707 : 0 : << "...not propagating instance because of " << cur << " " << ck
2708 : 0 : << std::endl;
2709 : 0 : return false;
2710 : : }
2711 : : }
2712 [ + + ]: 262 : } while (!visit.empty());
2713 : 118 : return true;
2714 : 118 : }
2715 : :
2716 : : } // namespace quantifiers
2717 : : } // namespace theory
2718 : : } // namespace cvc5::internal
|
