diff options
author | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-08 16:50:28 -0400 |
commit | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (patch) | |
tree | a1ea60d22fadc2d2ebefca3ab561fbcf74a6936b /src/proof/sat_proof.h | |
parent | ba8efaff308ef1eb14ec40dd74e0e18c16126d2c (diff) |
fixed uf proof with holes bugs
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r-- | src/proof/sat_proof.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 0ab86b554..5a1fa4680 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -36,7 +36,7 @@ namespace Minisat { #include "prop/minisat/core/SolverTypes.h" #include "util/proof.h" - +#include "prop/sat_solver_types.h" namespace std { using namespace __gnu_cxx; }/* std namespace */ @@ -89,7 +89,6 @@ typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; typedef std::vector < ResChain* > ResStack; -typedef std::hash_set < unsigned > VarSet; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; @@ -255,6 +254,7 @@ protected: void collectClauses(ClauseId id); CnfProof* d_cnfProof; CnfProof* getCnfProof(); + void addClauseToCnfProof(ClauseId id, ClauseKind kind); public: void setCnfProof(CnfProof* cnfProof); virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; |