Refactored code

diff --git a/src/Makefile.am b/src/Makefile.am
index 040be7fae905f675c5acfd4edf2fa6809539701c..26a677d90cd9f7374e2c16240e10e54b04deece0 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -257,6 +257,7 @@ libcvc4_la_SOURCES = \
        theory/sets/theory_sets_private.h \
        theory/sets/theory_sets_rels.cpp \
        theory/sets/theory_sets_rels.h \
+       theory/sets/rels_utils.h \
        theory/sets/theory_sets_rewriter.cpp \
        theory/sets/theory_sets_rewriter.h \
        theory/sets/theory_sets_type_enumerator.h \

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 434202a53a146fdb90862016ff6bc2501906e715..fee47e3cb0ebd4764756aa6770e6257780f780f5 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -726,14 +726,14 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
         std::vector<Node> left_tuple;
         left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
         for(int i = 0; i < left_len; i++) {
-          left_tuple.push_back(TheorySetsRels::nthElementOfTuple(*left_it,i));
+          left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
         Elements::const_iterator right_it = right.begin();
         int right_len = (*right_it).getType().getTupleLength();
         while(right_it != right.end()) {
           std::vector<Node> right_tuple;
           for(int j = 0; j < right_len; j++) {
-            right_tuple.push_back(TheorySetsRels::nthElementOfTuple(*right_it,j));
+            right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
           }
           std::vector<Node> new_tuple;
           new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
@@ -758,15 +758,15 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
         std::vector<Node> left_tuple;
         left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
         for(int i = 0; i < left_len - 1; i++) {
-          left_tuple.push_back(TheorySetsRels::nthElementOfTuple(*left_it,i));
+          left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
         Elements::const_iterator right_it = right.begin();
         int right_len = (*right_it).getType().getTupleLength();
         while(right_it != right.end()) {
-          if(TheorySetsRels::nthElementOfTuple(*left_it,left_len-1) == TheorySetsRels::nthElementOfTuple(*right_it,0)) {
+          if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) {
             std::vector<Node> right_tuple;
             for(int j = 1; j < right_len; j++) {
-              right_tuple.push_back(TheorySetsRels::nthElementOfTuple(*right_it,j));
+              right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
             }
             std::vector<Node> new_tuple;
             new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
@@ -929,20 +929,20 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
     m->assertRepresentative(shape);
   }
 
-#ifdef CVC4_ASSERTIONS
-  bool checkPassed = true;
-  BOOST_FOREACH(TNode term, terms) {
-    if( term.getType().isSet() ) {
-      checkPassed &= checkModel(settermElementsMap, term);
-    }
-  }
-  if(Trace.isOn("sets-checkmodel-ignore")) {
-    Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
-  } else {
-    Assert( checkPassed,
-            "THEORY_SETS check-model failed. Run with -d sets-model for details." );
-  }
-#endif
+// #ifdef CVC4_ASSERTIONS
+//   bool checkPassed = true;
+//   BOOST_FOREACH(TNode term, terms) {
+//     if( term.getType().isSet() ) {
+//       checkPassed &= checkModel(settermElementsMap, term);
+//     }
+//   }
+//   if(Trace.isOn("sets-checkmodel-ignore")) {
+//     Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
+//   } else {
+//     Assert( checkPassed,
+//             "THEORY_SETS check-model failed. Run with -d sets-model for details." );
+//   }
+// #endif
 }
 
 Node TheorySetsPrivate::getModelValue(TNode n)

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index ce81fac27c20c0071208db264561e4403140b2eb..a01e9a168ae13252fc30666ebd4e433da871cde0 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -26,6 +26,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/sets/term_info.h"
 #include "theory/sets/theory_sets_rels.h"
+#include "theory/sets/rels_utils.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index a1a799f4b85573dca3582cf38930bb3f64d80456..75e3d483183593cbd0c3fc7296a14ac91a2d935c 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -172,7 +172,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
         // need to add all tuple elements as shared terms
         } else if(n.getType().isTuple() && !n.isConst() && !n.isVar()) {
           for(unsigned int i = 0; i < n.getType().getTupleLength(); i++) {
-            Node element = nthElementOfTuple(n, i);
+            Node element = RelsUtils::nthElementOfTuple(n, i);
             if(!element.isConst()) {
               makeSharedTerm(element);
             }
@@ -208,13 +208,13 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     if(mem_it != d_membership_db.end()) {
       for(std::vector<Node>::iterator pair_it = mem_it->second.begin();
           pair_it != mem_it->second.end(); pair_it++) {
-        TC_PAIR_IT pair_set_it = tc_graph.find(nthElementOfTuple(*pair_it, 0));
+        TC_PAIR_IT pair_set_it = tc_graph.find(RelsUtils::nthElementOfTuple(*pair_it, 0));
         if( pair_set_it != tc_graph.end() ) {
-          pair_set_it->second.insert(nthElementOfTuple(*pair_it, 1));
+          pair_set_it->second.insert(RelsUtils::nthElementOfTuple(*pair_it, 1));
         } else {
           std::hash_set< Node, NodeHashFunction > snd_pair_set;
-          snd_pair_set.insert(nthElementOfTuple(*pair_it, 1));
-          tc_graph[nthElementOfTuple(*pair_it, 0)] = snd_pair_set;
+          snd_pair_set.insert(RelsUtils::nthElementOfTuple(*pair_it, 1));
+          tc_graph[RelsUtils::nthElementOfTuple(*pair_it, 0)] = snd_pair_set;
         }
       }
     }
@@ -243,13 +243,13 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     TC_IT tc_graph_it = d_membership_tc_cache.find(tc_rep);
     if(polarity) {
       if(tc_graph_it != d_membership_tc_cache.end()) {
-        TC_PAIR_IT pair_set_it = tc_graph_it->second.find(nthElementOfTuple(atom[0], 0));
+        TC_PAIR_IT pair_set_it = tc_graph_it->second.find(RelsUtils::nthElementOfTuple(atom[0], 0));
         if(pair_set_it != tc_graph_it->second.end()) {
-          pair_set_it->second.insert(nthElementOfTuple(atom[0], 1));
+          pair_set_it->second.insert(RelsUtils::nthElementOfTuple(atom[0], 1));
         } else {
           std::hash_set< Node, NodeHashFunction > pair_set;
-          pair_set.insert(nthElementOfTuple(atom[0], 1));
-          tc_graph_it->second[nthElementOfTuple(atom[0], 0)] = pair_set;
+          pair_set.insert(RelsUtils::nthElementOfTuple(atom[0], 1));
+          tc_graph_it->second[RelsUtils::nthElementOfTuple(atom[0], 0)] = pair_set;
         }
         Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]);
         std::map< Node, Node >::iterator exp_it = d_membership_tc_exp_cache.find(tc_rep);
@@ -259,8 +259,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
       } else {
         std::map< Node, std::hash_set< Node, NodeHashFunction > > pair_set;
         std::hash_set< Node, NodeHashFunction > set;
-        set.insert(nthElementOfTuple(atom[0], 1));
-        pair_set[nthElementOfTuple(atom[0], 0)] = set;
+        set.insert(RelsUtils::nthElementOfTuple(atom[0], 1));
+        pair_set[RelsUtils::nthElementOfTuple(atom[0], 0)] = set;
         d_membership_tc_cache[tc_rep] = pair_set;
         Node reason = getReason(tc_rep, tc_term, tc_r_rep, tc_term[0]);
         if(!reason.isNull()) {
@@ -270,8 +270,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     // check if atom[0] already exists in TC graph for conflict
     } else {
       if(tc_graph_it != d_membership_tc_cache.end()) {
-        checkTCGraphForConflict(atom, tc_rep, d_trueNode, nthElementOfTuple(atom[0], 0),
-                                nthElementOfTuple(atom[0], 1), tc_graph_it->second);
+        checkTCGraphForConflict(atom, tc_rep, d_trueNode, RelsUtils::nthElementOfTuple(atom[0], 0),
+                                RelsUtils::nthElementOfTuple(atom[0], 1), tc_graph_it->second);
       }
     }
   }
@@ -335,13 +335,13 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
 
     r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
     for(; i < s1_len; ++i) {
-      r1_element.push_back(nthElementOfTuple(atom[0], i));
+      r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i));
     }
 
     dt = r2_rep.getType().getSetElementType().getDatatype();
     r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
     for(; i < tup_len; ++i) {
-      r2_element.push_back(nthElementOfTuple(atom[0], i));
+      r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i));
     }
 
     Node fact_1;
