}while( !d_conflict && addedFact );
Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
if( !d_conflict ){
- Trace("dt-model-test") << std::endl;
- printModelDebug("dt-model-test");
+ Trace("dt-model-debug") << std::endl;
+ printModelDebug("dt-model-debug");
}
}
d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
}
-bool InstStrategySimplex::calculateShouldProcess( Node f ){
- //DO_THIS
- return false;
-}
-
void getInstantiationConstants( Node n, std::vector< Node >& ics ){
if( n.getKind()==INST_CONSTANT ){
if( std::find( ics.begin(), ics.end(), n )==ics.end() ){
void InstStrategySimplex::processResetInstantiationRound( Theory::Effort effort ){
Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
+ d_quantActive.clear();
d_instRows.clear();
d_tableaux_term.clear();
d_tableaux.clear();
if( e<2 ){
return STATUS_UNFINISHED;
}else if( e==2 ){
- //the point instantiation
- InstMatch m_point( f );
- bool m_point_valid = true;
- int lem = 0;
- //scan over all instantiation rows
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
- Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
- for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
- ArithVar x = d_instRows[ic][j];
- if( !d_ceTableaux[ic][x].empty() ){
- if( Debug.isOn("quant-arith-simplex") ){
- Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
- Debug("quant-arith-simplex") << " ";
- for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
- if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
- Debug("quant-arith-simplex") << it->first << " * " << it->second;
- }
- Debug("quant-arith-simplex") << " = ";
- Node v = getTableauxValue( x, false );
- Debug("quant-arith-simplex") << v << std::endl;
- Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl;
- Debug("quant-arith-simplex") << " ce-term : ";
- for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
- if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
- Debug("quant-arith-simplex") << it->first << " * " << it->second;
- }
- Debug("quant-arith-simplex") << std::endl;
- }
- //instantiation row will be A*e + B*t = beta,
- // where e is a vector of terms , and t is vector of ground terms.
- // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
- // We will construct the term ( beta - B*t)/coeff to use for e_i.
- InstMatch m( f );
- for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
- if( f[0][k].getType().isInteger() ){
- m.setValue( k, d_zero );
+ if( d_quantActive.find( f )!=d_quantActive.end() ){
+ //the point instantiation
+ InstMatch m_point( f );
+ bool m_point_valid = true;
+ int lem = 0;
+ //scan over all instantiation rows
+ for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
+ Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
+ for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+ ArithVar x = d_instRows[ic][j];
+ if( !d_ceTableaux[ic][x].empty() ){
+ if( Debug.isOn("quant-arith-simplex") ){
+ Debug("quant-arith-simplex") << "--- Check row " << ic << " " << x << std::endl;
+ Debug("quant-arith-simplex") << " ";
+ for( std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin(); it != d_ceTableaux[ic][x].end(); ++it ){
+ if( it!=d_ceTableaux[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
+ }
+ Debug("quant-arith-simplex") << " = ";
+ Node v = getTableauxValue( x, false );
+ Debug("quant-arith-simplex") << v << std::endl;
+ Debug("quant-arith-simplex") << " term : " << d_tableaux_term[ic][x] << std::endl;
+ Debug("quant-arith-simplex") << " ce-term : ";
+ for( std::map< Node, Node >::iterator it = d_tableaux_ce_term[ic][x].begin(); it != d_tableaux_ce_term[ic][x].end(); it++ ){
+ if( it!=d_tableaux_ce_term[ic][x].begin() ){ Debug("quant-arith-simplex") << " + "; }
+ Debug("quant-arith-simplex") << it->first << " * " << it->second;
+ }
+ Debug("quant-arith-simplex") << std::endl;
}
- }
- //By default, choose the first instantiation constant to be e_i.
- Node var = d_ceTableaux[ic][x].begin()->first;
- //if it is integer, we need to find variable with coefficent +/- 1
- if( var.getType().isInteger() ){
- std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
- while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
- ++it;
- if( it==d_ceTableaux[ic][x].end() ){
- var = Node::null();
- }else{
- var = it->first;
+ //instantiation row will be A*e + B*t = beta,
+ // where e is a vector of terms , and t is vector of ground terms.
+ // Say one term in A*e is coeff*e_i, where e_i is an instantiation constant
+ // We will construct the term ( beta - B*t)/coeff to use for e_i.
+ InstMatch m( f );
+ for( unsigned k=0; k<f[0].getNumChildren(); k++ ){
+ if( f[0][k].getType().isInteger() ){
+ m.setValue( k, d_zero );
}
}
- //Otherwise, try one that divides all ground term coefficients?
- // Might be futile, if rewrite ensures gcd of coeffs is 1.
- }
- if( !var.isNull() ){
- //add to point instantiation if applicable
- if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
- Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
- Node v = getTableauxValue( x, false );
- if( !var.getType().isInteger() || v.getType().isInteger() ){
- m_point.setValue( i, v );
- }else{
- m_point_valid = false;
+ //By default, choose the first instantiation constant to be e_i.
+ Node var = d_ceTableaux[ic][x].begin()->first;
+ //if it is integer, we need to find variable with coefficent +/- 1
+ if( var.getType().isInteger() ){
+ std::map< Node, Node >::iterator it = d_ceTableaux[ic][x].begin();
+ while( !var.isNull() && !d_ceTableaux[ic][x][var].isNull() && d_ceTableaux[ic][x][var]!=d_negOne ){
+ ++it;
+ if( it==d_ceTableaux[ic][x].end() ){
+ var = Node::null();
+ }else{
+ var = it->first;
+ }
}
+ //Otherwise, try one that divides all ground term coefficients?
+ // Might be futile, if rewrite ensures gcd of coeffs is 1.
}
- Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
- if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
- lem++;
+ if( !var.isNull() ){
+ //add to point instantiation if applicable
+ if( d_tableaux_ce_term[ic][x].empty() && d_tableaux_term[ic][x]==d_zero ){
+ Debug("quant-arith-simplex") << "*** Row contributes to point instantiation." << std::endl;
+ Node v = getTableauxValue( x, false );
+ if( !var.getType().isInteger() || v.getType().isInteger() ){
+ m_point.setValue( i, v );
+ }else{
+ m_point_valid = false;
+ }
+ }
+ Debug("quant-arith-simplex") << "Instantiate with var " << var << std::endl;
+ if( doInstantiation( f, ic, d_tableaux_term[ic][x], x, m, var ) ){
+ lem++;
+ }
+ }else{
+ Debug("quant-arith-simplex") << "Could not find var." << std::endl;
}
- }else{
- Debug("quant-arith-simplex") << "Could not find var." << std::endl;
}
}
}
- }
- if( lem==0 && m_point_valid ){
- if( d_quantEngine->addInstantiation( f, m_point ) ){
- Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+ if( lem==0 && m_point_valid ){
+ if( d_quantEngine->addInstantiation( f, m_point ) ){
+ Debug("quant-arith-simplex") << "...added point instantiation." << std::endl;
+ }
}
}
}
class InstStrategySimplex : public InstStrategy{
-protected:
- /** calculate if we should process this quantifier */
- bool calculateShouldProcess( Node f );
private:
/** reference to theory arithmetic */
arith::TheoryArith* d_th;
+ /** quantifiers we should process */
+ std::map< Node, bool > d_quantActive;
/** delta */
std::map< TypeNode, Node > d_deltas;
/** for each quantifier, simplex rows */
//priority levels :
//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers)
//2 : user patterns (when user-pat=resort ), auto gen patterns (for user pattern quantifiers, when user-pat=use)
-//3 : local theory extensions
+//3 :
//4 :
//5 : full saturate quantifiers
//#define MULTI_TRIGGER_FULL_EFFORT_HALF
-#define MULTI_MULTI_TRIGGERS
struct sortQuantifiersForSymbol {
QuantifiersEngine* d_qe;
}
}
-InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr ) :
- InstStrategy( qe ), d_tr_strategy( tstrt ){
- if( rgfr<0 ){
- d_regenerate = false;
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
+ //how to select trigger terms
+ if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
+ d_tr_strategy = Trigger::TS_MIN_TRIGGER;
+ }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
+ d_tr_strategy = Trigger::TS_MAX_TRIGGER;
}else{
- d_regenerate_frequency = rgfr;
+ d_tr_strategy = Trigger::TS_ALL;
+ }
+ //whether to select new triggers during the search
+ if( options::incrementTriggers() ){
+ d_regenerate_frequency = 3;
d_regenerate = true;
+ }else{
+ d_regenerate = false;
}
- d_generate_additional = true;
}
void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
//reset triggers
- for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
- for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
- itt->first->resetInstantiationRound();
- itt->first->reset( Node::null() );
+ for( unsigned r=0; r<2; r++ ){
+ for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
+ for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+ itt->first->resetInstantiationRound();
+ itt->first->reset( Node::null() );
+ }
}
}
d_processed_trigger.clear();
}
if( gen ){
generateTriggers( f, effort, e, status );
- if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){
+ 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;
}
}
// d_processed_trigger.clear();
// d_quantEngine->getEqualityQuery()->setLiberal( true );
//}
- 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;
- Trace("process-trigger") << " Process ";
- tr->debugPrint("process-trigger");
- Trace("process-trigger") << "..." << std::endl;
- InstMatch baseMatch( f );
- int numInst = tr->addInstantiations( baseMatch );
- 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{
+ bool hasInst = false;
+ for( unsigned r=0; r<2; r++ ){
+ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][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;
+ Trace("process-trigger") << " Process ";
+ tr->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
+ InstMatch baseMatch( f );
+ int numInst = tr->addInstantiations( baseMatch );
+ hasInst = numInst>0 || hasInst;
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen += numInst;
+ if( r==1 ){
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ //d_quantEngine->d_hasInstantiated[f] = true;
}
- if( tr->isMultiTrigger() ){
- d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
- }
- //d_quantEngine->d_hasInstantiated[f] = true;
}
}
+ if( hasInst && options::multiTriggerPriority() ){
+ break;
+ }
}
//if( e==4 ){
// d_quantEngine->getEqualityQuery()->setLiberal( false );
Trace("auto-gen-trigger") << std::endl;
}
- //populate candidate pattern term vector for the current trigger
- std::vector< Node > patTerms;
- //try to add single triggers first
- for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- if( d_single_trigger_gen.find( d_patTerms[0][f][i] )==d_single_trigger_gen.end() ){
- patTerms.push_back( d_patTerms[0][f][i] );
- }
- }
- //if no single triggers exist, add multi trigger terms
- if( patTerms.empty() && ( options::multiTriggerWhenSingle() || d_single_trigger_gen.empty() ) ){
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
- }
-
- if( !patTerms.empty() ){
- Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
- //sort terms based on relevance
- if( options::relevantTriggers() ){
- sortQuantifiersForSymbol sqfs;
- sqfs.d_qe = d_quantEngine;
- //sort based on # occurrences (this will cause Trigger to select rarer symbols)
- std::sort( patTerms.begin(), patTerms.end(), sqfs );
- Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
- for( int i=0; i<(int)patTerms.size(); i++ ){
- Debug("relevant-trigger") << " " << patTerms[i] << " (";
- Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
+ unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
+ unsigned rmax = ( options::multiTriggerWhenSingle() || e>2 ) ? 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++ ){
+ if( r==1 || d_single_trigger_gen.find( d_patTerms[r][f][i] )==d_single_trigger_gen.end() ){
+ patTerms.push_back( d_patTerms[r][f][i] );
}
- //Notice() << "Terms based on relevance: " << std::endl;
- //for( int i=0; i<(int)patTerms.size(); i++ ){
- // Notice() << " " << patTerms[i] << " (";
- // Notice() << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
- //}
}
- //now, generate the trigger...
- int matchOption = 0;
- Trigger* tr = NULL;
- if( d_is_single_trigger[ patTerms[0] ] ){
- 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
- if( !d_patTerms[0][f].empty() ){
- if( e<=5 ){
- status = STATUS_UNFINISHED;
- return;
- }else{
- Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
+ if( !patTerms.empty() ){
+ Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+ //sort terms based on relevance
+ if( options::relevantTriggers() ){
+ sortQuantifiersForSymbol sqfs;
+ sqfs.d_qe = d_quantEngine;
+ //sort based on # occurrences (this will cause Trigger to select rarer symbols)
+ std::sort( patTerms.begin(), patTerms.end(), sqfs );
+ Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+ for( int i=0; i<(int)patTerms.size(); i++ ){
+ Debug("relevant-trigger") << " " << patTerms[i] << " (";
+ Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
}
}
- //if we are re-generating triggers, shuffle based on some method
- if( d_made_multi_trigger[f] ){
-#ifndef MULTI_MULTI_TRIGGERS
- return;
-#endif
- std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+ //now, generate the trigger...
+ int matchOption = 0;
+ Trigger* tr = NULL;
+ if( d_is_single_trigger[ patTerms[0] ] ){
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
+ d_single_trigger_gen[ patTerms[0] ] = true;
}else{
- d_made_multi_trigger[f] = true;
- }
- //will possibly want to get an old trigger
- tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() );
- }
- if( tr ){
- if( tr->isMultiTrigger() ){
- //disable all other multi triggers
- for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[f].begin(); it != d_auto_gen_trigger[f].end(); ++it ){
- if( it->first->isMultiTrigger() ){
- d_auto_gen_trigger[f][ it->first ] = false;
+ //only generate multi trigger if effort level > 5, or if no single triggers exist
+ if( !d_patTerms[0][f].empty() ){
+ if( e<=5 && !options::multiTriggerWhenSingle() ){
+ status = STATUS_UNFINISHED;
+ return;
+ }else{
+ Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
}
}
+ //if we are re-generating triggers, shuffle based on some method
+ if( d_made_multi_trigger[f] ){
+ std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+ }else{
+ d_made_multi_trigger[f] = true;
+ }
+ //will possibly want to get an old trigger
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD, options::smartTriggers() );
}
- //making it during an instantiation round, so must reset
- if( d_auto_gen_trigger[f].find( tr )==d_auto_gen_trigger[f].end() ){
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- }
- d_auto_gen_trigger[f][tr] = true;
- //if we are generating additional triggers...
- if( d_generate_additional && d_is_single_trigger[ patTerms[0] ] ){
- int index = 0;
- if( index<(int)patTerms.size() ){
- //Notice() << "check add additional" << std::endl;
- //check if similar patterns exist, and if so, add them additionally
- int nqfs_curr = 0;
- if( options::relevantTriggers() ){
- nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+ if( tr ){
+ unsigned tindex;
+ if( tr->isMultiTrigger() ){
+ //disable all other multi triggers
+ for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){
+ d_auto_gen_trigger[1][f][ it->first ] = false;
}
- index++;
- bool success = true;
- while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
- success = false;
- if( !options::relevantTriggers() ||
- d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
- d_single_trigger_gen[ patTerms[index] ] = true;
- Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
- if( tr2 ){
- //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
- tr2->resetInstantiationRound();
- tr2->reset( Node::null() );
- d_auto_gen_trigger[f][tr2] = true;
- }
- success = true;
+ tindex = 1;
+ }else{
+ tindex = 0;
+ }
+ //making it during an instantiation round, so must reset
+ if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ }
+ d_auto_gen_trigger[tindex][f][tr] = true;
+ //if we are generating additional triggers...
+ if( tindex==0 ){
+ int index = 0;
+ if( index<(int)patTerms.size() ){
+ //Notice() << "check add additional" << std::endl;
+ //check if similar patterns exist, and if so, add them additionally
+ int nqfs_curr = 0;
+ if( options::relevantTriggers() ){
+ nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
}
index++;
+ bool success = true;
+ while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+ success = false;
+ if( !options::relevantTriggers() ||
+ d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+ d_single_trigger_gen[ patTerms[index] ] = true;
+ Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() );
+ if( tr2 ){
+ //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
+ tr2->resetInstantiationRound();
+ tr2->reset( Node::null() );
+ d_auto_gen_trigger[0][f][tr2] = true;
+ }
+ success = true;
+ }
+ index++;
+ }
+ //Notice() << "done check add additional" << std::endl;
}
- //Notice() << "done check add additional" << std::endl;
}
}
}
/** regeneration */
bool d_regenerate;
int d_regenerate_frequency;
- /** generate additional triggers */
- bool d_generate_additional;
- /** triggers for each quantifier */
- std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger;
+ /** (single,multi) triggers for each quantifier */
+ std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
std::map< Node, int > d_counter;
/** single, multi triggers for each quantifier */
std::map< Node, std::vector< Node > > d_patTerms[2];
void processResetInstantiationRound( Theory::Effort effort );
int process( Node f, Theory::Effort effort, int e );
/** generate triggers */
- void generateTriggers( Node f, Theory::Effort effort, int e, int & status );
+ void generateTriggers( Node f, Theory::Effort effort, int e, int& status );
+ //bool addTrigger( inst::Trigger * tr, Node f, unsigned r );
/** has user patterns */
bool hasUserPatterns( Node f );
/** has user patterns */
std::map< Node, bool > d_hasUserPatterns;
public:
- /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
- rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
- rgfr is the frequency at which triggers are generated */
- InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 );
+ InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
~InstStrategyAutoGenTriggers(){}
public:
/** get auto-generated trigger */
void InstantiationEngine::finishInit(){
if( options::eMatching() ){
//these are the instantiation strategies for E-matching
-
+
//user-provided patterns
if( options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){
d_isup = new InstStrategyUserPatterns( d_quantEngine );
d_instStrategies.push_back( d_isup );
}
-
+
//auto-generated patterns
- int tstrt = Trigger::TS_ALL;
- if( options::triggerSelMode()==TRIGGER_SEL_MIN ){
- tstrt = Trigger::TS_MIN_TRIGGER;
- }else if( options::triggerSelMode()==TRIGGER_SEL_MAX ){
- tstrt = Trigger::TS_MAX_TRIGGER;
- }
- d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
+ d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine );
d_instStrategies.push_back( d_i_ag );
}
-
+
//local theory extensions TODO?
//if( options::localTheoryExt() ){
// d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine );
// d_instStrategies.push_back( d_i_lte );
//}
-
+
//full saturation : instantiate from relevant domain, then arbitrary terms
if( options::fullSaturateQuant() ){
d_i_fs = new InstStrategyFreeVariable( d_quantEngine );
d_instStrategies.push_back( d_i_fs );
}
-
+
//counterexample-based quantifier instantiation
if( options::cbqi() ){
d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine );
}
}
//if not, proceed to instantiation round
- Debug("inst-engine") << "IE: Instantiation Round." << std::endl;
- Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
- //reset the quantifiers engine
- Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
- //reset the instantiators
+ //reset the instantiation strategies
for( size_t i=0; i<d_instStrategies.size(); ++i ){
InstStrategy* is = d_instStrategies[i];
is->processResetInstantiationRound( effort );
//check each instantiation strategy
for( size_t i=0; i<d_instStrategies.size(); ++i ){
InstStrategy* is = d_instStrategies[i];
- if( is->shouldProcess( f ) ){
- Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
- int quantStatus = is->process( f, effort, e_use );
- Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
- if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
- finished = false;
- }
+ Debug("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+ int quantStatus = is->process( f, effort, e_use );
+ Debug("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
+ if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+ finished = false;
}
}
}
}
e++;
}
- Debug("inst-engine") << "All instantiators finished, # added lemmas = ";
- Debug("inst-engine") << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
//Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
if( !d_quantEngine->hasAddedLemma() ){
- Debug("inst-engine-ctrl") << "---Fail." << std::endl;
return false;
}else{
- Debug("inst-engine-ctrl") << "---Done. " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->d_lemmas_waiting.size()-lastWaiting) << std::endl;
return true;
}
InstantiationEngine::Statistics::Statistics():
d_instantiations_user_patterns("InstantiationEngine::Instantiations_User_Patterns", 0),
d_instantiations_auto_gen("InstantiationEngine::Instantiations_Auto_Gen", 0),
- d_instantiations_auto_gen_min("InstantiationEngine::Instantiations_Auto_Gen_Min", 0),
d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0),
d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0),
d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0),
{
StatisticsRegistry::registerStat(&d_instantiations_user_patterns);
StatisticsRegistry::registerStat(&d_instantiations_auto_gen);
- StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min);
StatisticsRegistry::registerStat(&d_instantiations_guess);
StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith);
StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus);
InstantiationEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_instantiations_user_patterns);
StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen);
- StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min);
StatisticsRegistry::unregisterStat(&d_instantiations_guess);
StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
protected:
/** reference to the instantiation engine */
QuantifiersEngine* d_quantEngine;
- /** should process a quantifier */
- std::map< Node, bool > d_quantActive;
- /** calculate should process */
- virtual bool calculateShouldProcess( Node f ) { return true; }
public:
InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
virtual ~InstStrategy(){}
-
- /** should process quantified formula f? */
- bool shouldProcess( Node f ) {
- if( d_quantActive.find( f )==d_quantActive.end() ){
- d_quantActive[f] = calculateShouldProcess( f );
- }
- return d_quantActive[f];
- }
/** reset instantiation */
virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
/** process method, returns a status */
public:
IntStat d_instantiations_user_patterns;
IntStat d_instantiations_auto_gen;
- IntStat d_instantiations_auto_gen_min;
IntStat d_instantiations_guess;
IntStat d_instantiations_cbqi_arith;
IntStat d_instantiations_cbqi_arith_minus;
theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
-properties check propagate presolve getNextDecisionRequest
+properties check presolve getNextDecisionRequest
rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
-option eMatching --e-matching bool :read-write :default true
- whether to do heuristic E-matching
+#### rewriter options
# Whether to mini-scope quantifiers.
# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
option miniscopeQuant --miniscope-quant bool :default true :read-write
disable miniscope quantifiers
-
# Whether to mini-scope quantifiers based on formulas with no free variables.
# For example, forall x. ( P( x ) V Q ) will be rewritten to
# ( forall x. P( x ) ) V Q
option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
disable miniscope quantifiers for ground subformulas
-
# Whether to prenex (nested universal) quantifiers
option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h"
disable prenexing of quantified formulas
-
# Whether to variable-eliminate quantifiers.
# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
# forall y. P( c, y )
disable simple variable elimination for quantified formulas
option dtVarExpandQuant --dt-var-exp-quant bool :default true
expand datatype variables bound to one constructor in quantifiers
-
option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true
split variables occurring as conditions of ITE in quantifiers
option simpleIteLiftQuant --ite-lift-quant bool :default true
disable simple ite lifting for quantified formulas
-
# Whether to CNF quantifier bodies
option cnfQuant --cnf-quant bool :default false
apply CNF conversion to quantified formulas
# Whether to NNF quantifier bodies
option nnfQuant --nnf-quant bool :default true
apply NNF conversion to quantified formulas
-
option clauseSplit --clause-split bool :default false
apply clause splitting to quantified formulas
-
# Whether to pre-skolemize quantifier bodies.
# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
# forall x. P( x ) => f( S( x ) ) = x
option foPropQuant --fo-prop-quant bool :default false
perform first-order propagation on quantifiers
+#### E-matching options
+
+option eMatching --e-matching bool :read-write :default true
+ whether to do heuristic E-matching
+
option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h"
which ground terms to consider for instantiation
+# Whether to consider terms in the bodies of quantifiers for matching
+option registerQuantBodyTerms --register-quant-body-terms bool :default false
+ consider ground terms within bodies of quantified formulas for matching
+
# Whether to use smart triggers
option smartTriggers --smart-triggers bool :default true
disable smart triggers
purify dt triggers, match all constructors of correct form instead of selectors
option pureThTriggers --pure-th-triggers bool :default false :read-write
use pure theory terms as single triggers
-option multiTriggerWhenSingle --multi-trigger-when-single bool :default true
- never select multi-triggers when single triggers exist
+option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
+ select multi triggers when single triggers exist
+option multiTriggerPriority --multi-trigger-priority bool :default false
+ only try multi triggers if single triggers give no instantiations
option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
selection mode for triggers
-
-option quantFunWellDefined --quant-fun-wd bool :default false
- assume that function defined by quantifiers are well defined
-option fmfFunWellDefined --fmf-fun bool :default false
- find models for finite runs of defined functions, assumes functions are well-defined
+option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :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
-# Whether to consider terms in the bodies of quantifiers for matching
-option registerQuantBodyTerms --register-quant-body-terms bool :default false
- consider ground terms within bodies of quantified formulas for matching
-
option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
when to apply instantiation
+
+
option instMaxLevel --inst-max-level=N int :read-write :default -1
maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
option instLevelInputOnly --inst-level-input-only bool :default true
only input terms are assigned instantiation level zero
-
+option internalReps --quant-internal-reps bool :default true
+ instantiate with representatives chosen by quantifiers engine
+
+option incrementTriggers --increment-triggers bool :default true
+ generate additional triggers as needed during search
option eagerInstQuant --eager-inst-quant bool :default false
apply quantifier instantiation eagerly
-option instNoEntail --inst-no-entail bool :read-write :default false
- do not consider instances of quantified formulas that are currently entailed
-
option fullSaturateQuant --full-saturate-quant bool :default false
when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
choose literal matching mode
-option cbqi --enable-cbqi bool :read-write :default false
- turns on counterexample-based quantifier instantiation
-
-option recurseCbqi --cbqi-recurse bool :default false
- turns on recursive counterexample-based quantifier instantiation
-
-option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :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
-
-option internalReps --quant-internal-reps bool :default true
- disables instantiating with representatives chosen by quantifiers engine
+option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
+ policy for instantiating axioms
+
+### finite model finding options
+
option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
use finite model finding heuristic for quantifier instantiation
+option quantFunWellDefined --quant-fun-wd bool :default false
+ assume that function defined by quantifiers are well defined
+option fmfFunWellDefined --fmf-fun bool :default false
+ find models for finite runs of defined functions, assumes functions are well-defined
+
option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
choose mode for model-based quantifier instantiation
option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
finite model finding on bounded integer quantification
option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
enforce bounds for bounded integer quantification lazily via use of proxy variables
-
-option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
- policy for instantiating axioms
-
+
+### conflict-based instantiation options
+
option quantConflictFind --quant-cf bool :read-write :default true
enable conflict find mechanism for quantifiers
option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
option qcfTConstraint --qcf-tconstraint bool :read-write :default false
enable entailment checks for t-constraints in qcf algorithm
+option instNoEntail --inst-no-entail bool :read-write :default true
+ do not consider instances of quantified formulas that are currently entailed
+
+### rewrite rules options
+
option quantRewriteRules --rewrite-rules bool :default true
use rewrite rules module
option rrOneInstPerRound --rr-one-inst-per-round bool :default false
add one instance of rewrite rule per round
-
+
+### induction options
+
option quantInduction --quant-ind bool :default false
use all available techniques for inductive reasoning
option dtStcInduction --dt-stc-ind bool :read-write :default false
number of ground terms to generate for model filtering
option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
more aggressive merging for universal equality engine, introduces terms
-
+
+### synthesis options
+
option ceGuidedInst --cegqi bool :default false :read-write
counterexample-guided quantifier instantiation
option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
generalize based on arguments in global search space narrowing
option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
generalize based on content in global search space narrowing
+
+# older implementation
+option cbqi --enable-cbqi bool :read-write :default false
+ turns on counterexample-based quantifier instantiation
+option recurseCbqi --cbqi-recurse bool :default false
+ turns on recursive counterexample-based quantifier instantiation
+
+### local theory extensions options
option localTheoryExt --local-t-ext bool :default false
do instantiation based on local theory extensions
Modes for term database, supported by --term-db-mode:\n\
\n\
all \n\
-+ Consider all terms in the system.\n\
++ Quantifiers module considers all ground terms.\n\
\n\
relevant \n\
-+ Consider only terms connected to current assertions. \n\
++ Quantifiers module considers only ground terms connected to current assertions. \n\
\n\
";
}
return n;
}
-
-bool QuantifiersRewriter::isDtStrInductionQuantifier( Node q ){
- Assert( q.getKind()==FORALL );
- return q[0].getNumChildren()==1 && datatypes::DatatypesRewriter::isTermDatatype( q[0][0] );
-}
static Node rewriteRewriteRule( Node r );
static bool containsQuantifiers(Node n);
static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
-private:
- static bool isDtStrInductionQuantifier( Node q );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
getQuantifiersEngine()->check( e );
}
-void TheoryQuantifiers::propagate(Effort level){
- //getQuantifiersEngine()->propagate( level );
-}
-
Node TheoryQuantifiers::getNextDecisionRequest(){
return getQuantifiersEngine()->getNextDecisionRequest();
}
}
}
-bool TheoryQuantifiers::flipDecision(){
- //Debug("quantifiers-flip") << "No instantiation given, flip decision, level = " << d_valuation.getDecisionLevel() << std::endl;
- //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
- // Debug("quantifiers-flip") << " " << d_valuation.getDecision( i ) << std::endl;
- //}
- //if( d_valuation.getDecisionLevel()>0 ){
- // double r = double(rand())/double(RAND_MAX);
- // unsigned decisionLevel = (unsigned)(r*d_valuation.getDecisionLevel());
- // d_out->flipDecision( decisionLevel );
- // return true;
- //}else{
- // return false;
- //}
- return false;
-}
-
void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
}
void preRegisterTerm(TNode n);
void presolve();
void check(Effort e);
- void propagate(Effort level);
Node getNextDecisionRequest();
Node getValue(TNode n);
void collectModelInfo( TheoryModel* m, bool fullModel );
void shutdown() { }
std::string identify() const { return std::string("TheoryQuantifiers"); }
- bool flipDecision();
void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value);
eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
bool ppDontRewriteSubterm(TNode atom) { return atom.getKind() == kind::FORALL || atom.getKind() == kind::EXISTS; }
if(d_logicInfo.isQuantified()) {
// quantifiers engine must pass effort last call check
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
- // if we have given up, then possibly flip decision
- if(options::flipDecision()) {
- if(d_incomplete && !d_inConflict && !needCheck()) {
- ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision();
- }
- }
// if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
} else if(options::produceModels()) {
// must build model at this point
projects / cvc5.git / commitdiff