1bf53db9149ce65ac32598b0008c199e78a13762
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-2013 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"
23 using namespace CVC4::kind
;
24 using namespace CVC4::theory
;
25 using namespace CVC4::theory::quantifiers
;
30 Node
QcfNodeIndex::addTerm( QuantConflictFind
* qcf
, Node n
, bool doAdd
, int index
) {
31 if( index
==(int)n
.getNumChildren() ){
32 if( d_children
.empty() ){
34 d_children
[ n
].clear();
40 return d_children
.begin()->first
;
43 Node r
= qcf
->getRepresentative( n
[index
] );
44 return d_children
[r
].addTerm( qcf
, n
, doAdd
, index
+1 );
48 bool QcfNodeIndex::addTermEq( QuantConflictFind
* qcf
, Node n1
, Node n2
, int index
) {
49 if( index
==(int)n1
.getNumChildren() ){
50 Node n
= addTerm( qcf
, n2
);
53 Node r
= qcf
->getRepresentative( n1
[index
] );
54 return d_children
[r
].addTermEq( qcf
, n1
, n2
, index
+1 );
58 void QcfNodeIndex::debugPrint( const char * c
, int t
) {
59 for( std::map
< Node
, QcfNodeIndex
>::iterator it
= d_children
.begin(); it
!= d_children
.end(); ++it
){
60 if( !it
->first
.isNull() ){
61 for( int j
=0; j
<t
; j
++ ){ Trace(c
) << " "; }
62 Trace(c
) << it
->first
<< " : " << std::endl
;
63 it
->second
.debugPrint( c
, t
+1 );
68 EqRegistry::EqRegistry( context::Context
* c
) : d_active( c
, false ){//: d_t_eqc( c ){
72 void EqRegistry::debugPrint( const char * c
, int t
) {
73 d_qni
.debugPrint( c
, t
);
76 //QcfNode::QcfNode( context::Context* c ) : d_parent( NULL ){
81 QuantConflictFind::QuantConflictFind( QuantifiersEngine
* qe
, context::Context
* c
) :
82 QuantifiersModule( qe
),
84 d_conflict( c
, false ),
87 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
88 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
89 getFunctionId( d_true
);
90 getFunctionId( d_false
);
93 int QuantConflictFind::getFunctionId( Node f
) {
94 std::map
< Node
, int >::iterator it
= d_fid
.find( f
);
95 if( it
==d_fid
.end() ){
96 d_fid
[f
] = d_fid_count
;
103 bool QuantConflictFind::isLessThan( Node a
, Node b
) {
104 Assert( a
.getKind()==APPLY_UF
);
105 Assert( b
.getKind()==APPLY_UF
);
107 if( a.getOperator()==b.getOperator() ){
108 for( unsigned i=0; i<a.getNumChildren(); i++ ){
109 Node acr = getRepresentative( a[i] );
110 Node bcr = getRepresentative( b[i] );
120 return getFunctionId( a
.getOperator() )<getFunctionId( b
.getOperator() );
124 Node
QuantConflictFind::getFunction( Node n
, bool isQuant
) {
125 if( isQuant
&& !quantifiers::TermDb::hasBoundVarAttr( n
) ){
127 }else if( n
.getKind()==APPLY_UF
){
128 std::map
< Node
, Node
>::iterator it
= d_op_node
.find( n
.getOperator() );
129 if( it
==d_op_node
.end() ){
130 std::vector
< Node
> children
;
131 children
.push_back( n
.getOperator() );
132 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
133 children
.push_back( getFv( n
[i
].getType() ) );
135 Node nn
= NodeManager::currentNM()->mkNode( APPLY_UF
, children
);
136 d_op_node
[n
.getOperator()] = nn
;
142 //should be a variable
147 Node
QuantConflictFind::getFv( TypeNode tn
) {
148 if( d_fv
.find( tn
)==d_fv
.end() ){
149 std::stringstream ss
;
151 d_fv
[tn
] = NodeManager::currentNM()->mkSkolem( ss
.str(), tn
, "is for QCF" );
156 Node
QuantConflictFind::mkEqNode( Node a
, Node b
) {
157 if( a
.getType().isBoolean() ){
158 return a
.iffNode( b
);
160 return a
.eqNode( b
);
164 //-------------------------------------------------- registration
167 void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {
168 for( unsigned i=0; i<assertions.size(); i++ ){
169 registerAssertion( assertions[i] );
173 void QuantConflictFind::registerAssertion( Node n ) {
174 if( n.getKind()==FORALL ){
175 registerQuant( Node::null(), n[1], NULL, true, true );
177 if( n.getType().isBoolean() ){
178 for( unsigned i=0; i<n.getNumChildren(); i++ ){
179 registerAssertion( n[i] );
185 void QuantConflictFind::registerQuant( Node q
, Node n
, bool hasPol
, bool pol
) {
188 if( n
.getKind()!=OR
&& n
.getKind()!=AND
&& n
.getKind()!=IFF
&& n
.getKind()!=ITE
&& n
.getKind()!=NOT
){
189 if( quantifiers::TermDb::hasBoundVarAttr( n
) ){
191 for( unsigned i
=0; i
<2; i
++ ){
192 if( !hasPol
|| ( pol
!=(i
==0) ) ){
193 EqRegistry
* eqr
= getEqRegistry( i
==0, n
);
195 d_qinfo
[q
].d_rel_eqr
[ eqr
] = true;
199 if( n
.getKind()==APPLY_UF
||
200 ( n
.getKind()==EQUAL
&& ( n
[0].getKind()==BOUND_VARIABLE
|| n
[1].getKind()==BOUND_VARIABLE
) ) ){
203 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
208 Trace("qcf-qregister") << " RegisterGroundLit : " << n
;
213 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
216 QuantPhaseReq::getPolarity( n
, i
, hasPol
, pol
, newHasPol
, newPol
);
217 //QcfNode * qcfc = new QcfNode( d_c );
218 //qcfc->d_parent = qcf;
219 //qcf->d_child[i] = qcfc;
220 registerQuant( q
, n
[i
], newHasPol
, newPol
);
225 void QuantConflictFind::flatten( Node q
, Node n
) {
226 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
227 if( quantifiers::TermDb::hasBoundVarAttr( n
[i
] ) && n
.getKind()!=BOUND_VARIABLE
){
228 if( d_qinfo
[q
].d_var_num
.find( n
[i
] )==d_qinfo
[q
].d_var_num
.end() ){
229 //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;
230 d_qinfo
[q
].d_var_num
[n
[i
]] = d_qinfo
[q
].d_vars
.size();
231 d_qinfo
[q
].d_vars
.push_back( n
[i
] );
238 void QuantConflictFind::registerQuantifier( Node q
) {
239 d_quants
.push_back( q
);
240 d_quant_id
[q
] = d_quants
.size();
241 Trace("qcf-qregister") << "Register ";
242 debugPrintQuant( "qcf-qregister", q
);
243 Trace("qcf-qregister") << " : " << q
<< std::endl
;
245 //register the variables
246 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
247 d_qinfo
[q
].d_var_num
[q
[0][i
]] = i
;
248 d_qinfo
[q
].d_vars
.push_back( q
[0][i
] );
251 //make QcfNode structure
252 Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl
;
253 //d_qinfo[q].d_cf = new QcfNode( d_c );
254 registerQuant( q
, q
[1], true, true );
257 Trace("qcf-qregister") << "- Flattened structure is :" << std::endl
;
258 Trace("qcf-qregister") << " ";
259 debugPrintQuantBody( "qcf-qregister", q
, q
[1] );
260 Trace("qcf-qregister") << std::endl
;
261 if( d_qinfo
[q
].d_vars
.size()>q
[0].getNumChildren() ){
262 Trace("qcf-qregister") << " with additional constraints : " << std::endl
;
263 for( unsigned j
=q
[0].getNumChildren(); j
<d_qinfo
[q
].d_vars
.size(); j
++ ){
264 Trace("qcf-qregister") << " ?x" << j
<< " = ";
265 debugPrintQuantBody( "qcf-qregister", q
, d_qinfo
[q
].d_vars
[j
], false );
266 Trace("qcf-qregister") << std::endl
;
270 Trace("qcf-qregister") << "- Make match gen structure..." << std::endl
;
271 d_qinfo
[q
].d_mg
= new MatchGen( this, q
, q
[1], true );
273 Trace("qcf-qregister") << "Done registering quantifier." << std::endl
;
276 EqRegistry
* QuantConflictFind::getEqRegistry( bool polarity
, Node lit
, bool doCreate
) {
277 Assert( quantifiers::TermDb::hasBoundVarAttr( lit
) );
281 if( lit
.getKind()==EQUAL
){
282 i
= polarity
? 0 : 1;
283 f1
= getFunction( lit
[0], true );
284 f2
= getFunction( lit
[1], true );
285 }else if( lit
.getKind()==APPLY_UF
){
287 f1
= getFunction( lit
, true );
288 f2
= polarity
? d_true
: d_false
;
290 if( !f1
.isNull() && !f2
.isNull() ){
291 if( d_eqr
[i
][f1
].find( f2
)==d_eqr
[i
][f1
].end() ){
293 Trace("qcf-register") << "RegisterEqr : " << f1
<< " " << f2
<< ", polarity = " << (i
==0) << std::endl
;
294 d_eqr
[i
][f1
][f2
] = new EqRegistry( d_c
);
295 d_eqr
[i
][f2
][f1
] = d_eqr
[i
][f1
][f2
];
300 return d_eqr
[i
][f1
][f2
];
306 void QuantConflictFind::getEqRegistryApps( Node lit
, std::vector
< Node
>& terms
) {
307 Assert( quantifiers::TermDb::hasBoundVarAttr( lit
) );
308 if( lit
.getKind()==EQUAL
){
310 for( unsigned i
=0; i
<2; i
++ ){
311 if( quantifiers::TermDb::hasBoundVarAttr( lit
[i
] ) ){
312 if( lit
[i
].getKind()==BOUND_VARIABLE
){
313 //do not handle variable equalities
317 allUf
= allUf
&& lit
[i
].getKind()==APPLY_UF
;
318 terms
.push_back( lit
[i
] );
322 if( terms
.size()==2 && allUf
&& isLessThan( terms
[1], terms
[0] ) ){
327 }else if( lit
.getKind()==APPLY_UF
){
328 terms
.push_back( lit
);
332 int QuantConflictFind::evaluate( Node n
) {
334 if( n
.getKind()==EQUAL
){
335 Node n1
= getTerm( n
[0] );
336 Node n2
= getTerm( n
[1] );
337 Debug("qcf-eval") << "Evaluate : Normalize " << n
<< " to " << n1
<< " = " << n2
<< std::endl
;
338 if( areEqual( n1
, n2
) ){
340 }else if( areDisequal( n1
, n2
) ){
343 }else if( n
.getKind()==APPLY_UF
){
344 Node nn
= getTerm( n
);
345 Debug("qcf-eval") << "Evaluate : Normalize " << nn
<< " to " << n
<< std::endl
;
346 if( areEqual( nn
, d_true
) ){
348 }else if( areEqual( nn
, d_false
) ){
351 }else if( n
.getKind()==NOT
){
352 return -evaluate( n
[0] );
353 }else if( n
.getKind()==ITE
){
354 int cev1
= evaluate( n
[0] );
355 int cevc
[2] = { 0, 0 };
356 for( unsigned i
=0; i
<2; i
++ ){
357 if( ( i
==0 && cev1
!=-1 ) || ( i
==1 && cev1
!=1 ) ){
358 cevc
[i
] = evaluate( n
[i
+1] );
362 }else if( cevc
[i
]==0 ){
367 if( ret
==0 && cevc
[0]!=0 && cevc
[0]==cevc
[1] ){
370 }else if( n
.getKind()==IFF
){
371 int cev1
= evaluate( n
[0] );
373 int cev2
= evaluate( n
[1] );
375 ret
= cev1
==cev2
? 1 : -1;
381 if( n
.getKind()==OR
){
383 }else if( n
.getKind()==AND
){
387 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
388 int cev
= evaluate( n
[i
] );
396 if( ret
==0 && !isUnk
){
400 Debug("qcf-eval") << "Evaluate " << n
<< " to " << ret
<< std::endl
;
404 //-------------------------------------------------- handling assertions / eqc
406 void QuantConflictFind::assertNode( Node q
) {
407 Trace("qcf-proc") << "QCF : assertQuantifier : ";
408 debugPrintQuant("qcf-proc", q
);
409 Trace("qcf-proc") << std::endl
;
410 d_qassert
.push_back( q
);
411 //set the eqRegistries that this depends on to true
412 for( std::map
< EqRegistry
*, bool >::iterator it
= d_qinfo
[q
].d_rel_eqr
.begin(); it
!= d_qinfo
[q
].d_rel_eqr
.end(); ++it
){
413 it
->first
->d_active
.set( true );
417 eq::EqualityEngine
* QuantConflictFind::getEqualityEngine() {
418 //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();
419 return d_quantEngine
->getTheoryEngine()->getMasterEqualityEngine();
421 bool QuantConflictFind::areEqual( Node n1
, Node n2
) {
422 return getEqualityEngine()->hasTerm( n1
) && getEqualityEngine()->hasTerm( n2
) && getEqualityEngine()->areEqual( n1
,n2
);
424 bool QuantConflictFind::areDisequal( Node n1
, Node n2
) {
425 return getEqualityEngine()->hasTerm( n1
) && getEqualityEngine()->hasTerm( n2
) && getEqualityEngine()->areDisequal( n1
,n2
, false );
427 Node
QuantConflictFind::getRepresentative( Node n
) {
428 if( getEqualityEngine()->hasTerm( n
) ){
429 return getEqualityEngine()->getRepresentative( n
);
434 Node
QuantConflictFind::getTerm( Node n
) {
435 if( n
.getKind()==APPLY_UF
){
436 Node nn
= d_uf_terms
[n
.getOperator()].addTerm( this, n
, false );
444 QuantConflictFind::EqcInfo
* QuantConflictFind::getEqcInfo( Node n
, bool doCreate
) {
446 NodeBoolMap::iterator it = d_eqc.find( n );
447 if( it==d_eqc.end() ){
451 //equivalence class does not currently exist
455 //should only ask for valid equivalence classes
456 Assert( (*it).second );
459 std::map
< Node
, EqcInfo
* >::iterator it2
= d_eqc_info
.find( n
);
460 if( it2
==d_eqc_info
.end() ){
462 EqcInfo
* eqci
= new EqcInfo( d_c
);
463 d_eqc_info
[n
] = eqci
;
473 void QuantConflictFind::newEqClass( Node n
) {
474 Trace("qcf-proc-debug") << "QCF : newEqClass : " << n
<< std::endl
;
476 Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n
<< std::endl
;
480 void QuantConflictFind::merge( Node a
, Node b
) {
481 if( b
.getKind()==EQUAL
){
484 //merge( b[0], b[1] );
485 }else if( a
==d_false
){
486 assertDisequal( b
[0], b
[1] );
489 Trace("qcf-proc") << "QCF : merge : " << a
<< " " << b
<< std::endl
;
490 EqcInfo
* eqc_b
= getEqcInfo( b
, false );
491 EqcInfo
* eqc_a
= NULL
;
493 eqc_a
= getEqcInfo( a
);
494 //move disequalities of b into a
495 for( NodeBoolMap::iterator it
= eqc_b
->d_diseq
.begin(); it
!= eqc_b
->d_diseq
.end(); ++it
){
497 Node n
= (*it
).first
;
498 EqcInfo
* eqc_n
= getEqcInfo( n
, false );
500 if( !eqc_n
->isDisequal( a
) ){
501 Assert( !eqc_a
->isDisequal( n
) );
502 eqc_n
->setDisequal( a
);
503 eqc_a
->setDisequal( n
);
504 //setEqual( eqc_a, eqc_b, a, n, false );
506 eqc_n
->setDisequal( b
, false );
510 //move all previous EqcRegistry's regarding equalities within b
511 for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){
513 eqc_a->d_rel_eqr_e[(*it).first] = true;
518 //process new equalities
519 //setEqual( eqc_a, eqc_b, a, b, true );
520 Trace("qcf-proc2") << "QCF : finished merge : " << a
<< " " << b
<< std::endl
;
524 /** assert disequal */
525 void QuantConflictFind::assertDisequal( Node a
, Node b
) {
526 a
= getRepresentative( a
);
527 b
= getRepresentative( b
);
528 Trace("qcf-proc") << "QCF : assert disequal : " << a
<< " " << b
<< std::endl
;
529 EqcInfo
* eqc_a
= getEqcInfo( a
);
530 EqcInfo
* eqc_b
= getEqcInfo( b
);
531 if( !eqc_a
->isDisequal( b
) ){
532 Assert( !eqc_b
->isDisequal( a
) );
533 eqc_b
->setDisequal( a
);
534 eqc_a
->setDisequal( b
);
535 //setEqual( eqc_a, eqc_b, a, b, false );
537 Trace("qcf-proc2") << "QCF : finished assert disequal : " << a
<< " " << b
<< std::endl
;
540 //-------------------------------------------------- check function
543 void QuantConflictFind::check( Theory::Effort level
) {
544 Trace("qcf-check") << "QCF : check : " << level
<< std::endl
;
546 Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl
;
548 bool addedLemma
= false;
549 if( d_performCheck
){
550 ++(d_statistics
.d_inst_rounds
);
552 if( Trace
.isOn("qcf-engine") ){
553 clSet
= double(clock())/double(CLOCKS_PER_SEC
);
554 Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
<< "---" << std::endl
;
556 Trace("qcf-check") << "Compute relevant equalities..." << std::endl
;
557 computeRelevantEqr();
559 Trace("qcf-debug") << std::endl
;
560 debugPrint("qcf-debug");
561 Trace("qcf-debug") << std::endl
;
564 Trace("qcf-check") << "Checking quantified formulas..." << std::endl
;
565 for( unsigned j
=0; j
<d_qassert
.size(); j
++ ){
566 Node q
= d_qassert
[j
];
567 Trace("qcf-check") << "Check quantified formula ";
568 debugPrintQuant("qcf-check", q
);
569 Trace("qcf-check") << " : " << q
<< "..." << std::endl
;
571 Assert( d_qinfo
.find( q
)!=d_qinfo
.end() );
572 if( d_qinfo
[q
].d_mg
->isValid() ){
573 d_qinfo
[q
].reset_round( this );
574 //try to make a matches making the body false
575 d_qinfo
[q
].d_mg
->reset( this, false, q
);
576 while( d_qinfo
[q
].d_mg
->getNextMatch( this, q
) ){
578 Trace("qcf-check") << "*** Produced match : " << std::endl
;
579 d_qinfo
[q
].debugPrintMatch("qcf-check");
580 Trace("qcf-check") << std::endl
;
582 if( !d_qinfo
[q
].isMatchSpurious( this ) ){
583 //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
584 Trace("qcf-check") << std::endl
;
585 std::vector
< int > unassigned
;
586 std::vector
< TypeNode
> unassigned_tn
;
587 for( int i
=0; i
<d_qinfo
[q
].getNumVars(); i
++ ){
588 if( d_qinfo
[q
].d_match
.find( i
)==d_qinfo
[q
].d_match
.end() ){
589 Assert( i
<(int)q
[0].getNumChildren() );
590 unassigned
.push_back( i
);
591 unassigned_tn
.push_back( d_qinfo
[q
].getVar( i
).getType() );
595 if( !unassigned
.empty() ){
596 Trace("qcf-check") << "Assign to unassigned..." << std::endl
;
598 std::vector
< int > eqc_count
;
601 while( ( index
>=0 && (int)index
<(int)unassigned
.size() ) || invalidMatch
){
602 invalidMatch
= false;
603 if( index
==(int)eqc_count
.size() ){
604 eqc_count
.push_back( 0 );
606 Assert( index
==(int)eqc_count
.size()-1 );
607 if( eqc_count
[index
]<(int)d_eqcs
[unassigned_tn
[index
]].size() ){
608 int currIndex
= eqc_count
[index
];
610 Trace("qcf-check-unassign") << unassigned
[index
] << "->" << d_eqcs
[unassigned_tn
[index
]][currIndex
] << std::endl
;
611 if( d_qinfo
[q
].setMatch( this, unassigned
[index
], d_eqcs
[unassigned_tn
[index
]][currIndex
] ) ){
612 Trace("qcf-check-unassign") << "Succeeded match" << std::endl
;
615 Trace("qcf-check-unassign") << "Failed match" << std::endl
;
619 Trace("qcf-check-unassign") << "No more matches" << std::endl
;
620 eqc_count
.pop_back();
627 index
= (int)unassigned
.size()-1;
628 Trace("qcf-check-unassign") << " Try: " << std::endl
;
629 for( unsigned i
=0; i
<unassigned
.size(); i
++ ){
630 int ui
= unassigned
[i
];
631 Trace("qcf-check-unassign") << " Assigned #" << ui
<< " : " << d_qinfo
[q
].d_vars
[ui
] << " -> " << d_qinfo
[q
].d_match
[ui
] << std::endl
;
634 }while( success
&& d_qinfo
[q
].isMatchSpurious( this ) );
639 for( unsigned i
=0; i
<q
[0].getNumChildren(); i
++ ){
640 Node cv
= d_qinfo
[q
].getCurrentValue( d_qinfo
[q
].d_match
[i
] );
641 Debug("qcf-check-inst") << "INST : " << i
<< " -> " << cv
<< ", from " << d_qinfo
[q
].d_match
[i
] << std::endl
;
642 m
.set( d_quantEngine
, q
, i
, cv
);
644 if( Debug
.isOn("qcf-check-inst") ){
645 Node inst
= d_quantEngine
->getInstantiation( q
, m
);
646 Debug("qcf-check-inst") << "Check instantiation " << inst
<< "..." << std::endl
;
647 Assert( evaluate( inst
)==-1 );
649 if( d_quantEngine
->addInstantiation( q
, m
) ){
650 Trace("qcf-check") << " ... Added instantiation" << std::endl
;
651 d_quantEngine
->flushLemmas();
652 d_conflict
.set( true );
654 ++(d_statistics
.d_conflict_inst
);
657 Trace("qcf-check") << " ... Failed to add instantiation" << std::endl
;
661 Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl
;
663 for( unsigned i
=0; i
<unassigned
.size(); i
++ ){
664 d_qinfo
[q
].d_match
.erase( unassigned
[i
] );
667 Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl
;
675 if( Trace
.isOn("qcf-engine") ){
676 double clSet2
= double(clock())/double(CLOCKS_PER_SEC
);
677 Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2
-clSet
) << ", addedLemma = " << addedLemma
<< std::endl
;
680 Trace("qcf-check2") << "QCF : finished check : " << level
<< std::endl
;
684 bool QuantConflictFind::needsCheck( Theory::Effort level
) {
685 d_performCheck
= false;
686 if( !d_conflict
&& level
==Theory::EFFORT_FULL
){
687 d_performCheck
= true;
689 return d_performCheck
;
692 void QuantConflictFind::computeRelevantEqr() {
693 //first, reset information
694 for( unsigned i
=0; i
<2; i
++ ){
695 for( std::map
< Node
, std::map
< Node
, EqRegistry
* > >::iterator it
= d_eqr
[i
].begin(); it
!= d_eqr
[i
].end(); ++it
){
696 for( std::map
< Node
, EqRegistry
* >::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
697 it2
->second
->clear();
702 d_eqc_uf_terms
.clear();
705 //which nodes are irrelevant for disequality matches
706 std::map
< Node
, bool > irrelevant_dnode
;
707 //which eqc we have processed
708 std::map
< Node
, bool > process_eqc
;
710 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( getEqualityEngine() );
711 while( !eqcs_i
.isFinished() ){
713 d_eqcs
[r
.getType()].push_back( r
);
714 EqcInfo
* eqcir
= getEqcInfo( r
, false );
715 //get relevant nodes that we are disequal from
716 std::vector
< Node
> deqc
;
718 for( NodeBoolMap::iterator it
= eqcir
->d_diseq
.begin(); it
!= eqcir
->d_diseq
.end(); ++it
){
720 Node rd
= (*it
).first
;
721 //if we have processed the other direction
722 if( process_eqc
.find( rd
)!=process_eqc
.end() ){
723 eq::EqClassIterator eqcd_i
= eq::EqClassIterator( rd
, getEqualityEngine() );
724 while( !eqcd_i
.isFinished() ){
726 if( irrelevant_dnode
.find( nd
)==irrelevant_dnode
.end() ){
727 deqc
.push_back( nd
);
735 //the relevant nodes in this eqc
736 std::vector
< Node
> eqc
;
737 //process disequalities
738 eq::EqClassIterator eqc_i
= eq::EqClassIterator( r
, getEqualityEngine() );
739 while( !eqc_i
.isFinished() ){
742 if( n
.getKind()==APPLY_UF
){
743 Node nadd
= d_eqc_uf_terms
[r
][n
.getOperator()].addTerm( this, n
);
744 isRedundant
= (nadd
!=n
);
745 d_uf_terms
[n
.getOperator()].addTerm( this, n
);
749 //process all relevant equalities and disequalities to n
750 for( unsigned index
=0; index
<2; index
++ ){
751 std::map
< Node
, std::map
< Node
, EqRegistry
* > >::iterator itn
[2];
752 itn
[0] = d_eqr
[index
].find( n
);
754 if( n
.getKind()==APPLY_UF
&& !isRedundant
){
755 fn
= getFunction( n
);
756 itn
[1] = d_eqr
[index
].find( fn
);
759 bool relevant
= false;
760 for( unsigned j
=0; j
<2; j
++ ){
761 //if this node is relevant as an ground term or f-application
762 if( ( j
==0 || !fn
.isNull() ) && itn
[j
]!=d_eqr
[index
].end() ){
764 std::vector
< Node
>& rel_nodes
= index
==0 ? eqc
: deqc
;
765 for( unsigned i
=0; i
<rel_nodes
.size(); i
++ ){
766 Node m
= rel_nodes
[i
];
768 if( m
.getKind()==APPLY_UF
){
769 fm
= getFunction( m
);
771 //process equality/disequality
774 std::map
< Node
, EqRegistry
* >::iterator itm
= itn
[j
]->second
.find( m
);
775 if( itm
!=itn
[j
]->second
.end() ){
776 if( itm
->second
->d_qni
.addTerm( this, n
)==n
){
777 Trace("qcf-reqr") << "Add relevant : " << n
<< (index
==0?"":"!") << "=" << m
<< " for ";
778 Trace("qcf-reqr") << fn
<< " " << m
<< std::endl
;
783 std::map
< Node
, EqRegistry
* >::iterator itm
= itn
[j
]->second
.find( fm
);
784 if( itm
!=itn
[j
]->second
.end() ){
787 if( itm
->second
->d_qni
.addTerm( this, m
)==m
){
788 Trace("qcf-reqr") << "Add relevant : " << n
<< (index
==0?"":"!") << "=" << m
<< " for ";
789 Trace("qcf-reqr") << n
<< " " << fm
<< std::endl
;
793 bool mltn
= isLessThan( m
, n
);
794 for( unsigned i
=0; i
<2; i
++ ){
795 if( i
==0 || m
.getOperator()==n
.getOperator() ){
796 Node am
= ((i
==0)==mltn
) ? n
: m
;
797 Node an
= ((i
==0)==mltn
) ? m
: n
;
798 if( itm
->second
->d_qni
.addTermEq( this, an
, am
) ){
799 Trace("qcf-reqr") << "Add relevant (eq) : " << an
<< (index
==0?"":"!") << "=" << am
<< " for ";
800 Trace("qcf-reqr") << fn
<< " " << fm
<< std::endl
;
811 //if not relevant for disequalities, store it
813 irrelevant_dnode
[n
] = true;
816 //if relevant for equalities, store it
824 process_eqc
[r
] = true;
830 void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind
* p
) {
832 d_curr_var_deq
.clear();
833 //add built-in variable constraints
834 for( unsigned r
=0; r
<2; r
++ ){
835 for( std::map
< int, std::vector
< Node
> >::iterator it
= d_var_constraint
[r
].begin();
836 it
!= d_var_constraint
[r
].end(); ++it
){
837 for( unsigned j
=0; j
<it
->second
.size(); j
++ ){
838 Node rr
= it
->second
[j
];
840 rr
= p
->getRepresentative( rr
);
842 if( addConstraint( p
, it
->first
, rr
, r
==0 )==-1 ){
843 d_var_constraint
[0].clear();
844 d_var_constraint
[1].clear();
845 //quantified formula is actually equivalent to true
846 Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl
;
847 d_mg
->d_children
.clear();
848 d_mg
->d_n
= NodeManager::currentNM()->mkConst( true );
849 d_mg
->d_type
= MatchGen::typ_ground
;
855 d_mg
->reset_round( p
);
858 int QuantConflictFind::QuantInfo::getCurrentRepVar( int v
) {
859 std::map
< int, Node
>::iterator it
= d_match
.find( v
);
860 if( it
!=d_match
.end() ){
861 int vn
= getVarNum( it
->second
);
863 //int vr = getCurrentRepVar( vn );
864 //d_match[v] = d_vars[vr];
866 return getCurrentRepVar( vn
);
872 Node
QuantConflictFind::QuantInfo::getCurrentValue( Node n
) {
873 int v
= getVarNum( n
);
877 std::map
< int, Node
>::iterator it
= d_match
.find( v
);
878 if( it
==d_match
.end() ){
881 Assert( getVarNum( it
->second
)!=v
);
882 return getCurrentValue( it
->second
);
887 bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind
* p
, int v
, Node n
) {
888 //check disequalities
889 for( std::map
< Node
, int >::iterator it
= d_curr_var_deq
[v
].begin(); it
!= d_curr_var_deq
[v
].end(); ++it
){
890 Node cv
= getCurrentValue( it
->first
);
891 Debug("qcf-ccbe") << "compare " << cv
<< " " << n
<< std::endl
;
894 }else if( !isVar( n
) && !isVar( cv
) ){
895 //they must actually be disequal
896 if( !p
->areDisequal( n
, cv
) ){
904 int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind
* p
, int v
, Node n
, bool polarity
) {
905 v
= getCurrentRepVar( v
);
906 int vn
= getVarNum( n
);
907 vn
= vn
==-1 ? -1 : getCurrentRepVar( vn
);
908 n
= getCurrentValue( n
);
909 return addConstraint( p
, v
, n
, vn
, polarity
, false );
912 int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind
* p
, int v
, Node n
, int vn
, bool polarity
, bool doRemove
) {
913 //for handling equalities between variables, and disequalities involving variables
914 Debug("qcf-match-debug") << "- " << (doRemove
? "un" : "" ) << "constrain : " << v
<< " -> " << n
<< " (cv=" << getCurrentValue( n
) << ")";
915 Debug("qcf-match-debug") << ", (vn=" << vn
<< "), polarity = " << polarity
<< std::endl
;
916 Assert( n
==getCurrentValue( n
) );
917 Assert( doRemove
|| v
==getCurrentRepVar( v
) );
918 Assert( doRemove
|| vn
==getCurrentRepVar( getVarNum( n
) ) );
923 //if set to this in the opposite direction, clean up opposite instead
924 std::map
< int, Node
>::iterator itmn
= d_match
.find( vn
);
925 if( itmn
!=d_match
.end() && itmn
->second
==d_vars
[v
] ){
926 return addConstraint( p
, vn
, d_vars
[v
], v
, true, true );
928 //unsetting variables equal
930 //remove disequalities owned by this
931 std::vector
< Node
> remDeq
;
932 for( std::map
< Node
, int >::iterator it
= d_curr_var_deq
[vn
].begin(); it
!= d_curr_var_deq
[vn
].end(); ++it
){
934 remDeq
.push_back( it
->first
);
937 for( unsigned i
=0; i
<remDeq
.size(); i
++ ){
938 d_curr_var_deq
[vn
].erase( remDeq
[i
] );
945 std::map
< int, Node
>::iterator itm
= d_match
.find( v
);
948 Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl
;
949 std::map
< int, Node
>::iterator itmn
= d_match
.find( vn
);
950 if( itm
==d_match
.end() ){
951 //setting variables equal
952 bool alreadySet
= false;
953 if( itmn
!=d_match
.end() ){
955 Assert( !itmn
->second
.isNull() && !isVar( itmn
->second
) );
958 //copy or check disequalities
959 std::vector
< Node
> addDeq
;
960 for( std::map
< Node
, int >::iterator it
= d_curr_var_deq
[v
].begin(); it
!= d_curr_var_deq
[v
].end(); ++it
){
961 Node dv
= getCurrentValue( it
->first
);
963 if( d_curr_var_deq
[vn
].find( dv
)==d_curr_var_deq
[vn
].end() ){
964 d_curr_var_deq
[vn
][dv
] = v
;
965 addDeq
.push_back( dv
);
968 if( itmn
->second
!=dv
){
969 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
975 n
= getCurrentValue( n
);
978 if( itmn
==d_match
.end() ){
979 Debug("qcf-match-debug") << " ...Reverse direction" << std::endl
;
980 //set the opposite direction
981 return addConstraint( p
, vn
, d_vars
[v
], v
, true, false );
983 Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl
;
984 //are they currently equal
985 return itm
->second
==itmn
->second
? 0 : -1;
989 Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl
;
990 if( itm
==d_match
.end() ){
993 //compare ground values
994 Debug("qcf-match-debug") << " -> Ground value, compare " << itm
->second
<< " "<< n
<< std::endl
;
995 return itm
->second
==n
? 0 : -1;
998 if( setMatch( p
, v
, n
) ){
999 Debug("qcf-match-debug") << " -> success" << std::endl
;
1002 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
1007 Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl
;
1012 Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl
;
1016 Assert( d_curr_var_deq
[v
].find( n
)!=d_curr_var_deq
[v
].end() );
1017 d_curr_var_deq
[v
].erase( n
);
1020 if( d_curr_var_deq
[v
].find( n
)==d_curr_var_deq
[v
].end() ){
1021 //check if it respects equality
1022 std::map
< int, Node
>::iterator itm
= d_match
.find( v
);
1023 if( itm
!=d_match
.end() ){
1024 if( getCurrentValue( n
)==itm
->second
){
1025 Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl
;
1029 d_curr_var_deq
[v
][n
] = v
;
1030 Debug("qcf-match-debug") << " -> success" << std::endl
;
1033 Debug("qcf-match-debug") << " -> redundant disequality" << std::endl
;
1041 bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind
* p
, int v
, Node n
) {
1042 if( getCurrentCanBeEqual( p
, v
, n
) ){
1043 Debug("qcf-match-debug") << "-- bind : " << v
<< " -> " << n
<< ", checked " << d_curr_var_deq
[v
].size() << " disequalities" << std::endl
;
1051 bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind
* p
) {
1052 for( int i
=0; i
<getNumVars(); i
++ ){
1053 std::map
< int, Node
>::iterator it
= d_match
.find( i
);
1054 if( it
!=d_match
.end() ){
1055 if( !getCurrentCanBeEqual( p
, i
, it
->second
) ){
1063 void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c
) {
1064 for( int i
=0; i
<getNumVars(); i
++ ){
1065 Trace(c
) << " " << d_vars
[i
] << " -> ";
1066 if( d_match
.find( i
)!=d_match
.end() ){
1067 Trace(c
) << d_match
[i
];
1069 Trace(c
) << "(unassigned) ";
1071 if( !d_curr_var_deq
[i
].empty() ){
1072 Trace(c
) << ", DEQ{ ";
1073 for( std::map
< Node
, int >::iterator it
= d_curr_var_deq
[i
].begin(); it
!= d_curr_var_deq
[i
].end(); ++it
){
1074 Trace(c
) << it
->first
<< " ";
1078 Trace(c
) << std::endl
;
1083 struct MatchGenSort
{
1084 QuantConflictFind::MatchGen
* d_mg
;
1085 bool operator() (int i
,int j
) {
1086 return d_mg
->d_children
[i
].d_type
<d_mg
->d_children
[j
].d_type
;
1090 QuantConflictFind::MatchGen::MatchGen( QuantConflictFind
* p
, Node q
, Node n
, bool isTop
, bool isVar
){
1091 Trace("qcf-qregister-debug") << "Make match gen for " << n
<< ", top/var = " << isTop
<< " " << isVar
<< std::endl
;
1092 std::vector
< Node
> qni_apps
;
1095 Assert( p
->d_qinfo
[q
].d_var_num
.find( n
)!=p
->d_qinfo
[q
].d_var_num
.end() );
1096 if( n
.getKind()==APPLY_UF
){
1098 d_type_not
= true; //implicit disequality, in disjunction at top level
1100 qni_apps
.push_back( n
);
1102 //for now, unknown term
1103 d_type
= typ_invalid
;
1106 if( isTop
&& n
.getKind()!=OR
&& p
->d_qinfo
[q
].d_vars
.size()>q
[0].getNumChildren() ){
1107 //conjoin extra constraints based on flattening with quantifier body
1108 d_children
.push_back( MatchGen( p
, q
, n
) );
1109 if( d_children
[0].d_type
==typ_invalid
){
1111 d_type
= typ_invalid
;
1116 }else if( quantifiers::TermDb::hasBoundVarAttr( n
) ){
1117 //we handle not immediately
1118 d_n
= n
.getKind()==NOT
? n
[0] : n
;
1119 d_type_not
= n
.getKind()==NOT
;
1120 if( d_n
.getKind()==OR
|| d_n
.getKind()==AND
|| d_n
.getKind()==IFF
|| d_n
.getKind()==ITE
){
1123 for( unsigned i
=0; i
<d_n
.getNumChildren(); i
++ ){
1124 d_children
.push_back( MatchGen( p
, q
, d_n
[i
] ) );
1125 if( d_children
[d_children
.size()-1].d_type
==typ_invalid
){
1126 d_type
= typ_invalid
;
1129 }else if( isTop
&& n
.getKind()==OR
&& d_children
[d_children
.size()-1].d_type
==typ_var_eq
){
1130 Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl
;
1131 //if variable equality/disequality at top level, remove immediately
1132 bool cIsNot
= d_children
[d_children
.size()-1].d_type_not
;
1133 Node cn
= d_children
[d_children
.size()-1].d_n
;
1134 Assert( cn
.getKind()==EQUAL
);
1135 Assert( p
->d_qinfo
[q
].isVar( cn
[0] ) || p
->d_qinfo
[q
].isVar( cn
[1] ) );
1136 //make it a built-in constraint instead
1137 for( unsigned i
=0; i
<2; i
++ ){
1138 if( p
->d_qinfo
[q
].isVar( cn
[i
] ) ){
1139 int v
= p
->d_qinfo
[q
].getVarNum( cn
[i
] );
1140 Node cno
= cn
[i
==0 ? 1 : 0];
1141 p
->d_qinfo
[q
].d_var_constraint
[ cIsNot
? 0 : 1 ][v
].push_back( cno
);
1145 d_children
.pop_back();
1149 d_type
= typ_invalid
;
1151 if( d_n
.getKind()==APPLY_UF
|| d_n
.getKind()==EQUAL
){
1152 //get the applications (in order) that will be matching
1153 p
->getEqRegistryApps( d_n
, qni_apps
);
1154 bool isValid
= true;
1155 if( qni_apps
.size()>0 ){
1156 for( unsigned i
=0; i
<qni_apps
.size(); i
++ ){
1157 if( qni_apps
[i
].getKind()!=APPLY_UF
){
1158 //for now, cannot handle anything besides uf
1165 d_type
= typ_valid_lit
;
1167 }else if( d_n
.getKind()==EQUAL
){
1168 for( unsigned i
=0; i
<2; i
++ ){
1169 if( quantifiers::TermDb::hasBoundVarAttr( d_n
[i
] ) && !p
->d_qinfo
[q
].isVar( d_n
[i
] ) ){
1175 Assert( p
->d_qinfo
[q
].isVar( d_n
[0] ) || p
->d_qinfo
[q
].isVar( d_n
[1] ) );
1176 // variable equality
1177 d_type
= typ_var_eq
;
1183 //we will just evaluate
1185 d_type
= typ_ground
;
1187 if( d_type
!=typ_invalid
){
1188 //determine an efficient children ordering
1189 if( !d_children
.empty() ){
1190 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1191 d_children_order
.push_back( i
);
1193 //if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){
1194 //sort based on the type of the constraint : ground comes first, then literals, then others
1197 //std::sort( d_children_order.begin(), d_children_order.end(), mgs );
1201 int base
= d_children
.size();
1202 //add additional constraints based on flattening
1203 for( unsigned j
=q
[0].getNumChildren(); j
<p
->d_qinfo
[q
].d_vars
.size(); j
++ ){
1204 d_children
.push_back( MatchGen( p
, q
, p
->d_qinfo
[q
].d_vars
[j
], false, true ) );
1207 //choose variable order for variables based on when they are bound
1208 std::vector
< int > varOrder
;
1209 varOrder
.insert( varOrder
.end(), d_children_order
.begin(), d_children_order
.end() );
1210 d_children_order
.clear();
1211 std::map
< int, bool > bound
;
1212 for( unsigned i
=0; i
<varOrder
.size(); i
++ ){
1213 int curr
= varOrder
[i
];
1214 Trace("qcf-qregister-debug") << "Var Order : " << curr
<< std::endl
;
1215 d_children_order
.push_back( curr
);
1216 for( std::map
< int, int >::iterator it
= d_children
[curr
].d_qni_var_num
.begin();
1217 it
!= d_children
[curr
].d_qni_var_num
.end(); ++it
){
1218 if( it
->second
>=(int)q
[0].getNumChildren() && bound
.find( it
->second
)==bound
.end() ){
1219 bound
[ it
->second
] = true;
1220 int var
= base
+ it
->second
- (int)q
[0].getNumChildren();
1221 d_children_order
.push_back( var
);
1222 Trace("qcf-qregister-debug") << "Var Order, bound : " << var
<< std::endl
;
1226 for( unsigned j
=q
[0].getNumChildren(); j
<p
->d_qinfo
[q
].d_vars
.size(); j
++ ){
1227 if( bound
.find( j
)==bound
.end() ){
1228 int var
= base
+ j
- (int)q
[0].getNumChildren();
1229 d_children_order
.push_back( var
);
1230 Trace("qcf-qregister-debug") << "Var Order, remaining : " << j
<< std::endl
;
1236 if( d_type
!=typ_invalid
){
1237 if( !qni_apps
.empty() ){
1238 Trace("qcf-qregister-debug") << "Initialize matching..." << std::endl
;
1239 for( unsigned i
=0; i
<qni_apps
.size(); i
++ ){
1240 for( unsigned j
=0; j
<qni_apps
[i
].getNumChildren(); j
++ ){
1241 Node nn
= qni_apps
[i
][j
];
1242 Trace("qcf-qregister-debug") << " " << d_qni_size
;
1243 if( p
->d_qinfo
[q
].isVar( nn
) ){
1244 Trace("qcf-qregister-debug") << " is var #" << p
->d_qinfo
[q
].d_var_num
[nn
] << std::endl
;
1245 d_qni_var_num
[d_qni_size
] = p
->d_qinfo
[q
].d_var_num
[nn
];
1247 Trace("qcf-qregister-debug") << " is gterm " << nn
<< std::endl
;
1248 d_qni_gterm
[d_qni_size
] = nn
;
1255 Trace("qcf-qregister-debug") << "Done make match gen " << n
<< ", type = ";
1256 debugPrintType( "qcf-qregister-debug", d_type
, true );
1257 Trace("qcf-qregister-debug") << std::endl
;
1258 Assert( d_children
.size()==d_children_order
.size() );
1261 void QuantConflictFind::MatchGen::reset_round( QuantConflictFind
* p
) {
1262 for( std::map
< int, Node
>::iterator it
= d_qni_gterm
.begin(); it
!= d_qni_gterm
.end(); ++it
){
1263 d_qni_gterm_rep
[it
->first
] = p
->getRepresentative( it
->second
);
1265 for( unsigned i
=0; i
<d_children
.size(); i
++ ){
1266 d_children
[i
].reset_round( p
);
1270 void QuantConflictFind::MatchGen::reset( QuantConflictFind
* p
, bool tgt
, Node q
) {
1271 d_tgt
= d_type_not
? !tgt
: tgt
;
1272 Debug("qcf-match") << " Reset for : " << d_n
<< ", type : ";
1273 debugPrintType( "qcf-match", d_type
);
1274 Debug("qcf-match") << ", tgt = " << d_tgt
<< ", children = " << d_children
.size() << std::endl
;
1277 d_qni_bound
.clear();
1278 d_child_counter
= -1;
1280 //set up processing matches
1281 if( d_type
==typ_ground
){
1282 if( p
->evaluate( d_n
)==( d_tgt
? 1 : -1 ) ){
1283 //store dummy variable
1284 d_qn
.push_back( NULL
);
1286 }else if( d_type
==typ_var
){
1287 //check if variable is bound by now
1288 int vi
= p
->d_qinfo
[q
].getVarNum( d_n
);
1290 int repVar
= p
->d_qinfo
[q
].getCurrentRepVar( vi
);
1291 Assert( d_n
.getKind()==APPLY_UF
);
1292 Node f
= d_n
.getOperator();
1293 std::map
< int, Node
>::iterator it
= p
->d_qinfo
[q
].d_match
.find( repVar
);
1294 if( it
!=p
->d_qinfo
[q
].d_match
.end() && d_tgt
) {
1295 Debug("qcf-match") << " will be matching var within eqc = " << it
->second
<< std::endl
;
1296 //f-applications in the equivalence class in match[ repVar ]
1297 std::map
< Node
, QcfNodeIndex
>::iterator itut
= p
->d_eqc_uf_terms
[ it
->second
].find( f
);
1298 if( itut
!=p
->d_eqc_uf_terms
[ it
->second
].end() ){
1299 d_qn
.push_back( &itut
->second
);
1302 Debug("qcf-match") << " will be matching var within any eqc." << std::endl
;
1303 //we are binding rep var
1304 d_qni_bound_cons
[repVar
] = Node::null();
1305 //must look at all f-applications
1306 std::map
< Node
, QcfNodeIndex
>::iterator itut
= p
->d_uf_terms
.find( f
);
1307 if( itut
!=p
->d_uf_terms
.end() ){
1308 d_qn
.push_back( &itut
->second
);
1311 }else if( d_type
==typ_var_eq
){
1312 bool success
= false;
1313 for( unsigned i
=0; i
<2; i
++ ){
1314 int var
= p
->d_qinfo
[q
].getVarNum( d_n
[i
] );
1316 int repVar
= p
->d_qinfo
[q
].getCurrentRepVar( var
);
1317 Node o
= d_n
[ i
==0 ? 1 : 0 ];
1318 o
= p
->d_qinfo
[q
].getCurrentValue( o
);
1319 int vo
= p
->d_qinfo
[q
].getCurrentRepVar( p
->d_qinfo
[q
].getVarNum( o
) );
1320 int addCons
= p
->d_qinfo
[q
].addConstraint( p
, repVar
, o
, vo
, d_tgt
, false );
1321 success
= addCons
!=-1;
1322 //if successful and non-redundant, store that we need to cleanup this
1324 d_qni_bound_cons
[repVar
] = o
;
1325 d_qni_bound
[repVar
] = vo
;
1332 d_qn
.push_back( NULL
);
1334 }else if( d_type
==typ_valid_lit
){
1336 EqRegistry
* er
= p
->getEqRegistry( d_tgt
, d_n
, false );
1338 d_qn
.push_back( &(er
->d_qni
) );
1340 if( d_children
.empty() ){
1342 d_qn
.push_back( NULL
);
1344 //reset the first child to d_tgt
1345 d_child_counter
= 0;
1346 getChild( d_child_counter
)->reset( p
, d_tgt
, q
);
1349 Debug("qcf-match") << " Finished reset for " << d_n
<< ", success = " << ( !d_qn
.empty() || d_child_counter
!=-1 ) << std::endl
;
1352 bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind
* p
, Node q
) {
1353 Debug("qcf-match") << " Get next match for : " << d_n
<< ", type = ";
1354 debugPrintType( "qcf-match", d_type
);
1355 Debug("qcf-match") << ", children = " << d_children
.size() << std::endl
;
1356 if( d_children
.empty() ){
1357 bool success
= doMatching( p
, q
);
1359 for( std::map
< int, Node
>::iterator it
= d_qni_bound_cons
.begin(); it
!= d_qni_bound_cons
.end(); ++it
){
1360 if( !it
->second
.isNull() ){
1361 Debug("qcf-match") << " Clean up bound var " << it
->first
<< (d_tgt
? "!" : "") << " = " << it
->second
<< std::endl
;
1362 std::map
< int, int >::iterator itb
= d_qni_bound
.find( it
->first
);
1363 int vn
= itb
!=d_qni_bound
.end() ? itb
->second
: -1;
1364 p
->d_qinfo
[q
].addConstraint( p
, it
->first
, it
->second
, vn
, d_tgt
, true );
1366 d_qni_bound
.erase( vn
);
1370 d_qni_bound_cons
.clear();
1371 //clean up the match : remove equalities/disequalities
1372 for( std::map
< int, int >::iterator it
= d_qni_bound
.begin(); it
!= d_qni_bound
.end(); ++it
){
1373 Debug("qcf-match") << " Clean up bound var " << it
->second
<< std::endl
;
1374 Assert( it
->second
<p
->d_qinfo
[q
].getNumVars() );
1375 p
->d_qinfo
[q
].d_match
.erase( it
->second
);
1377 d_qni_bound
.clear();
1379 Debug("qcf-match") << " ...finished matching for " << d_n
<< ", success = " << success
<< std::endl
;
1382 if( d_child_counter
!=-1 ){
1383 bool success
= false;
1384 while( !success
&& d_child_counter
>=0 ){
1385 //transition system based on d_child_counter
1386 if( d_type
==typ_top
|| d_n
.getKind()==OR
|| d_n
.getKind()==AND
){
1387 if( (d_n
.getKind()==AND
)==d_tgt
){
1388 //all children must match simultaneously
1389 if( getChild( d_child_counter
)->getNextMatch( p
, q
) ){
1390 if( d_child_counter
<(int)(getNumChildren()-1) ){
1392 Debug("qcf-match-debug") << " Reset child " << d_child_counter
<< " of " << d_n
<< ", all match " << d_children_order
.size() << " " << d_children_order
[d_child_counter
] << std::endl
;
1393 getChild( d_child_counter
)->reset( p
, d_tgt
, q
);
1401 //one child must match
1402 if( !getChild( d_child_counter
)->getNextMatch( p
, q
) ){
1403 if( d_child_counter
<(int)(getNumChildren()-1) ){
1405 Debug("qcf-match-debug") << " Reset child " << d_child_counter
<< " of " << d_n
<< ", one match" << std::endl
;
1406 getChild( d_child_counter
)->reset( p
, d_tgt
, q
);
1408 d_child_counter
= -1;
1414 }else if( d_n
.getKind()==IFF
){
1415 //construct match based on both children
1416 if( d_child_counter
%2==0 ){
1417 if( getChild( 0 )->getNextMatch( p
, q
) ){
1419 getChild( 1 )->reset( p
, d_child_counter
==1, q
);
1421 if( d_child_counter
==0 ){
1422 d_child_counter
= 2;
1423 getChild( 0 )->reset( p
, !d_tgt
, q
);
1425 d_child_counter
= -1;
1429 if( d_child_counter
%2==1 ){
1430 if( getChild( 1 )->getNextMatch( p
, q
) ){
1436 }else if( d_n
.getKind()==ITE
){
1437 if( d_child_counter
%2==0 ){
1438 int index1
= d_child_counter
==4 ? 1 : 0;
1439 if( getChild( index1
)->getNextMatch( p
, q
) ){
1441 getChild( d_child_counter
==5 ? 2 : (d_tgt
==(d_child_counter
==0) ? 1 : 2) )->reset( p
, d_tgt
, q
);
1443 if( d_child_counter
==4 ){
1444 d_child_counter
= -1;
1446 d_child_counter
+=2;
1447 getChild( d_child_counter
==4 ? 1 : 0 )->reset( p
, d_child_counter
==2 ? !d_tgt
: d_tgt
, q
);
1451 if( d_child_counter
%2==1 ){
1452 int index2
= d_child_counter
==5 ? 2 : (d_tgt
==(d_child_counter
==0) ? 1 : 2);
1453 if( getChild( index2
)->getNextMatch( p
, q
) ){
1461 Debug("qcf-match") << " ...finished construct match for " << d_n
<< ", success = " << success
<< std::endl
;
1465 Debug("qcf-match") << " ...already finished for " << d_n
<< std::endl
;
1469 bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind
* p
, Node q
) {
1470 if( !d_qn
.empty() ){
1471 if( d_qn
[0]==NULL
){
1475 Assert( d_qni_size
>0 );
1478 invalidMatch
= false;
1479 Debug("qcf-match-debug") << " Do matching " << d_qn
.size() << " " << d_qni
.size() << std::endl
;
1480 if( d_qn
.size()==d_qni
.size()+1 ) {
1481 int index
= (int)d_qni
.size();
1484 std::map
< int, int >::iterator itv
= d_qni_var_num
.find( index
);
1485 if( itv
!=d_qni_var_num
.end() ){
1486 //get the representative variable this variable is equal to
1487 int repVar
= p
->d_qinfo
[q
].getCurrentRepVar( itv
->second
);
1488 Debug("qcf-match-debug") << " Match " << index
<< " is a variable " << itv
->second
<< ", which is repVar " << repVar
<< std::endl
;
1489 //get the value the rep variable
1490 std::map
< int, Node
>::iterator itm
= p
->d_qinfo
[q
].d_match
.find( repVar
);
1491 if( itm
!=p
->d_qinfo
[q
].d_match
.end() ){
1493 Assert( !val
.isNull() );
1494 Debug("qcf-match-debug") << " Variable is already bound to " << val
<< std::endl
;
1496 //binding a variable
1497 d_qni_bound
[index
] = repVar
;
1498 std::map
< Node
, QcfNodeIndex
>::iterator it
= d_qn
[index
]->d_children
.begin();
1499 if( it
!= d_qn
[index
]->d_children
.end() ) {
1500 d_qni
.push_back( it
);
1502 if( p
->d_qinfo
[q
].setMatch( p
, d_qni_bound
[index
], it
->first
) ){
1503 Debug("qcf-match-debug") << " Binding variable" << std::endl
;
1504 if( d_qn
.size()<d_qni_size
){
1505 d_qn
.push_back( &it
->second
);
1508 Debug("qcf-match") << " Binding variable, currently fail." << std::endl
;
1509 invalidMatch
= true;
1512 Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl
;
1517 Debug("qcf-match-debug") << " Match " << index
<< " is ground term" << std::endl
;
1518 Assert( d_qni_gterm
.find( index
)!=d_qni_gterm
.end() );
1519 Assert( d_qni_gterm_rep
.find( index
)!=d_qni_gterm_rep
.end() );
1520 val
= d_qni_gterm_rep
[index
];
1521 Assert( !val
.isNull() );
1523 if( !val
.isNull() ){
1524 //constrained by val
1525 std::map
< Node
, QcfNodeIndex
>::iterator it
= d_qn
[index
]->d_children
.find( val
);
1526 if( it
!=d_qn
[index
]->d_children
.end() ){
1527 Debug("qcf-match-debug") << " Match" << std::endl
;
1528 d_qni
.push_back( it
);
1529 if( d_qn
.size()<d_qni_size
){
1530 d_qn
.push_back( &it
->second
);
1533 Debug("qcf-match-debug") << " Failed to match" << std::endl
;
1538 Assert( d_qn
.size()==d_qni
.size() );
1539 int index
= d_qni
.size()-1;
1540 //increment if binding this variable
1541 bool success
= false;
1542 std::map
< int, int >::iterator itb
= d_qni_bound
.find( index
);
1543 if( itb
!=d_qni_bound
.end() ){
1545 if( d_qni
[index
]!=d_qn
[index
]->d_children
.end() ){
1547 if( p
->d_qinfo
[q
].setMatch( p
, itb
->second
, d_qni
[index
]->first
) ){
1548 Debug("qcf-match-debug") << " Bind next variable" << std::endl
;
1549 if( d_qn
.size()<d_qni_size
){
1550 d_qn
.push_back( &d_qni
[index
]->second
);
1553 Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl
;
1554 invalidMatch
= true;
1557 Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl
;
1560 //if not incrementing, move to next
1566 if( d_type
==typ_var
){
1567 if( !invalidMatch
&& d_qni
.size()==d_qni_size
){
1568 //if in the act of binding the variable by this term, bind the variable
1569 std::map
< int, Node
>::iterator itb
= d_qni_bound_cons
.begin();
1570 if( itb
!=d_qni_bound_cons
.end() ){
1571 QcfNodeIndex
* v_qni
= &d_qni
[d_qni
.size()-1]->second
;
1572 Assert( v_qni
->d_children
.begin()!=v_qni
->d_children
.end() );
1573 Node vb
= v_qni
->d_children
.begin()->first
;
1574 Assert( !vb
.isNull() );
1575 vb
= p
->getRepresentative( vb
);
1576 Debug("qcf-match-debug") << " For var, require binding " << itb
->first
<< " to " << vb
<< ", d_tgt = " << d_tgt
<< std::endl
;
1577 if( !itb
->second
.isNull() ){
1578 p
->d_qinfo
[q
].addConstraint( p
, itb
->first
, itb
->second
, -1, d_tgt
, true );
1580 int addCons
= p
->d_qinfo
[q
].addConstraint( p
, itb
->first
, vb
, -1, d_tgt
, false );
1582 Debug("qcf-match-debug") << " Failed set for var." << std::endl
;
1583 invalidMatch
= true;
1584 d_qni_bound_cons
[itb
->first
] = Node::null();
1586 Debug("qcf-match-debug") << " Succeeded set for var." << std::endl
;
1588 d_qni_bound_cons
[itb
->first
] = vb
;
1594 }while( ( !d_qn
.empty() && d_qni
.size()!=d_qni_size
) || invalidMatch
);
1597 return !d_qn
.empty();
1600 void QuantConflictFind::MatchGen::debugPrintType( const char * c
, short typ
, bool isTrace
) {
1603 case typ_invalid
: Trace(c
) << "invalid";break;
1604 case typ_ground
: Trace(c
) << "ground";break;
1605 case typ_valid_lit
: Trace(c
) << "valid_lit";break;
1606 case typ_valid
: Trace(c
) << "valid";break;
1607 case typ_var
: Trace(c
) << "var";break;
1608 case typ_var_eq
: Trace(c
) << "var_eq";break;
1609 case typ_top
: Trace(c
) << "top";break;
1613 case typ_invalid
: Debug(c
) << "invalid";break;
1614 case typ_ground
: Debug(c
) << "ground";break;
1615 case typ_valid_lit
: Debug(c
) << "valid_lit";break;
1616 case typ_valid
: Debug(c
) << "valid";break;
1617 case typ_var
: Debug(c
) << "var";break;
1618 case typ_var_eq
: Debug(c
) << "var_eq";break;
1619 case typ_top
: Debug(c
) << "top";break;
1625 //-------------------------------------------------- debugging
1628 void QuantConflictFind::debugPrint( const char * c
) {
1629 //print the equivalance classes
1630 Trace(c
) << "----------EQ classes" << std::endl
;
1631 eq::EqClassesIterator eqcs_i
= eq::EqClassesIterator( getEqualityEngine() );
1632 while( !eqcs_i
.isFinished() ){
1634 if( !n
.getType().isInteger() ){
1635 Trace(c
) << " - " << n
<< " : {";
1636 eq::EqClassIterator eqc_i
= eq::EqClassIterator( n
, getEqualityEngine() );
1638 while( !eqc_i
.isFinished() ){
1640 if( nn
.getKind()!=EQUAL
&& nn
!=n
){
1641 Trace(c
) << (pr
? "," : "" ) << " " << nn
;
1646 Trace(c
) << (pr
? " " : "" ) << "}" << std::endl
;
1647 EqcInfo
* eqcn
= getEqcInfo( n
, false );
1649 Trace(c
) << " DEQ : {";
1651 for( NodeBoolMap::iterator it
= eqcn
->d_diseq
.begin(); it
!= eqcn
->d_diseq
.end(); ++it
){
1653 Trace(c
) << (pr
? "," : "" ) << " " << (*it
).first
;
1657 Trace(c
) << (pr
? " " : "" ) << "}" << std::endl
;
1662 std::map
< Node
, std::map
< Node
, bool > > printed
;
1663 //print the equality registries
1664 for( unsigned i
=0; i
<2; i
++ ){
1666 Trace(c
) << "----------EQR, polarity = " << (i
==0) << std::endl
;
1667 for( std::map
< Node
, std::map
< Node
, EqRegistry
* > >::iterator it
= d_eqr
[i
].begin(); it
!= d_eqr
[i
].end(); ++it
){
1668 bool prHead
= false;
1669 for( std::map
< Node
, EqRegistry
* >::iterator it2
= it
->second
.begin(); it2
!= it
->second
.end(); ++it2
){
1671 if( it
->first
.getKind()==APPLY_UF
&& it2
->first
.getKind()==APPLY_UF
&&
1672 it
->first
.getOperator()!=it2
->first
.getOperator() ){
1673 print
= isLessThan( it
->first
, it2
->first
);
1675 print
= printed
[it
->first
].find( it2
->first
)==printed
[it
->first
].end();
1678 printed
[it
->first
][it2
->first
] = true;
1679 printed
[it2
->first
][it
->first
] = true;
1681 Trace(c
) << "- " << it
->first
<< std::endl
;
1684 Trace(c
) << " " << it2
->first
<< ", terms : " << std::endl
;
1687 Trace(c) << " " << it2->first << " : {";
1689 for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){
1690 if( (*it3).second ){
1691 Trace(c) << (pr ? "," : "" ) << " " << (*it3).first;
1695 Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
1697 //print qni structure
1698 it2
->second
->debugPrint( c
, 3 );
1705 void QuantConflictFind::debugPrintQuant( const char * c
, Node q
) {
1706 Trace(c
) << "Q" << d_quant_id
[q
];
1709 void QuantConflictFind::debugPrintQuantBody( const char * c
, Node q
, Node n
, bool doVarNum
) {
1710 if( n
.getNumChildren()==0 ){
1712 }else if( doVarNum
&& d_qinfo
[q
].d_var_num
.find( n
)!=d_qinfo
[q
].d_var_num
.end() ){
1713 Trace(c
) << "?x" << d_qinfo
[q
].d_var_num
[n
];
1716 if( n
.getKind()==APPLY_UF
){
1717 Trace(c
) << n
.getOperator();
1719 Trace(c
) << n
.getKind();
1721 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1723 debugPrintQuantBody( c
, q
, n
[i
] );
1729 QuantConflictFind::Statistics::Statistics():
1730 d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
1731 d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 )
1733 StatisticsRegistry::registerStat(&d_inst_rounds
);
1734 StatisticsRegistry::registerStat(&d_conflict_inst
);
1737 QuantConflictFind::Statistics::~Statistics(){
1738 StatisticsRegistry::unregisterStat(&d_inst_rounds
);
1739 StatisticsRegistry::unregisterStat(&d_conflict_inst
);