added rules for join and transpose operators

added more benchmarks

4 files changed, 186 insertions, 39 deletions

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9d3f7e08e..5e328b4fd 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1111,7 +1111,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
   d_rels(NULL)
 {
   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
-  d_rels = new TheorySetsRels(c, u, &d_equalityEngine);
+  d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict);
 
   d_equalityEngine.addFunctionKind(kind::UNION);
   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 24a69bfdb..fcab5b5ca 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -35,10 +35,12 @@ namespace sets {
 
   TheorySetsRels::TheorySetsRels(context::Context* c,
                                  context::UserContext* u,
-                                 eq::EqualityEngine* eq):
+                                 eq::EqualityEngine* eq,
+                                 context::CDO<bool>* conflict):
     d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
     d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
     d_eqEngine(eq),
+    d_conflict(conflict),
     d_relsSaver(c)
   {
     d_eqEngine->addFunctionKind(kind::PRODUCT);
@@ -59,10 +61,8 @@ namespace sets {
 
     while( !eqcs_i.isFinished() ){
       TNode r = (*eqcs_i);
-      bool firstTime = true;
-      Debug("rels-eqc") << "  " << r;
-      Debug("rels-eqc") << " : { ";
       eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine );
+
       while( !eqc_i.isFinished() ){
         TNode n = (*eqc_i);
 
@@ -70,53 +70,186 @@ namespace sets {
         if((d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode)
               || d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_falseNode))
             && !d_relsSaver.contains(n)) {
-          d_relsSaver.insert(n);
 
-          // case: (b, a) IS_IN (TRANSPOSE X)
-          //    => (a, b) IS_IN X
+          // case: [NOT] (b, a) IS_IN (TRANSPOSE X)
+          //    => [NOT] (a, b) IS_IN X
           if(n.getKind() == kind::MEMBER) {
+            d_relsSaver.insert(n);
             if(kind::TRANSPOSE == n[1].getKind()) {
               Node reversedTuple = reverseTuple(n[0]);
               Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, reversedTuple, n[1][0]);
-//              assertMembership(fact, n, r == d_trueNode);
+              Node exp = n;
+              if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_falseNode)) {
+                fact = fact.negate();
+                exp = n.negate();
+              }
+              d_pending_facts[fact] = exp;
             } else if(kind::JOIN == n[1].getKind()) {
-
+              TNode r1 = n[1][0];
+              TNode r2 = n[1][1];
+              // Need to do this efficiently... Join relations after collecting all of them
+              // So that we would just need to iterate over EE once
+              joinRelations(r1, r2, n[1].getType().getSetElementType());
+
+              // case: (a, b) IS_IN (X JOIN Y)
+              //      => (a, z) IS_IN X  && (z, b) IS_IN Y
+              if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode)) {
+                Debug("rels-join") << "Join rules (a, b) IS_IN (X JOIN Y) => ((a, z) IS_IN X  && (z, b) IS_IN Y)"<< std::endl;
+                Assert((r1.getType().getSetElementType()).isDatatype());
+                Assert((r2.getType().getSetElementType()).isDatatype());
+
+                unsigned int i = 0;
+                std::vector<Node> r1_tuple;
+                std::vector<Node> r2_tuple;
+                Node::iterator child_it = n[0].begin();
+                unsigned int s1_len = r1.getType().getSetElementType().getTupleLength();
+                Node shared_x = NodeManager::currentNM()->mkSkolem("sde_", r2.getType().getSetElementType().getTupleTypes()[0]);
+                Datatype dt = r1.getType().getSetElementType().getDatatype();
+
+                r1_tuple.push_back(Node::fromExpr(dt[0].getConstructor()));
+                for(; i < s1_len-1; ++child_it) {
+                  r1_tuple.push_back(*child_it);
+                  ++i;
+                }
+                r1_tuple.push_back(shared_x);
+                dt = r2.getType().getSetElementType().getDatatype();
+                r2_tuple.push_back(Node::fromExpr(dt[0].getConstructor()));
+                r2_tuple.push_back(shared_x);
+                for(; child_it != n[0].end(); ++child_it) {
+                  r2_tuple.push_back(*child_it);
+                }
+                Node t1 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r1_tuple);
+                Node t2 = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, r2_tuple);
+                Node f1 = NodeManager::currentNM()->mkNode(kind::MEMBER, t1, r1);
+                Node f2 = NodeManager::currentNM()->mkNode(kind::MEMBER, t2, r2);
+                d_pending_facts[f1] = n;
+                d_pending_facts[f2] = n;
+              }
             }else if(kind::PRODUCT == n[1].getKind()) {
 
             }
           }
         }
