From: Andrew Reynolds Date: Wed, 3 Oct 2012 23:04:08 +0000 (+0000) Subject: minor fix for mbqi in finite model finding X-Git-Tag: cvc5-1.0.0~7742 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c4debb1893109a4d4a2feacd910d3778aeca8f4;p=cvc5.git minor fix for mbqi in finite model finding --- diff --git a/src/theory/model.cpp b/src/theory/model.cpp index bd9e6aefa..4a3ddc9ca 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -604,6 +604,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps) { + Trace("tembn") << "Normalize " << r << std::endl; std::map::iterator itMap = constantReps.find(r); if (itMap != constantReps.end()) { return (*itMap).second; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e0723f432..33dcdd533 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -252,124 +252,118 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ //Message() << "Eval term " << n << std::endl; - if( !n.hasAttribute(InstConstantAttribute()) ){ - //if evaluating a ground term, just consult the standard getValue functionality - depIndex = -1; - return getValue( n ); - }else{ - Node val; - depIndex = ri->getNumTerms()-1; - //check the type of n - if( n.getKind()==INST_CONSTANT ){ - int v = n.getAttribute(InstVarNumAttribute()); - depIndex = ri->d_var_order[ v ]; - val = ri->getTerm( v ); - }else if( n.getKind()==ITE ){ - int depIndex1, depIndex2; - int eval = evaluate( n[0], depIndex1, ri ); - if( eval==0 ){ - //evaluate children to see if they are the same - Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri ); - Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri ); - if( val1==val2 ){ - val = val1; - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - }else{ - return Node::null(); - } - }else{ - val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri ); + Node val; + depIndex = ri->getNumTerms()-1; + //check the type of n + if( n.getKind()==INST_CONSTANT ){ + int v = n.getAttribute(InstVarNumAttribute()); + depIndex = ri->d_var_order[ v ]; + val = ri->getTerm( v ); + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eval = evaluate( n[0], depIndex1, ri ); + if( eval==0 ){ + //evaluate children to see if they are the same + Node val1 = evaluateTerm( n[ 1 ], depIndex1, ri ); + Node val2 = evaluateTerm( n[ 2 ], depIndex2, ri ); + if( val1==val2 ){ + val = val1; depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + }else{ + return Node::null(); } }else{ - std::vector< int > children_depIndex; - //for select, pre-process read over writes - if( n.getKind()==SELECT ){ + val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2, ri ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + } + }else{ + std::vector< int > children_depIndex; + //for select, pre-process read over writes + if( n.getKind()==SELECT ){ #if 0 - //std::cout << "Evaluate " << n << std::endl; - Node sel = evaluateTerm( n[1], depIndex, ri ); - if( sel.isNull() ){ - depIndex = ri->getNumTerms()-1; - return Node::null(); - } - Node arr = getRepresentative( n[0] ); - //if( n[0]!=getRepresentative( n[0] ) ){ - // std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl; - //} - int tempIndex; - int eval = 1; - while( arr.getKind()==STORE && eval!=0 ){ - eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri ); + //std::cout << "Evaluate " << n << std::endl; + Node sel = evaluateTerm( n[1], depIndex, ri ); + if( sel.isNull() ){ + depIndex = ri->getNumTerms()-1; + return Node::null(); + } + Node arr = getRepresentative( n[0] ); + //if( n[0]!=getRepresentative( n[0] ) ){ + // std::cout << n[0] << " is " << getRepresentative( n[0] ) << std::endl; + //} + int tempIndex; + int eval = 1; + while( arr.getKind()==STORE && eval!=0 ){ + eval = evaluate( sel.eqNode( arr[1] ), tempIndex, ri ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + if( eval==1 ){ + val = evaluateTerm( arr[2], tempIndex, ri ); depIndex = tempIndex > depIndex ? tempIndex : depIndex; - if( eval==1 ){ - val = evaluateTerm( arr[2], tempIndex, ri ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - return val; - }else if( eval==-1 ){ - arr = arr[0]; - } + return val; + }else if( eval==-1 ){ + arr = arr[0]; } - arr = evaluateTerm( arr, tempIndex, ri ); - depIndex = tempIndex > depIndex ? tempIndex : depIndex; - val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); + } + arr = evaluateTerm( arr, tempIndex, ri ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); #else - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); + val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); #endif - }else{ - //default term evaluate : evaluate all children, recreate the value - val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); - } - if( !val.isNull() ){ - bool setVal = false; - //custom ways of evaluating terms - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); + }else{ + //default term evaluate : evaluate all children, recreate the value + val = evaluateTermDefault( n, depIndex, children_depIndex, ri ); + } + if( !val.isNull() ){ + bool setVal = false; + //custom ways of evaluating terms + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; + //if it is a defined UF, then consult the interpretation + if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ + ++d_eval_uf_terms; + int argDepIndex = 0; + //make the term model specifically for n + makeEvalUfModel( n ); + //now, consult the model + if( d_eval_uf_use_default[n] ){ + val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); + }else{ + val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex ); + } //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //if it is a defined UF, then consult the interpretation - if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){ - ++d_eval_uf_terms; - int argDepIndex = 0; - //make the term model specifically for n - makeEvalUfModel( n ); - //now, consult the model - if( d_eval_uf_use_default[n] ){ - val = d_uf_model_tree[ op ].getValue( this, val, argDepIndex ); - }else{ - val = d_eval_uf_model[ n ].getValue( this, val, argDepIndex ); - } - //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); - Assert( !val.isNull() ); - //recalculate the depIndex - depIndex = -1; - for( int i=0; idepIndex ){ - depIndex = children_depIndex[index]; - } + //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe ); + Assert( !val.isNull() ); + //recalculate the depIndex + depIndex = -1; + for( int i=0; idepIndex ){ + depIndex = children_depIndex[index]; } - setVal = true; } - }else if( n.getKind()==SELECT ){ - //we are free to interpret this term however we want + setVal = true; } - //if not set already, rewrite and consult model for interpretation - if( !setVal ){ - val = Rewriter::rewrite( val ); - if( val.getMetaKind()!=kind::metakind::CONSTANT ){ - //FIXME: we cannot do this until we trust all theories collectModelInfo! - //val = getInterpretedValue( val ); - //val = getRepresentative( val ); - } + }else if( n.getKind()==SELECT ){ + //we are free to interpret this term however we want + } + //if not set already, rewrite and consult model for interpretation + if( !setVal ){ + val = Rewriter::rewrite( val ); + if( val.getMetaKind()!=kind::metakind::CONSTANT ){ + //FIXME: we cannot do this until we trust all theories collectModelInfo! + //val = getInterpretedValue( val ); + //val = getRepresentative( val ); } - Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; - printRepresentativeDebug( "fmf-eval-debug", val ); - Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; } + Debug("fmf-eval-debug") << "Evaluate term " << n << " = "; + printRepresentativeDebug( "fmf-eval-debug", val ); + Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl; } - return val; } + return val; } Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 8eac4da95..805d27008 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -302,32 +302,6 @@ int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ //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_lit[f].isNull() ){ -#if 0 - bool phase = d_quant_selection_lit[f].getKind()!=NOT; - Node lit = d_quant_selection_lit[f].getKind()==NOT ? d_quant_selection_lit[f][0] : d_quant_selection_lit[f]; - Assert( lit.hasAttribute(InstConstantAttribute()) ); - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node n2 = fm->d_uf_terms[op][i]; - if( n1!=n2 ){ - //match n1 and n2 - } - } - } - } -#else Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; for( size_t i=0; iaddInstantiations( d_quant_basis_match[f] ); } } -#endif } return addedLemmas; } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index b5a9ee74c..d9d6b8b0b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -26,8 +26,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" -//#define ME_PRINT_WARNINGS - #define EVAL_FAIL_SKIP_MULTIPLE using namespace std; @@ -157,6 +155,14 @@ bool ModelEngine::optOneQuantPerRound(){ return options::fmfOneQuantPerRound(); } +bool ModelEngine::optExhInstEvalSkipMultiple(){ +#ifdef EVAL_FAIL_SKIP_MULTIPLE + return true; +#else + return false; +#endif +} + int ModelEngine::initializeQuantifier( Node f ){ if( d_quant_init.find( f )==d_quant_init.end() ){ d_quant_init[f] = true; @@ -233,13 +239,13 @@ void ModelEngine::checkModel( int& addedLemmas ){ for( int i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); -#ifdef ME_PRINT_WARNINGS - if( addedLemmas>10000 ){ - Debug("fmf-exit") << std::endl; - debugPrint("fmf-exit"); - exit( 0 ); + if( Trace.isOn("model-engine-warn") ){ + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); + } } -#endif if( optOneQuantPerRound() && addedLemmas>0 ){ break; } @@ -261,6 +267,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ 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; @@ -272,14 +279,14 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ Trace("rel-dom") << std::endl; } } - int tests = 0; - int triedLemmas = 0; Debug("inst-fmf-ei") << "Add matches for " << f << "..." << std::endl; Debug("inst-fmf-ei") << " Instantiation Constants: "; for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ) << " "; } 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 @@ -289,6 +296,8 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool 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; @@ -324,21 +333,19 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ //add as instantiation if( d_quantEngine->addInstantiation( f, m ) ){ addedLemmas++; -#ifdef EVAL_FAIL_SKIP_MULTIPLE - if( eval==-1 ){ + //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(); } -#else - riter.increment(); -#endif }else{ - Debug("ajr-temp") << "* Failed Add instantiation " << m << std::endl; + 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; @@ -354,17 +361,15 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ 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; -#ifdef ME_PRINT_WARNINGS if( addedLemmas>1000 ){ - Notice() << "WARNING: many instantiations produced for " << f << ": " << std::endl; - Notice() << " Inst Total: " << totalInst << std::endl; - Notice() << " Inst Relevant: " << totalRelevant << std::endl; - Notice() << " Inst Tried: " << triedLemmas << std::endl; - Notice() << " Inst Added: " << addedLemmas << std::endl; - Notice() << " # Tests: " << tests << std::endl; - Notice() << std::endl; + 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; } -#endif } return addedLemmas; } diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index a292eb5f8..7a5954e5c 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -47,6 +47,7 @@ private: bool optOneInstPerQuantRound(); bool optUseRelevantDomain(); bool optOneQuantPerRound(); + bool optExhInstEvalSkipMultiple(); private: //initialize quantifiers, return number of lemmas produced int initializeQuantifier( Node f );