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; i<f[0].getNumChildren(); i++ ){
- Node val = get( i );
- if( val.isNull() ){
- Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
- val = qe->getTermDatabase()->getModelBasisTerm( ic.getType() );
- }
- inst.push_back( val );
+ inst.push_back( d_vals[i] );
}
}
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 );
}
};
+struct sortTriggers {
+ bool operator() (Node i, Node j) {
+ if( Trigger::isAtomicTrigger( i ) ){
+ return i<j || !Trigger::isAtomicTrigger( j );
+ }else{
+ return i<j && !Trigger::isAtomicTrigger( j );
+ }
+ }
+};
+
void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
//reset triggers
for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
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() ){
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;
}
//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() ){
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; i<patTermsF.size(); i++ ){
+ d_quantEngine->getTermDatabase()->getVarContainsNode( f, patTermsF[i], varContains[ patTermsF[i] ] );
+ bool newVar = false;
+ for( unsigned j=0; j<varContains[ patTermsF[i] ].size(); j++ ){
+ if( vcMap.find( varContains[ patTermsF[i] ][j] )==vcMap.end() ){
+ vcMap[varContains[ patTermsF[i] ][j]] = true;
+ newVar = true;
+ }
+ }
+ if( ntrivTriggers && !newVar && !Trigger::isAtomicTrigger( patTermsF[i] ) ){
+ Trace("auto-gen-trigger-debug") << "Exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
+ rmPatTermsF[patTermsF[i]] = true;
+ }
+ }
for( std::map< Node, std::vector< Node > >::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; i<d_patTerms[0][f].size(); i++ ){
+ Trace("auto-gen-trigger") << " " << d_patTerms[0][f][i] << std::endl;
}
- Trace("auto-gen-trigger") << std::endl;
- Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
- Trace("auto-gen-trigger") << " ";
- for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){
- Trace("auto-gen-trigger") << d_patTerms[1][f][i] << " ";
+ if( !d_patTerms[1][f].empty() ){
+ Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
+ for( unsigned i=0; i<d_patTerms[1][f].size(); i++ ){
+ Trace("auto-gen-trigger") << " " << d_patTerms[1][f][i] << std::endl;
+ }
}
- Trace("auto-gen-trigger") << std::endl;
}
unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
- unsigned rmax = ( options::multiTriggerWhenSingle() || e>2 ) ? 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++ ){
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
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;
for( int i=0; i<d_quantEngine->getModel()->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++;
}
}
}
-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;
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<f[0].getNumChildren(); i++ ){
+ unsigned ts;
if( r==0 ){
- Trace("inst-alg") << "-> 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; i<f[0].getNumChildren(); i++ ){
- unsigned ts;
- if( r==0 ){
- ts = rd->getRDomain( 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 ){
}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( nv<maxs[index] && nv<=max_i &&
- r==1 && quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+ quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
nv++;
}
}
//try instantiation
std::vector< Node > terms;
for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
- if( r==0 ){
+ if( max_zero[i] ){
+ //no terms available, will report incomplete instantiation
+ terms.push_back( Node::null() );
+ }else if( r==0 ){
terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
}else{
terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
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 );
/** 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(){}
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 );
}
}
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(){
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; i<d_model->getNumAssertedQuantifiers(); 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;
}
}
-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<n.getNumChildren(); i++ ){
if( !op.isNull() ){
computeRelevantDomainOpCh( rf, n[i] );
}
}
- //TODO
if( n[i].getKind()!=FORALL ){
bool newHasPol;
bool newPol;
QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- computeRelevantDomain( n[i], newHasPol, newPol );
+ computeRelevantDomain( q, n[i], newHasPol, newPol );
}
}
- if( n.getKind()==EQUAL || n.getKind()==GEQ ){
- int varCount = 0;
- std::vector< RDomain * > rds;
- int varCh = -1;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( n[i].getKind()==INST_CONSTANT ){
- Node q = d_qe->getTermDatabase()->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; i<d_rel_dom_lit[hasPol][pol][n].d_val.size(); i++ ){
+ rd->addTerm( d_rel_dom_lit[hasPol][pol][n].d_val[i] );
}
}
}
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<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==INST_CONSTANT ){
+ d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain( q, n[i].getAttribute(InstVarNumAttribute()), false );
+ varCount++;
+ varCh = i;
+ }else{
+ d_rel_dom_lit[hasPol][pol][n].d_rd[i] = NULL;
}
- ++eqc;
}
- //otherwise, may be equal to some non-ground term
-
- return r;
+
+ Node r_add;
+ bool varLhs = true;
+ if( varCount==2 ){
+ d_rel_dom_lit[hasPol][pol][n].d_merge = true;
+ }else{
+ if( varCount==1 ){
+ r_add = n[1-varCh];
+ varLhs = (varCh==0);
+ d_rel_dom_lit[hasPol][pol][n].d_rd[0] = d_rel_dom_lit[hasPol][pol][n].d_rd[varCh];
+ d_rel_dom_lit[hasPol][pol][n].d_rd[1] = NULL;
+ }else{
+ //solve the inequality for one/two variables, if possible
+ std::map< Node, Node > 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;
+ }
}
}
-*/
+
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(); }
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(){}
//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 */
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 );
}
Assert( terms.size()==q[0].getNumChildren() );
Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
- Trace("inst-add-debug") << " " << q[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
//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() );
}
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
}
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")) {
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() ){
projects / cvc5.git / commitdiff