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.)

19 files changed, 78 insertions, 47 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index cb8a7ba06..58f098713 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -136,7 +136,7 @@ using namespace CVC4;
 
 %include "util/integer.i"
 %include "util/rational.i"
-%include "util/stats.i"
+%include "util/statistics.i"
 %include "util/exception.i"
 %include "util/language.i"
 %include "options/options.i"
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 6b878ecd0..2d4ae2d52 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -16,6 +16,8 @@
  ** Decision engine
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__DECISION__DECISION_ENGINE_H
 #define __CVC4__DECISION__DECISION_ENGINE_H
 
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index dd6c7f548..2244b27b6 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -16,6 +16,8 @@
  ** Decision strategy
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__DECISION__DECISION_STRATEGY_H
 #define __CVC4__DECISION__DECISION_STRATEGY_H
 
@@ -34,7 +36,7 @@ namespace decision {
 
 class DecisionStrategy {
 protected:
-   DecisionEngine* d_decisionEngine;
+  DecisionEngine* d_decisionEngine;
 public:
   DecisionStrategy(DecisionEngine* de, context::Context *c) :
     d_decisionEngine(de) {
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 6d9493e89..f0f227ead 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -20,6 +20,8 @@
  ** It needs access to the simplified but non-clausal formula.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 #define __CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h
index a529b974e..61aab8811 100644
--- a/src/decision/relevancy.h
+++ b/src/decision/relevancy.h
@@ -30,6 +30,8 @@
  ** path from the root to the node go through a justified node.
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__DECISION__RELEVANCY
 #define __CVC4__DECISION__RELEVANCY
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index e2b1c21f0..4ac137ef1 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -308,9 +308,11 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   s_totalTime.stop();
 
+  // Set the global executor pointer to NULL first.  If we get a
+  // signal while dumping statistics, we don't want to try again.
+  pExecutor = NULL;
   if(opts[options::statistics]) {
     cmdExecutor.flushStatistics(*opts[options::err]);
   }
-  pExecutor = NULL;
   return returnValue;
 }
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 66dc97808..f29e98a9b 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__BASE_OPTIONS_HANDLERS_H
 #define __CVC4__BASE_OPTIONS_HANDLERS_H
 
diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h
index 97c19930e..c613ff8fd 100644
--- a/src/options/base_options_template.h
+++ b/src/options/base_options_template.h
@@ -16,17 +16,19 @@
  ** Contains code for handling command-line options
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__OPTIONS__${module_id}_H
 #define __CVC4__OPTIONS__${module_id}_H
 
 #include "options/options.h"
 ${module_includes}
 
-#line 26 "${template}"
+#line 28 "${template}"
 
 ${module_optionholder_spec}
 
-#line 30 "${template}"
+#line 32 "${template}"
 
 namespace CVC4 {
 
@@ -34,19 +36,19 @@ namespace options {
 
 ${module_decls}
 
-#line 38 "${template}"
+#line 40 "${template}"
 
 }/* CVC4::options namespace */
 
 ${module_specializations}
 
-#line 44 "${template}"
+#line 46 "${template}"
 
 namespace options {
 
 ${module_inlines}
 
-#line 50 "${template}"
+#line 52 "${template}"
 
 }/* CVC4::options namespace */
 
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 9e5fb2b81..69d7643c7 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -810,7 +810,6 @@ function handle_alias {
       expect_arg_long=required_argument
       arg="$(echo "$option" | sed 's,[^=]*=\(.*\),\1,')"
       option="$(echo "$option" | sed 's,--,,;s,=.*,,')"
-      echo "warning: not yet handling long-option alias =$arg" >&2
     else
       expect_arg_long=no_argument
       arg=
@@ -831,7 +830,6 @@ function handle_alias {
       expect_arg=:
       arg="$(echo "$option" | sed 's,[^=]*=,,')"
       option="$(echo "$option" | sed 's,-\(.\)=.*,\1,')"
-      echo "warning: not yet handling short-option alias =$arg" >&2
     else
       expect_arg=
       arg=
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 */
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index f10f4e767..926d3507b 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #include "smt/smt_engine.h"
 #include "util/tls.h"
 #include "util/Assert.h"
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 324921f9a..33ae5d2ff 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -16,6 +16,8 @@
  ** Algebraic solver.
  **/
 
+#include "cvc4_private.h"
+
 #pragma once
 
 #include "theory/bv/bv_subtheory.h"
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 01178b453..d0ba8abca 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -18,6 +18,8 @@
 
 #pragma once
 
+#include "cvc4_private.h"
+
 #include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
diff --git a/src/theory/rewriterules/theory_rewriterules_params.h b/src/theory/rewriterules/theory_rewriterules_params.h
index de51215d1..5e7db156b 100644
--- a/src/theory/rewriterules/theory_rewriterules_params.h
+++ b/src/theory/rewriterules/theory_rewriterules_params.h
@@ -17,6 +17,8 @@
  ** \todo document this file
  **/
 
+#include "cvc4_private.h"
+
 #ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
 #define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PARAMS_H
 
diff --git a/src/theory/rewriterules/theory_rewriterules_preprocess.h b/src/theory/rewriterules/theory_rewriterules_preprocess.h
index c90edcf27..3cd540ad0 100644
--- a/src/theory/rewriterules/theory_rewriterules_preprocess.h
+++ b/src/theory/rewriterules/theory_rewriterules_preprocess.h
@@ -15,9 +15,10 @@
  **
  **/
 
+#include "cvc4_private.h"
 
-#ifndef __CVC4__REWRITERULES_H
-#define __CVC4__REWRITERULES_H
+#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H
+#define __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H
 
 #include <vector>
 #include <ext/hash_set>
@@ -31,7 +32,7 @@ namespace CVC4 {
 namespace theory {
 namespace rewriterules {
 
-namespace rewriter{
+namespace rewriter {
 
   typedef Node TMPNode;
   typedef std::vector<Node> Subst;
@@ -43,7 +44,7 @@ namespace rewriter{
     /** match the node and add in Vars the found variables */
     virtual Node run(TMPNode node) = 0;
     virtual bool add(TMPNode pattern, TMPNode body, Subst & pvars, Subst & vars) = 0;
-  };
+  };/* struct Step */
 
   struct FinalStep : Step {
     Node body;
@@ -54,7 +55,7 @@ namespace rewriter{
                              subst.begin(), subst.end());
     }
 
-  };
+  };/* struct FinalStep */
 
   typedef std::hash_map< Node, int, NodeHashFunction > PVars;
 
@@ -106,7 +107,7 @@ namespace rewriter{
       return false;
     }
     
-  };
+  };/* struct Pattern */
 
 
   struct Args : Step {
@@ -144,7 +145,7 @@ namespace rewriter{
     void clear(){
       d_matches.clear();
     }
-  };
+  };/* struct Args */
 
 class RRPpRewrite : public uf::TheoryUF::PpRewrite {
   Args d_pattern;
@@ -164,13 +165,14 @@ public:
     return d_pattern.add(pattern,body,pvars,vars);
   }
 
-};
+};/* class RRPpRewrite */
 
 
 
-}
+}/* CVC4::theory::rewriterules::rewriter namespace */
 
-}
-}
-}
-#endif /* __CVC4__REWRITERULES_H */
+}/* CVC4::theory::rewriterules namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_PREPROCESS_H */
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index b2180ab59..870a88d66 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -148,7 +148,7 @@ template <>
 inline SExpr mkSExpr(const double& x) {
   // roundabout way to get a Rational from a double
   std::stringstream ss;
-  ss << std::fixed << x;
+  ss << std::fixed << std::setprecision(8) << x;
   return Rational::fromDecimal(ss.str());
 }
 
@@ -487,7 +487,7 @@ public:
 
   SExpr getValue() const {
     std::stringstream ss;
-    ss << d_data;
+    ss << std::fixed << std::setprecision(8) << d_data;
     return SExpr(Rational::fromDecimal(ss.str()));
   }
 
@@ -769,7 +769,7 @@ public:
 
   SExpr getValue() const {
     std::stringstream ss;
-    ss << std::fixed << d_data;
+    ss << std::fixed << std::setprecision(8) << d_data;
     return SExpr(Rational::fromDecimal(ss.str()));
   }