Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

2 files changed, 9 insertions, 31 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index d898b66a2..411b89514 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -232,8 +232,6 @@ CRef Solver::reason(Var x) {
     vec<Lit> explanation;
     MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
 
-    Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl;
-
     // Sort the literals by trail index level
     lemma_lt lt(*this);
     sort(explanation, lt);
@@ -268,12 +266,6 @@ CRef Solver::reason(Var x) {
     }
     explanation.shrink(i - j);
 
-    Debug("pf::sat") << "Solver::reason: explanation = " ;
-    for (int i = 0; i < explanation.size(); ++i) {
-      Debug("pf::sat") << explanation[i] << " ";
-    }
-    Debug("pf::sat") << std::endl;
-
     // We need an explanation clause so we add a fake literal
     if (j == 1) {
       // Add not TRUE to the clause
@@ -284,7 +276,6 @@ CRef Solver::reason(Var x) {
     CRef real_reason = ca.alloc(explLevel, explanation, true);
     // FIXME: at some point will need more information about where this explanation
     // came from (ie. the theory/sharing)
-    Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl;
     PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
            ProofManager::getCnfProof()->registerConvertedClause(id, true);
            // no need to pop current assertion as this is not converted to cnf
@@ -345,12 +336,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 
     // If we are in solve or decision level > 0
     if (minisat_busy || decisionLevel() > 0) {
-      Debug("pf::sat") << "Add clause adding a new lemma: ";
-      for (int k = 0; k < ps.size(); ++k) {
-        Debug("pf::sat") << ps[k] << " ";
-      }
-      Debug("pf::sat") << std::endl;
-
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
@@ -1681,13 +1666,6 @@ CRef Solver::updateLemmas() {
     {
       // The current lemma
       vec<Lit>& lemma = lemmas[i];
-
-      Debug("pf::sat") << "Solver::updateLemmas: working on lemma: ";
-      for (int k = 0; k < lemma.size(); ++k) {
-        Debug("pf::sat") << lemma[k] << " ";
-      }
-      Debug("pf::sat") << std::endl;
-
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
         Assert (! PROOF_ON());
@@ -1747,7 +1725,6 @@ CRef Solver::updateLemmas() {
          TNode cnf_assertion = lemmas_cnf_assertion[i].first;
          TNode cnf_def = lemmas_cnf_assertion[i].second;
 
-         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1764,7 +1741,6 @@ CRef Solver::updateLemmas() {
          Node cnf_assertion = lemmas_cnf_assertion[i].first;
          Node cnf_def = lemmas_cnf_assertion[i].second;
 
-         Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl;
          ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
          ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
          ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ff726e299..bfbf9da6f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   // FIXME: This relies on the invariant that when ok() is false
   // the SAT solver does not add the clause (which is what Minisat currently does)
   if (!ok()) {
-    return ClauseIdUndef;
+    return ClauseIdUndef; 
   }
   d_minisat->addClause(minisat_clause, removable, clause_id);
   PROOF( Assert (clause_id != ClauseIdError););
@@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() {
 }
 
 bool MinisatSatSolver::ok() const {
-  return d_minisat->okay();
+  return d_minisat->okay(); 
 }
 
 void MinisatSatSolver::interrupt() {
@@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const
   return true;
 }
 
-void MinisatSatSolver::requirePhase(SatLiteral lit) {
+void MinisatSatSolver::requirePhase(SatLiteral lit) { 
   Assert(!d_minisat->rnd_pol);
   Debug("minisat") << "requirePhase(" << lit << ")" << " " <<  lit.getSatVariable() << " " << lit.isNegated() << std::endl;
   SatVariable v = lit.getSatVariable();
   d_minisat->freezePolarity(v, lit.isNegated());
 }
 
-bool MinisatSatSolver::flipDecision() {
+bool MinisatSatSolver::flipDecision() { 
   Debug("minisat") << "flipDecision()" << std::endl;
   return d_minisat->flipDecision();
 }
 
-bool MinisatSatSolver::isDecision(SatVariable decn) const {
-  return d_minisat->isDecision( decn );
+bool MinisatSatSolver::isDecision(SatVariable decn) const { 
+  return d_minisat->isDecision( decn ); 
 }
 
 /** Incremental interface */
@@ -291,7 +291,7 @@ namespace CVC4 {
 template<>
 prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
   return prop::MinisatSatSolver::toSatLiteral(lit);
-}
+} 
 
 template<>
 void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
@@ -300,3 +300,5 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause&
 }
 
 } /* namespace CVC4 */
+
+