change transitive closure operator name to TCLOUSRE

diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644 (file)
index 0000000..44d6fcb
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,4 @@
+// Place your settings in this file to overwrite default and user settings.
+{
+    "editor.fontSize": 18
+}
\ No newline at end of file

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 27182cb6de18f3ecc6692b60b46fea99bd0a6fbb..967503074bc3fc45545072fbaf2e72c76895f518 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -208,7 +208,7 @@ tokens {
   JOIN_TOK = 'JOIN';
   TRANSPOSE_TOK = 'TRANSPOSE';
   PRODUCT_TOK = 'PRODUCT';
-  TRANSCLOSURE_TOK = 'TRANSCLOSURE';
+  TRANSCLOSURE_TOK = 'TCLOSURE';
 
   // Strings
 
@@ -1649,7 +1649,7 @@ bvNegTerm[CVC4::Expr& f]
   | TRANSPOSE_TOK bvNegTerm[f]
     { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
   | TRANSCLOSURE_TOK bvNegTerm[f]
-    { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); }
+    { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
   | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN
     { std::vector<Type> types;
       std::vector<Expr> args;

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 530e9da8b58e787e7fe0143208a13504da5f3466..ff22dd9c7c22fd1b9724f1d2d912b9432f166071 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -225,7 +225,7 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::SUBSET, "subset");
     addOperator(kind::MEMBER, "member");
     addOperator(kind::TRANSPOSE, "transpose");
-    addOperator(kind::TRANSCLOSURE, "transclosure");
+    addOperator(kind::TCLOSURE, "tclosure");
     addOperator(kind::JOIN, "join");
     addOperator(kind::PRODUCT, "product");
     addOperator(kind::SINGLETON, "singleton");

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 58835d4e6220df68bd4c4a0c8af8f864f12cf5c5..9de790d7b803e4709645c58849d6964add3ffe49 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -780,8 +780,8 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << "TRANSPOSE";
       opType = PREFIX;
       break;
-    case kind::TRANSCLOSURE:
-      op << "TRANSCLOSURE";
+    case kind::TCLOSURE:
+      op << "TCLOSURE";
       opType = PREFIX;
       break;
     case kind::SINGLETON:

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d37f4ae999cacd8f9b9dad6487146c6baa826a96..7c501ffecc6f86834be6e876d72b5674f7d55377 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -505,7 +505,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::SUBSET:
   case kind::MEMBER:
   case kind::SET_TYPE:
-  case kind::TRANSCLOSURE:
+  case kind::TCLOSURE:
   case kind::TRANSPOSE:
   case kind::JOIN:
   case kind::PRODUCT:
@@ -786,7 +786,7 @@ static string smtKindString(Kind k) throw() {
   case kind::SET_TYPE: return "Set";
   case kind::SINGLETON: return "singleton";
   case kind::INSERT: return "insert";
-  case kind::TRANSCLOSURE: return "transclosure";
+  case kind::TCLOSURE: return "tclosure";
   case kind::TRANSPOSE: return "transpose";
   case kind::PRODUCT: return "product";
   case kind::JOIN: return "join";

diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 6767de4815f59d8b8388fe956d54d2e75a783e22..efd00093aca83d1db86c11929b1e53fa5205dedf 100644 (file)
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -46,7 +46,7 @@ operator INSERT        2: "set obtained by inserting elements (first N-1 paramet
 operator JOIN             2  "set join"
 operator PRODUCT          2  "set cartesian product"
 operator TRANSPOSE        1  "set transpose"
-operator TRANSCLOSURE  1  "set transitive closure"
+operator TCLOSURE      1  "set transitive closure"
 
 typerule UNION          ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
@@ -60,7 +60,7 @@ typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
 typerule JOIN                  ::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule PRODUCT               ::CVC4::theory::sets::RelBinaryOperatorTypeRule
 typerule TRANSPOSE             ::CVC4::theory::sets::RelTransposeTypeRule
-typerule TRANSCLOSURE  ::CVC4::theory::sets::RelTransClosureTypeRule
+typerule TCLOSURE          ::CVC4::theory::sets::RelTransClosureTypeRule
 
 construle UNION         ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 construle INTERSECTION  ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
@@ -71,6 +71,6 @@ construle INSERT        ::CVC4::theory::sets::InsertTypeRule
 construle JOIN                         ::CVC4::theory::sets::RelBinaryOperatorTypeRule
 construle PRODUCT              ::CVC4::theory::sets::RelBinaryOperatorTypeRule
 construle TRANSPOSE    ::CVC4::theory::sets::RelTransposeTypeRule
-construle TRANSCLOSURE         ::CVC4::theory::sets::RelTransClosureTypeRule
+construle TCLOSURE         ::CVC4::theory::sets::RelTransClosureTypeRule
 
 endtheory

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index db4f4bf26d3943c3862aebf887e9d0603c6e0bf8..434202a53a146fdb90862016ff6bc2501906e715 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -782,7 +782,7 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap,
       Trace("rels-debug") << " ***** Done with check model for JOIN operator" << std::endl;
       break;
     }
-    case kind::TRANSCLOSURE:
+    case kind::TCLOSURE:
       break;
     default:
       Unhandled();

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index eae9a4e8fa18f5ec982452b4de1e00b99dd1f811..a1a799f4b85573dca3582cf38930bb3f64d80456 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -67,8 +67,6 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
         Node tp_rel_rep = getRepresentative(tp_rel);
         if(d_terms_cache.find(tp_rel_rep) != d_terms_cache.end()) {
           for(unsigned int i = 0; i < m_it->second.size(); i++) {
-//            Node exp = tp_rel == tp_rel_rep ? d_membership_exp_cache[rel_rep][i]
-//                                            : AND(d_membership_exp_cache[rel_rep][i], EQUAL(tp_rel, tp_rel_rep));
             // Lazily apply transpose-occur rule.
             // Need to eagerly apply if we don't send facts as lemmas
             applyTransposeRule(d_membership_exp_cache[rel_rep][i], tp_rel_rep, true);
@@ -100,8 +98,8 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
               applyProductRule(exp, product_terms[j]);
             }
           }
-          if(kind_terms.find(kind::TRANSCLOSURE) != kind_terms.end()) {
-            std::vector<Node> tc_terms = kind_terms[kind::TRANSCLOSURE];
+          if(kind_terms.find(kind::TCLOSURE) != kind_terms.end()) {
+            std::vector<Node> tc_terms = kind_terms[kind::TCLOSURE];
             for(unsigned int j = 0; j < tc_terms.size(); j++) {
               applyTCRule(exp, tc_terms[j]);
             }
@@ -153,7 +151,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
           if( n.getKind() == kind::TRANSPOSE ||
               n.getKind() == kind::JOIN ||
               n.getKind() == kind::PRODUCT ||
-              n.getKind() == kind::TRANSCLOSURE ) {
+              n.getKind() == kind::TCLOSURE ) {
             std::map<kind::Kind_t, std::vector<Node> > rel_terms;
             std::vector<Node> terms;
             // No r record is found
@@ -190,15 +188,15 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
   /*
    *
    *
-   * transitive closure rule 1:   y = (TRANSCLOSURE x)
+   * transitive closure rule 1:   y = (TCLOSURE x)
    *                           ---------------------------------------------
    *                              y = x | x.x | x.x.x | ... (| is union)
    *
    *
    *
-   * transitive closure rule 2:   TRANSCLOSURE(x)
+   * transitive closure rule 2:   TCLOSURE(x)
    *                            -----------------------------------------------------------
-   *                              x <= TRANSCLOSURE(x) && (x JOIN x) <= TRANSCLOSURE(x) ....
+   *                              x <= TCLOSURE(x) && (x JOIN x) <= TCLOSURE(x) ....
    *
    *                              TC(x) = TC(y) => x = y ?
    *
@@ -984,7 +982,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
   // tc_terms are transitive closure of rels and are modulo equal to tc_rep
   Node TheorySetsRels::findMemExp(Node tc_rep, Node tuple) {
     Trace("rels-exp") << "TheorySetsRels::findMemExp ( tc_rep = " << tc_rep << ", tuple = " << tuple << ")" << std::endl;
-    std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TRANSCLOSURE];
+    std::vector<Node> tc_terms = d_terms_cache.find(tc_rep)->second[kind::TCLOSURE];
     Assert(tc_terms.size() > 0);
     for(unsigned int i = 0; i < tc_terms.size(); i++) {
       Node tc_term = tc_terms[i];
@@ -1054,7 +1052,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     return Node::null();
   }
 
-  Node TheorySetsRels::nthElementOfTuple( Node tuple, int n_th ) {
+  Node TheorySetsRels::nthElementOfTuple( Node tuple, int n_th ) {    
     if(tuple.isConst() || (!tuple.isVar() && !tuple.isConst()))
       return tuple[n_th];
     Datatype dt = tuple.getType().getDatatype();
@@ -1159,7 +1157,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
     d_eqEngine->addFunctionKind(kind::PRODUCT);
     d_eqEngine->addFunctionKind(kind::JOIN);
     d_eqEngine->addFunctionKind(kind::TRANSPOSE);
-    d_eqEngine->addFunctionKind(kind::TRANSCLOSURE);
+    d_eqEngine->addFunctionKind(kind::TCLOSURE);
   }
 
   TheorySetsRels::~TheorySetsRels() {}
@@ -1188,7 +1186,7 @@ typedef std::map< Node, std::hash_set< Node, NodeHashFunction > >::iterator TC_P
 
   Node TupleTrie::existsTerm( std::vector< Node >& reps, int argIndex ) {
     if( argIndex==(int)reps.size() ){
-      if( d_data.empty() ){
+      if( d_data.empty() ){        
         return Node::null();
       }else{
         return d_data.begin()->first;

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 61ec07e9da7edfc8cd2e9eb74174ecf5f42cefc8..4c22f588d75b081a3d877d6046f32d23dd117928 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -296,14 +296,14 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
     break;
   }
 
-  case kind::TRANSCLOSURE: {
+  case kind::TCLOSURE: {
     if(node[0].getKind() == kind::EMPTYSET) {
       return RewriteResponse(REWRITE_DONE, nm->mkConst(EmptySet(nm->toType(node.getType()))));
     } else if (node[0].isConst()) {
 
-    } else if(node[0].getKind() == kind::TRANSCLOSURE) {
+    } else if(node[0].getKind() == kind::TCLOSURE) {
       return RewriteResponse(REWRITE_AGAIN, node[0]);
-    } else if(node[0].getKind() != kind::TRANSCLOSURE) {
+    } else if(node[0].getKind() != kind::TCLOSURE) {
       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 22127ad503cbc2b23828630371fa463a610832d6..fdcb094fc953a52b7e371b495e03515e52b5f454 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -233,7 +233,7 @@ struct RelTransposeTypeRule {
 struct RelTransClosureTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw (TypeCheckingExceptionPrivate, AssertionException) {
-    Assert(n.getKind() == kind::TRANSCLOSURE);
+    Assert(n.getKind() == kind::TCLOSURE);
     TypeNode setType = n[0].getType(check);
     if(check) {
       if(!setType.isSet() && !setType.getSetElementType().isTuple()) {
@@ -251,7 +251,7 @@ struct RelTransClosureTypeRule {
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-      Assert(n.getKind() == kind::TRANSCLOSURE);
+      Assert(n.getKind() == kind::TCLOSURE);
       return false;
     }
 };/* struct RelTransClosureTypeRule */