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

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index d4b08ab71..1526e91b9 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -33,11 +33,6 @@
 
 namespace CVC4 {
 
-namespace proof {
-class ClausalBitVectorProof;
-class ResolutionBitVectorProof;
-}  // namespace proof
-
 namespace prop {
 
 class TheoryProxy;
@@ -58,7 +53,7 @@ public:
 
   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
   virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
-  
+
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,6 +79,7 @@ public:
   virtual SatValue solve(const std::vector<SatLiteral>& assumptions)
   {
     Unimplemented() << "Solving under assumptions not implemented";
+    return SAT_VALUE_UNKNOWN;
   };
 
   /** Interrupt the solver */
@@ -101,10 +97,6 @@ public:
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
 
-  virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {}
-
-  virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {}
-
 };/* class SatSolver */