if( options::sortInference() ){
//sort inference technique
- SortInference si;
- si.simplify( d_assertionsToPreprocess );
+ d_smt.d_theoryEngine->getSortInference()->simplify( d_assertionsToPreprocess );
}
dumpAssertions("pre-simplify", d_assertionsToPreprocess);
void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
{
+ if (n.getKind()==FORALL || n.getKind()==EXISTS) {
+ return;
+ }
if (cache.find(n) != cache.end()) {
return;
}
}\r
}\r
\r
+void InstMatchGenerator::setActiveAdd(){\r
+ d_active_add = true;\r
+ if( !d_children.empty() ){\r
+ d_children[d_children.size()-1]->setActiveAdd();\r
+ }\r
+}\r
+\r
void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){\r
int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;\r
for( int i=0; i<(int)pats.size(); i++ ){\r
}\r
\r
void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){\r
+ d_active_add = false;\r
Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;\r
Assert( pat.hasAttribute(InstConstantAttribute()) );\r
d_pattern = pat;\r
}\r
\r
/** get match (not modulo equality) */\r
-bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){\r
+bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){\r
Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("\r
- << m.size() << ")" << ", " << d_children.size() << std::endl;\r
+ << m << ")" << ", " << d_children.size() << std::endl;\r
Assert( !d_match_pattern.isNull() );\r
if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){\r
return true;\r
int index = 0;\r
while( index>=0 && index<(int)d_children.size() ){\r
partial.push_back( InstMatch( &partial[index] ) );\r
- if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){\r
+ if( d_children[index]->getNextMatch2( f, partial[index+1], qe ) ){\r
index++;\r
}else{\r
d_children[index]->d_cg->reset( reps[index] );\r
}\r
}\r
if( index>=0 ){\r
- m = partial.back();\r
- return true;\r
+ if( d_children.empty() && d_active_add ){\r
+ Trace("active-add") << "Active Adding instantiation " << partial.back() << std::endl;\r
+ bool succ = qe->addInstantiation( f, partial.back() );\r
+ Trace("active-add") << "Success = " << succ << std::endl;\r
+ return succ;\r
+ }else{\r
+ m = partial.back();\r
+ return true;\r
+ }\r
}else{\r
return false;\r
}\r
}\r
}\r
\r
-bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){\r
+bool InstMatchGenerator::getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){\r
bool success = false;\r
Node t;\r
do{\r
t = d_cg->getNextCandidate();\r
//if t not null, try to fit it into match m\r
if( !t.isNull() && t.getType()==d_match_pattern.getType() ){\r
- success = getMatch( t, m, qe );\r
+ success = getMatch( f, t, m, qe );\r
}\r
}while( !success && !t.isNull() );\r
if (saveMatched) m.d_matched = t;\r
}\r
}\r
\r
-bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){\r
+bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){\r
m.d_matched = Node::null();\r
if( d_match_pattern.isNull() ){\r
int index = (int)d_partial.size();\r
}else{\r
d_partial.push_back( InstMatch() );\r
}\r
- if( d_children[index]->getNextMatch( d_partial[index], qe ) ){\r
+ if( d_children[index]->getNextMatch( f, d_partial[index], qe ) ){\r
index++;\r
}else{\r
d_children[index]->reset( Node::null(), qe );\r
return false;\r
}\r
}else{\r
- bool res = getNextMatch2( m, qe, true );\r
+ bool res = getNextMatch2( f, m, qe, true );\r
Assert(!res || !m.d_matched.isNull());\r
return res;\r
}\r
//now, try to add instantiation for each match produced\r
int addedLemmas = 0;\r
InstMatch m;\r
- while( getNextMatch( m, qe ) ){\r
- //m.makeInternal( d_quantEngine->getEqualityQuery() );\r
- m.add( baseMatch );\r
- if( qe->addInstantiation( f, m ) ){\r
- addedLemmas++;\r
- if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){\r
- return addedLemmas;\r
+ while( getNextMatch( f, m, qe ) ){\r
+ //if( d_active_add ){\r
+ // std::cout << "should not add at top level." << std::endl;\r
+ //}\r
+ if( !d_active_add ){\r
+ //m.makeInternal( d_quantEngine->getEqualityQuery() );\r
+ m.add( baseMatch );\r
+ if( qe->addInstantiation( f, m ) ){\r
+ addedLemmas++;\r
+ if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){\r
+ return addedLemmas;\r
+ }\r
}\r
+ m.clear();\r
}\r
- m.clear();\r
}\r
//return number of lemmas added\r
return addedLemmas;\r
Assert( options::eagerInstQuant() );\r
if( !d_match_pattern.isNull() ){\r
InstMatch m;\r
- if( getMatch( t, m, qe ) ){\r
+ if( getMatch( f, t, m, qe ) ){\r
if( qe->addInstantiation( f, m ) ){\r
return 1;\r
}\r
Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;\r
std::vector< InstMatch > newMatches;\r
InstMatch m;\r
- while( d_children[i]->getNextMatch( m, qe ) ){\r
+ while( d_children[i]->getNextMatch( f, m, qe ) ){\r
m.makeRepresentative( qe );\r
newMatches.push_back( InstMatch( &m ) );\r
m.clear();\r
if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){\r
InstMatch m;\r
//if it produces a match, then process it with the rest\r
- if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){\r
+ if( ((InstMatchGenerator*)d_children[i])->getMatch( f, t, m, qe ) ){\r
processNewMatch( qe, m, i, addedLemmas );\r
}\r
}\r
/** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;\r
/** get the next match. must call reset( eqc ) before this function. */\r
- virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;\r
+ virtual bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) = 0;\r
/** add instantiations directly */\r
virtual int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;\r
/** add ground term t, called when t is added to term db */\r
virtual int addTerm( Node f, Node t, QuantifiersEngine* qe ) = 0;\r
+ /** set active add */\r
+ virtual void setActiveAdd() {}\r
};/* class IMGenerator */\r
\r
class CandidateGenerator;\r
/** get the next match. must call d_cg->reset( ... ) before using.\r
only valid for use where !d_match_pattern.isNull().\r
*/\r
- bool getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );\r
+ bool getNextMatch2( Node f, InstMatch& m, QuantifiersEngine* qe, bool saveMatched = false );\r
/** for arithmetic */\r
bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );\r
public:\r
d_match_pattern and t should have the same shape.\r
only valid for use where !d_match_pattern.isNull().\r
*/\r
- bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );\r
+ bool getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe );\r
\r
/** constructors */\r
InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchOption = 0 );\r
/** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
void reset( Node eqc, QuantifiersEngine* qe );\r
/** get the next match. must call reset( eqc ) before this function. */\r
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );\r
+ bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe );\r
/** add instantiations */\r
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
/** add ground term t */\r
int addTerm( Node f, Node t, QuantifiersEngine* qe );\r
+\r
+ bool d_active_add;\r
+ void setActiveAdd();\r
};/* class InstMatchGenerator */\r
\r
/** smart multi-trigger implementation */\r
/** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
void reset( Node eqc, QuantifiersEngine* qe );\r
/** get the next match. must call reset( eqc ) before this function. (not implemented) */\r
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
+ bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
/** add instantiations */\r
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
/** add ground term t */\r
/** reset, eqc is the equivalence class to search in (any if eqc=null) */\r
void reset( Node eqc, QuantifiersEngine* qe ) {}\r
/** get the next match. must call reset( eqc ) before this function. (not implemented) */\r
- bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
+ bool getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ) { return false; }\r
/** add instantiations */\r
int addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe );\r
/** add ground term t, possibly add instantiations */\r
using namespace CVC4::theory::inst;\r
using namespace CVC4::theory::quantifiers;\r
\r
-#define USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER\r
//#define MULTI_TRIGGER_FULL_EFFORT_HALF\r
#define MULTI_MULTI_TRIGGERS\r
\r
//Notice() << "Try user-provided patterns..." << std::endl;\r
for( int i=0; i<(int)d_user_gen[f].size(); i++ ){\r
bool processTrigger = true;\r
- if( effort!=Theory::EFFORT_LAST_CALL && d_user_gen[f][i]->isMultiTrigger() ){\r
-//#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF\r
-// processTrigger = d_counter[f]%2==0;\r
-//#endif\r
- }\r
if( processTrigger ){\r
//if( d_user_gen[f][i]->isMultiTrigger() )\r
- //Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;\r
+ Trace("process-trigger") << " Process (user) " << (*d_user_gen[f][i]) << "..." << std::endl;\r
InstMatch baseMatch;\r
int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );\r
//if( d_user_gen[f][i]->isMultiTrigger() )\r
- //Notice() << " Done, numInst = " << numInst << "." << std::endl;\r
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;\r
d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_user_patterns += numInst;\r
if( d_user_gen[f][i]->isMultiTrigger() ){\r
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;\r
itt->first->reset( Node::null() );\r
}\r
}\r
+ d_processed_trigger.clear();\r
}\r
\r
int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){\r
if( e<peffort ){\r
return STATUS_UNFINISHED;\r
}else{\r
+ int status = STATUS_UNKNOWN;\r
bool gen = false;\r
if( e==peffort ){\r
if( d_counter.find( f )==d_counter.end() ){\r
gen = true;\r
}\r
if( gen ){\r
- generateTriggers( f );\r
+ generateTriggers( f, effort, e, status );\r
}\r
Debug("quant-uf-strategy") << "Try auto-generated triggers... " << d_tr_strategy << " " << e << std::endl;\r
//Notice() << "Try auto-generated triggers..." << std::endl;\r
Trigger* tr = itt->first;\r
if( tr ){\r
bool processTrigger = itt->second;\r
- if( effort!=Theory::EFFORT_LAST_CALL && tr->isMultiTrigger() ){\r
-#ifdef MULTI_TRIGGER_FULL_EFFORT_HALF\r
- processTrigger = d_counter[f]%2==0;\r
-#endif\r
- }\r
- if( processTrigger ){\r
+ if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){\r
+ d_processed_trigger[f][tr] = true;\r
//if( tr->isMultiTrigger() )\r
- Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;\r
+ Trace("process-trigger") << " Process " << (*tr) << "..." << std::endl;\r
InstMatch baseMatch;\r
int numInst = tr->addInstantiations( baseMatch );\r
//if( tr->isMultiTrigger() )\r
- Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;\r
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;\r
if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){\r
d_quantEngine->getInstantiationEngine()->d_statistics.d_instantiations_auto_gen_min += numInst;\r
}else{\r
}\r
Debug("quant-uf-strategy") << "done." << std::endl;\r
//Notice() << "done" << std::endl;\r
+ return status;\r
}\r
- return STATUS_UNKNOWN;\r
}\r
\r
-void InstStrategyAutoGenTriggers::generateTriggers( Node f ){\r
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;\r
+void InstStrategyAutoGenTriggers::generateTriggers( Node f, Theory::Effort effort, int e, int & status ){\r
+ Trace("auto-gen-trigger-debug") << "Generate trigger for " << f << std::endl;\r
if( d_patTerms[0].find( f )==d_patTerms[0].end() ){\r
//determine all possible pattern terms based on trigger term selection strategy d_tr_strategy\r
d_patTerms[0][f].clear();\r
d_patTerms[1][f].clear();\r
std::vector< Node > patTermsF;\r
Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true );\r
- Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;\r
- Debug("auto-gen-trigger") << " ";\r
+ Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl;\r
+ Trace("auto-gen-trigger") << " ";\r
for( int i=0; i<(int)patTermsF.size(); i++ ){\r
- Debug("auto-gen-trigger") << patTermsF[i] << " ";\r
+ Trace("auto-gen-trigger") << patTermsF[i] << " ";\r
}\r
- Debug("auto-gen-trigger") << std::endl;\r
+ Trace("auto-gen-trigger") << std::endl;\r
//extend to literal matching (if applicable)\r
d_quantEngine->getPhaseReqTerms( f, patTermsF );\r
//sort into single/multi triggers\r
}\r
}\r
d_made_multi_trigger[f] = false;\r
- Debug("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;\r
- Debug("auto-gen-trigger") << " ";\r
+ Trace("auto-gen-trigger") << "Single triggers for " << f << " : " << std::endl;\r
+ Trace("auto-gen-trigger") << " ";\r
for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){\r
- Debug("auto-gen-trigger") << d_patTerms[0][f][i] << " ";\r
+ Trace("auto-gen-trigger") << d_patTerms[0][f][i] << " ";\r
}\r
- Debug("auto-gen-trigger") << std::endl;\r
- Debug("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;\r
- Debug("auto-gen-trigger") << " ";\r
+ Trace("auto-gen-trigger") << std::endl;\r
+ Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;\r
+ Trace("auto-gen-trigger") << " ";\r
for( int i=0; i<(int)d_patTerms[1][f].size(); i++ ){\r
- Debug("auto-gen-trigger") << d_patTerms[1][f][i] << " ";\r
+ Trace("auto-gen-trigger") << d_patTerms[1][f][i] << " ";\r
}\r
- Debug("auto-gen-trigger") << std::endl;\r
+ Trace("auto-gen-trigger") << std::endl;\r
}\r
\r
//populate candidate pattern term vector for the current trigger\r
std::vector< Node > patTerms;\r
-#ifdef USE_SINGLE_TRIGGER_BEFORE_MULTI_TRIGGER\r
//try to add single triggers first\r
for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){\r
if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){\r
if( patTerms.empty() ){\r
patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );\r
}\r
-#else\r
- patTerms.insert( patTerms.begin(), d_patTerms[0][f].begin(), d_patTerms[0][f].end() );\r
- patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );\r
-#endif\r
\r
if( !patTerms.empty() ){\r
- Debug("auto-gen-trigger") << "Generate trigger for " << f << std::endl;\r
+ Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;\r
//sort terms based on relevance\r
if( d_rlv_strategy==RELEVANCE_DEFAULT ){\r
sortQuantifiersForSymbol sqfs;\r
options::smartTriggers() );\r
d_single_trigger_gen[ patTerms[0] ] = true;\r
}else{\r
+ //only generate multi trigger if effort level > 5, or if no single triggers exist\r
+ if( !d_patTerms[0][f].empty() ){\r
+ if( e<=5 ){\r
+ status = STATUS_UNFINISHED;\r
+ return;\r
+ }else{\r
+ Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;\r
+ }\r
+ }\r
//if we are re-generating triggers, shuffle based on some method\r
if( d_made_multi_trigger[f] ){\r
#ifndef MULTI_MULTI_TRIGGERS\r
std::map< Node, bool > d_is_single_trigger;\r
std::map< Node, bool > d_single_trigger_gen;\r
std::map< Node, bool > d_made_multi_trigger;\r
+ //processed trigger this round\r
+ std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;\r
private:\r
/** process functions */\r
void processResetInstantiationRound( Theory::Effort effort );\r
int process( Node f, Theory::Effort effort, int e );\r
/** generate triggers */\r
- void generateTriggers( Node f );\r
+ void generateTriggers( Node f, Theory::Effort effort, int e, int & status );\r
public:\r
/** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)\r
rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)\r
option smartTriggers /--disable-smart-triggers bool :default true
disable smart triggers
# Whether to use relevent triggers
-option relevantTriggers /--relevant-triggers bool :default true
- prefer triggers that are more relevant based on SInE style method
+option relevantTriggers --relevant-triggers bool :default true
+ prefer triggers that are more relevant based on SInE style analysis
# Whether to consider terms in the bodies of quantifiers for matching
option registerQuantBodyTerms --register-quant-body-terms bool :default false
ModelBasisAttribute mba;
mbt.setAttribute(mba,true);
d_model_basis_term[tn] = mbt;
+ Trace("model-basis-term") << "Choose " << mbt << " as model basis term for " << tn << std::endl;
}
return d_model_basis_term[tn];
}
Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" );
d_skolem_constants[ f ].push_back( skv );
vars.push_back( f[0][i] );
+ //carry information for sort inference
+ if( options::sortInference() ){
+ d_quantEngine->getTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], skv );
+ }
}
d_skolem_body[ f ] = f[ 1 ].substitute( vars.begin(), vars.end(),
d_skolem_constants[ f ].begin(), d_skolem_constants[ f ].end() );
return 0;
}
+bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){
+ if( n1==n2 ){
+ return true;
+ }else if( n2.getKind()==INST_CONSTANT ){
+ //if( !node_contains( n1, n2 ) ){
+ // return false;
+ //}
+ if( subs.find( n2 )==subs.end() ){
+ subs[n2] = n1;
+ }else if( subs[n2]!=n1 ){
+ return false;
+ }
+ return true;
+ }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){
+ if( n1.getOperator()!=n2.getOperator() ){
+ return false;
+ }
+ for( int i=0; i<(int)n1.getNumChildren(); i++ ){
+ if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){
+ return false;
+ }
+ }
+ return true;
+ }else{
+ return false;
+ }
+}
+
void TermDb::filterInstances( std::vector< Node >& nodes ){
std::vector< bool > active;
active.resize( nodes.size(), true );
if( active[i] && active[j] ){
int result = isInstanceOf( nodes[i], nodes[j] );
if( result==1 ){
+ Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
active[j] = false;
}else if( result==-1 ){
+ Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
active[i] = false;
}
}
std::map< TNode, std::vector< TNode > > d_var_contains;
/** triggers for each operator */
std::map< Node, std::vector< inst::Trigger* > > d_op_triggers;
+ /** helper for is intance of */
+ bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs );
public:
/** compute var contains */
void computeVarContains( Node n );
d_mg = new InstMatchGeneratorSimple( f, d_nodes[0] );
}else{
d_mg = new InstMatchGenerator( d_nodes[0], qe, matchOption );
+ d_mg->setActiveAdd();
}
}else{
d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe, matchOption );
++(qe->d_statistics.d_simple_triggers);
}
}else{
- Debug("multi-trigger") << "Multi-trigger " << (*this) << std::endl;
+ Trace("multi-trigger") << "Multi-trigger " << (*this) << " for " << f << std::endl;
//Notice() << "Multi-trigger for " << f << " : " << std::endl;
//Notice() << " " << (*this) << std::endl;
++(qe->d_statistics.d_multi_triggers);
d_mg->reset( eqc, d_quantEngine );
}
-bool Trigger::getNextMatch( InstMatch& m ){
- bool retVal = d_mg->getNextMatch( m, d_quantEngine );
+bool Trigger::getNextMatch( Node f, InstMatch& m ){
+ bool retVal = d_mg->getNextMatch( f, m, d_quantEngine );
return retVal;
}
-bool Trigger::getMatch( Node t, InstMatch& m ){
+bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
//FIXME: this assumes d_mg is an inst match generator
- return ((InstMatchGenerator*)d_mg)->getMatch( t, m, d_quantEngine );
+ return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
}
int Trigger::addTerm( Node t ){
temp.insert( temp.begin(), nodes.begin(), nodes.end() );
std::map< Node, bool > vars;
std::map< Node, std::vector< Node > > patterns;
+ size_t varCount = 0;
for( int i=0; i<(int)temp.size(); i++ ){
bool foundVar = false;
qe->getTermDatabase()->computeVarContains( temp[i] );
Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j];
if( v.getAttribute(InstConstantAttribute())==f ){
if( vars.find( v )==vars.end() ){
+ varCount++;
vars[ v ] = true;
foundVar = true;
}
patterns[ v ].push_back( temp[i] );
}
}
- }
- //now, minimalize the trigger
- for( int i=0; i<(int)trNodes.size(); i++ ){
- bool keepPattern = false;
- Node n = trNodes[i];
- for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
- Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
- if( patterns[v].size()==1 ){
- keepPattern = true;
- break;
- }
+ if( varCount==f[0].getNumChildren() ){
+ break;
}
- if( !keepPattern ){
- //remove from pattern vector
+ }
+ if( varCount<f[0].getNumChildren() ){
+ //do not generate multi-trigger if it does not contain all variables
+ return NULL;
+ }else{
+ //now, minimize the trigger
+ for( int i=0; i<(int)trNodes.size(); i++ ){
+ bool keepPattern = false;
+ Node n = trNodes[i];
for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
- for( int k=0; k<(int)patterns[v].size(); k++ ){
- if( patterns[v][k]==n ){
- patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
- break;
+ if( patterns[v].size()==1 ){
+ keepPattern = true;
+ break;
+ }
+ }
+ if( !keepPattern ){
+ //remove from pattern vector
+ for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){
+ Node v = qe->getTermDatabase()->d_var_contains[ n ][j];
+ for( int k=0; k<(int)patterns[v].size(); k++ ){
+ if( patterns[v][k]==n ){
+ patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+ break;
+ }
}
}
+ //remove from trigger nodes
+ trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+ i--;
}
- //remove from trigger nodes
- trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
- i--;
}
}
}else{
temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
qe->getTermDatabase()->filterInstances( temp );
if( temp.size()!=patTerms2.size() ){
- Debug("trigger-filter-instance") << "Filtered an instance: " << std::endl;
- Debug("trigger-filter-instance") << "Old: ";
+ Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl;
+ Trace("trigger-filter-instance") << "Old: ";
for( int i=0; i<(int)patTerms2.size(); i++ ){
- Debug("trigger-filter-instance") << patTerms2[i] << " ";
+ Trace("trigger-filter-instance") << patTerms2[i] << " ";
}
- Debug("trigger-filter-instance") << std::endl << "New: ";
+ Trace("trigger-filter-instance") << std::endl << "New: ";
for( int i=0; i<(int)temp.size(); i++ ){
- Debug("trigger-filter-instance") << temp[i] << " ";
+ Trace("trigger-filter-instance") << temp[i] << " ";
}
- Debug("trigger-filter-instance") << std::endl;
+ Trace("trigger-filter-instance") << std::endl;
}
if( tstrt==TS_ALL ){
patTerms.insert( patTerms.begin(), temp.begin(), temp.end() );
/** reset, eqc is the equivalence class to search in (search in any if eqc=null) */
void reset( Node eqc );
/** get next match. must call reset( eqc ) once before this function. */
- bool getNextMatch( InstMatch& m );
+ bool getNextMatch( Node f, InstMatch& m );
/** get the match against ground term or formula t.
the trigger and t should have the same shape.
Currently the trigger should not be a multi-trigger.
*/
- bool getMatch( Node t, InstMatch& m);
+ bool getMatch( Node f, Node t, InstMatch& m);
/** add ground term t, called when t is added to the TermDb */
int addTerm( Node t );
/** return whether this is a multi-trigger */
d_optMatchIgnoreModelBasis = false;
d_optInstLimitActive = false;
d_optInstLimit = 0;
+ d_total_inst_count_debug = 0;
}
QuantifiersEngine::~QuantifiersEngine(){
}
//build the model if not done so already
// this happens if no quantifiers are currently asserted and no model-building module is enabled
- if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
- d_te->getModelBuilder()->buildModel( d_model, true );
+ if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){
+ if( options::produceModels() && !d_model->isModelSet() ){
+ d_te->getModelBuilder()->buildModel( d_model, true );
+ }
+ if( Trace.isOn("inst-per-quant") ){
+ for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){
+ Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl;
+ }
+ }
+ }else{
+ if( Trace.isOn("inst-per-quant-round") ){
+ for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){
+ Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl;
+ d_temp_inst_debug[it->first] = 0;
+ }
+ }
}
-
Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
}
}
Node lem = nb;
//check for duplication
if( addLemma( lem ) ){
+ d_total_inst_debug[f]++;
+ d_temp_inst_debug[f]++;
+ d_total_inst_count_debug++;
Trace("inst") << "*** Instantiate " << f << " with " << std::endl;
uint64_t maxInstLevel = 0;
for( int i=0; i<(int)terms.size(); i++ ){
rrinst::TriggerTrie* d_rr_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
+ /** statistics for debugging */
+ std::map< Node, int > d_total_inst_debug;
+ std::map< Node, int > d_temp_inst_debug;
+ int d_total_inst_count_debug;
private:
KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time");
public:
#include "util/hash.h"
#include "util/cache.h"
#include "util/cvc4_assert.h"
+#include "util/sort_inference.h"
#include "theory/ite_simplifier.h"
#include "theory/unconstrained_simplifier.h"
#include "theory/uf/equality_engine.h"
RemoveITE& d_iteRemover;
+ /** sort inference module */
+ SortInference d_sortInfer;
+
/** Time spent in theory combination */
TimerStat d_combineTheoriesTime;
SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
+ SortInference* getSortInference() { return &d_sortInfer; }
private:
std::map< std::string, std::vector< theory::Theory* > > d_attr_handle;
public:
option ufssSmartSplits --uf-ss-smart-split bool :default false
use smart splitting heuristic for uf strong solver
option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
- add explained clique lemmas for uf strong solver
+ use explained clique lemmas for uf strong solver
+option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
+ always use simple clique lemmas for uf strong solver
endmodule
//internal disequality
d_regions[ai]->setDisequal( a, b, 1, true );
d_regions[ai]->setDisequal( b, a, 1, true );
+ checkRegion( ai, false ); //do not need to check if it needs to combine (no new ext. disequalities)
}else{
//external disequality
d_regions[ai]->setDisequal( a, b, 0, true );
if( level==Theory::EFFORT_FULL ){
if( !addedLemma ){
Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl;
- if( !options::ufssColoringSat() ){
+ Trace("uf-ss-si") << "Must combine region" << std::endl;
+ if( true || !options::ufssColoringSat() ){
bool recheck = false;
//naive strategy, force region combination involving the first valid region
- for( int i=0; i<(int)d_regions_index; i++ ){
- if( d_regions[i]->d_valid ){
- forceCombineRegion( i, false );
- recheck = true;
- break;
+ if( options::sortInference()){
+ std::map< int, int > sortsFound;
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ Node op = d_regions[i]->d_nodes.begin()->first;
+ int sort_id = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId(op) ;
+ if( sortsFound.find( sort_id )!=sortsFound.end() ){
+ combineRegions( sortsFound[sort_id], i );
+ recheck = true;
+ break;
+ }else{
+ sortsFound[sort_id] = i;
+ }
+ }
+ }
+ }
+ if( !recheck ) {
+ for( int i=0; i<(int)d_regions_index; i++ ){
+ if( d_regions[i]->d_valid ){
+ forceCombineRegion( i, false );
+ recheck = true;
+ break;
+ }
}
}
if( recheck ){
}
}
-void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool rec ){
+void StrongSolverTheoryUf::SortRepModel::checkRegion( int ri, bool checkCombine ){
if( isValid(ri) && d_hasCard ){
Assert( d_cardinality>0 );
- //first check if region is in conflict
- std::vector< Node > clique;
- if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
- //explain clique
- addCliqueLemma( clique, &d_th->getOutputChannel() );
- }else if( d_regions[ri]->getMustCombine( d_cardinality ) ){
+ if( checkCombine && d_regions[ri]->getMustCombine( d_cardinality ) ){
////alternatively, check if we can reduce the number of external disequalities by moving single nodes
//for( std::map< Node, bool >::iterator it = d_regions[i]->d_reps.begin(); it != d_regions[i]->d_reps.end(); ++it ){
// if( it->second ){
// }
//}
int riNew = forceCombineRegion( ri, true );
- if( riNew>=0 && rec ){
- checkRegion( riNew, rec );
+ if( riNew>=0 ){
+ checkRegion( riNew, checkCombine );
}
}
+ //now check if region is in conflict
+ std::vector< Node > clique;
+ if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
+ //explain clique
+ addCliqueLemma( clique, &d_th->getOutputChannel() );
+ }
}
}
Assert( s!=Node::null() && s.getKind()==EQUAL );
s = Rewriter::rewrite( s );
Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
+ if( options::sortInference()) {
+ for( int i=0; i<2; i++ ){
+ int si = d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference()->getSortId( s[i] );
+ Trace("uf-ss-split-si") << si << " ";
+ }
+ Trace("uf-ss-split-si") << std::endl;
+ }
//Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areEqual( s[0], s[1] ) << " ";
//Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl;
//Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl;
while( clique.size()>size_t(d_cardinality+1) ){
clique.pop_back();
}
- if( !options::ufssExplainedCliques() ){
+ if( options::ufssSimpleCliques() && !options::ufssExplainedCliques() ){
//add as lemma
std::vector< Node > eqs;
for( int i=0; i<(int)clique.size(); i++ ){
for( int j=0; j<i; j++ ){
+ Node r1 = d_th->d_equalityEngine.getRepresentative(clique[i]);
+ Node r2 = d_th->d_equalityEngine.getRepresentative(clique[j]);
eqs.push_back( clique[i].eqNode( clique[j] ) );
}
}
eqs.push_back( d_cardinality_literal[ d_cardinality ].notNode() );
Node lem = NodeManager::currentNM()->mkNode( OR, eqs );
+ Trace("uf-ss-lemma") << "*** Add clique conflict " << lem << std::endl;
+ ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
out->lemma( lem );
- return;
- }
- //if( options::ufssModelInference() ||
- if( Trace.isOn("uf-ss-cliques") ){
- std::vector< Node > clique_vec;
- clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
- d_cliques[ d_cardinality ].push_back( clique_vec );
- }
-
- //found a clique
- Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
- Debug("uf-ss-cliques") << " ";
- for( int i=0; i<(int)clique.size(); i++ ){
- Debug("uf-ss-cliques") << clique[i] << " ";
- }
- Debug("uf-ss-cliques") << std::endl;
- Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
- std::vector< Node > conflict;
- //collect disequalities, and nodes that must be equal within representatives
- std::map< Node, std::map< Node, bool > > explained;
- std::map< Node, std::map< Node, bool > > nodesWithinRep;
- for( int i=0; i<(int)d_disequalities_index; i++ ){
- //if both sides of disequality exist in clique
- Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
- Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
- if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
- std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
- std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
- explained[r1][r2] = true;
- explained[r2][r1] = true;
- conflict.push_back( d_disequalities[i] );
- Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl;
- nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
- nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
- if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
- break;
+ }else{
+ //debugging information
+ if( Trace.isOn("uf-ss-cliques") ){
+ std::vector< Node > clique_vec;
+ clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
+ d_cliques[ d_cardinality ].push_back( clique_vec );
+ }
+ //found a clique
+ Debug("uf-ss-cliques") << "Found a clique (cardinality=" << d_cardinality << ") :" << std::endl;
+ Debug("uf-ss-cliques") << " ";
+ for( int i=0; i<(int)clique.size(); i++ ){
+ Debug("uf-ss-cliques") << clique[i] << " ";
+ }
+ Debug("uf-ss-cliques") << std::endl;
+ Debug("uf-ss-cliques") << "Finding clique disequalities..." << std::endl;
+
+ //we will scan through each of the disequaltities
+ bool isSatConflict = true;
+ std::vector< Node > conflict;
+ //collect disequalities, and nodes that must be equal within representatives
+ std::map< Node, std::map< Node, bool > > explained;
+ std::map< Node, std::map< Node, bool > > nodesWithinRep;
+ //map from the reprorted clique members to those reported in the lemma
+ std::map< Node, Node > cliqueRepMap;
+ for( int i=0; i<(int)d_disequalities_index; i++ ){
+ //if both sides of disequality exist in clique
+ Node r1 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][0] );
+ Node r2 = d_th->d_equalityEngine.getRepresentative( d_disequalities[i][0][1] );
+ if( r1!=r2 && ( explained.find( r1 )==explained.end() || explained[r1].find( r2 )==explained[r1].end() ) &&
+ std::find( clique.begin(), clique.end(), r1 )!=clique.end() &&
+ std::find( clique.begin(), clique.end(), r2 )!=clique.end() ){
+ explained[r1][r2] = true;
+ explained[r2][r1] = true;
+ if( options::ufssExplainedCliques() ){
+ conflict.push_back( d_disequalities[i] );
+ Debug("uf-ss-cliques") << " -> disequality : " << d_disequalities[i] << std::endl;
+ nodesWithinRep[r1][ d_disequalities[i][0][0] ] = true;
+ nodesWithinRep[r2][ d_disequalities[i][0][1] ] = true;
+ }else{
+ //get the terms we report in the lemma
+ Node ru1 = r1;
+ if( cliqueRepMap.find( r1 )==cliqueRepMap.end() ){
+ ru1 = d_disequalities[i][0][0];
+ cliqueRepMap[r1] = ru1;
+ }else{
+ ru1 = cliqueRepMap[r1];
+ }
+ Node ru2 = r2;
+ if( cliqueRepMap.find( r2 )==cliqueRepMap.end() ){
+ ru2 = d_disequalities[i][0][1];
+ cliqueRepMap[r2] = ru2;
+ }else{
+ ru2 = cliqueRepMap[r2];
+ }
+ if( ru1!=d_disequalities[i][0][0] || ru2!=d_disequalities[i][0][1] ){
+ //disequalities have endpoints that are not connected within an equivalence class
+ // we will be producing a lemma, introducing a new literal ru1 != ru2
+ conflict.push_back( ru1.eqNode( ru2 ).notNode() );
+ isSatConflict = false;
+ }else{
+ conflict.push_back( d_disequalities[i] );
+ }
+ }
+ if( conflict.size()==(clique.size()*( clique.size()-1 )/2) ){
+ break;
+ }
}
}
- }
- //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
- Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
- //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
- Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
- //now, we must explain equalities within each equivalence class
- for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
- if( it->second.size()>1 ){
- Node prev;
- //add explanation of t1 = t2 = ... = tn
- Debug("uf-ss-cliques") << "Explain ";
- for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if( prev!=Node::null() ){
- Debug("uf-ss-cliques") << " = ";
- //explain it2->first and prev
- std::vector< TNode > expl;
- d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
- for( int i=0; i<(int)expl.size(); i++ ){
- if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
- conflict.push_back( expl[i] );
+ if( options::ufssExplainedCliques() ){
+ //Debug("uf-ss-cliques") << conflict.size() << " " << clique.size() << std::endl;
+ Assert( (int)conflict.size()==((int)clique.size()*( (int)clique.size()-1 )/2) );
+ //Assert( (int)conflict.size()==(int)clique.size()*( (int)clique.size()-1 )/2 );
+ Debug("uf-ss-cliques") << "Finding clique equalities internal to eq classes..." << std::endl;
+ //now, we must explain equalities within each equivalence class
+ for( std::map< Node, std::map< Node, bool > >::iterator it = nodesWithinRep.begin(); it != nodesWithinRep.end(); ++it ){
+ if( it->second.size()>1 ){
+ Node prev;
+ //add explanation of t1 = t2 = ... = tn
+ Debug("uf-ss-cliques") << "Explain ";
+ for( std::map< Node, bool >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ if( prev!=Node::null() ){
+ Debug("uf-ss-cliques") << " = ";
+ //explain it2->first and prev
+ std::vector< TNode > expl;
+ d_th->d_equalityEngine.explainEquality( it2->first, prev, true, expl );
+ for( int i=0; i<(int)expl.size(); i++ ){
+ if( std::find( conflict.begin(), conflict.end(), expl[i] )==conflict.end() ){
+ conflict.push_back( expl[i] );
+ }
+ }
}
+ prev = it2->first;
+ Debug("uf-ss-cliques") << prev;
}
+ Debug("uf-ss-cliques") << std::endl;
}
- prev = it2->first;
- Debug("uf-ss-cliques") << prev;
+ }
+ Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
+ for( int i=0; i<(int)conflict.size(); i++ ){
+ Debug("uf-ss-cliques") << conflict[i] << " ";
}
Debug("uf-ss-cliques") << std::endl;
}
- }
- Debug("uf-ss-cliques") << "Explanation of clique (size=" << conflict.size() << ") = " << std::endl;
- for( int i=0; i<(int)conflict.size(); i++ ){
- Debug("uf-ss-cliques") << conflict[i] << " ";
- //bool value;
- //bool hasValue = d_th->getValuation().hasSatValue( conflict[i], value );
- //Assert( hasValue );
- //Assert( value );
- }
- Debug("uf-ss-cliques") << std::endl;
- //now, make the conflict
-#if 1
- conflict.push_back( d_cardinality_literal[ d_cardinality ] );
- Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
- Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
- //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
- out->conflict( conflictNode );
- d_conflict = true;
-#else
- Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
- //add cardinality constraint
- Node cardNode = d_cardinality_literal[ d_cardinality ];
- //bool value;
- //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
- //Assert( hasValue );
- //Assert( value );
- conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
- Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
- //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
- out->lemma( conflictNode );
-#endif
- ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+ //now, make the conflict
+ if( isSatConflict ){
+ conflict.push_back( d_cardinality_literal[ d_cardinality ] );
+ Node conflictNode = NodeManager::currentNM()->mkNode( AND, conflict );
+ Trace("uf-ss-lemma") << "*** Add clique conflict " << conflictNode << std::endl;
+ //Notice() << "*** Add clique conflict " << conflictNode << std::endl;
+ out->conflict( conflictNode );
+ d_conflict = true;
+ ++( d_th->getStrongSolver()->d_statistics.d_clique_conflicts );
+ }else{
+ Node conflictNode = conflict.size()==1 ? conflict[0] : NodeManager::currentNM()->mkNode( AND, conflict );
+ //add cardinality constraint
+ Node cardNode = d_cardinality_literal[ d_cardinality ];
+ //bool value;
+ //bool hasValue = d_th->getValuation().hasSatValue( cardNode, value );
+ //Assert( hasValue );
+ //Assert( value );
+ conflictNode = NodeManager::currentNM()->mkNode( IMPLIES, conflictNode, cardNode.notNode() );
+ Trace("uf-ss-lemma") << "*** Add clique lemma " << conflictNode << std::endl;
+ out->lemma( conflictNode );
+ ++( d_th->getStrongSolver()->d_statistics.d_clique_lemmas );
+ }
- //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
+ //DO_THIS: ensure that the same clique is not reported??? Check standard effort after assertDisequal can produce same clique.
+ }
}
void StrongSolverTheoryUf::SortRepModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
}
void StrongSolverTheoryUf::SortRepModel::getRepresentatives( std::vector< Node >& reps ){
- if( !options::ufssColoringSat() ){
+ //if( !options::ufssColoringSat() ){
bool foundRegion = false;
for( int i=0; i<(int)d_regions_index; i++ ){
//should not have multiple regions at this point
foundRegion = true;
}
}
- }else{
- Unimplemented("Build representatives for fmf region sat is not implemented");
- }
-}
-
-
-/** initialize */
-void StrongSolverTheoryUf::InfRepModel::initialize( OutputChannel* out ){
-
-}
-
-/** new node */
-void StrongSolverTheoryUf::InfRepModel::newEqClass( Node n ){
- d_rep[n] = n;
- //d_const_rep[n] = n.getMetaKind()==metakind::CONSTANT;
-}
-
-/** merge */
-void StrongSolverTheoryUf::InfRepModel::merge( Node a, Node b ){
- //d_rep[b] = false;
- //d_const_rep[a] = d_const_rep[a] || d_const_rep[b];
- Node repb = d_rep[b];
- Assert( !repb.isNull() );
- if( repb.getMetaKind()==metakind::CONSTANT || isBadRepresentative( d_rep[a] ) ){
- d_rep[a] = repb;
- }
- d_rep[b] = Node::null();
-}
-
-/** check */
-void StrongSolverTheoryUf::InfRepModel::check( Theory::Effort level, OutputChannel* out ){
-
-}
-
-/** minimize */
-bool StrongSolverTheoryUf::InfRepModel::minimize( OutputChannel* out ){
-#if 0
- bool retVal = true;
-#else
- bool retVal = !addSplit( out );
-#endif
- if( retVal ){
- std::vector< Node > reps;
- getRepresentatives( reps );
- Trace("uf-ss-fmf") << "Num representatives of type " << d_type << " : " << reps.size() << std::endl;
- /*
- for( int i=0; i<(int)reps.size(); i++ ){
- std::cout << reps[i] << " ";
- }
- std::cout << std::endl;
- for( int i=0; i<(int)reps.size(); i++ ){
- std::cout << reps[i].getMetaKind() << " ";
- }
- std::cout << std::endl;
- for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
- Node rep = (*it).second;
- if( !rep.isNull() && !isBadRepresentative( rep ) ){
- for( NodeNodeMap::iterator it2 = d_rep.begin(); it2 != d_rep.end(); ++it2 ){
- Node rep2 = (*it2).second;
- if( !rep2.isNull() && !isBadRepresentative( rep2 ) ){
- if( d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, rep2 ) ){
- std::cout << "1 ";
- }else{
- std::cout << "0 ";
- }
- }
- }
- //std::cout << " : " << rep;
- std::cout << std::endl;
- }
- }
- */
- }
- return retVal;
-}
-
-/** get representatives */
-void StrongSolverTheoryUf::InfRepModel::getRepresentatives( std::vector< Node >& reps ){
- for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
- if( !(*it).second.isNull() ){
- reps.push_back( (*it).first );
- }
- }
-}
-
-
-/** add split function */
-bool StrongSolverTheoryUf::InfRepModel::addSplit( OutputChannel* out ){
- std::vector< Node > visited;
- for( NodeNodeMap::iterator it = d_rep.begin(); it != d_rep.end(); ++it ){
- Node rep = (*it).second;
- if( !rep.isNull() && !isBadRepresentative( rep ) ){
- bool constRep = rep.getMetaKind()==metakind::CONSTANT;
- for( size_t i=0; i<visited.size(); i++ ){
- if( !constRep || !visited[i].getMetaKind()==metakind::CONSTANT ){
- if( !d_th->getQuantifiersEngine()->getEqualityQuery()->areDisequal( rep, visited[i] ) ){
- //split on these nodes
- Node eq = rep.eqNode( visited[i] );
- Trace("uf-ss-lemma") << "*** Split on " << eq << std::endl;
- eq = Rewriter::rewrite( eq );
- Debug("uf-ss-lemma-debug") << "Rewritten " << eq << std::endl;
- out->split( eq );
- //explore the equals branch first
- out->requirePhase( eq, true );
- ++( d_th->getStrongSolver()->d_statistics.d_split_lemmas );
- return true;
- }
- }
- }
- visited.push_back( rep );
- }
- }
- return false;
-}
-
-bool StrongSolverTheoryUf::InfRepModel::isBadRepresentative( Node n ){
- return n.getKind()==kind::PLUS;
+ //}else{
+ // Unimplemented("Build representatives for fmf region sat is not implemented");
+ //}
}
StrongSolverTheoryUf::StrongSolverTheoryUf(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) :
if( level==Theory::EFFORT_FULL ){
debugPrint( "uf-ss-debug" );
}
+ if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
+ int lemmas = d_term_amb->disambiguateTerms( d_out );
+ d_statistics.d_disamb_term_lemmas += lemmas;
+ if( lemmas>=0 ){
+ return;
+ }
+ }
for( std::map< TypeNode, RepModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
it->second->check( level, d_out );
if( it->second->isConflict() ){
}
}
//disambiguate terms if necessary
- if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
- Assert( d_term_amb!=NULL );
- d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
- }
+ //if( !d_conflict && level==Theory::EFFORT_FULL && options::ufssColoringSat() ){
+ // Assert( d_term_amb!=NULL );
+ // d_statistics.d_disamb_term_lemmas += d_term_amb->disambiguateTerms( d_out );
+ //}
Trace("uf-ss-solver") << "Done StrongSolverTheoryUf: check " << level << std::endl;
}
}
if( tn.isSort() ){
Trace("uf-ss-register") << "Preregister sort " << tn << "." << std::endl;
rm = new SortRepModel( n, d_th->getSatContext(), d_th );
- }else if( tn.isInteger() ){
- //rm = new InfRepModel( tn, d_th->getSatContext(), d_th );
- //rm = new SortRepModel( tn, d_th->getSatContext(), d_th );
}else{
/*
if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
}
StrongSolverTheoryUf::Statistics::Statistics():
+ d_clique_conflicts("StrongSolverTheoryUf::Clique_Conflicts", 0),
d_clique_lemmas("StrongSolverTheoryUf::Clique_Lemmas", 0),
d_split_lemmas("StrongSolverTheoryUf::Split_Lemmas", 0),
d_disamb_term_lemmas("StrongSolverTheoryUf::Disambiguate_Term_Lemmas", 0),
d_totality_lemmas("StrongSolverTheoryUf::Totality_Lemmas", 0),
d_max_model_size("StrongSolverTheoryUf::Max_Model_Size", 1)
{
+ StatisticsRegistry::registerStat(&d_clique_conflicts);
StatisticsRegistry::registerStat(&d_clique_lemmas);
StatisticsRegistry::registerStat(&d_split_lemmas);
StatisticsRegistry::registerStat(&d_disamb_term_lemmas);
}
StrongSolverTheoryUf::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_clique_conflicts);
StatisticsRegistry::unregisterStat(&d_clique_lemmas);
StatisticsRegistry::unregisterStat(&d_split_lemmas);
StatisticsRegistry::unregisterStat(&d_disamb_term_lemmas);
}
Assert( children.size()>1 );
Node lem = NodeManager::currentNM()->mkNode( OR, children );
- Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
+ Trace( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
//Notice() << "*** Disambiguate lemma : " << lem << std::endl;
out->lemma( lem );
d_term_amb[ eq ] = false;
lemmaAdded++;
+ return lemmaAdded;
}
}
}
void setSplitScore( Node n, int s );
private:
/** check if we need to combine region ri */
- void checkRegion( int ri, bool rec = true );
+ void checkRegion( int ri, bool checkCombine = true );
/** force combine region */
int forceCombineRegion( int ri, bool useDensity = true );
/** merge regions */
/** get number of regions (for debugging) */
int getNumRegions();
}; /** class SortRepModel */
-private:
- /** infinite rep model */
- class InfRepModel : public RepModel
- {
- protected:
- /** theory uf pointer */
- TheoryUF* d_th;
- /** list of representatives */
- NodeNodeMap d_rep;
- /** whether representatives are constant */
- NodeBoolMap d_const_rep;
- /** add split */
- bool addSplit( OutputChannel* out );
- /** is bad representative */
- bool isBadRepresentative( Node n );
- public:
- InfRepModel( TypeNode tn, context::Context* c, TheoryUF* th ) : RepModel( tn ),
- d_th( th ), d_rep( c ), d_const_rep( c ){}
- virtual ~InfRepModel(){}
- /** initialize */
- void initialize( OutputChannel* out );
- /** new node */
- void newEqClass( Node n );
- /** merge */
- void merge( Node a, Node b );
- /** assert terms are disequal */
- void assertDisequal( Node a, Node b, Node reason ){}
- /** check */
- void check( Theory::Effort level, OutputChannel* out );
- /** minimize */
- bool minimize( OutputChannel* out );
- /** get representatives */
- void getRepresentatives( std::vector< Node >& reps );
- /** print debug */
- void debugPrint( const char* c ){}
- };
private:
/** The output channel for the strong solver. */
OutputChannel* d_out;
class Statistics {
public:
+ IntStat d_clique_conflicts;
IntStat d_clique_lemmas;
IntStat d_split_lemmas;
IntStat d_disamb_term_lemmas;
printSort( "sort-inference", it->second );\r
Trace("sort-inference") << std::endl;\r
}\r
+ for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){\r
+ Trace("sort-inference") << "Quantified formula " << it->first << " : " << std::endl;\r
+ for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ printSort( "sort-inference", it2->second );\r
+ Trace("sort-inference") << std::endl;\r
+ }\r
+ Trace("sort-inference") << std::endl;\r
+ }\r
}\r
if( doRewrite ){\r
//simplify all assertions by introducing new symbols wherever necessary (NOTE: this is unsound for quantifiers)\r
if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){\r
for( size_t i=0; i<n[0].getNumChildren(); i++ ){\r
//TODO: try applying sort inference to quantified variables\r
- //d_var_types[n][ n[0][i] ] = sortCount;\r
- //sortCount++;\r
+ d_var_types[n][ n[0][i] ] = sortCount;\r
+ sortCount++;\r
\r
//type of the quantified variable must be the same\r
- d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );\r
+ //d_var_types[n][ n[0][i] ] = getIdForType( n[0][i].getType() );\r
var_bound[ n[0][i] ] = n;\r
}\r
}\r
}\r
\r
}\r
+int SortInference::getSortId( Node n ) {\r
+ Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n;\r
+ return getRepresentative( d_op_return_types[op] );\r
+}\r
+\r
+int SortInference::getSortId( Node f, Node v ) {\r
+ return getRepresentative( d_var_types[f][v] );\r
+}\r
\r
+void SortInference::setSkolemVar( Node f, Node v, Node sk ){\r
+ d_op_return_types[sk] = getSortId( f, v );\r
}\r
+\r
+}
\ No newline at end of file
~SortInference(){}\r
\r
void simplify( std::vector< Node >& assertions, bool doRewrite = false );\r
+ int getSortId( Node n );\r
+ int getSortId( Node f, Node v );\r
+ //set that sk is the skolem variable of v for quantifier f\r
+ void setSkolemVar( Node f, Node v, Node sk );\r
};\r
\r
}\r
bug421.smt2 \
bug421b.smt2 \
bug425.cvc \
- bug480.smt2
-# bug486.cvc
+ bug480.smt2 \
+ bug486.cvc
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
smtlib46f14a.smt2 \
smtlibf957ea.smt2 \
gauss_init_0030.fof.smt2 \
- piVC_5581bd.smt2 \
- set3.smt2
+ piVC_5581bd.smt2
+
+# regression can be solved with --finite-model-find --fmf-inst-engine
+# set3.smt2
# removed because it now reports unknown
# symmetric_unsat_7.smt2 \
projects / cvc5.git / commitdiff