summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/fmf/model_builder.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/fmf/model_builder.cpp')
-rw-r--r--src/theory/quantifiers/fmf/model_builder.cpp684
1 files changed, 0 insertions, 684 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index c03fc7a32..8ef30fc4d 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -143,687 +143,3 @@ void QModelBuilder::debugModel( TheoryModel* m ){
}
}
}
-
-bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex)
-{
- if (argIndex < n.getNumChildren())
- {
- Node r;
- if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
- r = n[ argIndex ];
- }else{
- r = fm->getRepresentative( n[ argIndex ] );
- }
- std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
- if( it==d_data.end() ){
- d_data[r].addTerm(fm, n, argIndex + 1);
- return true;
- }else{
- return it->second.addTerm(fm, n, argIndex + 1);
- }
- }else{
- return false;
- }
-}
-
-void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q,
- Node r,
- bool isPro)
-{
- if (std::find(d_values.begin(), d_values.end(), r) == d_values.end())
- {
- d_values.push_back(r);
- }
- int index = isPro ? 0 : 1;
- if (std::find(
- d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), q)
- == d_value_pro_con[index][r].end())
- {
- d_value_pro_con[index][r].push_back(q);
- }
-}
-
-Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue(
- Node defaultTerm, TheoryModel* m)
-{
- Node defaultVal;
- double maxScore = -1;
- for (size_t i = 0, size = d_values.size(); i < size; i++)
- {
- Node v = d_values[i];
- double score = (1.0 + static_cast<double>(d_value_pro_con[0][v].size()))
- / (1.0 + static_cast<double>(d_value_pro_con[1][v].size()));
- Debug("fmf-model-cons-debug") << " - score( ";
- Debug("fmf-model-cons-debug") << m->getRepresentative(v);
- Debug("fmf-model-cons-debug") << " ) = " << score << std::endl;
- if (score > maxScore)
- {
- defaultVal = v;
- maxScore = score;
- }
- }
- 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 = defaultTerm.getType();
- Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values);
- if (!newDefaultVal.isNull())
- {
- defaultVal = newDefaultVal;
- Debug("fmf-model-cons-debug") << "-> Change default value to ";
- Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
- Debug("fmf-model-cons-debug") << std::endl;
- }
- else
- {
- Debug("fmf-model-cons-debug")
- << "-> Could not find arbitrary element of type "
- << tn[tn.getNumChildren() - 1] << std::endl;
- Debug("fmf-model-cons-debug") << " Excluding: " << d_values;
- Debug("fmf-model-cons-debug") << std::endl;
- }
- }
- // get the default term (this term must be defined non-ground in model)
- Debug("fmf-model-cons-debug") << " Choose ";
- Debug("fmf-model-cons-debug") << m->getRepresentative(defaultVal);
- Debug("fmf-model-cons-debug")
- << " as default value (" << defaultTerm << ")" << std::endl;
- Debug("fmf-model-cons-debug")
- << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size()
- << std::endl;
- Debug("fmf-model-cons-debug")
- << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size()
- << std::endl;
- return defaultVal;
-}
-
-QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe)
- : QModelBuilder(c, qe),
- d_didInstGen(false),
- d_numQuantSat(0),
- d_numQuantInstGen(0),
- d_numQuantNoInstGen(0),
- d_numQuantNoSelForm(0),
- d_instGenMatches(0) {}
-
-/*
-Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
- return n;
-}
-*/
-
-bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
- if (!m->areFunctionValuesEnabled())
- {
- // nothing to do if no functions
- return true;
- }
- FirstOrderModel* f = (FirstOrderModel*)m;
- FirstOrderModelIG* fm = f->asFirstOrderModelIG();
- Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
- d_didInstGen = false;
- //reset the internal information
- reset( fm );
- //only construct first order model if optUseModel() is true
- if( optUseModel() ){
- Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
- //check if any quantifiers are un-initialized
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i );
- if( d_qe->getModel()->isQuantifierActive( q ) ){
- int lems = initializeQuantifier(q, q, f);
- d_statistics.d_init_inst_gen_lemmas += lems;
- d_addedLemmas += lems;
- if( d_qe->inConflict() ){
- break;
- }
- }
- }
- if( d_addedLemmas>0 ){
- Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
- return false;
- }else{
- Assert( !d_qe->inConflict() );
- //initialize model
- fm->initialize();
- //analyze the functions
- Trace("model-engine-debug") << "Analyzing model..." << std::endl;
- analyzeModel( fm );
- //analyze the quantifiers
- Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
- d_uf_prefs.clear();
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i );
- analyzeQuantifier( fm, q );
- }
-
- //if applicable, find exceptions to model via inst-gen
- if( options::fmfInstGen() ){
- d_didInstGen = true;
- d_instGenMatches = 0;
- d_numQuantSat = 0;
- d_numQuantInstGen = 0;
- d_numQuantNoInstGen = 0;
- d_numQuantNoSelForm = 0;
- //now, see if we know that any exceptions via InstGen exist
- Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- if( d_qe->getModel()->isQuantifierActive( f ) ){
- int lems = doInstGen( fm, f );
- d_statistics.d_inst_gen_lemmas += lems;
- d_addedLemmas += lems;
- //temporary
- if( lems>0 ){
- d_numQuantInstGen++;
- }else if( hasInstGen( f ) ){
- d_numQuantNoInstGen++;
- }else{
- d_numQuantNoSelForm++;
- }
- if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
- break;
- }
- }else{
- d_numQuantSat++;
- }
- }
- Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
- Trace("model-engine-debug") << d_numQuantNoInstGen << " / " << d_numQuantNoSelForm << std::endl;
- Trace("model-engine-debug") << "Inst-gen # matches examined = " << d_instGenMatches << std::endl;
- if( Trace.isOn("model-engine") ){
- if( d_addedLemmas>0 ){
- Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
- }else{
- Trace("model-engine") << "No InstGen lemmas..." << std::endl;
- }
- }
- }
- //construct the model if necessary
- 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
- Trace("model-engine-debug") << "Building model..." << std::endl;
- //build model for UF
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
- constructModelUf( fm, it->first );
- }
- Trace("model-engine-debug") << "Done building models." << std::endl;
- }else{
- return false;
- }
- }
- }
- //update models
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- it->second.update( fm );
- Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
- //construct function values
- Node f_def = it->second.getFunctionValue( "$x" );
- fm->assignFunctionDefinition( it->first, f_def );
- }
- Assert( d_addedLemmas==0 );
- return TheoryEngineModelBuilder::processBuildModel( m );
-}
-
-int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm)
-{
- if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
- //create the basis match if necessary
- if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
- Trace("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;
- // }
- //}
- d_quant_basis_match[f] = InstMatch( f );
- for (unsigned j = 0; j < f[0].getNumChildren(); j++)
- {
- Node t = fm->getModelBasisTerm(f[0][j].getType());
- //calculate the basis match for f
- d_quant_basis_match[f].setValue( j, t );
- }
- ++(d_statistics.d_num_quants_init);
- }
- //try to add it
- Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl;
- //add model basis instantiation
- if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f]))
- {
- d_quant_basis_match_added[f] = true;
- return 1;
- }else{
- //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_quant_basis_match_added[f] = false;
- }
- }
- return 0;
-}
-
-void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
- FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
- d_uf_model_constructed.clear();
- //determine if any functions are constant
- for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){
- Node op = it->first;
- std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
- if( itut!=fmig->d_uf_terms.end() ){
- for( size_t i=0; i<itut->second.size(); i++ ){
- Node n = fmig->d_uf_terms[op][i];
- //for calculating if op is constant
- Node v = fmig->getRepresentative( n );
- if( i==0 ){
- d_uf_prefs[op].d_const_val = v;
- }else if( v!=d_uf_prefs[op].d_const_val ){
- d_uf_prefs[op].d_const_val = Node::null();
- break;
- }
- }
- }
- if( !d_uf_prefs[op].d_const_val.isNull() ){
- fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val );
- fmig->d_uf_model_gen[op].makeModel( fmig, it->second );
- Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
- Debug("fmf-model-cons") << d_uf_prefs[op].d_const_val;
- Debug("fmf-model-cons") << std::endl;
- d_uf_model_constructed[op] = true;
- }else{
- d_uf_model_constructed[op] = false;
- }
- }
-}
-
-bool QModelBuilderIG::hasConstantDefinition( Node n ){
- Node lit = n.getKind()==NOT ? n[0] : n;
- if( lit.getKind()==APPLY_UF ){
- Node op = lit.getOperator();
- if( !d_uf_prefs[op].d_const_val.isNull() ){
- return true;
- }
- }
- return false;
-}
-
-QModelBuilderIG::Statistics::Statistics()
- : d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
- d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers",
- 0),
- d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0),
- d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_num_quants_init);
- smtStatisticsRegistry()->registerStat(&d_num_partial_quants_init);
- smtStatisticsRegistry()->registerStat(&d_init_inst_gen_lemmas);
- smtStatisticsRegistry()->registerStat(&d_inst_gen_lemmas);
-}
-
-QModelBuilderIG::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_num_quants_init);
- smtStatisticsRegistry()->unregisterStat(&d_num_partial_quants_init);
- smtStatisticsRegistry()->unregisterStat(&d_init_inst_gen_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_inst_gen_lemmas);
-}
-
-//do exhaustive instantiation
-int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
- if( optUseModel() ){
- QRepBoundExt qrbe(d_qe);
- RepSetIterator riter(d_qe->getModel()->getRepSet(), &qrbe);
- if( riter.setQuantifier( f ) ){
- FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
- Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
- fmig->resetEvaluate();
- Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
- EqualityQuery* qy = d_qe->getEqualityQuery();
- Instantiate* inst = d_qe->getInstantiate();
- TermUtil* util = d_qe->getTermUtil();
- while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
- d_triedLemmas++;
- if( Debug.isOn("inst-fmf-ei-debug") ){
- for( int i=0; i<(int)riter.d_index.size(); i++ ){
- Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl;
- }
- }
- int eval = 0;
- int depIndex;
- //see if instantiation is already true in current model
- if( Debug.isOn("fmf-model-eval") ){
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
- }
- //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
- depIndex = riter.getNumTerms()-1;
- Debug("fmf-model-eval") << "We will evaluate "
- << util->getInstConstantBody(f) << std::endl;
- eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter);
- if( eval==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- }else{
- Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
- }
- if( eval==1 ){
- //instantiation is already true -> skip
- riter.incrementAtIndex(depIndex);
- }else{
- //instantiation was not shown to be true, construct the match
- InstMatch m( f );
- for (unsigned i = 0; i < riter.getNumTerms(); i++)
- {
- m.set(qy, i, riter.getCurrentTerm(i));
- }
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- //add as instantiation
- if (inst->addInstantiation(f, m, true))
- {
- d_addedLemmas++;
- if( d_qe->inConflict() ){
- break;
- }
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 ){
- riter.incrementAtIndex(depIndex);
- }else{
- riter.increment();
- }
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
- riter.increment();
- }
- }
- }
- //print debugging information
- Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl;
- Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl;
- Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl;
- if( d_addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
- }
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- return riter.isIncomplete() ? -1 : 1;
- }else{
- return 0;
- }
-}
-
-
-
-void QModelBuilderDefault::reset( FirstOrderModel* fm ){
- d_quant_selection_lit.clear();
- d_quant_selection_lit_candidates.clear();
- d_quant_selection_lit_terms.clear();
- d_term_selection_lit.clear();
- d_op_selection_terms.clear();
-}
-
-
-int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
- /*
- size_t maxChildren = 0;
- for( size_t i=0; i<uf_terms.size(); i++ ){
- if( uf_terms[i].getNumChildren()>maxChildren ){
- maxChildren = uf_terms[i].getNumChildren();
- }
- }
- //TODO: look at how many entries they have?
- return (int)maxChildren;
- */
- return 0;
-}
-
-void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
- if( d_qe->getModel()->isQuantifierActive( f ) ){
- FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
- Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
- //the pro/con preferences for this quantifier
- std::vector< Node > pro_con[2];
- //the terms in the selection literal we choose
- std::vector< Node > selectionLitTerms;
- Trace("inst-gen-debug-quant") << "Inst-gen analyze " << f << std::endl;
- //for each asserted quantifier f,
- // - determine selection literals
- // - check which function/predicates have good and bad definitions for satisfying f
- if( d_phase_reqs.find( f )==d_phase_reqs.end() ){
- d_phase_reqs[f].initialize( d_qe->getTermUtil()->getInstConstantBody( f ), true );
- }
- int selectLitScore = -1;
- for( std::map< Node, bool >::iterator it = d_phase_reqs[f].d_phase_reqs.begin(); it != d_phase_reqs[f].d_phase_reqs.end(); ++it ){
- //the literal n is phase-required for quantifier f
- Node n = it->first;
- Node gn = fm->getModelBasis(f, n);
- Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
- bool value;
- //if the corresponding ground abstraction literal has a SAT value
- if( d_qe->getValuation().hasSatValue( gn, value ) ){
- //collect the non-ground uf terms that this literal contains
- // and compute if all of the symbols in this literal have
- // constant definitions.
- bool isConst = true;
- std::vector< Node > uf_terms;
- if( TermUtil::hasInstConstAttr(n) ){
- isConst = false;
- if( gn.getKind()==APPLY_UF ){
- uf_terms.push_back( gn );
- isConst = hasConstantDefinition( gn );
- }else if( gn.getKind()==EQUAL ){
- isConst = true;
- for( int j=0; j<2; j++ ){
- if( TermUtil::hasInstConstAttr(n[j]) ){
- if( n[j].getKind()==APPLY_UF &&
- fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){
- uf_terms.push_back( gn[j] );
- isConst = isConst && hasConstantDefinition( gn[j] );
- }else{
- isConst = false;
- }
- }
- }
- }
- }
- //check if the value in the SAT solver matches the preference according to the quantifier
- int pref = 0;
- if( value!=it->second ){
- //we have a possible selection literal
- bool selectLit = d_quant_selection_lit[f].isNull();
- bool selectLitConstraints = true;
- //it is a constantly defined selection literal : the quantifier is sat
- if( isConst ){
- selectLit = selectLit || d_qe->getModel()->isQuantifierActive( f );
- d_qe->getModel()->setQuantifierActive( f, false );
- //check if choosing this literal would add any additional constraints to default definitions
- selectLitConstraints = false;
- selectLit = true;
- }
- //also check if it is naturally a better literal
- if( !selectLit ){
- int score = getSelectionScore( uf_terms );
- //Trace("inst-gen-debug") << "Check " << score << " < " << selectLitScore << std::endl;
- selectLit = score<selectLitScore;
- }
- //see if we wish to choose this as a selection literal
- d_quant_selection_lit_candidates[f].push_back( value ? n : n.notNode() );
- if( selectLit ){
- selectLitScore = getSelectionScore( uf_terms );
- Trace("inst-gen-debug") << "Choose selection literal " << gn << std::endl;
- Trace("inst-gen-debug") << " flags: " << isConst << " " << selectLitConstraints << " " << selectLitScore << std::endl;
- d_quant_selection_lit[f] = value ? n : n.notNode();
- selectionLitTerms.clear();
- selectionLitTerms.insert( selectionLitTerms.begin(), uf_terms.begin(), uf_terms.end() );
- if( !selectLitConstraints ){
- break;
- }
- }
- pref = 1;
- }else{
- pref = -1;
- }
- //if we are not yet SAT, so we will add to preferences
- if( d_qe->getModel()->isQuantifierActive( f ) ){
- Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
- Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- pro_con[ pref==1 ? 0 : 1 ].push_back( uf_terms[j] );
- }
- }
- }
- }
- //process information about selection literal for f
- if( !d_quant_selection_lit[f].isNull() ){
- d_quant_selection_lit_terms[f].insert( d_quant_selection_lit_terms[f].begin(), selectionLitTerms.begin(), selectionLitTerms.end() );
- for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
- d_term_selection_lit[ selectionLitTerms[i] ] = d_quant_selection_lit[f];
- d_op_selection_terms[ selectionLitTerms[i].getOperator() ].push_back( selectionLitTerms[i] );
- }
- }else{
- Trace("inst-gen-warn") << "WARNING: " << f << " has no selection literals" << std::endl;
- }
- //process information about requirements and preferences of quantifier f
- if( !d_qe->getModel()->isQuantifierActive( f ) ){
- Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
- for( int i=0; i<(int)selectionLitTerms.size(); i++ ){
- Debug("fmf-model-prefs") << selectionLitTerms[i] << " ";
- }
- Debug("fmf-model-prefs") << std::endl;
- }else{
- //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 = fmig->getRepresentative( pro_con[k][j] );
- d_uf_prefs[op].setValuePreference(f, r, k == 0);
- }
- }
- }
- }
-}
-
-int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
- int addedLemmas = 0;
- //we wish to add all known exceptions to our selection literal for f. 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.
- if( !d_quant_selection_lit[f].isNull() ){
- Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl;
- for( size_t i=0; i<d_quant_selection_lit_candidates[f].size(); i++ ){
- bool phase = d_quant_selection_lit_candidates[f][i].getKind()!=NOT;
- Node lit = d_quant_selection_lit_candidates[f][i].getKind()==NOT ? d_quant_selection_lit_candidates[f][i][0] : d_quant_selection_lit_candidates[f][i];
- Assert( TermUtil::hasInstConstAttr(lit) );
- 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(
- EQUAL, lit, NodeManager::currentNM()->mkConst(!phase));
- tr_terms.push_back( eq );
- }else if( lit.getKind()==EQUAL ){
- //collect trigger terms
- for( int j=0; j<2; j++ ){
- if( TermUtil::hasInstConstAttr(lit[j]) ){
- if( lit[j].getKind()==APPLY_UF ){
- tr_terms.push_back( lit[j] );
- }else{
- tr_terms.clear();
- 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 applicable, try to add exceptions here
- if( !tr_terms.empty() ){
- //make a trigger for these terms, add instantiations
- inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms, true, inst::Trigger::TR_MAKE_NEW );
- //Notice() << "Trigger = " << (*tr) << std::endl;
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- //d_qe->d_optInstMakeRepresentative = false;
- //d_qe->d_optMatchIgnoreModelBasis = true;
- addedLemmas += tr->addInstantiations();
- }
- }
- }
- return addedLemmas;
-}
-
-void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
- FirstOrderModelIG* fmig = fm->asFirstOrderModelIG();
- if( !d_uf_model_constructed[op] ){
- //construct the model for the uninterpretted function/predicate
- bool setDefaultVal = true;
- Node defaultTerm = fmig->getModelBasisOpTerm(op);
- Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
- //set the values in the model
- std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op );
- if( itut!=fmig->d_uf_terms.end() ){
- for( size_t i=0; i<itut->second.size(); i++ ){
- Node n = itut->second[i];
- // only consider unique up to congruence (in model equality engine)?
- Node v = fmig->getRepresentative( n );
- Trace("fmf-model-cons") << "Set term " << n << " : "
- << fmig->getRepSet()->getIndexFor(v) << " " << v
- << std::endl;
- //if this assertion did not help the model, just consider it ground
- //set n = v in the model tree
- //set it as ground value
- fmig->d_uf_model_gen[op].setValue( fm, n, v );
- // also set as default value if necessary
- if (n.hasAttribute(ModelBasisArgAttribute())
- && n.getAttribute(ModelBasisArgAttribute()) != 0)
- {
- Trace("fmf-model-cons") << " Set as default." << std::endl;
- fmig->d_uf_model_gen[op].setValue(fm, n, v, false);
- if( n==defaultTerm ){
- //incidentally already set, we will not need to find a default value
- setDefaultVal = false;
- }
- }
- }
- }
- //set the overall default value if not set already (is this necessary??)
- if( setDefaultVal ){
- Trace("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 );
- if( defaultVal.isNull() ){
- if (!fmig->getRepSet()->hasType(defaultTerm.getType()))
- {
- Node mbt = fmig->getModelBasisTerm(defaultTerm.getType());
- fmig->getRepSetPtr()->d_type_reps[defaultTerm.getType()].push_back(
- mbt);
- }
- defaultVal =
- fmig->getRepSet()->getRepresentative(defaultTerm.getType(), 0);
- }
- Assert( !defaultVal.isNull() );
- Trace("fmf-model-cons")
- << "Set default term : " << fmig->getRepSet()->getIndexFor(defaultVal)
- << std::endl;
- fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
- }
- Debug("fmf-model-cons") << " Making model...";
- fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] );
- d_uf_model_constructed[op] = true;
- Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl;
- }
-}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback