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.

4 files changed, 221 insertions, 0 deletions

diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 01dfd145f..3b4bac3f0 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -75,6 +75,69 @@ std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace)
   return o;
 }
 
+/**
+ * Print a list of clause indices to go to while doing UP.
+ *
+ * i.e. a value of type Trace
+ *
+ * @param o where to print to
+ * @param trace the trace (list of clauses) to print
+ */
+void printTrace(std::ostream& o, const LratUPTrace& trace)
+{
+  for (ClauseIdx idx : trace)
+  {
+    o << "(Tracec " << idx << " ";
+  }
+  o << "Tracen";
+  std::fill_n(std::ostream_iterator<char>(o), trace.size(), ')');
+}
+
+/**
+ * Print the RAT hints for a clause addition.
+ *
+ * i.e. prints an LFSC value of type RATHints
+ *
+ * @param o where to print to
+ * @param hints the RAT hints to print
+ */
+void printHints(std::ostream& o,
+                const std::vector<std::pair<ClauseIdx, LratUPTrace>>& hints)
+{
+  for (auto& hint : hints)
+  {
+    o << "\n    (RATHintsc " << hint.first << " ";
+    printTrace(o, hint.second);
+    o << " ";
+  }
+  o << "RATHintsn";
+  std::fill_n(std::ostream_iterator<char>(o), hints.size(), ')');
+}
+
+/**
+ * Print an index list
+ *
+ * i.e. prints an LFSC value of type CIList
+ *
+ * @param o where to print to
+ * @param indices the list of indices to print
+ */
+void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
+{
+  // Verify that the indices are sorted!
+  for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
+  {
+    Assert(indices[i] < indices[i + 1]);
+  }
+
+  for (ClauseIdx idx : indices)
+  {
+    o << "(CIListc " << idx << " ";
+  }
+  o << "CIListn";
+  std::fill_n(std::ostream_iterator<char>(o), indices.size(), ')');
+}
+
 }  // namespace
 
 // Prints the LRAT addition line in textual format
@@ -248,6 +311,17 @@ LratProof::LratProof(std::istream& textualProof)
   }
 }
 
+void LratProof::outputAsLfsc(std::ostream& o) const
+{
+  std::ostringstream closeParen;
+  for (const auto& i : d_instructions)
+  {
+    i->outputAsLfsc(o, closeParen);
+  }
+  o << "LRATProofn";
+  o << closeParen.str();
+}
+
 void LratAddition::outputAsText(std::ostream& o) const
 {
   o << d_idxOfClause << " ";
@@ -261,6 +335,18 @@ void LratAddition::outputAsText(std::ostream& o) const
   o << "0\n";
 }
 
+void LratAddition::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const
+{
+  o << "\n    (LRATProofa " << d_idxOfClause << " ";
+  closeParen << ")";
+  LFSCProofPrinter::printSatClause(d_clause, o, "bb");
+  o << " ";
+  printTrace(o, d_atTrace);
+  o << " ";
+  printHints(o, d_resolvants);
+  o << " ";
+}
+
 void LratDeletion::outputAsText(std::ostream& o) const
 {
   o << d_idxOfClause << " d ";
@@ -271,6 +357,14 @@ void LratDeletion::outputAsText(std::ostream& o) const
   o << "0\n";
 }
 
+void LratDeletion::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const
+{
+  o << "\n    (LRATProofd ";
+  closeParen << ")";
+  printIndices(o, d_clauses);
+  o << " ";
+}
+
 std::ostream& operator<<(std::ostream& o, const LratProof& p)
 {
   for (const auto& instr : p.getInstructions())
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index d976c1279..fb05bd71b 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -52,6 +52,15 @@ class LratInstruction
    * @param out the stream to write to
    */
   virtual void outputAsText(std::ostream& out) const = 0;
+  /**
+   * Write this LRAT instruction as an LFSC value
+   *
+   * @param out the stream to write to
+   * @param closeParen the stream to write any closing parentheses to
+   *
+   */
+  virtual void outputAsLfsc(std::ostream& o,
+                            std::ostream& closeParen) const = 0;
   virtual ~LratInstruction() = default;
 };
 
@@ -67,6 +76,7 @@ class LratDeletion : public LratInstruction
   LratDeletion() = default;
 
   void outputAsText(std::ostream& out) const override;
+  void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
 
  private:
   // This idx doesn't really matter, but it's in the format anyway, so we parse
@@ -97,6 +107,7 @@ class LratAddition : public LratInstruction
   }
 
   void outputAsText(std::ostream& out) const override;
+  void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
 
  private:
   // The idx for the new clause
@@ -153,6 +164,8 @@ class LratProof
     return d_instructions;
   }
 
+  void outputAsLfsc(std::ostream& o) const;
+
  private:
   // The instructions in the proof. Each is a deletion or addition.
   std::vector<std::unique_ptr<LratInstruction>> d_instructions;
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));
+}