From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 8 Oct 2013 03:52:21 +0000 (-0400)
Subject: fixed some bugs
X-Git-Tag: cvc5-1.0.0~7284
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba8efaff308ef1eb14ec40dd74e0e18c16126d2c;p=cvc5.git

fixed some bugs
---

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 43750a504..7ca1a1e65 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -34,8 +34,6 @@ ProofManager::ProofManager(ProofFormat format):
   d_fullProof(NULL),
   d_format(format)
 {
-  // FIXME this is until it actually has theory references
-  initTheoryProof(); 
 }
 
 ProofManager::~ProofManager() {
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 624aac237..dc83e6aa3 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -590,6 +590,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
     res->addStep(lit, res_id, !sign(lit)); 
   }
   registerResolution(d_emptyClauseId, res);
+  // FIXME: massive hack
+  Proof* proof = ProofManager::getProof();
+  proof->toStream(std::cout); 
 }
 
 /// CRef manager
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index a169d31e6..036877b6a 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -19,6 +19,7 @@
 #include "prop/theory_proxy.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
+#include "proof/proof_manager.h"
 
 #include "decision/decision_engine.h"
 #include "decision/options.h"
@@ -90,6 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
+  PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); 
 }
 
 PropEngine::~PropEngine() {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 78710e4b9..84bbbc179 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -46,6 +46,8 @@
 
 #include "theory/rewriterules/efficient_e_matching.h"
 
+#include "proof/proof_manager.h"
+
 using namespace std;
 
 using namespace CVC4;
@@ -138,6 +140,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
+  PROOF (ProofManager::currentPM()->initTheoryProof(); ); 
 }
 
 TheoryEngine::~TheoryEngine() {