fixed some bugs

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 43750a5040c56a301eb5ba4c8339ddffb1c89643..7ca1a1e654a5a9a8d9341e17122836eab753574c 100644 (file)
--- 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 624aac237ede221c56ee2cf943e4dcffe66bb1de..dc83e6aa359ac6c331b2505c4f15383b753afdd5 100644 (file)
--- 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 a169d31e6245f457465bb895deab6e0817f3bcda..036877b6a06b87ae1fcee63cfd3a117fc3014a45 100644 (file)
--- 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 78710e4b980c22184f53821fd8fe61bed74aebab..84bbbc17990f8fc32e0f2a1f5bc1372292aa465d 100644 (file)
--- 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() {