[LRAT] A C++ data structure for LRAT. (#2737)

* [LRAT] A C++ data structure for LRAT.

Added a data structure for storing (abstract) LRAT proofs.

The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.

Subsequent PRs will add:
   * LFSC representation of LRAT
   * Bitvector Proofs based on LRAT
   * Enabled tests for those proofs

* Documenting LRAT constructors

* Apply suggestions from code review

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

* Responding to Andres' review

Consisting of
   * Naming nits
   * Closed fds
   * Better implementation of disjoint union for LratInstruction
   * DRAT -> LRAT conversion is no longer an LratProof constructor

* include reorder

* Update src/proof/lrat/lrat_proof.h

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

* Addressed Andres' comments

* ANonymous namespaces and name resolution?

* Remove inlines, fix i negation

Thanks Andres!

* Use `std::abs`

Credit to Andres

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

* Remove uneeded public

2 files changed, 507 insertions, 0 deletions

diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
new file mode 100644
index 000000000..ea03a9e20
--- /dev/null
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -0,0 +1,345 @@
+/*********************                                                        */
+/*! \file lrat_proof.cpp
+ ** \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 DRAT Proof Format
+ **
+ ** Defines deserialization for DRAT proofs.
+ **/
+
+#include "proof/lrat/lrat_proof.h"
+
+#include <algorithm>
+#include <cstdlib>
+#include <fstream>
+#include <iostream>
+#include <unordered_map>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+
+namespace CVC4 {
+namespace proof {
+namespace lrat {
+
+using prop::SatClause;
+using prop::SatLiteral;
+using prop::SatVariable;
+
+namespace {
+// Prints the literal as a (+) or (-) int
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const SatLiteral& l)
+{
+  if (l.isNegated())
+  {
+    o << "-";
+  }
+  return o << l.getSatVariable();
+}
+
+// Prints the clause as a space-separated list of ints
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const SatClause& c)
+{
+  for (const auto l : c)
+  {
+    textOut(o, l) << " ";
+  }
+  return o << "0";
+}
+
+// Prints the trace as a space-separated list of (+) ints with a space at the
+// end.
+std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace)
+{
+  for (const auto& i : trace)
+  {
+    o << i << " ";
+  }
+  return o;
+}
+
+// Prints the LRAT addition line in textual format
+std::ostream& operator<<(std::ostream& o, const LratAdditionData& add)
+{
+  o << add.d_idxOfClause << " ";
+  textOut(o, add.d_clause) << " ";
+  o << add.d_atTrace;  // Inludes a space at the end.
+  for (const auto& rat : add.d_resolvants)
+  {
+    o << "-" << rat.first << " ";
+    o << rat.second;  // Includes a space at the end.
+  }
+  o << "0\n";
+  return o;
+}
+
+// Prints the LRAT addition line in textual format
+std::ostream& operator<<(std::ostream& o, const LratDeletionData& del)
+{
+  o << del.d_idxOfClause << " d ";
+  for (const auto& idx : del.d_clauses)
+  {
+    o << idx << " ";
+  }
+  return o << "0\n";
+}
+
+// Prints the LRAT line in textual format
+std::ostream& operator<<(std::ostream& o, const LratInstruction& i)
+{
+  switch (i.d_kind)
+  {
+    case LRAT_ADDITION: return o << i.d_data.d_addition;
+    case LRAT_DELETION: return o << i.d_data.d_deletion;
+    default: return o;
+  }
+}
+
+}
+
+LratInstruction::LratInstruction(LratInstruction&& instr) : d_kind(instr.d_kind)
+{
+  switch (d_kind)
+  {
+    case LRAT_ADDITION:
+    {
+      d_data.d_addition = instr.d_data.d_addition;
+      break;
+    }
+    case LRAT_DELETION:
+    {
+      d_data.d_deletion = instr.d_data.d_deletion;
+      break;
+    }
+  }
+}
+
+LratInstruction::LratInstruction(LratInstruction& instr) : d_kind(instr.d_kind)
+{
+  switch (d_kind)
+  {
+    case LRAT_ADDITION:
+    {
+      d_data.d_addition = instr.d_data.d_addition;
+      break;
+    }
+    case LRAT_DELETION:
+    {
+      d_data.d_deletion = instr.d_data.d_deletion;
+      break;
+    }
+  }
+}
+
+LratInstruction::LratInstruction(LratAdditionData&& addition)
+    : d_kind(LRAT_ADDITION)
+{
+  d_data.d_addition = std::move(addition);
+}
+
+LratInstruction::LratInstruction(LratDeletionData&& deletion)
+    : d_kind(LRAT_DELETION)
+{
+  d_data.d_deletion = std::move(deletion);
+}
+
+LratInstruction::~LratInstruction()
+{
+  switch (d_kind)
+  {
+    case LRAT_ADDITION:
+    {
+      d_data.d_addition.~LratAdditionData();
+      break;
+    }
+    case LRAT_DELETION:
+    {
+      d_data.d_deletion.~LratDeletionData();
+      break;
+    }
+  }
+}
+
+LratProof LratProof::fromDratProof(
+    const std::unordered_map<ClauseId, SatClause*>& usedClauses,
+    const std::vector<ClauseId>& clauseOrder,
+    const std::string& dratBinary)
+{
+  std::ostringstream cmd;
+  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+  char lratFilename[] = "/tmp/cvc4-lrat-XXXXXX";
+  int r;
+  r = mkstemp(formulaFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(dratFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(lratFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  std::ofstream formStream(formulaFilename);
+  size_t maxVar = 0;
+  for (auto& c : usedClauses)
+  {
+    for (auto l : *(c.second))
+    {
+      if (l.getSatVariable() + 1 > maxVar)
+      {
+        maxVar = l.getSatVariable() + 1;
+      }
+    }
+  }
+  formStream << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
+  for (auto ci : clauseOrder)
+  {
+    auto iterator = usedClauses.find(ci);
+    Assert(iterator != usedClauses.end());
+    for (auto l : *(iterator->second))
+    {
+      if (l.isNegated())
+      {
+        formStream << '-';
+      }
+      formStream << l.getSatVariable() + 1 << " ";
+    }
+    formStream << "0\n";
+  }
+  formStream.close();
+
+  std::ofstream dratStream(dratFilename);
+  dratStream << dratBinary;
+  dratStream.close();
+
+  // TODO(aozdemir) Add invocation of DRAT trim, once I get CMake to bundle it
+  // into CVC4 correctly.
+  Unimplemented();
+
+  std::ifstream lratStream(lratFilename);
+  LratProof lrat(lratStream);
+  remove(formulaFilename);
+  remove(dratFilename);
+  remove(lratFilename);
+  return lrat;
+}
+
+std::istream& operator>>(std::istream& in, SatLiteral& l)
+{
+  int64_t i;
+  in >> i;
+  l = SatLiteral(std::abs(i), i < 0);
+  return in;
+}
+
+// This parser is implemented to parse the textual RAT format found in
+// "Efficient Certified RAT Verification", by Cruz-Filipe et. All
+LratProof::LratProof(std::istream& textualProof)
+{
+  for (size_t line = 0;; ++line)
+  {
+    // Read beginning of instruction. EOF indicates that we're done.
+    size_t clauseIdx;
+    textualProof >> clauseIdx;
+    if (textualProof.eof())
+    {
+      return;
+    }
+
+    // Read the first word of the instruction. A 'd' indicates deletion.
+    std::string first;
+    textualProof >> first;
+    Trace("pf::lrat") << "First word: " << first << std::endl;
+    Assert(textualProof.good());
+    if (first == "d")
+    {
+      std::vector<ClauseIdx> clauses;
+      while (true)
+      {
+        ClauseIdx di;
+        textualProof >> di;
+        Assert(textualProof.good());
+        if (di == 0)
+        {
+          break;
+        }
+        clauses.push_back(di);
+      }
+      std::sort(clauses.begin(), clauses.end());
+      d_instructions.emplace_back(
+          LratDeletionData(clauseIdx, std::move(clauses)));
+    }
+    else
+    {
+      // We need to reparse the first word as a literal to read the clause
+      // we're parsing. It ends with a 0;
+      std::istringstream firstS(first);
+      SatLiteral lit;
+      firstS >> lit;
+      Trace("pf::lrat") << "First lit: " << lit << std::endl;
+      Assert(!firstS.fail(), "Couldn't parse first literal from addition line");
+
+      SatClause clause;
+      for (; lit != 0; textualProof >> lit)
+      {
+        Assert(textualProof.good());
+        clause.emplace_back(lit.getSatVariable() - 1, lit.isNegated());
+      }
+
+      // Now we read the AT UP trace. It ends at the first non-(+) #
+      std::vector<ClauseIdx> atTrace;
+      int64_t i;
+      textualProof >> i;
+      for (; i > 0; textualProof >> i)
+      {
+        Assert(textualProof.good());
+        atTrace.push_back(i);
+      }
+
+      // For each RAT hint... (each RAT hint starts with a (-)).
+      std::vector<std::pair<ClauseIdx, LratUPTrace>> resolvants;
+      for (; i<0; textualProof>> i)
+      {
+        Assert(textualProof.good());
+        // Create an entry in the RAT hint list
+        resolvants.emplace_back(-i, std::vector<ClauseIdx>());
+
+        // Record the UP trace. It ends with a (-) or 0.
+        textualProof >> i;
+        for (; i > 0; textualProof >> i)
+        {
+          resolvants.back().second.push_back(i);
+        }
+      }
+      // Pairs compare based on the first element, so this sorts by the
+      // resolution target index
+      std::sort(resolvants.begin(), resolvants.end());
+      d_instructions.emplace_back(LratAdditionData(clauseIdx,
+                                                   std::move(clause),
+                                                   std::move(atTrace),
+                                                   std::move(resolvants)));
+    }
+  }
+}
+
+std::ostream& operator<<(std::ostream& o, const LratProof& p)
+{
+  for (const auto& instr : p.getInstructions())
+  {
+    o << instr;
+  }
+  return o;
+}
+
+}  // namespace lrat
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
new file mode 100644
index 000000000..384fbbdf4
--- /dev/null
+++ b/src/proof/lrat/lrat_proof.h
@@ -0,0 +1,162 @@
+/*********************                                                        */
+/*! \file lrat_proof.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 LRAT Proof Format
+ **
+ ** Declares C++ types that represent a LRAT proof.
+ ** Defines serialization for these types.
+ **
+ ** Represents an **abstract** LRAT proof.
+ ** Does **not** represent an LFSC LRAT proof, or an LRAT proof being used to
+ ** prove things about bit-vectors.
+ **
+ ** Paper on LRAT: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
+#define __CVC4__PROOF__LRAT__LRAT_PROOF_H
+
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "proof/clause_id.h"
+// Included because we need operator<< for the SAT types
+#include "prop/sat_solver.h"
+
+namespace CVC4 {
+namespace proof {
+namespace lrat {
+
+// Refers to clause position within an LRAT proof
+using ClauseIdx = size_t;
+
+enum LratInstructionKind
+{
+  LRAT_DELETION,
+  LRAT_ADDITION,
+};
+
+struct LratDeletionData
+{
+  LratDeletionData(ClauseIdx idxOfClause, std::vector<ClauseIdx>&& clauses)
+      : d_idxOfClause(idxOfClause), d_clauses(clauses)
+  {
+    // Nothing left to do
+  }
+
+  ~LratDeletionData() = default;
+
+  // This idx doesn't really matter, but it's in the format anyway, so we parse
+  // it.
+  ClauseIdx d_idxOfClause;
+
+  // Clauses to delete
+  std::vector<ClauseIdx> d_clauses;
+};
+
+// A sequence of locations that will contain unit clauses during unit
+// propegation
+using LratUPTrace = std::vector<ClauseIdx>;
+
+struct LratAdditionData
+{
+  LratAdditionData(ClauseIdx idxOfClause,
+                   prop::SatClause&& clause,
+                   LratUPTrace&& atTrace,
+                   std::vector<std::pair<ClauseIdx, LratUPTrace>> resolvants)
+      : d_idxOfClause(idxOfClause),
+        d_clause(clause),
+        d_atTrace(atTrace),
+        d_resolvants(resolvants)
+  {
+    // Nothing left to do
+  }
+
+  ~LratAdditionData() = default;
+
+  // The idx for the new clause
+  ClauseIdx d_idxOfClause;
+  // The new clause
+  prop::SatClause d_clause;
+  // UP trace based on the negation of that clause
+  LratUPTrace d_atTrace;
+
+  // Clauses that can resolve with `clause` on its first variable,
+  // together with a UP trace after that resolution.
+  // Used for RAT checks.
+  std::vector<std::pair<ClauseIdx, LratUPTrace>> d_resolvants;
+};
+
+// This is conceptually an Either<Addition,Deletion>
+struct LratInstruction
+{
+  LratInstructionKind d_kind;
+  union LratInstructionData
+  {
+    LratAdditionData d_addition;
+    LratDeletionData d_deletion;
+    ~LratInstructionData(){/* Empty destructor */};
+    LratInstructionData(){/* Empty constructor */};
+  } d_data;
+
+  LratInstruction(LratInstruction&& instr);
+  LratInstruction(LratInstruction& instr);
+  LratInstruction(LratAdditionData&& addition);
+  LratInstruction(LratDeletionData&& deletion);
+  ~LratInstruction();
+};
+
+class LratProof
+{
+ public:
+  /**
+   * @brief Construct an LRAT proof from a DRAT proof, using drat-trim
+   *
+   * @param usedClauses The CNF formula that we're deriving bottom from.
+   *                    It's a map because other parts of the system represent
+   *                    it this way.
+   * @param clauseOrder A record of the order in which those clauses were
+   *                    given to the SAT solver.
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
+   */
+  static LratProof fromDratProof(
+      const std::unordered_map<ClauseId, prop::SatClause*>& usedClauses,
+      const std::vector<ClauseId>& clauseOrder,
+      const std::string& dratBinary);
+  /**
+   * @brief Construct an LRAT proof from its textual representation
+   *
+   * @param textualProof the textual encoding of the LRAT proof. See the paper
+   *                     in the file's header comment.
+   */
+  LratProof(std::istream& textualProof);
+
+  const std::vector<LratInstruction>& getInstructions() const
+  {
+    return d_instructions;
+  }
+
+ private:
+  // The instructions in the proof. Each is a deletion or addition.
+  std::vector<LratInstruction> d_instructions;
+};
+
+// Prints the LRAT proof in textual format
+std::ostream& operator<<(std::ostream& o, const LratProof& p);
+
+}  // namespace lrat
+}  // namespace proof
+}  // namespace CVC4
+
+#endif