From: Andrew Reynolds Date: Wed, 17 Oct 2012 02:59:07 +0000 (+0000) Subject: first working version of new inst-gen-style quantifier instantiation technique for... X-Git-Tag: cvc5-1.0.0~7698 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f10c78f572debd0ddf717bfb9f9453a42c015cb;p=cvc5.git first working version of new inst-gen-style quantifier instantiation technique for fmf (--fmf-new-inst-gen), minor cleanup --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fa619c653..3813f964d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1154,8 +1154,6 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect }else{ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); - NoMatchAttribute nma; - op.setAttribute(nma,true); std::vector< Node > funcArgs; funcArgs.push_back( op ); funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() ); diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index ea58840f5..099e3aa29 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -45,10 +45,11 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){ if( !qe->existsInstantiation( f, m, true ) ){ - //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ + //make sure no duplicates are produced + if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); - //} + } } } @@ -110,6 +111,8 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){ calculateMatchesInterpreted( qe, f, curr, terms, 0 ); } Trace("cm") << "done calculate matches" << std::endl; + //can clear information used for finding duplicates + d_inst_trie.clear(); } bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 3d1ca8f0d..e0ab047ab 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -538,7 +538,12 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ) //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 ); - Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl; + //if( !s.isNull() ){ + // s = Rewriter::rewrite( s ); + //} + d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f ); + Trace("sel-form") << "Selection formula " << f << std::endl; + Trace("sel-form") << " " << s << std::endl; if( !s.isNull() ){ d_quant_selection_formula[f] = s; Node gs = d_qe->getTermDatabase()->getModelBasis( f, s ); @@ -566,7 +571,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ //get all possible values of selection formula InstGenProcess igp( d_quant_selection_formula[f] ); igp.calculateMatches( d_qe, f ); - Trace("inst-gen-debug") << "Add inst-gen instantiations..." << std::endl; + Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl; for( int i=0; id_true ){ @@ -576,13 +581,13 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ // matches that are empty should trigger other instances that are non-empty if( !m.empty() ){ bool addInst = false; + Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl; //translate to be in terms match in terms of fp InstMatch mp; getParentQuantifierMatch( mp, fp, m, f ); //if this is a partial instantion if( !m.isComplete( f ) ){ - Trace("inst-gen-debug") << "- partial inst" << std::endl; //if the instantiation does not yet exist if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ //get the partial instantiation pf @@ -599,7 +604,6 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ addInst = true; } if( addInst ){ - Trace("inst-gen-debug") << "- complete inst" << std::endl; //otherwise, get instantiation and add ground instantiation in terms of root parent if( d_qe->addInstantiation( fp, mp ) ){ addedLemmas++; @@ -631,43 +635,48 @@ bool ModelEngineBuilderInstGen::shouldSetDefaultValue( Node n ){ return d_term_selected.find( n )!=d_term_selected.end(); } -//if possible, returns a formula n' such that ( n' <=> polarity ) => ( n <=> polarity ), and ( n' <=> polarity ) is true in the current context, +//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context, // and NULL otherwise Node ModelEngineBuilderInstGen::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 ){ - Node nn = getSelectionFormula( fn[0], n[0], !polarity, useOption ); - if( !nn.isNull() ){ - return nn.negate(); - } + ret = getSelectionFormula( fn[0], n[0], !polarity, useOption ); }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){ //whether we only need to find one or all bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity ); std::vector< Node > children; + bool retSet = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i]; Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i]; Node nn = getSelectionFormula( fnc, nc, polarity, useOption ); if( nn.isNull()!=posPol ){ //TODO: may want to weaken selection formula - return nn; + ret = nn; + retSet = true; + break; + } + if( std::find( children.begin(), children.end(), nn )==children.end() ){ + children.push_back( nn ); } - children.push_back( nn ); } - if( !posPol ){ - return NodeManager::currentNM()->mkNode( n.getKind()==AND ? AND : OR, children ); + if( !retSet && !posPol ){ + ret = NodeManager::currentNM()->mkNode( AND, children ); } }else if( n.getKind()==ITE ){ Node nn; Node nc[2]; //get selection formula for the for( int i=0; i<2; i++ ){ - nn = getSelectionFormula( i==0 ? fn[0] : fn[0].negate(), i==0 ? n[0] : n[0].negate(), true, useOption ); + 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() ){ - return NodeManager::currentNM()->mkNode( AND, nn, nc[i] ); + ret = NodeManager::currentNM()->mkNode( AND, nn, nc[i] ); + break; } } - if( !nc[0].isNull() && !nc[1].isNull() ){ - return NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] ); + if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){ + ret = NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] ); } }else if( n.getKind()==IFF || n.getKind()==XOR ){ bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF; @@ -675,13 +684,13 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar Node nn[2]; for( int i=0; i<2; i++ ){ bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 ); - nn[i] = getSelectionFormula( pol ? fn[i] : fn[i].negate(), pol ? n[i] : n[i].negate(), true, useOption ); + nn[i] = getSelectionFormula( fn[i], n[i], pol, useOption ); if( nn[i].isNull() ){ break; } } if( !nn[0].isNull() && !nn[1].isNull() ){ - return NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] ); + ret = NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] ); } } }else{ @@ -691,12 +700,16 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar bool value; if( d_qe->getValuation().hasSatValue( n, value ) ){ if( value==polarity ){ - return fn; + ret = fn; + if( !polarity ){ + ret = ret.negate(); + } } } } } - return Node::null(); + Trace("sel-form-debug") << " return " << ret << std::endl; + return ret; } void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ @@ -707,7 +720,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){ if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl; if( s.getAttribute(ModelBasisArgAttribute())==1 ){ d_term_selected[ s ] = true; - Trace("sel-form") << " " << s << " is a selected term." << std::endl; + Trace("sel-form-term") << " " << s << " is a selected term." << std::endl; } } for( int i=0; i<(int)s.getNumChildren(); i++ ){ @@ -744,18 +757,26 @@ Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){ } void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){ - int counter = 0; - for( size_t i=0; igetTermDatabase()->getInstantiationConstant( fp, i ); - if( fp[0][i]==f[0][counter] ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter ); - Node n = m.getValue( ic ); - if( !n.isNull() ){ - mp.setMatch( d_qe->getEqualityQuery(), icp, n ); + 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; igetTermDatabase()->getInstantiationConstant( fp, i ); + if( countergetTermDatabase()->getInstantiationConstant( f, counter ); + Node n = m.getValue( ic ); + if( !n.isNull() ){ + mp.setMatch( d_qe->getEqualityQuery(), icp, n ); + } + counter++; + } } - counter++; } + mp.add( d_sub_quant_inst[f] ); + }else{ + mp.add( m ); } - mp.add( d_sub_quant_inst[f] ); } diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index ba5c5c884..312261d3c 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -57,7 +57,7 @@ predicate\n\ "; static const std::string axiomInstModeHelp = "\ -Literal match modes currently supported by the --axiom-inst option:\n\ +Axiom instantiation modes currently supported by the --axiom-inst option:\n\ \n\ default \n\ + Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c8c884974..3b2778061 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -216,7 +216,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){ Node mbt; - if( d_type_map[ tn ].empty() || options::fmfNewInstGen() ){ + if( d_type_map[ tn ].empty() ){ std::stringstream ss; ss << Expr::setlanguage(options::outputLanguage()); ss << "e_" << tn; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d63eebf7e..bcd6b833d 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -144,8 +144,6 @@ private: std::map< Node, Node > d_inst_constants_map; /** make instantiation constants for */ void makeInstantiationConstantsFor( Node f ); - /** set instantiation constant attr */ - void setInstantiationConstantAttr( Node n, Node f ); public: /** get the i^th instantiation constant of f */ Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } @@ -174,6 +172,8 @@ public: Node getInstConstantIffTerm( Node n, bool pol ); /** make node, validating the inst constant attribute */ Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ); + /** set instantiation constant attr */ + void setInstantiationConstantAttr( Node n, Node f ); //for skolem private: diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9d7c8e315..4ba5c39e6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -97,17 +97,17 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_hasAddedLemma = false; if( e==Theory::EFFORT_LAST_CALL ){ + //if effort is last call, try to minimize model first + if( options::finiteModelFind() ){ + //first, check if we can minimize the model further + if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ + return; + } + } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); } - //if effort is last call, try to minimize model first - if( e==Theory::EFFORT_LAST_CALL && options::finiteModelFind() ){ - //first, check if we can minimize the model further - if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; - } - } for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->check( e ); }