#include "theory/quantifiers/model_builder.h"\r
#include "theory/quantifiers/first_order_model.h"\r
\r
-#define RECONSIDER_FUNC_CONSTANT\r
+//#define CHILD_USE_CONSIDER\r
\r
using namespace std;\r
using namespace CVC4;\r
}\r
\r
void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){\r
+ Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;\r
//whether we are doing a product or sum or matches\r
bool doProduct = true;\r
//get the model\r
std::vector< Node > considerTerms;\r
std::vector< std::vector< Node > > newConsiderVal;\r
std::vector< bool > newUseConsider;\r
+ std::map< Node, InstMatch > considerTermsMatch[2];\r
+ std::map< Node, bool > considerTermsSuccess[2];\r
newConsiderVal.resize( d_children.size() );\r
- newUseConsider.resize( d_children.size(), false );\r
+ newUseConsider.resize( d_children.size(), useConsider );\r
if( d_node.getKind()==APPLY_UF ){\r
Node op = d_node.getOperator();\r
if( useConsider ){\r
+#ifndef CHILD_USE_CONSIDER\r
+ for( size_t i=0; i<newUseConsider.size(); i++ ){\r
+ newUseConsider[i] = false;\r
+ }\r
+#endif\r
for( size_t i=0; i<considerVal.size(); i++ ){\r
eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( considerVal[i] ),\r
qe->getEqualityQuery()->getEngine() );\r
while( !eqc.isFinished() ){\r
Node en = (*eqc);\r
if( en.getKind()==APPLY_UF && en.getOperator()==op ){\r
- bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( en );\r
- bool isActive = !en.getAttribute(NoMatchAttribute());\r
- //check if we need to consider it\r
- if( isSelected || isActive ){\r
considerTerms.push_back( en );\r
-#if 0\r
- for( int i=0; i<(int)d_children.size(); i++ ){\r
- int childIndex = d_children_index[i];\r
- Node n = qe->getModel()->getRepresentative( n );\r
- if( std::find( newConsiderVal[i].begin(), newConsiderVal[i].end(), n )==newConsiderVal[i].end() ){\r
- newConsiderVal[i].push_back( n );\r
- }\r
- }\r
-#endif\r
- }\r
}\r
++eqc;\r
}\r
}else{\r
considerTerms.insert( considerTerms.begin(), fm->d_uf_terms[op].begin(), fm->d_uf_terms[op].end() );\r
}\r
- }else if( d_node.getType().isBoolean() ){\r
- if( useConsider ){\r
- Assert( considerVal.size()==1 );\r
- bool reqPol = considerVal[0]==fm->d_true;\r
- if( d_node.getKind()==NOT ){\r
- if( !newConsiderVal.empty() ){\r
- newConsiderVal[0].push_back( reqPol ? fm->d_false : fm->d_true );\r
- newUseConsider[0] = true;\r
+ //for each term we consider, calculate a current match\r
+ for( size_t i=0; i<considerTerms.size(); i++ ){\r
+ Node n = considerTerms[i];\r
+ bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );\r
+ bool hadSuccess = false;\r
+ for( int t=(isSelected ? 0 : 1); t<2; t++ ){\r
+ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){\r
+ considerTermsMatch[t][n] = InstMatch();\r
+ considerTermsSuccess[t][n] = true;\r
+ for( size_t j=0; j<d_node.getNumChildren(); j++ ){\r
+ if( d_children_map.find( j )==d_children_map.end() ){\r
+ if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){\r
+ if( d_node[j].getKind()==INST_CONSTANT ){\r
+ if( !considerTermsMatch[t][n].setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){\r
+ Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to ";\r
+ Trace("inst-gen-cm") << considerTermsMatch[t][n].getValue( d_node[j] ) << std::endl;\r
+ considerTermsSuccess[t][n] = false;\r
+ break;\r
+ }\r
+ }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){\r
+ Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;\r
+ considerTermsSuccess[t][n] = false;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ //if successful, store it\r
+ if( considerTermsSuccess[t][n] ){\r
+#ifdef CHILD_USE_CONSIDER\r
+ if( !hadSuccess ){\r
+ hadSuccess = true;\r
+ for( size_t k=0; k<d_children.size(); k++ ){\r
+ if( newUseConsider[k] ){\r
+ int childIndex = d_children_index[k];\r
+ //determine if we are restricted or not\r
+ if( t!=0 || !n[childIndex].getAttribute(ModelBasisAttribute()) ){\r
+ Node r = qe->getModel()->getRepresentative( n[childIndex] );\r
+ if( std::find( newConsiderVal[k].begin(), newConsiderVal[k].end(), r )==newConsiderVal[k].end() ){\r
+ newConsiderVal[k].push_back( r );\r
+ //check if we now need to consider the entire domain\r
+ TypeNode tn = r.getType();\r
+ if( qe->getModel()->d_rep_set.hasType( tn ) ){\r
+ if( (int)newConsiderVal[k].size()>=qe->getModel()->d_rep_set.getNumRepresentatives( tn ) ){\r
+ newConsiderVal[k].clear();\r
+ newUseConsider[k] = false;\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ //matching against selected term, will need to consider all values\r
+ newConsiderVal[k].clear();\r
+ newUseConsider[k] = false;\r
+ }\r
+ }\r
+ }\r
+ }\r
+#endif\r
+ }\r
}\r
- }else if( d_node.getKind()==AND || d_node.getKind()==OR ){\r
- for( size_t i=0; i<newConsiderVal.size(); i++ ){\r
- newConsiderVal[i].push_back( considerVal[0] );\r
- newUseConsider[i] = true;\r
+ }\r
+ }\r
+ }else{\r
+ //the interpretted case\r
+ if( d_node.getType().isBoolean() ){\r
+ if( useConsider ){\r
+ //if( considerVal.size()!=1 ) { std::cout << "consider val = " << considerVal.size() << std::endl; }\r
+ Assert( considerVal.size()==1 );\r
+ bool reqPol = considerVal[0]==fm->d_true;\r
+ Node ncv = considerVal[0];\r
+ if( d_node.getKind()==NOT ){\r
+ ncv = reqPol ? fm->d_false : fm->d_true;\r
}\r
- //instead we will do a sum\r
- if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){\r
- doProduct = false;\r
+ if( d_node.getKind()==NOT || d_node.getKind()==AND || d_node.getKind()==OR ){\r
+ for( size_t i=0; i<newConsiderVal.size(); i++ ){\r
+ newConsiderVal[i].push_back( ncv );\r
+ }\r
+ //instead we will do a sum\r
+ if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){\r
+ doProduct = false;\r
+ }\r
+ }else{\r
+ //do not use consider\r
+ for( size_t i=0; i<newUseConsider.size(); i++ ){\r
+ newUseConsider[i] = false;\r
+ }\r
}\r
}\r
}\r
return;\r
}\r
}\r
- Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;\r
if( d_node.getKind()==APPLY_UF ){\r
//if this is an uninterpreted function\r
Node op = d_node.getOperator();\r
//do not consider ground case if it is already congruent to another ground term\r
if( t==0 || !n.getAttribute(NoMatchAttribute()) ){\r
Trace("inst-gen-cm") << "calculate for " << n << ", selected = " << (t==0) << std::endl;\r
- bool success = true;\r
- InstMatch curr;\r
- for( size_t j=0; j<d_node.getNumChildren(); j++ ){\r
- if( d_children_map.find( j )==d_children_map.end() ){\r
- if( t!=0 || !n[j].getAttribute(ModelBasisAttribute()) ){\r
- if( d_node[j].getKind()==INST_CONSTANT ){\r
- //FIXME: is this correct?\r
- if( !curr.setMatch( qe->getEqualityQuery(), d_node[j], n[j] ) ){\r
- Trace("inst-gen-cm") << "fail match: " << n[j] << " is not equal to " << curr.get( d_node[j] ) << std::endl;\r
- Trace("inst-gen-cm") << " are equal : " << qe->getEqualityQuery()->areEqual( n[j], curr.get( d_node[j] ) ) << std::endl;\r
- success = false;\r
- break;\r
- }\r
- }else if( !qe->getEqualityQuery()->areEqual( d_node[j], n[j] ) ){\r
- Trace("inst-gen-cm") << "fail arg: " << n[j] << " is not equal to " << d_node[j] << std::endl;\r
- success = false;\r
- break;\r
- }\r
- }\r
- }\r
- }\r
- if( success ){\r
+ if( considerTermsSuccess[t][n] ){\r
//try to find unifier for d_node = n\r
- calculateMatchesUninterpreted( qe, f, curr, n, 0, t==0 );\r
+ calculateMatchesUninterpreted( qe, f, considerTermsMatch[t][n], n, 0, t==0 );\r
}\r
}\r
}\r
}\r
-\r
}else{\r
//if this is an interpreted function\r
if( doProduct ){\r
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;
// 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 );
}
}
-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 );
- //}
}
}
}
/** 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{
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 );
}
}
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 ) ){
/** 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 */
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 ){
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;
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 ){
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;
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++;
}else{
d_numQuantNoSelForm++;
}
- if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
+ if( optOneQuantPerRoundInstGen() && lems>0 ){
break;
}
}else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
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
//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.
}
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 ){
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++ ){
-
+////////////////////// 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 ){
}
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 ),
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;
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() ){
//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
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;
}
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
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 );
bool d_considerAxioms;
// set effort
void setEffort( int effort );
+ //debug model
+ void debugModel( FirstOrderModel* fm );
public:
//whether to construct model
virtual bool optUseModel();
/** 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();
};
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;
#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();
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;
- }
}
}
}
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;
}
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(){
StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
StatisticsRegistry::unregisterStat(&d_eval_lits);
StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
+ StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
}
IntStat d_eval_uf_terms;
IntStat d_eval_lits;
IntStat d_eval_lits_unknown;
+ IntStat d_exh_inst_lemmas;
Statistics();
~Statistics();
};
}
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;
}
}
+/** 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 );
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) */
bool Trigger::getNextMatch( InstMatch& m ){
bool retVal = d_mg->getNextMatch( m, d_quantEngine );
- //m.makeInternal( d_quantEngine->getEqualityQuery() );
return retVal;
}
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 ){
}
}
+int getDepth( Node n ){
+ if( n.getNumChildren()==0 ){
+ return 0;
+ }else{
+ int maxDepth = -1;
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ int depth = getDepth( n[i] );
+ if( depth>maxDepth ){
+ maxDepth = depth;
+ }
+ }
+ return maxDepth;
+ }
+}
+
int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
- return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
+ return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n]; //initial
+ //return ( d_rep_score.find( n )==d_rep_score.end() ? 100 : 0 ) + getDepth( n ); //term depth
}
}
}
-#if 0
-
-void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e ){
- if( e<4 ){
- return STATUS_UNFINISHED;
- }else{
- for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin();
- it != InstMatchGenerator::d_match_fails.end(); ++it ){
- for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
- if( !it2->second.empty() ){
- Node n1 = it->first;
- Node n2 = it2->first;
- if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){
- d_quantEngine->addSplitEquality( n1, n2, true );
- }
- it2->second.clear();
- }
- }
- }
- return STATUS_UNKNOWN;
- }
-}
-
-#endif /* 0 */
-
void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
}
void setGenerateAdditional( bool val ) { d_generate_additional = val; }
};/* class InstStrategyAutoGenTriggers */
-#if 0
-
-class InstStrategyAddFailSplits : public InstStrategy{
-private:
- /** InstantiatorTheoryUf class */
- InstantiatorTheoryUf* d_th;
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ){}
- ~InstStrategyAddFailSplits(){}
- /** identify */
- std::string identify() const { return std::string("AddFailSplits"); }
-};/* class InstStrategyAddFailSplits */
-
-#endif /* 0 */
-
class InstStrategyFreeVariable : public InstStrategy{
private:
/** InstantiatorTheoryUf class */
projects / cvc5.git / commitdiff