--- /dev/null
+/********************* */\r
+/*! \file quant_conflict_find.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief quant conflict find class\r
+ **\r
+ **/\r
+\r
+#include <vector>\r
+\r
+#include "theory/quantifiers/quant_conflict_find.h"\r
+#include "theory/quantifiers/quant_util.h"\r
+#include "theory/theory_engine.h"\r
+\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace std;\r
+\r
+namespace CVC4 {\r
+\r
+Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, bool doAdd, int index ) {\r
+ if( index==(int)n.getNumChildren() ){\r
+ if( d_children.empty() ){\r
+ if( doAdd ){\r
+ d_children[ n ].clear();\r
+ return n;\r
+ }else{\r
+ return Node::null();\r
+ }\r
+ }else{\r
+ return d_children.begin()->first;\r
+ }\r
+ }else{\r
+ Node r = qcf->getRepresentative( n[index] );\r
+ return d_children[r].addTerm( qcf, n, doAdd, index+1 );\r
+ }\r
+}\r
+\r
+bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index ) {\r
+ if( index==(int)n1.getNumChildren() ){\r
+ Node n = addTerm( qcf, n2 );\r
+ return n==n2;\r
+ }else{\r
+ Node r = qcf->getRepresentative( n1[index] );\r
+ return d_children[r].addTermEq( qcf, n1, n2, index+1 );\r
+ }\r
+}\r
+\r
+void QcfNodeIndex::debugPrint( const char * c, int t ) {\r
+ for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){\r
+ if( !it->first.isNull() ){\r
+ for( int j=0; j<t; j++ ){ Trace(c) << " "; }\r
+ Trace(c) << it->first << " : " << std::endl;\r
+ it->second.debugPrint( c, t+1 );\r
+ }\r
+ }\r
+}\r
+\r
+EqRegistry::EqRegistry( context::Context* c ) : d_active( c, false ){//: d_t_eqc( c ){\r
+\r
+}\r
+\r
+void EqRegistry::debugPrint( const char * c, int t ) {\r
+ d_qni.debugPrint( c, t );\r
+}\r
+\r
+//QcfNode::QcfNode( context::Context* c ) : d_parent( NULL ){\r
+// d_reg[0] = NULL;\r
+// d_reg[1] = NULL;\r
+//}\r
+\r
+QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :\r
+QuantifiersModule( qe ),\r
+d_c( c ),\r
+d_conflict( c, false ),\r
+d_qassert( c ) {\r
+ d_fid_count = 0;\r
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);\r
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);\r
+ getFunctionId( d_true );\r
+ getFunctionId( d_false );\r
+}\r
+\r
+int QuantConflictFind::getFunctionId( Node f ) {\r
+ std::map< Node, int >::iterator it = d_fid.find( f );\r
+ if( it==d_fid.end() ){\r
+ d_fid[f] = d_fid_count;\r
+ d_fid_count++;\r
+ return d_fid[f];\r
+ }\r
+ return it->second;\r
+}\r
+\r
+bool QuantConflictFind::isLessThan( Node a, Node b ) {\r
+ Assert( a.getKind()==APPLY_UF );\r
+ Assert( b.getKind()==APPLY_UF );\r
+ /*\r
+ if( a.getOperator()==b.getOperator() ){\r
+ for( unsigned i=0; i<a.getNumChildren(); i++ ){\r
+ Node acr = getRepresentative( a[i] );\r
+ Node bcr = getRepresentative( b[i] );\r
+ if( acr<bcr ){\r
+ return true;\r
+ }else if( acr>bcr ){\r
+ return false;\r
+ }\r
+ }\r
+ return false;\r
+ }else{\r
+ */\r
+ return getFunctionId( a.getOperator() )<getFunctionId( b.getOperator() );\r
+ //}\r
+}\r
+\r
+Node QuantConflictFind::getFunction( Node n, bool isQuant ) {\r
+ if( isQuant && !quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ return n;\r
+ }else if( n.getKind()==APPLY_UF ){\r
+ std::map< Node, Node >::iterator it = d_op_node.find( n.getOperator() );\r
+ if( it==d_op_node.end() ){\r
+ std::vector< Node > children;\r
+ children.push_back( n.getOperator() );\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ children.push_back( getFv( n[i].getType() ) );\r
+ }\r
+ Node nn = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ d_op_node[n.getOperator()] = nn;\r
+ return nn;\r
+ }else{\r
+ return it->second;\r
+ }\r
+ }else{\r
+ //should be a variable\r
+ return Node::null();\r
+ }\r
+}\r
+\r
+Node QuantConflictFind::getFv( TypeNode tn ) {\r
+ if( d_fv.find( tn )==d_fv.end() ){\r
+ std::stringstream ss;\r
+ ss << "_u";\r
+ d_fv[tn] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is for QCF" );\r
+ }\r
+ return d_fv[tn];\r
+}\r
+\r
+Node QuantConflictFind::mkEqNode( Node a, Node b ) {\r
+ if( a.getType().isBoolean() ){\r
+ return a.iffNode( b );\r
+ }else{\r
+ return a.eqNode( b );\r
+ }\r
+}\r
+\r
+//-------------------------------------------------- registration\r
+\r
+/*\r
+void QuantConflictFind::registerAssertions( std::vector< Node >& assertions ) {\r
+ for( unsigned i=0; i<assertions.size(); i++ ){\r
+ registerAssertion( assertions[i] );\r
+ }\r
+}\r
+\r
+void QuantConflictFind::registerAssertion( Node n ) {\r
+ if( n.getKind()==FORALL ){\r
+ registerQuant( Node::null(), n[1], NULL, true, true );\r
+ }else{\r
+ if( n.getType().isBoolean() ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ registerAssertion( n[i] );\r
+ }\r
+ }\r
+ }\r
+}\r
+*/\r
+void QuantConflictFind::registerQuant( Node q, Node n, bool hasPol, bool pol ) {\r
+ //qcf->d_node = n;\r
+ bool recurse = true;\r
+ if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=ITE && n.getKind()!=NOT ){\r
+ if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ //literals\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( !hasPol || ( pol!=(i==0) ) ){\r
+ EqRegistry * eqr = getEqRegistry( i==0, n );\r
+ if( eqr ){\r
+ d_qinfo[q].d_rel_eqr[ eqr ] = true;\r
+ }\r
+ }\r
+ }\r
+ if( n.getKind()==APPLY_UF ||\r
+ ( n.getKind()==EQUAL && ( n[0].getKind()==BOUND_VARIABLE || n[1].getKind()==BOUND_VARIABLE ) ) ){\r
+ flatten( q, n );\r
+ }else{\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( q, n[i] );\r
+ }\r
+ }\r
+ }else{\r
+ Trace("qcf-qregister") << " RegisterGroundLit : " << n;\r
+ }\r
+ recurse = false;\r
+ }\r
+ if( recurse ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ bool newHasPol;\r
+ bool newPol;\r
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
+ //QcfNode * qcfc = new QcfNode( d_c );\r
+ //qcfc->d_parent = qcf;\r
+ //qcf->d_child[i] = qcfc;\r
+ registerQuant( q, n[i], newHasPol, newPol );\r
+ }\r
+ }\r
+}\r
+\r
+void QuantConflictFind::flatten( Node q, Node n ) {\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ if( quantifiers::TermDb::hasBoundVarAttr( n[i] ) && n.getKind()!=BOUND_VARIABLE ){\r
+ if( d_qinfo[q].d_var_num.find( n[i] )==d_qinfo[q].d_var_num.end() ){\r
+ //Trace("qcf-qregister") << " Flatten term " << n[i] << std::endl;\r
+ d_qinfo[q].d_var_num[n[i]] = d_qinfo[q].d_vars.size();\r
+ d_qinfo[q].d_vars.push_back( n[i] );\r
+ flatten( q, n[i] );\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void QuantConflictFind::registerQuantifier( Node q ) {\r
+ d_quants.push_back( q );\r
+ d_quant_id[q] = d_quants.size();\r
+ Trace("qcf-qregister") << "Register ";\r
+ debugPrintQuant( "qcf-qregister", q );\r
+ Trace("qcf-qregister") << " : " << q << std::endl;\r
+\r
+ //register the variables\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ d_qinfo[q].d_var_num[q[0][i]] = i;\r
+ d_qinfo[q].d_vars.push_back( q[0][i] );\r
+ }\r
+\r
+ //make QcfNode structure\r
+ Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;\r
+ //d_qinfo[q].d_cf = new QcfNode( d_c );\r
+ registerQuant( q, q[1], true, true );\r
+\r
+ //debug print\r
+ Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;\r
+ Trace("qcf-qregister") << " ";\r
+ debugPrintQuantBody( "qcf-qregister", q, q[1] );\r
+ Trace("qcf-qregister") << std::endl;\r
+ if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
+ Trace("qcf-qregister") << " with additional constraints : " << std::endl;\r
+ for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){\r
+ Trace("qcf-qregister") << " ?x" << j << " = ";\r
+ debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );\r
+ Trace("qcf-qregister") << std::endl;\r
+ }\r
+ }\r
+\r
+ Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;\r
+ d_qinfo[q].d_mg = new MatchGen( this, q, q[1], true );\r
+\r
+ Trace("qcf-qregister") << "Done registering quantifier." << std::endl;\r
+}\r
+\r
+EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doCreate ) {\r
+ Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\r
+ int i;\r
+ Node f1;\r
+ Node f2;\r
+ if( lit.getKind()==EQUAL ){\r
+ i = polarity ? 0 : 1;\r
+ f1 = getFunction( lit[0], true );\r
+ f2 = getFunction( lit[1], true );\r
+ }else if( lit.getKind()==APPLY_UF ){\r
+ i = 0;\r
+ f1 = getFunction( lit, true );\r
+ f2 = polarity ? d_true : d_false;\r
+ }\r
+ if( !f1.isNull() && !f2.isNull() ){\r
+ if( d_eqr[i][f1].find( f2 )==d_eqr[i][f1].end() ){\r
+ if( doCreate ){\r
+ Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << std::endl;\r
+ d_eqr[i][f1][f2] = new EqRegistry( d_c );\r
+ d_eqr[i][f2][f1] = d_eqr[i][f1][f2];\r
+ }else{\r
+ return NULL;\r
+ }\r
+ }\r
+ return d_eqr[i][f1][f2];\r
+ }else{\r
+ return NULL;\r
+ }\r
+}\r
+\r
+void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) {\r
+ Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) );\r
+ if( lit.getKind()==EQUAL ){\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){\r
+ if( lit[i].getKind()==APPLY_UF ){\r
+ terms.push_back( lit[i] );\r
+ }else if( lit[i].getKind()==BOUND_VARIABLE ){\r
+ //do not handle variable equalities\r
+ terms.clear();\r
+ return;\r
+ }\r
+ }\r
+ }\r
+ if( terms.size()==2 && isLessThan( terms[1], terms[0] ) ){\r
+ Node t = terms[0];\r
+ terms[0] = terms[1];\r
+ terms[1] = t;\r
+ }\r
+ }else if( lit.getKind()==APPLY_UF ){\r
+ terms.push_back( lit );\r
+ }\r
+}\r
+\r
+int QuantConflictFind::evaluate( Node n ) {\r
+ int ret = 0;\r
+ if( n.getKind()==EQUAL ){\r
+ Node n1 = getTerm( n[0] );\r
+ Node n2 = getTerm( n[1] );\r
+ Debug("qcf-eval") << "Evaluate : Normalize " << n << " to " << n1 << " = " << n2 << std::endl;\r
+ if( areEqual( n1, n2 ) ){\r
+ ret = 1;\r
+ }else if( areDisequal( n1, n2 ) ){\r
+ ret = -1;\r
+ }\r
+ }else if( n.getKind()==APPLY_UF ){\r
+ Node nn = getTerm( n );\r
+ Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl;\r
+ if( areEqual( nn, d_true ) ){\r
+ ret = 1;\r
+ }else if( areEqual( nn, d_false ) ){\r
+ ret = -1;\r
+ }\r
+ }else if( n.getKind()==NOT ){\r
+ return -evaluate( n[0] );\r
+ }else if( n.getKind()==ITE ){\r
+ int cev1 = evaluate( n[0] );\r
+ int cevc[2] = { 0, 0 };\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( ( i==0 && cev1!=-1 ) || ( i==1 && cev1!=1 ) ){\r
+ cevc[i] = evaluate( n[i+1] );\r
+ if( cev1!=0 ){\r
+ ret = cevc[i];\r
+ break;\r
+ }else if( cevc[i]==0 ){\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ if( ret==0 && cevc[0]!=0 && cevc[0]==cevc[1] ){\r
+ ret = cevc[0];\r
+ }\r
+ }else if( n.getKind()==IFF ){\r
+ int cev1 = evaluate( n[0] );\r
+ if( cev1!=0 ){\r
+ int cev2 = evaluate( n[1] );\r
+ if( cev2!=0 ){\r
+ ret = cev1==cev2 ? 1 : -1;\r
+ }\r
+ }\r
+\r
+ }else{\r
+ int ssval = 0;\r
+ if( n.getKind()==OR ){\r
+ ssval = 1;\r
+ }else if( n.getKind()==AND ){\r
+ ssval = -1;\r
+ }\r
+ bool isUnk = false;\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ int cev = evaluate( n[i] );\r
+ if( cev==ssval ){\r
+ ret = ssval;\r
+ break;\r
+ }else if( cev==0 ){\r
+ isUnk = true;\r
+ }\r
+ }\r
+ if( ret==0 && !isUnk ){\r
+ ret = -ssval;\r
+ }\r
+ }\r
+ Debug("qcf-eval") << "Evaluate " << n << " to " << ret << std::endl;\r
+ return ret;\r
+}\r
+\r
+//-------------------------------------------------- handling assertions / eqc\r
+\r
+void QuantConflictFind::assertNode( Node q ) {\r
+ Trace("qcf-proc") << "QCF : assertQuantifier : ";\r
+ debugPrintQuant("qcf-proc", q);\r
+ Trace("qcf-proc") << std::endl;\r
+ d_qassert.push_back( q );\r
+ //set the eqRegistries that this depends on to true\r
+ for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){\r
+ it->first->d_active.set( true );\r
+ }\r
+}\r
+\r
+eq::EqualityEngine * QuantConflictFind::getEqualityEngine() {\r
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( theory::THEORY_UF ))->getEqualityEngine();\r
+ return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();\r
+}\r
+bool QuantConflictFind::areEqual( Node n1, Node n2 ) {\r
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areEqual( n1,n2 );\r
+}\r
+bool QuantConflictFind::areDisequal( Node n1, Node n2 ) {\r
+ return getEqualityEngine()->hasTerm( n1 ) && getEqualityEngine()->hasTerm( n2 ) && getEqualityEngine()->areDisequal( n1,n2, false );\r
+}\r
+Node QuantConflictFind::getRepresentative( Node n ) {\r
+ if( getEqualityEngine()->hasTerm( n ) ){\r
+ return getEqualityEngine()->getRepresentative( n );\r
+ }else{\r
+ return n;\r
+ }\r
+}\r
+Node QuantConflictFind::getTerm( Node n ) {\r
+ if( n.getKind()==APPLY_UF ){\r
+ Node nn = d_uf_terms[n.getOperator()].addTerm( this, n, false );\r
+ if( !nn.isNull() ){\r
+ return nn;\r
+ }\r
+ }\r
+ return n;\r
+}\r
+\r
+QuantConflictFind::EqcInfo * QuantConflictFind::getEqcInfo( Node n, bool doCreate ) {\r
+ /*\r
+ NodeBoolMap::iterator it = d_eqc.find( n );\r
+ if( it==d_eqc.end() ){\r
+ if( doCreate ){\r
+ d_eqc[n] = true;\r
+ }else{\r
+ //equivalence class does not currently exist\r
+ return NULL;\r
+ }\r
+ }else{\r
+ //should only ask for valid equivalence classes\r
+ Assert( (*it).second );\r
+ }\r
+ */\r
+ std::map< Node, EqcInfo * >::iterator it2 = d_eqc_info.find( n );\r
+ if( it2==d_eqc_info.end() ){\r
+ if( doCreate ){\r
+ EqcInfo * eqci = new EqcInfo( d_c );\r
+ d_eqc_info[n] = eqci;\r
+ return eqci;\r
+ }else{\r
+ return NULL;\r
+ }\r
+ }\r
+ return it2->second;\r
+}\r
+\r
+/** new node */\r
+void QuantConflictFind::newEqClass( Node n ) {\r
+ Trace("qcf-proc-debug") << "QCF : newEqClass : " << n << std::endl;\r
+\r
+ Trace("qcf-proc2-debug") << "QCF : finished newEqClass : " << n << std::endl;\r
+}\r
+\r
+/** merge */\r
+void QuantConflictFind::merge( Node a, Node b ) {\r
+ if( b.getKind()==EQUAL ){\r
+ if( a==d_true ){\r
+ //will merge anyways\r
+ //merge( b[0], b[1] );\r
+ }else if( a==d_false ){\r
+ assertDisequal( b[0], b[1] );\r
+ }\r
+ }else{\r
+ Trace("qcf-proc") << "QCF : merge : " << a << " " << b << std::endl;\r
+ EqcInfo * eqc_b = getEqcInfo( b, false );\r
+ EqcInfo * eqc_a = NULL;\r
+ if( eqc_b ){\r
+ eqc_a = getEqcInfo( a );\r
+ //move disequalities of b into a\r
+ for( NodeBoolMap::iterator it = eqc_b->d_diseq.begin(); it != eqc_b->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ Node n = (*it).first;\r
+ EqcInfo * eqc_n = getEqcInfo( n, false );\r
+ Assert( eqc_n );\r
+ if( !eqc_n->isDisequal( a ) ){\r
+ Assert( !eqc_a->isDisequal( n ) );\r
+ eqc_n->setDisequal( a );\r
+ eqc_a->setDisequal( n );\r
+ //setEqual( eqc_a, eqc_b, a, n, false );\r
+ }\r
+ eqc_n->setDisequal( b, false );\r
+ }\r
+ }\r
+ /*\r
+ //move all previous EqcRegistry's regarding equalities within b\r
+ for( NodeBoolMap::iterator it = eqc_b->d_rel_eqr_e.begin(); it != eqc_b->d_rel_eqr_e.end(); ++it ){\r
+ if( (*it).second ){\r
+ eqc_a->d_rel_eqr_e[(*it).first] = true;\r
+ }\r
+ }\r
+ */\r
+ }\r
+ //process new equalities\r
+ //setEqual( eqc_a, eqc_b, a, b, true );\r
+ Trace("qcf-proc2") << "QCF : finished merge : " << a << " " << b << std::endl;\r
+ }\r
+}\r
+\r
+/** assert disequal */\r
+void QuantConflictFind::assertDisequal( Node a, Node b ) {\r
+ a = getRepresentative( a );\r
+ b = getRepresentative( b );\r
+ Trace("qcf-proc") << "QCF : assert disequal : " << a << " " << b << std::endl;\r
+ EqcInfo * eqc_a = getEqcInfo( a );\r
+ EqcInfo * eqc_b = getEqcInfo( b );\r
+ if( !eqc_a->isDisequal( b ) ){\r
+ Assert( !eqc_b->isDisequal( a ) );\r
+ eqc_b->setDisequal( a );\r
+ eqc_a->setDisequal( b );\r
+ //setEqual( eqc_a, eqc_b, a, b, false );\r
+ }\r
+ Trace("qcf-proc2") << "QCF : finished assert disequal : " << a << " " << b << std::endl;\r
+}\r
+\r
+//-------------------------------------------------- check function\r
+\r
+/** check */\r
+void QuantConflictFind::check( Theory::Effort level ) {\r
+ Trace("qcf-check") << "QCF : check : " << level << std::endl;\r
+ if( d_conflict ){\r
+ Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;\r
+ }else{\r
+ bool addedLemma = false;\r
+ if( level==Theory::EFFORT_FULL ){\r
+ double clSet = 0;\r
+ if( Trace.isOn("qcf-engine") ){\r
+ clSet = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;\r
+ }\r
+ Trace("qcf-check") << "Compute relevant equalities..." << std::endl;\r
+ computeRelevantEqr();\r
+\r
+ Trace("qcf-debug") << std::endl;\r
+ debugPrint("qcf-debug");\r
+ Trace("qcf-debug") << std::endl;\r
+\r
+\r
+ Trace("qcf-check") << "Checking quantified formulas..." << std::endl;\r
+ for( unsigned j=0; j<d_qassert.size(); j++ ){\r
+ Node q = d_qassert[j];\r
+ Trace("qcf-check") << "Check quantified formula ";\r
+ debugPrintQuant("qcf-check", q);\r
+ Trace("qcf-check") << " : " << q << "..." << std::endl;\r
+\r
+ Assert( d_qinfo.find( q )!=d_qinfo.end() );\r
+ if( d_qinfo[q].d_mg->isValid() ){\r
+ d_qinfo[q].reset_round( this );\r
+ //try to make a matches making the body false\r
+ d_qinfo[q].d_mg->reset( this, false, q );\r
+ while( d_qinfo[q].d_mg->getNextMatch( this, q ) ){\r
+\r
+ Trace("qcf-check") << "*** Produced match : " << std::endl;\r
+ d_qinfo[q].debugPrintMatch("qcf-check");\r
+ Trace("qcf-check") << std::endl;\r
+\r
+ if( !d_qinfo[q].isMatchSpurious( this ) ){\r
+ //assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
+ Trace("qcf-check") << std::endl;\r
+ std::vector< int > unassigned;\r
+ std::vector< TypeNode > unassigned_tn;\r
+ for( int i=0; i<d_qinfo[q].getNumVars(); i++ ){\r
+ if( d_qinfo[q].d_match.find( i )==d_qinfo[q].d_match.end() ){\r
+ Assert( i<(int)q[0].getNumChildren() );\r
+ unassigned.push_back( i );\r
+ unassigned_tn.push_back( d_qinfo[q].getVar( i ).getType() );\r
+ }\r
+ }\r
+ bool success = true;\r
+ if( !unassigned.empty() ){\r
+ Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
+ int index = 0;\r
+ std::vector< int > eqc_count;\r
+ do {\r
+ bool invalidMatch;\r
+ while( ( index>=0 && (int)index<(int)unassigned.size() ) || invalidMatch ){\r
+ invalidMatch = false;\r
+ if( index==(int)eqc_count.size() ){\r
+ eqc_count.push_back( 0 );\r
+ }else{\r
+ Assert( index==(int)eqc_count.size()-1 );\r
+ if( eqc_count[index]<(int)d_eqcs[unassigned_tn[index]].size() ){\r
+ int currIndex = eqc_count[index];\r
+ eqc_count[index]++;\r
+ Trace("qcf-check-unassign") << unassigned[index] << "->" << d_eqcs[unassigned_tn[index]][currIndex] << std::endl;\r
+ if( d_qinfo[q].setMatch( this, unassigned[index], d_eqcs[unassigned_tn[index]][currIndex] ) ){\r
+ Trace("qcf-check-unassign") << "Succeeded match" << std::endl;\r
+ index++;\r
+ }else{\r
+ Trace("qcf-check-unassign") << "Failed match" << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Trace("qcf-check-unassign") << "No more matches" << std::endl;\r
+ eqc_count.pop_back();\r
+ index--;\r
+ }\r
+ }\r
+ }\r
+ success = index>=0;\r
+ if( success ){\r
+ index = (int)unassigned.size()-1;\r
+ Trace("qcf-check-unassign") << " Try: " << std::endl;\r
+ for( unsigned i=0; i<unassigned.size(); i++ ){\r
+ int ui = unassigned[i];\r
+ Trace("qcf-check-unassign") << " Assigned #" << ui << " : " << d_qinfo[q].d_vars[ui] << " -> " << d_qinfo[q].d_match[ui] << std::endl;\r
+ }\r
+ }\r
+ }while( success && d_qinfo[q].isMatchSpurious( this ) );\r
+ }\r
+\r
+ if( success ){\r
+ InstMatch m;\r
+ for( unsigned i=0; i<q[0].getNumChildren(); i++ ){\r
+ Node cv = d_qinfo[q].getCurrentValue( d_qinfo[q].d_match[i] );\r
+ Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_qinfo[q].d_match[i] << std::endl;\r
+ m.set( d_quantEngine, q, i, cv );\r
+ }\r
+ if( Debug.isOn("qcf-check-inst") ){\r
+ Node inst = d_quantEngine->getInstantiation( q, m );\r
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+ Assert( evaluate( inst )==-1 );\r
+ }\r
+ if( d_quantEngine->addInstantiation( q, m ) ){\r
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
+ d_quantEngine->flushLemmas();\r
+ d_conflict.set( true );\r
+ addedLemma = true;\r
+ break;\r
+ }else{\r
+ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
+ Assert( false );\r
+ }\r
+ }else{\r
+ Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
+ }\r
+ for( unsigned i=0; i<unassigned.size(); i++ ){\r
+ d_qinfo[q].d_match.erase( unassigned[i] );\r
+ }\r
+ }else{\r
+ Trace("qcf-check") << " ... Spurious instantiation (does not meet variable constraints)" << std::endl;\r
+ }\r
+ }\r
+ }\r
+ if( addedLemma ){\r
+ break;\r
+ }\r
+ }\r
+ if( Trace.isOn("qcf-engine") ){\r
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);\r
+ Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet) << ", addedLemma = " << addedLemma << std::endl;\r
+ }\r
+ }\r
+ Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
+ }\r
+}\r
+\r
+bool QuantConflictFind::needsCheck( Theory::Effort level ) {\r
+ return !d_conflict && level==Theory::EFFORT_FULL;\r
+}\r
+\r
+void QuantConflictFind::computeRelevantEqr() {\r
+ //first, reset information\r
+ for( unsigned i=0; i<2; i++ ){\r
+ for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){\r
+ for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ it2->second->clear();\r
+ }\r
+ }\r
+ }\r
+ d_uf_terms.clear();\r
+ d_eqc_uf_terms.clear();\r
+ d_eqcs.clear();\r
+\r
+ //which nodes are irrelevant for disequality matches\r
+ std::map< Node, bool > irrelevant_dnode;\r
+ //which eqc we have processed\r
+ std::map< Node, bool > process_eqc;\r
+ //now, store matches\r
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
+ while( !eqcs_i.isFinished() ){\r
+ Node r = (*eqcs_i);\r
+ d_eqcs[r.getType()].push_back( r );\r
+ EqcInfo * eqcir = getEqcInfo( r, false );\r
+ //get relevant nodes that we are disequal from\r
+ std::vector< Node > deqc;\r
+ if( eqcir ){\r
+ for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ Node rd = (*it).first;\r
+ //if we have processed the other direction\r
+ if( process_eqc.find( rd )!=process_eqc.end() ){\r
+ eq::EqClassIterator eqcd_i = eq::EqClassIterator( rd, getEqualityEngine() );\r
+ while( !eqcd_i.isFinished() ){\r
+ Node nd = (*eqcd_i);\r
+ if( irrelevant_dnode.find( nd )==irrelevant_dnode.end() ){\r
+ deqc.push_back( nd );\r
+ }\r
+ ++eqcd_i;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ //the relevant nodes in this eqc\r
+ std::vector< Node > eqc;\r
+ //process disequalities\r
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
+ while( !eqc_i.isFinished() ){\r
+ Node n = (*eqc_i);\r
+ bool isRedundant;\r
+ if( n.getKind()==APPLY_UF ){\r
+ Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( this, n );\r
+ isRedundant = (nadd!=n);\r
+ d_uf_terms[n.getOperator()].addTerm( this, n );\r
+ }else{\r
+ isRedundant = false;\r
+ }\r
+ //process all relevant equalities and disequalities to n\r
+ for( unsigned index=0; index<2; index++ ){\r
+ std::map< Node, std::map< Node, EqRegistry * > >::iterator itn[2];\r
+ itn[0] = d_eqr[index].find( n );\r
+ Node fn;\r
+ if( n.getKind()==APPLY_UF && !isRedundant ){\r
+ fn = getFunction( n );\r
+ itn[1] = d_eqr[index].find( fn );\r
+ }\r
+ //for n, fn...\r
+ bool relevant = false;\r
+ for( unsigned j=0; j<2; j++ ){\r
+ //if this node is relevant as an ground term or f-application\r
+ if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index].end() ){\r
+ relevant = true;\r
+ std::vector< Node >& rel_nodes = index==0 ? eqc : deqc;\r
+ for( unsigned i=0; i<rel_nodes.size(); i++ ){\r
+ Node m = rel_nodes[i];\r
+ Node fm;\r
+ if( m.getKind()==APPLY_UF ){\r
+ fm = getFunction( m );\r
+ }\r
+ //process equality/disequality\r
+ if( j==1 ){\r
+ //fn with m\r
+ std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( m );\r
+ if( itm!=itn[j]->second.end() ){\r
+ if( itm->second->d_qni.addTerm( this, n )==n ){\r
+ Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
+ Trace("qcf-reqr") << fn << " " << m << std::endl;\r
+ }\r
+ }\r
+ }\r
+ if( !fm.isNull() ){\r
+ std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm );\r
+ if( itm!=itn[j]->second.end() ){\r
+ if( j==0 ){\r
+ //n with fm\r
+ if( itm->second->d_qni.addTerm( this, m )==m ){\r
+ Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for ";\r
+ Trace("qcf-reqr") << n << " " << fm << std::endl;\r
+ }\r
+ }else{\r
+ //fn with fm\r
+ bool mltn = isLessThan( m, n );\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( i==0 || m.getOperator()==n.getOperator() ){\r
+ Node am = ((i==0)==mltn) ? n : m;\r
+ Node an = ((i==0)==mltn) ? m : n;\r
+ if( itm->second->d_qni.addTermEq( this, an, am ) ){\r
+ Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for ";\r
+ Trace("qcf-reqr") << fn << " " << fm << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ if( !relevant ){\r
+ //if not relevant for disequalities, store it\r
+ if( index==1 ){\r
+ irrelevant_dnode[n] = true;\r
+ }\r
+ }else{\r
+ //if relevant for equalities, store it\r
+ if( index==0 ){\r
+ eqc.push_back( n );\r
+ }\r
+ }\r
+ }\r
+ ++eqc_i;\r
+ }\r
+ process_eqc[r] = true;\r
+ ++eqcs_i;\r
+ }\r
+}\r
+\r
+\r
+void QuantConflictFind::QuantInfo::reset_round( QuantConflictFind * p ) {\r
+ d_match.clear();\r
+ d_curr_var_deq.clear();\r
+ //add built-in variable constraints\r
+ for( unsigned r=0; r<2; r++ ){\r
+ for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();\r
+ it != d_var_constraint[r].end(); ++it ){\r
+ for( unsigned j=0; j<it->second.size(); j++ ){\r
+ Node rr = it->second[j];\r
+ if( !isVar( rr ) ){\r
+ rr = p->getRepresentative( rr );\r
+ }\r
+ if( addConstraint( p, it->first, rr, r==0 )==-1 ){\r
+ d_var_constraint[0].clear();\r
+ d_var_constraint[1].clear();\r
+ //quantified formula is actually equivalent to true\r
+ Trace("qcf-qregister") << "Quantifier is equivalent to true!!!" << std::endl;\r
+ d_mg->d_children.clear();\r
+ d_mg->d_n = NodeManager::currentNM()->mkConst( true );\r
+ d_mg->d_type = MatchGen::typ_ground;\r
+ return;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ d_mg->reset_round( p );\r
+}\r
+\r
+int QuantConflictFind::QuantInfo::getCurrentRepVar( int v ) {\r
+ std::map< int, Node >::iterator it = d_match.find( v );\r
+ if( it!=d_match.end() ){\r
+ int vn = getVarNum( it->second );\r
+ if( vn!=-1 ){\r
+ //int vr = getCurrentRepVar( vn );\r
+ //d_match[v] = d_vars[vr];\r
+ //return vr;\r
+ return getCurrentRepVar( vn );\r
+ }\r
+ }\r
+ return v;\r
+}\r
+\r
+Node QuantConflictFind::QuantInfo::getCurrentValue( Node n ) {\r
+ int v = getVarNum( n );\r
+ if( v==-1 ){\r
+ return n;\r
+ }else{\r
+ std::map< int, Node >::iterator it = d_match.find( v );\r
+ if( it==d_match.end() ){\r
+ return n;\r
+ }else{\r
+ Assert( getVarNum( it->second )!=v );\r
+ return getCurrentValue( it->second );\r
+ }\r
+ }\r
+}\r
+\r
+bool QuantConflictFind::QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n ) {\r
+ //check disequalities\r
+ for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){\r
+ Node cv = getCurrentValue( it->first );\r
+ Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;\r
+ if( cv==n ){\r
+ return false;\r
+ }else if( !isVar( n ) && !isVar( cv ) ){\r
+ //they must actually be disequal\r
+ if( !p->areDisequal( n, cv ) ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ return true;\r
+}\r
+\r
+int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, bool polarity ) {\r
+ v = getCurrentRepVar( v );\r
+ int vn = getVarNum( n );\r
+ vn = vn==-1 ? -1 : getCurrentRepVar( vn );\r
+ n = getCurrentValue( n );\r
+ return addConstraint( p, v, n, vn, polarity, false );\r
+}\r
+\r
+int QuantConflictFind::QuantInfo::addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove ) {\r
+ //for handling equalities between variables, and disequalities involving variables\r
+ Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";\r
+ Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;\r
+ Assert( n==getCurrentValue( n ) );\r
+ Assert( doRemove || v==getCurrentRepVar( v ) );\r
+ Assert( doRemove || vn==getCurrentRepVar( getVarNum( n ) ) );\r
+ if( polarity ){\r
+ if( vn!=v ){\r
+ if( doRemove ){\r
+ if( vn!=-1 ){\r
+ //if set to this in the opposite direction, clean up opposite instead\r
+ std::map< int, Node >::iterator itmn = d_match.find( vn );\r
+ if( itmn!=d_match.end() && itmn->second==d_vars[v] ){\r
+ return addConstraint( p, vn, d_vars[v], v, true, true );\r
+ }else{\r
+ //unsetting variables equal\r
+\r
+ //remove disequalities owned by this\r
+ std::vector< Node > remDeq;\r
+ for( std::map< Node, int >::iterator it = d_curr_var_deq[vn].begin(); it != d_curr_var_deq[vn].end(); ++it ){\r
+ if( it->second==v ){\r
+ remDeq.push_back( it->first );\r
+ }\r
+ }\r
+ for( unsigned i=0; i<remDeq.size(); i++ ){\r
+ d_curr_var_deq[vn].erase( remDeq[i] );\r
+ }\r
+ }\r
+ }\r
+ d_match.erase( v );\r
+ return 1;\r
+ }else{\r
+ std::map< int, Node >::iterator itm = d_match.find( v );\r
+\r
+ if( vn!=-1 ){\r
+ Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;\r
+ std::map< int, Node >::iterator itmn = d_match.find( vn );\r
+ if( itm==d_match.end() ){\r
+ //setting variables equal\r
+ bool alreadySet = false;\r
+ if( itmn!=d_match.end() ){\r
+ alreadySet = true;\r
+ Assert( !itmn->second.isNull() && !isVar( itmn->second ) );\r
+ }\r
+\r
+ //copy or check disequalities\r
+ std::vector< Node > addDeq;\r
+ for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){\r
+ Node dv = getCurrentValue( it->first );\r
+ if( !alreadySet ){\r
+ if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){\r
+ d_curr_var_deq[vn][dv] = v;\r
+ addDeq.push_back( dv );\r
+ }\r
+ }else{\r
+ if( itmn->second!=dv ){\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
+ }\r
+ }\r
+ if( alreadySet ){\r
+ n = getCurrentValue( n );\r
+ }\r
+ }else{\r
+ if( itmn==d_match.end() ){\r
+ Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;\r
+ //set the opposite direction\r
+ return addConstraint( p, vn, d_vars[v], v, true, false );\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> Both variables bound, compare" << std::endl;\r
+ //are they currently equal\r
+ return itm->second==itmn->second ? 0 : -1;\r
+ }\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;\r
+ if( itm==d_match.end() ){\r
+\r
+ }else{\r
+ //compare ground values\r
+ Debug("qcf-match-debug") << " -> Ground value, compare " << itm->second << " "<< n << std::endl;\r
+ return itm->second==n ? 0 : -1;\r
+ }\r
+ }\r
+ if( setMatch( p, v, n ) ){\r
+ Debug("qcf-match-debug") << " -> success" << std::endl;\r
+ return 1;\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> redundant, variable identity" << std::endl;\r
+ return 0;\r
+ }\r
+ }else{\r
+ if( vn==v ){\r
+ Debug("qcf-match-debug") << " -> fail, variable identity" << std::endl;\r
+ return -1;\r
+ }else{\r
+ if( doRemove ){\r
+ Assert( d_curr_var_deq[v].find( n )!=d_curr_var_deq[v].end() );\r
+ d_curr_var_deq[v].erase( n );\r
+ return 1;\r
+ }else{\r
+ if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){\r
+ //check if it respects equality\r
+ std::map< int, Node >::iterator itm = d_match.find( v );\r
+ if( itm!=d_match.end() ){\r
+ if( getCurrentValue( n )==itm->second ){\r
+ Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl;\r
+ return -1;\r
+ }\r
+ }\r
+ d_curr_var_deq[v][n] = v;\r
+ Debug("qcf-match-debug") << " -> success" << std::endl;\r
+ return 1;\r
+ }else{\r
+ Debug("qcf-match-debug") << " -> redundant disequality" << std::endl;\r
+ return 0;\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+bool QuantConflictFind::QuantInfo::setMatch( QuantConflictFind * p, int v, Node n ) {\r
+ if( getCurrentCanBeEqual( p, v, n ) ){\r
+ Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;\r
+ d_match[v] = n;\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+bool QuantConflictFind::QuantInfo::isMatchSpurious( QuantConflictFind * p ) {\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ std::map< int, Node >::iterator it = d_match.find( i );\r
+ if( it!=d_match.end() ){\r
+ if( !getCurrentCanBeEqual( p, i, it->second ) ){\r
+ return true;\r
+ }\r
+ }\r
+ }\r
+ return false;\r
+}\r
+\r
+void QuantConflictFind::QuantInfo::debugPrintMatch( const char * c ) {\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ Trace(c) << " " << d_vars[i] << " -> ";\r
+ if( d_match.find( i )!=d_match.end() ){\r
+ Trace(c) << d_match[i];\r
+ }else{\r
+ Trace(c) << "(unassigned) ";\r
+ }\r
+ if( !d_curr_var_deq[i].empty() ){\r
+ Trace(c) << ", DEQ{ ";\r
+ for( std::map< Node, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){\r
+ Trace(c) << it->first << " ";\r
+ }\r
+ Trace(c) << "}";\r
+ }\r
+ Trace(c) << std::endl;\r
+ }\r
+}\r
+\r
+\r
+struct MatchGenSort {\r
+ QuantConflictFind::MatchGen * d_mg;\r
+ bool operator() (int i,int j) {\r
+ return d_mg->d_children[i].d_type<d_mg->d_children[j].d_type;\r
+ }\r
+};\r
+\r
+QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop, bool isVar ){\r
+ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", top/var = " << isTop << " " << isVar << std::endl;\r
+ std::vector< Node > qni_apps;\r
+ d_qni_size = 0;\r
+ if( isVar ){\r
+ Assert( p->d_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() );\r
+ if( n.getKind()==APPLY_UF ){\r
+ d_type = typ_var;\r
+ d_type_not = true; //implicit disequality, in disjunction at top level\r
+ d_n = n;\r
+ qni_apps.push_back( n );\r
+ }else{\r
+ //unknown term\r
+ d_type = typ_invalid;\r
+ }\r
+ }else{\r
+ if( isTop && n.getKind()!=OR && p->d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){\r
+ //conjoin extra constraints based on flattening with quantifier body\r
+ d_children.push_back( MatchGen( p, q, n ) );\r
+ if( d_children[0].d_type==typ_invalid ){\r
+ d_children.clear();\r
+ d_type = typ_invalid;\r
+ }else{\r
+ d_type = typ_top;\r
+ }\r
+ d_type_not = false;\r
+ }else if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ //we handle not immediately\r
+ d_n = n.getKind()==NOT ? n[0] : n;\r
+ d_type_not = n.getKind()==NOT;\r
+ if( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF || d_n.getKind()==ITE ){\r
+ //non-literals\r
+ d_type = typ_valid;\r
+ for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
+ d_children.push_back( MatchGen( p, q, d_n[i] ) );\r
+ if( d_children[d_children.size()-1].d_type==typ_invalid ){\r
+ d_type = typ_invalid;\r
+ d_children.clear();\r
+ break;\r
+ }else if( isTop && n.getKind()==OR && d_children[d_children.size()-1].d_type==typ_var_eq ){\r
+ Trace("qcf-qregister-debug") << "Remove child, make built-in constraint" << std::endl;\r
+ //if variable equality/disequality at top level, remove immediately\r
+ bool cIsNot = d_children[d_children.size()-1].d_type_not;\r
+ Node cn = d_children[d_children.size()-1].d_n;\r
+ Assert( cn.getKind()==EQUAL );\r
+ Assert( p->d_qinfo[q].isVar( cn[0] ) || p->d_qinfo[q].isVar( cn[1] ) );\r
+ //make it a built-in constraint instead\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( p->d_qinfo[q].isVar( cn[i] ) ){\r
+ int v = p->d_qinfo[q].getVarNum( cn[i] );\r
+ Node cno = cn[i==0 ? 1 : 0];\r
+ p->d_qinfo[q].d_var_constraint[ cIsNot ? 0 : 1 ][v].push_back( cno );\r
+ break;\r
+ }\r
+ }\r
+ d_children.pop_back();\r
+ }\r
+ }\r
+ }else{\r
+ d_type = typ_invalid;\r
+ //literals\r
+ if( d_n.getKind()==APPLY_UF || d_n.getKind()==EQUAL ){\r
+ //get the applications (in order) that will be matching\r
+ p->getEqRegistryApps( d_n, qni_apps );\r
+ if( qni_apps.size()>0 ){\r
+ d_type =typ_valid_lit;\r
+ }else if( d_n.getKind()==EQUAL ){\r
+ bool isValid = true;\r
+ for( unsigned i=0; i<2; i++ ){\r
+ if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) && !p->d_qinfo[q].isVar( d_n[i] ) ){\r
+ isValid = false;\r
+ break;\r
+ }\r
+ }\r
+ if( isValid ){\r
+ Assert( p->d_qinfo[q].isVar( d_n[0] ) || p->d_qinfo[q].isVar( d_n[1] ) );\r
+ // variable equality\r
+ d_type = typ_var_eq;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ //we will just evaluate\r
+ d_n = n;\r
+ d_type = typ_ground;\r
+ }\r
+ if( d_type!=typ_invalid ){\r
+ //determine an efficient children ordering\r
+ if( !d_children.empty() ){\r
+ for( unsigned i=0; i<d_children.size(); i++ ){\r
+ d_children_order.push_back( i );\r
+ }\r
+ if( !d_n.isNull() && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ) ){\r
+ //sort based on the type of the constraint : ground comes first, then literals, then others\r
+ //MatchGenSort mgs;\r
+ //mgs.d_mg = this;\r
+ //std::sort( d_children_order.begin(), d_children_order.end(), mbas );\r
+\r
+ }\r
+ }\r
+ if( isTop ){\r
+ int base = d_children.size();\r
+ //add additional constraints based on flattening\r
+ for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){\r
+ d_children.push_back( MatchGen( p, q, p->d_qinfo[q].d_vars[j], false, true ) );\r
+ }\r
+\r
+ //choose variable order for variables based on when they are bound\r
+ std::vector< int > varOrder;\r
+ varOrder.insert( varOrder.end(), d_children_order.begin(), d_children_order.end() );\r
+ d_children_order.clear();\r
+ std::map< int, bool > bound;\r
+ for( unsigned i=0; i<varOrder.size(); i++ ){\r
+ int curr = varOrder[i];\r
+ Trace("qcf-qregister-debug") << "Var Order : " << curr << std::endl;\r
+ d_children_order.push_back( curr );\r
+ for( std::map< int, int >::iterator it = d_children[curr].d_qni_var_num.begin();\r
+ it != d_children[curr].d_qni_var_num.end(); ++it ){\r
+ if( it->second>=(int)q[0].getNumChildren() && bound.find( it->second )==bound.end() ){\r
+ bound[ it->second ] = true;\r
+ int var = base + it->second - (int)q[0].getNumChildren();\r
+ d_children_order.push_back( var );\r
+ Trace("qcf-qregister-debug") << "Var Order, bound : " << var << std::endl;\r
+ }\r
+ }\r
+ }\r
+ for( unsigned j=q[0].getNumChildren(); j<p->d_qinfo[q].d_vars.size(); j++ ){\r
+ if( bound.find( j )==bound.end() ){\r
+ int var = base + j - (int)q[0].getNumChildren();\r
+ d_children_order.push_back( var );\r
+ Trace("qcf-qregister-debug") << "Var Order, remaining : " << j << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ if( d_type!=typ_invalid ){\r
+ if( !qni_apps.empty() ){\r
+ Trace("qcf-qregister-debug") << "Initialize matching..." << std::endl;\r
+ for( unsigned i=0; i<qni_apps.size(); i++ ){\r
+ for( unsigned j=0; j<qni_apps[i].getNumChildren(); j++ ){\r
+ Node nn = qni_apps[i][j];\r
+ Trace("qcf-qregister-debug") << " " << d_qni_size;\r
+ if( p->d_qinfo[q].isVar( nn ) ){\r
+ Trace("qcf-qregister-debug") << " is var #" << p->d_qinfo[q].d_var_num[nn] << std::endl;\r
+ d_qni_var_num[d_qni_size] = p->d_qinfo[q].d_var_num[nn];\r
+ }else{\r
+ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
+ d_qni_gterm[d_qni_size] = nn;\r
+ }\r
+ d_qni_size++;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";\r
+ debugPrintType( "qcf-qregister-debug", d_type, true );\r
+ Trace("qcf-qregister-debug") << std::endl;\r
+ Assert( d_children.size()==d_children_order.size() );\r
+}\r
+\r
+void QuantConflictFind::MatchGen::reset_round( QuantConflictFind * p ) {\r
+ for( std::map< int, Node >::iterator it = d_qni_gterm.begin(); it != d_qni_gterm.end(); ++it ){\r
+ d_qni_gterm_rep[it->first] = p->getRepresentative( it->second );\r
+ }\r
+ for( unsigned i=0; i<d_children.size(); i++ ){\r
+ d_children[i].reset_round( p );\r
+ }\r
+}\r
+\r
+void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q ) {\r
+ d_tgt = d_type_not ? !tgt : tgt;\r
+ Debug("qcf-match") << " Reset for : " << d_n << ", type : ";\r
+ debugPrintType( "qcf-match", d_type );\r
+ Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << std::endl;\r
+ d_qn.clear();\r
+ d_qni.clear();\r
+ d_qni_bound.clear();\r
+ d_child_counter = -1;\r
+\r
+ //set up processing matches\r
+ if( d_type==typ_ground ){\r
+ if( p->evaluate( d_n )==( d_tgt ? 1 : -1 ) ){\r
+ //store dummy variable\r
+ d_qn.push_back( NULL );\r
+ }\r
+ }else if( d_type==typ_var ){\r
+ //check if variable is bound by now\r
+ int vi = p->d_qinfo[q].getVarNum( d_n );\r
+ Assert( vi!=-1 );\r
+ int repVar = p->d_qinfo[q].getCurrentRepVar( vi );\r
+ Assert( d_n.getKind()==APPLY_UF );\r
+ Node f = d_n.getOperator();\r
+ std::map< int, Node >::iterator it = p->d_qinfo[q].d_match.find( repVar );\r
+ if( it!=p->d_qinfo[q].d_match.end() && d_tgt ) {\r
+ Debug("qcf-match") << " will be matching var within eqc = " << it->second << std::endl;\r
+ //f-applications in the equivalence class in match[ repVar ]\r
+ std::map< Node, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f );\r
+ if( itut!=p->d_eqc_uf_terms[ it->second ].end() ){\r
+ d_qn.push_back( &itut->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match") << " will be matching var within any eqc." << std::endl;\r
+ //we are binding rep var\r
+ d_qni_bound_cons[repVar] = Node::null();\r
+ //must look at all f-applications\r
+ std::map< Node, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f );\r
+ if( itut!=p->d_uf_terms.end() ){\r
+ d_qn.push_back( &itut->second );\r
+ }\r
+ }\r
+ }else if( d_type==typ_var_eq ){\r
+ bool success = false;\r
+ for( unsigned i=0; i<2; i++ ){\r
+ int var = p->d_qinfo[q].getVarNum( d_n[i] );\r
+ if( var!=-1 ){\r
+ int repVar = p->d_qinfo[q].getCurrentRepVar( var );\r
+ Node o = d_n[ i==0 ? 1 : 0 ];\r
+ o = p->d_qinfo[q].getCurrentValue( o );\r
+ int vo = p->d_qinfo[q].getCurrentRepVar( p->d_qinfo[q].getVarNum( o ) );\r
+ int addCons = p->d_qinfo[q].addConstraint( p, repVar, o, vo, d_tgt, false );\r
+ success = addCons!=-1;\r
+ //if successful and non-redundant, store that we need to cleanup this\r
+ if( addCons==1 ){\r
+ d_qni_bound_cons[repVar] = o;\r
+ d_qni_bound[repVar] = vo;\r
+ }\r
+ break;\r
+ }\r
+ }\r
+ if( success ){\r
+ //store dummy\r
+ d_qn.push_back( NULL );\r
+ }\r
+ }else if( d_type==typ_valid_lit ){\r
+ //literal\r
+ EqRegistry * er = p->getEqRegistry( d_tgt, d_n, false );\r
+ Assert( er );\r
+ d_qn.push_back( &(er->d_qni) );\r
+ }else{\r
+ if( d_children.empty() ){\r
+ //add dummy\r
+ d_qn.push_back( NULL );\r
+ }else{\r
+ //reset the first child to d_tgt\r
+ d_child_counter = 0;\r
+ getChild( d_child_counter )->reset( p, d_tgt, q );\r
+ }\r
+ }\r
+ Debug("qcf-match") << " Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;\r
+}\r
+\r
+bool QuantConflictFind::MatchGen::getNextMatch( QuantConflictFind * p, Node q ) {\r
+ Debug("qcf-match") << " Get next match for : " << d_n << ", type = ";\r
+ debugPrintType( "qcf-match", d_type );\r
+ Debug("qcf-match") << ", children = " << d_children.size() << std::endl;\r
+ if( d_children.empty() ){\r
+ bool success = doMatching( p, q );\r
+ if( !success ){\r
+ for( std::map< int, Node >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){\r
+ if( !it->second.isNull() ){\r
+ Debug("qcf-match") << " Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;\r
+ std::map< int, int >::iterator itb = d_qni_bound.find( it->first );\r
+ int vn = itb!=d_qni_bound.end() ? itb->second : -1;\r
+ p->d_qinfo[q].addConstraint( p, it->first, it->second, vn, d_tgt, true );\r
+ if( vn!=-1 ){\r
+ d_qni_bound.erase( vn );\r
+ }\r
+ }\r
+ }\r
+ d_qni_bound_cons.clear();\r
+ //clean up the match : remove equalities/disequalities\r
+ for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){\r
+ Debug("qcf-match") << " Clean up bound var " << it->second << std::endl;\r
+ Assert( it->second<p->d_qinfo[q].getNumVars() );\r
+ p->d_qinfo[q].d_match.erase( it->second );\r
+ }\r
+ d_qni_bound.clear();\r
+ }\r
+ Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;\r
+ return success;\r
+ }else{\r
+ if( d_child_counter!=-1 ){\r
+ bool success = false;\r
+ while( !success && d_child_counter>=0 ){\r
+ //transition system based on d_child_counter\r
+ if( d_type==typ_top || d_n.getKind()==OR || d_n.getKind()==AND ){\r
+ if( (d_n.getKind()==AND)==d_tgt ){\r
+ //all children must match simultaneously\r
+ if( getChild( d_child_counter )->getNextMatch( p, q ) ){\r
+ if( d_child_counter<(int)(getNumChildren()-1) ){\r
+ d_child_counter++;\r
+ 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;\r
+ getChild( d_child_counter )->reset( p, d_tgt, q );\r
+ }else{\r
+ success = true;\r
+ }\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }else{\r
+ //one child must match\r
+ if( !getChild( d_child_counter )->getNextMatch( p, q ) ){\r
+ if( d_child_counter<(int)(getNumChildren()-1) ){\r
+ d_child_counter++;\r
+ Debug("qcf-match-debug") << " Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;\r
+ getChild( d_child_counter )->reset( p, d_tgt, q );\r
+ }else{\r
+ d_child_counter = -1;\r
+ }\r
+ }else{\r
+ success = true;\r
+ }\r
+ }\r
+ }else if( d_n.getKind()==IFF ){\r
+ //construct match based on both children\r
+ if( d_child_counter%2==0 ){\r
+ if( getChild( 0 )->getNextMatch( p, q ) ){\r
+ d_child_counter++;\r
+ getChild( 1 )->reset( p, d_child_counter==1, q );\r
+ }else{\r
+ if( d_child_counter==0 ){\r
+ d_child_counter = 2;\r
+ getChild( 0 )->reset( p, !d_tgt, q );\r
+ }else{\r
+ d_child_counter = -1;\r
+ }\r
+ }\r
+ }\r
+ if( d_child_counter%2==1 ){\r
+ if( getChild( 1 )->getNextMatch( p, q ) ){\r
+ success = true;\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }\r
+ }else if( d_n.getKind()==ITE ){\r
+ if( d_child_counter%2==0 ){\r
+ int index1 = d_child_counter==4 ? 1 : 0;\r
+ if( getChild( index1 )->getNextMatch( p, q ) ){\r
+ d_child_counter++;\r
+ getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2) )->reset( p, d_tgt, q );\r
+ }else{\r
+ if( d_child_counter==4 ){\r
+ d_child_counter = -1;\r
+ }else{\r
+ d_child_counter +=2;\r
+ getChild( d_child_counter==4 ? 1 : 0 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, q );\r
+ }\r
+ }\r
+ }\r
+ if( d_child_counter%2==1 ){\r
+ int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==0) ? 1 : 2);\r
+ if( getChild( index2 )->getNextMatch( p, q ) ){\r
+ success = true;\r
+ }else{\r
+ d_child_counter--;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ Debug("qcf-match") << " ...finished construct match for " << d_n << ", success = " << success << std::endl;\r
+ return success;\r
+ }\r
+ }\r
+ Debug("qcf-match") << " ...already finished for " << d_n << std::endl;\r
+ return false;\r
+}\r
+\r
+bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) {\r
+ if( !d_qn.empty() ){\r
+ if( d_qn[0]==NULL ){\r
+ d_qn.clear();\r
+ return true;\r
+ }else{\r
+ Assert( d_qni_size>0 );\r
+ bool invalidMatch;\r
+ do {\r
+ invalidMatch = false;\r
+ Debug("qcf-match-debug") << " Do matching " << d_qn.size() << " " << d_qni.size() << std::endl;\r
+ if( d_qn.size()==d_qni.size()+1 ) {\r
+ int index = (int)d_qni.size();\r
+ //initialize\r
+ Node val;\r
+ std::map< int, int >::iterator itv = d_qni_var_num.find( index );\r
+ if( itv!=d_qni_var_num.end() ){\r
+ //get the representative variable this variable is equal to\r
+ int repVar = p->d_qinfo[q].getCurrentRepVar( itv->second );\r
+ Debug("qcf-match-debug") << " Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;\r
+ //get the value the rep variable\r
+ std::map< int, Node >::iterator itm = p->d_qinfo[q].d_match.find( repVar );\r
+ if( itm!=p->d_qinfo[q].d_match.end() ){\r
+ val = itm->second;\r
+ Assert( !val.isNull() );\r
+ Debug("qcf-match-debug") << " Variable is already bound to " << val << std::endl;\r
+ }else{\r
+ //binding a variable\r
+ d_qni_bound[index] = repVar;\r
+ std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin();\r
+ if( it != d_qn[index]->d_children.end() ) {\r
+ d_qni.push_back( it );\r
+ //set the match\r
+ if( p->d_qinfo[q].setMatch( p, d_qni_bound[index], it->first ) ){\r
+ Debug("qcf-match-debug") << " Binding variable" << std::endl;\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &it->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match") << " Binding variable, currently fail." << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Binding variable, fail, no more variables to bind" << std::endl;\r
+ d_qn.pop_back();\r
+ }\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Match " << index << " is ground term" << std::endl;\r
+ Assert( d_qni_gterm.find( index )!=d_qni_gterm.end() );\r
+ Assert( d_qni_gterm_rep.find( index )!=d_qni_gterm_rep.end() );\r
+ val = d_qni_gterm_rep[index];\r
+ Assert( !val.isNull() );\r
+ }\r
+ if( !val.isNull() ){\r
+ //constrained by val\r
+ std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val );\r
+ if( it!=d_qn[index]->d_children.end() ){\r
+ Debug("qcf-match-debug") << " Match" << std::endl;\r
+ d_qni.push_back( it );\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &it->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Failed to match" << std::endl;\r
+ d_qn.pop_back();\r
+ }\r
+ }\r
+ }else{\r
+ Assert( d_qn.size()==d_qni.size() );\r
+ int index = d_qni.size()-1;\r
+ //increment if binding this variable\r
+ bool success = false;\r
+ std::map< int, int >::iterator itb = d_qni_bound.find( index );\r
+ if( itb!=d_qni_bound.end() ){\r
+ d_qni[index]++;\r
+ if( d_qni[index]!=d_qn[index]->d_children.end() ){\r
+ success = true;\r
+ if( p->d_qinfo[q].setMatch( p, itb->second, d_qni[index]->first ) ){\r
+ Debug("qcf-match-debug") << " Bind next variable" << std::endl;\r
+ if( d_qn.size()<d_qni_size ){\r
+ d_qn.push_back( &d_qni[index]->second );\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Bind next variable, currently fail" << std::endl;\r
+ invalidMatch = true;\r
+ }\r
+ }else{\r
+ Debug("qcf-match-debug") << " Bind next variable, no more variables to bind" << std::endl;\r
+ }\r
+ }\r
+ //if not incrementing, move to next\r
+ if( !success ){\r
+ d_qn.pop_back();\r
+ d_qni.pop_back();\r
+ }\r
+ }\r
+ if( d_type==typ_var ){\r
+ if( !invalidMatch && d_qni.size()==d_qni_size ){\r
+ //if in the act of binding the variable by this term, bind the variable\r
+ std::map< int, Node >::iterator itb = d_qni_bound_cons.begin();\r
+ if( itb!=d_qni_bound_cons.end() ){\r
+ QcfNodeIndex * v_qni = &d_qni[d_qni.size()-1]->second;\r
+ Assert( v_qni->d_children.begin()!=v_qni->d_children.end() );\r
+ Node vb = v_qni->d_children.begin()->first;\r
+ Assert( !vb.isNull() );\r
+ vb = p->getRepresentative( vb );\r
+ Debug("qcf-match-debug") << " For var, require binding " << itb->first << " to " << vb << ", d_tgt = " << d_tgt << std::endl;\r
+ if( !itb->second.isNull() ){\r
+ p->d_qinfo[q].addConstraint( p, itb->first, itb->second, -1, d_tgt, true );\r
+ }\r
+ int addCons = p->d_qinfo[q].addConstraint( p, itb->first, vb, -1, d_tgt, false );\r
+ if( addCons==-1 ){\r
+ Debug("qcf-match-debug") << " Failed set for var." << std::endl;\r
+ invalidMatch = true;\r
+ d_qni_bound_cons[itb->first] = Node::null();\r
+ }else{\r
+ Debug("qcf-match-debug") << " Succeeded set for var." << std::endl;\r
+ if( addCons==1 ){\r
+ d_qni_bound_cons[itb->first] = vb;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );\r
+ }\r
+ }\r
+ return !d_qn.empty();\r
+}\r
+\r
+void QuantConflictFind::MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {\r
+ if( isTrace ){\r
+ switch( typ ){\r
+ case typ_invalid: Trace(c) << "invalid";break;\r
+ case typ_ground: Trace(c) << "ground";break;\r
+ case typ_valid_lit: Trace(c) << "valid_lit";break;\r
+ case typ_valid: Trace(c) << "valid";break;\r
+ case typ_var: Trace(c) << "var";break;\r
+ case typ_var_eq: Trace(c) << "var_eq";break;\r
+ case typ_top: Trace(c) << "top";break;\r
+ }\r
+ }else{\r
+ switch( typ ){\r
+ case typ_invalid: Debug(c) << "invalid";break;\r
+ case typ_ground: Debug(c) << "ground";break;\r
+ case typ_valid_lit: Debug(c) << "valid_lit";break;\r
+ case typ_valid: Debug(c) << "valid";break;\r
+ case typ_var: Debug(c) << "var";break;\r
+ case typ_var_eq: Debug(c) << "var_eq";break;\r
+ case typ_top: Debug(c) << "top";break;\r
+ }\r
+ }\r
+}\r
+\r
+\r
+//-------------------------------------------------- debugging\r
+\r
+\r
+void QuantConflictFind::debugPrint( const char * c ) {\r
+ //print the equivalance classes\r
+ Trace(c) << "----------EQ classes" << std::endl;\r
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );\r
+ while( !eqcs_i.isFinished() ){\r
+ Node n = (*eqcs_i);\r
+ if( !n.getType().isInteger() ){\r
+ Trace(c) << " - " << n << " : {";\r
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );\r
+ bool pr = false;\r
+ while( !eqc_i.isFinished() ){\r
+ Node nn = (*eqc_i);\r
+ if( nn.getKind()!=EQUAL && nn!=n ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << nn;\r
+ pr = true;\r
+ }\r
+ ++eqc_i;\r
+ }\r
+ Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
+ EqcInfo * eqcn = getEqcInfo( n, false );\r
+ if( eqcn ){\r
+ Trace(c) << " DEQ : {";\r
+ pr = false;\r
+ for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){\r
+ if( (*it).second ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << (*it).first;\r
+ pr = true;\r
+ }\r
+ }\r
+ Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
+ }\r
+ }\r
+ ++eqcs_i;\r
+ }\r
+ std::map< Node, std::map< Node, bool > > printed;\r
+ //print the equality registries\r
+ for( unsigned i=0; i<2; i++ ){\r
+ printed.clear();\r
+ Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl;\r
+ for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){\r
+ bool prHead = false;\r
+ for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ bool print;\r
+ if( it->first.getKind()==APPLY_UF && it2->first.getKind()==APPLY_UF &&\r
+ it->first.getOperator()!=it2->first.getOperator() ){\r
+ print = isLessThan( it->first, it2->first );\r
+ }else{\r
+ print = printed[it->first].find( it2->first )==printed[it->first].end();\r
+ }\r
+ if( print ){\r
+ printed[it->first][it2->first] = true;\r
+ printed[it2->first][it->first] = true;\r
+ if( !prHead ){\r
+ Trace(c) << "- " << it->first << std::endl;\r
+ prHead = true;\r
+ }\r
+ Trace(c) << " " << it2->first << ", terms : " << std::endl;\r
+\r
+ /*\r
+ Trace(c) << " " << it2->first << " : {";\r
+ bool pr = false;\r
+ for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){\r
+ if( (*it3).second ){\r
+ Trace(c) << (pr ? "," : "" ) << " " << (*it3).first;\r
+ pr = true;\r
+ }\r
+ }\r
+ Trace(c) << (pr ? " " : "" ) << "}" << std::endl;\r
+ */\r
+ //print qni structure\r
+ it2->second->debugPrint( c, 3 );\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {\r
+ Trace(c) << "Q" << d_quant_id[q];\r
+}\r
+\r
+void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) {\r
+ if( n.getNumChildren()==0 ){\r
+ Trace(c) << n;\r
+ }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){\r
+ Trace(c) << "?x" << d_qinfo[q].d_var_num[n];\r
+ }else{\r
+ Trace(c) << "(";\r
+ if( n.getKind()==APPLY_UF ){\r
+ Trace(c) << n.getOperator();\r
+ }else{\r
+ Trace(c) << n.getKind();\r
+ }\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ Trace(c) << " ";\r
+ debugPrintQuantBody( c, q, n[i] );\r
+ }\r
+ Trace(c) << ")";\r
+ }\r
+}\r
+\r
+}
\ No newline at end of file
projects / cvc5.git / commitdiff