From 6c49fe8691cf011237be30f4062affc79d8a5314 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 17 Nov 2015 16:41:56 +0100 Subject: [PATCH] Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings. --- src/theory/quantifiers/inst_match.cpp | 9 +- src/theory/quantifiers/inst_match.h | 2 +- .../quantifiers/inst_strategy_e_matching.cpp | 157 ++++++++------ .../quantifiers/inst_strategy_e_matching.h | 4 +- src/theory/quantifiers/relevant_domain.cpp | 191 +++++++++++------- src/theory/quantifiers/relevant_domain.h | 20 +- src/theory/quantifiers_engine.cpp | 10 +- src/theory/strings/options | 3 + src/theory/strings/theory_strings.cpp | 4 +- 9 files changed, 247 insertions(+), 153 deletions(-) diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 180ccc448..5eca87903 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -118,14 +118,9 @@ Node InstMatch::get( int i ) { return d_vals[i]; } -void InstMatch::getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ){ +void InstMatch::getTerms( Node f, std::vector< Node >& inst ){ for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); - val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() ); - } - inst.push_back( val ); + inst.push_back( d_vals[i] ); } } diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 6424b67d3..d66d331e5 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -76,7 +76,7 @@ public: void applyRewrite(); /** get */ Node get( int i ); - void getTerms( QuantifiersEngine* qe, Node f, std::vector< Node >& inst ); + void getTerms( Node f, std::vector< Node >& inst ); /** set */ void setValue( int i, TNode n ); bool set( QuantifiersEngine* qe, int i, TNode n ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 09cf9d2eb..9237d95c2 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -49,6 +49,16 @@ struct sortQuantifiersForSymbol { } }; +struct sortTriggers { + bool operator() (Node i, Node j) { + if( Trigger::isAtomicTrigger( i ) ){ + return i >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){ @@ -168,7 +178,6 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) return STATUS_UNFINISHED; }else{ Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl; - int status = STATUS_UNKNOWN; bool gen = false; if( e==peffort ){ if( d_counter.find( f )==d_counter.end() ){ @@ -182,7 +191,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) gen = true; } if( gen ){ - generateTriggers( f, effort, e, status ); + generateTriggers( f ); if( d_counter[f]==0 && d_auto_gen_trigger[0][f].empty() && d_auto_gen_trigger[1][f].empty() && f.getNumChildren()==2 ){ Trace("trigger-warn") << "Could not find trigger for " << f << std::endl; } @@ -222,17 +231,18 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ) //if( e==4 ){ // d_quantEngine->getEqualityQuery()->setLiberal( false ); //} - return status; + return STATUS_UNKNOWN; } } } -void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effort, int e, int & status ){ - Trace("auto-gen-trigger-debug") << "Generate trigger for " << f << std::endl; +void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ + Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << std::endl; if( d_patTerms[0].find( f )==d_patTerms[0].end() ){ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); + bool ntrivTriggers = options::relationalTriggers(); std::vector< Node > patTermsF; //well-defined function: can assume LHS is only trigger if( options::quantFunWellDefined() ){ @@ -246,42 +256,61 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor if( patTermsF.empty() ){ Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); Trigger::collectPatTerms( d_quantEngine, f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], true ); - Trace("auto-gen-trigger") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; - Trace("auto-gen-trigger") << " "; + Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; + Trace("auto-gen-trigger-debug") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ - Trace("auto-gen-trigger") << patTermsF[i] << " "; + Trace("auto-gen-trigger-debug") << patTermsF[i] << " "; + } + Trace("auto-gen-trigger-debug") << std::endl; + if( ntrivTriggers ){ + sortTriggers st; + std::sort( patTermsF.begin(), patTermsF.end(), st ); } - Trace("auto-gen-trigger") << std::endl; } //sort into single/multi triggers std::map< Node, std::vector< Node > > varContains; - d_quantEngine->getTermDatabase()->getVarContains( f, patTermsF, varContains ); + std::map< Node, bool > vcMap; + std::map< Node, bool > rmPatTermsF; + for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] ); + bool newVar = false; + for( unsigned j=0; j >::iterator it = varContains.begin(); it != varContains.end(); ++it ){ - if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){ - d_patTerms[0][f].push_back( it->first ); - d_is_single_trigger[ it->first ] = true; - }else{ - d_patTerms[1][f].push_back( it->first ); - d_is_single_trigger[ it->first ] = false; + if( rmPatTermsF.find( it->first )==rmPatTermsF.end() ){ + if( it->second.size()==f[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( it->first ) ) ){ + d_patTerms[0][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = true; + }else{ + d_patTerms[1][f].push_back( it->first ); + d_is_single_trigger[ it->first ] = false; + } } } d_made_multi_trigger[f] = false; Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl; - Trace("auto-gen-trigger") << " "; - for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){ - Trace("auto-gen-trigger") << d_patTerms[0][f][i] << " "; + for( unsigned i=0; i2 ) ? 1 : rmin; + unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin; for( unsigned r=rmin; r<=rmax; r++ ){ std::vector< Node > patTerms; for( int i=0; i<(int)d_patTerms[r][f].size(); i++ ){ @@ -310,13 +339,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effor tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); d_single_trigger_gen[ patTerms[0] ] = true; }else{ - //only generate multi trigger if effort level > 5, or if no single triggers exist + //only generate multi trigger if option set, or if no single triggers exist if( !d_patTerms[0][f].empty() ){ - if( e<=5 && !options::multiTriggerWhenSingle() ){ - status = STATUS_UNFINISHED; - return; - }else{ + if( options::multiTriggerWhenSingle() ){ Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl; + }else{ + return; } } //if we are re-generating triggers, shuffle based on some method @@ -471,12 +499,14 @@ void FullSaturation::reset_round( Theory::Effort e ) { void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { bool doCheck = false; + bool fullEffort = false; if( options::fullSaturateInst() ){ //we only add when interleaved with other strategies doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); } if( options::fullSaturateQuant() && !doCheck ){ doCheck = quant_e==QuantifiersEngine::QEFFORT_LAST_CALL; + fullEffort = !d_quantEngine->hasAddedLemma(); } if( doCheck ){ double clSet = 0; @@ -488,7 +518,7 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { for( int i=0; igetModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ - if( process( q, e, quant_e ) ){ + if( process( q, fullEffort ) ){ //added lemma addedLemmas++; } @@ -502,13 +532,13 @@ void FullSaturation::check( Theory::Effort e, unsigned quant_e ) { } } -bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){ +bool FullSaturation::process( Node f, bool fullEffort ){ //first, try from relevant domain RelevantDomain * rd = d_quantEngine->getRelevantDomain(); unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - unsigned rend = quant_e==QuantifiersEngine::QEFFORT_STANDARD ? rstart : 2; + unsigned rend = fullEffort ? 1 : rstart; for( unsigned r=rstart; r<=rend; r++ ){ - if( r==1 ){ + /* //complete guess if( d_guessed.find( f )==d_guessed.end() ){ Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl; @@ -519,38 +549,40 @@ bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){ return true; } } - }else{ - if( rd || r>0 ){ + */ + if( rd || r>0 ){ + if( r==0 ){ + Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl; + }else{ + Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + } + rd->compute(); + unsigned final_max_i = 0; + std::vector< unsigned > maxs; + std::vector< bool > max_zero; + bool has_zero = false; + for(unsigned i=0; i Relevant domain instantiate " << f << "..." << std::endl; + ts = rd->getRDomain( f, i )->d_terms.size(); }else{ - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl; + ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); } - rd->compute(); - bool max_zero = false; - unsigned final_max_i = 0; - std::vector< unsigned > maxs; - for(unsigned i=0; igetRDomain( f, i )->d_terms.size(); - }else{ - ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size(); - } + max_zero.push_back( fullEffort && ts==0 ); + ts = ( fullEffort && ts==0 ) ? 1 : ts; + Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; + if( ts==0 ){ + has_zero = true; + break; + }else{ maxs.push_back( ts ); - Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl; if( ts>final_max_i ){ final_max_i = ts; } - if( ts==0 ){ - max_zero = true; - } - } - if( max_zero ){ - final_max_i = 0; } + } + if( !has_zero ){ Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl; - unsigned max_i = 0; bool success; while( max_i<=final_max_i ){ @@ -564,10 +596,10 @@ bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){ }else{ Assert( index==(int)(childIndex.size())-1 ); unsigned nv = childIndex[index]+1; - if( options::cbqi() ){ + if( options::cbqi() && r==1 && !max_zero[index] ){ //skip inst constant nodes while( nvgetTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ + quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){ nv++; } } @@ -590,7 +622,10 @@ bool FullSaturation::process( Node f, Theory::Effort effort, unsigned quant_e ){ //try instantiation std::vector< Node > terms; for( unsigned i=0; igetRDomain( f, i )->d_terms[childIndex[i]] ); }else{ terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] ); diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index e9eed800e..2f7e7dcf1 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -87,7 +87,7 @@ private: void processResetInstantiationRound( Theory::Effort effort ); int process( Node q, Theory::Effort effort, int e ); /** generate triggers */ - void generateTriggers( Node q, Theory::Effort effort, int e, int& status ); + void generateTriggers( Node q ); //bool addTrigger( inst::Trigger * tr, Node f, unsigned r ); /** has user patterns */ bool hasUserPatterns( Node q ); @@ -110,7 +110,7 @@ private: /** guessed instantiations */ std::map< Node, bool > d_guessed; /** process functions */ - bool process( Node q, Theory::Effort effort, unsigned quant_e ); + bool process( Node q, bool fullEffort ); public: FullSaturation( QuantifiersEngine* qe ); ~FullSaturation(){} diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 49bbe5680..88793358e 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -34,15 +34,9 @@ void RelevantDomain::RDomain::merge( RDomain * r ) { d_terms.clear(); } -void RelevantDomain::RDomain::addTerm( Node t, bool nonGround ) { - if( !nonGround ){ - if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ - d_terms.push_back( t ); - } - }else{ - if( std::find( d_ng_terms.begin(), d_ng_terms.end(), t )==d_ng_terms.end() ){ - d_ng_terms.push_back( t ); - } +void RelevantDomain::RDomain::addTerm( Node t ) { + if( std::find( d_terms.begin(), d_terms.end(), t )==d_terms.end() ){ + d_terms.push_back( t ); } } @@ -79,13 +73,13 @@ RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_ d_is_computed = false; } -RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i ) { +RelevantDomain::RDomain * RelevantDomain::getRDomain( Node n, int i, bool getParent ) { if( d_rel_doms.find( n )==d_rel_doms.end() || d_rel_doms[n].find( i )==d_rel_doms[n].end() ){ d_rel_doms[n][i] = new RDomain; d_rn_map[d_rel_doms[n][i]] = n; d_ri_map[d_rel_doms[n][i]] = i; } - return d_rel_doms[n][i]->getParent(); + return getParent ? d_rel_doms[n][i]->getParent() : d_rel_doms[n][i]; } void RelevantDomain::reset(){ @@ -100,11 +94,11 @@ void RelevantDomain::compute(){ it2->second->reset(); } } - for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ - Node f = d_model->getAssertedQuantifier( i ); - Node icf = d_qe->getTermDatabase()->getInstConstantBody( f ); + for( int i=0; igetNumAssertedQuantifiers(); i++ ){ + Node q = d_model->getAssertedQuantifier( i ); + Node icf = d_qe->getTermDatabase()->getInstConstantBody( q ); Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl; - computeRelevantDomain( icf, true, true ); + computeRelevantDomain( q, icf, true, true ); } Trace("rel-dom-debug") << "account for ground terms" << std::endl; @@ -145,7 +139,7 @@ void RelevantDomain::compute(){ } } -void RelevantDomain::computeRelevantDomain( Node n, bool hasPol, bool pol ) { +void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ) { Node op = d_qe->getTermDatabase()->getOperator( n ); for( unsigned i=0; i rds; - int varCh = -1; - for( unsigned i=0; igetTermDatabase()->getInstConstAttr( n[i] ); - unsigned id = n[i].getAttribute(InstVarNumAttribute()); - rds.push_back( getRDomain( q, id ) ); - varCount++; - varCh = i; - }else{ - rds.push_back( NULL ); - } - } - if( varCount==2 ){ - //merge the two relevant domains - if( ( !hasPol || pol ) && rds[0]!=rds[1] ){ - rds[0]->merge( rds[1] ); + if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) && TermDb::hasInstConstAttr( n ) ){ + //compute the information for what this literal does + computeRelevantDomainLit( q, hasPol, pol, n ); + if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ + Assert( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL && d_rel_dom_lit[hasPol][pol][n].d_rd[1]!=NULL ); + RDomain * rd1 = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent(); + RDomain * rd2 = d_rel_dom_lit[hasPol][pol][n].d_rd[1]->getParent(); + if( rd1!=rd2 ){ + rd1->merge( rd2 ); } - }else if( varCount==1 ){ - int oCh = varCh==0 ? 1 : 0; - bool ng = d_qe->getTermDatabase()->hasInstConstAttr( n[oCh] ); - Trace("rel-dom-debug") << "...add term " << n[oCh] << ", is ground = " << (!ng) << ", pol = " << pol << ", hasPol = " << hasPol << ", kind = " << n.getKind() << std::endl; - //the negative occurrence adds the term to the domain - if( !hasPol || !pol ){ - rds[varCh]->addTerm( n[oCh], ng ); - } - //the positive occurence adds other terms - if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - rds[varCh]->addTerm( QuantArith::offset( n[oCh], i==0 ? 1 : -1 ), ng ); - } - }else if( n.getKind()==GEQ ){ - rds[varCh]->addTerm( QuantArith::offset( n[oCh], varCh==0 ? 1 : -1 ), ng ); + }else{ + if( d_rel_dom_lit[hasPol][pol][n].d_rd[0]!=NULL ){ + RDomain * rd = d_rel_dom_lit[hasPol][pol][n].d_rd[0]->getParent(); + for( unsigned i=0; iaddTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] ); } } } @@ -220,32 +192,107 @@ void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) { if( rf!=rq ){ rq->merge( rf ); } - }else if( !d_qe->getTermDatabase()->hasInstConstAttr( n ) ){ + }else if( !TermDb::hasInstConstAttr( n ) ){ Trace("rel-dom-debug") << "...add ground term to rel dom " << n << std::endl; //term to add rf->addTerm( n ); } } -/* -Node RelevantDomain::getRelevantTerm( Node f, int i, Node r ) { - RDomain * rf = getRDomain( f, i ); - Trace("rel-dom-debug") << "Get relevant domain " << rf << " " << r << std::endl; - if( !d_qe->getEqualityQuery()->getEngine()->hasTerm( r ) || rf->hasTerm( r ) ){ - return r; - }else{ - Node rr = d_model->getRepresentative( r ); - eq::EqClassIterator eqc( rr, d_qe->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - if( rf->hasTerm( en ) ){ - return en; +void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ) { + if( d_rel_dom_lit[hasPol][pol].find( n )==d_rel_dom_lit[hasPol][pol].end() ){ + d_rel_dom_lit[hasPol][pol][n].d_merge = false; + int varCount = 0; + int varCh = -1; + for( unsigned i=0; i msum; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + Node var; + Node var2; + bool hasNonVar = false; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){ + if( var.isNull() ){ + var = it->first; + }else if( var2.isNull() ){ + var2 = it->first; + }else{ + hasNonVar = true; + } + }else{ + hasNonVar = true; + } + } + if( !var.isNull() ){ + if( var2.isNull() ){ + //single variable solve + Node veq_c; + Node val; + int ires = QuantArith::isolate( var, msum, veq_c, val, n.getKind() ); + if( ires!=0 ){ + if( veq_c.isNull() ){ + r_add = val; + varLhs = (ires==1); + d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false ); + d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL; + } + } + }else if( !hasNonVar ){ + //merge the domains + d_rel_dom_lit[hasPol][pol][n].d_rd[0] = getRDomain( q, var.getAttribute(InstVarNumAttribute()), false ); + d_rel_dom_lit[hasPol][pol][n].d_rd[1] = getRDomain( q, var2.getAttribute(InstVarNumAttribute()), false ); + d_rel_dom_lit[hasPol][pol][n].d_merge = true; + } + } + } + } + } + if( d_rel_dom_lit[hasPol][pol][n].d_merge ){ + //do not merge if constant negative polarity + if( hasPol && !pol ){ + d_rel_dom_lit[hasPol][pol][n].d_merge = false; + } + }else if( !r_add.isNull() && !TermDb::hasInstConstAttr( r_add ) ){ + Trace("rel-dom-debug") << "...add term " << r_add << ", pol = " << pol << ", kind = " << n.getKind() << std::endl; + //the negative occurrence adds the term to the domain + if( !hasPol || !pol ){ + d_rel_dom_lit[hasPol][pol][n].d_val.push_back( r_add ); + } + //the positive occurence adds other terms + if( ( !hasPol || pol ) && n[0].getType().isInteger() ){ + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, i==0 ? 1 : -1 ) ); + } + }else if( n.getKind()==GEQ ){ + d_rel_dom_lit[hasPol][pol][n].d_val.push_back( QuantArith::offset( r_add, varLhs ? 1 : -1 ) ); + } + } + }else{ + d_rel_dom_lit[hasPol][pol][n].d_rd[0] = NULL; + d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL; + } } } -*/ + diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 25c821e10..3ce285bc8 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -33,9 +33,8 @@ private: void reset() { d_parent = NULL; d_terms.clear(); } RDomain * d_parent; std::vector< Node > d_terms; - std::vector< Node > d_ng_terms; void merge( RDomain * r ); - void addTerm( Node t, bool nonGround = false ); + void addTerm( Node t ); RDomain * getParent(); void removeRedundantTerms( QuantifiersEngine * qe ); bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } @@ -45,9 +44,21 @@ private: std::map< RDomain *, int > d_ri_map; QuantifiersEngine* d_qe; FirstOrderModel* d_model; - void computeRelevantDomain( Node n, bool hasPol, bool pol ); + void computeRelevantDomain( Node q, Node n, bool hasPol, bool pol ); void computeRelevantDomainOpCh( RDomain * rf, Node n ); bool d_is_computed; + + //what each literal does + class RDomainLit { + public: + RDomainLit() : d_merge(false){} + ~RDomainLit(){} + bool d_merge; + RDomain * d_rd[2]; + std::vector< Node > d_val; + }; + std::map< bool, std::map< bool, std::map< Node, RDomainLit > > > d_rel_dom_lit; + void computeRelevantDomainLit( Node q, bool hasPol, bool pol, Node n ); public: RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); virtual ~RelevantDomain(){} @@ -55,8 +66,7 @@ public: //compute the relevant domain void compute(); - RDomain * getRDomain( Node n, int i ); - //Node getRelevantTerm( Node f, int i, Node r ); + RDomain * getRDomain( Node n, int i, bool getParent = true ); };/* class RelevantDomain */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 584295c17..2c4c58900 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -899,7 +899,7 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool modInst, bool doVts ){ std::vector< Node > terms; - m.getTerms( this, q, terms ); + m.getTerms( q, terms ); return addInstantiation( q, terms, mkRep, modEq, modInst, doVts ); } @@ -910,7 +910,11 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo Assert( terms.size()==q[0].getNumChildren() ); Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; for( unsigned i=0; i " << terms[i] << std::endl; + Trace("inst-add-debug") << " " << q[0][i]; + Trace("inst-add-debug2") << " -> " << terms[i]; + if( terms[i].isNull() ){ + terms[i] = d_term_db->getModelBasisTerm( q[0][i].getType() ); + } //make it representative, this is helpful for recognizing duplication if( mkRep ){ //pick the best possible representative for instantiation, based on past use and simplicity of term @@ -919,7 +923,7 @@ bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bo //ensure the type is correct terms[i] = quantifiers::TermDb::mkNodeType( terms[i], q[0][i].getType() ); } - Trace("inst-add-debug2") << " -> " << terms[i] << std::endl; + Trace("inst-add-debug") << " -> " << terms[i] << std::endl; Assert( !terms[i].isNull() ); } diff --git a/src/theory/strings/options b/src/theory/strings/options index e44f388f4..59a95e5ec 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -16,6 +16,9 @@ option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predic option stringFMF strings-fmf --strings-fmf bool :default false :read-write the finite model finding used by the theory of strings + +option stringEager strings-eager --strings-eager bool :default false + strings eager check option stringEIT strings-eit --strings-eit bool :default false the eager intersection used by the theory of strings diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 630b2ae65..d4a3cf9c5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -527,7 +527,7 @@ void TheoryStrings::check(Effort e) { } doPendingFacts(); - if( e == EFFORT_FULL && !d_conflict && !d_valuation.needCheck() ) { + if( !d_conflict && ( ( e == EFFORT_FULL && !d_valuation.needCheck() ) || ( e==EFFORT_STANDARD && options::stringEager() ) ) ) { Trace("strings-check") << "Theory of strings full effort check " << std::endl; if(Trace.isOn("strings-eqc")) { @@ -573,7 +573,7 @@ void TheoryStrings::check(Effort e) { if( !hasProcessed() ){ checkFlatForms(); Trace("strings-process") << "Done check flat forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; - if( !hasProcessed() ){ + if( !hasProcessed() && e==EFFORT_FULL ){ checkNormalForms(); Trace("strings-process") << "Done check normal forms, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl; if( !hasProcessed() ){ -- 2.30.2