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 0355c07d89da1a0c789f3e3116665a29e3968d27..87509a3522d6da48504f0192241ed4f009a879f2 100644 (file)
--- 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 58275bf423fb552bc7d139dc50e9d68c58b130a9..e751b303f0432178fbce49a06285196c717ddc66 100644 (file)
--- 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,