@@ -424,7 +424,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
 
       r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
       for(; i < s1_len-1; ++i) {
-        r1_element.push_back(nthElementOfTuple(atom[0], i));
+        r1_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i));
       }
       r1_element.push_back(shared_x);
 
@@ -432,7 +432,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
       r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
       r2_element.push_back(shared_x);
       for(; i < tup_len; ++i) {
-        r2_element.push_back(nthElementOfTuple(atom[0], i));
+        r2_element.push_back(RelsUtils::nthElementOfTuple(atom[0], i));
       }
 
       Node t1 = nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element);
@@ -496,7 +496,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     Trace("rels-debug") << "\n[sets-rels] *********** Applying TRANSPOSE rule  " << std::endl;
     bool polarity = exp.getKind() != kind::NOT;
     Node atom = polarity ? exp : exp[0];
-    Node reversedTuple = getRepresentative(reverseTuple(atom[0]));
+    Node reversedTuple = getRepresentative(RelsUtils::reverseTuple(atom[0]));
 
     if(tp_occur) {
       Trace("rels-debug") << "\n[sets-rels] Apply TRANSPOSE-OCCUR rule on term: " << tp_term
@@ -671,7 +671,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     Assert(tuples.size() == exps.size());
     for(unsigned int i = 0; i < tuples.size(); i++) {
       Node reason = exps[i][1] == n0_rep ? exps[i] : AND(exps[i], EQUAL(exps[i][1], n0_rep));
-      Node rev_tup = getRepresentative(reverseTuple(tuples[i]));
+      Node rev_tup = getRepresentative(RelsUtils::reverseTuple(tuples[i]));
       Node fact = MEMBER(rev_tup, n_rep);
       if(holds(fact)) {
         Trace("rels-debug") << "[sets-rels] New fact: " << fact << " already holds! Skip..." << std::endl;
@@ -717,8 +717,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
       for(unsigned int j = 0; j < r2_elements.size(); j++) {
         std::vector<Node> composed_tuple;
         TypeNode tn = n.getType().getSetElementType();
-        Node r2_lmost = nthElementOfTuple(r2_elements[j], 0);
-        Node r1_rmost = nthElementOfTuple(r1_elements[i], t1_len-1);
+        Node r2_lmost = RelsUtils::nthElementOfTuple(r2_elements[j], 0);
+        Node r1_rmost = RelsUtils::nthElementOfTuple(r1_elements[i], t1_len-1);
         composed_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
 
         if((areEqual(r1_rmost, r2_lmost) && n.getKind() == kind::JOIN) ||
@@ -727,14 +727,14 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
           unsigned int k = 0;
           unsigned int l = 1;
           for(; k < t1_len - 1; ++k) {
-            composed_tuple.push_back(nthElementOfTuple(r1_elements[i], k));
+            composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k));
           }
           if(isProduct) {
-            composed_tuple.push_back(nthElementOfTuple(r1_elements[i], k));
-            composed_tuple.push_back(nthElementOfTuple(r2_elements[j], 0));
+            composed_tuple.push_back(RelsUtils::nthElementOfTuple(r1_elements[i], k));
+            composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], 0));
           }
           for(; l < t2_len; ++l) {
-            composed_tuple.push_back(nthElementOfTuple(r2_elements[j], l));
+            composed_tuple.push_back(RelsUtils::nthElementOfTuple(r2_elements[j], l));
           }
           Node composed_tuple_rep = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, composed_tuple));
           Node fact = MEMBER(composed_tuple_rep, new_rel_rep);
