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).

3 files changed, 34 insertions, 49 deletions

diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 2c5eab94c..eb87db4de 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -14,13 +14,15 @@
  ** This class implements pre-process steps for admissible recursive function definitions (Reynolds et al IJCAR2016)
  **/
 
+#include "theory/quantifiers/fun_def_process.h"
+
 #include <vector>
 
-#include "theory/quantifiers/fun_def_process.h"
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
-#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -86,7 +88,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
         Trace("fmf-fun-def") << "  to " << std::endl;
         Node new_q = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
         new_q = Rewriter::rewrite( new_q );
-        PROOF( ProofManager::currentPM()->addDependence(new_q, assertions[i]); );
+        if (options::unsatCores())
+        {
+          ProofManager::currentPM()->addDependence(new_q, assertions[i]);
+        }
         assertions[i] = new_q;
         Trace("fmf-fun-def") << "  " << assertions[i] << std::endl;
         fd_assertions.push_back( i );
@@ -120,7 +125,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) {
                                    << std::endl;
       Trace("fmf-fun-def-rewrite") << "  to " << std::endl;
       Trace("fmf-fun-def-rewrite") << "  " << n << std::endl;
-      PROOF(ProofManager::currentPM()->addDependence(n, assertions[i]););
+      if (options::unsatCores())
+      {
+        ProofManager::currentPM()->addDependence(n, assertions[i]);
+      }
       assertions[i] = n;
     }
   }
@@ -175,8 +183,12 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
             c = simplifyFormula( n[i], newPol, newHasPol, cconstraints, hd, false, visited, visited_cons );
             if( branch_pos ){
               // if at a branching position, the other constraints don't matter if this is satisfied
-              Node bcons = cconstraints.empty() ? NodeManager::currentNM()->mkConst( true ) : 
-                           ( cconstraints.size()==1 ? cconstraints[0] : NodeManager::currentNM()->mkNode( AND, cconstraints ) );
+              Node bcons = cconstraints.empty()
+                               ? NodeManager::currentNM()->mkConst(true)
+                               : (cconstraints.size() == 1
+                                      ? cconstraints[0]
+                                      : NodeManager::currentNM()->mkNode(
+                                          AND, cconstraints));
               branch_constraints.push_back( bcons );
               Trace("fmf-fun-def-debug2") << "Branching constraint at arg " << i << " is " << bcons << std::endl;
             }
@@ -201,10 +213,14 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod
             // in the default case, we care about all conditions
             branch_cond = constraints.size()==1 ? constraints[0] : NodeManager::currentNM()->mkNode( AND, constraints );
             for( unsigned i=0; i<n.getNumChildren(); i++ ){
-              // if this child holds with forcing polarity (true child of OR or false child of AND), 
-              // then we only care about its associated recursive conditions 
-              branch_cond = NodeManager::currentNM()->mkNode( kind::ITE, 
-                              ( n.getKind()==OR ? n[i] : n[i].negate() ), branch_constraints[i], branch_cond );
+              // if this child holds with forcing polarity (true child of OR or
+              // false child of AND), then we only care about its associated
+              // recursive conditions
+              branch_cond = NodeManager::currentNM()->mkNode(
+                  kind::ITE,
+                  (n.getKind() == OR ? n[i] : n[i].negate()),
+                  branch_constraints[i],
+                  branch_cond);
             }
           }
           Trace("fmf-fun-def-debug2") << "Made branching condition " << branch_cond << std::endl;
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 77b61e9dd..04b6e0dda 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -577,18 +579,21 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
 {
   // only if unsat core available
-  if (options::proof())
+  if (options::unsatCores())
   {
     if (!ProofManager::currentPM()->unsatCoreAvailable())
     {
       return false;
     }
   }
+  else
+  {
+    return false;
+  }
 
   Trace("inst-unsat-core") << "Get instantiations in unsat core..."
                            << std::endl;
-  ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS,
-                                                  active_lemmas);
+  ProofManager::currentPM()->getLemmasInUnsatCore(active_lemmas);
   if (Trace.isOn("inst-unsat-core"))
   {
     Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: "
@@ -602,27 +607,6 @@ bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
   return true;
 }
 
-bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
-                                     std::map<Node, Node>& weak_imp)
-{
-  if (getUnsatCoreLemmas(active_lemmas))
-  {
-    for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i)
-    {
-      Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore(
-          active_lemmas[i]);
-      if (n != active_lemmas[i])
-      {
-        Trace("inst-unsat-core") << "  weaken : " << active_lemmas[i] << " -> "
-                                 << n << std::endl;
-      }
-      weak_imp[active_lemmas[i]] = n;
-    }
-    return true;
-  }
-  return false;
-}
-
 void Instantiate::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node> >& tvecs)
 {
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index cb40bbbbc..8b1e0f7fc 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -268,21 +268,6 @@ class Instantiate : public QuantifiersUtil
    * This method returns false if the unsat core is not available.
    */
   bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
-  /** get unsat core lemmas
-   *
-   * If this method returns true, then it appends to active_lemmas all lemmas
-   * that are in the unsat core that originated from the theory of quantifiers.
-   * This method returns false if the unsat core is not available.
-   *
-   * It also computes a weak implicant for each of these lemmas. For each lemma
-   * L in active_lemmas, this is a formula L' such that:
-   *   L => L'
-   * and replacing L by L' in the unsat core results in a set that is still
-   * unsatisfiable. The map weak_imp stores this formula for each formula in
-   * active_lemmas.
-   */
-  bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas,
-                          std::map<Node, Node>& weak_imp);
   /** get explanation for instantiation lemmas
    *
    *