From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 20 Oct 2014 00:06:47 +0000 (-0400)
Subject: Finish sets type enumerator implementation.
X-Git-Tag: cvc5-1.0.0~6550^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4114f4faaab9ade220cbebed0b8be4d4282d5280;p=cvc5.git

Finish sets type enumerator implementation.
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 3e0831467..d82c0945d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -239,6 +239,7 @@ libcvc4_la_SOURCES = \
 	theory/datatypes/datatypes_rewriter.h \
 	theory/datatypes/theory_datatypes.cpp \
 	theory/sets/expr_patterns.h \
+	theory/sets/normal_form.h \
 	theory/sets/options_handlers.h \
 	theory/sets/scrutinize.h \
 	theory/sets/term_info.h \
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
new file mode 100644
index 000000000..bc34ea6f1
--- /dev/null
+++ b/src/theory/sets/normal_form.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file normal_form.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Normal form for set constants.
+ **
+ ** Normal form for set constants.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__NORMAL_FORM_H
+#define __CVC4__THEORY__SETS__NORMAL_FORM_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class NormalForm {
+public:
+
+  static Node elementsToSet(std::set<TNode> elements, TypeNode setType)
+  {
+    NodeManager* nm = NodeManager::currentNM();
+
+    if(elements.size() == 0) {
+      return nm->mkConst(EmptySet(nm->toType(setType)));
+    } else {
+      typeof(elements.begin()) it = elements.begin();
+      Node cur = nm->mkNode(kind::SINGLETON, *it);
+      while( ++it != elements.end() ) {
+        cur = nm->mkNode(kind::UNION, cur,
+                         nm->mkNode(kind::SINGLETON, *it));
+      }
+      return cur;
+    }
+  }
+
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 01ad51733..226eca62b 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/sets/theory_sets_rewriter.h"
+#include "theory/sets/normal_form.h"
 
 namespace CVC4 {
 namespace theory {
@@ -210,25 +211,6 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
   return it->second;
 }
 
-Node elementsToNormalConstant(Elements elements,
-                              TypeNode setType)
-{
-  NodeManager* nm = NodeManager::currentNM();
-
-  if(elements.size() == 0) {
-    return nm->mkConst(EmptySet(nm->toType(setType)));
-  } else {
-
-    Elements::iterator it = elements.begin();
-    Node cur = nm->mkNode(kind::SINGLETON, *it);
-    while( ++it != elements.end() ) {
-      cur = nm->mkNode(kind::UNION, cur,
-                       nm->mkNode(kind::SINGLETON, *it));
-    }
-    return cur;
-  }
-}
-
 
 // static
 RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
@@ -252,7 +234,7 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     //rewrite set to normal form
     SettermElementsMap setTermElementsMap;   // cache
     const Elements& elements = collectConstantElements(node, setTermElementsMap);
-    RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    RewriteResponse response(REWRITE_DONE, NormalForm::elementsToSet(elements, node.getType()));
     Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl
                                    << "[sets-rewrite-constant]        to " << response.node << std::endl;
     return response;
diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index 5d14006bb..718c329fd 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -25,6 +25,7 @@
 #include "expr/type_node.h"
 #include "expr/kind.h"
 #include "theory/rewriter.h"
+#include "theory/sets/normal_form.h"
 
 namespace CVC4 {
 namespace theory {
@@ -87,21 +88,17 @@ public:
     if (d_finished) {
       throw NoMoreValuesException(getType());
     }
-    Node n = d_setConst;
 
-    // For now only support only sets of size 1
-    Assert(d_index == 0 || d_index == 1);
-
-    if(d_index == 1) {
-      n = d_nm->mkNode(kind::SINGLETON, *(*(d_constituentVec[0])));
+    std::vector<Node> elements;
+    for(unsigned i = 0; i < d_constituentVec.size(); ++i) {
+      elements.push_back(*(*(d_constituentVec[i])));
     }
 
-    // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
-    //   n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
-    // }
-    Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
-    n = Rewriter::rewrite(n);
-    Trace("set-type-enum") << "operator * returning: " << n << std::endl;
+    Node n = NormalForm::elementsToSet(std::set<TNode>(elements.begin(), elements.end()),
+                                       getType());
+
+    Assert(n == Rewriter::rewrite(n));
+
     return n;
   }