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.

2 files changed, 119 insertions, 0 deletions

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());
+}