Fix the memout issue seen in recent nightly regressions (was due to a

Statistics-printing problem, limited to certain benchmarks).

Mark some unlabeled header files "cvc4_private.h".

Other minor cleanup.

(this commit was certified error- and warning-free by the test-and-commit script.)

4 files changed, 30 insertions, 21 deletions

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index c35b0dfff..e0ee4999c 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -18,6 +18,8 @@
  ** 
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 4ce621e43..cc8b5d45f 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -16,6 +16,8 @@
  ** Proof manager
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROOF__PROOF_H
 #define __CVC4__PROOF__PROOF_H
 
@@ -31,6 +33,4 @@
 #  define PROOF_ON() false
 #endif /* CVC4_PROOF */
 
-
-
 #endif /* __CVC4__PROOF__PROOF_H */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index e23fbd600..7719fc304 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -18,6 +18,8 @@
  ** 
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__PROOF_MANAGER_H
 #define __CVC4__PROOF_MANAGER_H
 
@@ -26,13 +28,15 @@
 
 // forward declarations
 namespace Minisat {
-class Solver;
+  class Solver;
 }
 
 namespace CVC4 {
+
 namespace prop {
-class CnfStream;
+  class CnfStream;
 }
+
 class Proof;
 class SatProof;
 class CnfProof;
@@ -41,7 +45,7 @@ class CnfProof;
 enum ProofFormat {
   LFSC,
   NATIVE
-};
+};/* enum ProofFormat */
 
 class ProofManager {
   SatProof*   d_satProof;
@@ -61,7 +65,8 @@ public:
   static SatProof* getSatProof();
   static CnfProof* getCnfProof();
 
-};
+};/* class ProofManager */
+
+}/* CVC4 namespace */
 
-} /* CVC4 namespace*/ 
 #endif /* __CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 1e6badc98..f768f307d 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -16,6 +16,8 @@
  ** Resolution proof
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__SAT__PROOF_H
 #define __CVC4__SAT__PROOF_H
 
@@ -26,22 +28,23 @@
 #include <ext/hash_map>
 #include <ext/hash_set>
 #include <sstream>
+
 namespace Minisat {
-class Solver;
-typedef uint32_t CRef;
-}
+  class Solver;
+  typedef uint32_t CRef;
+}/* Minisat namespace */
 
 #include "prop/minisat/core/SolverTypes.h"
 #include "util/proof.h"
 
 namespace std {
-using namespace __gnu_cxx;
-}
+  using namespace __gnu_cxx;
+}/* std namespace */
 
 namespace CVC4 {
+
 /** 
  * Helper debugging functions
- * 
  */
 void printDebug(::Minisat::Lit l);
 void printDebug(::Minisat::Clause& c); 
@@ -56,7 +59,7 @@ struct ResStep {
     id(i),
     sign(s)
   {}
-};
+};/* struct ResStep */
 
 typedef std::vector< ResStep > ResSteps; 
 typedef std::set < ::Minisat::Lit> LitSet; 
@@ -76,8 +79,7 @@ public:
   ClauseId  getStart()     { return d_start; }
   ResSteps& getSteps()     { return d_steps; }
   LitSet*   getRedundant() { return d_redundantLits; }
-};
-
+};/* class ResChain */
 
 typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
 typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
@@ -98,7 +100,7 @@ private:
 public:
   ProofProxy(SatProof* pf);
   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
-};
+};/* class ProofProxy */
 
 class SatProof : public Proof {
 protected:
@@ -217,7 +219,7 @@ public:
   void     storeUnitResolution(::Minisat::Lit lit); 
   
   ProofProxy* getProxy() {return d_proxy; } 
-};
+};/* class SatProof */
 
 class LFSCSatProof: public SatProof {
 private:
@@ -251,8 +253,8 @@ public:
     d_seenInput()
   {} 
   virtual void toStream(std::ostream& out);  
-};
+};/* class LFSCSatProof */
 
-}
+}/* CVC4 namespace */
 
-#endif
+#endif /* __CVC4__SAT__PROOF_H */