From 3361081acd11178d0eb580ce91279a2ecaa7aa65 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Tue, 8 Oct 2013 16:50:28 -0400
Subject: fixed uf proof with holes bugs

---
 src/proof/sat_proof.h | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/proof/sat_proof.h')

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;
-- 
cgit v1.2.3