Reflowing code as per agreed clang-format

Note: only difference is that comments have been asked of clang not to
be re-flown much, as it interferes with comments sometimes. No other
change.

.clang-format

@@ -12,6 +12,9 @@ IndentCaseLabels: true
 PointerAlignment: Left
 IndentWidth: 2
 TabWidth: 2
+ReflowComments:  false
+SpacesBeforeTrailingComments: 1
+PenaltyBreakComment: 1300
 # Although LLVM doesn't use tabs either I want to be **very** explicit about this
 UseTab: Never
 ...

include/stp/AST/AST.h

@@ -25,21 +25,22 @@ THE SOFTWARE.
 #ifndef AST_H
 #define AST_H
 
-#include "UsefulDefs.h"
 #include "ASTNode.h"
+#include "UsefulDefs.h"
 #include "stp/Util/Attributes.h"
 
 namespace stp
 {
-DLL_PUBLIC ATTR_NORETURN void FatalError(const char* str, const ASTNode& a, int w = 0);
+DLL_PUBLIC ATTR_NORETURN void FatalError(const char* str, const ASTNode& a,
+                                         int w = 0);
 DLL_PUBLIC ATTR_NORETURN void FatalError(const char* str);
 void SortByExprNum(ASTVec& c);
 void SortByArith(ASTVec& c);
 bool exprless(const ASTNode n1, const ASTNode n2);
 bool arithless(const ASTNode n1, const ASTNode n2);
 bool isAtomic(Kind k);
 bool isCommutative(const Kind k);
-bool containsArrayOps(const ASTNode& n, STPMgr *stp);
+bool containsArrayOps(const ASTNode& n, STPMgr* stp);
 bool numberOfReadsLessThan(const ASTNode& n, int v);
 
 // If (a > b) in the termorder, then return 1 elseif (a < b) in the
@@ -66,18 +67,23 @@ bool BVTypeCheckRecursive(const ASTNode& n);
 unsigned int GetUnsignedConst(const ASTNode n);
 
 typedef std::unordered_map<ASTNode, ASTNode, ASTNode::ASTNodeHasher,
-                 ASTNode::ASTNodeEqual> ASTNodeMap;
+                           ASTNode::ASTNodeEqual>
+    ASTNodeMap;
 
 typedef std::unordered_map<ASTNode, int32_t, ASTNode::ASTNodeHasher,
-                 ASTNode::ASTNodeEqual> ASTNodeCountMap;
+                           ASTNode::ASTNodeEqual>
+    ASTNodeCountMap;
 
-typedef std::unordered_set<ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual>
+typedef std::unordered_set<ASTNode, ASTNode::ASTNodeHasher,
+                           ASTNode::ASTNodeEqual>
     ASTNodeSet;
 
-typedef std::unordered_multiset<ASTNode, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual>
+typedef std::unordered_multiset<ASTNode, ASTNode::ASTNodeHasher,
+                                ASTNode::ASTNodeEqual>
     ASTNodeMultiSet;
 
-typedef std::unordered_map<ASTNode, ASTVec, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual>
+typedef std::unordered_map<ASTNode, ASTVec, ASTNode::ASTNodeHasher,
+                           ASTNode::ASTNodeEqual>
     ASTNodeToVecMap;
 
 void FlattenKindNoDuplicates(const Kind k, const ASTVec& children,

include/stp/AST/ASTBVConst.h

@@ -64,14 +64,17 @@ class ASTBVConst : public ASTInternal
     bool operator()(const ASTBVConst* bvc1, const ASTBVConst* bvc2) const;
   };
 
-
   ASTBVConst(CBV bv, unsigned int width);
-  ASTBVConst(STPMgr * mgr, CBV bv, unsigned int /*width*/, bool managed_outside = false)
+  ASTBVConst(STPMgr* mgr, CBV bv, unsigned int /*width*/,
+             bool managed_outside = false)
       : ASTInternal(mgr, BVCONST)
   {
-    if (managed_outside) {
+    if (managed_outside)
+    {
       _bvconst = (bv);
-    } else {
+    }
+    else
+    {
       _bvconst = CONSTANTBV::BitVector_Clone(bv);
     }
     cbv_managed_outside = managed_outside;
@@ -98,12 +101,11 @@ class ASTBVConst : public ASTInternal
 
   const static ASTVec astbv_empty_children;
 
-  void setIndexWidth(uint32_t i)  { assert(i==0);}
-  uint32_t getIndexWidth() const {return 0;}
-
-  void setValueWidth(uint32_t v ) { assert(v == getValueWidth());}
-  uint32_t getValueWidth()  const {return bits_(_bvconst);}
+  void setIndexWidth(uint32_t i) { assert(i == 0); }
+  uint32_t getIndexWidth() const { return 0; }
 
+  void setValueWidth(uint32_t v) { assert(v == getValueWidth()); }
+  uint32_t getValueWidth() const { return bits_(_bvconst); }
 
 public:
   virtual ASTVec const& GetChildren() const { return astbv_empty_children; }

include/stp/AST/ASTInterior.h

@@ -25,9 +25,9 @@ THE SOFTWARE.
 #ifndef ASTINTERIOR_H
 #define ASTINTERIOR_H
 
-#include "UsefulDefs.h"
 #include "ASTInternal.h"
 #include "NodeFactory/HashingNodeFactory.h"
+#include "UsefulDefs.h"
 
 namespace stp
 {
@@ -90,32 +90,34 @@ class ASTInterior : public ASTInternal
 
   uint32_t _value_width;
   uint32_t _index_width;
-
-  virtual void setIndexWidth(uint32_t i)  { _index_width =i;}
-  virtual uint32_t getIndexWidth() const {return _index_width;}
-
-  virtual void setValueWidth(uint32_t v) {_value_width=v; }
-  virtual uint32_t getValueWidth() const  {return _value_width;}
 
+  virtual void setIndexWidth(uint32_t i) { _index_width = i; }
+  virtual uint32_t getIndexWidth() const { return _index_width; }
+
+  virtual void setValueWidth(uint32_t v) { _value_width = v; }
+  virtual uint32_t getValueWidth() const { return _value_width; }
 
 public:
-  ASTInterior(STPMgr *mgr, Kind kind, ASTVec& children)
-      : ASTInternal(mgr, kind), _children(children), _value_width(0), _index_width(0)
+  ASTInterior(STPMgr* mgr, Kind kind, ASTVec& children)
+      : ASTInternal(mgr, kind), _children(children), _value_width(0),
+        _index_width(0)
   {
     is_simplified = false;
     if (kind == NOT)
-      node_uid = children[0].GetNodeNum()+1;
+      node_uid = children[0].GetNodeNum() + 1;
   }
 
   // This copies the contents of the child nodes
   // array, along with everything else. Assigning the smart pointer,
   // ASTNode, does NOT invoke this.
-  ASTInterior(const ASTInterior& int_node) : ASTInternal(int_node), _children(int_node._children), _value_width(int_node._value_width), _index_width(int_node._index_width)
+  ASTInterior(const ASTInterior& int_node)
+      : ASTInternal(int_node), _children(int_node._children),
+        _value_width(int_node._value_width), _index_width(int_node._index_width)
   {
     is_simplified = false;
   }
 
-  ASTInterior & operator= (const ASTInterior & other) =delete;
+  ASTInterior& operator=(const ASTInterior& other) = delete;
 
   virtual ~ASTInterior();
 

include/stp/AST/ASTInternal.h

@@ -24,9 +24,9 @@ THE SOFTWARE.
 #ifndef ASTINTERNAL_H
 #define ASTINTERNAL_H
 
-#include <iostream>
 #include "stp/AST/ASTNode.h"
 #include "stp/AST/UsefulDefs.h"
+#include <iostream>
 
 using std::ostream;
 
@@ -65,14 +65,14 @@ class ASTInternal
 
 protected:
   // Pointer back to the node manager that holds this.
-  STPMgr * nodeManager;
+  STPMgr* nodeManager;
 
   // node_uid is a unique positive integer for the node.  The node_uid
   // of a node should always be greater than its descendents (which
   // is easily achieved by incrementing the number each time a new
   // node is created). NOT nodes are odd, and one more than the thing
   // the are NOTs of.
-  // 
+  //
   uint64_t node_uid;
   static THREAD_LOCAL uint64_t node_uid_cntr;
 
@@ -88,7 +88,7 @@ class ASTInternal
    *******************************************************************/
   virtual void setIndexWidth(uint32_t) = 0;
   virtual uint32_t getIndexWidth() const = 0;
-  
+
   virtual void setValueWidth(uint32_t) = 0;
   virtual uint32_t getValueWidth() const = 0;
 
@@ -136,8 +136,8 @@ class ASTInternal
 public:
   // Constructor (kind only, empty children, int nodenum)
   ASTInternal(STPMgr* mgr, Kind kind)
-      : nodeManager(mgr), node_uid(node_uid_cntr+=2),
-         _ref_count(0), _kind(kind), iteration(0)
+      : nodeManager(mgr), node_uid(node_uid_cntr += 2), _ref_count(0),
+        _kind(kind), iteration(0)
   {
   }
 
@@ -148,7 +148,7 @@ class ASTInternal
   // FIXME:  I don't think children need to be copied.
   ASTInternal(const ASTInternal& int_node)
       : nodeManager(int_node.nodeManager), node_uid(int_node.node_uid),
-         _ref_count(0), _kind(int_node._kind), iteration(0)
+        _ref_count(0), _kind(int_node._kind), iteration(0)
 
   {
   }

include/stp/AST/ASTNode.h

@@ -24,13 +24,15 @@ THE SOFTWARE.
 #ifndef ASTNODE_H
 #define ASTNODE_H
 
-#include "stp/AST/ASTInternal.h"
 #include "stp/AST/NodeFactory/HashingNodeFactory.h"
 #include "stp/Util/Attributes.h"
+#include "ASTInternal.h"
+#include "stp/Globals/Globals.h"
 
 namespace stp
 {
 using std::ostream;
+class ASTInternal;
 
 /******************************************************************
  *  A Kind of Smart pointer to actual ASTInternal datastructure.  *
@@ -44,7 +46,7 @@ class ASTNode
   friend class ASTInterior;
   friend class vector<ASTNode>;
   friend ASTNode HashingNodeFactory::CreateNode(const stp::Kind kind,
-                                             const ASTVec& back_children);
+                                                const ASTVec& back_children);
   friend bool exprless(const ASTNode n1, const ASTNode n2);
   friend bool arithless(const ASTNode n1, const ASTNode n2);
 
@@ -69,7 +71,7 @@ class ASTNode
     return (node1.Hash() < node2.Hash());
   }
 
-  STPMgr * GetSTPMgr() const;
+  STPMgr* GetSTPMgr() const;
 
 public:
   static THREAD_LOCAL int copy;
@@ -84,7 +86,7 @@ class ASTNode
   DLL_PUBLIC ASTNode() : _int_node_ptr(NULL){};
   DLL_PUBLIC ASTNode(const ASTNode& n);
   DLL_PUBLIC ~ASTNode();
-  DLL_PUBLIC ASTNode ( ASTNode && other ) noexcept;
+  DLL_PUBLIC ASTNode(ASTNode&& other) noexcept;
 
   // Print the arguments in lisp format
   friend ostream& LispPrintVec(ostream& os, const ASTVec& v, int indentation);
@@ -104,7 +106,7 @@ class ASTNode
   bool isITE() const
   {
     Kind k = GetKind();
-    return k== ITE;
+    return k == ITE;
   }
 
   bool isAtom() const
@@ -116,8 +118,8 @@ class ASTNode
   bool isPred() const
   {
     const Kind k = GetKind();
-    return k == BVLT || k == BVLE || k == BVGT || k == BVGE ||
-            k == BVSLT || k == BVSLE || k == BVSGT || k == BVSGE || k == EQ;
+    return k == BVLT || k == BVLE || k == BVGT || k == BVGE || k == BVSLT ||
+           k == BVSLE || k == BVSGT || k == BVSGE || k == EQ;
   }
 
   // delegates to the ASTInternal node.
@@ -126,7 +128,7 @@ class ASTNode
   // Assignment (for ref counting)
   DLL_PUBLIC ASTNode& operator=(const ASTNode& n);
   DLL_PUBLIC ASTNode& operator=(ASTNode&& n);
-  
+
   // Access node number
   unsigned GetNodeNum() const;
 
@@ -176,7 +178,7 @@ class ASTNode
   types GetType(void) const;
 
   // Hash using pointer value of _int_node_ptr.
-  DLL_PUBLIC size_t Hash() const ;
+  DLL_PUBLIC size_t Hash() const;
 
   void NFASTPrint(int l, int max, int prefix) const;
 
@@ -185,8 +187,8 @@ class ASTNode
   ostream& LispPrint_indent(ostream& os, int indentation) const;
 
   // Presentation Language Printer
-  ostream& PL_Print(ostream& os , STPMgr *mgr, int indentation = 0) const;
-  ostream& PL_Print(ostream& os , int /*indentation = 0*/) const
+  ostream& PL_Print(ostream& os, STPMgr* mgr, int indentation = 0) const;
+  ostream& PL_Print(ostream& os, int /*indentation = 0*/) const
   {
     return PL_Print(os, GetSTPMgr(), 0);
   }
@@ -236,7 +238,6 @@ class ASTNode
       return (n1.Hash() == n2.Hash());
     }
   };
-
 };
 
 } // end of namespace