@@ -883,20 +883,6 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     d_pending_split_facts.clear();
   }
 
-  Node TheorySetsRels::reverseTuple( Node tuple ) {
-    Assert( tuple.getType().isTuple() );
-    std::vector<Node> elements;
-    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( Node::fromExpr(dt[0].getConstructor() ) );
-    for(int i = tuple_types.size() - 1; i >= 0; --i) {
-      elements.push_back( nthElementOfTuple(tuple, i) );
-    }
-    return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, elements );
-  }
-
   void TheorySetsRels::assertMembership( Node fact, Node reason, bool polarity ) {
     d_eqEngine->assertPredicate( fact, polarity, reason );
   }
@@ -921,7 +907,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     } else if(a.getType().isTuple()) {
       bool equal = true;
       for(unsigned int i = 0; i < a.getType().getTupleLength(); i++) {
-        equal = equal && areEqual(nthElementOfTuple(a, i), nthElementOfTuple(b, i));
+        equal = equal && areEqual(RelsUtils::nthElementOfTuple(a, i), RelsUtils::nthElementOfTuple(b, i));
       }
       return equal;
     } else if(!a.getType().isBoolean()){
@@ -1001,11 +987,11 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
               exp = AND(exp, explain(EQUAL(tc_rep, tc_term)));
             }
             if(tc_r_mems->second[i] != tuple) {
-              if(nthElementOfTuple(tc_r_mems->second[i], 0) != nthElementOfTuple(tuple, 0)) {
-                exp = AND(exp, explain(EQUAL(nthElementOfTuple(tc_r_mems->second[i], 0), nthElementOfTuple(tuple, 0))));
+              if(RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 0) != RelsUtils::nthElementOfTuple(tuple, 0)) {
+                exp = AND(exp, explain(EQUAL(RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 0), RelsUtils::nthElementOfTuple(tuple, 0))));
               }
-              if(nthElementOfTuple(tc_r_mems->second[i], 1) != nthElementOfTuple(tuple, 1)) {
-                exp = AND(exp, explain(EQUAL(nthElementOfTuple(tc_r_mems->second[i], 1), nthElementOfTuple(tuple, 1))));
+              if(RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 1) != RelsUtils::nthElementOfTuple(tuple, 1)) {
+                exp = AND(exp, explain(EQUAL(RelsUtils::nthElementOfTuple(tc_r_mems->second[i], 1), RelsUtils::nthElementOfTuple(tuple, 1))));
               }
               exp = AND(exp, EQUAL(tc_r_mems->second[i], tuple));
             }
@@ -1028,11 +1014,11 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
               exp = AND(exp, explain(EQUAL(tc_term_rep, tc_terms[i])));
             }
             if(tc_t_mems->second[j] != tuple) {
-              if(nthElementOfTuple(tc_t_mems->second[j], 0) != nthElementOfTuple(tuple, 0)) {
-                exp = AND(exp, explain(EQUAL(nthElementOfTuple(tc_t_mems->second[j], 0), nthElementOfTuple(tuple, 0))));
+              if(RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 0) != RelsUtils::nthElementOfTuple(tuple, 0)) {
+                exp = AND(exp, explain(EQUAL(RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 0), RelsUtils::nthElementOfTuple(tuple, 0))));
               }
-              if(nthElementOfTuple(tc_t_mems->second[j], 1) != nthElementOfTuple(tuple, 1)) {
-                exp = AND(exp, explain(EQUAL(nthElementOfTuple(tc_t_mems->second[j], 1), nthElementOfTuple(tuple, 1))));
+              if(RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 1) != RelsUtils::nthElementOfTuple(tuple, 1)) {
+                exp = AND(exp, explain(EQUAL(RelsUtils::nthElementOfTuple(tc_t_mems->second[j], 1), RelsUtils::nthElementOfTuple(tuple, 1))));
               }
               exp = AND(exp, EQUAL(tc_t_mems->second[j], tuple));
             }
@@ -1052,13 +1038,6 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     return Node::null();
   }
 
-  Node TheorySetsRels::nthElementOfTuple( Node tuple, int n_th ) {    
-    if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst()))
-      return tuple[n_th];
-    Datatype dt = tuple.getType().getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][n_th].getSelector(), tuple);
-  }
-
   void TheorySetsRels::addSharedTerm( TNode n ) {
     Trace("rels-debug") << "[sets-rels] Add a shared term:  " << n << std::endl;
     d_sets_theory.addSharedTerm(n);
@@ -1102,7 +1081,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
   void TheorySetsRels::computeTupleReps( Node n ) {
     if( d_tuple_reps.find( n ) == d_tuple_reps.end() ){
       for( unsigned i = 0; i < n.getType().getTupleLength(); i++ ){
-        d_tuple_reps[n].push_back( getRepresentative( nthElementOfTuple(n, i) ) );
+        d_tuple_reps[n].push_back( getRepresentative( RelsUtils::nthElementOfTuple(n, i) ) );
       }
     }
   }
@@ -1125,7 +1104,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
       std::vector<Node> tuple_elements;
       tuple_elements.push_back(Node::fromExpr((n[0].getType().getDatatype())[0].getConstructor()));
       for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
-        Node element = nthElementOfTuple(n[0], i);
+        Node element = RelsUtils::nthElementOfTuple(n[0], i);
         makeSharedTerm(element);
         tuple_elements.push_back(element);
       }
@@ -1435,18 +1414,18 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     Node n1;
     if(reverseOnly) {
       if(polarity) {
-        n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(reverseTuple(t1), t2[0]) );
+        n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]) );
       } else {
-        n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(reverseTuple(t1), t2[0]).negate() );
+        n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]).negate() );
       }
     } else {
       Node n2;
       if(polarity) {
         n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(t1, t2) );
-        n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(reverseTuple(t1), t2[0]) );
+        n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]) );
       } else {
         n1 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(t1, t2).negate() );
-        n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(reverseTuple(t1), t2[0]).negate() );
+        n2 = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, MEMBER(RelsUtils::reverseTuple(t1), t2[0]).negate() );
       }
       Trace("rels-std") << "[sets-rels-lemma] Generate a lemma by applying transpose rule: "
                         << n2 << std::endl;
@@ -1485,13 +1464,13 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
 
     r1_element.push_back(Node::fromExpr(dt[0].getConstructor()));
     for(; i < s1_len; ++i) {
-      r1_element.push_back(nthElementOfTuple(t1, i));
+      r1_element.push_back(RelsUtils::nthElementOfTuple(t1, i));
     }
 
     dt = r2.getType().getSetElementType().getDatatype();
     r2_element.push_back(Node::fromExpr(dt[0].getConstructor()));
     for(; i < tup_len; ++i) {
-      r2_element.push_back(nthElementOfTuple(t1, i));
+      r2_element.push_back(RelsUtils::nthElementOfTuple(t1, i));
     }
     Node tuple_1 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r1_element));
     Node tuple_2 = getRepresentative(nm->mkNode(kind::APPLY_CONSTRUCTOR, r2_element));
@@ -1576,6 +1555,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
 
     return conjunction;
   }/* mkAnd() */
+  
 
 }
 }

diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index b5e36603b0a7fb2288e2f20670a1fb390d388dfd..ff62b67abbfefcc22d8ad6af2073ec2feb82286c 100644 (file)
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -21,6 +21,7 @@
 #include "theory/uf/equality_engine.h"
 #include "context/cdhashset.h"
 #include "context/cdchunk_list.h"
+#include "theory/sets/rels_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -177,10 +178,6 @@ private:
   bool isRel( Node n ) {return n.getType().isSet() && n.getType().getSetElementType().isTuple();}
   Node mkAnd( std::vector< TNode >& assumptions );
 
