From 7c798a5a2085754b26a0720d162b2ee45a705c4e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sun, 16 Aug 2015 12:44:11 +0200 Subject: [PATCH] More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds. --- src/smt/smt_engine.cpp | 6 +- src/theory/quantifiers/macros.cpp | 233 ++++++++++-------- src/theory/quantifiers/macros.h | 16 +- src/theory/quantifiers/modes.h | 2 + src/theory/quantifiers/options | 4 +- src/theory/quantifiers/options_handlers.h | 5 + src/theory/quantifiers/term_database.cpp | 108 ++++---- src/theory/quantifiers/term_database.h | 18 +- src/theory/quantifiers/trigger.cpp | 55 +++-- src/theory/quantifiers/trigger.h | 4 +- .../regress0/push-pop/quant-fun-proc.smt2 | 2 +- 11 files changed, 235 insertions(+), 218 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 87cd815e9..192485dcc 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1427,6 +1427,10 @@ void SmtEngine::setDefaults() { if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); } + //do not do macros + if( !options::macrosQuant.wasSetByUser()) { + options::macrosQuant.set( false ); + } } //cbqi options @@ -3309,7 +3313,7 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-skolem-quant", d_assertions); if( options::macrosQuant() ){ //quantifiers macro expansion - quantifiers::QuantifierMacros qm; + quantifiers::QuantifierMacros qm( d_smt.d_theoryEngine->getQuantifiersEngine() ); bool success; do{ success = qm.simplify( d_assertions.ref(), true ); diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index c26aea465..163005806 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -22,6 +22,8 @@ #include "smt/smt_engine_scope.h" #include "theory/quantifiers/modes.h" #include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" using namespace CVC4; using namespace std; @@ -31,26 +33,14 @@ using namespace CVC4::kind; bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ - unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_GROUND ? 1 : 2; + unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; for( unsigned r=0; r simp_assertions; - int last_macro = -1; for( int i=0; i<(int)assertions.size(); i++ ){ Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; - Node curr = assertions[i]; - //do simplification before process - if( doRewrite && !d_macro_defs_new.empty() ){ - curr = simplify( assertions[i] ); - curr = Rewriter::rewrite( curr ); - if( curr!=assertions[i] ){ - simp_assertions[i] = curr; - } - } - if( processAssertion( curr ) ){ - last_macro = i; + if( processAssertion( assertions[i] ) ){ //process this assertion again i--; } @@ -61,15 +51,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite Trace("macros") << "Do simplifications..." << std::endl; //now, rewrite based on macro definitions for( unsigned i=0; i::iterator it = simp_assertions.find( i ); - if( it!=simp_assertions.end() ){ - curr = it->second; - } - //simplify again if before last macro - if( (int)i& assertions, bool doRewrite } } } - for( int i=0; i<(int)assertions.size(); i++ ){ - if( Trace.isOn("macros-warn") ){ + if( Trace.isOn("macros-warn") ){ + for( int i=0; i<(int)assertions.size(); i++ ){ debugMacroDefinition( assertions[i], assertions[i] ); } } @@ -99,47 +81,45 @@ bool QuantifierMacros::processAssertion( Node n ) { return true; } } - return false; - }else if( n.getKind()==FORALL ){ + }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){ std::vector< Node > args; for( size_t j=0; j& opc, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + Node nop = n.getOperator(); + if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ return true; } - } - return false; - } -} - -bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc ){ - if( n.getKind()==APPLY_UF ){ - Node nop = n.getOperator(); - if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ + if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ + opc.push_back( nop ); + } + }else if( d_ground_macros && n.getKind()==FORALL ){ return true; } - if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ - opc.push_back( nop ); - } - }else if( d_ground_macros && n.getKind()==FORALL ){ - return true; - } - for( size_t i=0; igetTermDatabase()->getInstConstantNode( n, f ); + Trace("macros-debug2") << "Get free variables in " << icn << std::endl; + std::vector< Node > var; + d_qe->getTermDatabase()->getVarContainsNode( f, icn, var ); + Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; + std::vector< Node > trigger_var; + inst::Trigger::getTriggerVariables( d_qe, icn, f, trigger_var ); + Trace("macros-debug2") << "Done." << std::endl; + //only if all variables are also trigger variables + return trigger_var.size()>=var.size(); +} + bool QuantifierMacros::isBoundVarApplyUf( Node n ) { Assert( n.getKind()==APPLY_UF ); TypeNode tn = n.getOperator().getType(); @@ -168,22 +161,25 @@ bool QuantifierMacros::isBoundVarApplyUf( Node n ) { return true; } -void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates ){ - if( n.getKind()==APPLY_UF ){ - if( isBoundVarApplyUf( n ) ){ - candidates.push_back( n ); - } - }else if( n.getKind()==PLUS ){ - for( size_t i=0; i& candidates, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + if( isBoundVarApplyUf( n ) ){ + candidates.push_back( n ); + } + }else if( n.getKind()==PLUS ){ + for( size_t i=0; i& v_quant, std::vector< Node >& vars, bool retOnly ){ - if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ - if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ - if( retOnly ){ - return true; - }else{ - vars.push_back( n ); +bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ + if( retOnly ){ + return true; + }else{ + vars.push_back( n ); + } } } - } - for( size_t i=0; i& args, Nod }else{ //literal case if( isMacroLiteral( n, pol ) ){ + std::map< Node, bool > visited; std::vector< Node > candidates; for( size_t i=0; i fvs; - getFreeVariables( m, args, fvs, false ); + visited.clear(); + getFreeVariables( m, args, fvs, false, visited ); //get definition and condition Node n_def = solveInEquality( m, n ); //definition for the macro - //definition must exist and not contain any free variables apart from fvs, opc is list of functions it contains - std::vector< Node > opc; - if( !n_def.isNull() && !getFreeVariables( n_def, args, fvs, true ) && !containsBadOp( n_def, op, opc ) ){ - Node n_cond; //condition when this definition holds - //conditional must not contain any free variables apart from fvs - if( n_cond.isNull() || !getFreeVariables( n_cond, args, fvs, true ) ){ - Trace("macros-debug") << m << " is possible macro in " << f << std::endl; - //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where - // x1 ... xn are distinct variables - if( d_macro_basis[op].empty() ){ - for( size_t a=0; amkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); - d_macro_basis[op].push_back( v ); + if( !n_def.isNull() ){ + Trace("macros-debug") << m << " is possible macro in " << f << std::endl; + Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl; + visited.clear(); + //definition must exist and not contain any free variables apart from fvs + if( !getFreeVariables( n_def, args, fvs, true, visited ) ){ + Trace("macros-debug") << "...free variables are contained." << std::endl; + visited.clear(); + //cannot contain a defined operator, opc is list of functions it contains + std::vector< Node > opc; + if( !containsBadOp( n_def, op, opc, visited ) ){ + Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; + //must be ground UF term if mode is GROUND_UF + if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){ + Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; + //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where + // x1 ... xn are distinct variables + if( d_macro_basis[op].empty() ){ + for( size_t a=0; amkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + } + std::map< Node, Node > solved; + for( size_t a=0; a vars; + std::vector< Node > subs; + if( getSubstitution( fvs, solved, vars, subs, true ) ){ + n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + addMacro( op, n_def, opc ); + return true; + } } } - std::map< Node, Node > solved; - for( size_t a=0; a vars; - std::vector< Node > subs; - if( getSubstitution( fvs, solved, vars, subs, true ) ){ - n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - addMacro( op, n_def, opc ); - return true; - } } } } @@ -416,7 +427,11 @@ void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) { } void QuantifierMacros::finalizeDefinitions() { - if( options::incrementalSolving() || options::produceModels() || Trace.isOn("macros-warn") ){ + bool doDefs = false; + if( Trace.isOn("macros-warn") ){ + doDefs = true; + } + if( options::incrementalSolving() || options::produceModels() || doDefs ){ Trace("macros") << "Store as defined functions..." << std::endl; //also store as defined functions for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ diff --git a/src/theory/quantifiers/macros.h b/src/theory/quantifiers/macros.h index 74fb0f47b..06e2d652a 100644 --- a/src/theory/quantifiers/macros.h +++ b/src/theory/quantifiers/macros.h @@ -23,23 +23,26 @@ #include #include "expr/node.h" #include "expr/type_node.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { class QuantifierMacros{ +private: + QuantifiersEngine * d_qe; private: bool d_ground_macros; bool processAssertion( Node n ); bool isBoundVarApplyUf( Node n ); bool process( Node n, bool pol, std::vector< Node >& args, Node f ); - bool contains( Node n, Node n_s ); - bool containsBadOp( Node n, Node op, std::vector< Node >& opc ); + bool containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ); bool isMacroLiteral( Node n, bool pol ); - void getMacroCandidates( Node n, std::vector< Node >& candidates ); + bool isGroundUfTerm( Node f, Node n ); + void getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ); Node solveInEquality( Node n, Node lit ); - bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly ); + bool getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ); bool getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ); //map from operators to macro basis terms @@ -49,14 +52,15 @@ private: std::map< Node, Node > d_macro_defs_new; //operators to macro ops that contain them std::map< Node, std::vector< Node > > d_macro_def_contains; - //simplify cache + //simplify caches std::map< Node, Node > d_simplify_cache; + std::map< Node, bool > d_quant_macros; private: Node simplify( Node n ); void addMacro( Node op, Node n, std::vector< Node >& opc ); void debugMacroDefinition( Node oo, Node n ); public: - QuantifierMacros(){} + QuantifierMacros( QuantifiersEngine * qe ) : d_qe( qe ){} ~QuantifierMacros(){} bool simplify( std::vector< Node >& assertions, bool doRewrite = false ); diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 75e75637f..94ba7daaf 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -166,6 +166,8 @@ typedef enum { MACROS_QUANT_MODE_ALL, /** infer ground definitions */ MACROS_QUANT_MODE_GROUND, + /** infer ground uf definitions */ + MACROS_QUANT_MODE_GROUND_UF, } MacrosQuantMode; }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 0edd3f1ea..48a9fdea2 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -260,9 +260,9 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas -option macrosQuant --macros-quant bool :default false +option macrosQuant --macros-quant bool :read-write :default false perform quantifiers macro expansion -option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h" +option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h" mode for quantifiers macro expansion ### recursive function options diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 699dd0296..791ad6e90 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -239,6 +239,9 @@ all \n\ ground (default) \n\ + Only infer ground definitions for functions.\n\ \n\ +ground-uf \n\ ++ Only infer ground definitions for functions that result in triggers for all free variables.\n\ +\n\ "; inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { @@ -487,6 +490,8 @@ inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string o return MACROS_QUANT_MODE_ALL; } else if(optarg == "ground") { return MACROS_QUANT_MODE_GROUND; + } else if(optarg == "ground-uf") { + return MACROS_QUANT_MODE_GROUND_UF; } else if(optarg == "help") { puts(macrosQuantHelp.c_str()); exit(1); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 7616e770a..7973abcc6 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -753,7 +753,6 @@ int TermDb::getNumInstantiationConstants( Node f ) const { Node TermDb::getInstConstantBody( Node f ){ std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); if( it==d_inst_const_body.end() ){ - makeInstantiationConstantsFor( f ); Node n = getInstConstantNode( f[1], f ); d_inst_const_body[ f ] = n; return n; @@ -783,15 +782,9 @@ Node TermDb::getCounterexampleLiteral( Node f ){ } Node TermDb::getInstConstantNode( Node n, Node f ){ - Assert( d_inst_constants.find( f )!=d_inst_constants.end() ); - return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); -} - -Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & vars, - const std::vector & inst_constants){ - Node n2 = n.substitute( vars.begin(), vars.end(), - inst_constants.begin(), - inst_constants.end() ); + makeInstantiationConstantsFor( f ); + Node n2 = n.substitute( d_vars[f].begin(), d_vars[f].end(), + d_inst_constants[f].begin(), d_inst_constants[f].end() ); return n2; } @@ -1001,66 +994,47 @@ Node TermDb::getFreeVariableForType( TypeNode tn ) { return d_free_vars[tn]; } -void TermDb::computeVarContains( Node n ) { - if( d_var_contains.find( n )==d_var_contains.end() ){ - d_var_contains[n].clear(); - computeVarContains2( n, n ); - } +void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, varContains, visited ); } -void TermDb::computeVarContains2( Node n, Node parent ){ - if( n.getKind()==INST_CONSTANT ){ - if( std::find( d_var_contains[parent].begin(), d_var_contains[parent].end(), n )==d_var_contains[parent].end() ){ - d_var_contains[parent].push_back( n ); - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeVarContains2( n[i], parent ); - } - } -} - -bool TermDb::isVariableSubsume( Node n1, Node n2 ){ - if( n1==n2 ){ - return true; - }else{ - //Notice() << "is variable subsume ? " << n1 << " " << n2 << std::endl; - computeVarContains( n1 ); - computeVarContains( n2 ); - for( int i=0; i<(int)d_var_contains[n2].size(); i++ ){ - if( std::find( d_var_contains[n1].begin(), d_var_contains[n1].end(), d_var_contains[n2][i] )==d_var_contains[n1].end() ){ - //Notice() << "no" << std::endl; - return false; +void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==INST_CONSTANT ){ + if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ + varContains.push_back( n ); + } + }else{ + for( unsigned i=0; i& pats, std::map< Node, std::vector< Node > >& varContains ){ - for( int i=0; i<(int)pats.size(); i++ ){ - computeVarContains( pats[i] ); + for( unsigned i=0; i& varContains ){ - computeVarContains( n ); - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ - if( d_var_contains[n][j].getAttribute(InstConstantAttribute())==f ){ - varContains.push_back( d_var_contains[n][j] ); + std::vector< Node > vars; + computeVarContains( n, vars ); + for( unsigned j=0; j& varContains1, std::vector< Node >& varContains2 ){ if( n1==n2 ){ return 1; }else if( n1.getKind()==n2.getKind() ){ @@ -1069,7 +1043,7 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){ int result = 0; for( int i=0; i<(int)n1.getNumChildren(); i++ ){ if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf( n1[i], n2[i] ); + int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 ); if( cResult==0 ){ return 0; }else if( cResult!=result ){ @@ -1086,25 +1060,31 @@ int TermDb::isInstanceOf( Node n1, Node n2 ){ } return 0; }else if( n2.getKind()==INST_CONSTANT ){ - computeVarContains( n1 ); //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ // return 1; //} - if( d_var_contains[ n1 ].size()==1 && d_var_contains[ n1 ][ 0 ]==n2 ){ + if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){ return 1; } }else if( n1.getKind()==INST_CONSTANT ){ - computeVarContains( n2 ); //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ // return -1; //} - if( d_var_contains[ n2 ].size()==1 && d_var_contains[ n2 ][ 0 ]==n1 ){ + if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){ return 1; } } return 0; } +int TermDb::isInstanceOf( Node n1, Node n2 ){ + std::vector< Node > varContains1; + std::vector< Node > varContains2; + computeVarContains( n1, varContains1 ); + computeVarContains( n1, varContains2 ); + return isInstanceOf2( n1, n2, varContains1, varContains2 ); +} + bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ if( n1==n2 ){ return true; @@ -1136,10 +1116,14 @@ bool TermDb::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& su void TermDb::filterInstances( std::vector< Node >& nodes ){ std::vector< bool > active; active.resize( nodes.size(), true ); - for( int i=0; i<(int)nodes.size(); i++ ){ - for( int j=i+1; j<(int)nodes.size(); j++ ){ + std::map< int, std::vector< Node > > varContains; + for( unsigned i=0; i& nodes ){ } } std::vector< Node > temp; - for( int i=0; i<(int)nodes.size(); i++ ){ + for( unsigned i=0; i & vars, - const std::vector & nvars); static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); @@ -306,18 +298,16 @@ public: //for triggers private: /** helper function for compute var contains */ - void computeVarContains2( Node n, Node parent ); - /** var contains */ - std::map< TNode, std::vector< TNode > > d_var_contains; + void computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ); /** triggers for each operator */ std::map< Node, std::vector< inst::Trigger* > > d_op_triggers; /** helper for is instance of */ bool isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ); + /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ + int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); public: /** compute var contains */ - void computeVarContains( Node n ); - /** variables subsume, return true if n1 contains all free variables in n2 */ - bool isVariableSubsume( Node n1, Node n2 ); + void computeVarContains( Node n, std::vector< Node >& varContains ); /** get var contains for each of the patterns in pats */ void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index e4d9a2730..0085177cc 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -121,23 +121,23 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& std::map< Node, bool > vars; std::map< Node, std::vector< Node > > patterns; size_t varCount = 0; - for( int i=0; i<(int)temp.size(); i++ ){ + std::map< Node, std::vector< Node > > varContains; + qe->getTermDatabase()->getVarContains( f, temp, varContains ); + for( unsigned i=0; igetTermDatabase()->computeVarContains( temp[i] ); - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; - if( quantifiers::TermDb::getInstConstAttr(v)==f ){ - if( vars.find( v )==vars.end() ){ - varCount++; - vars[ v ] = true; - foundVar = true; - } + for( unsigned j=0; jgetTermDatabase()->d_var_contains[ temp[i] ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ temp[i] ][j]; + for( unsigned j=0; j& return NULL; }else{ //now, minimize the trigger - for( int i=0; i<(int)trNodes.size(); i++ ){ + for( unsigned i=0; igetTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; + for( unsigned j=0; j& } if( !keepPattern ){ //remove from pattern vector - for( int j=0; j<(int)qe->getTermDatabase()->d_var_contains[ n ].size(); j++ ){ - Node v = qe->getTermDatabase()->d_var_contains[ n ][j]; - for( int k=0; k<(int)patterns[v].size(); k++ ){ + for( unsigned j=0; j& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ +bool Trigger::collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ){ if( patMap.find( n )==patMap.end() ){ patMap[ n ] = false; bool newHasPol = n.getKind()==IFF ? false : hasPol; @@ -347,7 +347,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< bool retVal = false; for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ + if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } @@ -383,7 +383,7 @@ bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< if( n.getKind()!=FORALL ){ for( int i=0; i<(int)n.getNumChildren(); i++ ){ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol; - if( collectPatTerms2( qe, f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ + if( collectPatTerms2( f, n[i], patMap, tstrt, exclude, newPol, newHasPol2 ) ){ retVal = true; } } @@ -491,7 +491,7 @@ void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vecto } } } - collectPatTerms2( qe, f, n, patMap, tstrt, exclude, true, true ); + collectPatTerms2( f, n, patMap, tstrt, exclude, true, true ); for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){ if( it->second ){ patTerms.push_back( it->first ); @@ -568,6 +568,17 @@ Node Trigger::getInversion( Node n, Node x ) { return Node::null(); } +void Trigger::getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ) { + std::vector< Node > patTerms; + //collect all patterns from icn + std::vector< Node > exclude; + collectPatTerms( qe, f, icn, patTerms, TS_ALL, exclude ); + //collect all variables from all patterns in patTerms, add to t_vars + for( unsigned i=0; igetTermDatabase()->getVarContainsNode( f, patTerms[i], t_vars ); + } +} + InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) { if( n.getKind()==INST_CONSTANT ){ return NULL; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 60e268a4f..f601a02ab 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -94,7 +94,7 @@ private: static bool isUsable( Node n, Node f ); static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false ); /** collect all APPLY_UF pattern terms for f in n */ - static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); + static bool collectPatTerms2( Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol ); public: //different strategies for choosing trigger terms enum { @@ -116,6 +116,8 @@ public: static InstMatchGenerator* getInstMatchGenerator( Node q, Node n ); static Node getInversionVariable( Node n ); static Node getInversion( Node n, Node x ); + /** get all variables that E-matching can possibly handle */ + static void getTriggerVariables( QuantifiersEngine* qe, Node icn, Node f, std::vector< Node >& t_vars ); inline void toStream(std::ostream& out) const { /* diff --git a/test/regress/regress0/push-pop/quant-fun-proc.smt2 b/test/regress/regress0/push-pop/quant-fun-proc.smt2 index 8f4758df6..2a12cb677 100644 --- a/test/regress/regress0/push-pop/quant-fun-proc.smt2 +++ b/test/regress/regress0/push-pop/quant-fun-proc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --fmf-fun --macros-quant --no-check-models +; COMMAND-LINE: --incremental --fmf-fun --macros-quant --macros-quant-mode=ground --no-check-models (set-logic UFLIA) (define-fun f ((x Int)) Int x) -- 2.30.2