From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 11 Oct 2009 01:31:34 +0000 (+0000)
Subject: minor edits
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5f503c1d2a53f54281bccfd10dd70d69d4ac9896;p=francis%2Fstp.git

minor edits

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

diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index 0355c07..87509a3 100644
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -58,7 +58,6 @@ namespace BEEV
 
     friend bool operator<(const ASTNode node1, const ASTNode node2)
     {
-      //FIXME: Nondeterministic code. Questionable pointer comparison
       return 
 	((size_t) node1._int_node_ptr) < 
 	((size_t) node2._int_node_ptr);
diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 58275bf..e751b30 100644
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -19,11 +19,19 @@
 #include "../parser/let-funcs.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 
+/********************************************************************
+ *  This file gives the class description of the STP class          *
+ ********************************************************************/
 
 namespace BEEV
 {
   class STP {
   public:
+    /****************************************************************
+     * Public Data:
+     *  
+     * Absolute toplevel class. No need to make data private
+     ****************************************************************/
     STPMgr * bm;
     Simplifier * simp;
     BVSolver * bvsolver;
@@ -31,6 +39,10 @@ namespace BEEV
     ToSAT * tosat;
     AbsRefine_CounterExample * Ctr_Example;
 
+    /****************************************************************
+     * Constructor and Destructor                                   *
+     ****************************************************************/
+
     //Constructor
     STP(STPMgr* b,
 	Simplifier* s,
@@ -52,6 +64,10 @@ namespace BEEV
       ClearAllTables();	  
     }
 
+    /****************************************************************
+     * Public Member Functions                                      *
+     ****************************************************************/
+
     // The absolute TopLevel function that invokes STP on the input
     // formula
     SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts,