summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/term_util.cpp110
-rw-r--r--src/theory/quantifiers/term_util.h10
-rw-r--r--src/theory/quantifiers/trigger.cpp196
-rw-r--r--src/theory/quantifiers/trigger.h41
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<nodes.size(); i++ ){
- computeVarContains( nodes[i], varContains[i] );
- }
- for( unsigned i=0; i<nodes.size(); i++ ){
- for( unsigned j=i+1; j<nodes.size(); j++ ){
- if( active[i] && active[j] ){
- int result = isInstanceOf2( nodes[i], nodes[j], varContains[i], varContains[j] );
- if( result==1 ){
- Trace("filter-instances") << nodes[j] << " is an instance of " << nodes[i] << std::endl;
- active[j] = false;
- }else if( result==-1 ){
- Trace("filter-instances") << nodes[i] << " is an instance of " << nodes[j] << std::endl;
- active[i] = false;
- }
- }
- }
- }
- std::vector< Node > 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() );
-}
-
int TermUtil::getIdForOperator( Node op ) {
std::map< Node, int >::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<Node, std::vector<Node> > 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<patTerms2.size(); i++ ){
- Trace("trigger-filter-instance") << patTerms2[i] << " ";
- }
- Trace("trigger-filter-instance") << std::endl << "New: ";
- for( unsigned i=0; i<temp.size(); i++ ){
- Trace("trigger-filter-instance") << temp[i] << " ";
+ filterTriggerInstances(temp);
+ if (Trace.isOn("trigger-filter-instance"))
+ {
+ if (temp.size() != patTerms2.size())
+ {
+ Trace("trigger-filter-instance") << "Filtered an instance: "
+ << std::endl;
+ Trace("trigger-filter-instance") << "Old: ";
+ for (unsigned i = 0; i < patTerms2.size(); i++)
+ {
+ Trace("trigger-filter-instance") << patTerms2[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl << "New: ";
+ for (unsigned i = 0; i < temp.size(); i++)
+ {
+ Trace("trigger-filter-instance") << temp[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl;
}
- Trace("trigger-filter-instance") << std::endl;
}
if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
for( unsigned i=0; i<temp.size(); i++ ){
@@ -646,6 +666,148 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
}
}
+int Trigger::isTriggerInstanceOf(Node n1,
+ Node n2,
+ std::vector<Node>& fv1,
+ std::vector<Node>& fv2)
+{
+ Assert(n1 != n2);
+ int status = 0;
+ std::unordered_set<TNode, TNodeHashFunction> subs_vars;
+ std::unordered_set<std::pair<TNode, TNode>,
+ PairHashFunction<TNode,
+ TNode,
+ TNodeHashFunction,
+ TNodeHashFunction> >
+ visited;
+ std::vector<std::pair<TNode, TNode> > visit;
+ std::pair<TNode, TNode> cur;
+ TNode cur1;
+ TNode cur2;
+ visit.push_back(std::pair<TNode, TNode>(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<TNode, TNode>(cur1, cur2));
+ for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
+ {
+ if (cur1[i] != cur2[i])
+ {
+ visit.push_back(std::pair<TNode, TNode>(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<Node>& 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<Node>& nodes)
+{
+ std::map<unsigned, std::vector<Node> > fvs;
+ for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ {
+ quantifiers::TermUtil::computeVarContains(nodes[i], fvs[i]);
+ }
+ std::vector<bool> active;
+ active.resize(nodes.size(), true);
+ for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ {
+ std::vector<Node>& 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<Node> 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<Node> 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<Node>& 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<Node>& fv1,
+ std::vector<Node>& fv2);
+
/** add an instantiation (called by InstMatchGenerator)
*
* This calls Instantiate::addInstantiation(...) for instantiations
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback