From 276fb84a1bb1905ce2080c007f63fefff536a970 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 Jan 2014 09:57:12 -0600 Subject: [PATCH] More optimizations for quantifiers conflict find. Add trust user patterns mode. --- .../quantifiers/inst_strategy_e_matching.cpp | 109 ++-- .../quantifiers/instantiation_engine.cpp | 2 +- src/theory/quantifiers/modes.h | 11 +- src/theory/quantifiers/options | 4 +- src/theory/quantifiers/options_handlers.h | 30 +- .../quantifiers/quant_conflict_find.cpp | 487 ++++++++++-------- src/theory/quantifiers/quant_conflict_find.h | 26 +- 7 files changed, 373 insertions(+), 296 deletions(-) diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index ef81d55a1..9acdf6152 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -123,68 +123,71 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort } int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){ - int peffort = f.getNumChildren()==3 ? 2 : 1; - //int peffort = f.getNumChildren()==3 ? 2 : 1; - //int peffort = 1; - if( egetEqualityQuery()->setLiberal( true ); - //} - Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; - //Notice() << "Try auto-generated triggers..." << std::endl; - for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ - Trigger* tr = itt->first; - if( tr ){ - bool processTrigger = itt->second; - if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){ - d_processed_trigger[f][tr] = true; - //if( tr->isMultiTrigger() ) - Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl; - InstMatch baseMatch; - int numInst = tr->addInstantiations( baseMatch ); - //if( tr->isMultiTrigger() ) - Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; - if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ - d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; - }else{ - d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst; - } - if( tr->isMultiTrigger() ){ - d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + //if( e==4 ){ + // d_processed_trigger.clear(); + // d_quantEngine->getEqualityQuery()->setLiberal( true ); + //} + Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl; + //Notice() << "Try auto-generated triggers..." << std::endl; + for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[f].begin(); itt != d_auto_gen_trigger[f].end(); ++itt ){ + Trigger* tr = itt->first; + if( tr ){ + bool processTrigger = itt->second; + if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){ + d_processed_trigger[f][tr] = true; + //if( tr->isMultiTrigger() ) + Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl; + InstMatch baseMatch; + int numInst = tr->addInstantiations( baseMatch ); + //if( tr->isMultiTrigger() ) + Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl; + if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){ + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst; + }else{ + d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst; + } + if( tr->isMultiTrigger() ){ + d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst; + } + //d_quantEngine->d_hasInstantiated[f] = true; } - //d_quantEngine->d_hasInstantiated[f] = true; } } + //if( e==4 ){ + // d_quantEngine->getEqualityQuery()->setLiberal( false ); + //} + Debug("quant-uf-strategy") << "done." << std::endl; + //Notice() << "done" << std::endl; + return status; } - //if( e==4 ){ - // d_quantEngine->getEqualityQuery()->setLiberal( false ); - //} - Debug("quant-uf-strategy") << "done." << std::endl; - //Notice() << "done" << std::endl; - return status; } } diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index fa7b4e342..e3ed8d0e0 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -42,7 +42,7 @@ void InstantiationEngine::finishInit(){ // addInstStrategy( new InstStrategyCheckCESolved( this, d_quantEngine ) ); //} //these are the instantiation strategies for basic E-matching - if( options::userPatternsQuant() ){ + if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ d_isup = new InstStrategyUserPatterns( d_quantEngine ); addInstStrategy( d_isup ); }else{ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 7a7ce9b54..4eb12c98d 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -75,10 +75,19 @@ typedef enum { QCF_WHEN_MODE_DEFAULT, /** apply at standard effort */ QCF_WHEN_MODE_STD, - /** default */ + /** apply based on heuristics */ QCF_WHEN_MODE_STD_H, } QcfWhenMode; +typedef enum { + /** default, use but do not trust */ + USER_PAT_MODE_DEFAULT, + /** if patterns are supplied for a quantifier, use only those */ + USER_PAT_MODE_TRUST, + /** ignore user patterns */ + USER_PAT_MODE_IGNORE, +} UserPatMode; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index dc016be3f..4a853b6cd 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -82,8 +82,8 @@ option cbqi --enable-cbqi bool :default false option recurseCbqi --cbqi-recurse bool :default false turns on recursive counterexample-based quantifier instantiation -option userPatternsQuant /--ignore-user-patterns bool :default true - ignore user-provided patterns for quantifier instantiation +option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" + policy for handling user-provided patterns for quantifier instantiation option flipDecision --flip-decision/ bool :default false turns on flip decision heuristic diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e0b1e30e8..5bd710a79 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -110,7 +110,20 @@ std-h \n\ + Apply conflict finding at standard effort when heuristic says to. \n\ \n\ "; - +static const std::string userPatModeHelp = "\ +User pattern modes currently supported by the --user-pat option:\n\ +\n\ +default \n\ ++ Default, use both user-provided and auto-generated patterns when patterns\n\ + are provided for a quantified formula.\n\ +\n\ +trust \n\ ++ When provided, use only user-provided patterns for a quantified formula.\n\ +\n\ +ignore \n\ ++ Ignore user-provided patterns. \n\ +\n\ +"; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -215,6 +228,21 @@ inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, S } } +inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return USER_PAT_MODE_DEFAULT; + } else if(optarg == "trust") { + return USER_PAT_MODE_TRUST; + } else if(optarg == "ignore") { + return USER_PAT_MODE_IGNORE; + } else if(optarg == "help") { + puts(userPatModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --user-pat: `") + + optarg + "'. Try --user-pat help."); + } +} }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index d7111ea39..4cb62b523 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -27,53 +27,7 @@ using namespace std; namespace CVC4 { -/* -Node QcfNodeIndex::existsTerm( QuantConflictFind * qcf, Node n, int index ) { - if( index==(int)n.getNumChildren() ){ - if( d_children.empty() ){ - return Node::null(); - }else{ - return d_children.begin()->first; - } - }else{ - Node r = qcf->getRepresentative( n[index] ); - if( d_children.find( r )==d_children.end() ){ - return n; - }else{ - return d_children[r].existsTerm( qcf, n, index+1 ); - } - } -} - - -Node QcfNodeIndex::addTerm( QuantConflictFind * qcf, Node n, int index ) { - if( index==(int)n.getNumChildren() ){ - if( d_children.empty() ){ - d_children[ n ].clear(); - return n; - }else{ - return d_children.begin()->first; - } - }else{ - Node r = qcf->getRepresentative( n[index] ); - return d_children[r].addTerm( qcf, n, index+1 ); - } -} - -bool QcfNodeIndex::addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index ) { - if( index==(int)n1.getNumChildren() ){ - Node n = addTerm( qcf, n2 ); - return n==n2; - }else{ - Node r = qcf->getRepresentative( n1[index] ); - return d_children[r].addTermEq( qcf, n1, n2, index+1 ); - } -} -*/ - - - -Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) { +Node QcfNodeIndex::existsTerm( TNode n, std::vector< TNode >& reps, int index ) { if( index==(int)reps.size() ){ if( d_children.empty() ){ return Node::null(); @@ -89,7 +43,7 @@ Node QcfNodeIndex::existsTerm( Node n, std::vector< Node >& reps, int index ) { } } -Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) { +Node QcfNodeIndex::addTerm( TNode n, std::vector< TNode >& reps, int index ) { if( index==(int)reps.size() ){ if( d_children.empty() ){ d_children[ n ].clear(); @@ -102,7 +56,7 @@ Node QcfNodeIndex::addTerm( Node n, std::vector< Node >& reps, int index ) { } } -bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index ) { +bool QcfNodeIndex::addTermEq( TNode n1, TNode n2, std::vector< TNode >& reps1, std::vector< TNode >& reps2, int index ) { if( index==(int)reps1.size() ){ Node n = addTerm( n2, reps2 ); return n==n2; @@ -114,7 +68,7 @@ bool QcfNodeIndex::addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std: void QcfNodeIndex::debugPrint( const char * c, int t ) { - for( std::map< Node, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ + for( std::map< TNode, QcfNodeIndex >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ if( !it->first.isNull() ){ for( int j=0; jfirst << " : " << std::endl; @@ -159,8 +113,8 @@ int QuantConflictFind::getFunctionId( Node f ) { } bool QuantConflictFind::isLessThan( Node a, Node b ) { - Assert( a.getKind()==APPLY_UF ); - Assert( b.getKind()==APPLY_UF ); + //Assert( a.getKind()==APPLY_UF ); + //Assert( b.getKind()==APPLY_UF ); /* if( a.getOperator()==b.getOperator() ){ for( unsigned i=0; i::iterator it = d_op_node.find( n.getOperator() ); if( it==d_op_node.end() ){ std::vector< Node > children; @@ -190,14 +146,15 @@ Node QuantConflictFind::getFunction( Node n, bool isQuant ) { for( unsigned i=0; imkNode( APPLY_UF, children ); + Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); d_op_node[n.getOperator()] = nn; return nn; }else{ return it->second; - } + }*/ + index = 1; + return n.getOperator(); }else{ - //should be a variable return Node::null(); } } @@ -344,26 +301,29 @@ EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doC int i; Node f1; Node f2; + int f1Index; + int f2Index; if( lit.getKind()==EQUAL ){ i = polarity ? 0 : 1; - f1 = getFunction( lit[0], true ); - f2 = getFunction( lit[1], true ); + f1 = getFunction( lit[0], f1Index, true ); + f2 = getFunction( lit[1], f2Index, true ); }else if( lit.getKind()==APPLY_UF ){ i = 0; - f1 = getFunction( lit, true ); + f1 = getFunction( lit, f1Index, true ); f2 = polarity ? d_true : d_false; + f2Index = 0; } if( !f1.isNull() && !f2.isNull() ){ - if( d_eqr[i][f1].find( f2 )==d_eqr[i][f1].end() ){ + if( d_eqr[i][f1Index][f1][f2Index].find( f2 )==d_eqr[i][f1Index][f1][f2Index].end() ){ if( doCreate ){ - Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << std::endl; - d_eqr[i][f1][f2] = new EqRegistry( d_c ); - d_eqr[i][f2][f1] = d_eqr[i][f1][f2]; + Trace("qcf-register") << "RegisterEqr : " << f1 << " " << f2 << ", polarity = " << (i==0) << ", indices : " << f1Index << " " << f2Index << std::endl; + d_eqr[i][f1Index][f1][f2Index][f2] = new EqRegistry( d_c ); + d_eqr[i][f2Index][f2][f1Index][f1] = d_eqr[i][f1Index][f1][f2Index][f2]; }else{ return NULL; } } - return d_eqr[i][f1][f2]; + return d_eqr[i][f1Index][f1][f2Index][f2]; }else{ return NULL; } @@ -372,7 +332,6 @@ EqRegistry * QuantConflictFind::getEqRegistry( bool polarity, Node lit, bool doC void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms ) { Assert( quantifiers::TermDb::hasBoundVarAttr( lit ) ); if( lit.getKind()==EQUAL ){ - bool allUf = false; for( unsigned i=0; i<2; i++ ){ if( quantifiers::TermDb::hasBoundVarAttr( lit[i] ) ){ if( lit[i].getKind()==BOUND_VARIABLE ){ @@ -380,12 +339,11 @@ void QuantConflictFind::getEqRegistryApps( Node lit, std::vector< Node >& terms terms.clear(); return; }else{ - allUf = allUf && lit[i].getKind()==APPLY_UF; terms.push_back( lit[i] ); } } } - if( terms.size()==2 && allUf && isLessThan( terms[1], terms[0] ) ){ + if( terms.size()==2 && isLessThan( terms[1].getOperator(), terms[0].getOperator() ) ){ Node t = terms[0]; terms[0] = terms[1]; terms[1] = t; @@ -406,7 +364,7 @@ int QuantConflictFind::evaluate( Node n ) { }else if( areDisequal( n1, n2 ) ){ ret = -1; } - }else if( n.getKind()==APPLY_UF ){ + }else if( n.getKind()==APPLY_UF ){ //predicate Node nn = getTerm( n ); Debug("qcf-eval") << "Evaluate : Normalize " << nn << " to " << n << std::endl; if( areEqual( nn, d_true ) ){ @@ -498,7 +456,7 @@ Node QuantConflictFind::getRepresentative( Node n ) { } } Node QuantConflictFind::getTerm( Node n ) { - if( n.getKind()==APPLY_UF ){ + if( isHandledUfTerm( n ) ){ computeArgReps( n ); Node nn = d_uf_terms[n.getOperator()].existsTerm( n, d_arg_reps[n] ); if( !nn.isNull() ){ @@ -626,9 +584,11 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-check") << "Compute relevant equalities..." << std::endl; computeRelevantEqr(); - Trace("qcf-debug") << std::endl; - debugPrint("qcf-debug"); - Trace("qcf-debug") << std::endl; + if( Trace.isOn("qcf-debug") ){ + Trace("qcf-debug") << std::endl; + debugPrint("qcf-debug"); + Trace("qcf-debug") << std::endl; + } Trace("qcf-check") << "Checking quantified formulas..." << std::endl; @@ -714,9 +674,13 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) { void QuantConflictFind::computeRelevantEqr() { //first, reset information for( unsigned i=0; i<2; i++ ){ - for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){ - for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - it2->second->clear(); + for( unsigned j=0; j<2; j++ ){ + for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){ + for( unsigned jj=0; jj<2; jj++ ){ + for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){ + it2->second->clear(); + } + } } } } @@ -724,14 +688,28 @@ void QuantConflictFind::computeRelevantEqr() { d_eqc_uf_terms.clear(); d_eqcs.clear(); d_arg_reps.clear(); + double clSet = 0; + if( Trace.isOn("qcf-opt") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + } + + long nTermst = 0; + long nTerms = 0; + long nEqc = 0; + long nEq1 = 0; + long nEq2 = 0; + long nEq1t = 0; + long nEq2t = 0; + long nComp = 0; + //relevant nodes for eq registries + std::map< TNode, std::map< TNode, std::vector< TNode > > > eqr_to_node[2]; //which nodes are irrelevant for disequality matches - std::map< Node, bool > irrelevant_dnode; - //which eqc we have processed - std::map< Node, bool > process_eqc; + std::map< TNode, bool > irrelevant_dnode; //now, store matches eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() ); while( !eqcs_i.isFinished() ){ + nEqc++; Node r = (*eqcs_i); d_eqcs[r.getType()].push_back( r ); EqcInfo * eqcir = getEqcInfo( r, false ); @@ -740,18 +718,12 @@ void QuantConflictFind::computeRelevantEqr() { if( eqcir ){ for( NodeBoolMap::iterator it = eqcir->d_diseq.begin(); it != eqcir->d_diseq.end(); ++it ){ if( (*it).second ){ - Node rd = (*it).first; - //if we have processed the other direction - if( process_eqc.find( rd )!=process_eqc.end() ){ - eq::EqClassIterator eqcd_i = eq::EqClassIterator( rd, getEqualityEngine() ); - while( !eqcd_i.isFinished() ){ - Node nd = (*eqcd_i); - if( irrelevant_dnode.find( nd )==irrelevant_dnode.end() ){ - deqc.push_back( nd ); - } - ++eqcd_i; - } - } + //Node rd = (*it).first; + //if( rd!=getRepresentative( rd ) ){ + // std::cout << "Bad rep!" << std::endl; + // exit( 0 ); + //} + deqc.push_back( (*it).first ); } } } @@ -760,105 +732,159 @@ void QuantConflictFind::computeRelevantEqr() { //process disequalities eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() ); while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - bool isRedundant; - if( n.getKind()==APPLY_UF ){ - computeArgReps( n ); - Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] ); - isRedundant = (nadd!=n); - d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] ); - }else{ - isRedundant = false; - } - //process all relevant equalities and disequalities to n - for( unsigned index=0; index<2; index++ ){ - std::map< Node, std::map< Node, EqRegistry * > >::iterator itn[2]; - itn[0] = d_eqr[index].find( n ); - Node fn; - if( n.getKind()==APPLY_UF && !isRedundant ){ - fn = getFunction( n ); - itn[1] = d_eqr[index].find( fn ); + TNode n = (*eqc_i); + if( n.getKind()!=EQUAL ){ + nTermst++; + //node_to_rep[n] = r; + //if( n.getNumChildren()>0 ){ + // if( n.getKind()!=APPLY_UF ){ + // std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl; + // } + //} + + bool isRedundant; + std::map< TNode, std::vector< TNode > >::iterator it_na; + TNode fn; + if( isHandledUfTerm( n ) ){ + computeArgReps( n ); + it_na = d_arg_reps.find( n ); + Assert( it_na!=d_arg_reps.end() ); + Node nadd = d_eqc_uf_terms[r][n.getOperator()].addTerm( n, d_arg_reps[n] ); + isRedundant = (nadd!=n); + d_uf_terms[n.getOperator()].addTerm( n, d_arg_reps[n] ); + if( !isRedundant ){ + int jindex; + fn = getFunction( n, jindex ); + } + }else{ + isRedundant = false; } - //for n, fn... - bool relevant = false; - for( unsigned j=0; j<2; j++ ){ - //if this node is relevant as an ground term or f-application - if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index].end() ){ - relevant = true; - std::vector< Node >& rel_nodes = index==0 ? eqc : deqc; - for( unsigned i=0; i::iterator itm = itn[j]->second.find( m ); - if( itm!=itn[j]->second.end() ){ - if( itm->second->d_qni.addTerm( n, d_arg_reps[n] )==n ){ - Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; - Trace("qcf-reqr") << fn << " " << m << std::endl; - } - } - } - if( !fm.isNull() ){ - std::map< Node, EqRegistry * >::iterator itm = itn[j]->second.find( fm ); - if( itm!=itn[j]->second.end() ){ - Assert( d_arg_reps.find( m )!=d_arg_reps.end() ); - if( j==0 ){ - //n with fm - if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){ - Trace("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; - Trace("qcf-reqr") << n << " " << fm << std::endl; - } - }else{ - //fn with fm - bool mltn = isLessThan( m, n ); - for( unsigned i=0; i<2; i++ ){ - if( i==0 || m.getOperator()==n.getOperator() ){ - Node am = ((i==0)==mltn) ? n : m; - Node an = ((i==0)==mltn) ? m : n; - if( itm->second->d_qni.addTermEq( an, am, d_arg_reps[n], d_arg_reps[m] ) ){ - Trace("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for "; - Trace("qcf-reqr") << fn << " " << fm << std::endl; + nTerms += isRedundant ? 0 : 1; + + Trace("qcf-reqr") << "^ Process " << n << std::endl; + //process all relevant equalities and disequalities to n + for( unsigned index=0; index<2; index++ ){ + std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator itn[2]; + itn[0] = d_eqr[index][0].find( n ); + if( !fn.isNull() ){ + itn[1] = d_eqr[index][1].find( fn ); + } + //for n, fn... + bool relevant = false; + for( unsigned j=0; j<2; j++ ){ + //if this node is relevant as an ground term or f-application + if( ( j==0 || !fn.isNull() ) && itn[j]!=d_eqr[index][j].end() ){ + relevant = true; + for( unsigned jj=0; jj<2; jj++ ){ + if( j==1 || jj==1 ){ + Trace("qcf-reqr") << "^^ " << index << " " << j << " " << jj << std::endl; + //check with others + for( std::map< TNode, EqRegistry * >::iterator itm = itn[j]->second[jj].begin(); itm != itn[j]->second[jj].end(); ++itm ){ + std::map< TNode, std::map< TNode, std::vector< TNode > > >::iterator itv = eqr_to_node[index].find( itm->first ); + if( itv!=eqr_to_node[index].end() ){ + //for( unsigned k=0; ksecond.size(); k++ ){ + for( std::map< TNode, std::vector< TNode > >::iterator itvr = itv->second.begin(); itvr != itv->second.end(); ++itvr ){ + TNode mr = itvr->first; + //Assert( j==0 || getFunction( m )==itm->first ); + nComp++; + //if it is equal or disequal to this + if( ( index==0 && mr==r ) || + ( index==1 && std::find( deqc.begin(), deqc.end(), mr )!=deqc.end() ) ){ + Debug("qcf-reqr") << "^^ Check with : " << itv->first << ", # = " << itvr->second.size() << std::endl; + for( unsigned k=0; ksecond.size(); k++ ){ + TNode m = itvr->second[k]; + Debug("qcf-reqr") << "Comparing " << n << " and " << m << ", j = " << j << ", index = " << index << std::endl; + Debug("qcf-reqr") << "Meets the criteria of " << itn[j]->first << " " << itm->first << std::endl; + //process equality/disequality + if( j==0 ){ + Assert( d_arg_reps.find( m )!=d_arg_reps.end() ); + //n with fm + nEq1t++; + if( itm->second->d_qni.addTerm( m, d_arg_reps[m] )==m ){ + nEq1++; + Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; + Debug("qcf-reqr") << n << " " << itm->first << std::endl; + } + }else{ + if( jj==0 ){ + //fn with m + nEq1t++; + if( itm->second->d_qni.addTerm( n, it_na->second )==n ){ + nEq1++; + Debug("qcf-reqr") << "Add relevant : " << n << (index==0?"":"!") << "=" << m << " for "; + Debug("qcf-reqr") << fn << " " << m << std::endl; + } + }else{ + Assert( d_arg_reps.find( m )!=d_arg_reps.end() ); + //fn with fm + bool mltn = isLessThan( itm->first, fn ); + for( unsigned i=0; i<2; i++ ){ + if( i==0 || itm->first==fn ){ + TNode am = ((i==0)==mltn) ? n : m; + TNode an = ((i==0)==mltn) ? m : n; + nEq2t++; + if( itm->second->d_qni.addTermEq( an, am, it_na->second, d_arg_reps[m] ) ){ + nEq2++; + Debug("qcf-reqr") << "Add relevant (eq) : " << an << (index==0?"":"!") << "=" << am << " for "; + Debug("qcf-reqr") << fn << " " << itm->first << std::endl; + } + } + } + } + } + } } } } } } } + Trace("qcf-reqr") << "- Node " << n << " is relevant for " << (j==0 ? n : fn) << ", index = " << index << std::endl; + //add it to relevant + eqr_to_node[index][j==0 ? n : fn][r].push_back( n ); } } - } - if( !relevant ){ - //if not relevant for disequalities, store it - if( index==1 ){ - irrelevant_dnode[n] = true; - } - }else{ - //if relevant for equalities, store it - if( index==0 ){ - eqc.push_back( n ); + if( !relevant ){ + //if not relevant for disequalities, store it + if( index==1 ){ + irrelevant_dnode[n] = true; + } + }else{ + //if relevant for equalities, store it + if( index==0 ){ + eqc.push_back( n ); + } } } } ++eqc_i; } - process_eqc[r] = true; + //process_eqc[r] = true; ++eqcs_i; } + if( Trace.isOn("qcf-opt") ){ + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("qcf-opt") << "Compute rel eqc : " << std::endl; + Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl; + Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl; + Trace("qcf-opt") << " " << nEq1 << " / " << nEq1t << " pattern terms." << std::endl; + Trace("qcf-opt") << " " << nEq2 << " / " << nEq2t << " pattern equalities." << std::endl; + Trace("qcf-opt") << " " << nComp << " compares." << std::endl; + Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl; + } } -void QuantConflictFind::computeArgReps( Node n ) { +void QuantConflictFind::computeArgReps( TNode n ) { if( d_arg_reps.find( n )==d_arg_reps.end() ){ + Assert( isHandledUfTerm( n ) ); for( unsigned j=0; j remDeq; - for( std::map< Node, int >::iterator it = d_curr_var_deq[vn].begin(); it != d_curr_var_deq[vn].end(); ++it ){ - if( it->second==v ){ - remDeq.push_back( it->first ); + std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( vn ); + if( itd!=d_curr_var_deq.end() ){ + //remove disequalities owned by this + std::vector< Node > remDeq; + for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){ + if( it->second==v ){ + remDeq.push_back( it->first ); + } + } + for( unsigned i=0; i addDeq; - for( std::map< Node, int >::iterator it = d_curr_var_deq[v].begin(); it != d_curr_var_deq[v].end(); ++it ){ - Node dv = getCurrentValue( it->first ); - if( !alreadySet ){ - if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){ - d_curr_var_deq[vn][dv] = v; - addDeq.push_back( dv ); - } - }else{ - if( itmn->second!=dv ){ - Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; - return -1; + std::map< int, std::map< Node, int > >::iterator itd = d_curr_var_deq.find( v ); + if( itd!=d_curr_var_deq.end() ){ + //std::vector< Node > addDeq; + for( std::map< Node, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){ + Node dv = getCurrentValue( it->first ); + if( !alreadySet ){ + if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){ + d_curr_var_deq[vn][dv] = v; + //addDeq.push_back( dv ); + } + }else{ + if( itmn->second!=dv ){ + Debug("qcf-match-debug") << " -> fail, conflicting disequality" << std::endl; + return -1; + } } } } @@ -1103,7 +1134,7 @@ bool QuantConflictFind::QuantInfo::completeMatch( QuantConflictFind * p, Node q, std::vector< TypeNode > unassigned_tn[2]; for( int i=0; id_qinfo[q].d_var_num.find( n )!=p->d_qinfo[q].d_var_num.end() ); - if( n.getKind()==APPLY_UF ){ + if( p->isHandledUfTerm( n ) ){ d_type = typ_var; //d_type_not = true; //implicit disequality, in disjunction at top level d_type_not = false; @@ -1277,7 +1308,7 @@ QuantConflictFind::MatchGen::MatchGen( QuantConflictFind * p, Node q, Node n, bo bool isValid = true; if( qni_apps.size()>0 ){ for( unsigned i=0; iisHandledUfTerm( qni_apps[i] ) ){ //for now, cannot handle anything besides uf isValid = false; qni_apps.clear(); @@ -1413,13 +1444,13 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q int vi = p->d_qinfo[q].getVarNum( d_n ); Assert( vi!=-1 ); int repVar = p->d_qinfo[q].getCurrentRepVar( vi ); - Assert( d_n.getKind()==APPLY_UF ); + Assert( p->isHandledUfTerm( d_n ) ); Node f = d_n.getOperator(); std::map< int, Node >::iterator it = p->d_qinfo[q].d_match.find( repVar ); if( it!=p->d_qinfo[q].d_match.end() && d_tgt ) { Debug("qcf-match") << " will be matching var within eqc = " << it->second << std::endl; //f-applications in the equivalence class in match[ repVar ] - std::map< Node, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f ); + std::map< TNode, QcfNodeIndex >::iterator itut = p->d_eqc_uf_terms[ it->second ].find( f ); if( itut!=p->d_eqc_uf_terms[ it->second ].end() ){ d_qn.push_back( &itut->second ); } @@ -1428,7 +1459,7 @@ void QuantConflictFind::MatchGen::reset( QuantConflictFind * p, bool tgt, Node q //we are binding rep var d_qni_bound_cons[repVar] = Node::null(); //must look at all f-applications - std::map< Node, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f ); + std::map< TNode, QcfNodeIndex >::iterator itut = p->d_uf_terms.find( f ); if( itut!=p->d_uf_terms.end() ){ d_qn.push_back( &itut->second ); } @@ -1655,7 +1686,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { }else{ //binding a variable d_qni_bound[index] = repVar; - std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin(); + std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.begin(); if( it != d_qn[index]->d_children.end() ) { d_qni.push_back( it ); //set the match @@ -1682,7 +1713,7 @@ bool QuantConflictFind::MatchGen::doMatching( QuantConflictFind * p, Node q ) { } if( !val.isNull() ){ //constrained by val - std::map< Node, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val ); + std::map< TNode, QcfNodeIndex >::iterator it = d_qn[index]->d_children.find( val ); if( it!=d_qn[index]->d_children.end() ){ Debug("qcf-match-debug") << " Match" << std::endl; d_qni.push_back( it ); @@ -1829,38 +1860,42 @@ void QuantConflictFind::debugPrint( const char * c ) { for( unsigned i=0; i<2; i++ ){ printed.clear(); Trace(c) << "----------EQR, polarity = " << (i==0) << std::endl; - for( std::map< Node, std::map< Node, EqRegistry * > >::iterator it = d_eqr[i].begin(); it != d_eqr[i].end(); ++it ){ - bool prHead = false; - for( std::map< Node, EqRegistry * >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - bool print; - if( it->first.getKind()==APPLY_UF && it2->first.getKind()==APPLY_UF && - it->first.getOperator()!=it2->first.getOperator() ){ - print = isLessThan( it->first, it2->first ); - }else{ - print = printed[it->first].find( it2->first )==printed[it->first].end(); - } - if( print ){ - printed[it->first][it2->first] = true; - printed[it2->first][it->first] = true; - if( !prHead ){ - Trace(c) << "- " << it->first << std::endl; - prHead = true; - } - Trace(c) << " " << it2->first << ", terms : " << std::endl; - - /* - Trace(c) << " " << it2->first << " : {"; - bool pr = false; - for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){ - if( (*it3).second ){ - Trace(c) << (pr ? "," : "" ) << " " << (*it3).first; - pr = true; + for( unsigned j=0; j<2; j++ ){ + for( std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > >::iterator it = d_eqr[i][j].begin(); it != d_eqr[i][j].end(); ++it ){ + bool prHead = false; + for( unsigned jj=0; jj<2; jj++ ){ + for( std::map< TNode, EqRegistry * >::iterator it2 = it->second[jj].begin(); it2 != it->second[jj].end(); ++it2 ){ + bool print; + if( isHandledUfTerm( it->first ) && isHandledUfTerm( it2->first ) && + it->first.getOperator()!=it2->first.getOperator() ){ + print = isLessThan( it->first.getOperator(), it2->first.getOperator() ); + }else{ + print = printed[it->first].find( it2->first )==printed[it->first].end(); + } + if( print ){ + printed[it->first][it2->first] = true; + printed[it2->first][it->first] = true; + if( !prHead ){ + Trace(c) << "- " << it->first << std::endl; + prHead = true; + } + Trace(c) << " " << it2->first << ", terms : " << std::endl; + + /* + Trace(c) << " " << it2->first << " : {"; + bool pr = false; + for( NodeBoolMap::iterator it3 = it2->second->d_t_eqc.begin(); it3 != it2->second->d_t_eqc.end(); ++it3 ){ + if( (*it3).second ){ + Trace(c) << (pr ? "," : "" ) << " " << (*it3).first; + pr = true; + } + } + Trace(c) << (pr ? " " : "" ) << "}" << std::endl; + */ + //print qni structure + it2->second->debugPrint( c, 3 ); } } - Trace(c) << (pr ? " " : "" ) << "}" << std::endl; - */ - //print qni structure - it2->second->debugPrint( c, 3 ); } } } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0b503d49b..657586d1a 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -31,16 +31,16 @@ class QuantConflictFind; class QcfNodeIndex { public: - std::map< Node, QcfNodeIndex > d_children; + std::map< TNode, QcfNodeIndex > d_children; void clear() { d_children.clear(); } //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 ); //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 ); //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 ); void debugPrint( const char * c, int t ); //optimized versions - Node existsTerm( Node n, std::vector< Node >& reps, int index = 0 ); - Node addTerm( Node n, std::vector< Node >& reps, int index = 0 ); - bool addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index = 0 ); + Node existsTerm( TNode n, std::vector< TNode >& reps, int index = 0 ); + Node addTerm( TNode n, std::vector< TNode >& reps, int index = 0 ); + bool addTermEq( TNode n1, TNode n2, std::vector< TNode >& reps1, std::vector< TNode >& reps2, int index = 0 ); }; class EqRegistry { @@ -91,14 +91,14 @@ private: std::map< Node, Node > d_op_node; int getFunctionId( Node f ); bool isLessThan( Node a, Node b ); - Node getFunction( Node n, bool isQuant = false ); + Node getFunction( Node n, int& index, bool isQuant = false ); int d_fid_count; std::map< Node, int > d_fid; Node mkEqNode( Node a, Node b ); private: //for ground terms Node d_true; Node d_false; - std::map< Node, std::map< Node, EqRegistry * > > d_eqr[2]; + std::map< int, std::map< TNode, std::map< int, std::map< TNode, EqRegistry * > > > > d_eqr[2]; EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true ); void getEqRegistryApps( Node lit, std::vector< Node >& terms ); int evaluate( Node n ); @@ -114,7 +114,7 @@ public: //for quantifiers MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } //current matching information std::vector< QcfNodeIndex * > d_qn; - std::vector< std::map< Node, QcfNodeIndex >::iterator > d_qni; + std::vector< std::map< TNode, QcfNodeIndex >::iterator > d_qni; bool doMatching( QuantConflictFind * p, Node q ); //for matching : each index is either a variable or a ground term unsigned d_qni_size; @@ -200,15 +200,17 @@ private: //for equivalence classes std::map< Node, EqcInfo * > d_eqc_info; EqcInfo * getEqcInfo( Node n, bool doCreate = true ); // operator -> index(terms) - std::map< Node, QcfNodeIndex > d_uf_terms; + std::map< TNode, QcfNodeIndex > d_uf_terms; // eqc x operator -> index(terms) - std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms; + std::map< TNode, std::map< TNode, QcfNodeIndex > > d_eqc_uf_terms; // type -> list(eqc) - std::map< TypeNode, std::vector< Node > > d_eqcs; + std::map< TypeNode, std::vector< TNode > > d_eqcs; //mapping from UF terms to representatives of their arguments - std::map< Node, std::vector< Node > > d_arg_reps; + std::map< TNode, std::vector< TNode > > d_arg_reps; //compute arg reps - void computeArgReps( Node n ); + void computeArgReps( TNode n ); + // is this term treated as UF application? + bool isHandledUfTerm( TNode n ); public: QuantConflictFind( QuantifiersEngine * qe, context::Context* c ); -- 2.30.2