From 517b6ba3bb029470bdb3f230188af1f398b14a91 Mon Sep 17 00:00:00 2001
From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 9 Jan 2019 09:18:29 +0100
Subject: Clause proof printing (#2779)

* Print LFSC proofs of CNF formulas

* Unit Test for clause printing

* Added SAT input proof printing unit test

* Fixed cnf_holds reference. Proofs of CMap_holds

There were references to clauses_hold, which should have been references
to cnf_holds.

Also added a function for printing a value of type CMap_holds, and a
test for this function.
---
 src/proof/lfsc_proof_printer.cpp | 41 +++++++++++++++++++++++++++++++++
 src/proof/lfsc_proof_printer.h   | 49 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 90 insertions(+)

(limited to 'src')

diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp
index e1fa3acdb..be1259837 100644
--- a/src/proof/lfsc_proof_printer.cpp
+++ b/src/proof/lfsc_proof_printer.cpp
@@ -16,7 +16,9 @@
 
 #include "proof/lfsc_proof_printer.h"
 
+#include <algorithm>
 #include <iostream>
+#include <iterator>
 
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/minisat/core/Solver.h"
@@ -144,6 +146,45 @@ void LFSCProofPrinter::printResolutionEmptyClause(TSatProof<Solver>* satProof,
   printResolution(satProof, satProof->getEmptyClauseId(), out, paren);
 }
 
+void LFSCProofPrinter::printSatInputProof(const std::vector<ClauseId>& clauses,
+                                      std::ostream& out,
+                                      const std::string& namingPrefix)
+{
+  for (auto i = clauses.begin(), end = clauses.end(); i != end; ++i)
+  {
+    out << "\n    (cnfc_proof _ _ _ "
+        << ProofManager::getInputClauseName(*i, namingPrefix) << " ";
+  }
+  out << "cnfn_proof";
+  std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
+}
+
+void LFSCProofPrinter::printCMapProof(const std::vector<ClauseId>& clauses,
+                                      std::ostream& out,
+                                      const std::string& namingPrefix)
+{
+  for (size_t i = 0, n = clauses.size(); i < n; ++i)
+  {
+    out << "\n    (CMapc_proof " << (i + 1) << " _ _ _ "
+        << ProofManager::getInputClauseName(clauses[i], namingPrefix) << " ";
+  }
+  out << "CMapn_proof";
+  std::fill_n(std::ostream_iterator<char>(out), clauses.size(), ')');
+}
+
+void LFSCProofPrinter::printSatClause(const prop::SatClause& clause,
+                                      std::ostream& out,
+                                      const std::string& namingPrefix)
+{
+  for (auto i = clause.cbegin(); i != clause.cend(); ++i)
+  {
+    out << "(clc " << (i->isNegated() ? "(neg " : "(pos ")
+        << ProofManager::getVarName(i->getSatVariable(), namingPrefix) << ") ";
+  }
+  out << "cln";
+  std::fill_n(std::ostream_iterator<char>(out), clause.size(), ')');
+}
+
 // Template specializations
 template void LFSCProofPrinter::printAssumptionsResolution(
     TSatProof<CVC4::Minisat::Solver>* satProof,
diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h
index bf4bfabad..36a3490f7 100644
--- a/src/proof/lfsc_proof_printer.h
+++ b/src/proof/lfsc_proof_printer.h
@@ -74,7 +74,56 @@ class LFSCProofPrinter
                                          std::ostream& out,
                                          std::ostream& paren);
 
+  /**
+   * The SAT solver is given a list of clauses.
+   * Assuming that each clause has alreay been individually proven,
+   * defines a proof of the input to the SAT solver.
+   *
+   * Prints an LFSC value corresponding to the proof, i.e. a value of type
+   * (cnf_holds ...)
+   *
+   * @param clauses The clauses to print a proof of
+   * @param out The stream to print to
+   * @param namingPrefix The prefix for LFSC names
+   */
+  static void printSatInputProof(const std::vector<ClauseId>& clauses,
+                                 std::ostream& out,
+                                 const std::string& namingPrefix);
+
+  /**
+   * The LRAT proof signature uses the concept of a _clause map_ (CMap), which
+   * represents an indexed collection of (conjoined) clauses.
+   *
+   * Specifically, the signatures rely on a proof that a CMap containing the
+   * clauses given to the SAT solver hold.
+   *
+   * Assuming that the individual clauses already have proofs, this function
+   * prints a proof of the CMap mapping 1 to the first clause, 2 to the second,
+   * and so on.
+   *
+   * That is, it prints a value of type (CMap_holds ...)
+   *
+   * @param clauses The clauses to print a proof of
+   * @param out The stream to print to
+   * @param namingPrefix The prefix for LFSC names
+   */
+  static void printCMapProof(const std::vector<ClauseId>& clauses,
+                             std::ostream& out,
+                             const std::string& namingPrefix);
+
+  /**
+   * Prints a clause
+   *
+   * @param clause The clause to print
+   * @param out The stream to print to
+   * @param namingPrefix The prefix for LFSC names
+   */
+  static void printSatClause(const prop::SatClause& clause,
+                             std::ostream& out,
+                             const std::string& namingPrefix);
+
  private:
+
   /**
    * Maps a clause id to a string identifier used in the LFSC proof.
    *
-- 
cgit v1.2.3