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, 102 deletions

diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
deleted file mode 100644
index 88467aea6..000000000
--- a/src/proof/proof_output_channel.cpp
+++ /dev/null
@@ -1,102 +0,0 @@
-/*********************                                                        */
-/*! \file proof_output_channel.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Guy Katz, Tim King, Liana Hadarean
- ** 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
- **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
-
-#include "proof/proof_output_channel.h"
-
-#include "base/check.h"
-#include "theory/term_registration_visitor.h"
-#include "theory/valuation.h"
-
-namespace CVC4 {
-
-ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(nullptr) {}
-const Proof& ProofOutputChannel::getConflictProof() const
-{
-  Assert(hasConflict());
-  return *d_proof;
-}
-
-void ProofOutputChannel::conflict(TNode n, std::unique_ptr<Proof> pf)
-{
-  Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl;
-  Assert(!hasConflict());
-  Assert(!d_proof);
-  d_conflict = n;
-  d_proof = std::move(pf);
-  Assert(hasConflict());
-  Assert(d_proof);
-}
-
-bool ProofOutputChannel::propagate(TNode x) {
-  Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x
-                  << std::endl;
-  d_propagations.insert(x);
-  return true;
-}
-
-theory::LemmaStatus ProofOutputChannel::lemma(TNode n,
-                                              ProofRule rule,
-                                              theory::LemmaProperty p)
-{
-  Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
-  // TODO(#1231): We should transition to supporting multiple lemmas. The
-  // following assertion cannot be enabled due to
-  // "test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt".
-  // Assert(
-  //     d_lemma.isNull()) <<
-  //     "Multiple calls to ProofOutputChannel::lemma() are not supported.";
-  d_lemma = n;
-  return theory::LemmaStatus(TNode::null(), 0);
-}
-
-theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) {
-  AlwaysAssert(false);
-  return theory::LemmaStatus(TNode::null(), 0);
-}
-
-void ProofOutputChannel::requirePhase(TNode n, bool b) {
-  Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl;
-  Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
-}
-
-void ProofOutputChannel::setIncomplete() {
-  Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
-  AlwaysAssert(false);
-}
-
-
-MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory)
-  : d_theory(theory)
-  , d_visited() {
-}
-
-bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
-  return d_visited.find(current) != d_visited.end();
-}
-
-void MyPreRegisterVisitor::visit(TNode current, TNode parent) {
-  d_theory->preRegisterTerm(current);
-  d_visited.insert(current);
-}
-
-void MyPreRegisterVisitor::start(TNode node) {
-}
-
-void MyPreRegisterVisitor::done(TNode node) {
-}
-
-} /* namespace CVC4 */