c796333b3a1347f918c365fbd2354cc78de700d7
1 /********************* */
2 /*! \file quant_conflict_find.cpp
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
12 ** \brief quant conflict find class
16 #include "theory/quantifiers/quant_conflict_find.h"
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"
28 using namespace CVC4::kind
;
33 namespace quantifiers
{
35 QuantInfo::QuantInfo()
39 QuantInfo::~QuantInfo() {
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
;
50 void QuantInfo::initialize( QuantConflictFind
* p
, Node q
, Node qn
) {
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() );
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() );
64 registerNode( qn
, true, true );
67 Trace("qcf-qregister") << "- Make match gen structure..." << std::endl
;
68 d_mg
= new MatchGen( this, qn
);
70 if( d_mg
->isValid() ){
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;
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
){
85 if( !MatchGen::isHandledUfTerm( d_vars
[j
] ) && d_vars
[j
].getKind()!=ITE
){
87 d_tsym_vars
.push_back( j
);
89 if( !is_tsym
|| options::qcfTConstraint() ){
90 d_var_mg
[j
] = new MatchGen( this, d_vars
[j
], true );
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
;
97 std::vector
< int > bvars
;
98 d_var_mg
[j
]->determineVariableOrder( this, bvars
);
102 if( d_mg
->isValid() ){
103 std::vector
< int > bvars
;
104 d_mg
->determineVariableOrder( this, bvars
);
108 Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl
;
110 Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg
->isValid() ? "VALID " : "INVALID" ) << " : " << q
<< std::endl
;
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] );
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
++ ){
126 TNode f
= p
->getTermDatabase()->getMatchOperator( v
);
128 Trace("qcf-opt") << "Record variable argument positions in " << v
<< ", op=" << f
<< "..." << std::endl
;
129 for( unsigned k
=0; k
<v
.getNumChildren(); 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
);
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() ){
150 if( d_var_num
.find( n
)!=d_var_num
.end() ){
151 Assert( std::find( vars
.begin(), vars
.end(), n
)==vars
.end() );
153 }else if( MatchGen::isHandledBoolConnective( n
) ){
154 Assert( n
.getKind()!=IMPLIES
);
155 QuantPhaseReq::getEntailPolarity( n
, 0, true, pol
, rec
, newPol
);
157 Trace("qcf-opt-debug") << "getPropagateVars " << n
<< ", pol = " << pol
<< ", rec = " << rec
<< std::endl
;
159 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
160 getPropagateVars( vars
, n
[i
], pol
, visited
);
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 );
171 if( !MatchGen::isHandledBoolConnective( n
) ){
172 if( n
.hasBoundVar() ){
174 if( n
.getKind()==EQUAL
){
175 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
176 flatten( n
[i
], beneathQuant
);
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
);
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
);
193 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
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
);
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;
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 );
223 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
224 flatten( n
[i
], beneathQuant
);
228 Trace("qcf-qregister-debug2") << "...already processed" << std::endl
;
231 Trace("qcf-qregister-debug2") << "...is ground." << std::endl
;
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();
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
];
250 rr
= p
->getRepresentative( rr
);
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
;
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
);
269 //now, reset for matching
270 d_mg
->reset( p
, false, this );
273 int QuantInfo::getCurrentRepVar( int v
) {
274 if( v
!=-1 && !d_match
[v
].isNull() ){
275 int vn
= getVarNum( d_match
[v
] );
277 //int vr = getCurrentRepVar( vn );
278 //d_match[v] = d_vars[vr];
280 return getCurrentRepVar( vn
);
286 TNode
QuantInfo::getCurrentValue( TNode n
) {
287 int v
= getVarNum( n
);
291 if( d_match
[v
].isNull() ){
294 Assert( getVarNum( d_match
[v
] )!=v
);
295 return getCurrentValue( d_match
[v
] );
300 TNode
QuantInfo::getCurrentExpValue( TNode n
) {
301 int v
= getVarNum( n
);
305 if( d_match
[v
].isNull() ){
308 Assert( getVarNum( d_match
[v
] )!=v
);
309 if( d_match_term
[v
].isNull() ){
310 return getCurrentValue( d_match
[v
] );
312 return d_match_term
[v
];
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
;
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
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 );
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
) ) );
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 );
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
){
371 remDeq
.push_back( it
->first
);
374 for( unsigned i
=0; i
<remDeq
.size(); i
++ ){
375 d_curr_var_deq
[vn
].erase( remDeq
[i
] );
380 d_match
[v
] = TNode::null();
383 //std::map< int, TNode >::iterator itm = d_match.find( v );
384 bool isGroundRep
= false;
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() ){
393 Assert( !isVar( d_match
[vn
] ) );
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
);
402 if( d_curr_var_deq
[vn
].find( dv
)==d_curr_var_deq
[vn
].end() ){
403 d_curr_var_deq
[vn
][dv
] = v
;
406 if( !p
->areMatchDisequal( d_match
[vn
], dv
) ){
407 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
414 n
= getCurrentValue( n
);
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 );
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;
428 Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl
;
429 if( d_match
[v
].isNull() ){
430 //isGroundRep = true; ??
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;
437 if( setMatch( p
, v
, n
, isGroundRep
) ){
438 Debug("qcf-match-debug") << " -> success" << std::endl
;
441 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
446 Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl
;
451 Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl
;
455 Assert( d_curr_var_deq
[v
].find( n
)!=d_curr_var_deq
[v
].end() );
456 d_curr_var_deq
[v
].erase( n
);
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
;
469 d_curr_var_deq
[v
][n
] = v
;
470 Debug("qcf-match-debug") << " -> success" << std::endl
;
473 Debug("qcf-match-debug") << " -> redundant disequality" << std::endl
;
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() ){
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
){
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
){
503 bool QuantInfo::setMatch( QuantConflictFind
* p
, int v
, TNode n
, bool isGroundRep
) {
504 if( getCurrentCanBeEqual( p
, v
, n
) ){
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
;
520 Debug("qcf-match-debug") << "-- bind : " << v
<< " -> " << n
<< ", checked " << d_curr_var_deq
[v
].size() << " disequalities" << std::endl
;
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
) ){
540 bool QuantInfo::isTConstraintSpurious( QuantConflictFind
* p
, std::vector
< Node
>& terms
) {
541 if( !d_tconstraints
.empty() ){
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
) ){
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
;
561 }else if( rew
!=p
->d_true
){
562 //if checking for conflicts, we must be sure that the (negation of) constraint is (not) entailed
564 rew
= Rewriter::rewrite( rew
.negate() );
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
;
572 Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew
<< "." << std::endl
;
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;
585 Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
591 Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
596 Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl
;
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)
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
] );
615 if( v
==d_vars
[index
] ){
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
] );
625 TNode vv
= getCurrentValue( d_vars
[index
][j
] );
626 if( vv
==d_vars
[index
][j
] ){
627 //we will assign this
629 Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn
<< std::endl
;
631 if( p
->d_effort
!=QuantConflictFind::effort_conflict
){
635 Node z
= p
->getZero( k
);
637 Trace("qcf-tconstraint-debug") << "...set " << d_vars
[vn
] << " = " << z
<< std::endl
;
638 assigned
.push_back( vn
);
639 if( !setMatch( p
, vn
, z
, false ) ){
646 Trace("qcf-tconstraint-debug") << "...sum value " << vv
<< std::endl
;
647 children
.push_back( vv
);
650 Trace("qcf-tconstraint-debug") << "...sum " << d_vars
[index
][j
] << std::endl
;
651 children
.push_back( d_vars
[index
][j
] );
657 if( children
.empty() ){
658 lhs
= p
->getZero( k
);
659 }else if( children
.size()==1 ){
662 lhs
= NodeManager::currentNM()->mkNode( k
, children
);
665 if( v
==d_vars
[index
] ){
668 if( p
->d_effort
==QuantConflictFind::effort_conflict
){
670 if( d_vars
[index
].getKind()==PLUS
){
674 sum
= NodeManager::currentNM()->mkNode( kn
, v
, lhs
);
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 ) ){
684 p
->d_tempCache
.push_back( sum
);
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
) ){
693 p
->d_tempCache
.push_back( sum
);
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
);
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() );
721 d_una_eqc_count
.clear();
726 if( !d_unassigned
.empty() && ( success
|| doContinue
) ){
727 Trace("qcf-check") << "Assign to unassigned (" << d_unassigned
.size() << ")..." << std::endl
;
730 Trace("qcf-check-unassign") << "Failure, try again..." << std::endl
;
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 );
741 d_var_mg
[ d_unassigned
[d_una_index
] ]->reset( p
, true, this );
742 d_una_eqc_count
.push_back( 0 );
745 d_una_eqc_count
.push_back( 0 );
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
;
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
;
759 Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index
<< std::endl
;
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
;
772 Trace("qcf-check-unassign") << "Failed match " << d_una_index
<< std::endl
;
777 Trace("qcf-check-unassign") << "No more matches " << d_una_index
<< std::endl
;
781 if( doFail
|| failed
){
784 d_una_eqc_count
.pop_back();
789 }while( d_una_index
>=0 && d_una_eqc_count
[d_una_index
]==-1 );
793 success
= d_una_index
>=0;
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
;
804 }while( success
&& isMatchSpurious( p
) );
805 Trace("qcf-check") << "done assigning." << std::endl
;
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
;
816 for( unsigned i
=0; i
<assigned
.size(); i
++ ){
817 d_match
[ assigned
[i
] ] = TNode::null();
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
);
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
];
833 cv
= d_match
[repVar
];
835 Debug("qcf-check-inst") << "INST : " << i
<< " -> " << cv
<< ", from " << d_match
[i
] << std::endl
;
836 terms
.push_back( cv
);
840 void QuantInfo::revertMatch( std::vector
< int >& assigned
) {
841 for( unsigned i
=0; i
<assigned
.size(); i
++ ){
842 d_match
[ assigned
[i
] ] = TNode::null();
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
];
852 Trace(c
) << "(unassigned) ";
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
<< " ";
861 if( !d_match_term
[i
].isNull() && d_match_term
[i
]!=d_match
[i
] ){
862 Trace(c
) << ", EXP : " << d_match_term
[i
];
864 Trace(c
) << std::endl
;
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
;
881 d_type( typ_invalid
),
886 MatchGen::MatchGen( QuantInfo
* qi
, Node n
, bool isVar
)
896 Trace("qcf-qregister-debug") << "Make match gen for " << n
<< ", isVar = " << isVar
<< std::endl
;
897 std::vector
< Node
> qni_apps
;
900 Assert( qi
->d_var_num
.find( n
)!=qi
->d_var_num
.end() );
901 if( n
.getKind()==ITE
){
903 d_type = typ_ite_var;
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() ){
920 d_type
= typ_invalid
;
923 d_type
= isHandledUfTerm( n
) ? typ_var
: typ_tsym
;
924 d_qni_var_num
[0] = qi
->getVarNum( n
);
928 //Node f = getMatchOperator( n );
929 for( unsigned j
=0; j
<d_n
.getNumChildren(); 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 );
938 Trace("qcf-qregister-debug") << " is gterm " << nn
<< std::endl
;
939 d_qni_gterm
[d_qni_size
] = nn
;
945 if( n
.hasBoundVar() ){
948 if( d_n
.getKind()==NOT
){
950 d_type_not
= !d_type_not
;
953 if( isHandledBoolConnective( d_n
) ){
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() ){
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 );
981 d_children.pop_back();
986 d_type
= typ_invalid
;
988 if( isHandledUfTerm( d_n
) ){
989 Assert( qi
->isVar( d_n
) );
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
;
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
]];
1005 d_qni_gterm
[i
] = d_n
[i
];
1008 d_type
= d_n
.getKind()==EQUAL
? typ_eq
: typ_tconstraint
;
1009 Trace("qcf-tconstraint") << "T-Constraint : " << d_n
<< std::endl
;
1013 //we will just evaluate
1015 d_type
= typ_ground
;
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 );
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
1027 //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
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() );
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
);
1044 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1045 collectBoundVar( qi
, n
[i
], cbvars
);
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 );
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() ){
1069 bvars
.push_back( v
);
1077 //children that bind the least number of unbound variables go first
1080 int min_score_index
= -1;
1081 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1083 int score
= vu_count
[i
];
1084 if( min_score
==-1 || score
<min_score
){
1086 min_score_index
= i
;
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 );
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
];
1110 bvars
.push_back( v
);
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
;
1117 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1118 d_children_order
.push_back( i
);
1119 d_children
[i
].determineVariableOrder( qi
, bvars
);
1125 void MatchGen::reset_round( QuantConflictFind
* p
) {
1127 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1128 d_children
[i
].reset_round( p
);
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
);
1133 if( d_type
==typ_ground
){
1134 //int e = p->evaluate( d_n );
1136 // d_ground_eval[0] = p->d_true;
1137 //}else if( e==-1 ){
1138 // d_ground_eval[0] = p->d_false;
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
;
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
] );
1151 d_ground_eval
[i
] = d_n
[i
];
1153 d_ground_eval
[i
] = t
;
1158 d_qni_bound_cons
.clear();
1159 d_qni_bound_cons_var
.clear();
1160 d_qni_bound
.clear();
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
;
1170 d_qni_bound
.clear();
1171 d_child_counter
= -1;
1174 //set up processing matches
1175 if( d_type
==typ_invalid
){
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;
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
) );
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;
1192 if( p
->getTermDatabase()->isEntailed( n
, d_tgt
) ){
1193 d_child_counter
= 0;
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;
1201 if( d_child_counter
==0 ){
1202 d_qn
.push_back( NULL
);
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
);
1210 d_qn
.push_back( qni
);
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
;
1221 d_qn
.push_back( NULL
);
1222 }else if( d_type
==typ_pred
|| d_type
==typ_eq
){
1223 //add initial constraint
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
);
1233 for( unsigned i
=0; i
<2; i
++ ){
1235 std::map
< int, TNode
>::iterator it
= d_qni_gterm_rep
.find( i
);
1236 if( it
!=d_qni_gterm_rep
.end() ){
1241 nn
[i
] = qi
->getCurrentValue( nc
);
1242 vn
[i
] = qi
->getCurrentRepVar( qi
->getVarNum( nn
[i
] ) );
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
1251 success
= p
->areMatchEqual( nn
[0], nn
[1] );
1253 if( p
->d_effort
==QuantConflictFind::effort_conflict
){
1254 success
= p
->areDisequal( nn
[0], nn
[1] );
1256 success
= p
->areMatchDisequal( nn
[0], nn
[1] );
1260 //otherwise, add a constraint to a variable
1261 if( vn
[1]!=-1 && vn
[0]==-1 ){
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 );
1273 //if successful and non-redundant, store that we need to cleanup this
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
];
1281 d_qni_bound_cons
[vn
[0]] = nn
[1];
1282 d_qni_bound_cons_var
[vn
[0]] = vn
[1];
1285 //if successful, we will bind values to variables
1287 d_qn
.push_back( NULL
);
1290 if( d_children
.empty() ){
1292 d_qn
.push_back( NULL
);
1294 if( d_tgt
&& d_n
.getKind()==FORALL
){
1297 //reset the first child to d_tgt
1298 d_child_counter
= 0;
1299 getChild( d_child_counter
)->reset( p
, d_tgt
, qi
);
1305 Debug("qcf-match") << " reset: Finished reset for " << d_n
<< ", success = " << ( !d_qn
.empty() || d_child_counter
!=-1 ) << std::endl
;
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;
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;
1324 bool doReset
= false;
1325 bool doFail
= false;
1327 if( doMatching( p
, qi
) ){
1328 Debug("qcf-match-debug") << " - Matching succeeded" << std::endl
;
1330 d_binding_it
= d_qni_bound
.begin();
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
){
1345 Debug("qcf-match-debug") << " - Matching failed" << std::endl
;
1353 //also need to create match for each variable we bound
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
;
1359 while( ( success
&& d_binding_it
!=d_qni_bound
.end() ) || doFail
){
1360 QuantInfo::VarMgMap::const_iterator itm
;
1362 Debug("qcf-match-debug") << " check variable " << d_binding_it
->second
<< std::endl
;
1363 itm
= qi
->var_mg_find( d_binding_it
->second
);
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
;
1368 itm
->second
->reset( p
, true, qi
);
1370 if( doFail
|| !itm
->second
->getNextMatch( p
, qi
) ){
1372 if( d_binding_it
==d_qni_bound
.begin() ){
1373 Debug("qcf-match-debug") << " failed." << std::endl
;
1377 Debug("qcf-match-debug") << " decrement..." << std::endl
;
1380 ( d_binding_it
->first
==0 ||
1381 (!qi
->containsVarMg(d_binding_it
->second
))));
1385 Debug("qcf-match-debug") << " increment..." << std::endl
;
1390 Debug("qcf-match-debug") << " skip..." << d_binding_it
->second
<< std::endl
;
1399 if( d_binding_it
==d_qni_bound
.begin() ){
1404 }while( !terminate
);
1405 //if not successful, clean up the variables you bound
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 );
1418 d_qni_bound_cons
.clear();
1419 d_qni_bound_cons_var
.clear();
1420 d_qni_bound
.clear();
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();
1429 d_qni_bound
.clear();
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();
1439 Debug("qcf-match") << " ...finished matching for " << d_n
<< ", success = " << success
<< std::endl
;
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 ){
1447 d_child_counter
= -1;
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) ){
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
);
1464 //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
1465 // d_child_counter--;
1471 //one child must match
1472 if( !getChild( d_child_counter
)->getNextMatch( p
, qi
) ){
1473 if( d_child_counter
<(int)(getNumChildren()-1) ){
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
);
1478 d_child_counter
= -1;
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
) ){
1489 getChild( 1 )->reset( p
, d_child_counter
==1, qi
);
1491 if( d_child_counter
==0 ){
1492 d_child_counter
= 2;
1493 getChild( 0 )->reset( p
, !d_tgt
, qi
);
1495 d_child_counter
= -1;
1499 if( d_child_counter
>=0 && d_child_counter
%2==1 ){
1500 if( getChild( 1 )->getNextMatch( p
, qi
) ){
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
) ){
1511 getChild( d_child_counter
==5 ? 2 : (d_tgt
==(d_child_counter
==1) ? 1 : 2) )->reset( p
, d_tgt
, qi
);
1513 if( d_child_counter
==4 || ( d_type
==typ_ite_var
&& d_child_counter
==2 ) ){
1514 d_child_counter
= -1;
1516 d_child_counter
+=2;
1517 getChild( d_child_counter
==2 ? 0 : 1 )->reset( p
, d_child_counter
==2 ? !d_tgt
: d_tgt
, qi
);
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
) ){
1529 }else if( d_n
.getKind()==FORALL
){
1530 if( getChild( d_child_counter
)->getNextMatch( p
, qi
) ){
1533 d_child_counter
= -1;
1538 Debug("qcf-match") << " ...finished construct match for " << d_n
<< ", success = " << success
<< std::endl
;
1542 Debug("qcf-match") << " ...already finished for " << d_n
<< std::endl
;
1546 bool MatchGen::getExplanation( QuantConflictFind
* p
, QuantInfo
* qi
, std::vector
< Node
>& exp
) {
1547 if( d_type
==typ_eq
){
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
);
1553 Node eq
= n
[0].eqNode( n
[1] );
1557 exp
.push_back( eq
);
1558 Trace("qcf-explain") << "Explanation for " << d_n
<< " (tgt=" << d_tgt_orig
<< ") is " << eq
<< ", set = " << d_wasSet
<< std::endl
;
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
);
1567 Trace("qcf-explain") << "Explanation for " << d_n
<< " (tgt=" << d_tgt_orig
<< ") is " << n
<< ", set = " << d_wasSet
<< std::endl
;
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
) ){
1579 return getChild( d_child_counter
)->getExplanation( p
, qi
, exp
);
1581 }else if( d_n
.getKind()==IFF
){
1582 for( unsigned i
=0; i
<2; i
++ ){
1583 if( !getChild( i
)->getExplanation( p
, qi
, exp
) ){
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 ) ) );
1593 if( !getChild( i
)->getExplanation( p
, qi
, exp
) ){
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
);
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
);
1624 bool MatchGen::doMatching( QuantConflictFind
* p
, QuantInfo
* qi
) {
1625 if( !d_qn
.empty() ){
1626 if( d_qn
[0]==NULL
){
1630 Assert( d_type
==typ_var
);
1631 Assert( d_qni_size
>0 );
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();
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
;
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
);
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
);
1663 Debug("qcf-match") << " Binding variable, currently fail." << std::endl
;
1664 invalidMatch
= true;
1667 Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl
;
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() );
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
);
1688 Debug("qcf-match-debug") << " Failed to match" << std::endl
;
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() ){
1700 if( d_qni
[index
]!=d_qn
[index
]->d_data
.end() ){
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
);
1708 Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl
;
1709 invalidMatch
= true;
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
;
1717 //TODO : if it equal to something else, also try that
1719 //if not incrementing, move to next
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
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];
1747 return !d_qn
.empty();
1750 void MatchGen::debugPrintType( const char * c
, short typ
, bool isTrace
) {
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;
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;
1776 void MatchGen::setInvalid() {
1777 d_type
= typ_invalid
;
1781 bool MatchGen::isHandledBoolConnective( TNode n
) {
1782 return n
.getType().isBoolean() && TermDb::isBoolConnective( n
.getKind() );
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() );
1793 Node
MatchGen::getMatchOperator( QuantConflictFind
* p
, Node n
) {
1794 if( isHandledUfTerm( n
) ){
1795 return p
->getTermDatabase()->getMatchOperator( n
);
1797 return Node::null();
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
){
1806 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1807 if( !isHandled( n
[i
] ) ){
1816 QuantConflictFind::QuantConflictFind( QuantifiersEngine
* qe
, context::Context
* c
) :
1817 QuantifiersModule( qe
),
1818 d_conflict( c
, false ) {
1820 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
1821 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
1824 Node
QuantConflictFind::mkEqNode( Node a
, Node b
) {
1825 if( a
.getType().isBoolean() ){
1826 return a
.iffNode( b
);
1828 return a
.eqNode( b
);
1832 //-------------------------------------------------- registration
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] );
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
;
1859 Trace("qcf-qregister") << "Done registering quantifier." << std::endl
;
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
;
1873 bool QuantConflictFind::areMatchEqual( TNode n1
, TNode n2
) {
1874 //if( d_effort==QuantConflictFind::effort_mc ){
1875 // return n1==n2 || !areDisequal( n1, n2 );
1881 bool QuantConflictFind::areMatchDisequal( TNode n1
, TNode n2
) {
1882 //if( d_effort==QuantConflictFind::effort_conflict ){
1883 // return areDisequal( n1, n2 );
1889 //-------------------------------------------------- handling assertions / eqc
1891 void QuantConflictFind::assertNode( Node q
) {
1893 if( d_quantEngine->hasOwnership( q, this ) ){
1894 Trace("qcf-proc") << "QCF : assertQuantifier : ";
1895 debugPrintQuant("qcf-proc", q);
1896 Trace("qcf-proc") << std::endl;
1902 void QuantConflictFind::newEqClass( Node n
) {
1907 void QuantConflictFind::merge( Node a
, Node b
) {
1911 /** assert disequal */
1912 void QuantConflictFind::assertDisequal( Node a
, Node b
) {
1916 //-------------------------------------------------- check function
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
;
1929 return performCheck
;
1932 void QuantConflictFind::reset_round( Theory::Effort level
) {
1933 d_needs_computeRelEqr
= true;
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
;
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
;
1947 int addedLemmas
= 0;
1948 ++(d_statistics
.d_inst_rounds
);
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
;
1956 computeRelevantEqr();
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
);
1966 if( Trace
.isOn("qcf-debug") ){
1967 Trace("qcf-debug") << std::endl
;
1968 debugPrint("qcf-debug");
1969 Trace("qcf-debug") << std::endl
;
1971 short end_e
= getMaxQcfEffort();
1972 bool isConflict
= false;
1973 for( short e
= effort_conflict
; e
<=end_e
; e
++ ){
1975 Trace("qcf-check") << "Checking quantified formulas at effort " << e
<< "..." << std::endl
;
1976 for( unsigned j
=0; j
<qorder
.size(); j
++ ){
1978 QuantInfo
* qi
= &d_qinfo
[q
];
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
;
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
) ){
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
);
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
;
2013 if( e
==effort_conflict
){
2014 d_quantEngine
->markRelevant( q
);
2015 ++(d_statistics
.d_conflict_inst
);
2016 if( options::qcfAllConflict() ){
2019 d_conflict
.set( true );
2022 }else if( e
==effort_prop_eq
){
2023 d_quantEngine
->markRelevant( q
);
2024 ++(d_statistics
.d_prop_inst
);
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
2034 qi
->revertMatch( assigned
);
2035 d_tempCache
.clear();
2037 Trace("qcf-inst") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl
;
2040 Trace("qcf-inst") << " ... Spurious instantiation (match is inconsistent)" << std::endl
;
2043 Trace("qcf-check") << "Done, conflict = " << d_conflict
<< std::endl
;
2049 if( addedLemmas
>0 ){
2054 d_conflict
.set( true );
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
;
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
;
2069 Trace("qcf-check2") << "QCF : finished check : " << level
<< std::endl
;
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();
2081 //d_arg_reps.clear();
2083 //if( Trace.isOn("qcf-opt") ){
2084 // clSet = double(clock())/double(CLOCKS_PER_SEC);
2087 //now, store matches
2088 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( getEqualityEngine() );
2089 while( !eqcs_i
.isFinished() ){
2091 if( getTermDatabase()->hasTermCurrent( r
) ){
2092 TypeNode rtn
= r
.getType();
2093 if( !options::cbqi() || !TermDb::hasInstConstAttr( r
) ){
2094 d_eqcs
[rtn
].push_back( r
);
2103 //-------------------------------------------------- debugging
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() ){
2112 //if( !n.getType().isInteger() ){
2113 Trace(c
) << " - " << n
<< " : {";
2114 eq::EqClassIterator eqc_i
= eq::EqClassIterator( n
, getEqualityEngine() );
2116 while( !eqc_i
.isFinished() ){
2118 if( nn
.getKind()!=EQUAL
&& nn
!=n
){
2119 Trace(c
) << (pr
? "," : "" ) << " " << nn
;
2124 Trace(c
) << (pr
? " " : "" ) << "}" << std::endl
;
2129 void QuantConflictFind::debugPrintQuant( const char * c
, Node q
) {
2130 Trace(c
) << "Q" << d_quant_id
[q
];
2133 void QuantConflictFind::debugPrintQuantBody( const char * c
, Node q
, Node n
, bool doVarNum
) {
2134 if( n
.getNumChildren()==0 ){
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
];
2140 if( n
.getKind()==APPLY_UF
){
2141 Trace(c
) << n
.getOperator();
2143 Trace(c
) << n
.getKind();
2145 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
2147 debugPrintQuantBody( c
, q
, n
[i
] );
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)
2159 smtStatisticsRegistry()->registerStat(&d_inst_rounds
);
2160 smtStatisticsRegistry()->registerStat(&d_conflict_inst
);
2161 smtStatisticsRegistry()->registerStat(&d_prop_inst
);
2162 smtStatisticsRegistry()->registerStat(&d_entailment_checks
);
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
);
2172 TNode
QuantConflictFind::getZero( Kind k
) {
2173 std::map
< Kind
, Node
>::iterator it
= d_zero
.find( k
);
2174 if( it
==d_zero
.end() ){
2177 nn
= NodeManager::currentNM()->mkConst( Rational(0) );
2186 } /* namespace CVC4::theory::quantifiers */
2187 } /* namespace CVC4::theory */
2188 } /* namespace CVC4 */