Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

1 files changed, 0 insertions, 140 deletions

diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h
deleted file mode 100644
index 1213c80c7..000000000
--- a/src/proof/drat/drat_proof.h
+++ /dev/null
@@ -1,140 +0,0 @@
-/*********************                                                        */
-/*! \file drat_proof.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Mathias Preiner
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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;
-
-  /**
-   * Write the DRAT proof as an LFSC value
-   * The format is from the LFSC signature drat.plf
-   *
-   * Reads the current `ProofManager` to determine what the variables should be
-   * named.
-   *
-   * @param os the stream to write to
-   * @param indentation the number of spaces to indent each proof instruction
-   */
-  void outputAsLfsc(std::ostream& os, uint8_t indentation) 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