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

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index defc66b74..74e3c3f56 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -24,8 +24,8 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "proof/bitvector_proof.h"
 #include "prop/bv_sat_solver_notify.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
@@ -64,7 +64,6 @@ class TBitblaster
   // sat solver used for bitblasting and associated CnfStream
   std::unique_ptr<context::Context> d_nullContext;
   std::unique_ptr<prop::CnfStream> d_cnfStream;
-  proof::BitVectorProof* d_bvp;
 
   void initAtomBBStrategies();
   void initTermBBStrategies();
@@ -91,7 +90,6 @@ class TBitblaster
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
   virtual void storeBBTerm(TNode term, const Bits& bits);
-  virtual void setProofLog(proof::BitVectorProof* bvp);
 
   /**
    * Return a constant representing the value of a in the  model.
@@ -186,8 +184,7 @@ TBitblaster<T>::TBitblaster()
     : d_termCache(),
       d_modelCache(),
       d_nullContext(new context::Context()),
-      d_cnfStream(),
-      d_bvp(nullptr)
+      d_cnfStream()
 {
   initAtomBBStrategies();
   initTermBBStrategies();
@@ -218,20 +215,6 @@ void TBitblaster<T>::invalidateModelCache()
 }
 
 template <class T>
-void TBitblaster<T>::setProofLog(proof::BitVectorProof* bvp)
-{
-  if (THEORY_PROOF_ON())
-  {
-    d_bvp = bvp;
-    prop::SatSolver* satSolver = getSatSolver();
-    bvp->attachToSatSolver(*satSolver);
-    prop::SatVariable t = satSolver->trueVar();
-    prop::SatVariable f = satSolver->falseVar();
-    bvp->initCnfProof(d_cnfStream.get(), d_nullContext.get(), t, f);
-  }
-}
-
-template <class T>
 Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 {
   if (d_modelCache.find(node) != d_modelCache.end()) return d_modelCache[node];