-public:
-  static Node reverseTuple( Node );
-  static Node nthElementOfTuple( Node, int);
-
 };
 
 

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 4c22f588d75b081a3d877d6046f32d23dd117928..9156e3a75a0ffcaa6b9c6cbf211ec25073be5fee 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/sets/theory_sets_rewriter.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/theory_sets_rels.h"
+#include "theory/sets/rels_utils.h"
 
 namespace CVC4 {
 namespace theory {
@@ -190,7 +191,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       std::set<Node>::iterator tuple_it = tuple_set.begin();
 
       while(tuple_it != tuple_set.end()) {
-        new_tuple_set.insert(TheorySetsRels::reverseTuple(*tuple_it));
+        new_tuple_set.insert(RelsUtils::reverseTuple(*tuple_it));
         tuple_it++;
       }
       Node new_node = NormalForm::elementsToSet(new_tuple_set, node.getType());
@@ -224,7 +225,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
         std::vector<Node> left_tuple;
         left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
         for(int i = 0; i < left_len; i++) {
-          left_tuple.push_back(TheorySetsRels::nthElementOfTuple(*left_it,i));
+          left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
         std::set<Node>::iterator right_it = right.begin();
         int right_len = (*right_it).getType().getTupleLength();
@@ -232,7 +233,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
           Trace("rels-debug") << "Sets::postRewrite processing left_it = " <<  *right_it << std::endl;
           std::vector<Node> right_tuple;
           for(int j = 0; j < right_len; j++) {
-            right_tuple.push_back(TheorySetsRels::nthElementOfTuple(*right_it,j));
+            right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
           }
           std::vector<Node> new_tuple;
           new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
@@ -267,15 +268,15 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
         std::vector<Node> left_tuple;
         left_tuple.push_back(Node::fromExpr(tn.getDatatype()[0].getConstructor()));
         for(int i = 0; i < left_len - 1; i++) {
-          left_tuple.push_back(TheorySetsRels::nthElementOfTuple(*left_it,i));
+          left_tuple.push_back(RelsUtils::nthElementOfTuple(*left_it,i));
         }
         std::set<Node>::iterator right_it = right.begin();
         int right_len = (*right_it).getType().getTupleLength();
         while(right_it != right.end()) {
-          if(TheorySetsRels::nthElementOfTuple(*left_it,left_len-1) == TheorySetsRels::nthElementOfTuple(*right_it,0)) {
+          if(RelsUtils::nthElementOfTuple(*left_it,left_len-1) == RelsUtils::nthElementOfTuple(*right_it,0)) {
             std::vector<Node> right_tuple;
             for(int j = 1; j < right_len; j++) {
-              right_tuple.push_back(TheorySetsRels::nthElementOfTuple(*right_it,j));
+              right_tuple.push_back(RelsUtils::nthElementOfTuple(*right_it,j));
             }
             std::vector<Node> new_tuple;
             new_tuple.insert(new_tuple.end(), left_tuple.begin(), left_tuple.end());
@@ -300,7 +301,13 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     if(node[0].getKind() == kind::EMPTYSET) {
       return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
     } else if (node[0].isConst()) {
-
+      std::set<Node> rel_mems = NormalForm::getElementsFromNormalConstant(node[0]);
+      std::set<Node> tc_rel_mems = RelsUtils::computeTC(rel_mems, node);
+      Node new_node = NormalForm::elementsToSet(tc_rel_mems, node.getType());
+      Assert(new_node.isConst());
+      Trace("sets-postrewrite") << "Sets::postRewrite returning " << new_node << std::endl;
+      return RewriteResponse(REWRITE_DONE, new_node);
+      
     } else if(node[0].getKind() == kind::TCLOSURE) {
       return RewriteResponse(REWRITE_AGAIN, node[0]);
     } else if(node[0].getKind() != kind::TCLOSURE) {