504c3dcffaf1898bcc94e7a92e4535d8dc04f281
1 /********************* */
2 /*! \file quant_conflict_find.cpp
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
12 ** \brief quant conflict find class
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"
26 using namespace CVC4::kind
;
27 using namespace CVC4::theory
;
28 using namespace CVC4::theory::quantifiers
;
35 void QuantInfo::initialize( Node q
, Node qn
) {
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() );
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
] );
48 registerNode( qn
, true, true );
51 Trace("qcf-qregister") << "- Make match gen structure..." << std::endl
;
52 d_mg
= new MatchGen( this, qn
);
54 if( d_mg
->isValid() ){
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;
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
){
69 if( !MatchGen::isHandledUfTerm( d_vars
[j
] ) && d_vars
[j
].getKind()!=ITE
){
71 d_tsym_vars
.push_back( j
);
73 if( !is_tsym
|| options::qcfTConstraint() ){
74 d_var_mg
[j
] = new MatchGen( this, d_vars
[j
], true );
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
;
81 std::vector
< int > bvars
;
82 d_var_mg
[j
]->determineVariableOrder( this, bvars
);
86 if( d_mg
->isValid() ){
87 std::vector
< int > bvars
;
88 d_mg
->determineVariableOrder( this, bvars
);
92 Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl
;
94 Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg
->isValid() ? "VALID " : "INVALID" ) << " : " << q
<< std::endl
;
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 );
102 if( !MatchGen::isHandledBoolConnective( n
) ){
103 if( n
.hasBoundVar() ){
105 if( n
.getKind()==EQUAL
){
106 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
107 flatten( n
[i
], beneathQuant
);
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
);
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
);
124 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
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
);
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;
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 );
153 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
154 flatten( n
[i
], beneathQuant
);
158 Trace("qcf-qregister-debug2") << "...already processed" << std::endl
;
161 Trace("qcf-qregister-debug2") << "...is ground." << std::endl
;
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();
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
];
180 rr
= p
->getRepresentative( rr
);
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
;
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
);
199 //now, reset for matching
200 d_mg
->reset( p
, false, this );
203 int QuantInfo::getCurrentRepVar( int v
) {
204 if( v
!=-1 && !d_match
[v
].isNull() ){
205 int vn
= getVarNum( d_match
[v
] );
207 //int vr = getCurrentRepVar( vn );
208 //d_match[v] = d_vars[vr];
210 return getCurrentRepVar( vn
);
216 TNode
QuantInfo::getCurrentValue( TNode n
) {
217 int v
= getVarNum( n
);
221 if( d_match
[v
].isNull() ){
224 Assert( getVarNum( d_match
[v
] )!=v
);
225 return getCurrentValue( d_match
[v
] );
230 TNode
QuantInfo::getCurrentExpValue( TNode n
) {
231 int v
= getVarNum( n
);
235 if( d_match
[v
].isNull() ){
238 Assert( getVarNum( d_match
[v
] )!=v
);
239 if( d_match_term
[v
].isNull() ){
240 return getCurrentValue( d_match
[v
] );
242 return d_match_term
[v
];
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
;
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
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 );
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
) ) );
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 );
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
){
301 remDeq
.push_back( it
->first
);
304 for( unsigned i
=0; i
<remDeq
.size(); i
++ ){
305 d_curr_var_deq
[vn
].erase( remDeq
[i
] );
310 d_match
[v
] = TNode::null();
313 //std::map< int, TNode >::iterator itm = d_match.find( v );
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() ){
323 Assert( !isVar( d_match
[vn
] ) );
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
);
332 if( d_curr_var_deq
[vn
].find( dv
)==d_curr_var_deq
[vn
].end() ){
333 d_curr_var_deq
[vn
][dv
] = v
;
336 if( !p
->areMatchDisequal( d_match
[vn
], dv
) ){
337 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
344 n
= getCurrentValue( n
);
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 );
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;
358 Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl
;
359 if( d_match
[v
].isNull() ){
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;
366 if( setMatch( p
, v
, n
) ){
367 Debug("qcf-match-debug") << " -> success" << std::endl
;
370 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
375 Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl
;
380 Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl
;
384 Assert( d_curr_var_deq
[v
].find( n
)!=d_curr_var_deq
[v
].end() );
385 d_curr_var_deq
[v
].erase( n
);
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
;
398 d_curr_var_deq
[v
][n
] = v
;
399 Debug("qcf-match-debug") << " -> success" << std::endl
;
402 Debug("qcf-match-debug") << " -> redundant disequality" << std::endl
;
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() ){
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
){
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
){
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
;
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
) ){
454 bool QuantInfo::isTConstraintSpurious( QuantConflictFind
* p
, std::vector
< Node
>& terms
) {
455 if( !d_tconstraints
.empty() ){
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
) ){
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
;
477 }else if( rew
!=p
->d_true
){
478 //if checking for conflicts, we must be sure that the constraint is entailed
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
;
486 Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew
<< "." << std::endl
;
492 Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl
;
496 Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl
;
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)
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
] );
515 if( v
==d_vars
[index
] ){
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
] );
525 TNode vv
= getCurrentValue( d_vars
[index
][j
] );
526 if( vv
==d_vars
[index
][j
] ){
527 //we will assign this
529 Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn
<< std::endl
;
531 if( p
->d_effort
!=QuantConflictFind::effort_conflict
){
535 Node z
= p
->getZero( k
);
537 Trace("qcf-tconstraint-debug") << "...set " << d_vars
[vn
] << " = " << z
<< std::endl
;
538 assigned
.push_back( vn
);
539 if( !setMatch( p
, vn
, z
) ){
546 Trace("qcf-tconstraint-debug") << "...sum value " << vv
<< std::endl
;
547 children
.push_back( vv
);
550 Trace("qcf-tconstraint-debug") << "...sum " << d_vars
[index
][j
] << std::endl
;
551 children
.push_back( d_vars
[index
][j
] );
557 if( children
.empty() ){
558 lhs
= p
->getZero( k
);
559 }else if( children
.size()==1 ){
562 lhs
= NodeManager::currentNM()->mkNode( k
, children
);
565 if( v
==d_vars
[index
] ){
568 if( p
->d_effort
==QuantConflictFind::effort_conflict
){
570 if( d_vars
[index
].getKind()==PLUS
){
574 sum
= NodeManager::currentNM()->mkNode( kn
, v
, lhs
);
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
) ){
584 p
->d_tempCache
.push_back( sum
);
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
) ){
593 p
->d_tempCache
.push_back( sum
);
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
);
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() );
621 d_una_eqc_count
.clear();
626 if( !d_unassigned
.empty() && ( success
|| doContinue
) ){
627 Trace("qcf-check") << "Assign to unassigned..." << std::endl
;
630 Trace("qcf-check-unassign") << "Failure, try again..." << std::endl
;
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 );
641 d_var_mg
[ d_unassigned
[d_una_index
] ]->reset( p
, true, this );
642 d_una_eqc_count
.push_back( 0 );
645 d_una_eqc_count
.push_back( 0 );
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
;
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
;
659 Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index
<< std::endl
;
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
;
672 Trace("qcf-check-unassign") << "Failed match " << d_una_index
<< std::endl
;
677 Trace("qcf-check-unassign") << "No more matches " << d_una_index
<< std::endl
;
681 if( doFail
|| failed
){
684 d_una_eqc_count
.pop_back();
689 }while( d_una_index
>=0 && d_una_eqc_count
[d_una_index
]==-1 );
693 success
= d_una_index
>=0;
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
;
704 }while( success
&& isMatchSpurious( p
) );
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
;
715 for( unsigned i
=0; i
<assigned
.size(); i
++ ){
716 d_match
[ assigned
[i
] ] = TNode::null();
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
);
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
];
732 cv
= d_match
[repVar
];
734 Debug("qcf-check-inst") << "INST : " << i
<< " -> " << cv
<< ", from " << d_match
[i
] << std::endl
;
735 terms
.push_back( cv
);
739 void QuantInfo::revertMatch( std::vector
< int >& assigned
) {
740 for( unsigned i
=0; i
<assigned
.size(); i
++ ){
741 d_match
[ assigned
[i
] ] = TNode::null();
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
];
751 Trace(c
) << "(unassigned) ";
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
<< " ";
760 if( !d_match_term
[i
].isNull() && d_match_term
[i
]!=d_match
[i
] ){
761 Trace(c
) << ", EXP : " << d_match_term
[i
];
763 Trace(c
) << std::endl
;
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
;
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
;
778 Assert( qi
->d_var_num
.find( n
)!=qi
->d_var_num
.end() );
779 if( n
.getKind()==ITE
){
780 d_type
= typ_ite_var
;
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() ){
796 d_type
= typ_invalid
;
799 d_type
= isHandledUfTerm( n
) ? typ_var
: typ_tsym
;
800 d_qni_var_num
[0] = qi
->getVarNum( n
);
804 //Node f = getOperator( n );
805 for( unsigned j
=0; j
<d_n
.getNumChildren(); 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 );
814 Trace("qcf-qregister-debug") << " is gterm " << nn
<< std::endl
;
815 d_qni_gterm
[d_qni_size
] = nn
;
821 if( n
.hasBoundVar() ){
824 if( d_n
.getKind()==NOT
){
826 d_type_not
= !d_type_not
;
829 if( isHandledBoolConnective( d_n
) ){
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() ){
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 );
857 d_children.pop_back();
862 d_type
= typ_invalid
;
864 if( isHandledUfTerm( d_n
) ){
865 Assert( qi
->isVar( d_n
) );
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
;
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
]];
881 d_qni_gterm
[i
] = d_n
[i
];
884 d_type
= d_n
.getKind()==EQUAL
? typ_eq
: typ_tconstraint
;
885 Trace("qcf-tconstraint") << "T-Constraint : " << d_n
<< std::endl
;
889 //we will just evaluate
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 );
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
903 //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
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() );
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
);
920 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
921 collectBoundVar( qi
, n
[i
], cbvars
);
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 );
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() ){
945 bvars
.push_back( v
);
953 //children that bind the least number of unbound variables go first
956 int min_score_index
= -1;
957 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
959 int score
= vu_count
[i
];
960 if( min_score
==-1 || score
<min_score
){
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 );
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
];
986 bvars
.push_back( v
);
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
;
993 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
994 d_children_order
.push_back( i
);
995 d_children
[i
].determineVariableOrder( qi
, bvars
);
1001 void MatchGen::reset_round( QuantConflictFind
* p
) {
1003 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1004 d_children
[i
].reset_round( p
);
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
);
1009 if( d_type
==typ_ground
){
1010 int e
= p
->evaluate( d_n
);
1012 d_ground_eval
[0] = p
->d_true
;
1014 d_ground_eval
[0] = p
->d_false
;
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
] );
1023 d_qni_bound_cons
.clear();
1024 d_qni_bound_cons_var
.clear();
1025 d_qni_bound
.clear();
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
;
1035 d_qni_bound
.clear();
1036 d_child_counter
= -1;
1039 //set up processing matches
1040 if( d_type
==typ_invalid
){
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;
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
) );
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;
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;
1062 if( d_child_counter
==0 ){
1063 d_qn
.push_back( NULL
);
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
);
1071 d_qn
.push_back( qni
);
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
;
1082 d_qn
.push_back( NULL
);
1083 }else if( d_type
==typ_pred
|| d_type
==typ_eq
){
1084 //add initial constraint
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
);
1094 for( unsigned i
=0; i
<2; i
++ ){
1096 std::map
< int, TNode
>::iterator it
= d_qni_gterm_rep
.find( i
);
1097 if( it
!=d_qni_gterm_rep
.end() ){
1102 nn
[i
] = qi
->getCurrentValue( nc
);
1103 vn
[i
] = qi
->getCurrentRepVar( qi
->getVarNum( nn
[i
] ) );
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
1112 success
= p
->areMatchEqual( nn
[0], nn
[1] );
1114 if( p
->d_effort
==QuantConflictFind::effort_conflict
){
1115 success
= p
->areDisequal( nn
[0], nn
[1] );
1117 success
= p
->areMatchDisequal( nn
[0], nn
[1] );
1121 //otherwise, add a constraint to a variable
1122 if( vn
[1]!=-1 && vn
[0]==-1 ){
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 );
1134 //if successful and non-redundant, store that we need to cleanup this
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
];
1142 d_qni_bound_cons
[vn
[0]] = nn
[1];
1143 d_qni_bound_cons_var
[vn
[0]] = vn
[1];
1146 //if successful, we will bind values to variables
1148 d_qn
.push_back( NULL
);
1151 if( d_children
.empty() ){
1153 d_qn
.push_back( NULL
);
1155 if( d_tgt
&& d_n
.getKind()==FORALL
){
1158 //reset the first child to d_tgt
1159 d_child_counter
= 0;
1160 getChild( d_child_counter
)->reset( p
, d_tgt
, qi
);
1166 Debug("qcf-match") << " reset: Finished reset for " << d_n
<< ", success = " << ( !d_qn
.empty() || d_child_counter
!=-1 ) << std::endl
;
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;
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;
1185 bool doReset
= false;
1186 bool doFail
= false;
1188 if( doMatching( p
, qi
) ){
1189 Debug("qcf-match-debug") << " - Matching succeeded" << std::endl
;
1191 d_binding_it
= d_qni_bound
.begin();
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
){
1206 Debug("qcf-match-debug") << " - Matching failed" << std::endl
;
1214 //also need to create match for each variable we bound
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
;
1220 while( ( success
&& d_binding_it
!=d_qni_bound
.end() ) || doFail
){
1221 std::map
< int, MatchGen
* >::iterator itm
;
1223 Debug("qcf-match-debug") << " check variable " << d_binding_it
->second
<< std::endl
;
1224 itm
= qi
->d_var_mg
.find( d_binding_it
->second
);
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
;
1229 itm
->second
->reset( p
, true, qi
);
1231 if( doFail
|| !itm
->second
->getNextMatch( p
, qi
) ){
1233 if( d_binding_it
==d_qni_bound
.begin() ){
1234 Debug("qcf-match-debug") << " failed." << std::endl
;
1238 Debug("qcf-match-debug") << " decrement..." << std::endl
;
1240 }while( success
&& ( d_binding_it
->first
==0 || qi
->d_var_mg
.find( d_binding_it
->second
)==qi
->d_var_mg
.end() ) );
1244 Debug("qcf-match-debug") << " increment..." << std::endl
;
1249 Debug("qcf-match-debug") << " skip..." << d_binding_it
->second
<< std::endl
;
1258 if( d_binding_it
==d_qni_bound
.begin() ){
1263 }while( !terminate
);
1264 //if not successful, clean up the variables you bound
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 );
1277 d_qni_bound_cons
.clear();
1278 d_qni_bound_cons_var
.clear();
1279 d_qni_bound
.clear();
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();
1288 d_qni_bound
.clear();
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();
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 ) ){
1304 d_qni_bound[0] = d_qni_var_num[0];
1309 Debug("qcf-match") << " ...finished matching for " << d_n
<< ", success = " << success
<< std::endl
;
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 ){
1317 d_child_counter
= -1;
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) ){
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
);
1334 //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
1335 // d_child_counter--;
1341 //one child must match
1342 if( !getChild( d_child_counter
)->getNextMatch( p
, qi
) ){
1343 if( d_child_counter
<(int)(getNumChildren()-1) ){
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
);
1348 d_child_counter
= -1;
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
) ){
1359 getChild( 1 )->reset( p
, d_child_counter
==1, qi
);
1361 if( d_child_counter
==0 ){
1362 d_child_counter
= 2;
1363 getChild( 0 )->reset( p
, !d_tgt
, qi
);
1365 d_child_counter
= -1;
1369 if( d_child_counter
>=0 && d_child_counter
%2==1 ){
1370 if( getChild( 1 )->getNextMatch( p
, qi
) ){
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
) ){
1381 getChild( d_child_counter
==5 ? 2 : (d_tgt
==(d_child_counter
==1) ? 1 : 2) )->reset( p
, d_tgt
, qi
);
1383 if( d_child_counter
==4 || ( d_type
==typ_ite_var
&& d_child_counter
==2 ) ){
1384 d_child_counter
= -1;
1386 d_child_counter
+=2;
1387 getChild( d_child_counter
==2 ? 0 : 1 )->reset( p
, d_child_counter
==2 ? !d_tgt
: d_tgt
, qi
);
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
) ){
1399 }else if( d_n
.getKind()==FORALL
){
1400 if( getChild( d_child_counter
)->getNextMatch( p
, qi
) ){
1403 d_child_counter
= -1;
1408 Debug("qcf-match") << " ...finished construct match for " << d_n
<< ", success = " << success
<< std::endl
;
1412 Debug("qcf-match") << " ...already finished for " << d_n
<< std::endl
;
1416 bool MatchGen::getExplanation( QuantConflictFind
* p
, QuantInfo
* qi
, std::vector
< Node
>& exp
) {
1417 if( d_type
==typ_eq
){
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
);
1423 Node eq
= n
[0].eqNode( n
[1] );
1427 exp
.push_back( eq
);
1428 Trace("qcf-explain") << "Explanation for " << d_n
<< " (tgt=" << d_tgt_orig
<< ") is " << eq
<< ", set = " << d_wasSet
<< std::endl
;
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
);
1437 Trace("qcf-explain") << "Explanation for " << d_n
<< " (tgt=" << d_tgt_orig
<< ") is " << n
<< ", set = " << d_wasSet
<< std::endl
;
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
) ){
1449 return getChild( d_child_counter
)->getExplanation( p
, qi
, exp
);
1451 }else if( d_n
.getKind()==IFF
){
1452 for( unsigned i
=0; i
<2; i
++ ){
1453 if( !getChild( i
)->getExplanation( p
, qi
, exp
) ){
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 ) ) );
1463 if( !getChild( i
)->getExplanation( p
, qi
, exp
) ){
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
);
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
);
1494 bool MatchGen::doMatching( QuantConflictFind
* p
, QuantInfo
* qi
) {
1495 if( !d_qn
.empty() ){
1496 if( d_qn
[0]==NULL
){
1500 Assert( d_type
==typ_var
);
1501 Assert( d_qni_size
>0 );
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();
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
;
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
);
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
);
1533 Debug("qcf-match") << " Binding variable, currently fail." << std::endl
;
1534 invalidMatch
= true;
1537 Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl
;
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() );
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
);
1558 Debug("qcf-match-debug") << " Failed to match" << std::endl
;
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() ){
1570 if( d_qni
[index
]!=d_qn
[index
]->d_data
.end() ){
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
);
1578 Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl
;
1579 invalidMatch
= true;
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
;
1587 //TODO : if it equal to something else, also try that
1589 //if not incrementing, move to next
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
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];
1617 return !d_qn
.empty();
1620 void MatchGen::debugPrintType( const char * c
, short typ
, bool isTrace
) {
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;
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;
1646 void MatchGen::setInvalid() {
1647 d_type
= typ_invalid
;
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
);
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() );
1661 Node
MatchGen::getOperator( QuantConflictFind
* p
, Node n
) {
1662 if( isHandledUfTerm( n
) ){
1663 return p
->getQuantifiersEngine()->getTermDatabase()->getOperator( n
);
1665 return Node::null();
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
){
1674 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1675 if( !isHandled( n
[i
] ) ){
1684 QuantConflictFind::QuantConflictFind( QuantifiersEngine
* qe
, context::Context
* c
) :
1685 QuantifiersModule( qe
),
1687 d_conflict( c
, false ),
1690 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
1691 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
1694 Node
QuantConflictFind::mkEqNode( Node a
, Node b
) {
1695 if( a
.getType().isBoolean() ){
1696 return a
.iffNode( b
);
1698 return a
.eqNode( b
);
1702 //-------------------------------------------------- registration
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] );
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
;
1729 Trace("qcf-qregister") << "Done registering quantifier." << std::endl
;
1733 int QuantConflictFind::evaluate( Node n
, bool pref
, bool hasPref
) {
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
) ){
1741 }else if( areDisequal( n1
, n2
) ){
1744 //else if( d_effort>QuantConflictFind::effort_conflict ){
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
) ){
1752 }else if( areEqual( nn
, d_false
) ){
1755 //else if( d_effort>QuantConflictFind::effort_conflict ){
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] );
1769 }else if( cevc
[i
]==0 ){
1774 if( ret
==0 && cevc
[0]!=0 && cevc
[0]==cevc
[1] ){
1777 }else if( n
.getKind()==IFF
){
1778 int cev1
= evaluate( n
[0] );
1780 int cev2
= evaluate( n
[1] );
1782 ret
= cev1
==cev2
? 1 : -1;
1788 if( n
.getKind()==OR
){
1790 }else if( n
.getKind()==AND
){
1794 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1795 int cev
= evaluate( n
[i
] );
1803 if( ret
==0 && !isUnk
){
1807 Debug("qcf-eval") << "Evaluate " << n
<< " to " << ret
<< std::endl
;
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
){
1823 bool QuantConflictFind::areMatchEqual( TNode n1
, TNode n2
) {
1824 //if( d_effort==QuantConflictFind::effort_mc ){
1825 // return n1==n2 || !areDisequal( n1, n2 );
1831 bool QuantConflictFind::areMatchDisequal( TNode n1
, TNode n2
) {
1832 //if( d_effort==QuantConflictFind::effort_conflict ){
1833 // return areDisequal( n1, n2 );
1839 //-------------------------------------------------- handling assertions / eqc
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 );
1854 eq::EqualityEngine
* QuantConflictFind::getEqualityEngine() {
1855 //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
1856 return d_quantEngine
->getTheoryEngine()->getMasterEqualityEngine();
1858 bool QuantConflictFind::areEqual( Node n1
, Node n2
) {
1859 return getEqualityEngine()->hasTerm( n1
) && getEqualityEngine()->hasTerm( n2
) && getEqualityEngine()->areEqual( n1
,n2
);
1861 bool QuantConflictFind::areDisequal( Node n1
, Node n2
) {
1862 return n1
!=n2
&& getEqualityEngine()->hasTerm( n1
) && getEqualityEngine()->hasTerm( n2
) && getEqualityEngine()->areDisequal( n1
,n2
, false );
1864 Node
QuantConflictFind::getRepresentative( Node n
) {
1865 if( getEqualityEngine()->hasTerm( n
) ){
1866 return getEqualityEngine()->getRepresentative( n
);
1871 TermDb
* QuantConflictFind::getTermDatabase() {
1872 return d_quantEngine
->getTermDatabase();
1875 Node
QuantConflictFind::evaluateTerm( Node n
) {
1876 if( MatchGen::isHandledUfTerm( n
) ){
1877 Node f
= MatchGen::getOperator( this, n
);
1879 if( getEqualityEngine()->hasTerm( n
) ){
1880 nn
= getTermDatabase()->existsTerm( f
, n
);
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
);
1887 nn
= getTermDatabase()->d_func_map_trie
[f
].existsTerm( args
);
1890 Debug("qcf-eval") << "GT: Term " << nn
<< " for " << n
<< " hasTerm = " << getEqualityEngine()->hasTerm( n
) << std::endl
;
1891 return getRepresentative( nn
);
1893 Debug("qcf-eval") << "GT: No term for " << n
<< " hasTerm = " << getEqualityEngine()->hasTerm( n
) << std::endl
;
1896 }else if( n
.getKind()==ITE
){
1897 int v
= evaluate( n
[0], false, false );
1899 return evaluateTerm( n
[1] );
1901 return evaluateTerm( n
[2] );
1904 return getRepresentative( n
);
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;
1914 void QuantConflictFind::merge( Node a
, Node b
) {
1918 /** assert disequal */
1919 void QuantConflictFind::assertDisequal( Node a
, Node b
) {
1923 //-------------------------------------------------- check function
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
;
1936 return performCheck
;
1939 void QuantConflictFind::reset_round( Theory::Effort level
) {
1940 d_needs_computeRelEqr
= true;
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
;
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
;
1954 int addedLemmas
= 0;
1955 ++(d_statistics
.d_inst_rounds
);
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
;
1963 computeRelevantEqr();
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;
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
);
1979 d_quant_order
.clear();
1980 d_quant_order
.insert( d_quant_order
.begin(), qorder
.begin(), qorder
.end() );
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
);
1989 if( Trace
.isOn("qcf-debug") ){
1990 Trace("qcf-debug") << std::endl
;
1991 debugPrint("qcf-debug");
1992 Trace("qcf-debug") << std::endl
;
1994 short end_e
= getMaxQcfEffort();
1995 for( short e
= effort_conflict
; e
<=end_e
; e
++ ){
1997 Trace("qcf-check") << "Checking quantified formulas at effort " << e
<< "..." << std::endl
;
1998 for( unsigned j
=0; j
<qorder
.size(); j
++ ){
2000 QuantInfo
* qi
= &d_qinfo
[q
];
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
;
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
);
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
;
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
);
2041 }else if( e
==effort_prop_eq
){
2042 ++(d_statistics
.d_prop_inst
);
2045 Trace("qcf-check") << " ... Failed to add instantiation" << std::endl
;
2050 qi
->revertMatch( assigned
);
2051 d_tempCache
.clear();
2053 Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl
;
2056 Trace("qcf-check") << " ... Spurious instantiation (match is inconsistent)" << std::endl
;
2064 if( addedLemmas
>0 ){
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
;
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
;
2081 Trace("qcf-check2") << "QCF : finished check : " << level
<< std::endl
;
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();
2093 d_model_basis
.clear();
2094 //d_arg_reps.clear();
2096 //if( Trace.isOn("qcf-opt") ){
2097 // clSet = double(clock())/double(CLOCKS_PER_SEC);
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() ){
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
;
2120 Node mbr
= getRepresentative( mb
);
2122 d_eqcs
[rtn
].push_back( mbr
);
2124 d_eqcs
[rtn
].push_back( r
);
2125 d_model_basis
[rtn
] = mb
;
2127 itt
->second
.push_back( r
);
2130 d_eqcs
[rtn
].push_back( r
);
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;
2147 //-------------------------------------------------- debugging
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() ){
2156 //if( !n.getType().isInteger() ){
2157 Trace(c
) << " - " << n
<< " : {";
2158 eq::EqClassIterator eqc_i
= eq::EqClassIterator( n
, getEqualityEngine() );
2160 while( !eqc_i
.isFinished() ){
2162 if( nn
.getKind()!=EQUAL
&& nn
!=n
){
2163 Trace(c
) << (pr
? "," : "" ) << " " << nn
;
2168 Trace(c
) << (pr
? " " : "" ) << "}" << std::endl
;
2170 EqcInfo * eqcn = getEqcInfo( n, false );
2172 Trace(c) << " DEQ : {";
2174 for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
2176 Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
2180 Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2188 void QuantConflictFind::debugPrintQuant( const char * c
, Node q
) {
2189 Trace(c
) << "Q" << d_quant_id
[q
];
2192 void QuantConflictFind::debugPrintQuantBody( const char * c
, Node q
, Node n
, bool doVarNum
) {
2193 if( n
.getNumChildren()==0 ){
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
];
2199 if( n
.getKind()==APPLY_UF
){
2200 Trace(c
) << n
.getOperator();
2202 Trace(c
) << n
.getKind();
2204 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2206 debugPrintQuantBody( c
, q
, n
[i
] );
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)
2218 StatisticsRegistry::registerStat(&d_inst_rounds
);
2219 StatisticsRegistry::registerStat(&d_conflict_inst
);
2220 StatisticsRegistry::registerStat(&d_prop_inst
);
2221 StatisticsRegistry::registerStat(&d_entailment_checks
);
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
);
2231 TNode
QuantConflictFind::getZero( Kind k
) {
2232 std::map
< Kind
, Node
>::iterator it
= d_zero
.find( k
);
2233 if( it
==d_zero
.end() ){
2236 nn
= NodeManager::currentNM()->mkConst( Rational(0) );