projects / cvc5.git / blob
? search:


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