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

diff --git a/src/smt/command.h b/src/smt/command.h
index a0e591269..9fbd1bf73 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -33,7 +33,6 @@
 #include "expr/type.h"
 #include "expr/variable_type_map.h"
 #include "proof/unsat_core.h"
-#include "util/proof.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 
@@ -1131,9 +1130,7 @@ class CVC4_PUBLIC GetProofCommand : public Command
  public:
   GetProofCommand();
 
-  const Proof& getResult() const;
   void invoke(SmtEngine* smtEngine) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
@@ -1144,11 +1141,6 @@ class CVC4_PUBLIC GetProofCommand : public Command
       bool types = false,
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
-
- protected:
-  SmtEngine* d_smtEngine;
-  // d_result is owned by d_smtEngine.
-  const Proof* d_result;
 }; /* class GetProofCommand */
 
 class CVC4_PUBLIC GetInstantiationsCommand : public Command