if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){\r
d_match_values.push_back( val );\r
d_matches.push_back( InstMatch( &m ) );\r
+ qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;\r
}\r
}\r
}\r
\r
-void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){\r
+void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){\r
+ //whether we are doing a product or sum or matches\r
+ bool doProduct = true;\r
+ //get the model\r
+ FirstOrderModel* fm = qe->getModel();\r
+\r
+ //calculate terms we will consider\r
+ std::vector< Node > considerTerms;\r
+ std::vector< std::vector< Node > > newConsiderVal;\r
+ std::vector< bool > newUseConsider;\r
+ newConsiderVal.resize( d_children.size() );\r
+ newUseConsider.resize( d_children.size(), false );\r
+ if( d_node.getKind()==APPLY_UF ){\r
+ Node op = d_node.getOperator();\r
+ if( useConsider ){\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
+ }\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
+ }\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
+ //instead we will do a sum\r
+ if( ( d_node.getKind()==AND && !reqPol ) || ( d_node.getKind()==OR && reqPol ) ){\r
+ doProduct = false;\r
+ }\r
+ }\r
+ }\r
+ }\r
+\r
//calculate all matches for children\r
for( int i=0; i<(int)d_children.size(); i++ ){\r
- d_children[i].calculateMatches( qe, f );\r
- if( d_children[i].getNumMatches()==0 ){\r
+ d_children[i].calculateMatches( qe, f, newConsiderVal[i], newUseConsider[i] );\r
+ if( doProduct && d_children[i].getNumMatches()==0 ){\r
return;\r
}\r
}\r
Trace("inst-gen-cm") << "* Calculate matches " << d_node << std::endl;\r
- //get the model\r
- FirstOrderModel* fm = qe->getModel();\r
if( d_node.getKind()==APPLY_UF ){\r
//if this is an uninterpreted function\r
Node op = d_node.getOperator();\r
//process all values\r
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
- Node n = fm->d_uf_terms[op][i];\r
+ for( size_t i=0; i<considerTerms.size(); i++ ){\r
+ Node n = considerTerms[i];\r
bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );\r
for( int t=(isSelected ? 0 : 1); t<2; t++ ){\r
//do not consider ground case if it is already congruent to another ground term\r
}\r
\r
}else{\r
- InstMatch curr;\r
//if this is an interpreted function\r
- std::vector< Node > terms;\r
- calculateMatchesInterpreted( qe, f, curr, terms, 0 );\r
+ if( doProduct ){\r
+ //combining children matches\r
+ InstMatch curr;\r
+ std::vector< Node > terms;\r
+ calculateMatchesInterpreted( qe, f, curr, terms, 0 );\r
+ }else{\r
+ //summing children matches\r
+ Assert( considerVal.size()==1 );\r
+ for( int i=0; i<(int)d_children.size(); i++ ){\r
+ for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){\r
+ InstMatch m;\r
+ if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){\r
+ addMatchValue( qe, f, considerVal[0], m );\r
+ }\r
+ }\r
+ }\r
+ }\r
}\r
Trace("inst-gen-cm") << "done calculate matches" << std::endl;\r
//can clear information used for finding duplicates\r
val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms );\r
val = Rewriter::rewrite( val );\r
}\r
- Trace("inst-gen-cm") << " - i-match : " << val << std::endl;\r
+ Trace("inst-gen-cm") << " - i-match : " << d_node << std::endl;\r
+ Trace("inst-gen-cm") << " : " << val << std::endl;\r
Trace("inst-gen-cm") << " : " << curr << std::endl;\r
addMatchValue( qe, f, val, curr );\r
}else{\r
InstGenProcess( Node n );\r
virtual ~InstGenProcess(){}\r
\r
- void calculateMatches( QuantifiersEngine* qe, Node f );\r
+ void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider );\r
int getNumMatches() { return d_matches.size(); }\r
bool getMatch( EqualityQuery* q, int i, InstMatch& m );\r
Node getMatchValue( int i ) { return d_match_values[i]; }\r
}
}else{
d_curr_model = fm;
- //build model for relevant symbols contained in quantified formulas
d_addedLemmas = 0;
+ d_didInstGen = false;
//reset the internal information
reset( fm );
//only construct first order model if optUseModel() is true
if( optUseModel() ){
- Trace("model-engine") << "Initializing quantifiers..." << std::endl;
+ Trace("model-engine-debug") << "Initializing quantifiers..." << std::endl;
//check if any quantifiers are un-initialized
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
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 ) ){
}
//if applicable, find exceptions
if( optInstGen() ){
+ d_didInstGen = true;
+ d_instGenMatches = 0;
+ d_numQuantSat = 0;
+ d_numQuantInstGen = 0;
+ d_numQuantNoInstGen = 0;
+ d_numQuantNoSelForm = 0;
//now, see if we know that any exceptions via InstGen exist
Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
- d_addedLemmas += doInstGen( fm, f );
- if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+ int addedLemmas = doInstGen( fm, f );
+ d_addedLemmas += addedLemmas;
+ //temporary
+ if( addedLemmas>0 ){
+ d_numQuantInstGen++;
+ }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ d_numQuantSat++;
+ }else if( hasInstGen( f ) ){
+ d_numQuantNoInstGen++;
+ }else{
+ d_numQuantNoSelForm++;
+ }
+ if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
break;
}
}
}
+ Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
+ Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
+ Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
if( Trace.isOn("model-engine") ){
if( d_addedLemmas>0 ){
Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
}
}
}
- if( d_addedLemmas==0 ){
+ //construct the model if necessary
+ if( d_addedLemmas==0 || optExhInstNonInstGenQuant() ){
//if no immediate exceptions, build the model
// this model will be an approximation that will need to be tested via exhaustive instantiation
Trace("model-engine-debug") << "Building model..." << std::endl;
return options::fmfInstGenOneQuantPerRound();
}
+bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
+ return true;
+}
+
void ModelEngineBuilder::setEffort( int effort ){
d_considerAxioms = effort>=1;
}
if( hasConstantDefinition( s ) ){
d_quant_sat[f] = true;
}
+ }else{
+ Trace("sel-form-null") << "*** No selection formula for " << f << std::endl;
}
//analyze sub quantifiers
if( d_quant_sat.find( f )==d_quant_sat.end() ){
int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
- Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
- if( fp!=f ) Trace("inst-gen") << " ";
- 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;
int addedLemmas = 0;
if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
+ if( fp!=f ) Trace("inst-gen") << " ";
+ 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.
if( !d_quant_selection_formula[f].isNull() ){
//first, try on sub quantifiers
+ bool subQuantSat = true;
for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
addedLemmas += doInstGen( fm, d_sub_quants[f][i] );
+ if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
+ subQuantSat = false;
+ }
}
- if( addedLemmas>0 ){
- Trace("inst-gen") << " -> children added lemmas" << std::endl;
+ if( addedLemmas>0 || !subQuantSat ){
+ Trace("inst-gen") << " -> children added lemmas or non-satisfied" << std::endl;
return addedLemmas;
}else{
Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl;
//get all possible values of selection formula
InstGenProcess igp( d_quant_selection_formula[f] );
- igp.calculateMatches( d_qe, f );
+ std::vector< Node > considered;
+ considered.push_back( fm->d_false );
+ igp.calculateMatches( d_qe, f, considered, true );
+ //igp.calculateMatches( d_qe, f);
Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
for( int i=0; i<igp.getNumMatches(); i++ ){
//if the match is not already true in the model
if( !m.isComplete( f ) ){
//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_child_sub_quant_inst_trie[f].addInstMatch( d_qe, f, m );
//get the partial instantiation pf
Node pf = d_qe->getInstantiation( fp, mp );
Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl;
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
mp.add( d_quant_basis_match[ fp ] );
d_quant_basis_match[ pf ] = InstMatch( &mp );
addedLemmas += initializeQuantifier( pf, fp );
Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl;
+ subQuantSat = false;
}
}else{
if( d_qe->addInstantiation( fp, mp ) ){
}
if( addedLemmas==0 ){
//all sub quantifiers must be satisfied as well
- bool subQuantSat = true;
- for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
- if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){
- subQuantSat = false;
- break;
- }
- }
if( subQuantSat ){
d_quant_sat[ f ] = true;
}
return addedLemmas;
}
+Node mkAndSelectionFormula( std::vector< Node >& children ){
+ std::vector< Node > ch;
+ for( size_t i=0; i<children.size(); i++ ){
+ if( children[i].getKind()==AND ){
+ for( size_t j=0; j<children[i].getNumChildren(); j++ ){
+ ch.push_back( children[i][j] );
+ }
+ }else{
+ ch.push_back( children[i] );
+ }
+ }
+ return NodeManager::currentNM()->mkNode( AND, ch );
+}
+Node mkAndSelectionFormula( Node n1, Node n2 ){
+ std::vector< Node > children;
+ children.push_back( n1 );
+ children.push_back( n2 );
+ return mkAndSelectionFormula( children );
+}
+
//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
// and NULL otherwise
Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
break;
}
if( !nn.isNull() ){
- if( favorPol ){ //temporary
- return nn; //
- } //
+ //if( favorPol ){ //temporary
+ // return nn; //
+ //} //
if( std::find( children.begin(), children.end(), nn )==children.end() ){
children.push_back( nn );
}
ret = min_lit;
}else{
//selection formula must be conjunction of children
- ret = NodeManager::currentNM()->mkNode( AND, children );
+ ret = mkAndSelectionFormula( children );
}
}else{
ret = Node::null();
nn = getSelectionFormula( fn[0], n[0], i==0, useOption );
nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption );
if( !nn.isNull() && !nc[i].isNull() ){
- ret = NodeManager::currentNM()->mkNode( AND, nn, nc[i] );
+ ret = mkAndSelectionFormula( nn, nc[i] );
break;
}
}
if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){
- ret = NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] );
+ ret = mkAndSelectionFormula( nc[0], nc[1] );
}
}else if( n.getKind()==IFF || n.getKind()==XOR ){
bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF;
}
}
if( !nn[0].isNull() && !nn[1].isNull() ){
- ret = NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] );
+ ret = mkAndSelectionFormula( nn[0], nn[1] );
}
}
}else{
}
fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] );
d_uf_model_constructed[op] = true;
+}
+
+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 );
}
\ No newline at end of file
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
//built model uf
std::map< Node, bool > d_uf_model_constructed;
+ //whether inst gen was done
+ bool d_didInstGen;
/** process build model */
virtual void processBuildModel( TheoryModel* m, bool fullModel );
protected:
std::map< Node, bool > d_quant_basis_match_added;
//map from quantifiers to model basis match
std::map< Node, InstMatch > d_quant_basis_match;
+protected: //helper functions
+ /** term has constant definition */
+ bool hasConstantDefinition( Node n );
public:
ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
virtual ~ModelEngineBuilder(){}
bool d_considerAxioms;
// set effort
void setEffort( int effort );
-protected: //helper functions
- /** term has constant definition */
- bool hasConstantDefinition( Node n );
public:
- //options
+ //whether to construct model
virtual bool optUseModel();
+ //whether to add inst-gen lemmas
virtual bool optInstGen();
+ //whether to only consider only quantifier per round of inst-gen
virtual bool optOneQuantPerRoundInstGen();
+ //whether we should exhaustively instantiate quantifiers where inst-gen is not working
+ virtual bool optExhInstNonInstGenQuant();
/** statistics class */
class Statistics {
public:
bool isTermActive( Node n );
// is term selected
virtual bool isTermSelected( Node n ) { return false; }
+ /** exist instantiation ? */
+ virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+ /** quantifier has inst-gen definition */
+ virtual bool hasInstGen( Node f ) = 0;
+ /** did inst gen this round? */
+ bool didInstGen() { return d_didInstGen; }
+
+ //temporary stats
+ int d_numQuantSat;
+ int d_numQuantInstGen;
+ int d_numQuantNoInstGen;
+ int d_numQuantNoSelForm;
+ //temporary stat
+ int d_instGenMatches;
};/* class ModelEngineBuilder */
~ModelEngineBuilderDefault(){}
//options
bool optReconsiderFuncConstants() { return true; }
+ //has inst gen
+ bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
};
class ModelEngineBuilderInstGen : public ModelEngineBuilder
{
private: ///information for (new) InstGen
- //map from quantifiers to their selection literals
+ //map from quantifiers to their selection formulas
std::map< Node, Node > d_quant_selection_formula;
//map of terms that are selected
std::map< Node, bool > d_term_selected;
- //a collection of InstMatch structures produced for each quantifier
+ //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
+ 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;
//instances of each partial instantiation with respect to the root
bool isUsableSelectionLiteral( Node n, int useOption );
//get parent quantifier match
void getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f );
+ //get parent quantifier
+ Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; }
public:
ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
~ModelEngineBuilderInstGen(){}
// is term selected
bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); }
+ /** exist instantiation ? */
+ bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false );
+ //has inst gen
+ bool hasInstGen( Node f ) { return !d_quant_selection_formula[f].isNull(); }
};
}/* CVC4::theory::quantifiers namespace */
Trace("model-engine-debug") << "Build model..." << std::endl;
d_builder->setEffort( effort );
d_builder->buildModel( fm, false );
+ addedLemmas += (int)d_builder->d_addedLemmas;
//if builder has lemmas, add and return
- if( d_builder->d_addedLemmas>0 ){
- addedLemmas += (int)d_builder->d_addedLemmas;
- }else{
+ if( addedLemmas==0 ){
Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
//let the strong solver verify that the model is minimal
uf::StrongSolverTheoryUf* uf_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
//for debugging, this will if there are terms in the model that the strong solver was not notified of
uf_ss->debugModel( fm );
Trace("model-engine-debug") << "Check model..." << std::endl;
+ d_incomplete_check = false;
//print debug
Debug("fmf-model-complete") << std::endl;
debugPrint("fmf-model-complete");
//successfully built an acceptable model, now check it
- checkModel( addedLemmas );
- //print debug information
- if( Trace.isOn("model-engine") ){
- Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
- Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
- Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
- }
+ addedLemmas += checkModel( check_model_full );
+ }else if( d_builder->didInstGen() && d_builder->optExhInstNonInstGenQuant() ){
+ Trace("model-engine-debug") << "Check model for non-inst gen quantifiers..." << std::endl;
+ //check quantifiers that inst-gen didn't apply to
+ addedLemmas += checkModel( check_model_no_inst_gen );
+ }
+ if( Trace.isOn("model-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
}
}
if( addedLemmas==0 ){
Trace("fmf-consistent") << std::endl;
debugPrint("fmf-consistent");
if( options::produceModels() ){
- // finish building the model in the standard way
+ // finish building the model
d_builder->buildModel( fm, true );
}
//if the check was incomplete, we must set incomplete flag
#endif
}
-void ModelEngine::checkModel( int& addedLemmas ){
+int ModelEngine::checkModel( int checkOption ){
+ int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
//for debugging
if( Trace.isOn("model-engine") ){
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
if( it->first.isSort() ){
Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Trace("model-engine-debug") << " ";
}
}
}
- //verify we are SAT by trying exhaustive instantiation
- d_incomplete_check = false;
+ //compute the relevant domain if necessary
if( optUseRelevantDomain() ){
d_rel_domain.compute();
}
d_testLemmas = 0;
d_relevantLemmas = 0;
d_totalLemmas = 0;
- Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl;
+ Debug("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
- addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
- if( Trace.isOn("model-engine-warn") ){
- if( addedLemmas>10000 ){
- Debug("fmf-exit") << std::endl;
- debugPrint("fmf-exit");
- exit( 0 );
+ //keep track of total instantiations for statistics
+ int totalInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ TypeNode tn = f[0][i].getType();
+ if( fm->d_rep_set.hasType( tn ) ){
+ totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
}
}
- if( optOneQuantPerRound() && addedLemmas>0 ){
- break;
+ d_totalLemmas += totalInst;
+ //determine if we should check this quantifiers
+ bool checkQuant = false;
+ if( checkOption==check_model_full ){
+ checkQuant = d_builder->isQuantifierActive( f );
+ }else if( checkOption==check_model_no_inst_gen ){
+ checkQuant = !d_builder->hasInstGen( f );
+ }
+ //if we need to consider this quantifier on this iteration
+ if( checkQuant ){
+ addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
+ if( Trace.isOn("model-engine-warn") ){
+ if( addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
+ }
+ }
+ if( optOneQuantPerRound() && addedLemmas>0 ){
+ break;
+ }
}
}
- Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
- Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+ //print debug information
+ if( Trace.isOn("model-engine") ){
+ Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
+ Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+ Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+ }
+ return addedLemmas;
}
int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
int addedLemmas = 0;
- //keep track of total instantiations for statistics
- int totalInst = 1;
+ Debug("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl;
+ Debug("inst-fmf-ei") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- TypeNode tn = f[0][i].getType();
- if( d_quantEngine->getModel()->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ tn ].size();
- }
+ Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
}
- d_totalLemmas += totalInst;
- //if we need to consider this quantifier on this iteration
- if( d_builder->isQuantifierActive( f ) ){
- //debug printing
- Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
- if( useRelInstDomain ){
- Trace("rel-dom") << "Relevant domain : " << std::endl;
- for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
- Trace("rel-dom") << " " << i << " : ";
- for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
- Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
- }
- Trace("rel-dom") << std::endl;
- }
- }
- Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl;
- Debug("inst-fmf-ei") << " Instantiation Constants: ";
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
- }
- Debug("inst-fmf-ei") << std::endl;
+ Debug("inst-fmf-ei") << std::endl;
- //create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- riter.setQuantifier( f );
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = d_incomplete_check || riter.d_incomplete;
- //set the domain for the iterator (the sufficient set of instantiations to try)
- if( useRelInstDomain ){
- riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
- }
- d_quantEngine->getModel()->resetEvaluate();
- int tests = 0;
- int triedLemmas = 0;
- while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
- d_testLemmas++;
- int eval = 0;
- int depIndex;
- if( d_builder->optUseModel() ){
- //see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
- tests++;
- //if evaluate(...)==1, then the instantiation is already true in the model
- // depIndex is the index of the least significant variable that this evaluation relies upon
- depIndex = riter.getNumTerms()-1;
- eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
- if( eval==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- }else{
- Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
- }
- }
+ //create a rep set iterator and iterate over the (relevant) domain of the quantifier
+ RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+ riter.setQuantifier( f );
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ d_incomplete_check = d_incomplete_check || riter.d_incomplete;
+ //set the domain for the iterator (the sufficient set of instantiations to try)
+ if( useRelInstDomain ){
+ riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+ }
+ d_quantEngine->getModel()->resetEvaluate();
+ int tests = 0;
+ int triedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ d_testLemmas++;
+ int eval = 0;
+ int depIndex;
+ if( d_builder->optUseModel() ){
+ //see if instantiation is already true in current model
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ tests++;
+ //if evaluate(...)==1, then the instantiation is already true in the model
+ // depIndex is the index of the least significant variable that this evaluation relies upon
+ depIndex = riter.getNumTerms()-1;
+ eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
if( eval==1 ){
- //instantiation is already true -> skip
- riter.increment2( depIndex );
+ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
}else{
- //instantiation was not shown to be true, construct the match
- InstMatch m;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
- }
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- d_triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 && optExhInstEvalSkipMultiple() ){
- riter.increment2( depIndex );
- }else{
- riter.increment();
- }
+ Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+ }
+ }
+ if( eval==1 ){
+ //instantiation is already true -> skip
+ riter.increment2( depIndex );
+ }else{
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ d_triedLemmas++;
+ //add as instantiation
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 && optExhInstEvalSkipMultiple() ){
+ riter.increment2( depIndex );
}else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
riter.increment();
}
+ }else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+ riter.increment();
}
}
- //print debugging information
- d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
- d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
- d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
- d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
- int relevantInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- relevantInst = relevantInst * (int)riter.d_domain[i].size();
- }
- d_relevantLemmas += relevantInst;
- Debug("inst-fmf-ei") << "Finished: " << std::endl;
- Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
- Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
- Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
- Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl;
- if( addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
- Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
- Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
+ }
+ //print debugging information
+ d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
+ d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
+ d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
+ d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+ int relevantInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ relevantInst = relevantInst * (int)riter.d_domain[i].size();
+ }
+ d_relevantLemmas += relevantInst;
+ Debug("inst-fmf-ei") << "Finished: " << std::endl;
+ //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
+ Debug("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
+ Debug("inst-fmf-ei") << " # Tests: " << tests << std::endl;
+ if( addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
+ Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
+ Trace("model-engine-warn") << std::endl;
}
return addedLemmas;
}
bool optOneQuantPerRound();
bool optExhInstEvalSkipMultiple();
private:
+ enum{
+ check_model_full,
+ check_model_no_inst_gen,
+ };
//check model
- void checkModel( int& addedLemmas );
+ int checkModel( int checkOption );
//exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
private:
}
Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){
- //Notice() << "Compute var elimination for " << f << std::endl;
+ Trace("var-elim-quant") << "Compute var elimination for " << body << std::endl;
QuantPhaseReq qpr( body );
std::vector< Node > vars;
std::vector< Node > subs;
}
}
if( !vars.empty() ){
- //Notice() << "VE " << vars.size() << "/" << n[0].getNumChildren() << std::endl;
+ Trace("var-elim-quant") << "VE " << vars.size() << "/" << args.size() << std::endl;
//remake with eliminated nodes
body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
body = Rewriter::rewrite( body );
if( !ipl.isNull() ){
ipl = ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
}
+ Trace("var-elim-quant") << "Return " << body << std::endl;
}
return body;
}
//general method for computing various rewrites
Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
- std::vector< Node > args;
- for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
- args.push_back( f[0][i] );
- }
- NodeBuilder<> defs(kind::AND);
- Node n = f[1];
- Node ipl;
- if( f.getNumChildren()==3 ){
- ipl = f[2];
- }
- if( computeOption==COMPUTE_NNF ){
- n = computeNNF( n );
- }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
- n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
- }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
- Node prev;
- do{
- prev = n;
- n = computeVarElimination( n, args, ipl );
- }while( prev!=n && !args.empty() );
- }else if( computeOption==COMPUTE_CNF ){
- //n = computeNNF( n );
- n = computeCNF( n, args, defs, false );
- ipl = Node::null();
- }
- if( f[1]==n && args.size()==f[0].getNumChildren() ){
- return f;
- }else{
- if( args.empty() ){
- defs << n;
+ if( f.getKind()==FORALL ){
+ Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+ std::vector< Node > args;
+ for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+ args.push_back( f[0][i] );
+ }
+ NodeBuilder<> defs(kind::AND);
+ Node n = f[1];
+ Node ipl;
+ if( f.getNumChildren()==3 ){
+ ipl = f[2];
+ }
+ if( computeOption==COMPUTE_NNF ){
+ n = computeNNF( n );
+ }else if( computeOption==COMPUTE_PRENEX || computeOption==COMPUTE_PRE_SKOLEM ){
+ n = computePrenex( n, args, true, computeOption==COMPUTE_PRENEX );
+ }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+ Node prev;
+ do{
+ prev = n;
+ n = computeVarElimination( n, args, ipl );
+ }while( prev!=n && !args.empty() );
+ }else if( computeOption==COMPUTE_CNF ){
+ //n = computeNNF( n );
+ n = computeCNF( n, args, defs, false );
+ ipl = Node::null();
+ }
+ Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
+ if( f[1]==n && args.size()==f[0].getNumChildren() ){
+ return f;
}else{
- std::vector< Node > children;
- children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
- children.push_back( n );
- if( !ipl.isNull() ){
- children.push_back( ipl );
+ if( args.empty() ){
+ defs << n;
+ }else{
+ std::vector< Node > children;
+ children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+ children.push_back( n );
+ if( !ipl.isNull() ){
+ children.push_back( ipl );
+ }
+ defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
}
- defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
+ return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
}
- return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
+ }else{
+ return f;
}
}
}
}while( !success );
Trace("rel-dom") << "done compute relevant domain" << std::endl;
+ /*
+ //debug printing
+ Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl;
+ if( useRelInstDomain ){
+ Trace("rel-dom") << "Relevant domain : " << std::endl;
+ for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){
+ Trace("rel-dom") << " " << i << " : ";
+ for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){
+ Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " ";
+ }
+ Trace("rel-dom") << std::endl;
+ }
+ }
+ */
}
bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){
}
bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
- return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst );
+ if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){
+ if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){
+ return true;
+ }
+ }
+ //also check model engine (it may contain instantiations internally)
+ if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
+ return true;
+ }
+ return false;
}
bool QuantifiersEngine::addLemma( Node lem ){
** \brief Implementation of Theory UF Model
**/
-#include "theory/quantifiers/model_engine.h"
#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf_model.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
-#include "theory/uf/theory_uf_strong_solver.h"
-#include "theory/uf/theory_uf_instantiator.h"
-#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#define RECONSIDER_FUNC_DEFAULT_VALUE
}
void StrongSolverTheoryUf::SortRepModel::debugModel( TheoryModel* m ){
- std::vector< Node > eqcs;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- Node eqc = (*eqcs_i);
- if( eqc.getType()==d_type ){
- if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
- eqcs.push_back( eqc );
- //we must ensure that this equivalence class has been accounted for
- if( d_regions_map.find( eqc )==d_regions_map.end() ){
- Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
- Trace("uf-ss-warn") << " type : " << d_type << std::endl;
- Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
+ if( Trace.isOn("uf-ss-warn") ){
+ std::vector< Node > eqcs;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ Node eqc = (*eqcs_i);
+ if( eqc.getType()==d_type ){
+ if( std::find( eqcs.begin(), eqcs.end(), eqc )==eqcs.end() ){
+ eqcs.push_back( eqc );
+ //we must ensure that this equivalence class has been accounted for
+ if( d_regions_map.find( eqc )==d_regions_map.end() ){
+ Trace("uf-ss-warn") << "WARNING : equivalence class " << eqc << " unaccounted for." << std::endl;
+ Trace("uf-ss-warn") << " type : " << d_type << std::endl;
+ Trace("uf-ss-warn") << " kind : " << eqc.getKind() << std::endl;
+ }
}
}
+ ++eqcs_i;
+ }
+ if( (int)eqcs.size()!=d_cardinality ){
+ Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
+ Trace("uf-ss-warn") << " cardinality : " << d_cardinality << std::endl;
+ Trace("uf-ss-warn") << " # reps : " << (int)eqcs.size() << std::endl;
}
- ++eqcs_i;
- }
- if( (int)eqcs.size()!=d_cardinality ){
- Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl;
- Trace("uf-ss-warn") << " cardinality : " << d_cardinality << std::endl;
- Trace("uf-ss-warn") << " # reps : " << (int)eqcs.size() << std::endl;
}
}
projects / cvc5.git / commitdiff