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, 31 insertions, 24 deletions

diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 6641310cc..9429e4ced 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,7 +23,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "proof/clause_id.h"
-#include "proof/proof.h"
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/System.h"
 
@@ -64,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
       asymm_lits(0),
       eliminated_vars(0),
       elimorder(1),
-      use_simplification(!PROOF_ON()),
+      use_simplification(true),
       occurs(ClauseDeleted(ca)),
       elim_heap(ElimLt(n_occ)),
       bwdsub_assigns(0),
@@ -94,7 +93,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
 
 SimpSolver::~SimpSolver()
 {
-  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time); 
+  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
 }
 
 
@@ -111,7 +110,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
         touched   .push(0);
         elim_heap .insert(v);
         if (freeze) {
-          setFrozen(v, true); 
+          setFrozen(v, true);
         }
     }
     return v;
@@ -122,7 +121,7 @@ Var SimpSolver::newVar(bool sign, bool dvar, bool freeze) {
 lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 {
     only_bcp = false;
-  
+
     vec<Var> extra_frozen;
     lbool    result = l_True;
 
@@ -210,14 +209,15 @@ void SimpSolver::removeClause(CRef cr)
   const Clause& clause = ca[cr];
 
   if (use_simplification)
+  {
     for (int i = 0; i < clause.size(); i++)
     {
       n_occ[toInt(clause[i])]--;
       updateElimHeap(var(clause[i]));
       occurs.smudge(var(clause[i]));
     }
-
-    Solver::removeClause(cr);
+  }
+  Solver::removeClause(cr);
 }
 
 
@@ -546,9 +546,10 @@ bool SimpSolver::eliminateVar(Var v)
 
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++)
-            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
-                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
-                return true;
+          if (merge(ca[pos[i]], ca[neg[j]], v, clause_size)
+              && (++cnt > cls.size() + grow
+                  || (clause_lim != -1 && clause_size > clause_lim)))
+            return true;
 
     // Delete and store old clauses:
     eliminated[v] = true;
@@ -565,8 +566,7 @@ bool SimpSolver::eliminateVar(Var v)
         mkElimClause(elimclauses, ~mkLit(v));
     }
 
-    for (int i = 0; i < cls.size(); i++)
-        removeClause(cls[i]); 
+    for (int i = 0; i < cls.size(); i++) removeClause(cls[i]);
 
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
@@ -580,7 +580,7 @@ bool SimpSolver::eliminateVar(Var v)
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
-    
+
     // Free watchers lists for this variable, if possible:
     if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
     if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
@@ -600,7 +600,7 @@ bool SimpSolver::substitute(Var v, Lit x)
     eliminated[v] = true;
     setDecisionVar(v, false);
     const vec<CRef>& cls = occurs.lookup(v);
-    
+
     vec<Lit>& subst_clause = add_tmp;
     for (int i = 0; i < cls.size(); i++){
       Clause& clause = ca[cls[i]];
@@ -643,7 +643,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 {
 
   //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
-  
+
     if (!simplify())
         return false;
     else if (!use_simplification)
@@ -655,9 +655,12 @@ bool SimpSolver::eliminate(bool turn_off_elim)
 
         gatherTouchedClauses();
         // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
-        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
-            !backwardSubsumptionCheck(true)){
-            ok = false; goto cleanup; }
+        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+            && !backwardSubsumptionCheck(true))
+        {
+          ok = false;
+          goto cleanup;
+        }
 
         // Empty elim_heap and return immediately on user-interrupt:
         if (asynch_interrupt){
@@ -670,7 +673,7 @@ bool SimpSolver::eliminate(bool turn_off_elim)
         // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
         for (int cnt = 0; !elim_heap.empty(); cnt++){
             Var elim = elim_heap.removeMin();
-            
+
             if (asynch_interrupt) break;
 
             if (isEliminated(elim) || value(elim) != l_Undef) continue;
@@ -720,8 +723,10 @@ bool SimpSolver::eliminate(bool turn_off_elim)
     }
 
     if (verbosity >= 1 && elimclauses.size() > 0)
-        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
-               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
+      printf(
+          "|  Eliminated clauses:     %10.2f Mb                                "
+          "      |\n",
+          double(elimclauses.size() * sizeof(uint32_t)) / (1024 * 1024));
 
     return ok;
 
@@ -772,15 +777,17 @@ void SimpSolver::garbageCollect()
 {
     // Initialize the next region to a size corresponding to the estimated utilization degree. This
     // is not precise but should avoid some unnecessary reallocations for the new region:
-    ClauseAllocator to(ca.size() - ca.wasted()); 
+    ClauseAllocator to(ca.size() - ca.wasted());
 
     cleanUpClauses();
     to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
     relocAll(to);
     Solver::relocAll(to);
     if (verbosity >= 2)
-        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
-               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
+      printf(
+          "|  Garbage collection:   %12d bytes => %12d bytes             |\n",
+          ca.size() * ClauseAllocator::Unit_Size,
+          to.size() * ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }