diff options
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 1667 |
1 files changed, 474 insertions, 1193 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index a72b103d1..ad259f864 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -15,19 +15,23 @@ **/ #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/rep_set_iterator.h" #include "theory/theory_engine.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 ME_PRINT_PROCESS_TIMES +//#define ME_PRINT_WARNINGS //#define DISABLE_EVAL_SKIP_MULTIPLE -#define RECONSIDER_FUNC_DEFAULT_VALUE + #define RECONSIDER_FUNC_CONSTANT -#define USE_INDEX_ORDERING -//#define ONE_INST_PER_QUANT_PER_ROUND +#define EVAL_FAIL_SKIP_MULTIPLE +//#define ONE_QUANT_PER_ROUND_INST_GEN +//#define ONE_QUANT_PER_ROUND using namespace std; using namespace CVC4; @@ -36,570 +40,417 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -void printRepresentative( const char* c, QuantifiersEngine* qe, Node r ){ - if( r.getType()==NodeManager::currentNM()->booleanType() ){ - if( qe->getEqualityQuery()->areEqual( r, NodeManager::currentNM()->mkConst( true ) ) ){ - Debug( c ) << "true"; - }else{ - Debug( c ) << "false"; - } - }else{ - Debug( c ) << qe->getEqualityQuery()->getRepresentative( r ); - } -} - -RepAlphabet::RepAlphabet( RepAlphabet& ra, QuantifiersEngine* qe ){ - //translate to current representatives - for( std::map< TypeNode, std::vector< Node > >::iterator it = ra.d_type_reps.begin(); it != ra.d_type_reps.end(); ++it ){ - std::vector< Node > reps; - for( int i=0; i<(int)it->second.size(); i++ ){ - //reps.push_back( ie->getEqualityQuery()->getRepresentative( it->second[i] ) ); - reps.push_back( it->second[i] ); - } - set( it->first, reps ); - } -} - -void RepAlphabet::set( TypeNode t, std::vector< Node >& reps ){ - d_type_reps[t].insert( d_type_reps[t].begin(), reps.begin(), reps.end() ); - for( int i=0; i<(int)reps.size(); i++ ){ - d_tmap[ reps[i] ] = i; - } -} - -void RepAlphabet::debugPrint( const char* c, QuantifiersEngine* qe ){ - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ - Debug( c ) << it->first << " : " << std::endl; - for( int i=0; i<(int)it->second.size(); i++ ){ - Debug( c ) << " " << i << ": " << it->second[i] << std::endl; - Debug( c ) << " eq_class( " << it->second[i] << " ) : "; - ((uf::InstantiatorTheoryUf*)qe->getInstantiator( THEORY_UF ))->outputEqClass( c, it->second[i] ); - Debug( c ) << std::endl; - } - } -} - -RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model ){ - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - d_index_order.push_back( i ); - } - initialize( qe, f, model ); -} - -RepAlphabetIterator::RepAlphabetIterator( QuantifiersEngine* qe, Node f, ModelEngine* model, std::vector< int >& indexOrder ){ - d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); - initialize( qe, f, model ); -} - -void RepAlphabetIterator::initialize( QuantifiersEngine* qe, Node f, ModelEngine* model ){ - d_f = f; - d_model = model; - //store instantiation constants - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - d_ic.push_back( qe->getInstantiationConstant( d_f, i ) ); - d_index.push_back( 0 ); - } - //make the d_var_order mapping - for( size_t i=0; i<d_index_order.size(); i++ ){ - d_var_order[d_index_order[i]] = i; - } - //for testing - d_inst_tried = 0; - d_inst_tests = 0; -} - -void RepAlphabetIterator::increment2( QuantifiersEngine* qe, int counter ){ - Assert( !isFinished() ); - //increment d_index - while( counter>=0 && d_index[counter]==(int)(d_model->getReps()->d_type_reps[d_f[0][d_index_order[counter]].getType()].size()-1) ){ - counter--; - } - if( counter==-1 ){ - d_index.clear(); - }else{ - for( int i=(int)d_index.size()-1; i>counter; i-- ){ - d_index[i] = 0; - d_model->clearEvalFailed( i ); - } - d_index[counter]++; - d_model->clearEvalFailed( counter ); - } -} - -void RepAlphabetIterator::increment( QuantifiersEngine* qe ){ - if( !isFinished() ){ - increment2( qe, (int)d_index.size()-1 ); - } -} +ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) : +TheoryEngineModelBuilder( qe->getTheoryEngine() ), +d_qe( qe ){ -bool RepAlphabetIterator::isFinished(){ - return d_index.empty(); } -void RepAlphabetIterator::getMatch( QuantifiersEngine* ie, InstMatch& m ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - m.d_map[ ie->getInstantiationConstant( d_f, i ) ] = getTerm( i ); - } +Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){ + return eqc; } -Node RepAlphabetIterator::getTerm( int i ){ - TypeNode tn = d_f[0][d_index_order[i]].getType(); - Assert( d_model->getReps()->d_type_reps.find( tn )!=d_model->getReps()->d_type_reps.end() ); - return d_model->getReps()->d_type_reps[tn][d_index[d_index_order[i]]]; -} - -void RepAlphabetIterator::calculateTerms( QuantifiersEngine* qe ){ - d_terms.clear(); - for( int i=0; i<qe->getNumInstantiationConstants( d_f ); i++ ){ - d_terms.push_back( getTerm( i ) ); - } -} - -void RepAlphabetIterator::debugPrint( const char* c ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << i << ": " << d_index[i] << ", (" << getTerm( i ) << " / " << d_ic[ i ] << std::endl; - } -} - -void RepAlphabetIterator::debugPrintSmall( const char* c ){ - Debug( c ) << "RI: "; - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << d_index[i] << ": " << getTerm( i ) << " "; - } - Debug( c ) << std::endl; -} - -//set value function -void UfModelTree::setValue( QuantifiersEngine* qe, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){ - if( d_data.empty() ){ - d_value = v; - }else if( !d_value.isNull() && d_value!=v ){ - d_value = Node::null(); - } - if( argIndex<(int)n.getNumChildren() ){ - //take r = null when argument is the model basis - Node r; - if( ground || !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ){ - r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] ); - } - d_data[ r ].setValue( qe, n, v, indexOrder, ground, argIndex+1 ); - } -} - -//get value function -Node UfModelTree::getValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){ - if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){ - //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl; - depIndex = argIndex; - return d_value; - }else{ - Node val; - int childDepIndex[2] = { argIndex, argIndex }; - for( int i=0; i<2; i++ ){ - //first check the argument, then check default - Node r; - if( i==0 ){ - r = qe->getEqualityQuery()->getRepresentative( n[ indexOrder[argIndex] ] ); +void ModelEngineBuilder::processBuildModel( TheoryModel* m ) { + d_addedLemmas = 0; + //only construct first order model if optUseModel() is true + if( optUseModel() ){ + FirstOrderModel* fm = (FirstOrderModel*)m; + //initialize model + fm->initialize(); + //analyze the quantifiers + Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; + analyzeQuantifiers( fm ); + //if applicable, find exceptions + if( optInstGen() ){ + //now, see if we know that any exceptions via InstGen exist + Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl; + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + if( d_quant_sat.find( f )==d_quant_sat.end() ){ + d_addedLemmas += doInstGen( fm, f ); + if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){ + break; + } + } } - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - val = it->second.getValue( qe, n, indexOrder, childDepIndex[i], argIndex+1 ); - if( !val.isNull() ){ - break; + if( Options::current()->printModelEngine ){ + if( d_addedLemmas>0 ){ + Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl; + }else{ + Message() << "No InstGen lemmas..." << std::endl; } - }else{ - //argument is not a defined argument: thus, it depends on this argument - childDepIndex[i] = argIndex+1; } + Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl; + } + if( d_addedLemmas==0 ){ + //if no immediate exceptions, build the model + // this model will be an approximation that will need to be tested via exhaustive instantiation + Debug("fmf-model-debug") << "Building model..." << std::endl; + finishBuildModel( fm ); } - //update depIndex - depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1]; - //Notice() << "Return " << val << ", depIndex = " << depIndex; - //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl; - return val; } } -//simplify function -void UfModelTree::simplify( Node op, Node defaultVal, int argIndex ){ - if( argIndex<(int)op.getType().getNumChildren()-1 ){ - std::vector< Node > eraseData; - //first process the default argument - Node r; - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( r ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){ - defaultVal = it->second.d_value; +void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){ + d_quant_selection_lits.clear(); + d_quant_sat.clear(); + d_uf_prefs.clear(); + int quantSatInit = 0; + int nquantSatInit = 0; + //analyze the preferences of each quantifier + for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; + std::vector< Node > pro_con[2]; + std::vector< Node > constantSatOps; + bool constantSatReconsider; + //for each asserted quantifier f, + // - determine which literals form model basis for each quantifier + // - check which function/predicates have good and bad definitions according to f + for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); + it != d_qe->d_phase_reqs[f].end(); ++it ){ + Node n = it->first; + Node gn = d_qe->getTermDatabase()->getModelBasis( n ); + Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; + //calculate preference + int pref = 0; + bool value; + if( d_qe->getValuation().hasSatValue( gn, value ) ){ + if( value!=it->second ){ + //store this literal as a model basis literal + // this literal will force a default values in model that (modulo exceptions) shows + // that f is satisfied by the model + d_quant_selection_lits[f].push_back( value ? n : n.notNode() ); + pref = 1; }else{ - defaultVal = Node::null(); + pref = -1; } } - } - //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( it->first ); + if( pref!=0 ){ + //Store preferences for UF + bool isConst = !n.hasAttribute(InstConstantAttribute()); + std::vector< Node > uf_terms; + if( gn.getKind()==APPLY_UF ){ + uf_terms.push_back( gn ); + isConst = fm->d_uf_model[gn.getOperator()].isConstant(); + }else if( gn.getKind()==EQUAL ){ + isConst = true; + for( int j=0; j<2; j++ ){ + if( n[j].hasAttribute(InstConstantAttribute()) ){ + if( n[j].getKind()==APPLY_UF ){ + Node op = gn[j].getOperator(); + if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){ + uf_terms.push_back( gn[j] ); + isConst = isConst && fm->d_uf_model[op].isConstant(); + }else{ + isConst = false; + } + }else{ + isConst = false; + } + } + } + } + Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); + Debug("fmf-model-prefs") << " the definition of " << n << std::endl; + if( pref==1 && isConst ){ + d_quant_sat[f] = true; + //instead, just note to the model for each uf term that f is pro its definition + constantSatReconsider = false; + constantSatOps.clear(); + for( int j=0; j<(int)uf_terms.size(); j++ ){ + Node op = uf_terms[j].getOperator(); + constantSatOps.push_back( op ); + if( d_uf_prefs[op].d_reconsiderModel ){ + constantSatReconsider = true; + } + } + if( !constantSatReconsider ){ + break; + } }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); + int pcIndex = pref==1 ? 0 : 1; + for( int j=0; j<(int)uf_terms.size(); j++ ){ + pro_con[pcIndex].push_back( uf_terms[j] ); + } } } } - for( int i=0; i<(int)eraseData.size(); i++ ){ - d_data.erase( eraseData[i] ); - } - } -} - -//is total function -bool UfModelTree::isTotal( Node op, int argIndex ){ - if( argIndex==(int)(op.getType().getNumChildren()-1) ){ - return !d_value.isNull(); - }else{ - Node r; - std::map< Node, UfModelTree >::iterator it = d_data.find( r ); - if( it!=d_data.end() ){ - return it->second.isTotal( op, argIndex+1 ); + if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; + for( int i=0; i<(int)constantSatOps.size(); i++ ){ + Debug("fmf-model-prefs") << constantSatOps[i] << " "; + d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false; + } + Debug("fmf-model-prefs") << std::endl; + quantSatInit++; + d_statistics.d_pre_sat_quant += quantSatInit; }else{ - return false; - } - } -} - -Node UfModelTree::getConstantValue( QuantifiersEngine* qe, Node n, std::vector< int >& indexOrder, int argIndex ){ - return d_value; -} - -void indent( const char* c, int ind ){ - for( int i=0; i<ind; i++ ){ - Debug( c ) << " "; - } -} - -void UfModelTree::debugPrint( const char* c, QuantifiersEngine* qe, std::vector< int >& indexOrder, int ind, int arg ){ - if( !d_data.empty() ){ - for( std::map< Node, UfModelTree >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - indent( c, ind ); - Debug( c ) << "if x_" << indexOrder[arg] << " == " << it->first << std::endl; - it->second.debugPrint( c, qe, indexOrder, ind+2, arg+1 ); + nquantSatInit++; + d_statistics.d_pre_nsat_quant += quantSatInit; + //note quantifier's value preferences to models + for( int k=0; k<2; k++ ){ + for( int j=0; j<(int)pro_con[k].size(); j++ ){ + Node op = pro_con[k][j].getOperator(); + Node r = fm->getRepresentative( pro_con[k][j] ); + d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + } } } - if( d_data.find( Node::null() )!=d_data.end() ){ - d_data[ Node::null() ].debugPrint( c, qe, indexOrder, ind, arg+1 ); - } - }else{ - indent( c, ind ); - Debug( c ) << "return "; - printRepresentative( c, qe, d_value ); - //Debug( c ) << " { "; - //for( int i=0; i<(int)d_explicit.size(); i++ ){ - // Debug( c ) << d_explicit[i] << " "; - //} - //Debug( c ) << "}"; - Debug( c ) << std::endl; } + Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; } -UfModel::UfModel( Node op, ModelEngine* me ) : d_op( op ), d_me( me ), - d_model_constructed( false ), d_reconsider_model( false ){ - - d_tree = UfModelTreeOrdered( op ); TypeNode tn = d_op.getType(); tn = tn[(int)tn.getNumChildren()-1]; Assert( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ); //look at ground assertions - for( int i=0; i<(int)d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ].size(); i++ ){ - Node n = d_me->getQuantifiersEngine()->getTermDatabase()->d_op_map[ d_op ][i]; - bool add = true; - if( n.getAttribute(NoMatchAttribute()) ){ - add = false; - //determine if it has model basis attribute - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - if( n[j].getAttribute(ModelBasisAttribute()) ){ - add = true; - break; +int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){ + //we wish to add all known exceptions to our model basis literal(s) + // 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. + int addedLemmas = 0; + for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){ + bool phase = d_quant_selection_lits[f][i].getKind()!=NOT; + Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i]; + Assert( lit.hasAttribute(InstConstantAttribute()) ); + std::vector< Node > tr_terms; + if( lit.getKind()==APPLY_UF ){ + //only match predicates that are contrary to this one, use literal matching + Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + fm->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + tr_terms.push_back( eq ); + }else if( lit.getKind()==EQUAL ){ + //collect trigger terms + for( int j=0; j<2; j++ ){ + if( lit[j].hasAttribute(InstConstantAttribute()) ){ + if( lit[j].getKind()==APPLY_UF ){ + tr_terms.push_back( lit[j] ); + }else{ + tr_terms.clear(); + break; + } } } - } - if( add ){ - d_ground_asserts.push_back( n ); - Node r = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n ); - d_ground_asserts_reps.push_back( r ); - } - } - //determine if it is constant - if( !d_ground_asserts.empty() ){ - bool isConstant = true; - for( int i=1; i<(int)d_ground_asserts.size(); i++ ){ - if( d_ground_asserts_reps[0]!=d_ground_asserts_reps[i] ){ - isConstant = false; - break; + if( tr_terms.size()==1 && !phase ){ + //equality between a function and a ground term, use literal matching + tr_terms.clear(); + tr_terms.push_back( lit ); } } - if( isConstant ){ - //set constant value - Node t = d_me->getModelBasisApplyUfTerm( d_op ); - Node r = d_ground_asserts_reps[0]; - setValue( t, r, false ); - setModel(); - d_reconsider_model = true; - Debug("fmf-model-cons") << "Function " << d_op << " is the constant function "; - printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), r ); - Debug("fmf-model-cons") << std::endl; + //if applicable, try to add exceptions here + if( !tr_terms.empty() ){ + //make a trigger for these terms, add instantiations + Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms ); + //Notice() << "Trigger = " << (*tr) << std::endl; + tr->resetInstantiationRound(); + tr->reset( Node::null() ); + //d_qe->d_optInstMakeRepresentative = false; + //d_qe->d_optMatchIgnoreModelBasis = true; + addedLemmas += tr->addInstantiations( d_quant_basis_match[f] ); } } + return addedLemmas; } -void UfModel::setValue( Node n, Node v, bool ground ){ - d_set_values[ ground ? 1 : 0 ][n] = v; -} - -void UfModel::setModel(){ - makeModel( d_me->getQuantifiersEngine(), d_tree ); - d_model_constructed = true; -} - -void UfModel::clearModel(){ - for( int k=0; k<2; k++ ){ - d_set_values[k].clear(); +void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){ + //build model for UF + for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){ + finishBuildModelUf( fm, it->second ); } - d_tree.clear(); - d_model_constructed = false; -} - -Node UfModel::getConstantValue( QuantifiersEngine* qe, Node n ){ - if( d_model_constructed ){ - return d_tree.getConstantValue( qe, n ); - }else{ - return Node::null(); + //build model for arrays + for( std::map< Node, Node >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){ + //consult the model basis select term + // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term + TypeNode tn = it->first.getType(); + Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) ); + it->second = fm->getRepresentative( selModelBasis ); } + Debug("fmf-model-debug") << "Done building models." << std::endl; } -bool UfModel::isConstant(){ - Node gn = d_me->getModelBasisApplyUfTerm( d_op ); - Node n = getConstantValue( d_me->getQuantifiersEngine(), gn ); - return !n.isNull(); -} - -void UfModel::buildModel(){ +void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){ + Node op = model.getOperator(); #ifdef RECONSIDER_FUNC_CONSTANT - if( d_model_constructed ){ - if( d_reconsider_model ){ + if( model.isModelConstructed() && model.isConstant() ){ + if( d_uf_prefs[op].d_reconsiderModel ){ //if we are allowed to reconsider default value, then see if the default value can be improved - Node t = d_me->getModelBasisApplyUfTerm( d_op ); - Node v = d_set_values[0][t]; - if( d_value_pro_con[1][v].size()>d_value_pro_con[0][v].size() ){ - Debug("fmf-model-cons-debug") << "Consider changing the default value for " << d_op << std::endl; - clearModel(); + Node t = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + Node v = model.getConstantValue( t ); + if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ + Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; + model.clearModel(); } } } #endif - //now, construct models for each uninterpretted function/predicate - if( !d_model_constructed ){ - Debug("fmf-model-cons") << "Construct model for " << d_op << "..." << std::endl; - //now, set the values in the model - for( int i=0; i<(int)d_ground_asserts.size(); i++ ){ - Node n = d_ground_asserts[i]; - Node v = d_ground_asserts_reps[i]; + if( !model.isModelConstructed() ){ + //construct the model for the uninterpretted function/predicate + bool setDefaultVal = true; + Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); + Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; + //set the values in the model + for( size_t i=0; i<model.d_ground_asserts.size(); i++ ){ + Node n = model.d_ground_asserts[i]; + Node v = model.d_ground_asserts_reps[i]; //if this assertion did not help the model, just consider it ground //set n = v in the model tree Debug("fmf-model-cons") << " Set " << n << " = "; - printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v ); + fm->printRepresentativeDebug( "fmf-model-cons", v ); Debug("fmf-model-cons") << std::endl; //set it as ground value - setValue( n, v ); - } - //set the default value - //chose defaultVal based on heuristic (the best proportion of "pro" responses) - Node defaultVal; - double maxScore = -1; - for( int i=0; i<(int)d_values.size(); i++ ){ - Node v = d_values[i]; - double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)d_value_pro_con[1][v].size() ); - Debug("fmf-model-cons") << " - score( "; - printRepresentative( "fmf-model-cons", d_me->getQuantifiersEngine(), v ); - Debug("fmf-model-cons") << " ) = " << score << std::endl; - if( score>maxScore ){ - defaultVal = v; - maxScore = score; - } - } -#ifdef RECONSIDER_FUNC_DEFAULT_VALUE - if( maxScore<1.0 ){ - //consider finding another value, if possible - Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; - TypeNode tn = d_op.getType(); - Node newDefaultVal = d_me->getArbitraryElement( tn[(int)tn.getNumChildren()-1], d_values ); - if( !newDefaultVal.isNull() ){ - defaultVal = newDefaultVal; - Debug("fmf-model-cons-debug") << "-> Change default value to "; - printRepresentative( "fmf-model-cons-debug", d_me->getQuantifiersEngine(), defaultVal ); - Debug("fmf-model-cons-debug") << std::endl; + model.setValue( n, v ); + if( model.optUsePartialDefaults() ){ + //also set as default value if necessary + //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){ + if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){ + model.setValue( n, v, false ); + if( n==defaultTerm ){ + //incidentally already set, we will not need to find a default value + setDefaultVal = false; + } + } }else{ - Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl; - Debug("fmf-model-cons-debug") << " Excluding: "; - for( int i=0; i<(int)d_values.size(); i++ ){ - Debug("fmf-model-cons-debug") << d_values[i] << " "; + if( n==defaultTerm ){ + model.setValue( n, v, false ); + //incidentally already set, we will not need to find a default value + setDefaultVal = false; } - Debug("fmf-model-cons-debug") << std::endl; } } -#endif - Assert( !defaultVal.isNull() ); - //get the default term (this term must be defined non-ground in model) - Node defaultTerm = d_me->getModelBasisApplyUfTerm( d_op ); - Debug("fmf-model-cons") << " Choose "; - printRepresentative("fmf-model-cons", d_me->getQuantifiersEngine(), defaultVal ); - Debug("fmf-model-cons") << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; - Debug("fmf-model-cons") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; - setValue( defaultTerm, defaultVal, false ); + //set the overall default value if not set already (is this necessary??) + if( setDefaultVal ){ + Debug("fmf-model-cons") << " Choose default value..." << std::endl; + //chose defaultVal based on heuristic, currently the best ratio of "pro" responses + Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); + Assert( !defaultVal.isNull() ); + model.setValue( defaultTerm, defaultVal, false ); + } Debug("fmf-model-cons") << " Making model..."; - setModel(); - Debug("fmf-model-cons") << " Finished constructing model for " << d_op << "." << std::endl; + model.setModel(); + Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; } } -void UfModel::setValuePreference( Node f, Node n, bool isPro ){ - Node v = d_me->getQuantifiersEngine()->getEqualityQuery()->getRepresentative( n ); - //Notice() << "Set value preference " << n << " = " << v << " " << isPro << std::endl; - if( std::find( d_values.begin(), d_values.end(), v )==d_values.end() ){ - d_values.push_back( v ); - } - int index = isPro ? 0 : 1; - if( std::find( d_value_pro_con[index][v].begin(), d_value_pro_con[index][v].end(), f )==d_value_pro_con[index][v].end() ){ - d_value_pro_con[index][v].push_back( f ); - } +bool ModelEngineBuilder::optUseModel() { + return Options::current()->fmfModelBasedInst; } -void UfModel::makeModel( QuantifiersEngine* qe, UfModelTreeOrdered& tree ){ - for( int k=0; k<2; k++ ){ - for( std::map< Node, Node >::iterator it = d_set_values[k].begin(); it != d_set_values[k].end(); ++it ){ - tree.setValue( qe, it->first, it->second, k==1 ); - } - } - tree.simplify(); +bool ModelEngineBuilder::optInstGen(){ + return Options::current()->fmfInstGen; +} + +bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ +#ifdef ONE_QUANT_PER_ROUND_INST_GEN + return true; +#else + return false; +#endif } -void UfModel::debugPrint( const char* c ){ - //Debug( c ) << "Function " << d_op << std::endl; - //Debug( c ) << " Type: " << d_op.getType() << std::endl; - //Debug( c ) << " Ground asserts:" << std::endl; - //for( int i=0; i<(int)d_ground_asserts.size(); i++ ){ - // Debug( c ) << " " << d_ground_asserts[i] << " = "; - // printRepresentative( c, d_me->getQuantifiersEngine(), d_ground_asserts[i] ); - // Debug( c ) << std::endl; - //} - //Debug( c ) << " Model:" << std::endl; +ModelEngineBuilder::Statistics::Statistics(): + d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0), + d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0) +{ + StatisticsRegistry::registerStat(&d_pre_sat_quant); + StatisticsRegistry::registerStat(&d_pre_nsat_quant); +} - TypeNode t = d_op.getType(); - Debug( c ) << d_op << "( "; - for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){ - Debug( c ) << "x_" << i << " : " << t[i]; - if( i<(int)(t.getNumChildren()-2) ){ - Debug( c ) << ", "; - } - } - Debug( c ) << " ) : " << t[(int)t.getNumChildren()-1] << std::endl; - if( d_tree.isEmpty() ){ - Debug( c ) << " [undefined]" << std::endl; - }else{ - d_tree.debugPrint( c, d_me->getQuantifiersEngine(), 3 ); - Debug( c ) << std::endl; - } - //Debug( c ) << " Phase reqs:" << std::endl; //for( int i=0; i<2; i++ ){ - // for( std::map< Node, std::vector< Node > >::iterator it = d_reqs[i].begin(); it != d_reqs[i].end(); ++it ){ - // Debug( c ) << " " << it->first << std::endl; - // for( int j=0; j<(int)it->second.size(); j++ ){ - // Debug( c ) << " " << it->second[j] << " -> " << (i==1) << std::endl; - // } - // } - //} - //Debug( c ) << std::endl; - //for( int i=0; i<2; i++ ){ - // for( std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_eq_reqs[i].begin(); it != d_eq_reqs[i].end(); ++it ){ - // Debug( c ) << " " << "For " << it->first << ":" << std::endl; - // for( std::map< Node, std::vector< Node > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ - // for( int j=0; j<(int)it2->second.size(); j++ ){ - // Debug( c ) << " " << it2->first << ( i==1 ? "==" : "!=" ) << it2->second[j] << std::endl; - // } - // } - // } - //} +ModelEngineBuilder::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_pre_sat_quant); + StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); } //Model Engine constructor -ModelEngine::ModelEngine( TheoryQuantifiers* th ){ - d_th = th; - d_quantEngine = th->getQuantifiersEngine(); - d_ss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver(); +ModelEngine::ModelEngine( QuantifiersEngine* qe ) : +QuantifiersModule( qe ), +d_builder( qe ), +d_rel_domain( qe->getModel() ){ + } void ModelEngine::check( Theory::Effort e ){ - if( e==Theory::EFFORT_LAST_CALL ){ - bool quantsInit = true; + if( e==Theory::EFFORT_LAST_CALL && !d_quantEngine->hasAddedLemma() ){ //first, check if we can minimize the model further - if( !d_ss->minimize() ){ + if( !((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getStrongSolver()->minimize() ){ return; } - if( useModel() ){ - //now, check if any quantifiers are un-initialized - for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getAssertedQuantifier( i ); - if( !initializeQuantifier( f ) ){ - quantsInit = false; - } + //the following will attempt to build a model and test that it satisfies all asserted universal quantifiers + int addedLemmas = 0; + if( d_builder.optUseModel() ){ + //check if any quantifiers are un-initialized + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + addedLemmas += initializeQuantifier( f ); } } - if( quantsInit ){ -#ifdef ME_PRINT_PROCESS_TIMES - Notice() << "---Instantiation Round---" << std::endl; -#endif + if( addedLemmas==0 ){ + //quantifiers are initialized, we begin an instantiation round + double clSet = 0; + if( Options::current()->printModelEngine ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Message() << "---Model Engine Round---" << std::endl; + } Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl; ++(d_statistics.d_inst_rounds); - d_quantEngine->getTermDatabase()->reset( e ); - //build the representatives - Debug("fmf-model-debug") << "Building representatives..." << std::endl; - buildRepresentatives(); - if( useModel() ){ - //initialize the model - Debug("fmf-model-debug") << "Initializing model..." << std::endl; - initializeModel(); - //analyze the quantifiers - Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl; - analyzeQuantifiers(); - //build the model - Debug("fmf-model-debug") << "Building model..." << std::endl; - for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.buildModel(); + //reset the quantifiers engine + d_quantEngine->resetInstantiationRound( e ); + //initialize the model + Debug("fmf-model-debug") << "Build model..." << std::endl; + d_builder.buildModel( d_quantEngine->getModel() ); + d_quantEngine->d_model_set = true; + //if builder has lemmas, add and return + if( d_builder.d_addedLemmas>0 ){ + addedLemmas += (int)d_builder.d_addedLemmas; + }else{ + //print debug + Debug("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); + //verify we are SAT by trying exhaustive instantiation + if( optUseRelevantDomain() ){ + d_rel_domain.compute(); } - } - //print debug - debugPrint("fmf-model-complete"); - //try exhaustive instantiation - Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; - int addedLemmas = 0; - for( int i=0; i<d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getAssertedQuantifier( i ); - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - addedLemmas += instantiateQuantifier( f ); + d_triedLemmas = 0; + d_testLemmas = 0; + d_relevantLemmas = 0; + d_totalLemmas = 0; + Debug("fmf-model-debug") << "Do exhaustive instantiation..." << std::endl; + for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( d_builder.d_quant_sat.find( f )==d_builder.d_quant_sat.end() ){ + addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() ); + if( optOneQuantPerRound() && addedLemmas>0 ){ + break; + } + } +#ifdef ME_PRINT_WARNINGS + if( addedLemmas>10000 ){ + break; + } +#endif + } + Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + if( Options::current()->printModelEngine ){ + Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / "; + Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl; + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl; + } +#ifdef ME_PRINT_WARNINGS + if( addedLemmas>10000 ){ + Debug("fmf-exit") << std::endl; + debugPrint("fmf-exit"); + exit( 0 ); } - } -#ifdef ME_PRINT_PROCESS_TIMES - Notice() << "Added Lemmas = " << addedLemmas << std::endl; #endif - if( addedLemmas==0 ){ - //debugPrint("fmf-consistent"); - //for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - // it->second.simplify(); - //} - Debug("fmf-consistent") << std::endl; - debugPrint("fmf-consistent"); } } - d_quantEngine->flushLemmas( &d_th->getOutputChannel() ); + if( addedLemmas==0 ){ + //CVC4 will answer SAT + Debug("fmf-consistent") << std::endl; + debugPrint("fmf-consistent"); + }else{ + //otherwise, the search will continue + d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() ); + } } } @@ -611,19 +462,31 @@ void ModelEngine::assertNode( Node f ){ } -bool ModelEngine::useModel() { - return Options::current()->fmfModelBasedInst; +bool ModelEngine::optOneInstPerQuantRound(){ + return Options::current()->fmfOneInstPerRound; +} + +bool ModelEngine::optUseRelevantDomain(){ + return Options::current()->fmfRelevantDomain; +} + +bool ModelEngine::optOneQuantPerRound(){ +#ifdef ONE_QUANT_PER_ROUND + return true; +#else + return false; +#endif } -bool ModelEngine::initializeQuantifier( Node f ){ +int ModelEngine::initializeQuantifier( Node f ){ if( d_quant_init.find( f )==d_quant_init.end() ){ d_quant_init[f] = true; Debug("inst-fmf-init") << "Initialize " << f << std::endl; //add the model basis instantiation // This will help produce the necessary information for model completion. - // We do this by extending distinguish ground assertions (those + // We do this by extending distinguish ground assertions (those // containing terms with "model basis" attribute) to hold for all cases. - + ////first, check if any variables are required to be equal //for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ @@ -632,747 +495,167 @@ bool ModelEngine::initializeQuantifier( Node f ){ // Notice() << "Unhandled phase req: " << n << std::endl; // } //} - + std::vector< Node > ics; std::vector< Node > terms; for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - terms.push_back( getModelBasisTerm( f[0][j].getType() ) ); + Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j ); + Node t = d_quantEngine->getTermDatabase()->getModelBasisTerm( ic.getType() ); + ics.push_back( ic ); + terms.push_back( t ); + //calculate the basis match for f + d_builder.d_quant_basis_match[f].d_map[ ic ] = t; } ++(d_statistics.d_num_quants_init); + //register model basis body + Node n = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); + Node gn = n.substitute( ics.begin(), ics.end(), terms.begin(), terms.end() ); + d_quantEngine->getTermDatabase()->registerModelBasis( n, gn ); + //add model basis instantiation if( d_quantEngine->addInstantiation( f, terms ) ){ - return false; + return 1; }else{ - //usually shouldn't happen + //shouldn't happen usually, but will occur if x != y is a required literal for f. //Notice() << "No model basis for " << f << std::endl; ++(d_statistics.d_num_quants_init_fail); } } - return true; -} - -void ModelEngine::buildRepresentatives(){ - d_ra.clear(); - //collect all representatives for all types and store as representative alphabet - for( int i=0; i<d_ss->getNumCardinalityTypes(); i++ ){ - TypeNode tn = d_ss->getCardinalityType( i ); - std::vector< Node > reps; - d_ss->getRepresentatives( tn, reps ); - Assert( !reps.empty() ); - //if( (int)reps.size()!=d_ss->getCardinality( tn ) ){ - // Notice() << "InstStrategyFinteModelFind::processResetInstantiationRound: Bad representatives for type." << std::endl; - // Notice() << " " << tn << " has cardinality " << d_ss->getCardinality( tn ); - // Notice() << " but only " << (int)reps.size() << " were given." << std::endl; - // Unimplemented( 27 ); - //} - Debug("fmf-model-debug") << " " << tn << " -> " << reps.size() << std::endl; - Debug("fmf-model-debug") << " "; - for( int i=0; i<(int)reps.size(); i++ ){ - Debug("fmf-model-debug") << reps[i] << " "; - } - Debug("fmf-model-debug") << std::endl; - //set them in the alphabet - d_ra.set( tn, reps ); -#ifdef ME_PRINT_PROCESS_TIMES - Notice() << tn << " has " << reps.size() << " representatives. " << std::endl; -#endif - } + return 0; } -void ModelEngine::initializeModel(){ - d_uf_model.clear(); - d_quant_sat.clear(); - for( int k=0; k<2; k++ ){ - d_pro_con_quant[k].clear(); - } - - ////now analyze quantifiers (temporary) - //for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - // Node f = d_quantEngine->getAssertedQuantifier( i ); - // Debug("fmf-model-req") << "Phase requirements for " << f << ": " << std::endl; - // for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); - // it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ - // Node n = it->first; - // Debug("fmf-model-req") << " " << n << " -> " << it->second << std::endl; - // if( n.getKind()==APPLY_UF ){ - // processPredicate( f, n, it->second ); - // }else if( n.getKind()==EQUAL ){ - // processEquality( f, n, it->second ); - // } - // } - //} - for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getAssertedQuantifier( i ); - initializeUf( f[1] ); - //register model basis terms - std::vector< Node > vars; - std::vector< Node > subs; - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - vars.push_back( d_quantEngine->getInstantiationConstant( f, j ) ); - subs.push_back( getModelBasisTerm( f[0][j].getType() ) ); - } - Node n = d_quantEngine->getCounterexampleBody( f ); - Node gn = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - registerModelBasis( n, gn ); - } -} - -void ModelEngine::analyzeQuantifiers(){ - int quantSatInit = 0; - int nquantSatInit = 0; - //analyze the preferences of each quantifier - for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getAssertedQuantifier( i ); - Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; - std::vector< Node > pro_con[2]; - std::vector< Node > pro_con_patterns[2]; - //check which model basis terms have good and bad definitions according to f - for( std::map< Node, bool >::iterator it = d_quantEngine->d_phase_reqs[f].begin(); - it != d_quantEngine->d_phase_reqs[f].end(); ++it ){ - Node n = it->first; - Node gn = d_model_basis[n]; - Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl; - int pref = 0; - bool isConst = true; - std::vector< Node > uf_terms; - std::vector< Node > uf_term_patterns; - if( gn.getKind()==APPLY_UF ){ - if( d_quantEngine->getEqualityQuery()->hasTerm( gn ) ){ - uf_terms.push_back( gn ); - uf_term_patterns.push_back( n ); - bool phase = areEqual( gn, NodeManager::currentNM()->mkConst( true ) ); - pref = phase!=it->second ? 1 : -1; - } - }else if( gn.getKind()==EQUAL ){ - bool success = true; - for( int j=0; j<2; j++ ){ - if( n[j].getKind()==APPLY_UF ){ - Node op = gn[j].getOperator(); - if( d_uf_model.find( op )!=d_uf_model.end() ){ - Assert( gn[j].getKind()==APPLY_UF ); - uf_terms.push_back( gn[j] ); - uf_term_patterns.push_back( n[j] ); - }else{ - //found undefined uf operator - success = false; - } - }else if( n[j].hasAttribute(InstConstantAttribute()) ){ - isConst = false; - } - } - if( success && !uf_terms.empty() ){ - if( (!it->second && areEqual( gn[0], gn[1] )) || (it->second && areDisequal( gn[0], gn[1] )) ){ - pref = 1; - }else if( (it->second && areEqual( gn[0], gn[1] )) || (!it->second && areDisequal( gn[0], gn[1] )) ){ - pref = -1; - } - } - } - if( pref!=0 ){ - Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" ); - Debug("fmf-model-prefs") << " the definition of " << n << std::endl; - if( pref==1 ){ - if( isConst ){ - for( int j=0; j<(int)uf_terms.size(); j++ ){ - //the only uf that is initialized are those that are constant - Node op = uf_terms[j].getOperator(); - Assert( d_uf_model.find( op )!=d_uf_model.end() ); - if( !d_uf_model[op].isConstant() ){ - isConst = false; - break; - } - } - if( isConst ){ - d_quant_sat[f] = true; - //we only need to consider current term definition(s) for this quantifier to be satisified, ignore the others - for( int k=0; k<2; k++ ){ - pro_con[k].clear(); - pro_con_patterns[k].clear(); - } - //instead, just note to the model for each uf term that f is pro its definition - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - d_uf_model[op].d_reconsider_model = false; - } - } - } - } - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - Debug("fmf-model-prefs") << " * Constant SAT due to definition of " << n << std::endl; - break; - }else{ - int pcIndex = pref==1 ? 0 : 1; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - pro_con[pcIndex].push_back( uf_terms[j] ); - pro_con_patterns[pcIndex].push_back( uf_term_patterns[j] ); - } - } - } - } - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - quantSatInit++; - d_statistics.d_pre_sat_quant += quantSatInit; - }else{ - nquantSatInit++; - d_statistics.d_pre_nsat_quant += quantSatInit; - } - //add quantifier's preferences to vector - for( int k=0; k<2; k++ ){ - for( int j=0; j<(int)pro_con[k].size(); j++ ){ - Node op = pro_con[k][j].getOperator(); - d_uf_model[op].setValuePreference( f, pro_con[k][j], k==0 ); - d_pro_con_quant[k][ f ].push_back( pro_con_patterns[k][j] ); - } - } - } - Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl; -} - -int ModelEngine::instantiateQuantifier( Node f ){ +int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ + int tests = 0; int addedLemmas = 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; i<f[0].getNumChildren(); i++ ){ - Debug("inst-fmf-ei") << d_quantEngine->getInstantiationConstant( f, i ) << " "; + Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " "; } Debug("inst-fmf-ei") << std::endl; - for( int k=0; k<2; k++ ){ - Debug("inst-fmf-ei") << " " << ( k==0 ? "Pro" : "Con" ) << " definitions:" << std::endl; - for( int i=0; i<(int)d_pro_con_quant[k][f].size(); i++ ){ - Debug("inst-fmf-ei") << " " << d_pro_con_quant[k][f][i] << std::endl; - } - } - if( d_pro_con_quant[0][f].empty() ){ - Debug("inst-fmf-ei") << "WARNING: " << f << " has no pros for default literal definitions" << std::endl; - } - d_eval_failed_lits.clear(); - d_eval_failed.clear(); - d_eval_term_model.clear(); - //d_eval_term_vals.clear(); - //d_eval_term_fv_deps.clear(); - RepAlphabetIterator riter( d_quantEngine, f, this ); - increment( &riter ); -#ifdef ONE_INST_PER_QUANT_PER_ROUND - while( !riter.isFinished() && addedLemmas==0 ){ -#else - while( !riter.isFinished() ){ + if( d_builder.d_quant_selection_lits[f].empty() ){ + Debug("inst-fmf-ei") << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; +#ifdef ME_PRINT_WARNINGS + Message() << "WARNING: " << f << " has no model literal definitions (is f clausified?)" << std::endl; #endif - InstMatch m; - riter.getMatch( d_quantEngine, m ); - Debug("fmf-model-eval") << "* Add instantiation " << std::endl; - riter.d_inst_tried++; - if( d_quantEngine->addInstantiation( f, m ) ){ - addedLemmas++; - } - riter.increment( d_quantEngine ); - increment( &riter ); - } - if( Debug.isOn("inst-fmf-ei") ){ - int totalInst = 1; - for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - totalInst = totalInst * (int)getReps()->d_type_reps[ f[0][i].getType() ].size(); - } - Debug("inst-fmf-ei") << "Finished: " << std::endl; - Debug("inst-fmf-ei") << " Inst Skipped: " << (totalInst-riter.d_inst_tried) << std::endl; - Debug("inst-fmf-ei") << " Inst Tried: " << riter.d_inst_tried << std::endl; - Debug("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl; - Debug("inst-fmf-ei") << " # Tests: " << riter.d_inst_tests << std::endl; - } - return addedLemmas; -} - -void ModelEngine::registerModelBasis( Node n, Node gn ){ - if( d_model_basis.find( n )==d_model_basis.end() ){ - d_model_basis[n] = gn; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - registerModelBasis( n[i], gn[i] ); - } - } -} - -Node ModelEngine::getArbitraryElement( TypeNode tn, std::vector< Node >& exclude ){ - Node retVal; - if( tn==NodeManager::currentNM()->booleanType() ){ - if( exclude.empty() ){ - retVal = NodeManager::currentNM()->mkConst( false ); - }else if( exclude.size()==1 ){ - retVal = NodeManager::currentNM()->mkConst( areEqual( exclude[0], NodeManager::currentNM()->mkConst( false ) ) ); - } - }else if( d_ra.d_type_reps.find( tn )!=d_ra.d_type_reps.end() ){ - for( int i=0; i<(int)d_ra.d_type_reps[tn].size(); i++ ){ - if( std::find( exclude.begin(), exclude.end(), d_ra.d_type_reps[tn][i] )==exclude.end() ){ - retVal = d_ra.d_type_reps[tn][i]; - break; - } - } - } - if( !retVal.isNull() ){ - return d_quantEngine->getEqualityQuery()->getRepresentative( retVal ); }else{ - return Node::null(); - } -} - -Node ModelEngine::getModelBasisTerm( TypeNode tn, int i ){ - return d_ss->getCardinalityTerm( tn ); -} - -Node ModelEngine::getModelBasisApplyUfTerm( Node op ){ - if( d_model_basis_term.find( op )==d_model_basis_term.end() ){ - TypeNode t = op.getType(); - std::vector< Node > children; - children.push_back( op ); - for( int i=0; i<(int)t.getNumChildren()-1; i++ ){ - children.push_back( getModelBasisTerm( t[i] ) ); - } - d_model_basis_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - } - return d_model_basis_term[op]; -} - -bool ModelEngine::isModelBasisTerm( Node op, Node n ){ - if( n.getOperator()==op ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !n[i].getAttribute(ModelBasisAttribute()) ){ - return false; - } - } - return true; - }else{ - return false; - } -} - -void ModelEngine::initializeUf( Node n ){ - std::vector< Node > terms; - collectUfTerms( n, terms ); - for( int i=0; i<(int)terms.size(); i++ ){ - initializeUfModel( terms[i].getOperator() ); - } -} - -void ModelEngine::collectUfTerms( Node n, std::vector< Node >& terms ){ - if( n.getKind()==APPLY_UF ){ - terms.push_back( n ); - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - collectUfTerms( n[i], terms ); - } -} - -void ModelEngine::initializeUfModel( Node op ){ - if( d_uf_model.find( op )==d_uf_model.end() ){ - TypeNode tn = op.getType(); - tn = tn[ (int)tn.getNumChildren()-1 ]; - if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){ - d_uf_model[ op ] = UfModel( op, this ); - } - } -} - -void ModelEngine::makeEvalTermModel( Node n ){ - if( d_eval_term_model.find( n )==d_eval_term_model.end() ){ - makeEvalTermIndexOrder( n ); - if( !d_eval_term_use_default_model[n] ){ - Node op = n.getOperator(); - d_eval_term_model[n] = UfModelTreeOrdered( op, d_eval_term_index_order[n] ); - d_uf_model[op].makeModel( d_quantEngine, d_eval_term_model[n] ); - Debug("fmf-model-index-order") << "Make model for " << n << " : " << std::endl; - d_eval_term_model[n].debugPrint( "fmf-model-index-order", d_quantEngine, 2 ); - } - } -} - -struct sortGetMaxVariableNum { - std::map< Node, int > d_max_var_num; - int computeMaxVariableNum( Node n ){ - if( n.getKind()==INST_CONSTANT ){ - return n.getAttribute(InstVarNumAttribute()); - }else if( n.hasAttribute(InstConstantAttribute()) ){ - int maxVal = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - int val = getMaxVariableNum( n[i] ); - if( val>maxVal ){ - maxVal = val; - } - } - return maxVal; - }else{ - return -1; - } - } - int getMaxVariableNum( Node n ){ - std::map< Node, int >::iterator it = d_max_var_num.find( n ); - if( it==d_max_var_num.end() ){ - int num = computeMaxVariableNum( n ); - d_max_var_num[n] = num; - return num; - }else{ - return it->second; - } - } - bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} -}; - -void ModelEngine::makeEvalTermIndexOrder( Node n ){ - if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ - //sort arguments in order of least significant vs. most significant variable in default ordering - std::map< Node, std::vector< int > > argIndex; - std::vector< Node > args; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( argIndex.find( n[i] )==argIndex.end() ){ - args.push_back( n[i] ); - } - argIndex[n[i]].push_back( i ); - } - sortGetMaxVariableNum sgmvn; - std::sort( args.begin(), args.end(), sgmvn ); - for( int i=0; i<(int)args.size(); i++ ){ - for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ - d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); - } - } - bool useDefault = true; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - if( i!=d_eval_term_index_order[n][i] ){ - useDefault = false; - break; - } - } - d_eval_term_use_default_model[n] = useDefault; - Debug("fmf-model-index-order") << "Will consider the following index ordering for " << n << " : "; - for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ - Debug("fmf-model-index-order") << d_eval_term_index_order[n][i] << " "; - } - Debug("fmf-model-index-order") << std::endl; - } -} - -//void ModelEngine::processPredicate( Node f, Node p, bool phase ){ -// Node op = p.getOperator(); -// initializeUfModel( op ); -// d_uf_model[ op ].addRequirement( f, p, phase ); -//} -// -//void ModelEngine::processEquality( Node f, Node eq, bool phase ){ -// for( int i=0; i<2; i++ ){ -// int j = i==0 ? 1 : 0; -// if( eq[i].getKind()==APPLY_UF && eq[i].hasAttribute(InstConstantAttribute()) ){ -// Node op = eq[i].getOperator(); -// initializeUfModel( op ); -// d_uf_model[ op ].addEqRequirement( f, eq[i], eq[j], phase ); -// } -// } -//} - -void ModelEngine::increment( RepAlphabetIterator* rai ){ - if( useModel() ){ - bool success; - do{ - success = true; - if( !rai->isFinished() ){ - //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaulating "; - rai->debugPrintSmall("fmf-model-eval"); - //calculate represenative terms we are currently considering - rai->calculateTerms( d_quantEngine ); - rai->d_inst_tests++; - //if eVal is not (int)rai->d_index.size(), then the instantiation is already true in the model, - // and eVal is the highest index in rai which we can safely iterate - int depIndex; - if( evaluate( rai, d_quantEngine->getCounterexampleBody( rai->d_f ), depIndex )==1 ){ - Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; - //Notice() << "Returned eVal = " << eVal << "/" << rai->d_index.size() << std::endl; - if( depIndex<(int)rai->d_index.size() ){ -#ifdef DISABLE_EVAL_SKIP_MULTIPLE - depIndex = (int)rai->d_index.size()-1; -#endif - rai->increment2( d_quantEngine, depIndex ); - success = false; + Debug("inst-fmf-ei") << " Model literal definitions:" << std::endl; + for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ + Debug("inst-fmf-ei") << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; + } + } + RepSetIterator riter( f, d_quantEngine->getModel() ); + //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] ); + } + RepSetEvaluator reval( d_quantEngine->getModel(), &riter ); + while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){ + d_testLemmas++; + 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 + int depIndex = riter.getNumTerms()-1; + int eval = reval.evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex ); + if( eval==1 ){ + Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; + riter.increment2( depIndex ); + }else{ + Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl; + InstMatch m; + riter.getMatch( d_quantEngine, m ); + Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; + triedLemmas++; + d_triedLemmas++; + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; +#ifdef EVAL_FAIL_SKIP_MULTIPLE + if( eval==-1 ){ + riter.increment2( depIndex ); + }else{ + riter.increment(); } +#else + riter.increment(); +#endif }else{ - Debug("fmf-model-eval") << " Returned failure." << std::endl; - } - } - }while( !success ); - } -} - -//if evaluate( rai, n, phaseReq ) = eVal, -// if eVal = rai->d_index.size() -// then the formula n instantiated with rai cannot be proven to be equal to phaseReq -// otherwise, -// each n{rai->d_index[0]/x_0...rai->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model -int ModelEngine::evaluate( RepAlphabetIterator* rai, Node n, int& depIndex ){ - ++(d_statistics.d_eval_formulas); - //Debug("fmf-model-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; - if( n.getKind()==NOT ){ - int val = evaluate( rai, n[0], depIndex ); - return val==1 ? -1 : ( val==-1 ? 1 : 0 ); - }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){ - int baseVal = n.getKind()==AND ? 1 : -1; - int eVal = baseVal; - int posDepIndex = (int)rai->d_index.size(); - int negDepIndex = -1; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - //evaluate subterm - int childDepIndex; - Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; - int eValT = evaluate( rai, nn, childDepIndex ); - if( eValT==baseVal ){ - if( eVal==baseVal ){ - if( childDepIndex>negDepIndex ){ - negDepIndex = childDepIndex; - } - } - }else if( eValT==-baseVal ){ - eVal = -baseVal; - if( childDepIndex<posDepIndex ){ - posDepIndex = childDepIndex; - if( posDepIndex==-1 ){ - break; - } - } - }else if( eValT==0 ){ - if( eVal==baseVal ){ - eVal = 0; + Debug("ajr-temp") << "* Failed Add instantiation " << m << std::endl; + riter.increment(); } } - } - if( eVal!=0 ){ - depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; - return eVal; - }else{ - return 0; - } - }else if( n.getKind()==IFF || n.getKind()==XOR ){ - int depIndex1; - int eVal = evaluate( rai, n[0], depIndex1 ); - if( eVal!=0 ){ - int depIndex2; - int eVal2 = evaluate( rai, n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 ); - if( eVal2!=0 ){ - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eVal==eVal2 ? 1 : -1; - } - } - return 0; - }else if( n.getKind()==ITE ){ - int depIndex1; - int eVal = evaluate( rai, n[0], depIndex1 ); - if( eVal==0 ){ - //DO_THIS: evaluate children to see if they are the same value? - return 0; }else{ - int depIndex2; - int eValT = evaluate( rai, n[eVal==1 ? 1 : 2], depIndex2 ); - depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; - return eValT; - } - }else if( n.getKind()==FORALL ){ - return 0; - }else{ - ////if we know we will fail again, immediately return - //if( d_eval_failed.find( n )!=d_eval_failed.end() ){ - // if( d_eval_failed[n] ){ - // return -1; - // } - //} - //Debug("fmf-model-eval-debug") << "Evaluate literal " << n << std::endl; - //this should be a literal - Node gn = n.substitute( rai->d_ic.begin(), rai->d_ic.end(), rai->d_terms.begin(), rai->d_terms.end() ); - //Debug("fmf-model-eval-debug") << " Ground version = " << gn << std::endl; - int retVal = 0; - std::vector< Node > fv_deps; - if( n.getKind()==APPLY_UF ){ - //case for boolean predicates - Node val = evaluateTerm( n, gn, fv_deps ); - if( d_quantEngine->getEqualityQuery()->hasTerm( val ) ){ - if( areEqual( val, NodeManager::currentNM()->mkConst( true ) ) ){ - retVal = 1; - }else{ - retVal = -1; - } - } - }else if( n.getKind()==EQUAL ){ - //case for equality - retVal = evaluateEquality( n[0], n[1], gn[0], gn[1], fv_deps ); - } - if( retVal!=0 ){ - int maxIndex = -1; - for( int i=0; i<(int)fv_deps.size(); i++ ){ - int index = rai->d_var_order[ fv_deps[i].getAttribute(InstVarNumAttribute()) ]; - if( index>maxIndex ){ - maxIndex = index; - if( index==(int)rai->d_index.size()-1 ){ - break; - } - } + InstMatch m; + riter.getMatch( d_quantEngine, m ); + Debug("fmf-model-eval") << "* Add instantiation " << std::endl; + triedLemmas++; + d_triedLemmas++; + if( d_quantEngine->addInstantiation( f, m ) ){ + addedLemmas++; } - Debug("fmf-model-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << maxIndex << std::endl; - depIndex = maxIndex; + riter.increment(); } - return retVal; - } -} - -int ModelEngine::evaluateEquality( Node n1, Node n2, Node gn1, Node gn2, std::vector< Node >& fv_deps ){ - ++(d_statistics.d_eval_eqs); - Debug("fmf-model-eval-debug") << "Evaluate equality: " << std::endl; - Debug("fmf-model-eval-debug") << " " << n1 << " = " << n2 << std::endl; - Debug("fmf-model-eval-debug") << " " << gn1 << " = " << gn2 << std::endl; - Node val1 = evaluateTerm( n1, gn1, fv_deps ); - Node val2 = evaluateTerm( n2, gn2, fv_deps ); - Debug("fmf-model-eval-debug") << " Values : "; - printRepresentative( "fmf-model-eval-debug", d_quantEngine, val1 ); - Debug("fmf-model-eval-debug") << " = "; - printRepresentative( "fmf-model-eval-debug", d_quantEngine, val2 ); - Debug("fmf-model-eval-debug") << std::endl; - int retVal = 0; - if( areEqual( val1, val2 ) ){ - retVal = 1; - }else if( areDisequal( val1, val2 ) ){ - retVal = -1; - } - if( retVal!=0 ){ - Debug("fmf-model-eval-debug") << " ---> Success, value = " << (retVal==1) << std::endl; - }else{ - Debug("fmf-model-eval-debug") << " ---> Failed" << std::endl; - } - Debug("fmf-model-eval-debug") << " Value depends on variables: "; - for( int i=0; i<(int)fv_deps.size(); i++ ){ - Debug("fmf-model-eval-debug") << fv_deps[i] << " "; } - Debug("fmf-model-eval-debug") << std::endl; - return retVal; -} - -Node ModelEngine::evaluateTerm( Node n, Node gn, std::vector< Node >& fv_deps ){ - if( n.hasAttribute(InstConstantAttribute()) ){ - if( n.getKind()==INST_CONSTANT ){ - fv_deps.push_back( n ); - return gn; - //}else if( d_eval_term_fv_deps.find( n )!=d_eval_term_fv_deps.end() && - // d_eval_term_fv_deps[n].find( gn )!=d_eval_term_fv_deps[n].end() ){ - // fv_deps.insert( fv_deps.end(), d_eval_term_fv_deps[n][gn].begin(), d_eval_term_fv_deps[n][gn].end() ); - // return d_eval_term_vals[gn]; - }else{ - //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl; - //first we must evaluate the arguments - Node val = gn; - if( n.getKind()==APPLY_UF ){ - Node op = gn.getOperator(); - //if it is a defined UF, then consult the interpretation - Node gnn = gn; - ++(d_statistics.d_eval_uf_terms); - int depIndex = 0; - //first we must evaluate the arguments - bool childrenChanged = false; - std::vector< Node > children; - children.push_back( op ); - std::map< int, std::vector< Node > > children_var_deps; - //for each argument, calculate its value, and the variables its value depends upon - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nn = evaluateTerm( n[i], gn[i], children_var_deps[i] ); - children.push_back( nn ); - childrenChanged = childrenChanged || nn!=gn[i]; - } - //remake gn if changed - if( childrenChanged ){ - gnn = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - } - if( d_uf_model.find( op )!=d_uf_model.end() ){ -#ifdef USE_INDEX_ORDERING - //make the term model specifically for n - makeEvalTermModel( n ); - //now, consult the model - if( d_eval_term_use_default_model[n] ){ - val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex ); - }else{ - val = d_eval_term_model[ n ].getValue( d_quantEngine, gnn, depIndex ); - } - //Debug("fmf-model-eval-debug") << "Evaluate term " << n << " (" << gn << ", " << gnn << ")" << std::endl; - //d_eval_term_model[ n ].debugPrint("fmf-model-eval-debug", d_quantEngine ); - Assert( !val.isNull() ); -#else - //now, consult the model - val = d_uf_model[op].d_tree.getValue( d_quantEngine, gnn, depIndex ); -#endif - }else{ - d_eval_term_use_default_model[n] = true; - val = gnn; - depIndex = (int)n.getNumChildren(); - } - Debug("fmf-model-eval-debug") << "Evaluate term " << n << " = " << gn << " = " << gnn << " = "; - printRepresentative( "fmf-model-eval-debug", d_quantEngine, val ); - Debug("fmf-model-eval-debug") << ", depIndex = " << depIndex << std::endl; - if( !val.isNull() ){ -#ifdef USE_INDEX_ORDERING - for( int i=0; i<depIndex; i++ ){ - int index = d_eval_term_use_default_model[n] ? i : d_eval_term_index_order[n][i]; - Debug("fmf-model-eval-debug") << "Add variables from " << index << "..." << std::endl; - fv_deps.insert( fv_deps.end(), children_var_deps[index].begin(), - children_var_deps[index].end() ); - } -#else - //calculate the free variables that the value depends on : take those in children_var_deps[0...depIndex-1] - for( std::map< int, std::vector< Node > >::iterator it = children_var_deps.begin(); it != children_var_deps.end(); ++it ){ - if( it->first<depIndex ){ - fv_deps.insert( fv_deps.end(), it->second.begin(), it->second.end() ); - } - } -#endif - } - ////cache the result - //d_eval_term_vals[gn] = val; - //d_eval_term_fv_deps[n][gn].insert( d_eval_term_fv_deps[n][gn].end(), fv_deps.begin(), fv_deps.end() ); + d_statistics.d_eval_formulas += reval.d_eval_formulas; + d_statistics.d_eval_eqs += reval.d_eval_eqs; + d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms; + int totalInst = 1; + int relevantInst = 1; + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size(); + relevantInst = relevantInst * (int)riter.d_domain[i].size(); + } + d_totalLemmas += totalInst; + 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; +///----------- +#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; + if( !d_builder.d_quant_selection_lits[f].empty() ){ + Notice() << " Model literal definitions:" << std::endl; + for( size_t i=0; i<d_builder.d_quant_selection_lits[f].size(); i++ ){ + Notice() << " " << d_builder.d_quant_selection_lits[f][i] << std::endl; } - return val; + Notice() << std::endl; } - }else{ - return n; - } -} - -void ModelEngine::clearEvalFailed( int index ){ - for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ - d_eval_failed[ d_eval_failed_lits[index][i] ] = false; } - d_eval_failed_lits[index].clear(); -} - -bool ModelEngine::areEqual( Node a, Node b ){ - return d_quantEngine->getEqualityQuery()->areEqual( a, b ); -} - -bool ModelEngine::areDisequal( Node a, Node b ){ - return d_quantEngine->getEqualityQuery()->areDisequal( a, b ); +#endif +///----------- + return addedLemmas; } void ModelEngine::debugPrint( const char* c ){ - Debug( c ) << "---Current Model---" << std::endl; - Debug( c ) << "Representatives: " << std::endl; - d_ra.debugPrint( c, d_quantEngine ); Debug( c ) << "Quantifiers: " << std::endl; - for( int i=0; i<(int)d_quantEngine->getNumAssertedQuantifiers(); i++ ){ - Node f = d_quantEngine->getAssertedQuantifier( i ); + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug( c ) << " "; - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + if( d_builder.d_quant_sat.find( f )!=d_builder.d_quant_sat.end() ){ Debug( c ) << "*SAT* "; }else{ Debug( c ) << " "; } Debug( c ) << f << std::endl; } - Debug( c ) << "Functions: " << std::endl; - for( std::map< Node, UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){ - it->second.debugPrint( c ); - Debug( c ) << std::endl; - } + //d_quantEngine->getModel()->debugPrint( c ); } ModelEngine::Statistics::Statistics(): d_inst_rounds("ModelEngine::Inst_Rounds", 0), - d_pre_sat_quant("ModelEngine::Status_quant_pre_sat", 0), - d_pre_nsat_quant("ModelEngine::Status_quant_pre_non_sat", 0), d_eval_formulas("ModelEngine::Eval_Formulas", 0 ), d_eval_eqs("ModelEngine::Eval_Equalities", 0 ), d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ), @@ -1380,8 +663,6 @@ ModelEngine::Statistics::Statistics(): d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 ) { StatisticsRegistry::registerStat(&d_inst_rounds); - StatisticsRegistry::registerStat(&d_pre_sat_quant); - StatisticsRegistry::registerStat(&d_pre_nsat_quant); StatisticsRegistry::registerStat(&d_eval_formulas); StatisticsRegistry::registerStat(&d_eval_eqs); StatisticsRegistry::registerStat(&d_eval_uf_terms); @@ -1391,11 +672,11 @@ ModelEngine::Statistics::Statistics(): ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); - StatisticsRegistry::unregisterStat(&d_pre_sat_quant); - StatisticsRegistry::unregisterStat(&d_pre_nsat_quant); StatisticsRegistry::unregisterStat(&d_eval_formulas); StatisticsRegistry::unregisterStat(&d_eval_eqs); StatisticsRegistry::unregisterStat(&d_eval_uf_terms); StatisticsRegistry::unregisterStat(&d_num_quants_init); StatisticsRegistry::unregisterStat(&d_num_quants_init_fail); } + + |