From: Tim King <taking@google.com>
Date: Wed, 31 Aug 2016 22:54:23 +0000 (-0700)
Subject: Removing typeof from sets normal form and beautifying the file.
X-Git-Tag: cvc5-1.0.0~6028^2~72
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16d27018ed668adbeaddc68795a3f0cbcc48a1e9;p=cvc5.git

Removing typeof from sets normal form and beautifying the file.
---

diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 6da7e9f8f..c1f05ae85 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -24,58 +24,64 @@ namespace theory {
 namespace sets {
 
 class NormalForm {
-public:
-
-  template<bool ref_count>
-  static Node elementsToSet(std::set<NodeTemplate<ref_count> > elements, TypeNode setType)
-  {
+ public:
+  template <bool ref_count>
+  static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements,
+                            TypeNode setType) {
+    typedef typename std::set<NodeTemplate<ref_count> >::const_iterator
+        ElementsIterator;
     NodeManager* nm = NodeManager::currentNM();
-
-    if(elements.size() == 0) {
+    if (elements.size() == 0) {
       return nm->mkConst(EmptySet(nm->toType(setType)));
     } else {
-      typeof(elements.begin()) it = elements.begin();
+      ElementsIterator 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));
+      while (++it != elements.end()) {
+        cur = nm->mkNode(kind::UNION, cur, nm->mkNode(kind::SINGLETON, *it));
       }
       return cur;
     }
   }
 
   static bool checkNormalConstant(TNode n) {
-    Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :" << std::endl;
-    if(n.getKind() == kind::EMPTYSET) {
+    Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :"
+                              << std::endl;
+    if (n.getKind() == kind::EMPTYSET) {
       return true;
-    } else if(n.getKind() == kind::SINGLETON) {
+    } else if (n.getKind() == kind::SINGLETON) {
       return n[0].isConst();
-    } else if(n.getKind() == kind::UNION) {
-
-      // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ... {BiggestNodeId})
+    } else if (n.getKind() == kind::UNION) {
+      // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ...
+      // {BiggestNodeId})
 
       // store BiggestNodeId in prvs
-      if(n[1].getKind() != kind::SINGLETON) return false;
-      if( !n[1][0].isConst() ) return false;
-      Debug("sets-checknormal") << "[sets-checknormal]              frst element = " << n[1][0] << " " << n[1][0].getId() << std::endl;
+      if (n[1].getKind() != kind::SINGLETON) return false;
+      if (!n[1][0].isConst()) return false;
+      Debug("sets-checknormal")
+          << "[sets-checknormal]              frst element = " << n[1][0] << " "
+          << n[1][0].getId() << std::endl;
       TNode prvs = n[1][0];
       n = n[0];
 
       // check intermediate nodes
-      while(n.getKind() == kind::UNION) {
-	if(n[1].getKind() != kind::SINGLETON) return false;
-	if( !n[1].isConst() ) return false;
-	Debug("sets-checknormal") << "[sets-checknormal]              element = " << n[1][0] << " " << n[1][0].getId() << std::endl;
-	if( n[1][0] >= prvs ) return false;
-	TNode prvs = n[1][0];
-	n = n[0];
+      while (n.getKind() == kind::UNION) {
+        if (n[1].getKind() != kind::SINGLETON) return false;
+        if (!n[1].isConst()) return false;
+        Debug("sets-checknormal")
+            << "[sets-checknormal]              element = " << n[1][0] << " "
+            << n[1][0].getId() << std::endl;
+        if (n[1][0] >= prvs) return false;
+        TNode prvs = n[1][0];
+        n = n[0];
       }
 
       // check SmallestNodeID is smallest
-      if(n.getKind() != kind::SINGLETON) return false;
-      if( !n[0].isConst() ) return false;
-      Debug("sets-checknormal") << "[sets-checknormal]              lst element = " << n[0] << " " << n[0].getId() << std::endl;
-      if( n[0] >= prvs ) return false;
+      if (n.getKind() != kind::SINGLETON) return false;
+      if (!n[0].isConst()) return false;
+      Debug("sets-checknormal")
+          << "[sets-checknormal]              lst element = " << n[0] << " "
+          << n[0].getId() << std::endl;
+      if (n[0] >= prvs) return false;
 
       // we made it
       return true;
@@ -88,10 +94,10 @@ public:
   static std::set<Node> getElementsFromNormalConstant(TNode n) {
     Assert(n.isConst());
     std::set<Node> ret;
-    if(n.getKind() == kind::EMPTYSET) {
+    if (n.getKind() == kind::EMPTYSET) {
       return ret;
     }
-    while(n.getKind() == kind::UNION) {
+    while (n.getKind() == kind::UNION) {
       Assert(n[1].getKind() == kind::SINGLETON);
       ret.insert(ret.begin(), n[1][0]);
       n = n[0];
@@ -100,9 +106,7 @@ public:
     ret.insert(n[0]);
     return ret;
   }
-
 };
-
 }
 }
 }