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, 2 insertions, 14 deletions

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 0fd610c58..23d7d8784 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -22,11 +22,9 @@
 #include <memory>
 
 #include "expr/proof_node.h"
-#include "proof/proof_manager.h"
 #include "smt/logic_exception.h"
 #include "theory/interrupted.h"
 #include "theory/trust_node.h"
-#include "util/proof.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -135,10 +133,8 @@ class OutputChannel {
    * assigned false), or else a literal by itself (in the case of a
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
-   * @param pf - a proof of the conflict. This is only non-null if proofs
-   * are enabled.
    */
-  virtual void conflict(TNode n, std::unique_ptr<Proof> pf = nullptr) = 0;
+  virtual void conflict(TNode n) = 0;
 
   /**
    * Propagate a theory literal.
@@ -153,19 +149,11 @@ class OutputChannel {
    * been detected.  (This requests a split.)
    *
    * @param n - a theory lemma valid at decision level 0
-   * @param rule - the proof rule for this lemma
    * @param p The properties of the lemma
    * @return the "status" of the lemma, including user level at which
    * the lemma resides; the lemma will be removed when this user level pops
    */
-  virtual LemmaStatus lemma(TNode n,
-                            ProofRule rule,
-                            LemmaProperty p = LemmaProperty::NONE) = 0;
-
-  /**
-   * Variant of the lemma function that does not require providing a proof rule.
-   */
-  virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE);
+  virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0;
 
   /**
    * Request a split on a new theory atom.  This is equivalent to