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

diff --git a/src/cvc4.i b/src/cvc4.i
index cb8a7ba067161195c8655fe3b9dc835715a94aa3..58f098713549edac95562ba2d1de8377c24ddc18 100644 (file)
--- 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 6b878ecd0f97b0048f529d6cf2a58f980c7b9a65..2d4ae2d521fa1f6e459c8e4a04351e197ce4d875 100644 (file)
--- 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 dd6c7f548c9f0b98f922e175016cbeb105459cb5..2244b27b62643a57815f3888b0f32df62745c569 100644 (file)
--- 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 6d9493e890f4020dce535d5f1d857851ae3e586b..f0f227ead2ecdd3c17bc10f0bf35132282bf091c 100644 (file)
--- 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 a529b974e4ebbe4de8eb3dfab889b499d1b92ce3..61aab88117ef28ce59244166bc37c2b05d7e6e3f 100644 (file)
--- 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 e2b1c21f0a2aa16f9ca7228c897ed158bab94ba9..4ac137ef137bf699cc008b8d6fab86611af37871 100644 (file)
--- 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 66dc9780842dc3efa7e493d1255c757620ffb888..f29e98a9be57a4ebf52813ba088d7a9f00374423 100644 (file)
--- 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 97c19930edfaa08232f298860ebeaacd36558731..c613ff8fd9ea923d1c2c81afdad41a53dd8f86dd 100644 (file)
--- 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 9e5fb2b8113f666b9e4319447c05458960dccf92..69d7643c76a82d7b8470e996d02ca44b4d5d7e11 100755 (executable)
--- 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 c35b0dfffbe5b0c61244e58d5896260e4675b9b0..e0ee4999c21c00e88d29282fc714647d6b83512a 100644 (file)
--- 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 4ce621e439bf91e7f4504ba3a72270be2f676868..cc8b5d45f5dcb117f018553d6c1d208f837d97a1 100644 (file)
--- 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 e23fbd600b9e6b5eb41ed836dd0e7522b8d0ccf4..7719fc304b7243f1b3aff5efdb0d183cecf5cd22 100644 (file)
--- 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 1e6badc9861c6e1c4636ee1b192040e1df3ff836..f768f307d59d3bea1e5ede3363e2c544dad1440f 100644 (file)
--- 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 f10f4e767819a8aff44e7761ccfabbc9243bf2e0..926d3507bf60d0cba2897ad488a59812ec741a34 100644 (file)
--- 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 324921f9a2b2e5df3dd20754351b3c322d3380d4..33ae5d2ffff2247d006d2a32ecd9fe6b42f13c1c 100644 (file)
--- 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 01178b4537e353cb462b4fa4c32fbd4fb9aa5973..d0ba8abca29484f75cc644546f9099b10a6c5e7a 100644 (file)
--- 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 de51215d11dcce02a513fa361cc3143ce7dd0c18..5e7db156ba298a74dc925cbc5ba691b9f7751ed7 100644 (file)
--- 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 c90edcf2790f37ac65b1a9e13f98d8539106e421..3cd540ad0ebceef83251ab8e6e0ab1433d97316a 100644 (file)
--- 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 b2180ab59dff6704f74b24cdcb1a10ff0abaa070..870a88d66ddbc4e116adb8364c4164a41dcfd969 100644 (file)
--- 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()));
   }