diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-24 18:37:22 +0000 |
commit | 1f48835b7252757bb778a93bdac2d62e1dea59bc (patch) | |
tree | 1b2f2cda4091a146a2ddfbfcf137459e712fcc17 /src/proof/sat_proof.h | |
parent | e2611a54c5479086df0c4a80f56597aae80b5c4e (diff) |
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.)
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r-- | src/proof/sat_proof.h | 30 |
1 files changed, 16 insertions, 14 deletions
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 */ |