diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/quantifiers/model_engine.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 1401 |
1 files changed, 1401 insertions, 0 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp new file mode 100644 index 000000000..a72b103d1 --- /dev/null +++ b/src/theory/quantifiers/model_engine.cpp @@ -0,0 +1,1401 @@ +/********************* */ +/*! \file model_engine.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of model engine class + **/ + +#include "theory/quantifiers/model_engine.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" + +//#define ME_PRINT_PROCESS_TIMES + +//#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 + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +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 ); + } +} + +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 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] ] ); + } + 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; + } + }else{ + //argument is not a defined argument: thus, it depends on this argument + childDepIndex[i] = argIndex+1; + } + } + //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; + }else{ + defaultVal = Node::null(); + } + } + } + //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 ); + }else{ + it->second.simplify( op, defaultVal, argIndex+1 ); + } + } + } + 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 ); + }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 ); + } + } + 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; + } +} + +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; + } + } + } + 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( 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; + } + } +} + +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(); + } + 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(); + } +} + +bool UfModel::isConstant(){ + Node gn = d_me->getModelBasisApplyUfTerm( d_op ); + Node n = getConstantValue( d_me->getQuantifiersEngine(), gn ); + return !n.isNull(); +} + +void UfModel::buildModel(){ +#ifdef RECONSIDER_FUNC_CONSTANT + if( d_model_constructed ){ + if( d_reconsider_model ){ + //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(); + } + } + } +#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 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 ); + 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; + }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] << " "; + } + 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 ); + Debug("fmf-model-cons") << " Making model..."; + setModel(); + Debug("fmf-model-cons") << " Finished constructing model for " << d_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 ); + } +} + +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(); +} + +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; + + 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; + // } + // } + // } + //} +} + +//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(); +} + +void ModelEngine::check( Theory::Effort e ){ + if( e==Theory::EFFORT_LAST_CALL ){ + bool quantsInit = true; + //first, check if we can minimize the model further + if( !d_ss->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; + } + } + } + if( quantsInit ){ +#ifdef ME_PRINT_PROCESS_TIMES + Notice() << "---Instantiation Round---" << std::endl; +#endif + 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(); + } + } + //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 ); + } + } +#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() ); + } +} + +void ModelEngine::registerQuantifier( Node f ){ + +} + +void ModelEngine::assertNode( Node f ){ + +} + +bool ModelEngine::useModel() { + return Options::current()->fmfModelBasedInst; +} + +bool 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 + // 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 ){ + // Node n = it->first; + // if( n.getKind()==EQUAL && n[0].getKind()==INST_CONSTANT && n[1].getKind()==INST_CONSTANT ){ + // Notice() << "Unhandled phase req: " << n << std::endl; + // } + //} + + std::vector< Node > terms; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + terms.push_back( getModelBasisTerm( f[0][j].getType() ) ); + } + ++(d_statistics.d_num_quants_init); + if( d_quantEngine->addInstantiation( f, terms ) ){ + return false; + }else{ + //usually shouldn't happen + //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 + } +} + +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 addedLemmas = 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") << 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() ){ +#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; + } + }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; + } + } + } + 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; + } + } + } + Debug("fmf-model-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << maxIndex << std::endl; + depIndex = maxIndex; + } + 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() ); + } + return val; + } + }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 ); +} + +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 ); + Debug( c ) << " "; + if( d_quant_sat.find( f )!=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; + } +} + +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 ), + d_num_quants_init("ModelEngine::Num_Quants", 0 ), + 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); + StatisticsRegistry::registerStat(&d_num_quants_init); + StatisticsRegistry::registerStat(&d_num_quants_init_fail); +} + +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); +} |