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

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5da190a3d..74fcda668 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -19,7 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
-#include "options/proof_options.h"
+#include "options/smt_options.h"
 #include "proof/proof_manager.h"
 
 using namespace std;
@@ -45,16 +45,21 @@ theory::TrustNode RemoveTermFormulas::run(
 {
   Node itesRemoved = run(assertion, newAsserts, newSkolems, false, false);
   // In some calling contexts, not necessary to report dependence information.
-  if (reportDeps
-      && (options::unsatCores() || options::fewerPreprocessingHoles()))
+  if (reportDeps && options::unsatCores())
   {
     // new assertions have a dependence on the node
-    PROOF(ProofManager::currentPM()->addDependence(itesRemoved, assertion);)
+    if (options::unsatCores())
+    {
+      ProofManager::currentPM()->addDependence(itesRemoved, assertion);
+    }
     unsigned n = 0;
     while (n < newAsserts.size())
     {
-      PROOF(ProofManager::currentPM()->addDependence(newAsserts[n].getProven(),
-                                                     assertion);)
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(newAsserts[n].getProven(),
+                                                 assertion);
+      }
       ++n;
     }
   }
@@ -380,7 +385,7 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
   }else if( !inTerm && hasNestedTermChildren( node ) ){
     // Remember if we're inside a term
     inTerm = true;
-  }  
+  }
 
   vector<Node> newChildren;
   bool somethingChanged = false;
@@ -402,13 +407,14 @@ Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const {
   }
 }
 
-// returns true if the children of node should be considered nested terms 
+// returns true if the children of node should be considered nested terms
 bool RemoveTermFormulas::hasNestedTermChildren( TNode node ) {
-  return theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && 
-         node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && 
-         node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL && 
-         node.getKind()!=kind::BITVECTOR_EAGER_ATOM;
-         // dont' worry about FORALL or EXISTS (handled separately)
+  return theory::kindToTheoryId(node.getKind()) != theory::THEORY_BOOL
+         && node.getKind() != kind::EQUAL && node.getKind() != kind::SEP_STAR
+         && node.getKind() != kind::SEP_WAND
+         && node.getKind() != kind::SEP_LABEL
+         && node.getKind() != kind::BITVECTOR_EAGER_ATOM;
+  // dont' worry about FORALL or EXISTS (handled separately)
 }
 
 Node RemoveTermFormulas::getAxiomFor(Node n)