+        ++eqc_i;
+      }
+      ++eqcs_i;
+    }
+    doPendingFacts();
+  }
 
-        if( r!=n ){
-          if( firstTime ){
-            Debug("rels-eqc") << std::endl;
-            firstTime = false;
-          }
-          if (n.getKind() == kind::PRODUCT ||
-              n.getKind() == kind::JOIN ||
-              n.getKind() == kind::TRANSCLOSURE ||
-              n.getKind() == kind::TRANSPOSE) {
-            Debug("rels-eqc") << "    *** " << n << std::endl;
-          }else{
-            Debug("rels-eqc") << "    " << n <<std::endl;
+  // Join all explicitly specified tuples in r1, r2
+  // e.g. If (a, b) in X and (b, c) in Y, (a, c) in (X JOIN Y)
+  void TheorySetsRels::joinRelations(TNode r1, TNode r2, TypeNode tn) {
+    if (!d_eqEngine->consistent())
+          return;
+    Debug("rels-join") << "start joining tuples in "
+                       << r1 << " and " << r2 << std::endl;
+
+    std::vector<Node> r1_elements;
+    std::vector<Node> r2_elements;
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine );
+
+    // collect all tuples that are in r1, r2
+    while( !eqcs_i.isFinished() ){
+      TNode r = (*eqcs_i);
+      eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine );
+      while( !eqc_i.isFinished() ){
+        TNode n = (*eqc_i);
+        if(d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode)
+            && n.getKind() == kind::MEMBER && n[0].getType().isTuple()) {
+          if(n[1] == r1) {
+            Debug("rels-join") << "r1 tuple: " << n[0] << std::endl;
+            r1_elements.push_back(n[0]);
+          } else if (n[1] == r2) {
+            Debug("rels-join") << "r2 tuple: " << n[0] << std::endl;
+            r2_elements.push_back(n[0]);
           }
         }
         ++eqc_i;
       }
-      if( !firstTime ){ Debug("rels-eqc") << "  "; }
-      Debug("rels-eqc") << "}" << std::endl;
       ++eqcs_i;
     }
+    if(r1_elements.size() == 0 || r2_elements.size() == 0)
+      return;
+
+    // Join r1 and r2
+    joinTuples(r1, r2, r1_elements, r2_elements, tn);
+
   }
 
