From 1f48835b7252757bb778a93bdac2d62e1dea59bc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 24 Sep 2012 18:37:22 +0000 Subject: [PATCH] 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.) --- src/cvc4.i | 2 +- src/decision/decision_engine.h | 2 ++ src/decision/decision_strategy.h | 4 ++- src/decision/justification_heuristic.h | 2 ++ src/decision/relevancy.h | 2 ++ src/main/driver_unified.cpp | 4 ++- src/options/base_options_handlers.h | 2 ++ src/options/base_options_template.h | 12 ++++---- src/options/mkoptions | 2 -- src/proof/cnf_proof.h | 2 ++ src/proof/proof.h | 4 +-- src/proof/proof_manager.h | 15 ++++++---- src/proof/sat_proof.h | 30 ++++++++++--------- src/smt/smt_engine_scope.h | 2 ++ src/theory/bv/bv_subtheory_bitblast.h | 2 ++ src/theory/bv/bv_subtheory_eq.h | 2 ++ .../rewriterules/theory_rewriterules_params.h | 2 ++ .../theory_rewriterules_preprocess.h | 28 +++++++++-------- src/util/statistics_registry.h | 6 ++-- 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 #include #include + 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 #include @@ -31,7 +32,7 @@ namespace CVC4 { namespace theory { namespace rewriterules { -namespace rewriter{ +namespace rewriter { typedef Node TMPNode; typedef std::vector 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())); } -- 2.30.2