From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 21 Sep 2009 23:42:04 +0000 (+0000)
Subject: All fixed. RNA example is running again. I had introduced some Abstraction-refinement... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=aaf2b566cef07925ed47a46f01e4c13a201db84c;p=francis%2Fstp.git

All fixed. RNA example is running again. I had introduced some Abstraction-refinement code in AST.h. It seems to have pushed the system to limits of memory consumption

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index f8e5235..24be83a 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -96,7 +96,7 @@ namespace BEEV
     //Integer that helps sort the ASTNodes. This sorting is different
     //from the sorting based on NodeNum. This is used as a way of
     //achieving abstraction-refinement.
-    unsigned int _sort_for_absrefine;
+    //unsigned int _sort_for_absrefine;
 
     //Equal iff ASTIntNode pointers are the same.
     friend bool operator==(const ASTNode node1, const ASTNode node2)
@@ -122,18 +122,18 @@ namespace BEEV
     }
 
   public:
-    //Set the sorting integer for abstraction refinement
-    void SetAbsRefineInt(unsigned int a) {_sort_for_absrefine = a;}
-
-    //Get the sorting integer for abstraction refinement
-    unsigned int GetAbsRefineInt(void) {return _sort_for_absrefine;}
-
-    //Compare two ASTNodes based on their abstraction refinement
-    //number
-    bool CmpAbsRefine(const ASTNode node1, const ASTNode node2) {
-      return (node1._sort_for_absrefine < node2._sort_for_absrefine);
-    }
-
+    //     //Set the sorting integer for abstraction refinement
+    //     void SetAbsRefineInt(unsigned int a) {_sort_for_absrefine = a;}
+    
+    //     //Get the sorting integer for abstraction refinement
+    //     unsigned int GetAbsRefineInt(void) {return _sort_for_absrefine;}
+    
+    //     //Compare two ASTNodes based on their abstraction refinement
+    //     //number
+    //     bool CmpAbsRefine(const ASTNode node1, const ASTNode node2) {
+    //       return (node1._sort_for_absrefine < node2._sort_for_absrefine);
+    //     }
+    
     //Check if it points to a null node
     bool IsNull() const
     {
@@ -211,7 +211,7 @@ namespace BEEV
     ASTNode() :
       _int_node_ptr(NULL)
     {
-      _sort_for_absrefine=0;
+      //_sort_for_absrefine=0;
     }
     ;