diff options
Diffstat (limited to 'src/theory/quantifiers')
| -rwxr-xr-x | src/theory/quantifiers/inst_gen.cpp | 152 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 37 | ||||
| -rw-r--r-- | src/theory/quantifiers/inst_match.h | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 123 | ||||
| -rw-r--r-- | src/theory/quantifiers/model_builder.h | 12 | ||||
| -rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 34 | ||||
| -rw-r--r-- | src/theory/quantifiers/model_engine.h | 1 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 55 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 5 |
10 files changed, 239 insertions, 192 deletions
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 428a224ee..932a00185 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -19,7 +19,7 @@ #include "theory/quantifiers/model_builder.h"
#include "theory/quantifiers/first_order_model.h"
-#define RECONSIDER_FUNC_CONSTANT
+//#define CHILD_USE_CONSIDER
using namespace std;
using namespace CVC4;
@@ -55,6 +55,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins }
void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){
+ Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
//whether we are doing a product or sum or matches
bool doProduct = true;
//get the model
@@ -64,32 +65,25 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto std::vector< Node > considerTerms;
std::vector< std::vector< Node > > newConsiderVal;
std::vector< bool > newUseConsider;
+ std::map< Node, InstMatch > considerTermsMatch[2];
+ std::map< Node, bool > considerTermsSuccess[2];
newConsiderVal.resize( d_children.size() );
- newUseConsider.resize( d_children.size(), false );
+ newUseConsider.resize( d_children.size(), useConsider );
if( d_node.getKind()==APPLY_UF ){
Node op = d_node.getOperator();
if( useConsider ){
+#ifndef CHILD_USE_CONSIDER
+ for( size_t i=0; i<newUseConsider.size(); i++ ){
+ newUseConsider[i] = false;
+ }
+#endif
for( size_t i=0; i<considerVal.size(); i++ ){
eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),
qe->getEqualityQuery()->getEngine() );
while( !eqc.isFinished() ){
Node en = (*eqc);
if( en.getKind()==APPLY_UF && en.getOperator()==op ){
- bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( en );
- bool isActive = !en.getAttribute(NoMatchAttribute());
- //check if we need to consider it
- if( isSelected || isActive ){
considerTerms.push_back( en );
-#if 0
- for( int i=0; i<(int)d_children.size(); i++ ){
- int childIndex = d_children_index[i];
- Node n = qe->getModel()->getRepresentative( n );
- if( std::find( newConsiderVal[i].begin(), newConsiderVal[i].end(), n )==newConsiderVal[i].end() ){
- newConsiderVal[i].push_back( n );
- }
- }
-#endif
- }
}
++eqc;
}
@@ -97,23 +91,92 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto }else{
considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );
}
- }else if( d_node.getType().isBoolean() ){
- if( useConsider ){
- Assert( considerVal.size()==1 );
- bool reqPol = considerVal[0]==fm->d_true;
- if( d_node.getKind()==NOT ){
- if( !newConsiderVal.empty() ){
- newConsiderVal[0].push_back( reqPol ? fm->d_false : fm->d_true );
- newUseConsider[0] = true;
+ //for each term we consider, calculate a current match
+ for( size_t i=0; i<considerTerms.size(); i++ ){
+ Node n = considerTerms[i];
+ bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+ bool hadSuccess = false;
+ for( int t=(isSelected ? 0 : 1); t<2; t++ ){
+ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
+ considerTermsMatch[t][n] = InstMatch();
+ considerTermsSuccess[t][n] = true;
+ for( size_t j=0; j<d_node.getNumChildren(); j++ ){
+ if( d_children_map.find( j )==d_children_map.end() ){
+ if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
+ if( d_node[j].getKind()==INST_CONSTANT ){
+ if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
+ Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";
+ Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;
+ considerTermsSuccess[t][n] = false;
+ break;
+ }
+ }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
+ Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
+ considerTermsSuccess[t][n] = false;
+ break;
+ }
+ }
+ }
+ }
+ //if successful, store it
+ if( considerTermsSuccess[t][n] ){
+#ifdef CHILD_USE_CONSIDER
+ if( !hadSuccess ){
+ hadSuccess = true;
+ for( size_t k=0; k<d_children.size(); k++ ){
+ if( newUseConsider[k] ){
+ int childIndex = d_children_index[k];
+ //determine if we are restricted or not
+ if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){
+ Node r = qe->getModel()->getRepresentative( n[childIndex] );
+ if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){
+ newConsiderVal[k].push_back( r );
+ //check if we now need to consider the entire domain
+ TypeNode tn = r.getType();
+ if( qe->getModel()->d_rep_set.hasType( tn ) ){
+ if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){
+ newConsiderVal[k].clear();
+ newUseConsider[k] = false;
+ }
+ }
+ }
+ }else{
+ //matching against selected term, will need to consider all values
+ newConsiderVal[k].clear();
+ newUseConsider[k] = false;
+ }
+ }
+ }
+ }
+#endif
+ }
}
- }else if( d_node.getKind()==AND || d_node.getKind()==OR ){
- for( size_t i=0; i<newConsiderVal.size(); i++ ){
- newConsiderVal[i].push_back( considerVal[0] );
- newUseConsider[i] = true;
+ }
+ }
+ }else{
+ //the interpretted case
+ if( d_node.getType().isBoolean() ){
+ if( useConsider ){
+ //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }
+ Assert( considerVal.size()==1 );
+ bool reqPol = considerVal[0]==fm->d_true;
+ Node ncv = considerVal[0];
+ if( d_node.getKind()==NOT ){
+ ncv = reqPol ? fm->d_false : fm->d_true;
}
- //instead we will do a sum
- if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){
- doProduct = false;
+ if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){
+ for( size_t i=0; i<newConsiderVal.size(); i++ ){
+ newConsiderVal[i].push_back( ncv );
+ }
+ //instead we will do a sum
+ if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){
+ doProduct = false;
+ }
+ }else{
+ //do not use consider
+ for( size_t i=0; i<newUseConsider.size(); i++ ){
+ newUseConsider[i] = false;
+ }
}
}
}
@@ -126,7 +189,6 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto return;
}
}
- Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;
if( d_node.getKind()==APPLY_UF ){
//if this is an uninterpreted function
Node op = d_node.getOperator();
@@ -138,35 +200,13 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //do not consider ground case if it is already congruent to another ground term
if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;
- bool success = true;
- InstMatch curr;
- for( size_t j=0; j<d_node.getNumChildren(); j++ ){
- if( d_children_map.find( j )==d_children_map.end() ){
- if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){
- if( d_node[j].getKind()==INST_CONSTANT ){
- //FIXME: is this correct?
- if( !curr.setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){
- Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl;
- Trace("inst-gen-cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl;
- success = false;
- break;
- }
- }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){
- Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;
- success = false;
- break;
- }
- }
- }
- }
- if( success ){
+ if( considerTermsSuccess[t][n] ){
//try to find unifier for d_node = n
- calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 );
+ calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );
}
}
}
}
-
}else{
//if this is an interpreted function
if( doProduct ){
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 4a89a4dd3..16f06017e 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -54,9 +54,11 @@ bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){ bool InstMatch::add( InstMatch& m ){ for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){ - std::map< Node, Node >::iterator itf = d_map.find( it->first ); - if( itf==d_map.end() || itf->second.isNull() ){ - d_map[it->first] = it->second; + if( !it->second.isNull() ){ + std::map< Node, Node >::iterator itf = d_map.find( it->first ); + if( itf==d_map.end() || itf->second.isNull() ){ + d_map[it->first] = it->second; + } } } return true; @@ -91,7 +93,7 @@ void InstMatch::debugPrint( const char* c ){ // Debug( c ) << std::endl; //} } -/* + void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ for( size_t i=0; i<f[0].getNumChildren(); i++ ){ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i ); @@ -101,27 +103,18 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ } } -void InstMatch::makeInternal( QuantifiersEngine* qe ){ - if( options::cbqi() ){ - for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ - if( it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second ); - if( it->second.hasAttribute(InstConstantAttribute()) ){ - d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); - } - } - } +void InstMatch::makeInternalRepresentative( QuantifiersEngine* qe ){ + EqualityQueryQuantifiersEngine* eqqe = (EqualityQueryQuantifiersEngine*)qe->getEqualityQuery(); + for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ + d_map[ it->first ] = eqqe->getInternalRepresentative( it->second ); } } -*/ + void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){ if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){ d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second ); } - //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){ - // d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first ); - //} } } @@ -132,8 +125,8 @@ void InstMatch::applyRewrite(){ } /** get value */ -Node InstMatch::getValue( Node var ){ - std::map< Node, Node >::iterator it = d_map.find( var ); +Node InstMatch::getValue( Node var ) const{ + std::map< Node, Node >::const_iterator it = d_map.find( var ); if( it!=d_map.end() ){ return it->second; }else{ @@ -145,7 +138,7 @@ Node InstMatch::getValue( Node var ){ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); d_data[n].addInstMatch2( qe, f, m, index+1, imtio ); } } @@ -156,7 +149,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& return true; }else{ int i_index = imtio ? imtio->d_order[index] : index; - Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 43c0d26c7..41ebb63d2 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -55,13 +55,13 @@ public: /** is complete? */ bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); } /** make complete */ - //void makeComplete( Node f, QuantifiersEngine* qe ); - /** make internal: ensure that no term in d_map contains instantiation constants */ - //void makeInternal( QuantifiersEngine* qe ); + void makeComplete( Node f, QuantifiersEngine* qe ); + /** make internal representative */ + void makeInternalRepresentative( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); /** get value */ - Node getValue( Node var ); + Node getValue( Node var ) const; /** clear */ void clear(){ d_map.clear(); } /** is_empty */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 8b34a3a12..c7e68acb1 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -59,6 +59,35 @@ d_qe( qe ), d_curr_model( c, NULL ){ d_considerAxioms = true; } +void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){ + //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true + if( Trace.isOn("quant-model-warn") ){ + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + std::vector< Node > vars; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + vars.push_back( f[0][j] ); + } + RepSetIterator riter( &(fm->d_rep_set) ); + riter.setQuantifier( f ); + while( !riter.isFinished() ){ + std::vector< Node > terms; + for( int i=0; i<riter.getNumTerms(); i++ ){ + terms.push_back( riter.getTerm( i ) ); + } + Node n = d_qe->getInstantiation( f, vars, terms ); + Node val = fm->getValue( n ); + if( val!=fm->d_true ){ + Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; + Trace("quant-model-warn") << " " << f << std::endl; + Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + } + riter.increment(); + } + } + } +} + void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* fm = (FirstOrderModel*)m; if( fullModel ){ @@ -73,33 +102,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { TheoryEngineModelBuilder::processBuildModel( m, fullModel ); //mark that the model has been set fm->markModelSet(); - //FOR DEBUGGING - if( Trace.isOn("quant-model-warn") ){ - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - std::vector< Node > vars; - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - vars.push_back( f[0][j] ); - } - RepSetIterator riter( &(fm->d_rep_set) ); - riter.setQuantifier( f ); - while( !riter.isFinished() ){ - std::vector< Node > terms; - for( int i=0; i<riter.getNumTerms(); i++ ){ - terms.push_back( riter.getTerm( i ) ); - } - Node n = d_qe->getInstantiation( f, vars, terms ); - Node val = fm->getValue( n ); - if( val!=fm->d_true ){ - Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; - Trace("quant-model-warn") << " " << f << std::endl; - Trace("quant-model-warn") << " Evaluates to " << val << std::endl; - } - riter.increment(); - } - } - } - //END FOR DEBUGGING + //debug the model + debugModel( fm ); }else{ d_curr_model = fm; d_addedLemmas = 0; @@ -113,7 +117,9 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ - d_addedLemmas += initializeQuantifier( f, f ); + int lems = initializeQuantifier( f, f ); + d_statistics.d_init_inst_gen_lemmas += lems; + d_addedLemmas += lems; } } if( d_addedLemmas>0 ){ @@ -128,14 +134,14 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl; d_quant_sat.clear(); d_uf_prefs.clear(); - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ analyzeQuantifier( fm, f ); } } - //if applicable, find exceptions + + //if applicable, find exceptions to model via inst-gen if( optInstGen() ){ d_didInstGen = true; d_instGenMatches = 0; @@ -148,10 +154,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ - int addedLemmas = doInstGen( fm, f ); - d_addedLemmas += addedLemmas; + int lems = doInstGen( fm, f ); + d_statistics.d_inst_gen_lemmas += lems; + d_addedLemmas += lems; //temporary - if( addedLemmas>0 ){ + if( lems>0 ){ d_numQuantInstGen++; }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ d_numQuantSat++; @@ -160,7 +167,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { }else{ d_numQuantNoSelForm++; } - if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){ + if( optOneQuantPerRoundInstGen() && lems>0 ){ break; } }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ @@ -208,7 +215,7 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){ //create the basis match if necessary if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){ - Trace("inst-fmf-init") << "Initialize " << f << ", parent = " << fp << std::endl; + Trace("inst-fmf-init") << "Initialize " << f << std::endl; //add the model basis instantiation // This will help produce the necessary information for model completion. // We do this by extending distinguish ground assertions (those @@ -236,7 +243,6 @@ int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){ //add model basis instantiation if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ d_quant_basis_match_added[f] = true; - ++(d_statistics.d_num_quants_init_success); return 1; }else{ //shouldn't happen usually, but will occur if x != y is a required literal for f. @@ -322,22 +328,22 @@ void ModelEngineBuilder::setEffort( int effort ){ } ModelEngineBuilder::Statistics::Statistics(): - d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), - d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0), - d_num_quants_init("ModelEngine::Num_Quants", 0 ), - d_num_quants_init_success("ModelEngine::Num_Quants_Inst_Gen_Success", 0 ) + d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0), + d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0), + d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ), + d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 ) { - StatisticsRegistry::registerStat(&d_pre_sat_quant); - StatisticsRegistry::registerStat(&d_pre_nsat_quant); StatisticsRegistry::registerStat(&d_num_quants_init); - StatisticsRegistry::registerStat(&d_num_quants_init_success); + StatisticsRegistry::registerStat(&d_num_partial_quants_init); + StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas); + StatisticsRegistry::registerStat(&d_inst_gen_lemmas); } ModelEngineBuilder::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_pre_sat_quant); - StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); StatisticsRegistry::unregisterStat(&d_num_quants_init); - StatisticsRegistry::unregisterStat(&d_num_quants_init_success); + StatisticsRegistry::unregisterStat(&d_num_partial_quants_init); + StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas); + StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas); } bool ModelEngineBuilder::isQuantifierActive( Node f ){ @@ -470,9 +476,7 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false; } Debug("fmf-model-prefs") << std::endl; - ++(d_statistics.d_pre_sat_quant); }else{ - ++(d_statistics.d_pre_nsat_quant); //note quantifier's value preferences to models for( int k=0; k<2; k++ ){ for( int j=0; j<(int)pro_con[k].size(); j++ ){ @@ -604,12 +608,14 @@ void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ) - +////////////////////// Inst-Gen style Model Builder /////////// void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){ //for new inst gen d_quant_selection_formula.clear(); d_term_selected.clear(); + + //d_sub_quant_inst_trie.clear();//* } int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ @@ -621,6 +627,9 @@ int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){ } void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + //Node fp = getParentQuantifier( f );//* + //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ); + //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//* Trace("sel-form-debug") << "* Analyze " << f << std::endl; //determine selection formula, set terms in selection formula as being selected Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ), @@ -659,9 +668,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; if( fp!=f ) Trace("inst-gen") << " "; Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula[f] << std::endl; - //we wish to add all known exceptions to our selection literal for f. this will help to refine our current model. - //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms, - // effectively acting as partial instantiations instead of pointwise instantiations. + //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model. if( !d_quant_selection_formula[f].isNull() ){ //first, try on sub quantifiers bool subQuantSat = true; @@ -688,6 +695,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ if( igp.getMatchValue( i )!=fm->d_true ){ InstMatch m; igp.getMatch( d_qe->getEqualityQuery(), i, m ); + //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl; //we only consider matches that are non-empty // matches that are empty should trigger other instances that are non-empty if( !m.empty() ){ @@ -695,9 +703,12 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ //translate to be in terms match in terms of fp InstMatch mp; getParentQuantifierMatch( mp, fp, m, f ); - //if this is a partial instantion if( !m.isComplete( f ) ){ + //need to make it internal here + //Trace("mkInternal") << "Make internal representative " << mp << std::endl; + //mp.makeInternalRepresentative( d_qe ); + //Trace("mkInternal") << "Got " << mp << std::endl; //if the instantiation does not yet exist if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ //also add it to children @@ -709,9 +720,11 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ d_sub_quants[ f ].push_back( pf ); d_sub_quant_inst[ pf ] = InstMatch( &mp ); d_sub_quant_parent[ pf ] = fp; - //now make the match mp complete + //now make mp a complete match mp.add( d_quant_basis_match[ fp ] ); d_quant_basis_match[ pf ] = InstMatch( &mp ); + ++(d_statistics.d_num_quants_init); + ++(d_statistics.d_num_partial_quants_init); addedLemmas += initializeQuantifier( pf, fp ); Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; subQuantSat = false; @@ -979,5 +992,5 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ) } bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ - return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, modInst ); + return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); }
\ No newline at end of file diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 7331daf8e..908cfca2b 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -69,7 +69,7 @@ protected: protected: //reset virtual void reset( FirstOrderModel* fm ) = 0; - //initialize quantifiers, return number of lemmas produced, fp is the parent of quantifier f + //initialize quantifiers, return number of lemmas produced virtual int initializeQuantifier( Node f, Node fp ); //analyze model virtual void analyzeModel( FirstOrderModel* fm ); @@ -98,6 +98,8 @@ public: bool d_considerAxioms; // set effort void setEffort( int effort ); + //debug model + void debugModel( FirstOrderModel* fm ); public: //whether to construct model virtual bool optUseModel(); @@ -110,10 +112,10 @@ public: /** statistics class */ class Statistics { public: - IntStat d_pre_sat_quant; - IntStat d_pre_nsat_quant; IntStat d_num_quants_init; - IntStat d_num_quants_init_success; + IntStat d_num_partial_quants_init; + IntStat d_init_inst_gen_lemmas; + IntStat d_inst_gen_lemmas; Statistics(); ~Statistics(); }; @@ -180,7 +182,7 @@ private: ///information for (new) InstGen std::map< Node, bool > d_term_selected; //a collection of (complete) InstMatch structures produced for each root quantifier std::map< Node, inst::InstMatchTrie > d_sub_quant_inst_trie; - //a collection of InstMatch structures, representing the children for each quantifier + //for each quantifier, a collection of InstMatch structures, representing the children std::map< Node, inst::InstMatchTrie > d_child_sub_quant_inst_trie; //children quantifiers for each quantifier, each is an instance std::map< Node, std::vector< Node > > d_sub_quants; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 87f842862..defb58bf2 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -153,19 +153,6 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #endif } -bool containsNN( Node n, Node nc ){ - if( n==nc ){ - return true; - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( containsNN( n[i], nc ) ){ - return true; - } - } - return false; - } -} - int ModelEngine::checkModel( int checkOption ){ int addedLemmas = 0; FirstOrderModel* fm = d_quantEngine->getModel(); @@ -177,20 +164,11 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " "; for( size_t i=0; i<it->second.size(); i++ ){ - Trace("model-engine-debug") << it->second[i] << " "; + //Trace("model-engine-debug") << it->second[i] << " "; + Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getInternalRepresentative( it->second[i] ); + Trace("model-engine-debug") << r << " "; } Trace("model-engine-debug") << std::endl; - for( size_t i=0; i<it->second.size(); i++ ){ - std::vector< Node > eqc; - d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc ); - Trace("model-engine-debug-eqc") << " " << it->second[i] << " : { "; - for( size_t j=0; j<eqc.size(); j++ ){ - if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){ - Trace("model-engine-debug-eqc") << eqc[j] << " "; - } - } - Trace("model-engine-debug-eqc") << "}" << std::endl; - } } } } @@ -242,6 +220,7 @@ int ModelEngine::checkModel( int checkOption ){ Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; } + d_statistics.d_exh_inst_lemmas += addedLemmas; return addedLemmas; } @@ -361,13 +340,15 @@ ModelEngine::Statistics::Statistics(): d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), d_eval_lits("ModelEngine::Eval_Lits", 0 ), - d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ) + d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ), + d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_eval_formulas); StatisticsRegistry::registerStat(&d_eval_uf_terms); StatisticsRegistry::registerStat(&d_eval_lits); StatisticsRegistry::registerStat(&d_eval_lits_unknown); + StatisticsRegistry::registerStat(&d_exh_inst_lemmas); } ModelEngine::Statistics::~Statistics(){ @@ -376,6 +357,7 @@ ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_eval_uf_terms); StatisticsRegistry::unregisterStat(&d_eval_lits); StatisticsRegistry::unregisterStat(&d_eval_lits_unknown); + StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 2560cf50e..394ceaf42 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -78,6 +78,7 @@ public: IntStat d_eval_uf_terms; IntStat d_eval_lits; IntStat d_eval_lits_unknown; + IntStat d_exh_inst_lemmas; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d637fa25f..591270ab0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -161,27 +161,29 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ } for( int i=0; i<2; i++ ){ Node n = NodeManager::currentNM()->mkConst( i==1 ); - eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ), - d_quantEngine->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - computeModelBasisArgAttribute( en ); - if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ - if( !en.getAttribute(NoMatchAttribute()) ){ - Node op = en.getOperator(); - if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ - NoMatchAttribute nma; - en.setAttribute(nma,true); - congruentCount++; + if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){ + eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ), + d_quantEngine->getEqualityQuery()->getEngine() ); + while( !eqc.isFinished() ){ + Node en = (*eqc); + computeModelBasisArgAttribute( en ); + if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){ + if( !en.getAttribute(NoMatchAttribute()) ){ + Node op = en.getOperator(); + if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ + NoMatchAttribute nma; + en.setAttribute(nma,true); + congruentCount++; + }else{ + nonCongruentCount++; + d_op_count[ op ]++; + } }else{ - nonCongruentCount++; - d_op_count[ op ]++; + alreadyCongruentCount++; } - }else{ - alreadyCongruentCount++; } + ++eqc; } - ++eqc; } } Debug("term-db-cong") << "TermDb: Reset" << std::endl; @@ -300,6 +302,25 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){ } } +/** get the i^th instantiation constant of f */ +Node TermDb::getInstantiationConstant( Node f, int i ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return it->second[i]; + }else{ + return Node::null(); + } +} + +/** get number of instantiation constants for f */ +int TermDb::getNumInstantiationConstants( Node f ) const { + std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( f ); + if( it!=d_inst_constants.end() ){ + return (int)it->second.size(); + }else{ + return 0; + } +} Node TermDb::getInstConstantBody( Node f ){ std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index e1786d44c..5060ac1a7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -154,9 +154,9 @@ private: void makeInstantiationConstantsFor( Node f ); public: /** get the i^th instantiation constant of f */ - Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } + Node getInstantiationConstant( Node f, int i ) const; /** get number of instantiation constants for f */ - int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } + int getNumInstantiationConstants( Node f ) const; /** get the ce body f[e/x] */ Node getInstConstantBody( Node f ); /** get counterexample literal (for cbqi) */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c64a75ec4..553189d13 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -85,7 +85,6 @@ void Trigger::reset( Node eqc ){ bool Trigger::getNextMatch( InstMatch& m ){ bool retVal = d_mg->getNextMatch( m, d_quantEngine ); - //m.makeInternal( d_quantEngine->getEqualityQuery() ); return retVal; } @@ -98,10 +97,6 @@ int Trigger::addTerm( Node t ){ return d_mg->addTerm( d_f, t, d_quantEngine ); } -//bool Trigger::nonunifiable( TNode t, const std::vector<Node> & vars){ -// return d_mg->nonunifiable(t,vars); -//} - int Trigger::addInstantiations( InstMatch& baseMatch ){ int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine ); if( addedLemmas>0 ){ |