[DRAT] DRAT data structure (#2767)

* Copied old DRAT data-structure files.

Next step: clean up the code, and adapt them to our current usage plans.

* Polished the DRAT class.

Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.

More explicit about whether methods handle binary or text.

Better constructor patterns

* Added implementation of textual DRAT output

* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction

* use emplace_back

* Addressing Yoni's first review

* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation

* Removed aside about std::string

* Addressed Mathias' comments

Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.

* Unit tests for binary DRAT parsing

* Added text output test

* s/white/black/ derp

1 files changed, 128 insertions, 0 deletions

diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h
new file mode 100644
index 000000000..4bd4f4c04
--- /dev/null
+++ b/src/proof/drat/drat_proof.h
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \file drat_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 DRAT Proof Format
+ **
+ ** Declares C++ types that represent a DRAT proof.
+ ** Defines serialization for these types.
+ **
+ ** You can find an introduction to DRAT in the drat-trim paper:
+ **    http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
+ **
+ **/
+
+#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#define __CVC4__PROOF__DRAT__DRAT_PROOF_H
+
+#include "cvc4_private.h"
+#include "prop/sat_solver.h"
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+namespace proof {
+namespace drat {
+
+using CVC4::prop::SatClause;
+using CVC4::prop::SatLiteral;
+using CVC4::prop::SatVariable;
+
+class CVC4_PUBLIC InvalidDratProofException : public CVC4::Exception
+{
+ public:
+  InvalidDratProofException() : Exception("Invalid DRAT Proof") {}
+
+  InvalidDratProofException(const std::string& msg) : Exception(msg) {}
+
+  InvalidDratProofException(const char* msg) : Exception(msg) {}
+}; /* class InvalidDratProofException */
+
+enum DratInstructionKind
+{
+  ADDITION,
+  DELETION
+};
+
+struct DratInstruction
+{
+  DratInstruction(DratInstructionKind kind, SatClause clause);
+
+  /**
+   * Write the DRAT instruction in textual format.
+   * The format is described in:
+   *    http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
+   *
+   * @param os the stream to write to
+   */
+  void outputAsText(std::ostream& os) const;
+
+  DratInstructionKind d_kind;
+  SatClause d_clause;
+};
+
+class DratProof
+{
+ public:
+  DratProof(const DratProof&) = default;
+
+  DratProof(DratProof&&) = default;
+
+  ~DratProof() = default;
+
+  /**
+   * Parses a DRAT proof from the **binary format**.
+   * The format is described at:
+   *    https://www.cs.utexas.edu/~marijn/drat-trim/#contact
+   *
+   * What do the standard authors mean by the format being "binary"?
+   * They just mean that proofs in this format should be understood as
+   * sequences of bytes, not sequences of ASCII/Unicode/your favorite character
+   * set characters.
+   *
+   * @param binaryProof a string containing the bytes of the binary proof.
+   *        Even though the proof isn't text, it's safe to store it in a string
+   *        because C++ strings don't make any gaurantees about the encoding of
+   *        their contents. This makes them (effectively) just byte sequences.
+   *
+   * @return the parsed proof
+   */
+  static DratProof fromBinary(const std::string& binaryProof);
+
+  /**
+   * @return The instructions in this proof
+   */
+  const std::vector<DratInstruction>& getInstructions() const;
+
+  /**
+   * Write the DRAT proof in textual format.
+   * The format is described in:
+   *    http://www.cs.utexas.edu/~marijn/publications/drat-trim.pdf
+   *
+   * @param os the stream to write to
+   */
+  void outputAsText(std::ostream& os) const;
+
+ private:
+  /**
+   * Create an DRAT proof with no instructions.
+   */
+  DratProof();
+
+  /**
+   * The instructions of the DRAT proof.
+   */
+  std::vector<DratInstruction> d_instructions;
+};
+
+}  // namespace drat
+}  // namespace proof
+}  // namespace CVC4
+
+#endif  // __CVC4__PROOF__DRAT__DRAT_PROOF_H