+  void TheorySetsRels::joinTuples(TNode r1, TNode r2, std::vector<Node>& r1_elements, std::vector<Node>& r2_elements, TypeNode tn) {
+    Datatype dt = tn.getDatatype();
+    unsigned int t1_len = r1_elements.front().getType().getTupleLength();
+    unsigned int t2_len = r2_elements.front().getType().getTupleLength();
+
+    for(unsigned int i = 0; i < r1_elements.size(); i++) {
+      for(unsigned int j = 0; j < r2_elements.size(); j++) {
+        if(r1_elements[i][t1_len-1] == r2_elements[j][0]) {
+          std::vector<Node> joinedTuple;
+          joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor()));
+          for(unsigned int k = 0; k < t1_len - 1; ++k) {
+            joinedTuple.push_back(r1_elements[i][k]);
+          }
+          for(unsigned int l = 1; l < t2_len; ++l) {
+            joinedTuple.push_back(r2_elements[j][l]);
+          }
+          Node fact = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, joinedTuple);
+          fact = NodeManager::currentNM()->mkNode(kind::MEMBER, fact, NodeManager::currentNM()->mkNode(kind::JOIN, r1, r2));
+          Node reason = NodeManager::currentNM()->mkNode(kind::AND,
+                                                         NodeManager::currentNM()->mkNode(kind::MEMBER, r1_elements[i], r1),
+                                                         NodeManager::currentNM()->mkNode(kind::MEMBER, r2_elements[j], r2));
+          Debug("rels-join") << "join tuples: " << r1_elements[i]
+                             << " and " << r2_elements[j]
+                             << "\nnew fact: " << fact
+                             << "\nreason: " << reason<< std::endl;
+          d_pending_facts[fact] = reason;
+        }
+      }
+    }
+  }
+
+
+  void TheorySetsRels::sendLemma(TNode fact, TNode reason, bool polarity) {
+
+  }
+
+  void TheorySetsRels::doPendingFacts() {
+    std::map<Node, Node>::iterator map_it = d_pending_facts.begin();
+    while( !(*d_conflict) && map_it != d_pending_facts.end()) {
+
+      Node fact = map_it->first;
+      Node exp = d_pending_facts[ fact ];
+      Debug("rels") << "sending out pending fact: " << fact
+                    << "  reason: " << exp
+                    << std::endl;
+      if(fact.getKind() == kind::AND) {
+        for(size_t j=0; j<fact.getNumChildren(); j++) {
+          bool polarity = fact[j].getKind() != kind::NOT;
+          TNode atom = polarity ? fact[j] : fact[j][0];
+          assertMembership(atom, exp, polarity);
+        }
+      } else {
+        bool polarity = fact.getKind() != kind::NOT;
+        TNode atom = polarity ? fact : fact[0];
+        assertMembership(atom, exp, polarity);
+      }
+      map_it++;
+    }
+    d_pending_facts.clear();
+  }
+
+
+
   Node TheorySetsRels::reverseTuple(TNode tuple) {
-    // need to register the newly created tuple?
-    Assert(tuple.getType().isDatatype());
+    Assert(tuple.getType().isTuple());
 
     std::vector<Node> elements;
-    Datatype dt = (Datatype)((tuple.getType()).getDatatype());
+    std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
+    std::reverse(tuple_types.begin(), tuple_types.end());
+    TypeNode tn = NodeManager::currentNM()->mkTupleType(tuple_types);
+    Datatype dt = tn.getDatatype();
 
-    elements.push_back(tuple.getOperator());
+    elements.push_back(Node::fromExpr(dt[0].getConstructor()));
     for(Node::iterator child_it = tuple.end()-1;
               child_it != tuple.begin()-1; --child_it) {
       elements.push_back(*child_it);
@@ -125,12 +258,10 @@ namespace sets {
   }
 
   void TheorySetsRels::assertMembership(TNode fact, TNode reason, bool polarity) {
-    TNode explain = reason;
-    if(!polarity) {
-      explain = reason.negate();
-    }
-    Debug("rels") << " polarity : " << polarity << " reason: " << explain << std::endl;
-    d_eqEngine->assertPredicate(fact, polarity, explain);
+    Debug("rels") << "fact: " << fact
+                  << "\npolarity : " << polarity
+                  << "\nreason: " << reason << std::endl;
+    d_eqEngine->assertPredicate(fact, polarity, reason);
   }
 }
 }
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index c48217275..537fc2d43 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -30,7 +30,8 @@ class TheorySetsRels {
 public:
   TheorySetsRels(context::Context* c,
                  context::UserContext* u,
-                 eq::EqualityEngine*);
+                 eq::EqualityEngine*,
+                 context::CDO<bool>* );
 
   ~TheorySetsRels();
 
@@ -42,14 +43,31 @@ private:
   Node d_trueNode;
   Node d_falseNode;
 
+  // Facts and lemmas to be sent to EE
+  std::map< Node, Node> d_pending_facts;
+  std::vector< Node > d_lemma_cache;
+
+  // Relation pairs to be joined
+//  std::map<TNode, TNode> d_rel_pairs;
+//  std::hash_set<TNode> d_rels;
+
   eq::EqualityEngine *d_eqEngine;
+  context::CDO<bool> *d_conflict;
 
   // save all the relational terms seen so far
   context::CDHashSet <Node, NodeHashFunction> d_relsSaver;
 
   void assertMembership(TNode fact, TNode reason, bool polarity);
 
-  Node reverseTuple(TNode tuple);
+  void joinRelations(TNode, TNode, TypeNode);
+  void joinTuples(TNode, TNode, std::vector<Node>&, std::vector<Node>&, TypeNode tn);
+
+  Node reverseTuple(TNode);
+
+  void sendLemma(TNode fact, TNode reason, bool polarity);
+  void doPendingLemmas();
+  void doPendingFacts();
+
 };
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 8d294ceeb..0909d8442 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -209,8 +209,6 @@ struct RelBinaryOperatorTypeRule {
       }
       resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
     }
-
-    Debug("rels") << "The resulting Type is " << resultType << std::endl;
     return resultType;
   }
 
@@ -263,7 +261,7 @@ struct RelTransClosureTypeRule {
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
       Assert(n.getKind() == kind::TRANSCLOSURE);
-      return true;
+      return false;
     }
 };/* struct RelTransClosureTypeRule */