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

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 19a10eba8..f8444965f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -43,26 +43,10 @@ namespace CVC4 {
 namespace theory {
 namespace eq {
 
-
-class EqProof;
 class EqClassesIterator;
 class EqClassIterator;
 
 /**
- * An interface for equality engine notifications during equality path reconstruction.
- * Can be used to add theory-specific logic for, e.g., proof construction.
- */
-class PathReconstructionNotify {
-public:
-
-  virtual ~PathReconstructionNotify() {}
-
-  virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
-                      std::vector<TNode>& equalities,
-                      EqProof* proof) const = 0;
-};
-
-/**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
  * notifications via an EqualityEngineNotify object.
  */
@@ -152,9 +136,6 @@ private:
   /** The map of kinds with operators to be considered external (for higher-order) */
   KindMap d_congruenceKindsExtOperators;
 
-  /** Objects that need to be notified during equality path reconstruction */
-  std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers;
-
   /** Map from nodes to their ids */
   std::unordered_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
@@ -196,9 +177,6 @@ private:
   /** Memory for the use-list nodes */
   std::vector<UseListNode> d_useListNodes;
 
-  /** A fresh merge reason type to return upon request */
-  unsigned d_freshMergeReasonType;
-
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -861,16 +839,6 @@ private:
    */
   bool consistent() const { return !d_done; }
 
-  /**
-   * Marks an object for merge type based notification during equality path reconstruction.
-   */
-  void addPathReconstructionTrigger(unsigned trigger, const PathReconstructionNotify* notify);
-
-  /**
-   * Returns a fresh merge reason type tag for the client to use.
-   */
-  unsigned getFreshMergeReasonType();
-
   /** Identify this equality engine (for debugging, etc..) */
   std::string identify() const;
 };