Move functions around so that clang links.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1363 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index b050a51e072826fa4989e96bd36628e7401cd714..84bca7e197d72718aec388573d27ec808efdfe1f 100644 (file)
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -22,6 +22,7 @@ namespace BEEV
    *  This class defines the node datastructure for the DAG that    *
    *  captures input formulas to STP.                               *
    ******************************************************************/
+
   class ASTNode
   {
     friend class STPMgr;
@@ -29,6 +30,8 @@ namespace BEEV
     friend class ASTInterior;
     friend class vector<ASTNode>;
     friend BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind,       const BEEV::ASTVec & back_children);
+    friend bool exprless(const ASTNode n1, const ASTNode n2);
+    friend bool arithless(const ASTNode n1, const ASTNode n2);
 
   private:
     /****************************************************************
@@ -95,52 +98,6 @@ namespace BEEV
       return _int_node_ptr == NULL;
     }
 
-    // Sort ASTNodes by expression numbers
-    friend bool exprless(const ASTNode n1, const ASTNode n2)
-    {
-      return (n1.GetNodeNum() < n2.GetNodeNum());
-    }
-
-    // This is for sorting by arithmetic expressions (for
-    // combining like terms, etc.)
-    friend bool arithless(const ASTNode n1, const ASTNode n2)
-    {
-      Kind k1 = n1.GetKind();
-      Kind k2 = n2.GetKind();
-
-      if (n1 == n2)
-        {
-          // necessary for "strict weak ordering"
-          return false;
-        }
-      else if (BVCONST == k1 && BVCONST != k2)
-        {
-          // put consts first
-          return true;
-        }
-      else if (BVCONST != k1 && BVCONST == k2)
-        {
-          // put consts first
-          return false;
-        }
-      else if (SYMBOL == k1 && SYMBOL != k2)
-        {
-          // put symbols next
-          return true;
-        }
-      else if (SYMBOL != k1 && SYMBOL == k2)
-        {
-          // put symbols next
-          return false;
-        }
-      else
-        {
-          // otherwise, sort by exprnum (descendents will appear
-          // before ancestors).
-          return (n1.GetNodeNum() < n2.GetNodeNum());
-        }
-    } //end of arithless
-
     bool isConstant() const
     {
        const Kind k = GetKind();
@@ -426,5 +383,6 @@ namespace BEEV
     }; //End of ASTNodeEqual
 
   }; //End of Class ASTNode
+
 }; //end of namespace
 #endif

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index bac06bccf531e5c4b41cf5ddae38100c09ce2722..833571a32786cb4708a91f4843106a5bc5e5b41b 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -16,6 +16,53 @@ namespace BEEV
    * Universal Helper Functions                                   *
    ****************************************************************/
 
+  // Sort ASTNodes by expression numbers
+  bool exprless(const ASTNode n1, const ASTNode n2)
+  {
+    return (n1.GetNodeNum() < n2.GetNodeNum());
+  }
+
+  // This is for sorting by arithmetic expressions (for
+  // combining like terms, etc.)
+  bool arithless(const ASTNode n1, const ASTNode n2)
+  {
+    Kind k1 = n1.GetKind();
+    Kind k2 = n2.GetKind();
+
+    if (n1 == n2)
+      {
+        // necessary for "strict weak ordering"
+        return false;
+      }
+    else if (BVCONST == k1 && BVCONST != k2)
+      {
+        // put consts first
+        return true;
+      }
+    else if (BVCONST != k1 && BVCONST == k2)
+      {
+        // put consts first
+        return false;
+      }
+    else if (SYMBOL == k1 && SYMBOL != k2)
+      {
+        // put symbols next
+        return true;
+      }
+    else if (SYMBOL != k1 && SYMBOL == k2)
+      {
+        // put symbols next
+        return false;
+      }
+    else
+      {
+        // otherwise, sort by exprnum (descendents will appear
+        // before ancestors).
+        return (n1.GetNodeNum() < n2.GetNodeNum());
+      }
+  } //end of arithless
+
+
 bool containsArrayOps(const ASTNode& n, ASTNodeSet& visited)
 {
        if (visited.find(n) != visited.end())