Resolution proof: separate printing from proof (#1964)

Currently, we have an LFSCSatProof which inherits from TSatProof and
implements printing the proof. The seperation is not clean (e.g.
clauseName is used for printing only but is in TSatProof) and the
inheritance does not add any value while making dependencies more
confusing. The plan is that TSatProof becomes a self-contained part that
the MiniSat implementations generate and ProofManager prints out. This
commit is a first step in that direction. For SAT solvers with native
capabilities for producing proofs, we would simply implement a different
LFSC printer of their proof representation without changing the SAT
solver itself. The inheritance would make this awkward to deal with.

Additionally, the commit cleans up some unused functions and adjusts the
visibility of TSatProof methods and members.

1 files changed, 5 insertions, 135 deletions

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 82e7cb7b2..96f99be47 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -188,9 +188,12 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
 template <class Solver>
 TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
                              const std::string& name, bool checkRes)
-    : d_solver(solver),
+    : d_name(name),
+      d_emptyClauseId(ClauseIdEmpty),
+      d_seenLearnt(),
+      d_assumptionConflictsDebug(),
+      d_solver(solver),
       d_context(context),
-      d_cnfProof(NULL),
       d_idClause(),
       d_clauseId(),
       d_idUnit(context),
@@ -200,19 +203,15 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
       d_lemmaClauses(),
       d_assumptions(),
       d_assumptionConflicts(),
-      d_assumptionConflictsDebug(),
       d_resolutionChains(d_context),
       d_resStack(),
       d_checkRes(checkRes),
-      d_emptyClauseId(ClauseIdEmpty),
       d_nullId(-2),
       d_temp_clauseId(),
       d_temp_idClause(),
       d_unitConflictId(context),
       d_trueLit(ClauseIdUndef),
       d_falseLit(ClauseIdUndef),
-      d_name(name),
-      d_seenLearnt(),
       d_seenInputs(),
       d_seenLemmas(),
       d_satProofConstructed(false),
@@ -266,12 +265,6 @@ TSatProof<Solver>::~TSatProof() {
   }
 }
 
