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, 343 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