From 37593fa07954e74d52e7100aade64091f3ae74ae Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Nov 2017 13:35:28 -0600 Subject: [PATCH] Improve trigger filter instances (#1402) --- src/theory/quantifiers/term_util.cpp | 110 --------------- src/theory/quantifiers/term_util.h | 10 +- src/theory/quantifiers/trigger.cpp | 196 ++++++++++++++++++++++++--- src/theory/quantifiers/trigger.h | 41 +++++- 4 files changed, 216 insertions(+), 141 deletions(-) diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index def9a68bc..bccf6829c 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -317,116 +317,6 @@ void TermUtil::getVarContainsNode( Node f, Node n, std::vector< Node >& varConta } } -int TermUtil::isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ){ - if( n1==n2 ){ - return 1; - }else if( n1.getKind()==n2.getKind() ){ - if( n1.getKind()==APPLY_UF ){ - if( n1.getOperator()==n2.getOperator() ){ - int result = 0; - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( n1[i]!=n2[i] ){ - int cResult = isInstanceOf2( n1[i], n2[i], varContains1, varContains2 ); - if( cResult==0 ){ - return 0; - }else if( cResult!=result ){ - if( result!=0 ){ - return 0; - }else{ - result = cResult; - } - } - } - } - return result; - } - } - return 0; - }else if( n2.getKind()==INST_CONSTANT ){ - //if( std::find( d_var_contains[ n1 ].begin(), d_var_contains[ n1 ].end(), n2 )!=d_var_contains[ n1 ].end() ){ - // return 1; - //} - if( varContains1.size()==1 && varContains1[ 0 ]==n2 ){ - return 1; - } - }else if( n1.getKind()==INST_CONSTANT ){ - //if( std::find( d_var_contains[ n2 ].begin(), d_var_contains[ n2 ].end(), n1 )!=d_var_contains[ n2 ].end() ){ - // return -1; - //} - if( varContains2.size()==1 && varContains2[ 0 ]==n1 ){ - return 1; - } - } - return 0; -} - -int TermUtil::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 TermUtil::isUnifiableInstanceOf( Node n1, Node n2, std::map< Node, Node >& subs ){ - if( n1==n2 ){ - return true; - }else if( n2.getKind()==INST_CONSTANT ){ - //if( !node_contains( n1, n2 ) ){ - // return false; - //} - if( subs.find( n2 )==subs.end() ){ - subs[n2] = n1; - }else if( subs[n2]!=n1 ){ - return false; - } - return true; - }else if( n1.getKind()==n2.getKind() && n1.getMetaKind()==kind::metakind::PARAMETERIZED ){ - if( n1.getOperator()!=n2.getOperator() ){ - return false; - } - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( !isUnifiableInstanceOf( n1[i], n2[i], subs ) ){ - return false; - } - } - return true; - }else{ - return false; - } -} - -void TermUtil::filterInstances( std::vector< Node >& nodes ){ - std::vector< bool > active; - active.resize( nodes.size(), true ); - std::map< int, std::vector< Node > > varContains; - for( unsigned i=0; i temp; - for( unsigned i=0; i::iterator it = d_op_id.find( op ); if( it==d_op_id.end() ){ diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index ed6cd018f..83d9d7940 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -179,17 +179,9 @@ public: //quantified simplify (treat free variables in n as quantified and run rewriter) static Node getQuantSimplify( Node n ); -//for triggers -private: + private: /** helper function for compute var contains */ static void computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ); - /** helper for is instance of */ - static 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 */ - static int isInstanceOf2( Node n1, Node n2, std::vector< Node >& varContains1, std::vector< Node >& varContains2 ); - /** -1: n1 is an instance of n2, 1: n1 is an instance of n2 */ - static int isInstanceOf(Node n1, Node n2); - public: /** compute var contains */ static void computeVarContains( Node n, std::vector< Node >& varContains ); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index d06b5268b..ce306541f 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -42,6 +42,7 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ }else{ //determined a ground (dis)equality must hold or else q is a tautology? } + d_weight = Trigger::getTriggerWeight(n); } /** trigger class constructor */ @@ -220,7 +221,8 @@ Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& } // check if higher-order - Trace("trigger") << "Collect higher-order variable triggers..." << std::endl; + Trace("trigger-debug") << "Collect higher-order variable triggers..." + << std::endl; std::map > ho_apps; HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps); Trace("trigger") << "...got " << ho_apps.size() @@ -490,9 +492,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod tinfo.erase( added2[i] ); }else{ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){ - //discard if we added a subterm as a trigger with all variables that nu has - Trace("auto-gen-trigger-debug2") << "......subsumes parent." << std::endl; - rm_nu = true; + if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight) + { + // discard if we added a subterm as a trigger with all + // variables that nu has + Trace("auto-gen-trigger-debug2") + << "......subsumes parent " << tinfo[nu].d_weight << " " + << tinfo[added2[i]].d_weight << "." << std::endl; + rm_nu = true; + } } if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){ added.push_back( added2[i] ); @@ -550,8 +558,13 @@ bool Trigger::isPureTheoryTrigger( Node n ) { } int Trigger::getTriggerWeight( Node n ) { - if( isAtomicTrigger( n ) ){ + if (n.getKind() == APPLY_UF) + { return 0; + } + else if (isAtomicTrigger(n)) + { + return 1; }else{ if( options::relationalTriggers() ){ if( isRelationalTrigger( n ) ){ @@ -562,7 +575,7 @@ int Trigger::getTriggerWeight( Node n ) { } } } - return 1; + return 2; } } @@ -608,18 +621,25 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false ); std::vector< Node > temp; temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() ); - quantifiers::TermUtil::filterInstances( temp ); - if( temp.size()!=patTerms2.size() ){ - Trace("trigger-filter-instance") << "Filtered an instance: " << std::endl; - Trace("trigger-filter-instance") << "Old: "; - for( unsigned i=0; i& patTerms, qu } } +int Trigger::isTriggerInstanceOf(Node n1, + Node n2, + std::vector& fv1, + std::vector& fv2) +{ + Assert(n1 != n2); + int status = 0; + std::unordered_set subs_vars; + std::unordered_set, + PairHashFunction > + visited; + std::vector > visit; + std::pair cur; + TNode cur1; + TNode cur2; + visit.push_back(std::pair(n1, n2)); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + cur1 = cur.first; + cur2 = cur.second; + Assert(cur1 != cur2); + // recurse if they have the same operator + if (cur1.hasOperator() && cur2.hasOperator() + && cur1.getNumChildren() == cur2.getNumChildren() + && cur1.getOperator() == cur2.getOperator() + && cur1.getOperator().getKind()!=INST_CONSTANT) + { + visit.push_back(std::pair(cur1, cur2)); + for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++) + { + if (cur1[i] != cur2[i]) + { + visit.push_back(std::pair(cur1[i], cur2[i])); + } + else if (cur1[i].getKind() == INST_CONSTANT) + { + if (subs_vars.find(cur1[i]) != subs_vars.end()) + { + return 0; + } + // the variable must map to itself in the substitution + subs_vars.insert(cur1[i]); + } + } + } + else + { + bool success = false; + // check if we are in a unifiable instance case + // must be only this case + for (unsigned r = 0; r < 2; r++) + { + if (status == 0 || ((status == 1) == (r == 0))) + { + TNode curi = r == 0 ? cur1 : cur2; + if (curi.getKind() == INST_CONSTANT + && subs_vars.find(curi) == subs_vars.end()) + { + TNode curj = r == 0 ? cur2 : cur1; + // RHS must be a simple trigger + if (getTriggerWeight(curj) == 0) + { + // must occur in the free variables in the other + std::vector& free_vars = r == 0 ? fv2 : fv1; + if (std::find(free_vars.begin(), free_vars.end(), curi) + != free_vars.end()) + { + status = r == 0 ? 1 : -1; + subs_vars.insert(curi); + success = true; + break; + } + } + } + } + } + if (!success) + { + return 0; + } + } + } + } while (!visit.empty()); + return status; +} + +void Trigger::filterTriggerInstances(std::vector& nodes) +{ + std::map > fvs; + for (unsigned i = 0, size = nodes.size(); i < size; i++) + { + quantifiers::TermUtil::computeVarContains(nodes[i], fvs[i]); + } + std::vector active; + active.resize(nodes.size(), true); + for (unsigned i = 0, size = nodes.size(); i < size; i++) + { + std::vector& fvsi = fvs[i]; + if (active[i]) + { + for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++) + { + if (active[j]) + { + int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]); + if (result == 1) + { + Trace("filter-instances") << nodes[j] << " is an instance of " + << nodes[i] << std::endl; + active[i] = false; + break; + } + else if (result == -1) + { + Trace("filter-instances") << nodes[i] << " is an instance of " + << nodes[j] << std::endl; + active[j] = false; + } + } + } + } + } + std::vector temp; + for (unsigned i = 0; i < nodes.size(); i++) + { + if (active[i]) + { + temp.push_back(nodes[i]); + } + } + nodes.clear(); + nodes.insert(nodes.begin(), temp.begin(), temp.end()); +} + Node Trigger::getInversionVariable( Node n ) { if( n.getKind()==INST_CONSTANT ){ return n; diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 105878df1..2beafb984 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -55,16 +55,16 @@ class InstMatchGenerator; * This example is referenced for each of the functions below. */ class TriggerTermInfo { -public: - TriggerTermInfo() : d_reqPol(0){} - ~TriggerTermInfo(){} + public: + TriggerTermInfo() : d_reqPol(0), d_weight(0) {} + ~TriggerTermInfo() {} /** The free variables in the node * * In the trigger term info for f( x ) in the above example, d_fv = { x } * In the trigger term info for g( y ) in the above example, d_fv = { y } * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z } */ - std::vector< Node > d_fv; + std::vector d_fv; /** Required polarity: 1 for equality, -1 for disequality, 0 for none * * In the trigger term info for f( x ) in the above example, d_reqPol = -1 @@ -89,12 +89,14 @@ public: * d_reqPolEq = false */ Node d_reqPolEq; + /** the weight of the trigger (see Trigger::getTriggerWeight). */ + int d_weight; /** Initialize this information class (can be called more than once). * q is the quantified formula that n is a trigger term for * n is the trigger term * reqPol/reqPolEq are described above */ - void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() ); + void init(Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null()); }; /** A collection of nodes representing a trigger. @@ -280,6 +282,7 @@ class Trigger { static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, bool filterInst = false ); + /** Is n a usable trigger in quantified formula q? * * A usable trigger is one that is matchable and contains free variables only @@ -393,6 +396,34 @@ class Trigger { quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false ); + /** filter all nodes that have trigger instances + * + * This is used during collectModelInfo to filter certain trigger terms, + * stored in nodes. This updates nodes so that no pairs of distinct nodes + * (i,j) is such that i is a trigger instance of j or vice versa (see below). + */ + static void filterTriggerInstances(std::vector& nodes); + + /** is instance of + * + * We say a term t is an trigger instance of term s if + * (1) t = s * { x1 -> t1 ... xn -> tn } + * (2) { x1, ..., xn } are a subset of FV( t ). + * For example, f( g( h( x, x ) ) ) and f( g( x ) ) are instances of f( x ), + * but f( g( y ) ) and g( x ) are not instances of f( x ). + * + * When this method returns -1, n1 is an instance of n2, + * When this method returns 1, n1 is an instance of n2. + * + * The motivation for this method is to discard triggers s that are less + * restrictive (criteria (1)) and serve to bind the same variables (criteria + * (2)) as another trigger t. This often helps avoiding matching loops. + */ + static int isTriggerInstanceOf(Node n1, + Node n2, + std::vector& fv1, + std::vector& fv2); + /** add an instantiation (called by InstMatchGenerator) * * This calls Instantiate::addInstantiation(...) for instantiations -- 2.30.2