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.

4 files changed, 209 insertions, 0 deletions

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.
    *
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
index 9f462f756..8d76644dc 100644
--- a/test/unit/proof/CMakeLists.txt
+++ b/test/unit/proof/CMakeLists.txt
@@ -2,3 +2,4 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(drat_proof_black proof)
+cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h
new file mode 100644
index 000000000..27372b62d
--- /dev/null
+++ b/test/unit/proof/lfsc_proof_printer_black.h
@@ -0,0 +1,118 @@
+/*********************                                                        */
+/*! \file lfsc_proof_printer_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of LFSC proof printing
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "proof/lfsc_proof_printer.h"
+#include "prop/sat_solver_types.h"
+#include "proof/clause_id.h"
+
+using namespace CVC4::proof;
+using namespace CVC4::prop;
+
+class LfscProofPrinterBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testPrintClause();
+  void testPrintSatInputProof();
+  void testPrintCMapProof();
+};
+
+void LfscProofPrinterBlack::testPrintClause()
+{
+  SatClause clause{
+      SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, false)};
+  std::ostringstream lfsc;
+
+  LFSCProofPrinter::printSatClause(clause, lfsc, "");
+
+  std::string expectedLfsc =
+      "(clc (pos .v0) "
+      "(clc (neg .v1) "
+      "(clc (pos .v3) "
+      "cln)))";
+
+  TS_ASSERT_EQUALS(lfsc.str(), expectedLfsc);
+}
+
+void LfscProofPrinterBlack::testPrintSatInputProof()
+{
+  std::vector<CVC4::ClauseId> ids{2, 40, 3};
+  std::ostringstream lfsc;
+
+  LFSCProofPrinter::printSatInputProof(ids, lfsc, "");
+
+  std::string expectedLfsc =
+      "(cnfc_proof _ _ _ .pb2 "
+      "(cnfc_proof _ _ _ .pb40 "
+      "(cnfc_proof _ _ _ .pb3 "
+      "cnfn_proof)))";
+
+  std::ostringstream lfscWithoutWhitespace;
+  for (char c : lfsc.str())
+  {
+    if (!std::isspace(c))
+    {
+      lfscWithoutWhitespace << c;
+    }
+  }
+  std::ostringstream expectedLfscWithoutWhitespace;
+  for (char c : expectedLfsc)
+  {
+    if (!std::isspace(c))
+    {
+      expectedLfscWithoutWhitespace << c;
+    }
+  }
+
+  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
+                   expectedLfscWithoutWhitespace.str());
+}
+
+void LfscProofPrinterBlack::testPrintCMapProof()
+{
+  std::vector<CVC4::ClauseId> ids{2, 40, 3};
+  std::ostringstream lfsc;
+
+  LFSCProofPrinter::printCMapProof(ids, lfsc, "");
+
+  std::string expectedLfsc =
+      "(CMapc_proof 1 _ _ _ .pb2 "
+      "(CMapc_proof 2 _ _ _ .pb40 "
+      "(CMapc_proof 3 _ _ _ .pb3 "
+      "CMapn_proof)))";
+
+  std::ostringstream lfscWithoutWhitespace;
+  for (char c : lfsc.str())
+  {
+    if (!std::isspace(c))
+    {
+      lfscWithoutWhitespace << c;
+    }
+  }
+  std::ostringstream expectedLfscWithoutWhitespace;
+  for (char c : expectedLfsc)
+  {
+    if (!std::isspace(c))
+    {
+      expectedLfscWithoutWhitespace << c;
+    }
+  }
+
+  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
+                   expectedLfscWithoutWhitespace.str());
+}