projects / cvc5.git / blob
? search:


504c3dcffaf1898bcc94e7a92e4535d8dc04f281
[cvc5.git] / src / theory / quantifiers / quant_conflict_find.cpp
1 /********************* */
2 /*! \file quant_conflict_find.cpp
3 ** \verbatim
4 ** Original author: Andrew Reynolds
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
11 **
12 ** \brief quant conflict find class
13 **
14 **/
15
16 #include <vector>
17
18 #include "theory/quantifiers/quant_conflict_find.h"
19 #include "theory/quantifiers/quant_util.h"
20 #include "theory/theory_engine.h"
21 #include "theory/quantifiers/options.h"
22 #include "theory/quantifiers/term_database.h"
23 #include "theory/quantifiers/trigger.h"
24
25 using namespace CVC4;
26 using namespace CVC4::kind;
27 using namespace CVC4::theory;
28 using namespace CVC4::theory::quantifiers;
29 using namespace std;
30
31 namespace CVC4 {
32
33
34
35 void QuantInfo::initialize( Node q, Node qn ) {
36 d_q = q;
37 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
38 d_match.push_back( TNode::null() );
39 d_match_term.push_back( TNode::null() );
40 }
41
42 //register the variables
43 for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
44 d_var_num[q[0][i]] = i;
45 d_vars.push_back( q[0][i] );
46 }
47
48 registerNode( qn, true, true );
49
50
51 Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
52 d_mg = new MatchGen( this, qn );
53
54 if( d_mg->isValid() ){
55 /*
56 for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
57 if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
58 Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
59 d_mg->setInvalid();
60 break;
61 }
62 }
63 */
64 if( d_mg->isValid() ){
65 for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
66 if( d_vars[j].getKind()!=BOUND_VARIABLE ){
67 d_var_mg[j] = NULL;
68 bool is_tsym = false;
69 if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
70 is_tsym = true;
71 d_tsym_vars.push_back( j );
72 }
73 if( !is_tsym || options::qcfTConstraint() ){
74 d_var_mg[j] = new MatchGen( this, d_vars[j], true );
75 }
76 if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
77 Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
78 d_mg->setInvalid();
79 break;
80 }else{
81 std::vector< int > bvars;
82 d_var_mg[j]->determineVariableOrder( this, bvars );
83 }
84 }
85 }
86 if( d_mg->isValid() ){
87 std::vector< int > bvars;
88 d_mg->determineVariableOrder( this, bvars );
89 }
90 }
91 }else{
92 Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
93 }
94 Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
95 }
96
97 void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
98 Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
99 if( n.getKind()==FORALL ){
100 registerNode( n[1], hasPol, pol, true );
101 }else{
102 if( !MatchGen::isHandledBoolConnective( n ) ){
103 if( n.hasBoundVar() ){
104 //literals
105 if( n.getKind()==EQUAL ){
106 for( unsigned i=0; i<n.getNumChildren(); i++ ){
107 flatten( n[i], beneathQuant );
108 }
109 }else if( MatchGen::isHandledUfTerm( n ) ){
110 flatten( n, beneathQuant );
111 }else if( n.getKind()==ITE ){
112 for( unsigned i=1; i<=2; i++ ){
113 flatten( n[i], beneathQuant );
114 }
115 registerNode( n[0], false, pol, beneathQuant );
116 }else if( options::qcfTConstraint() ){
117 //a theory-specific predicate
118 for( unsigned i=0; i<n.getNumChildren(); i++ ){
119 flatten( n[i], beneathQuant );
120 }
121 }
122 }
123 }else{
124 for( unsigned i=0; i<n.getNumChildren(); i++ ){
125 bool newHasPol;
126 bool newPol;
127 QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
128 //QcfNode * qcfc = new QcfNode( d_c );
129 //qcfc->d_parent = qcf;
130 //qcf->d_child[i] = qcfc;
131 registerNode( n[i], newHasPol, newPol, beneathQuant );
132 }
133 }
134 }
135 }
136
137 void QuantInfo::flatten( Node n, bool beneathQuant ) {
138 Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
139 if( n.hasBoundVar() ){
140 if( n.getKind()==BOUND_VARIABLE ){
141 d_inMatchConstraint[n] = true;
142 }
143 //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
144 if( d_var_num.find( n )==d_var_num.end() ){
145 Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
146 d_var_num[n] = d_vars.size();
147 d_vars.push_back( n );
148 d_match.push_back( TNode::null() );
149 d_match_term.push_back( TNode::null() );
150 if( n.getKind()==ITE ){
151 registerNode( n, false, false );
152 }else{
153 for( unsigned i=0; i<n.getNumChildren(); i++ ){
154 flatten( n[i], beneathQuant );
155 }
156 }
157 }else{
158 Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
159 }
160 }else{
161 Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
162 }
163 }
164
165
166 void QuantInfo::reset_round( QuantConflictFind * p ) {
167 for( unsigned i=0; i<d_match.size(); i++ ){
168 d_match[i] = TNode::null();
169 d_match_term[i] = TNode::null();
170 }
171 d_curr_var_deq.clear();
172 d_tconstraints.clear();
173 //add built-in variable constraints
174 for( unsigned r=0; r<2; r++ ){
175 for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
176 it != d_var_constraint[r].end(); ++it ){
177 for( unsigned j=0; j<it->second.size(); j++ ){
178 Node rr = it->second[j];
179 if( !isVar( rr ) ){
180 rr = p->getRepresentative( rr );
181 }
182 if( addConstraint( p, it->first, rr, r==0 )==-1 ){
183 d_var_constraint[0].clear();
184 d_var_constraint[1].clear();
185 //quantified formula is actually equivalent to true
186 Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;
187 d_mg->d_children.clear();
188 d_mg->d_n = NodeManager::currentNM()->mkConst( true );
189 d_mg->d_type = MatchGen::typ_ground;
190 return;
191 }
192 }
193 }
194 }
195 d_mg->reset_round( p );
196 for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
197 it->second->reset_round( p );
198 }
199 //now, reset for matching
200 d_mg->reset( p, false, this );
201 }
202
203 int QuantInfo::getCurrentRepVar( int v ) {
204 if( v!=-1 && !d_match[v].isNull() ){
205 int vn = getVarNum( d_match[v] );
206 if( vn!=-1 ){
207 //int vr = getCurrentRepVar( vn );
208 //d_match[v] = d_vars[vr];
209 //return vr;
210 return getCurrentRepVar( vn );
211 }
212 }
213 return v;
214 }
215
216 TNode QuantInfo::getCurrentValue( TNode n ) {
217 int v = getVarNum( n );
218 if( v==-1 ){
219 return n;
220 }else{
221 if( d_match[v].isNull() ){
222 return n;
223 }else{
224 Assert( getVarNum( d_match[v] )!=v );
225 return getCurrentValue( d_match[v] );
226 }
227 }
228 }
229
230 TNode QuantInfo::getCurrentExpValue( TNode n ) {
231 int v = getVarNum( n );
232 if( v==-1 ){
233 return n;
234 }else{
235 if( d_match[v].isNull() ){
236 return n;
237 }else{
238 Assert( getVarNum( d_match[v] )!=v );
239 if( d_match_term[v].isNull() ){
240 return getCurrentValue( d_match[v] );
241 }else{
242 return d_match_term[v];
243 }
244 }
245 }
246 }
247
248 bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
249 //check disequalities
250 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
251 if( itd!=d_curr_var_deq.end() ){
252 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
253 Node cv = getCurrentValue( it->first );
254 Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
255 if( cv==n ){
256 return false;
257 }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
258 //they must actually be disequal if we are looking for conflicts
259 if( !p->areDisequal( n, cv ) ){
260 //TODO : check for entailed disequal
261
262 return false;
263 }
264 }
265 }
266 }
267 return true;
268 }
269
270 int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {
271 v = getCurrentRepVar( v );
272 int vn = getVarNum( n );
273 vn = vn==-1 ? -1 : getCurrentRepVar( vn );
274 n = getCurrentValue( n );
275 return addConstraint( p, v, n, vn, polarity, false );
276 }
277
278 int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {
279 //for handling equalities between variables, and disequalities involving variables
280 Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
281 Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
282 Assert( doRemove || n==getCurrentValue( n ) );
283 Assert( doRemove || v==getCurrentRepVar( v ) );
284 Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );
285 if( polarity ){
286 if( vn!=v ){
287 if( doRemove ){
288 if( vn!=-1 ){
289 //if set to this in the opposite direction, clean up opposite instead
290 // std::map< int, TNode >::iterator itmn = d_match.find( vn );
291 if( d_match[vn]==d_vars[v] ){
292 return addConstraint( p, vn, d_vars[v], v, true, true );
293 }else{
294 //unsetting variables equal
295 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
296 if( itd!=d_curr_var_deq.end() ){
297 //remove disequalities owned by this
298 std::vector< TNode > remDeq;
299 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
300 if( it->second==v ){
301 remDeq.push_back( it->first );
302 }
303 }
304 for( unsigned i=0; i<remDeq.size(); i++ ){
305 d_curr_var_deq[vn].erase( remDeq[i] );
306 }
307 }
308 }
309 }
310 d_match[v] = TNode::null();
311 return 1;
312 }else{
313 //std::map< int, TNode >::iterator itm = d_match.find( v );
314
315 if( vn!=-1 ){
316 Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
317 //std::map< int, TNode >::iterator itmn = d_match.find( vn );
318 if( d_match[v].isNull() ){
319 //setting variables equal
320 bool alreadySet = false;
321 if( !d_match[vn].isNull() ){
322 alreadySet = true;
323 Assert( !isVar( d_match[vn] ) );
324 }
325
326 //copy or check disequalities
327 std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
328 if( itd!=d_curr_var_deq.end() ){
329 for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
330 Node dv = getCurrentValue( it->first );
331 if( !alreadySet ){
332 if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
333 d_curr_var_deq[vn][dv] = v;
334 }
335 }else{
336 if( !p->areMatchDisequal( d_match[vn], dv ) ){
337 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
338 return -1;
339 }
340 }
341 }
342 }
343 if( alreadySet ){
344 n = getCurrentValue( n );
345 }
346 }else{
347 if( d_match[vn].isNull() ){
348 Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;
349 //set the opposite direction
350 return addConstraint( p, vn, d_vars[v], v, true, false );
351 }else{
352 Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;
353 //are they currently equal
354 return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
355 }
356 }
357 }else{
358 Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;
359 if( d_match[v].isNull() ){
360 }else{
361 //compare ground values
362 Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
363 return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
364 }
365 }
366 if( setMatch( p, v, n ) ){
367 Debug("qcf-match-debug") << " -> success" << std::endl;
368 return 1;
369 }else{
370 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
371 return -1;
372 }
373 }
374 }else{
375 Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl;
376 return 0;
377 }
378 }else{
379 if( vn==v ){
380 Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl;
381 return -1;
382 }else{
383 if( doRemove ){
384 Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );
385 d_curr_var_deq[v].erase( n );
386 return 1;
387 }else{
388 if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
389 //check if it respects equality
390 //std::map< int, TNode >::iterator itm = d_match.find( v );
391 if( !d_match[v].isNull() ){
392 TNode nv = getCurrentValue( n );
393 if( !p->areMatchDisequal( nv, d_match[v] ) ){
394 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;
395 return -1;
396 }
397 }
398 d_curr_var_deq[v][n] = v;
399 Debug("qcf-match-debug") << " -> success" << std::endl;
400 return 1;
401 }else{
402 Debug("qcf-match-debug") << " -> redundant disequality" << std::endl;
403 return 0;
404 }
405 }
406 }
407 }
408 }
409
410 bool QuantInfo::isConstrainedVar( int v ) {
411 if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
412 return true;
413 }else{
414 Node vv = getVar( v );
415 //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
416 for( unsigned i=0; i<d_match.size(); i++ ){
417 if( d_match[i]==vv ){
418 return true;
419 }
420 }
421 for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
422 for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
423 if( it2->first==vv ){
424 return true;
425 }
426 }
427 }
428 return false;
429 }
430 }
431
432 bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
433 if( getCurrentCanBeEqual( p, v, n ) ){
434 Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;
435 d_match[v] = n;
436 return true;
437 }else{
438 return false;
439 }
440 }
441
442 bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
443 for( int i=0; i<getNumVars(); i++ ){
444 //std::map< int, TNode >::iterator it = d_match.find( i );
445 if( !d_match[i].isNull() ){
446 if( !getCurrentCanBeEqual( p, i, d_match[i], p->d_effort==QuantConflictFind::effort_conflict ) ){
447 return true;
448 }
449 }
450 }
451 return false;
452 }
453
454 bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
455 if( !d_tconstraints.empty() ){
456 //check constraints
457 for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
458 //apply substitution to the tconstraint
459 Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),
460 p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),
461 terms.begin(), terms.end() );
462 cons = it->second ? cons : cons.negate();
463 if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
464 return true;
465 }
466 }
467 }
468 return false;
469 }
470
471 bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
472 Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
473 Node rew = Rewriter::rewrite( lit );
474 if( rew==p->d_false ){
475 Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
476 return false;
477 }else if( rew!=p->d_true ){
478 //if checking for conflicts, we must be sure that the constraint is entailed
479 if( chEnt ){
480 //check if it is entailed
481 Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
482 std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
483 ++(p->d_statistics.d_entailment_checks);
484 Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
485 if( !et.first ){
486 Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
487 return false;
488 }else{
489 return true;
490 }
491 }else{
492 Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
493 return true;
494 }
495 }else{
496 Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
497 return true;
498 }
499 }
500
501 bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
502 //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
503 bool doFail = false;
504 bool success = true;
505 if( doContinue ){
506 doFail = true;
507 success = false;
508 }else{
509 //solve for interpreted symbol matches
510 // this breaks the invariant that all introduced constraints are over existing terms
511 for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
512 int index = d_tsym_vars[i];
513 TNode v = getCurrentValue( d_vars[index] );
514 int slv_v = -1;
515 if( v==d_vars[index] ){
516 slv_v = index;
517 }
518 Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
519 if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
520 Kind k = d_vars[index].getKind();
521 std::vector< TNode > children;
522 for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
523 int vn = getVarNum( d_vars[index][j] );
524 if( vn!=-1 ){
525 TNode vv = getCurrentValue( d_vars[index][j] );
526 if( vv==d_vars[index][j] ){
527 //we will assign this
528 if( slv_v==-1 ){
529 Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
530 slv_v = vn;
531 if( p->d_effort!=QuantConflictFind::effort_conflict ){
532 break;
533 }
534 }else{
535 Node z = p->getZero( k );
536 if( !z.isNull() ){
537 Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
538 assigned.push_back( vn );
539 if( !setMatch( p, vn, z ) ){
540 success = false;
541 break;
542 }
543 }
544 }
545 }else{
546 Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
547 children.push_back( vv );
548 }
549 }else{
550 Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
551 children.push_back( d_vars[index][j] );
552 }
553 }
554 if( success ){
555 if( slv_v!=-1 ){
556 Node lhs;
557 if( children.empty() ){
558 lhs = p->getZero( k );
559 }else if( children.size()==1 ){
560 lhs = children[0];
561 }else{
562 lhs = NodeManager::currentNM()->mkNode( k, children );
563 }
564 Node sum;
565 if( v==d_vars[index] ){
566 sum = lhs;
567 }else{
568 if( p->d_effort==QuantConflictFind::effort_conflict ){
569 Kind kn = k;
570 if( d_vars[index].getKind()==PLUS ){
571 kn = MINUS;
572 }
573 if( kn!=k ){
574 sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
575 }
576 }
577 }
578 if( !sum.isNull() ){
579 assigned.push_back( slv_v );
580 Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
581 if( !setMatch( p, slv_v, sum ) ){
582 success = false;
583 }
584 p->d_tempCache.push_back( sum );
585 }
586 }else{
587 //must show that constraint is met
588 Node sum = NodeManager::currentNM()->mkNode( k, children );
589 Node eq = sum.eqNode( v );
590 if( !entailmentTest( p, eq ) ){
591 success = false;
592 }
593 p->d_tempCache.push_back( sum );
594 }
595 }
596 }
597
598 if( !success ){
599 break;
600 }
601 }
602 if( success ){
603 //check what is left to assign
604 d_unassigned.clear();
605 d_unassigned_tn.clear();
606 std::vector< int > unassigned[2];
607 std::vector< TypeNode > unassigned_tn[2];
608 for( int i=0; i<getNumVars(); i++ ){
609 if( d_match[i].isNull() ){
610 int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
611 unassigned[rindex].push_back( i );
612 unassigned_tn[rindex].push_back( getVar( i ).getType() );
613 assigned.push_back( i );
614 }
615 }
616 d_unassigned_nvar = unassigned[0].size();
617 for( unsigned i=0; i<2; i++ ){
618 d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
619 d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
620 }
621 d_una_eqc_count.clear();
622 d_una_index = 0;
623 }
624 }
625
626 if( !d_unassigned.empty() && ( success || doContinue ) ){
627 Trace("qcf-check") << "Assign to unassigned..." << std::endl;
628 do {
629 if( doFail ){
630 Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
631 }
632 bool invalidMatch = false;
633 while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){
634 invalidMatch = false;
635 if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){
636 //check if it has now been assigned
637 if( d_una_index<d_unassigned_nvar ){
638 if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
639 d_una_eqc_count.push_back( -1 );
640 }else{
641 d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );
642 d_una_eqc_count.push_back( 0 );
643 }
644 }else{
645 d_una_eqc_count.push_back( 0 );
646 }
647 }else{
648 bool failed = false;
649 if( !doFail ){
650 if( d_una_index<d_unassigned_nvar ){
651 if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
652 Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
653 d_una_index++;
654 }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){
655 Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
656 d_una_index++;
657 }else{
658 failed = true;
659 Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
660 }
661 }else{
662 Assert( doFail || d_una_index==(int)d_una_eqc_count.size()-1 );
663 if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
664 int currIndex = d_una_eqc_count[d_una_index];
665 d_una_eqc_count[d_una_index]++;
666 Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
667 if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
668 d_match_term[d_unassigned[d_una_index]] = TNode::null();
669 Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
670 d_una_index++;
671 }else{
672 Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
673 invalidMatch = true;
674 }
675 }else{
676 failed = true;
677 Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
678 }
679 }
680 }
681 if( doFail || failed ){
682 do{
683 if( !doFail ){
684 d_una_eqc_count.pop_back();
685 }else{
686 doFail = false;
687 }
688 d_una_index--;
689 }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );
690 }
691 }
692 }
693 success = d_una_index>=0;
694 if( success ){
695 doFail = true;
696 Trace("qcf-check-unassign") << " Try: " << std::endl;
697 for( unsigned i=0; i<d_unassigned.size(); i++ ){
698 int ui = d_unassigned[i];
699 if( !d_match[ui].isNull() ){
700 Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
701 }
702 }
703 }
704 }while( success && isMatchSpurious( p ) );
705 }
706 if( success ){
707 for( unsigned i=0; i<d_unassigned.size(); i++ ){
708 int ui = d_unassigned[i];
709 if( !d_match[ui].isNull() ){
710 Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
711 }
712 }
713 return true;
714 }else{
715 for( unsigned i=0; i<assigned.size(); i++ ){
716 d_match[ assigned[i] ] = TNode::null();
717 }
718 assigned.clear();
719 return false;
720 }
721 }
722
723 void QuantInfo::getMatch( std::vector< Node >& terms ){
724 for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
725 //Node cv = qi->getCurrentValue( qi->d_match[i] );
726 int repVar = getCurrentRepVar( i );
727 Node cv;
728 //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
729 if( !d_match_term[repVar].isNull() ){
730 cv = d_match_term[repVar];
731 }else{
732 cv = d_match[repVar];
733 }
734 Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
735 terms.push_back( cv );
736 }
737 }
738
739 void QuantInfo::revertMatch( std::vector< int >& assigned ) {
740 for( unsigned i=0; i<assigned.size(); i++ ){
741 d_match[ assigned[i] ] = TNode::null();
742 }
743 }
744
745 void QuantInfo::debugPrintMatch( const char * c ) {
746 for( int i=0; i<getNumVars(); i++ ){
747 Trace(c) << " " << d_vars[i] << " -> ";
748 if( !d_match[i].isNull() ){
749 Trace(c) << d_match[i];
750 }else{
751 Trace(c) << "(unassigned) ";
752 }
753 if( !d_curr_var_deq[i].empty() ){
754 Trace(c) << ", DEQ{ ";
755 for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
756 Trace(c) << it->first << " ";
757 }
758 Trace(c) << "}";
759 }
760 if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
761 Trace(c) << ", EXP : " << d_match_term[i];
762 }
763 Trace(c) << std::endl;
764 }
765 if( !d_tconstraints.empty() ){
766 Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
767 for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
768 Trace(c) << " " << it->first << " -> " << it->second << std::endl;
769 }
770 }
771 }
772
773 MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
774 Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
775 std::vector< Node > qni_apps;
776 d_qni_size = 0;
777 if( isVar ){
778 Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
779 if( n.getKind()==ITE ){
780 d_type = typ_ite_var;
781 d_type_not = false;
782 d_n = n;
783 d_children.push_back( MatchGen( qi, d_n[0] ) );
784 if( d_children[0].isValid() ){
785 d_type = typ_ite_var;
786 for( unsigned i=1; i<=2; i++ ){
787 Node nn = n.eqNode( n[i] );
788 d_children.push_back( MatchGen( qi, nn ) );
789 d_children[d_children.size()-1].d_qni_bound_except.push_back( 0 );
790 if( !d_children[d_children.size()-1].isValid() ){
791 setInvalid();
792 break;
793 }
794 }
795 }else{
796 d_type = typ_invalid;
797 }
798 }else{
799 d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
800 d_qni_var_num[0] = qi->getVarNum( n );
801 d_qni_size++;
802 d_type_not = false;
803 d_n = n;
804 //Node f = getOperator( n );
805 for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
806 Node nn = d_n[j];
807 Trace("qcf-qregister-debug") << " " << d_qni_size;
808 if( qi->isVar( nn ) ){
809 int v = qi->d_var_num[nn];
810 Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
811 d_qni_var_num[d_qni_size] = v;
812 //qi->addFuncParent( v, f, j );
813 }else{
814 Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
815 d_qni_gterm[d_qni_size] = nn;
816 }
817 d_qni_size++;
818 }
819 }
820 }else{
821 if( n.hasBoundVar() ){
822 d_type_not = false;
823 d_n = n;
824 if( d_n.getKind()==NOT ){
825 d_n = d_n[0];
826 d_type_not = !d_type_not;
827 }
828
829 if( isHandledBoolConnective( d_n ) ){
830 //non-literals
831 d_type = typ_formula;
832 for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
833 if( d_n.getKind()!=FORALL || i==1 ){
834 d_children.push_back( MatchGen( qi, d_n[i], false ) );
835 if( !d_children[d_children.size()-1].isValid() ){
836 setInvalid();
837 break;
838 }
839 }
840 /*
841 else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){
842 Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;
843 //if variable equality/disequality at top level, remove immediately
844 bool cIsNot = d_children[d_children.size()-1].d_type_not;
845 Node cn = d_children[d_children.size()-1].d_n;
846 Assert( cn.getKind()==EQUAL );
847 Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );
848 //make it a built-in constraint instead
849 for( unsigned i=0; i<2; i++ ){
850 if( p->d_qinfo[q].isVar( cn[i] ) ){
851 int v = p->d_qinfo[q].getVarNum( cn[i] );
852 Node cno = cn[i==0 ? 1 : 0];
853 p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );
854 break;
855 }
856 }
857 d_children.pop_back();
858 }
859 */
860 }
861 }else{
862 d_type = typ_invalid;
863 //literals
864 if( isHandledUfTerm( d_n ) ){
865 Assert( qi->isVar( d_n ) );
866 d_type = typ_pred;
867 }else if( d_n.getKind()==BOUND_VARIABLE ){
868 Assert( d_n.getType().isBoolean() );
869 d_type = typ_bool_var;
870 }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
871 for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
872 if( d_n[i].hasBoundVar() ){
873 if( !qi->isVar( d_n[i] ) ){
874 Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;
875 }
876 Assert( qi->isVar( d_n[i] ) );
877 if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
878 d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
879 }
880 }else{
881 d_qni_gterm[i] = d_n[i];
882 }
883 }
884 d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
885 Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
886 }
887 }
888 }else{
889 //we will just evaluate
890 d_n = n;
891 d_type = typ_ground;
892 }
893 //if( d_type!=typ_invalid ){
894 //determine an efficient children ordering
895 //if( !d_children.empty() ){
896 //for( unsigned i=0; i<d_children.size(); i++ ){
897 // d_children_order.push_back( i );
898 //}
899 //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){
900 //sort based on the type of the constraint : ground comes first, then literals, then others
901 //MatchGenSort mgs;
902 //mgs.d_mg = this;
903 //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
904 //}
905 //}
906 //}
907 }
908 Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
909 debugPrintType( "qcf-qregister-debug", d_type, true );
910 Trace("qcf-qregister-debug") << std::endl;
911 //Assert( d_children.size()==d_children_order.size() );
912
913 }
914
915 void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars ) {
916 int v = qi->getVarNum( n );
917 if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
918 cbvars.push_back( v );
919 }
920 for( unsigned i=0; i<n.getNumChildren(); i++ ){
921 collectBoundVar( qi, n[i], cbvars );
922 }
923 }
924
925 void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
926 Trace("qcf-qregister-debug") << "Determine variable order " << d_n << std::endl;
927 bool isCom = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF );
928 std::map< int, std::vector< int > > c_to_vars;
929 std::map< int, std::vector< int > > vars_to_c;
930 std::map< int, int > vb_count;
931 std::map< int, int > vu_count;
932 std::vector< bool > assigned;
933 Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
934 for( unsigned i=0; i<d_children.size(); i++ ){
935 collectBoundVar( qi, d_children[i].d_n, c_to_vars[i] );
936 assigned.push_back( false );
937 vb_count[i] = 0;
938 vu_count[i] = 0;
939 for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
940 int v = c_to_vars[i][j];
941 vars_to_c[v].push_back( i );
942 if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
943 vu_count[i]++;
944 if( !isCom ){
945 bvars.push_back( v );
946 }
947 }else{
948 vb_count[i]++;
949 }
950 }
951 }
952 if( isCom ){
953 //children that bind the least number of unbound variables go first
954 do {
955 int min_score = -1;
956 int min_score_index = -1;
957 for( unsigned i=0; i<d_children.size(); i++ ){
958 if( !assigned[i] ){
959 int score = vu_count[i];
960 if( min_score==-1 || score<min_score ){
961 min_score = score;
962 min_score_index = i;
963 }
964 }
965 }
966 Trace("qcf-qregister-debug") << "...assign child " << min_score_index << "/" << d_children.size() << std::endl;
967 Assert( min_score_index!=-1 );
968 //add to children order
969 d_children_order.push_back( min_score_index );
970 assigned[min_score_index] = true;
971 //if( vb_count[min_score_index]==0 ){
972 // d_independent.push_back( min_score_index );
973 //}
974 //determine order internal to children
975 d_children[min_score_index].determineVariableOrder( qi, bvars );
976 Trace("qcf-qregister-debug") << "...bind variables" << std::endl;
977 //now, make it a bound variable
978 for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
979 int v = c_to_vars[min_score_index][i];
980 if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
981 for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
982 int vc = vars_to_c[v][j];
983 vu_count[vc]--;
984 vb_count[vc]++;
985 }
986 bvars.push_back( v );
987 }
988 }
989 Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
990 }while( d_children_order.size()!=d_children.size() );
991 Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
992 }else{
993 for( unsigned i=0; i<d_children.size(); i++ ){
994 d_children_order.push_back( i );
995 d_children[i].determineVariableOrder( qi, bvars );
996 }
997 }
998 }
999
1000
1001 void MatchGen::reset_round( QuantConflictFind * p ) {
1002 d_wasSet = false;
1003 for( unsigned i=0; i<d_children.size(); i++ ){
1004 d_children[i].reset_round( p );
1005 }
1006 for( std::map< int, TNode >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){
1007 d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );
1008 }
1009 if( d_type==typ_ground ){
1010 int e = p->evaluate( d_n );
1011 if( e==1 ){
1012 d_ground_eval[0] = p->d_true;
1013 }else if( e==-1 ){
1014 d_ground_eval[0] = p->d_false;
1015 }
1016 }else if( d_type==typ_eq ){
1017 for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
1018 if( !d_n[i].hasBoundVar() ){
1019 d_ground_eval[i] = p->evaluateTerm( d_n[i] );
1020 }
1021 }
1022 }
1023 d_qni_bound_cons.clear();
1024 d_qni_bound_cons_var.clear();
1025 d_qni_bound.clear();
1026 }
1027
1028 void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
1029 d_tgt = d_type_not ? !tgt : tgt;
1030 Debug("qcf-match") << " Reset for : " << d_n << ", type : ";
1031 debugPrintType( "qcf-match", d_type );
1032 Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;
1033 d_qn.clear();
1034 d_qni.clear();
1035 d_qni_bound.clear();
1036 d_child_counter = -1;
1037 d_tgt_orig = d_tgt;
1038
1039 //set up processing matches
1040 if( d_type==typ_invalid ){
1041 //do nothing
1042 }else if( d_type==typ_ground ){
1043 if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
1044 d_child_counter = 0;
1045 }
1046 }else if( d_type==typ_bool_var ){
1047 //get current value of the variable
1048 TNode n = qi->getCurrentValue( d_n );
1049 int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
1050 if( vn==-1 ){
1051 //evaluate the value, see if it is compatible
1052 int e = p->evaluate( n );
1053 if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
1054 d_child_counter = 0;
1055 }
1056 }else{
1057 //unassigned, set match to true/false
1058 d_qni_bound[0] = vn;
1059 qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
1060 d_child_counter = 0;
1061 }
1062 if( d_child_counter==0 ){
1063 d_qn.push_back( NULL );
1064 }
1065 }else if( d_type==typ_var ){
1066 Assert( isHandledUfTerm( d_n ) );
1067 Node f = getOperator( p, d_n );
1068 Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl;
1069 TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f );
1070 if( qni!=NULL ){
1071 d_qn.push_back( qni );
1072 }
1073 d_matched_basis = false;
1074 }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
1075 for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
1076 int repVar = qi->getCurrentRepVar( it->second );
1077 if( qi->d_match[repVar].isNull() ){
1078 Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
1079 d_qni_bound[it->first] = repVar;
1080 }
1081 }
1082 d_qn.push_back( NULL );
1083 }else if( d_type==typ_pred || d_type==typ_eq ){
1084 //add initial constraint
1085 Node nn[2];
1086 int vn[2];
1087 if( d_type==typ_pred ){
1088 nn[0] = qi->getCurrentValue( d_n );
1089 vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
1090 nn[1] = p->getRepresentative( d_tgt ? p->d_true : p->d_false );
1091 vn[1] = -1;
1092 d_tgt = true;
1093 }else{
1094 for( unsigned i=0; i<2; i++ ){
1095 TNode nc;
1096 std::map< int, TNode >::iterator it = d_qni_gterm_rep.find( i );
1097 if( it!=d_qni_gterm_rep.end() ){
1098 nc = it->second;
1099 }else{
1100 nc = d_n[i];
1101 }
1102 nn[i] = qi->getCurrentValue( nc );
1103 vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
1104 }
1105 }
1106 bool success;
1107 if( vn[0]==-1 && vn[1]==-1 ){
1108 //Trace("qcf-explain") << " reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
1109 Debug("qcf-match-debug") << " reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
1110 //just compare values
1111 if( d_tgt ){
1112 success = p->areMatchEqual( nn[0], nn[1] );
1113 }else{
1114 if( p->d_effort==QuantConflictFind::effort_conflict ){
1115 success = p->areDisequal( nn[0], nn[1] );
1116 }else{
1117 success = p->areMatchDisequal( nn[0], nn[1] );
1118 }
1119 }
1120 }else{
1121 //otherwise, add a constraint to a variable
1122 if( vn[1]!=-1 && vn[0]==-1 ){
1123 //swap
1124 Node t = nn[1];
1125 nn[1] = nn[0];
1126 nn[0] = t;
1127 vn[0] = vn[1];
1128 vn[1] = -1;
1129 }
1130 Debug("qcf-match-debug") << " reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
1131 //add some constraint
1132 int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
1133 success = addc!=-1;
1134 //if successful and non-redundant, store that we need to cleanup this
1135 if( addc==1 ){
1136 //Trace("qcf-explain") << " reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
1137 for( unsigned i=0; i<2; i++ ){
1138 if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
1139 d_qni_bound[vn[i]] = vn[i];
1140 }
1141 }
1142 d_qni_bound_cons[vn[0]] = nn[1];
1143 d_qni_bound_cons_var[vn[0]] = vn[1];
1144 }
1145 }
1146 //if successful, we will bind values to variables
1147 if( success ){
1148 d_qn.push_back( NULL );
1149 }
1150 }else{
1151 if( d_children.empty() ){
1152 //add dummy
1153 d_qn.push_back( NULL );
1154 }else{
1155 if( d_tgt && d_n.getKind()==FORALL ){
1156 //do nothing
1157 }else{
1158 //reset the first child to d_tgt
1159 d_child_counter = 0;
1160 getChild( d_child_counter )->reset( p, d_tgt, qi );
1161 }
1162 }
1163 }
1164 d_binding = false;
1165 d_wasSet = true;
1166 Debug("qcf-match") << " reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
1167 }
1168
1169 bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
1170 Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";
1171 debugPrintType( "qcf-match", d_type );
1172 Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
1173 if( d_type==typ_invalid || d_type==typ_ground ){
1174 if( d_child_counter==0 ){
1175 d_child_counter = -1;
1176 return true;
1177 }else{
1178 d_wasSet = false;
1179 return false;
1180 }
1181 }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 ){
1182 bool success = false;
1183 bool terminate = false;
1184 do {
1185 bool doReset = false;
1186 bool doFail = false;
1187 if( !d_binding ){
1188 if( doMatching( p, qi ) ){
1189 Debug("qcf-match-debug") << " - Matching succeeded" << std::endl;
1190 d_binding = true;
1191 d_binding_it = d_qni_bound.begin();
1192 doReset = true;
1193 //for tconstraint, add constraint
1194 if( d_type==typ_tconstraint ){
1195 std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
1196 if( it==qi->d_tconstraints.end() ){
1197 qi->d_tconstraints[d_n] = d_tgt;
1198 //store that we added this constraint
1199 d_qni_bound_cons[0] = d_n;
1200 }else if( d_tgt!=it->second ){
1201 success = false;
1202 terminate = true;
1203 }
1204 }
1205 }else{
1206 Debug("qcf-match-debug") << " - Matching failed" << std::endl;
1207 success = false;
1208 terminate = true;
1209 }
1210 }else{
1211 doFail = true;
1212 }
1213 if( d_binding ){
1214 //also need to create match for each variable we bound
1215 success = true;
1216 Debug("qcf-match-debug") << " Produce matches for bound variables by " << d_n << ", type = ";
1217 debugPrintType( "qcf-match-debug", d_type );
1218 Debug("qcf-match-debug") << "..." << std::endl;
1219
1220 while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
1221 std::map< int, MatchGen * >::iterator itm;
1222 if( !doFail ){
1223 Debug("qcf-match-debug") << " check variable " << d_binding_it->second << std::endl;
1224 itm = qi->d_var_mg.find( d_binding_it->second );
1225 }
1226 if( doFail || ( d_binding_it->first!=0 && itm!=qi->d_var_mg.end() ) ){
1227 Debug("qcf-match-debug") << " we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
1228 if( doReset ){
1229 itm->second->reset( p, true, qi );
1230 }
1231 if( doFail || !itm->second->getNextMatch( p, qi ) ){
1232 do {
1233 if( d_binding_it==d_qni_bound.begin() ){
1234 Debug("qcf-match-debug") << " failed." << std::endl;
1235 success = false;
1236 }else{
1237 --d_binding_it;
1238 Debug("qcf-match-debug") << " decrement..." << std::endl;
1239 }
1240 }while( success && ( d_binding_it->first==0 || qi->d_var_mg.find( d_binding_it->second )==qi->d_var_mg.end() ) );
1241 doReset = false;
1242 doFail = false;
1243 }else{
1244 Debug("qcf-match-debug") << " increment..." << std::endl;
1245 ++d_binding_it;
1246 doReset = true;
1247 }
1248 }else{
1249 Debug("qcf-match-debug") << " skip..." << d_binding_it->second << std::endl;
1250 ++d_binding_it;
1251 doReset = true;
1252 }
1253 }
1254 if( !success ){
1255 d_binding = false;
1256 }else{
1257 terminate = true;
1258 if( d_binding_it==d_qni_bound.begin() ){
1259 d_binding = false;
1260 }
1261 }
1262 }
1263 }while( !terminate );
1264 //if not successful, clean up the variables you bound
1265 if( !success ){
1266 if( d_type==typ_eq || d_type==typ_pred ){
1267 //clean up the constraints you added
1268 for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
1269 if( !it->second.isNull() ){
1270 Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
1271 std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
1272 int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
1273 //Trace("qcf-explain") << " cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;
1274 qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
1275 }
1276 }
1277 d_qni_bound_cons.clear();
1278 d_qni_bound_cons_var.clear();
1279 d_qni_bound.clear();
1280 }else{
1281 //clean up the matches you set
1282 for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1283 Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;
1284 Assert( it->second<qi->getNumVars() );
1285 qi->d_match[ it->second ] = TNode::null();
1286 qi->d_match_term[ it->second ] = TNode::null();
1287 }
1288 d_qni_bound.clear();
1289 }
1290 if( d_type==typ_tconstraint ){
1291 //remove constraint if applicable
1292 if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
1293 qi->d_tconstraints.erase( d_n );
1294 d_qni_bound_cons.clear();
1295 }
1296 }
1297 /*
1298 if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
1299 d_matched_basis = true;
1300 Node f = getOperator( d_n );
1301 TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );
1302 if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
1303 success = true;
1304 d_qni_bound[0] = d_qni_var_num[0];
1305 }
1306 }
1307 */
1308 }
1309 Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;
1310 d_wasSet = success;
1311 return success;
1312 }else if( d_type==typ_formula || d_type==typ_ite_var ){
1313 bool success = false;
1314 if( d_child_counter<0 ){
1315 if( d_child_counter<-1 ){
1316 success = true;
1317 d_child_counter = -1;
1318 }
1319 }else{
1320 while( !success && d_child_counter>=0 ){
1321 //transition system based on d_child_counter
1322 if( d_n.getKind()==OR || d_n.getKind()==AND ){
1323 if( (d_n.getKind()==AND)==d_tgt ){
1324 //all children must match simultaneously
1325 if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1326 if( d_child_counter<(int)(getNumChildren()-1) ){
1327 d_child_counter++;
1328 Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << std::endl;
1329 getChild( d_child_counter )->reset( p, d_tgt, qi );
1330 }else{
1331 success = true;
1332 }
1333 }else{
1334 //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
1335 // d_child_counter--;
1336 //}else{
1337 d_child_counter--;
1338 //}
1339 }
1340 }else{
1341 //one child must match
1342 if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
1343 if( d_child_counter<(int)(getNumChildren()-1) ){
1344 d_child_counter++;
1345 Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;
1346 getChild( d_child_counter )->reset( p, d_tgt, qi );
1347 }else{
1348 d_child_counter = -1;
1349 }
1350 }else{
1351 success = true;
1352 }
1353 }
1354 }else if( d_n.getKind()==IFF ){
1355 //construct match based on both children
1356 if( d_child_counter%2==0 ){
1357 if( getChild( 0 )->getNextMatch( p, qi ) ){
1358 d_child_counter++;
1359 getChild( 1 )->reset( p, d_child_counter==1, qi );
1360 }else{
1361 if( d_child_counter==0 ){
1362 d_child_counter = 2;
1363 getChild( 0 )->reset( p, !d_tgt, qi );
1364 }else{
1365 d_child_counter = -1;
1366 }
1367 }
1368 }
1369 if( d_child_counter>=0 && d_child_counter%2==1 ){
1370 if( getChild( 1 )->getNextMatch( p, qi ) ){
1371 success = true;
1372 }else{
1373 d_child_counter--;
1374 }
1375 }
1376 }else if( d_n.getKind()==ITE ){
1377 if( d_child_counter%2==0 ){
1378 int index1 = d_child_counter==4 ? 1 : 0;
1379 if( getChild( index1 )->getNextMatch( p, qi ) ){
1380 d_child_counter++;
1381 getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
1382 }else{
1383 if( d_child_counter==4 || ( d_type==typ_ite_var && d_child_counter==2 ) ){
1384 d_child_counter = -1;
1385 }else{
1386 d_child_counter +=2;
1387 getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
1388 }
1389 }
1390 }
1391 if( d_child_counter>=0 && d_child_counter%2==1 ){
1392 int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
1393 if( getChild( index2 )->getNextMatch( p, qi ) ){
1394 success = true;
1395 }else{
1396 d_child_counter--;
1397 }
1398 }
1399 }else if( d_n.getKind()==FORALL ){
1400 if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1401 success = true;
1402 }else{
1403 d_child_counter = -1;
1404 }
1405 }
1406 }
1407 d_wasSet = success;
1408 Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;
1409 return success;
1410 }
1411 }
1412 Debug("qcf-match") << " ...already finished for " << d_n << std::endl;
1413 return false;
1414 }
1415
1416 bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp ) {
1417 if( d_type==typ_eq ){
1418 Node n[2];
1419 for( unsigned i=0; i<2; i++ ){
1420 Trace("qcf-explain") << "Explain term " << d_n[i] << "..." << std::endl;
1421 n[i] = getExplanationTerm( p, qi, d_n[i], exp );
1422 }
1423 Node eq = n[0].eqNode( n[1] );
1424 if( !d_tgt_orig ){
1425 eq = eq.negate();
1426 }
1427 exp.push_back( eq );
1428 Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << eq << ", set = " << d_wasSet << std::endl;
1429 return true;
1430 }else if( d_type==typ_pred ){
1431 Trace("qcf-explain") << "Explain term " << d_n << "..." << std::endl;
1432 Node n = getExplanationTerm( p, qi, d_n, exp );
1433 if( !d_tgt_orig ){
1434 n = n.negate();
1435 }
1436 exp.push_back( n );
1437 Trace("qcf-explain") << "Explanation for " << d_n << " (tgt=" << d_tgt_orig << ") is " << n << ", set = " << d_wasSet << std::endl;
1438 return true;
1439 }else if( d_type==typ_formula ){
1440 Trace("qcf-explain") << "Explanation get for " << d_n << ", counter = " << d_child_counter << ", tgt = " << d_tgt_orig << ", set = " << d_wasSet << std::endl;
1441 if( d_n.getKind()==OR || d_n.getKind()==AND ){
1442 if( (d_n.getKind()==AND)==d_tgt ){
1443 for( unsigned i=0; i<getNumChildren(); i++ ){
1444 if( !getChild( i )->getExplanation( p, qi, exp ) ){
1445 return false;
1446 }
1447 }
1448 }else{
1449 return getChild( d_child_counter )->getExplanation( p, qi, exp );
1450 }
1451 }else if( d_n.getKind()==IFF ){
1452 for( unsigned i=0; i<2; i++ ){
1453 if( !getChild( i )->getExplanation( p, qi, exp ) ){
1454 return false;
1455 }
1456 }
1457 }else if( d_n.getKind()==ITE ){
1458 for( unsigned i=0; i<3; i++ ){
1459 bool isActive = ( ( i==0 && d_child_counter!=5 ) ||
1460 ( i==1 && d_child_counter!=( d_tgt ? 3 : 1 ) ) ||
1461 ( i==2 && d_child_counter!=( d_tgt ? 1 : 3 ) ) );
1462 if( isActive ){
1463 if( !getChild( i )->getExplanation( p, qi, exp ) ){
1464 return false;
1465 }
1466 }
1467 }
1468 }else{
1469 return false;
1470 }
1471 return true;
1472 }else{
1473 return false;
1474 }
1475 }
1476
1477 Node MatchGen::getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp ) {
1478 Node v = qi->getCurrentExpValue( t );
1479 if( isHandledUfTerm( t ) ){
1480 for( unsigned i=0; i<t.getNumChildren(); i++ ){
1481 Node vi = getExplanationTerm( p, qi, t[i], exp );
1482 if( vi!=v[i] ){
1483 Node eq = vi.eqNode( v[i] );
1484 if( std::find( exp.begin(), exp.end(), eq )==exp.end() ){
1485 Trace("qcf-explain") << " add : " << eq << "." << std::endl;
1486 exp.push_back( eq );
1487 }
1488 }
1489 }
1490 }
1491 return v;
1492 }
1493
1494 bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
1495 if( !d_qn.empty() ){
1496 if( d_qn[0]==NULL ){
1497 d_qn.clear();
1498 return true;
1499 }else{
1500 Assert( d_type==typ_var );
1501 Assert( d_qni_size>0 );
1502 bool invalidMatch;
1503 do {
1504 invalidMatch = false;
1505 Debug("qcf-match-debug") << " Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
1506 if( d_qn.size()==d_qni.size()+1 ) {
1507 int index = (int)d_qni.size();
1508 //initialize
1509 TNode val;
1510 std::map< int, int >::iterator itv = d_qni_var_num.find( index );
1511 if( itv!=d_qni_var_num.end() ){
1512 //get the representative variable this variable is equal to
1513 int repVar = qi->getCurrentRepVar( itv->second );
1514 Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
1515 //get the value the rep variable
1516 //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
1517 if( !qi->d_match[repVar].isNull() ){
1518 val = qi->d_match[repVar];
1519 Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;
1520 }else{
1521 //binding a variable
1522 d_qni_bound[index] = repVar;
1523 std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin();
1524 if( it != d_qn[index]->d_data.end() ) {
1525 d_qni.push_back( it );
1526 //set the match
1527 if( qi->setMatch( p, d_qni_bound[index], it->first ) ){
1528 Debug("qcf-match-debug") << " Binding variable" << std::endl;
1529 if( d_qn.size()<d_qni_size ){
1530 d_qn.push_back( &it->second );
1531 }
1532 }else{
1533 Debug("qcf-match") << " Binding variable, currently fail." << std::endl;
1534 invalidMatch = true;
1535 }
1536 }else{
1537 Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl;
1538 d_qn.pop_back();
1539 }
1540 }
1541 }else{
1542 Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl;
1543 Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );
1544 Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );
1545 val = d_qni_gterm_rep[index];
1546 Assert( !val.isNull() );
1547 }
1548 if( !val.isNull() ){
1549 //constrained by val
1550 std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val );
1551 if( it!=d_qn[index]->d_data.end() ){
1552 Debug("qcf-match-debug") << " Match" << std::endl;
1553 d_qni.push_back( it );
1554 if( d_qn.size()<d_qni_size ){
1555 d_qn.push_back( &it->second );
1556 }
1557 }else{
1558 Debug("qcf-match-debug") << " Failed to match" << std::endl;
1559 d_qn.pop_back();
1560 }
1561 }
1562 }else{
1563 Assert( d_qn.size()==d_qni.size() );
1564 int index = d_qni.size()-1;
1565 //increment if binding this variable
1566 bool success = false;
1567 std::map< int, int >::iterator itb = d_qni_bound.find( index );
1568 if( itb!=d_qni_bound.end() ){
1569 d_qni[index]++;
1570 if( d_qni[index]!=d_qn[index]->d_data.end() ){
1571 success = true;
1572 if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
1573 Debug("qcf-match-debug") << " Bind next variable" << std::endl;
1574 if( d_qn.size()<d_qni_size ){
1575 d_qn.push_back( &d_qni[index]->second );
1576 }
1577 }else{
1578 Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl;
1579 invalidMatch = true;
1580 }
1581 }else{
1582 qi->d_match[ itb->second ] = TNode::null();
1583 qi->d_match_term[ itb->second ] = TNode::null();
1584 Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl;
1585 }
1586 }else{
1587 //TODO : if it equal to something else, also try that
1588 }
1589 //if not incrementing, move to next
1590 if( !success ){
1591 d_qn.pop_back();
1592 d_qni.pop_back();
1593 }
1594 }
1595 }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
1596 if( d_qni.size()==d_qni_size ){
1597 //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
1598 //Debug("qcf-match-debug") << " We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
1599 Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
1600 TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
1601 Debug("qcf-match-debug") << " " << d_n << " matched " << t << std::endl;
1602 qi->d_match_term[d_qni_var_num[0]] = t;
1603 //set the match terms
1604 for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1605 Debug("qcf-match-debug") << " position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
1606 //if( it->second<(int)qi->d_q[0].getNumChildren() ){ //if it is an actual variable, we are interested in knowing the actual term
1607 if( it->first>0 ){
1608 Assert( !qi->d_match[ it->second ].isNull() );
1609 Assert( p->areEqual( t[it->first-1], qi->d_match[ it->second ] ) );
1610 qi->d_match_term[it->second] = t[it->first-1];
1611 }
1612 //}
1613 }
1614 }
1615 }
1616 }
1617 return !d_qn.empty();
1618 }
1619
1620 void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
1621 if( isTrace ){
1622 switch( typ ){
1623 case typ_invalid: Trace(c) << "invalid";break;
1624 case typ_ground: Trace(c) << "ground";break;
1625 case typ_eq: Trace(c) << "eq";break;
1626 case typ_pred: Trace(c) << "pred";break;
1627 case typ_formula: Trace(c) << "formula";break;
1628 case typ_var: Trace(c) << "var";break;
1629 case typ_ite_var: Trace(c) << "ite_var";break;
1630 case typ_bool_var: Trace(c) << "bool_var";break;
1631 }
1632 }else{
1633 switch( typ ){
1634 case typ_invalid: Debug(c) << "invalid";break;
1635 case typ_ground: Debug(c) << "ground";break;
1636 case typ_eq: Debug(c) << "eq";break;
1637 case typ_pred: Debug(c) << "pred";break;
1638 case typ_formula: Debug(c) << "formula";break;
1639 case typ_var: Debug(c) << "var";break;
1640 case typ_ite_var: Debug(c) << "ite_var";break;
1641 case typ_bool_var: Debug(c) << "bool_var";break;
1642 }
1643 }
1644 }
1645
1646 void MatchGen::setInvalid() {
1647 d_type = typ_invalid;
1648 d_children.clear();
1649 }
1650
1651 bool MatchGen::isHandledBoolConnective( TNode n ) {
1652 return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT );
1653 }
1654
1655 bool MatchGen::isHandledUfTerm( TNode n ) {
1656 //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
1657 // n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
1658 return inst::Trigger::isAtomicTriggerKind( n.getKind() );
1659 }
1660
1661 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
1662 if( isHandledUfTerm( n ) ){
1663 return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );
1664 }else{
1665 return Node::null();
1666 }
1667 }
1668
1669 bool MatchGen::isHandled( TNode n ) {
1670 if( n.getKind()!=BOUND_VARIABLE && n.hasBoundVar() ){
1671 if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
1672 return false;
1673 }
1674 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1675 if( !isHandled( n[i] ) ){
1676 return false;
1677 }
1678 }
1679 }
1680 return true;
1681 }
1682
1683
1684 QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
1685 QuantifiersModule( qe ),
1686 d_c( c ),
1687 d_conflict( c, false ),
1688 d_qassert( c ) {
1689 d_fid_count = 0;
1690 d_true = NodeManager::currentNM()->mkConst<bool>(true);
1691 d_false = NodeManager::currentNM()->mkConst<bool>(false);
1692 }
1693
1694 Node QuantConflictFind::mkEqNode( Node a, Node b ) {
1695 if( a.getType().isBoolean() ){
1696 return a.iffNode( b );
1697 }else{
1698 return a.eqNode( b );
1699 }
1700 }
1701
1702 //-------------------------------------------------- registration
1703
1704 void QuantConflictFind::registerQuantifier( Node q ) {
1705 if( !TermDb::isRewriteRule( q ) ){
1706 d_quants.push_back( q );
1707 d_quant_id[q] = d_quants.size();
1708 Trace("qcf-qregister") << "Register ";
1709 debugPrintQuant( "qcf-qregister", q );
1710 Trace("qcf-qregister") << " : " << q << std::endl;
1711 //make QcfNode structure
1712 Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
1713 d_qinfo[q].initialize( q, q[1] );
1714
1715 //debug print
1716 Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
1717 Trace("qcf-qregister") << " ";
1718 debugPrintQuantBody( "qcf-qregister", q, q[1] );
1719 Trace("qcf-qregister") << std::endl;
1720 if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
1721 Trace("qcf-qregister") << " with additional constraints : " << std::endl;
1722 for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
1723 Trace("qcf-qregister") << " ?x" << j << " = ";
1724 debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
1725 Trace("qcf-qregister") << std::endl;
1726 }
1727 }
1728
1729 Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
1730 }
1731 }
1732
1733 int QuantConflictFind::evaluate( Node n, bool pref, bool hasPref ) {
1734 int ret = 0;
1735 if( n.getKind()==EQUAL ){
1736 Node n1 = evaluateTerm( n[0] );
1737 Node n2 = evaluateTerm( n[1] );
1738 Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;
1739 if( areEqual( n1, n2 ) ){
1740 ret = 1;
1741 }else if( areDisequal( n1, n2 ) ){
1742 ret = -1;
1743 }
1744 //else if( d_effort>QuantConflictFind::effort_conflict ){
1745 // ret = -1;
1746 //}
1747 }else if( MatchGen::isHandledUfTerm( n ) ){ //predicate
1748 Node nn = evaluateTerm( n );
1749 Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;
1750 if( areEqual( nn, d_true ) ){
1751 ret = 1;
1752 }else if( areEqual( nn, d_false ) ){
1753 ret = -1;
1754 }
1755 //else if( d_effort>QuantConflictFind::effort_conflict ){
1756 // ret = -1;
1757 //}
1758 }else if( n.getKind()==NOT ){
1759 return -evaluate( n[0] );
1760 }else if( n.getKind()==ITE ){
1761 int cev1 = evaluate( n[0] );
1762 int cevc[2] = { 0, 0 };
1763 for( unsigned i=0; i<2; i++ ){
1764 if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){
1765 cevc[i] = evaluate( n[i+1] );
1766 if( cev1!=0 ){
1767 ret = cevc[i];
1768 break;
1769 }else if( cevc[i]==0 ){
1770 break;
1771 }
1772 }
1773 }
1774 if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){
1775 ret = cevc[0];
1776 }
1777 }else if( n.getKind()==IFF ){
1778 int cev1 = evaluate( n[0] );
1779 if( cev1!=0 ){
1780 int cev2 = evaluate( n[1] );
1781 if( cev2!=0 ){
1782 ret = cev1==cev2 ? 1 : -1;
1783 }
1784 }
1785
1786 }else{
1787 int ssval = 0;
1788 if( n.getKind()==OR ){
1789 ssval = 1;
1790 }else if( n.getKind()==AND ){
1791 ssval = -1;
1792 }
1793 bool isUnk = false;
1794 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1795 int cev = evaluate( n[i] );
1796 if( cev==ssval ){
1797 ret = ssval;
1798 break;
1799 }else if( cev==0 ){
1800 isUnk = true;
1801 }
1802 }
1803 if( ret==0 && !isUnk ){
1804 ret = -ssval;
1805 }
1806 }
1807 Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;
1808 return ret;
1809 }
1810
1811 short QuantConflictFind::getMaxQcfEffort() {
1812 if( options::qcfMode()==QCF_CONFLICT_ONLY ){
1813 return effort_conflict;
1814 }else if( options::qcfMode()==QCF_PROP_EQ ){
1815 return effort_prop_eq;
1816 }else if( options::qcfMode()==QCF_MC ){
1817 return effort_mc;
1818 }else{
1819 return 0;
1820 }
1821 }
1822
1823 bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
1824 //if( d_effort==QuantConflictFind::effort_mc ){
1825 // return n1==n2 || !areDisequal( n1, n2 );
1826 //}else{
1827 return n1==n2;
1828 //}
1829 }
1830
1831 bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
1832 //if( d_effort==QuantConflictFind::effort_conflict ){
1833 // return areDisequal( n1, n2 );
1834 //}else{
1835 return n1!=n2;
1836 //}
1837 }
1838
1839 //-------------------------------------------------- handling assertions / eqc
1840
1841 void QuantConflictFind::assertNode( Node q ) {
1842 if( !TermDb::isRewriteRule( q ) ){
1843 Trace("qcf-proc") << "QCF : assertQuantifier : ";
1844 debugPrintQuant("qcf-proc", q);
1845 Trace("qcf-proc") << std::endl;
1846 d_qassert.push_back( q );
1847 //set the eqRegistries that this depends on to true
1848 //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
1849 // it->first->d_active.set( true );
1850 //}
1851 }
1852 }
1853
1854 eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {
1855 //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
1856 return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
1857 }
1858 bool QuantConflictFind::areEqual( Node n1, Node n2 ) {
1859 return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );
1860 }
1861 bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {
1862 return n1!=n2 && getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );
1863 }
1864 Node QuantConflictFind::getRepresentative( Node n ) {
1865 if( getEqualityEngine()->hasTerm( n ) ){
1866 return getEqualityEngine()->getRepresentative( n );
1867 }else{
1868 return n;
1869 }
1870 }
1871 TermDb* QuantConflictFind::getTermDatabase() {
1872 return d_quantEngine->getTermDatabase();
1873 }
1874
1875 Node QuantConflictFind::evaluateTerm( Node n ) {
1876 if( MatchGen::isHandledUfTerm( n ) ){
1877 Node f = MatchGen::getOperator( this, n );
1878 Node nn;
1879 if( getEqualityEngine()->hasTerm( n ) ){
1880 nn = getTermDatabase()->existsTerm( f, n );
1881 }else{
1882 std::vector< TNode > args;
1883 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1884 Node c = evaluateTerm( n[i] );
1885 args.push_back( c );
1886 }
1887 nn = getTermDatabase()->d_func_map_trie[f].existsTerm( args );
1888 }
1889 if( !nn.isNull() ){
1890 Debug("qcf-eval") << "GT: Term " << nn << " for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
1891 return getRepresentative( nn );
1892 }else{
1893 Debug("qcf-eval") << "GT: No term for " << n << " hasTerm = " << getEqualityEngine()->hasTerm( n ) << std::endl;
1894 return n;
1895 }
1896 }else if( n.getKind()==ITE ){
1897 int v = evaluate( n[0], false, false );
1898 if( v==1 ){
1899 return evaluateTerm( n[1] );
1900 }else if( v==-1 ){
1901 return evaluateTerm( n[2] );
1902 }
1903 }
1904 return getRepresentative( n );
1905 }
1906
1907 /** new node */
1908 void QuantConflictFind::newEqClass( Node n ) {
1909 //Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;
1910 //Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;
1911 }
1912
1913 /** merge */
1914 void QuantConflictFind::merge( Node a, Node b ) {
1915
1916 }
1917
1918 /** assert disequal */
1919 void QuantConflictFind::assertDisequal( Node a, Node b ) {
1920
1921 }
1922
1923 //-------------------------------------------------- check function
1924
1925 bool QuantConflictFind::needsCheck( Theory::Effort level ) {
1926 bool performCheck = false;
1927 if( options::quantConflictFind() && !d_conflict ){
1928 if( level==Theory::EFFORT_LAST_CALL ){
1929 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
1930 }else if( level==Theory::EFFORT_FULL ){
1931 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
1932 }else if( level==Theory::EFFORT_STANDARD ){
1933 performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
1934 }
1935 }
1936 return performCheck;
1937 }
1938
1939 void QuantConflictFind::reset_round( Theory::Effort level ) {
1940 d_needs_computeRelEqr = true;
1941 }
1942
1943 /** check */
1944 void QuantConflictFind::check( Theory::Effort level, unsigned quant_e ) {
1945 if( quant_e==QuantifiersEngine::QEFFORT_CONFLICT ){
1946 Trace("qcf-check") << "QCF : check : " << level << std::endl;
1947 if( d_conflict ){
1948 Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
1949 if( level>=Theory::EFFORT_FULL ){
1950 Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
1951 //Assert( false );
1952 }
1953 }else{
1954 int addedLemmas = 0;
1955 ++(d_statistics.d_inst_rounds);
1956 double clSet = 0;
1957 int prevEt = 0;
1958 if( Trace.isOn("qcf-engine") ){
1959 prevEt = d_statistics.d_entailment_checks.getData();
1960 clSet = double(clock())/double(CLOCKS_PER_SEC);
1961 Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
1962 }
1963 computeRelevantEqr();
1964
1965 //determine order for quantified formulas
1966 std::vector< Node > qorder;
1967 std::map< Node, bool > qassert;
1968 //mark which are asserted
1969 for( unsigned i=0; i<d_qassert.size(); i++ ){
1970 qassert[d_qassert[i]] = true;
1971 }
1972 //add which ones are specified in the order
1973 for( unsigned i=0; i<d_quant_order.size(); i++ ){
1974 Node n = d_quant_order[i];
1975 if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
1976 qorder.push_back( n );
1977 }
1978 }
1979 d_quant_order.clear();
1980 d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
1981 //add remaining
1982 for( unsigned i=0; i<d_qassert.size(); i++ ){
1983 Node n = d_qassert[i];
1984 if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
1985 qorder.push_back( n );
1986 }
1987 }
1988
1989 if( Trace.isOn("qcf-debug") ){
1990 Trace("qcf-debug") << std::endl;
1991 debugPrint("qcf-debug");
1992 Trace("qcf-debug") << std::endl;
1993 }
1994 short end_e = getMaxQcfEffort();
1995 for( short e = effort_conflict; e<=end_e; e++ ){
1996 d_effort = e;
1997 Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
1998 for( unsigned j=0; j<qorder.size(); j++ ){
1999 Node q = qorder[j];
2000 QuantInfo * qi = &d_qinfo[q];
2001
2002 Assert( d_qinfo.find( q )!=d_qinfo.end() );
2003 if( qi->d_mg->isValid() ){
2004 Trace("qcf-check") << "Check quantified formula ";
2005 debugPrintQuant("qcf-check", q);
2006 Trace("qcf-check") << " : " << q << "..." << std::endl;
2007
2008 Trace("qcf-check-debug") << "Reset round..." << std::endl;
2009 qi->reset_round( this );
2010 //try to make a matches making the body false
2011 Trace("qcf-check-debug") << "Get next match..." << std::endl;
2012 while( qi->d_mg->getNextMatch( this, qi ) ){
2013 Trace("qcf-check") << "*** Produced match at effort " << e << " : " << std::endl;
2014 qi->debugPrintMatch("qcf-check");
2015 Trace("qcf-check") << std::endl;
2016 std::vector< int > assigned;
2017 if( !qi->isMatchSpurious( this ) ){
2018 if( qi->completeMatch( this, assigned ) ){
2019 std::vector< Node > terms;
2020 qi->getMatch( terms );
2021 if( !qi->isTConstraintSpurious( this, terms ) ){
2022 if( Debug.isOn("qcf-check-inst") ){
2023 //if( e==effort_conflict ){
2024 Node inst = d_quantEngine->getInstantiation( q, terms );
2025 Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
2026 Assert( evaluate( inst )!=1 );
2027 Assert( evaluate( inst )==-1 || e>effort_conflict );
2028 //}
2029 }
2030 if( d_quantEngine->addInstantiation( q, terms, false ) ){
2031 Trace("qcf-check") << " ... Added instantiation" << std::endl;
2032 Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
2033 qi->debugPrintMatch("qcf-inst");
2034 Trace("qcf-inst") << std::endl;
2035 ++addedLemmas;
2036 if( e==effort_conflict ){
2037 d_quant_order.insert( d_quant_order.begin(), q );
2038 d_conflict.set( true );
2039 ++(d_statistics.d_conflict_inst);
2040 break;
2041 }else if( e==effort_prop_eq ){
2042 ++(d_statistics.d_prop_inst);
2043 }
2044 }else{
2045 Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
2046 //Assert( false );
2047 }
2048 }
2049 //clean up assigned
2050 qi->revertMatch( assigned );
2051 d_tempCache.clear();
2052 }else{
2053 Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
2054 }
2055 }else{
2056 Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl;
2057 }
2058 }
2059 if( d_conflict ){
2060 break;
2061 }
2062 }
2063 }
2064 if( addedLemmas>0 ){
2065 break;
2066 }
2067 }
2068 if( Trace.isOn("qcf-engine") ){
2069 double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
2070 Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
2071 if( addedLemmas>0 ){
2072 Trace("qcf-engine") << ", effort = " << ( d_effort==effort_conflict ? "conflict" : ( d_effort==effort_prop_eq ? "prop_eq" : "mc" ) );
2073 Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
2074 }
2075 Trace("qcf-engine") << std::endl;
2076 int currEt = d_statistics.d_entailment_checks.getData();
2077 if( currEt!=prevEt ){
2078 Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
2079 }
2080 }
2081 Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
2082 }
2083 }
2084 }
2085
2086 void QuantConflictFind::computeRelevantEqr() {
2087 if( d_needs_computeRelEqr ){
2088 d_needs_computeRelEqr = false;
2089 Trace("qcf-check") << "Compute relevant equalities..." << std::endl;
2090 //d_uf_terms.clear();
2091 //d_eqc_uf_terms.clear();
2092 d_eqcs.clear();
2093 d_model_basis.clear();
2094 //d_arg_reps.clear();
2095 //double clSet = 0;
2096 //if( Trace.isOn("qcf-opt") ){
2097 // clSet = double(clock())/double(CLOCKS_PER_SEC);
2098 //}
2099
2100 //long nTermst = 0;
2101 //long nTerms = 0;
2102 //long nEqc = 0;
2103
2104 //which nodes are irrelevant for disequality matches
2105 std::map< TNode, bool > irrelevant_dnode;
2106 //now, store matches
2107 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2108 while( !eqcs_i.isFinished() ){
2109 //nEqc++;
2110 Node r = (*eqcs_i);
2111 TypeNode rtn = r.getType();
2112 if( options::qcfMode()==QCF_MC ){
2113 std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
2114 if( itt==d_eqcs.end() ){
2115 Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );
2116 if( !getEqualityEngine()->hasTerm( mb ) ){
2117 Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
2118 Assert( false );
2119 }
2120 Node mbr = getRepresentative( mb );
2121 if( mbr!=r ){
2122 d_eqcs[rtn].push_back( mbr );
2123 }
2124 d_eqcs[rtn].push_back( r );
2125 d_model_basis[rtn] = mb;
2126 }else{
2127 itt->second.push_back( r );
2128 }
2129 }else{
2130 d_eqcs[rtn].push_back( r );
2131 }
2132 ++eqcs_i;
2133 }
2134 /*
2135 if( Trace.isOn("qcf-opt") ){
2136 double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
2137 Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
2138 Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;
2139 Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;
2140 Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;
2141 }
2142 */
2143 }
2144 }
2145
2146
2147 //-------------------------------------------------- debugging
2148
2149
2150 void QuantConflictFind::debugPrint( const char * c ) {
2151 //print the equivalance classes
2152 Trace(c) << "----------EQ classes" << std::endl;
2153 eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2154 while( !eqcs_i.isFinished() ){
2155 Node n = (*eqcs_i);
2156 //if( !n.getType().isInteger() ){
2157 Trace(c) << " - " << n << " : {";
2158 eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
2159 bool pr = false;
2160 while( !eqc_i.isFinished() ){
2161 Node nn = (*eqc_i);
2162 if( nn.getKind()!=EQUAL && nn!=n ){
2163 Trace(c) << (pr ? "," : "" ) << " " << nn;
2164 pr = true;
2165 }
2166 ++eqc_i;
2167 }
2168 Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2169 /*
2170 EqcInfo * eqcn = getEqcInfo( n, false );
2171 if( eqcn ){
2172 Trace(c) << " DEQ : {";
2173 pr = false;
2174 for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
2175 if( (*it).second ){
2176 Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
2177 pr = true;
2178 }
2179 }
2180 Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2181 }
2182 //}
2183 */
2184 ++eqcs_i;
2185 }
2186 }
2187
2188 void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {
2189 Trace(c) << "Q" << d_quant_id[q];
2190 }
2191
2192 void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) {
2193 if( n.getNumChildren()==0 ){
2194 Trace(c) << n;
2195 }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){
2196 Trace(c) << "?x" << d_qinfo[q].d_var_num[n];
2197 }else{
2198 Trace(c) << "(";
2199 if( n.getKind()==APPLY_UF ){
2200 Trace(c) << n.getOperator();
2201 }else{
2202 Trace(c) << n.getKind();
2203 }
2204 for( unsigned i=0; i<n.getNumChildren(); i++ ){
2205 Trace(c) << " ";
2206 debugPrintQuantBody( c, q, n[i] );
2207 }
2208 Trace(c) << ")";
2209 }
2210 }
2211
2212 QuantConflictFind::Statistics::Statistics():
2213 d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
2214 d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
2215 d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
2216 d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
2217 {
2218 StatisticsRegistry::registerStat(&d_inst_rounds);
2219 StatisticsRegistry::registerStat(&d_conflict_inst);
2220 StatisticsRegistry::registerStat(&d_prop_inst);
2221 StatisticsRegistry::registerStat(&d_entailment_checks);
2222 }
2223
2224 QuantConflictFind::Statistics::~Statistics(){
2225 StatisticsRegistry::unregisterStat(&d_inst_rounds);
2226 StatisticsRegistry::unregisterStat(&d_conflict_inst);
2227 StatisticsRegistry::unregisterStat(&d_prop_inst);
2228 StatisticsRegistry::unregisterStat(&d_entailment_checks);
2229 }
2230
2231 TNode QuantConflictFind::getZero( Kind k ) {
2232 std::map< Kind, Node >::iterator it = d_zero.find( k );
2233 if( it==d_zero.end() ){
2234 Node nn;
2235 if( k==PLUS ){
2236 nn = NodeManager::currentNM()->mkConst( Rational(0) );
2237 }
2238 d_zero[k] = nn;
2239 return nn;
2240 }else{
2241 return it->second;
2242 }
2243 }
2244
2245
2246 }