From: Andrew Reynolds Date: Mon, 29 Oct 2012 21:49:41 +0000 (+0000) Subject: more updates and minor bug fixes for fmf/inst-gen quantifier instantiation X-Git-Tag: cvc5-1.0.0~7655 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a8a3449b130b0154ae55ad223f362c6d662d6ce;p=cvc5.git more updates and minor bug fixes for fmf/inst-gen quantifier instantiation --- diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index b4aed6021..428a224ee 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -49,27 +49,90 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); + qe->getModelEngine()->getModelBuilder()->d_instGenMatches++; } } } -void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ +void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ){ + //whether we are doing a product or sum or matches + bool doProduct = true; + //get the model + FirstOrderModel* fm = qe->getModel(); + + //calculate terms we will consider + std::vector< Node > considerTerms; + std::vector< std::vector< Node > > newConsiderVal; + std::vector< bool > newUseConsider; + newConsiderVal.resize( d_children.size() ); + newUseConsider.resize( d_children.size(), false ); + if( d_node.getKind()==APPLY_UF ){ + Node op = d_node.getOperator(); + if( useConsider ){ + for( size_t i=0; igetEqualityQuery()->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; + } + } + }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; + } + }else if( d_node.getKind()==AND || d_node.getKind()==OR ){ + for( size_t i=0; igetModel(); if( d_node.getKind()==APPLY_UF ){ //if this is an uninterpreted function Node op = d_node.getOperator(); //process all values - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; igetModelEngine()->getModelBuilder()->isTermSelected( n ); for( int t=(isSelected ? 0 : 1); t<2; t++ ){ //do not consider ground case if it is already congruent to another ground term @@ -105,10 +168,24 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ } }else{ - InstMatch curr; //if this is an interpreted function - std::vector< Node > terms; - calculateMatchesInterpreted( qe, f, curr, terms, 0 ); + if( doProduct ){ + //combining children matches + InstMatch curr; + std::vector< Node > terms; + calculateMatchesInterpreted( qe, f, curr, terms, 0 ); + }else{ + //summing children matches + Assert( considerVal.size()==1 ); + for( int i=0; i<(int)d_children.size(); i++ ){ + for( int j=0; j<(int)d_children[ i ].getNumMatches(); j++ ){ + InstMatch m; + if( d_children[ i ].getMatch( qe->getEqualityQuery(), j, m ) ){ + addMatchValue( qe, f, considerVal[0], m ); + } + } + } + } } Trace("inst-gen-cm") << "done calculate matches" << std::endl; //can clear information used for finding duplicates @@ -158,7 +235,8 @@ void InstGenProcess::calculateMatchesInterpreted( QuantifiersEngine* qe, Node f, val = NodeManager::currentNM()->mkNode( d_node.getKind(), terms ); val = Rewriter::rewrite( val ); } - Trace("inst-gen-cm") << " - i-match : " << val << std::endl; + Trace("inst-gen-cm") << " - i-match : " << d_node << std::endl; + Trace("inst-gen-cm") << " : " << val << std::endl; Trace("inst-gen-cm") << " : " << curr << std::endl; addMatchValue( qe, f, val, curr ); }else{ diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index 3386001af..f6e6a372e 100755 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -48,7 +48,7 @@ public: InstGenProcess( Node n ); virtual ~InstGenProcess(){} - void calculateMatches( QuantifiersEngine* qe, Node f ); + void calculateMatches( QuantifiersEngine* qe, Node f, std::vector< Node >& considerVal, bool useConsider ); int getNumMatches() { return d_matches.size(); } bool getMatch( EqualityQuery* q, int i, InstMatch& m ); Node getMatchValue( int i ) { return d_match_values[i]; } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 598b50957..f2e195d2e 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -101,13 +101,13 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } }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; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); @@ -127,6 +127,7 @@ 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; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); if( isQuantifierActive( f ) ){ @@ -135,17 +136,37 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } //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; igetNumAssertedQuantifiers(); 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; @@ -154,7 +175,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } } - 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; @@ -288,6 +310,10 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ return options::fmfInstGenOneQuantPerRound(); } +bool ModelEngineBuilder::optExhInstNonInstGenQuant(){ + return true; +} + void ModelEngineBuilder::setEffort( int effort ){ d_considerAxioms = effort>=1; } @@ -610,6 +636,8 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) 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() ){ @@ -621,29 +649,36 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) 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; i0 ){ - 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; igetInstantiation( fp, mp ); Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; @@ -669,10 +706,12 @@ 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 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 ) ){ @@ -684,13 +723,6 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ } if( addedLemmas==0 ){ //all sub quantifiers must be satisfied as well - bool subQuantSat = true; - for( size_t i=0; i& children ){ + std::vector< Node > ch; + for( size_t i=0; imkNode( 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 ){ @@ -728,9 +780,9 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar 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 ); } @@ -758,7 +810,7 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar ret = min_lit; }else{ //selection formula must be conjunction of children - ret = NodeManager::currentNM()->mkNode( AND, children ); + ret = mkAndSelectionFormula( children ); } }else{ ret = Node::null(); @@ -771,12 +823,12 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar 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; @@ -790,7 +842,7 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar } } if( !nn[0].isNull() && !nn[1].isNull() ){ - ret = NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] ); + ret = mkAndSelectionFormula( nn[0], nn[1] ); } } }else{ @@ -921,4 +973,8 @@ void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ) } 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 diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 7c720d604..d0348dff8 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -64,6 +64,8 @@ protected: 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: @@ -86,6 +88,9 @@ 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(){} @@ -95,14 +100,15 @@ public: 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: @@ -120,6 +126,20 @@ 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 */ @@ -149,17 +169,21 @@ public: ~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 @@ -188,11 +212,17 @@ private: 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 */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 7952d3c21..40a61f7c5 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -71,29 +71,29 @@ void ModelEngine::check( Theory::Effort e ){ 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 ){ @@ -113,7 +113,7 @@ void ModelEngine::check( Theory::Effort e ){ 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 @@ -155,11 +155,13 @@ bool ModelEngine::optExhInstEvalSkipMultiple(){ #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") << " "; @@ -170,8 +172,7 @@ void ModelEngine::checkModel( int& addedLemmas ){ } } } - //verify we are SAT by trying exhaustive instantiation - d_incomplete_check = false; + //compute the relevant domain if necessary if( optUseRelevantDomain() ){ d_rel_domain.compute(); } @@ -179,141 +180,141 @@ void ModelEngine::checkModel( int& addedLemmas ){ 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; igetNumAssertedQuantifiers(); 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; id_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; igetModel()->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; igetTermDatabase()->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; igetTermDatabase()->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; igetTermDatabase()->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; i1000 ){ - 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; i1000 ){ + 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; } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 377fe9aa9..2560cf50e 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -44,8 +44,12 @@ private: 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: diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 7bf1f30e9..063875235 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -280,7 +280,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ } 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; @@ -309,13 +309,14 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& } } 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; } @@ -524,46 +525,52 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b //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; } } diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 7b4440c31..ad6c241e7 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -83,6 +83,20 @@ void RelevantDomain::compute(){ } }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; igetModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){ + return true; + } + return false; } bool QuantifiersEngine::addLemma( Node lem ){ diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 02e2412a4..efe3aebf4 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -12,13 +12,10 @@ ** \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 diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index ed8ccef4a..d037c374d 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1173,27 +1173,29 @@ void StrongSolverTheoryUf::SortRepModel::debugPrint( const char* c ){ } 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; } }