include/stp/AST/ASTSymbol.h

@@ -25,8 +25,8 @@ THE SOFTWARE.
 #ifndef ASTSYMBOL_H
 #define ASTSYMBOL_H
 
-#include "stp/Util/StringHash.h"
 #include "stp/AST/ASTInternal.h"
+#include "stp/Util/StringHash.h"
 
 namespace stp
 {
@@ -88,28 +88,28 @@ class ASTSymbol : public ASTInternal
 
   uint32_t _value_width;
   uint32_t _index_width;
-
-  virtual void setIndexWidth(uint32_t i)  { _index_width =i;}
-  virtual uint32_t getIndexWidth() const {return _index_width;}
-
-  virtual void setValueWidth(uint32_t v) {_value_width=v; }
-  virtual uint32_t getValueWidth()  const {return _value_width;}
-
 
+  virtual void setIndexWidth(uint32_t i) { _index_width = i; }
+  virtual uint32_t getIndexWidth() const { return _index_width; }
 
+  virtual void setValueWidth(uint32_t v) { _value_width = v; }
+  virtual uint32_t getValueWidth() const { return _value_width; }
 
 public:
   virtual ASTVec const& GetChildren() const { return empty_children; }
 
   // Constructor.  This does NOT copy its argument.
-  ASTSymbol(STPMgr *mgr, const char* const name) : ASTInternal(mgr, SYMBOL),
-     _name(name), _value_width(0), _index_width(0) {}
+  ASTSymbol(STPMgr* mgr, const char* const name)
+      : ASTInternal(mgr, SYMBOL), _name(name), _value_width(0), _index_width(0)
+  {
+  }
 
   virtual ~ASTSymbol() {}
 
   // Copy constructor
-  ASTSymbol(const ASTSymbol& sym) : ASTInternal(sym.nodeManager, sym._kind),
-     _name(sym._name), _value_width(sym._value_width), _index_width(sym._index_width)
+  ASTSymbol(const ASTSymbol& sym)
+      : ASTInternal(sym.nodeManager, sym._kind), _name(sym._name),
+        _value_width(sym._value_width), _index_width(sym._index_width)
   {
     // printf("inside ASTSymbol constructor %s\n", _name);
   }

include/stp/AST/MutableASTNode.h

@@ -149,13 +149,12 @@ class MutableASTNode
 
     if (n.GetType() == BOOLEAN_TYPE)
     {
-      n = stpMgr->hashingNodeFactory->CreateNode(n.GetKind(),
-                                                        newChildren);
+      n = stpMgr->hashingNodeFactory->CreateNode(n.GetKind(), newChildren);
     }
     else if (n.GetType() == BITVECTOR_TYPE)
     {
-      n = stpMgr->hashingNodeFactory->CreateTerm(
-          n.GetKind(), n.GetValueWidth(), newChildren);
+      n = stpMgr->hashingNodeFactory->CreateTerm(n.GetKind(), n.GetValueWidth(),
+                                                 newChildren);
     }
     else
     {

include/stp/AST/NodeFactory/HashingNodeFactory.h

@@ -35,10 +35,9 @@ class HashingNodeFactory : public NodeFactory
   DLL_PUBLIC HashingNodeFactory(STPMgr& bm_) : NodeFactory(bm_) {}
   DLL_PUBLIC virtual ~HashingNodeFactory();
 
-  DLL_PUBLIC ASTNode CreateNode(const Kind kind,
-                           const ASTVec& back_children);
+  DLL_PUBLIC ASTNode CreateNode(const Kind kind, const ASTVec& back_children);
   DLL_PUBLIC ASTNode CreateTerm(Kind kind, unsigned int width,
-                           const ASTVec& children);
+                                const ASTVec& children);
 
   virtual std::string getName() { return "hashing"; }
 };