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