Support E-matching/QCF for Set operators.

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 24f17d0c18acfecbce366ed38982eea4323348d3..731b53dc40a664d4123c5abc46330346fd1e344b 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -20,6 +20,7 @@
 #include "theory/theory_engine.h"\r
 #include "theory/quantifiers/options.h"\r
 #include "theory/quantifiers/term_database.h"\r
+#include "theory/quantifiers/trigger.h"\r
 \r
 using namespace CVC4;\r
 using namespace CVC4::kind;\r
@@ -1692,8 +1693,9 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 }\r
 \r
 bool MatchGen::isHandledUfTerm( TNode n ) {\r
-  return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||\r
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;\r
+  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||\r
+  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;\r
+  return inst::Trigger::isAtomicTriggerKind( n.getKind() );  \r
 }\r
 \r
 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 5636e0c5f93e9f774c17121af6ea3691bd1dbf12..9f25b08257b804b12b99f3570e67e3066ace4083 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -73,25 +73,21 @@ unsigned TermDb::getNumGroundTerms( Node f ) {
 
 Node TermDb::getOperator( Node n ) {
   //return n.getOperator();
-
-  if( n.getKind()==SELECT || n.getKind()==STORE ){
+  Kind k = n.getKind();
+  if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON ){
     //since it is parametric, use a particular one as op
-    TypeNode tn1 = n[0].getType();
-    TypeNode tn2 = n[1].getType();
+    TypeNode tn = n[0].getType();
     Node op = n.getOperator();
-    std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > >::iterator ito = d_par_op_map.find( op );
+    std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
     if( ito!=d_par_op_map.end() ){
-      std::map< TypeNode, std::map< TypeNode, Node > >::iterator it = ito->second.find( tn1 );
+      std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
       if( it!=ito->second.end() ){
-        std::map< TypeNode, Node >::iterator it2 = it->second.find( tn2 );
-        if( it2!=it->second.end() ){
-          return it2->second;
-        }
+        return it->second;
       }
     }
-    d_par_op_map[op][tn1][tn2] = n;
+    d_par_op_map[op][tn] = n;
     return n;
-  }else if( inst::Trigger::isAtomicTrigger( n ) ){
+  }else if( inst::Trigger::isAtomicTriggerKind( k ) ){
     return n.getOperator();
   }else{
     return Node::null();

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2592e1fd646d648f17bf79e903322a3d9eb636aa..e82fcd00d9327cb9a749ae3320aa465f14aea178 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -97,7 +97,7 @@ private:
   std::hash_set< Node, NodeHashFunction > d_processed;
 private:
   /** select op map */
-  std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map;
+  std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
   /** count number of ground terms per operator (user-context dependent) */
   NodeIntMap d_op_ccount;
 public:

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5802632da7c67c9cb9c6106d230c2390fa46a5f3..8335a084aa0265730484bc968d3da6ce60ca0275 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -109,10 +109,10 @@ void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
 void TheoryQuantifiers::check(Effort e) {
   CodeTimer codeTimer(d_theoryTime);
 
-  Debug("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
+  Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
   while(!done()) {
     Node assertion = get();
-    Debug("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
+    Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
     switch(assertion.getKind()) {
     case kind::FORALL:
       assertUniversal( assertion );

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 3de12b9c97e89e5324dce0cf5c04f89054bc989f..77a4efff5855128a26defdd8b65e6446f2a6f4e3 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -323,9 +323,16 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 }
 
 bool Trigger::isAtomicTrigger( Node n ){
-  return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
+  Kind k = n.getKind();
+  return ( k==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || 
+         ( k!=APPLY_UF && isAtomicTriggerKind( k ) );
 }
+bool Trigger::isAtomicTriggerKind( Kind k ) {
+  return k==APPLY_UF || k==SELECT || k==STORE ||
+         k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
+         k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SET_SINGLETON;
+}
+
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){
     for( int i=0; i<(int)n.getNumChildren(); i++ ){

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 74fc167644c6452c8728607920a7c6ba2cb1a730..9254105dd4990095a3588358a0669aa366003f34 100644 (file)
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -107,6 +107,7 @@ public:
   static bool isUsableTrigger( std::vector< Node >& nodes, Node f );
   static bool isUsableTrigger( Node n, Node f );
   static bool isAtomicTrigger( Node n );
+  static bool isAtomicTriggerKind( Kind k );
   static bool isSimpleTrigger( Node n );
   /** get pattern arithmetic */
   static bool isArithmeticTrigger( Node f, Node n, std::map< Node, Node >& coeffs );

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 3a5b61390167b10e40e1f3d5ce8eb31093645677..c230b9ac56e8b4c21f0a22769ddea07c7767e591 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,6 +34,10 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
+void TheorySets::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_internal->setMasterEqualityEngine(eq);
+}
+
 void TheorySets::addSharedTerm(TNode n) {
   d_internal->addSharedTerm(n);
 }

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 9f74064cb0d223d9d900ff4068d3affe1c60e4cf..6ff41d5f5092f8e5de96248c31c5824e0da73767 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -48,6 +48,8 @@ public:
 
   ~TheorySets();
 
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+  
   void addSharedTerm(TNode);
 
   void check(Effort);

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index af96b50d06c410254fb63b045117b4a0f65a7d24..8c9441483b87c72c6cb8e49ab24bb3cb5f360f67 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -880,6 +880,10 @@ bool TheorySetsPrivate::propagate(TNode literal) {
 }/* TheorySetsPropagate::propagate(TNode) */
 
 
+void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
+  d_equalityEngine.setMasterEqualityEngine(eq);
+}
+
 void TheorySetsPrivate::addSharedTerm(TNode n) {
   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 73c0c419e410214409895f900e08e9b39b513c3a..90dec7c0be1d7d79d64e28bb6591ed035c5a5558 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -47,6 +47,8 @@ public:
                     context::UserContext* u);
 
   ~TheorySetsPrivate();
+  
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
   void addSharedTerm(TNode);