diff options
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 387 |
1 files changed, 0 insertions, 387 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index f6392a0b2..53f55e70b 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -22,7 +22,6 @@ #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/inst_gen.h" #include "theory/quantifiers/trigger.h" #include "theory/quantifiers/options.h" @@ -754,389 +753,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ } - - -////////////////////// Inst-Gen style Model Builder /////////// - -void QModelBuilderInstGen::reset( FirstOrderModel* fm ){ - //for new inst gen - d_quant_selection_formula.clear(); - d_term_selected.clear(); - - //d_sub_quant_inst_trie.clear();//* -} - -int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){ - int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp ); - for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ - addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp ); - } - return addedLemmas; -} - -void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ - //Node fp = getParentQuantifier( f );//* - //bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ); - //if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//* - Trace("sel-form-debug") << "* Analyze " << f << std::endl; - //determine selection formula, set terms in selection formula as being selected - Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ), - d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); - //if( !s.isNull() ){ - // s = Rewriter::rewrite( s ); - //} - Trace("sel-form-debug") << "Selection formula " << f << std::endl; - Trace("sel-form-debug") << " " << s << std::endl; - if( !s.isNull() ){ - d_quant_selection_formula[f] = s; - Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); - setSelectedTerms( gs ); - //quick check if it is constant sat - if( hasConstantDefinition( s ) ){ - d_quant_sat[f] = true; - } - }else{ - Trace("sel-form-null") << "*** No selection formula for " << f << std::endl; - } - //analyze sub quantifiers - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ - analyzeQuantifier( fm, d_sub_quants[f][i] ); - } - } -} - - -int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ - int addedLemmas = 0; - if( d_quant_sat.find( f )==d_quant_sat.end() ){ - Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << "Do Inst-Gen for " << f << std::endl; - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << "Sel Form : " << d_quant_selection_formula[f] << std::endl; - //we wish to add all known exceptions to our selection formula for f. this will help to refine our current model. - if( !d_quant_selection_formula[f].isNull() ){ - //first, try on sub quantifiers - bool subQuantSat = true; - for( size_t i=0; i<d_sub_quants[f].size(); i++ ){ - addedLemmas += doInstGen( fm, d_sub_quants[f][i] ); - if( d_quant_sat.find( d_sub_quants[f][i] )==d_quant_sat.end() ){ - subQuantSat = false; - } - } - if( addedLemmas>0 || !subQuantSat ){ - Trace("inst-gen") << " -> children added lemmas or non-satisfied" << std::endl; - return addedLemmas; - }else{ - Trace("inst-gen-debug") << "Calculate inst-gen instantiations..." << std::endl; - //get all possible values of selection formula - InstGenProcess igp( d_quant_selection_formula[f] ); - std::vector< Node > considered; - considered.push_back( fm->d_false ); - igp.calculateMatches( d_qe, f, considered, true ); - //igp.calculateMatches( d_qe, f); - Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl; - for( int i=0; i<igp.getNumMatches(); i++ ){ - //if the match is not already true in the model - if( igp.getMatchValue( i )!=fm->d_true ){ - InstMatch m( f ); - igp.getMatch( d_qe->getEqualityQuery(), i, m ); - //Trace("inst-gen-debug") << "Inst Gen : " << m << std::endl; - //we only consider matches that are non-empty - // matches that are empty should trigger other instances that are non-empty - if( !m.empty() ){ - Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; - //translate to be in terms match in terms of fp - InstMatch mp(f); - getParentQuantifierMatch( mp, fp, m, f ); - //if this is a partial instantion - if( !m.isComplete() ){ - //need to make it internal here - //Trace("mkInternal") << "Make internal representative " << mp << std::endl; - //mp.makeInternalRepresentative( d_qe ); - //Trace("mkInternal") << "Got " << mp << std::endl; - //if the instantiation does not yet exist - if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ - //also add it to children - d_child_sub_quant_inst_trie[f].addInstMatch( d_qe, f, m ); - //get the partial instantiation pf - Node pf = d_qe->getInstantiation( fp, mp ); - Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; - Trace("inst-gen-pi") << " " << pf << std::endl; - d_sub_quants[ f ].push_back( pf ); - d_sub_quant_inst[ pf ] = InstMatch( &mp ); - d_sub_quant_parent[ pf ] = fp; - //now make mp a complete match - mp.add( d_quant_basis_match[ fp ] ); - d_quant_basis_match[ pf ] = InstMatch( &mp ); - ++(d_statistics.d_num_quants_init); - ++(d_statistics.d_num_partial_quants_init); - addedLemmas += initializeQuantifier( pf, fp ); - Trace("inst-gen-pi") << "Done adding partial instantiation" << std::endl; - subQuantSat = false; - } - }else{ - if( d_qe->addInstantiation( fp, mp ) ){ - addedLemmas++; - } - } - } - } - } - if( addedLemmas==0 ){ - //all sub quantifiers must be satisfied as well - if( subQuantSat ){ - d_quant_sat[ f ] = true; - } - } - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << " -> added lemmas = " << addedLemmas << std::endl; - if( d_quant_sat.find( f )!=d_quant_sat.end() ){ - if( fp!=f ) Trace("inst-gen") << " "; - Trace("inst-gen") << " -> *** it is satisfied" << std::endl; - } - } - } - } - return addedLemmas; -} - -Node mkAndSelectionFormula( std::vector< Node >& children ){ - std::vector< Node > ch; - for( size_t i=0; i<children.size(); i++ ){ - if( children[i].getKind()==AND ){ - for( size_t j=0; j<children[i].getNumChildren(); j++ ){ - ch.push_back( children[i][j] ); - } - }else{ - ch.push_back( children[i] ); - } - } - return NodeManager::currentNM()->mkNode( AND, ch ); -} -Node mkAndSelectionFormula( Node n1, Node n2 ){ - std::vector< Node > children; - children.push_back( n1 ); - children.push_back( n2 ); - return mkAndSelectionFormula( children ); -} - -//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context, -// and NULL otherwise -Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){ - Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl; - Node ret; - if( n.getKind()==NOT ){ - ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); - }else if( n.getKind()==OR || n.getKind()==AND ){ - //whether we only need to find one or all - bool favorPol = ( n.getKind()!=AND && polarity ) || ( n.getKind()==AND && !polarity ); - std::vector< Node > children; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node fnc = fn[i]; - Node nc = n[i]; - Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); - if( nn.isNull() && !favorPol ){ - //cannot make selection formula - children.clear(); - break; - } - if( !nn.isNull() ){ - //if( favorPol ){ //temporary - // return nn; // - //} // - if( std::find( children.begin(), children.end(), nn )==children.end() ){ - children.push_back( nn ); - } - } - } - if( !children.empty() ){ - if( favorPol ){ - //filter which formulas we wish to keep, make disjunction - Node min_lit; - int min_score = -1; - for( size_t i=0; i<children.size(); i++ ){ - //if it is constant apply uf application, return it for sure - if( hasConstantDefinition( children[i] ) ){ - min_lit = children[i]; - break; - }else{ - int score = getSelectionFormulaScore( children[i] ); - if( min_score<0 || score<min_score ){ - min_score = score; - min_lit = children[i]; - } - } - } - //currently just return the best single literal - ret = min_lit; - }else{ - //selection formula must be conjunction of children - ret = mkAndSelectionFormula( children ); - } - }else{ - ret = Node::null(); - } - }else if( n.getKind()==ITE ){ - Node nn; - Node nc[2]; - //get selection formula for the - for( int i=0; i<2; i++ ){ - nn = getSelectionFormula( fn[0], n[0], i==0, useOption ); - nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption ); - if( !nn.isNull() && !nc[i].isNull() ){ - ret = mkAndSelectionFormula( nn, nc[i] ); - break; - } - } - if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){ - ret = mkAndSelectionFormula( nc[0], nc[1] ); - } - }else if( n.getKind()==IFF ){ - bool opPol = !polarity; - for( int p=0; p<2; p++ ){ - Node nn[2]; - for( int i=0; i<2; i++ ){ - bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 ); - nn[i] = getSelectionFormula( fn[i], n[i], pol, useOption ); - if( nn[i].isNull() ){ - break; - } - } - if( !nn[0].isNull() && !nn[1].isNull() ){ - ret = mkAndSelectionFormula( nn[0], nn[1] ); - } - } - }else{ - //literal case - //first, check if it is a usable selection literal - if( isUsableSelectionLiteral( n, useOption ) ){ - bool value; - if( d_qe->getValuation().hasSatValue( n, value ) ){ - if( value==polarity ){ - ret = fn; - if( !polarity ){ - ret = ret.negate(); - } - }else{ - Trace("sel-form-debug") << " (wrong polarity)" << std::endl; - } - }else{ - Trace("sel-form-debug") << " (does not have sat value)" << std::endl; - } - }else{ - Trace("sel-form-debug") << " (is not usable literal)" << std::endl; - } - } - Trace("sel-form-debug") << " return " << ret << std::endl; - return ret; -} - -int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ - if( fn.getType().isBoolean() ){ - if( fn.getKind()==APPLY_UF ){ - Node op = fn.getOperator(); - //return total number of terms - return d_qe->getTermDatabase()->d_op_nonred_count[op]; - }else{ - int score = 0; - for( size_t i=0; i<fn.getNumChildren(); i++ ){ - score += getSelectionFormulaScore( fn[i] ); - } - return score; - } - }else{ - return 0; - } -} - -void QModelBuilderInstGen::setSelectedTerms( Node s ){ - - //if it is apply uf and has model basis arguments, then mark term as being "selected" - if( s.getKind()==APPLY_UF ){ - Assert( s.hasAttribute(ModelBasisArgAttribute()) ); - if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; - if( s.getAttribute(ModelBasisArgAttribute())!=0 ){ - d_term_selected[ s ] = true; - Trace("sel-form-term") << " " << s << " is a selected term." << std::endl; - } - } - for( int i=0; i<(int)s.getNumChildren(); i++ ){ - setSelectedTerms( s[i] ); - } -} - -bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){ - if( n.getKind()==FORALL ){ - return false; - }else if( n.getKind()!=APPLY_UF ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - //if it is a variable, then return false - if( n[i].getAttribute(ModelBasisAttribute()) ){ - return false; - } - } - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( !isUsableSelectionLiteral( n[i], useOption ) ){ - return false; - } - } - return true; -} - -void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ - if( f!=fp ){ - //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl; - //std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl; - int counter = 0; - for( size_t i=0; i<fp[0].getNumChildren(); i++ ){ - if( (int)counter< (int)f[0].getNumChildren() ){ - if( fp[0][i]==f[0][counter] ){ - Node n = m.get( counter ); - if( !n.isNull() ){ - mp.set( d_qe, i, n ); - } - counter++; - } - } - } - mp.add( d_sub_quant_inst[f] ); - }else{ - mp.add( m ); - } -} - -void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ - FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - bool setDefaultVal = true; - Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); - //set the values in the model - for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ - Node n = fmig->d_uf_terms[op][i]; - if( isTermActive( n ) ){ - Node v = fmig->getRepresentative( n ); - fmig->d_uf_model_gen[op].setValue( fm, n, v ); - } - //also possible set as default - if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){ - Node v = fmig->getRepresentative( n ); - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); - if( n==defaultTerm ){ - setDefaultVal = false; - } - } - } - //set the overall default value if not set already (is this necessary??) - if( setDefaultVal ){ - Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); - } - fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); - d_uf_model_constructed[op] = true; -} - -bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ - return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true ); -} |