summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r--src/theory/quantifiers/model_engine.cpp1401
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);
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback