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