-template <class Solver>
-void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) {
-  Assert(d_cnfProof == NULL);
-  d_cnfProof = cnf_proof;
-}
-
 /**
  * Returns true if the resolution chain corresponding to id
  * does resolve to the clause associated to id
@@ -448,14 +441,6 @@ TSatProof<Solver>::getResolutionChain(ClauseId id) const {
 }
 
 template <class Solver>
-typename TSatProof<Solver>::ResolutionChain*
-TSatProof<Solver>::getMutableResolutionChain(ClauseId id) {
-  Assert(hasResolutionChain(id));
-  ResolutionChain* chain = d_resolutionChains.find(id)->second;
-  return chain;
-}
-
-template <class Solver>
 bool TSatProof<Solver>::isInputClause(ClauseId id) const {
   return d_inputClauses.find(id) != d_inputClauses.end();
 }
@@ -767,15 +752,6 @@ void TSatProof<Solver>::endResChain(ClauseId id) {
   d_resStack.pop_back();
 }
 
-// template <class Solver>
-// void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) {
-//   Assert(d_resStack.size() > 0);
-//   ClauseId id = registerClause(clause, LEARNT);
-//   ResChain<Solver>* res = d_resStack.back();
-//   registerResolution(id, res);
-//   d_resStack.pop_back();
-// }
-
 template <class Solver>
 void TSatProof<Solver>::endResChain(typename Solver::TLit lit) {
   Assert(d_resStack.size() > 0);
@@ -846,11 +822,6 @@ ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
   registerResolution(unit_id, res);
   return unit_id;
 }
-template <class Solver>
-void TSatProof<Solver>::toStream(std::ostream& out) {
-  Debug("proof:sat") << "TSatProof<Solver>::printProof\n";
-  Unimplemented("native proof printing not supported yet");
-}
 
 template <class Solver>
 ClauseId TSatProof<Solver>::storeUnitConflict(
@@ -985,21 +956,6 @@ bool TSatProof<Solver>::proofConstructed() const {
 }
 
 template <class Solver>
-std::string TSatProof<Solver>::clauseName(ClauseId id) {
-  std::ostringstream os;
-  if (isInputClause(id)) {
-    os << ProofManager::getInputClauseName(id, d_name);
-    return os.str();
-  } else if (isLemmaClause(id)) {
-    os << ProofManager::getLemmaClauseName(id, d_name);
-    return os.str();
-  } else {
-    os << ProofManager::getLearntClauseName(id, d_name);
-    return os.str();
-  }
-}
-
-template <class Solver>
 prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
   if (isUnit(id)) {
     typename Solver::TLit lit = getUnit(id);
@@ -1105,92 +1061,6 @@ TSatProof<Solver>::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
 }
 
-/// LFSCSatProof class
-template <class Solver>
-void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out,
-                                           std::ostream& paren) {
-  out << "(satlem_simplify _ _ _";
-  paren << ")";
-
-  const ResChain<Solver>& res = this->getResolutionChain(id);
-  const typename ResChain<Solver>::ResSteps& steps = res.getSteps();
-
-  for (int i = steps.size() - 1; i >= 0; i--) {
-    out << " (";
-    out << (steps[i].sign ? "R" : "Q") << " _ _";
-  }
-
-  ClauseId start_id = res.getStart();
-  out << " " << this->clauseName(start_id);
-
-  for (unsigned i = 0; i < steps.size(); i++) {
-    prop::SatVariable v =
-        prop::MinisatSatSolver::toSatVariable(var(steps[i].lit));
-    out << " " << this->clauseName(steps[i].id) << " "
-        << ProofManager::getVarName(v, this->d_name) << ")";
-  }
-
-  if (id == this->d_emptyClauseId) {
-    out <<" (\\ empty empty)";
-    return;
-  }
-
-  out << " (\\ " << this->clauseName(id) << "\n";   // bind to lemma name
-  paren << ")";
-}
-
-/// LFSCSatProof class
-template <class Solver>
-void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id,
-                                                      std::ostream& out,
-                                                      std::ostream& paren) {
-  Assert(this->isAssumptionConflict(id));
-  // print the resolution proving the assumption conflict
-  printResolution(id, out, paren);
-  // resolve out assumptions to prove empty clause
-  out << "(satlem_simplify _ _ _ ";
-  std::vector<typename Solver::TLit>& confl =
-      *(this->d_assumptionConflictsDebug[id]);
-
-  Assert(confl.size());
-
-  for (unsigned i = 0; i < confl.size(); ++i) {
-    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
-    out << "(";
-    out << (lit.isNegated() ? "Q" : "R") << " _ _ ";
-  }
-
-  out << this->clauseName(id) << " ";
-  for (int i = confl.size() - 1; i >= 0; --i) {
-    prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]);
-    prop::SatVariable v = lit.getSatVariable();
-    out << "unit" << v << " ";
-    out << ProofManager::getVarName(v, this->d_name) << ")";
-  }
-  out << "(\\ e e)\n";
-  paren << ")";
-}
-
-template <class Solver>
-void LFSCSatProof<Solver>::printResolutions(std::ostream& out,
-                                            std::ostream& paren) {
-  Debug("bv-proof") << "; print resolutions" << std::endl;
-  std::set<ClauseId>::iterator it = this->d_seenLearnt.begin();
-  for (; it != this->d_seenLearnt.end(); ++it) {
-    if (*it != this->d_emptyClauseId) {
-      Debug("bv-proof") << "; print resolution for " << *it << std::endl;
-      printResolution(*it, out, paren);
-    }
-  }
-  Debug("bv-proof") << "; done print resolutions" << std::endl;
-}
-
-template <class Solver>
-void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out,
-                                                      std::ostream& paren) {
-  printResolution(this->d_emptyClauseId, out, paren);
-}
-
 inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
   switch (k) {
     case CVC4::INPUT: