LFSC LRAT Output (#2787)

* LFSC ouput & unit test

* Renamed lrat unit test file

* s/DRAT/LRAT/

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

* Addressed Andres' comments

1. Extracted a filter whitespace function.
2. Added @param annotations.

* Addressing Yoni's comments

Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.

2 files changed, 114 insertions, 0 deletions

diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
index 8d76644dc..00c893bdb 100644
--- a/test/unit/proof/CMakeLists.txt
+++ b/test/unit/proof/CMakeLists.txt
@@ -2,4 +2,5 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(drat_proof_black proof)
+cvc4_add_unit_test_black(lrat_proof_black proof)
 cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
new file mode 100644
index 000000000..49d18ac53
--- /dev/null
+++ b/test/unit/proof/lrat_proof_black.h
@@ -0,0 +1,113 @@
+/*********************                                                        */
+/*! \file lrat_proof_black.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 the LRAT proof class
+ **
+ ** In particular, tests LRAT LFSC output.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <algorithm>
+#include <cctype>
+#include <iostream>
+#include <iterator>
+
+#include "proof/lrat/lrat_proof.h"
+#include "prop/sat_solver_types.h"
+
+using namespace CVC4::proof::lrat;
+using namespace CVC4::prop;
+
+class LfscProofBlack : public CxxTest::TestSuite
+{
+ public:
+  void setUp() override {}
+  void tearDown() override {}
+
+  void testOutputAsLfsc();
+};
+
+/**
+ * Creates a new stream with whitespace removed.
+ *
+ * @param s the source string
+ *
+ * @return a string without whitespace
+ */
+std::string filterWhitespace(const std::string& s)
+{
+  std::string out;
+  std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) {
+    return !std::isspace(c);
+  });
+  return out;
+}
+
+void LfscProofBlack::testOutputAsLfsc()
+{
+  std::vector<std::unique_ptr<LratInstruction>> instructions;
+
+  // 6   d 1 2
+  std::vector<ClauseIdx> clausesToDelete{1, 2};
+  std::unique_ptr<LratDeletion> deletion = std::unique_ptr<LratDeletion>(
+      new LratDeletion(6, std::move(clausesToDelete)));
+  instructions.push_back(std::move(deletion));
+
+  // 7   1 2 0  5 2 0
+  std::vector<SatLiteral> firstAddedClause{SatLiteral(1, false),
+                                           SatLiteral(2, false)};
+  LratUPTrace firstTrace{5, 2};
+  std::vector<std::pair<ClauseIdx, LratUPTrace>> firstHints;
+  std::unique_ptr<LratAddition> add1 =
+      std::unique_ptr<LratAddition>(new LratAddition(
+          7, std::move(firstAddedClause), std::move(firstTrace), firstHints));
+  instructions.push_back(std::move(add1));
+
+  // 8   2 0  -1 3  -5 2 0
+  std::vector<SatLiteral> secondAddedClause{SatLiteral(2, false)};
+  LratUPTrace secondTrace;
+  std::vector<std::pair<ClauseIdx, LratUPTrace>> secondHints;
+  LratUPTrace secondHints0Trace{3};
+  secondHints.emplace_back(1, secondHints0Trace);
+  LratUPTrace secondHints1Trace{2};
+  secondHints.emplace_back(5, secondHints1Trace);
+  std::unique_ptr<LratAddition> add2 = std::unique_ptr<LratAddition>(
+      new LratAddition(8,
+                       std::move(secondAddedClause),
+                       std::move(secondTrace),
+                       secondHints));
+  instructions.push_back(std::move(add2));
+
+  LratProof proof(std::move(instructions));
+
+  std::ostringstream lfsc;
+  proof.outputAsLfsc(lfsc);
+
+  // 6   d 1 2
+  // 7   1 2 0  5 2 0
+  // 8   2 0  -1 3  -5 2 0
+  std::string expectedLfsc =
+      "(LRATProofd (CIListc 1 (CIListc 2 CIListn)) "
+      "(LRATProofa 7 "
+      "  (clc (pos bb.v1) (clc (pos bb.v2) cln))"
+      "  (Tracec 5 (Tracec 2 Tracen))"
+      "  RATHintsn "
+      "(LRATProofa 8 "
+      "  (clc (pos bb.v2) cln)"
+      "  Tracen "
+      "  (RATHintsc 1 (Tracec 3 Tracen)"
+      "    (RATHintsc 5 (Tracec 2 Tracen)"
+      "    RATHintsn)) "
+      "LRATProofn)))";
+
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(expectedLfsc));
+}