adapted the solver to accept sets of built-in types (int, string, real)

use dummy lemmas to find tuple elements equality

4 files changed, 150 insertions, 83 deletions

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 2b35fb077..ec2d28fa6 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -108,11 +108,11 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
         if(getRepresentative(r) == getRepresentative(d_trueNode) ||
            getRepresentative(r) == getRepresentative(d_falseNode)) {
           // collect membership info
-          if(n.getKind() == kind::MEMBER && n[0].getType().isTuple()) {
+          if(n.getKind() == kind::MEMBER) {
             Node tup_rep = getRepresentative(n[0]);
             Node rel_rep = getRepresentative(n[1]);
             // No rel_rep is found
-            if(d_membership_cache.find(rel_rep) == d_membership_cache.end()) {
+            if( d_membership_cache.find(rel_rep) == d_membership_cache.end() ) {
               std::vector<Node> tups;
               tups.push_back(tup_rep);
               d_membership_cache[rel_rep] = tups;
@@ -122,9 +122,9 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
               tups.clear();
               tups.push_back(exp);
               d_membership_exp_cache[rel_rep] = tups;
-            } else if(std::find(d_membership_cache.at(rel_rep).begin(),
-                                d_membership_cache.at(rel_rep).end(), tup_rep)
-                      == d_membership_cache.at(rel_rep).end()) {
+            } else if( std::find(d_membership_cache[rel_rep].begin(),
+                                 d_membership_cache[rel_rep].end(), tup_rep)
+                       == d_membership_cache[rel_rep].end() ) {
               d_membership_cache[rel_rep].push_back(tup_rep);
               Node exp = n;
               if(getRepresentative(r) == getRepresentative(d_falseNode))
@@ -133,22 +133,22 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
             }
           }
         // collect term info
-        } else if(r.getType().isSet() && r.getType().getSetElementType().isTuple()) {
-          if(n.getKind() == kind::TRANSPOSE ||
-             n.getKind() == kind::JOIN ||
-             n.getKind() == kind::PRODUCT ||
-             n.getKind() == kind::TRANSCLOSURE) {
+        } else if( r.getType().isSet() ) {
+          if( n.getKind() == kind::TRANSPOSE ||
+              n.getKind() == kind::JOIN ||
+              n.getKind() == kind::PRODUCT ||
+              n.getKind() == kind::TRANSCLOSURE ) {
             std::map<kind::Kind_t, std::vector<Node> > rel_terms;
             std::vector<Node> terms;
             // No r record is found
-            if(d_terms_cache.find(r) == d_terms_cache.end()) {
+            if( d_terms_cache.find(r) == d_terms_cache.end() ) {
               terms.push_back(n);
               rel_terms[n.getKind()] = terms;
               d_terms_cache[r] = rel_terms;
             } else {
               rel_terms = d_terms_cache[r];
               // No n's kind record is found
-              if(rel_terms.find(n.getKind()) == rel_terms.end()) {
+              if( rel_terms.find(n.getKind()) == rel_terms.end() ) {
                 terms.push_back(n);
                 rel_terms[n.getKind()] = terms;
               } else {
@@ -228,8 +228,8 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Node r1 = join_term[0];
     Node r2 = join_term[1];
 
-    // case: (a, b) IS_IN (X JOIN Y)
-    //      => (a, z) IS_IN X  && (z, b) IS_IN Y
+    // join-split rule: (a, b) IS_IN (X JOIN Y)
+    //               => (a, z) IS_IN X  && (z, b) IS_IN Y
     if(polarity) {
       Debug("rels-join") << "[sets-rels] Join rules (a, b) IS_IN (X JOIN Y) => "
                             "((a, z) IS_IN X  && (z, b) IS_IN Y)"<< std::endl;
@@ -386,6 +386,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     Node r2 = n[1];
     Node r1_rep = getRepresentative(r1);
     Node r2_rep = getRepresentative(r2);
+    NodeManager* nm = NodeManager::currentNM();
     Trace("rels-debug") << "[sets-rels] start composing tuples in relations "
                        << r1 << " and " << r2
                        << "\n r1_rep: " << r1_rep
@@ -395,8 +396,6 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
        d_membership_cache.find(r2_rep) == d_membership_cache.end())
     return;
 
-    TypeNode tn = n.getType().getSetElementType();
-    Datatype dt = tn.getDatatype();
     std::vector<Node> new_tups;
     std::vector<Node> new_exps;
     std::vector<Node> r1_elements = d_membership_cache[r1_rep];
@@ -405,28 +404,47 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     std::vector<Node> r2_exps = d_membership_exp_cache[r2_rep];
     Node new_rel = n.getKind() == kind::JOIN ? NodeManager::currentNM()->mkNode(kind::JOIN, r1_rep, r2_rep)
                                              : NodeManager::currentNM()->mkNode(kind::PRODUCT, r1_rep, r2_rep);
-    unsigned int t1_len = r1_elements.front().getType().getTupleLength();
-    unsigned int t2_len = r2_elements.front().getType().getTupleLength();
-
+    unsigned int t1_len = 1;
+    unsigned int t2_len = 1;
+    if(r1_elements.front().getType().isTuple())
+      t1_len = r1_elements.front().getType().getTupleLength();
+    if(r2_elements.front().getType().isTuple())
+      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++) {
-        std::vector<Node> joinedTuple;
-        joinedTuple.push_back(Node::fromExpr(dt[0].getConstructor()));
-        if((areEqual(r1_elements[i][t1_len-1], r2_elements[j][0]) && n.getKind() == kind::JOIN) ||
-            n.getKind() == kind::PRODUCT) {
+
+        std::vector<Node> composedTuple;
+        TypeNode tn = n.getType().getSetElementType();
+        if(tn.isTuple()) {
+          composedTuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
+        }
+        Node r1_e = r1_elements[i];
+        Node r2_e = r2_elements[j];
+        if(r1_e.getType().isTuple())
+          r1_e = r1_elements[i][t1_len-1];
+        if(r2_e.getType().isTuple())
+          r2_e = r2_elements[j][0];
+
+        if((areEqual(r1_e, r2_e) && n.getKind() == kind::JOIN) ||
+           n.getKind() == kind::PRODUCT) {
           unsigned int k = 0;
           unsigned int l = 1;
           for(; k < t1_len - 1; ++k) {
-            joinedTuple.push_back(r1_elements[i][k]);
+            composedTuple.push_back(r1_elements[i][k]);
           }
           if(kind::PRODUCT == n.getKind()) {
-            joinedTuple.push_back(r1_elements[i][k]);
-            joinedTuple.push_back(r1_elements[j][0]);
+            composedTuple.push_back(r1_elements[i][k]);
+            composedTuple.push_back(r1_elements[j][0]);
           }
           for(; l < t2_len; ++l) {
-            joinedTuple.push_back(r2_elements[j][l]);
+            composedTuple.push_back(r2_elements[j][l]);
+          }
+          Node fact;
+          if(tn.isTuple()) {
+            fact = nm->mkNode(kind::APPLY_CONSTRUCTOR, composedTuple);
+          } else {
+            fact = composedTuple[0];
           }
-          Node fact = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, joinedTuple);
           new_tups.push_back(fact);
           fact = MEMBER(fact, new_rel);
           std::vector<Node> reasons;
@@ -435,7 +453,7 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
           //Todo: think about how to deal with shared terms(?)
           if(n.getKind() == kind::JOIN)
-            reasons.push_back(EQUAL(r1_elements[i][t1_len-1], r2_elements[j][0]));
+            reasons.push_back(EQUAL(r1_e, r2_e));
 
           if(r1 != r1_rep) {
             reasons.push_back(EQUAL(r1, r1_rep));
@@ -500,8 +518,9 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
     d_lemma_cache.push_back( lemma_or );
   }
 
-  void TheorySetsRels::sendLemma(Node fact, Node reason, bool polarity) {
-
+  void TheorySetsRels::sendLemma(Node conc, Node ant, const char * c) {
+    Trace("rels-lemma") << "[sets-rels] Infer " << conc << " from " << ant << " by " << c << std::endl;
+    d_lemma_cache.push_back(conc);
   }
 
   void TheorySetsRels::sendInfer( Node fact, Node exp, const char * c ) {
@@ -549,47 +568,55 @@ typedef std::map<Node, std::vector<Node> >::iterator mem_it;
 
   bool TheorySetsRels::areEqual( Node a, Node b ){
     if( hasTerm( a ) && hasTerm( b ) ){
-      if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) &&
-          d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) {
-        // Get representative trigger terms
-          TNode x_shared = d_eqEngine->getTriggerTermRepresentative(a, THEORY_SETS);
-          TNode y_shared = d_eqEngine->getTriggerTermRepresentative(b, THEORY_SETS);
-          EqualityStatus eqStatusDomain = d_sets.d_valuation.getEqualityStatus(x_shared, y_shared);
-          switch (eqStatusDomain) {
-            case EQUALITY_TRUE_AND_PROPAGATED:
-              // Should have been propagated to us
-              Trace("rels-debug") << "EQUALITY_TRUE_AND_PROPAGATED ****  equality( a, b ) = true" << std::endl;
-              return true;
-              break;
-            case EQUALITY_TRUE:
-              // Missed propagation - need to add the pair so that theory engine can force propagation
-              Trace("rels-debug") << "EQUALITY_TRUE **** equality( a, b ) = true" << std::endl;
-              return true;
-              break;
-            case EQUALITY_FALSE_AND_PROPAGATED:
-              // Should have been propagated to us
-              Trace("rels-debug") << "EQUALITY_FALSE_AND_PROPAGATED ******** equality( a, b ) = false" << std::endl;
-              return false;
-              break;
-            case EQUALITY_FALSE:
-              Trace("rels-debug") << "EQUALITY_FALSE **** equality( a, b ) = false" << std::endl;
-              return false;
-              break;
-
-            default:
-              // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
-              break;
-          }
-      }
+//      if( d_eqEngine->isTriggerTerm(a, THEORY_SETS) &&
+//          d_eqEngine->isTriggerTerm(b, THEORY_SETS) ) {
+//        // Get representative trigger terms
+//          TNode x_shared = d_eqEngine->getTriggerTermRepresentative(a, THEORY_SETS);
+//          TNode y_shared = d_eqEngine->getTriggerTermRepresentative(b, THEORY_SETS);
+//          EqualityStatus eqStatusDomain = d_sets.d_valuation.getEqualityStatus(x_shared, y_shared);
+//          switch (eqStatusDomain) {
+//            case EQUALITY_TRUE_AND_PROPAGATED:
+//              // Should have been propagated to us
+//              Trace("rels-debug") << "EQUALITY_TRUE_AND_PROPAGATED ****  equality( a, b ) = true" << std::endl;
+//              return true;
+//              break;
+//            case EQUALITY_TRUE:
+//              // Missed propagation - need to add the pair so that theory engine can force propagation
+//              Trace("rels-debug") << "EQUALITY_TRUE **** equality( a, b ) = true" << std::endl;
+//              return true;
+//              break;
+//            case EQUALITY_FALSE_AND_PROPAGATED:
+//              // Should have been propagated to us
+//              Trace("rels-debug") << "EQUALITY_FALSE_AND_PROPAGATED ******** equality( a, b ) = false" << std::endl;
+//              return false;
+//              break;
+//            case EQUALITY_FALSE:
+//              Trace("rels-debug") << "EQUALITY_FALSE **** equality( a, b ) = false" << std::endl;
+//              return false;
+//              break;
+//
+//            default:
+//              // Covers EQUALITY_TRUE_IN_MODEL (common case) and EQUALITY_UNKNOWN
+//              break;
+//          }
+//      }
       Trace("rels-debug") << "has a and b " << a << " " << b << " are equal? "<<  d_eqEngine->areEqual( a, b ) << std::endl;
       return d_eqEngine->areEqual( a, b );
     }else if( a.isConst() && b.isConst() ){
       return a == b;
     }else {
       Trace("rels-debug") << "to split a and b " << a << " " << b << std::endl;
+      Node x = NodeManager::currentNM()->mkSkolem( "sde", a.getType() );
+      Node y = NodeManager::currentNM()->mkSkolem( "sde", b.getType() );
+      Node set_a = NodeManager::currentNM()->mkNode( kind::SINGLETON, a );
+      Node set_b = NodeManager::currentNM()->mkNode( kind::SINGLETON, b );
+      Node dummy_lemma_1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, set_a );
+      Node dummy_lemma_2 = NodeManager::currentNM()->mkNode( kind::MEMBER, y, set_b );
+      sendLemma( dummy_lemma_1, d_trueNode, "dummy-lemma" );
+      sendLemma( dummy_lemma_2, d_trueNode, "dummy-lemma" );
       addSharedTerm(a);
       addSharedTerm(b);
-      sendSplit(a, b, "tuple-element-equality");
+//      sendSplit(a, b, "tuple-element-equality");
       return false;
     }
   }
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index d0d926e69..16329fd43 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -82,7 +82,7 @@ private:
   Node reverseTuple( Node );
 
   void sendInfer( Node fact, Node exp, const char * c );
-  void sendLemma( Node fact, Node reason, bool polarity );
+  void sendLemma( Node fact, Node reason, const char * c );
   void sendSplit( Node a, Node b, const char * c );
   void doPendingFacts();
   void doPendingSplitFacts();
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index dac554d4f..8b639a2e5 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -64,6 +64,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     }
     if(node[1].getKind() == kind::TRANSPOSE) {
       // only work for node[0] is an actual tuple like (a, b), won't work for tuple variables
+      if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple()) {
+        Node atom = node;
+        bool polarity = node.getKind() != kind::NOT;
+        if( !polarity )
+          atom = atom[0];
+        Node new_node = NodeManager::currentNM()->mkNode(kind::MEMBER, atom[0], atom[1][0]);
+        if(!polarity)
+          new_node = new_node.negate();
+        return RewriteResponse(REWRITE_AGAIN, new_node);
+      }
       if(node[0].isVar())
         return RewriteResponse(REWRITE_DONE, node);
       std::vector<Node> elements;
@@ -198,6 +208,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   }//kind::UNION
 
   case kind::TRANSPOSE: {
+    if(node[0].getType().isSet() && !node[0].getType().getSetElementType().isTuple())
+      return RewriteResponse(REWRITE_AGAIN, node[0]);
     if(node[0].getKind() != kind::TRANSPOSE) {
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << node << std::endl;
       return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 0909d8442..6a606ef5c 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -179,35 +179,60 @@ struct RelBinaryOperatorTypeRule {
       if(!firstRelType.isSet() || !secondRelType.isSet()) {
         throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets");
       }
-      if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
-        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
-      }
+//      if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) {
+//        throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)");
+//      }
 
       std::vector<TypeNode> newTupleTypes;
-      std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes();
-      std::vector<TypeNode> secondTupleTypes = secondRelType[0].getTupleTypes();
+      TypeNode set_element_type_1 = firstRelType.getSetElementType();
+      TypeNode set_element_type_2 = secondRelType.getSetElementType();
+      std::vector<TypeNode> firstTupleTypes;
+      std::vector<TypeNode> secondTupleTypes;
+
       // JOIN is not allowed to apply on two unary sets
-      if(n.getKind() == kind::JOIN) {
-        if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) {
+      if( n.getKind() == kind::JOIN ) {
+        if( !set_element_type_1.isTuple() && !set_element_type_2.isTuple()) {
           throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
-        }
-        if(firstTupleTypes.back() != secondTupleTypes.front()) {
-          throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
-        }
-
-        if(firstTupleTypes.size() == 1) {
+        } else if ( !set_element_type_1.isTuple() ) {
+          secondTupleTypes = set_element_type_2.getTupleTypes();
+          if(set_element_type_1 != secondTupleTypes.front()) {
+            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
+          }
           newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
-        } else if (secondTupleTypes.size() == 1) {
+        } else if ( !set_element_type_2.isTuple() ) {
+          firstTupleTypes = set_element_type_1.getTupleTypes();
+          if(set_element_type_2 != firstTupleTypes.front()) {
+            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
+          }
           newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
         } else {
+          firstTupleTypes = set_element_type_1.getTupleTypes();
+          secondTupleTypes = set_element_type_2.getTupleTypes();
+          if(firstTupleTypes.back() != secondTupleTypes.front()) {
+            throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations");
+          }
           newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1);
           newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end());
         }
-      }else if(n.getKind() == kind::PRODUCT) {
+      }else if( n.getKind() == kind::PRODUCT ) {
+        if( !set_element_type_1.isTuple() ) {
+          firstTupleTypes.push_back(set_element_type_1);
+        } else {
+          firstTupleTypes = set_element_type_1.getTupleTypes();
+        }
+        if( !set_element_type_2.isTuple() ) {
+          secondTupleTypes.push_back(set_element_type_2);
+        } else {
+          secondTupleTypes = set_element_type_2.getTupleTypes();
+        }
         newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end());
         newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end());
       }
-      resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+      Assert(newTupleTypes.size() >= 1);
+      if(newTupleTypes.size() > 1)
+        resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes));
+      else
+        resultType = nodeManager->mkSetType(newTupleTypes[0]);
     }
     return resultType;
   }
@@ -223,17 +248,20 @@ struct RelTransposeTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
     Assert(n.getKind() == kind::TRANSPOSE);
+
+
     TypeNode setType = n[0].getType(check);
-    if(check && !setType.isSet() && !setType[0].isTuple()) {
+    if(check && !setType.isSet()) {
         throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation");
     }
+    if(!setType.getSetElementType().isTuple())
+      return setType;
 
     std::vector<TypeNode> tupleTypes;
     std::vector<TypeNode> originalTupleTypes = setType[0].getTupleTypes();
     for(std::vector<TypeNode>::reverse_iterator it = originalTupleTypes.rbegin(); it != originalTupleTypes.rend(); ++it) {
       tupleTypes.push_back(*it);
     }
-
     return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes));
   }