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).

2 files changed, 0 insertions, 527 deletions

diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
deleted file mode 100644
index 69ffa623a..000000000
--- a/src/proof/lrat/lrat_proof.cpp
+++ /dev/null
@@ -1,343 +0,0 @@
-/*********************                                                        */
-/*! \file lrat_proof.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Andres Noetzli, 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
- **
- ** Defines deserialization for DRAT proofs.
- **/
-
-#include "proof/lrat/lrat_proof.h"
-
-#include <algorithm>
-#include <cstdlib>
-#include <fstream>
-#include <iostream>
-#include <memory>
-#include <sstream>
-#include <unordered_map>
-
-#include "base/check.h"
-#include "base/output.h"
-#include "proof/dimacs.h"
-#include "proof/lfsc_proof_printer.h"
-#include "util/utility.h"
-
-#if CVC4_USE_DRAT2ER
-#include "drat2er_options.h"
-#include "drat_trim_interface.h"
-#endif
-
-namespace CVC4 {
-namespace proof {
-namespace lrat {
-
-using prop::SatClause;
-using prop::SatLiteral;
-using prop::SatVariable;
-
-namespace {
-
-// 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;
-}
-
-/**
- * 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)
-{
-  Assert(indices.size() > 0);
-  // 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
-
-LratProof LratProof::fromDratProof(
-    const std::unordered_map<ClauseId, prop::SatClause>& clauses,
-    const std::vector<ClauseId> usedIds,
-    const std::string& dratBinary,
-    TimerStat& toolTimer)
-{
-  std::ostringstream cmd;
-  std::string formulaFilename("cvc4-dimacs-XXXXXX");
-  std::string dratFilename("cvc4-drat-XXXXXX");
-  std::string lratFilename("cvc4-lrat-XXXXXX");
-
-  std::unique_ptr<std::fstream> formStream = openTmpFile(&formulaFilename);
-  printDimacs(*formStream, clauses, usedIds);
-  formStream->close();
-
-  std::unique_ptr<std::fstream> dratStream = openTmpFile(&dratFilename);
-  (*dratStream) << dratBinary;
-  dratStream->close();
-
-  std::unique_ptr<std::fstream> lratStream = openTmpFile(&lratFilename);
-
-  {
-    CodeTimer blockTimer{toolTimer};
-#if CVC4_USE_DRAT2ER
-    drat2er::drat_trim::CheckAndConvertToLRAT(
-        formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
-#else
-    Unimplemented()
-        << "LRAT proof production requires drat2er.\n"
-        << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild";
-#endif
-  }
-
-  LratProof lrat(*lratStream);
-  remove(formulaFilename.c_str());
-  remove(dratFilename.c_str());
-  remove(lratFilename.c_str());
-  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);
-      }
-      if (clauses.size() > 0)
-      {
-        std::sort(clauses.begin(), clauses.end());
-        std::unique_ptr<LratInstruction> instr(
-            new LratDeletion(clauseIdx, std::move(clauses)));
-        d_instructions.push_back(std::move(instr));
-      }
-    }
-    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());
-      std::unique_ptr<LratInstruction> instr(
-          new LratAddition(clauseIdx,
-                           std::move(clause),
-                           std::move(atTrace),
-                           std::move(resolvants)));
-      d_instructions.push_back(std::move(instr));
-    }
-  }
-}
-
-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 << " ";
-  textOut(o, d_clause) << " ";
-  o << d_atTrace;  // Inludes a space at the end.
-  for (const auto& rat : d_resolvants)
-  {
-    o << "-" << rat.first << " ";
-    o << rat.second;  // Includes a space at the end.
-  }
-  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 ";
-  for (const auto& idx : d_clauses)
-  {
-    o << idx << " ";
-  }
-  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())
-  {
-    o << *instr;
-  }
-  return o;
-}
-
-std::ostream& operator<<(std::ostream& o, const LratInstruction& i)
-{
-  i.outputAsText(o);
-  return o;
-}
-
-}  // namespace lrat
-}  // namespace proof
-}  // namespace CVC4
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
deleted file mode 100644
index 1c065a08e..000000000
--- a/src/proof/lrat/lrat_proof.h
+++ /dev/null
@@ -1,184 +0,0 @@
-/*********************                                                        */
-/*! \file lrat_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 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 <iosfwd>
-#include <string>
-#include <unordered_map>
-#include <utility>
-#include <vector>
-
-#include "proof/clause_id.h"
-// Included because we need operator<< for the SAT types
-#include "prop/sat_solver.h"
-#include "util/statistics_registry.h"
-
-namespace CVC4 {
-namespace proof {
-namespace lrat {
-
-// Refers to clause position within an LRAT proof
-using ClauseIdx = size_t;
-
-// This is conceptually an Either<Addition,Deletion>
-class LratInstruction
-{
- public:
-  /**
-   * Write this LRAT instruction in textual format
-   *
-   * @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;
-};
-
-class LratDeletion : public LratInstruction
-{
- public:
-  LratDeletion(ClauseIdx idxOfClause, std::vector<ClauseIdx>&& clauses)
-      : d_idxOfClause(idxOfClause), d_clauses(clauses)
-  {
-    // Nothing left to do
-  }
-
-  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
-  // 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>;
-
-class LratAddition : public LratInstruction
-{
- public:
-  LratAddition(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
-  }
-
-  void outputAsText(std::ostream& out) const override;
-  void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
-
- private:
-  // 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;
-};
-
-class LratProof
-{
- public:
-  /**
-   * @brief Construct an LRAT proof from a DRAT proof, using drat-trim
-   *
-   * @param clauses A store of clauses that might be in our formula
-   * @param usedIds the ids of clauses that are actually in our formula
-   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
-   *
-   * @return an LRAT proof an a timer for how long it took to run drat-trim
-   */
-  static LratProof fromDratProof(
-      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
-      const std::vector<ClauseId> usedIds,
-      const std::string& dratBinary,
-      TimerStat& toolTimer);
-  /**
-   * @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);
-
-  /**
-   * Construct a LRAT proof from an explicit instruction list
-   *
-   * @param instructions
-   */
-  LratProof(std::vector<std::unique_ptr<LratInstruction>>&& instructions)
-      : d_instructions(std::move(instructions))
-  {
-    // Nothing else
-  }
-
-  const std::vector<std::unique_ptr<LratInstruction>>& getInstructions() const
-  {
-    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;
-};
-
-// Prints the LRAT proof in textual format
-std::ostream& operator<<(std::ostream& o, const LratProof& p);
-std::ostream& operator<<(std::ostream& o, const LratInstruction& i);
-
-}  // namespace lrat
-}  // namespace proof
-}  // namespace CVC4
-
-#endif