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

6 files changed, 7 insertions, 17 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4de32a426..1a33ee3a5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -622,7 +622,6 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/options/invalid_dump.smt2
-  regress0/options/invalid_option_inc_proofs.smt2
   regress0/opt-abd-no-use.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
@@ -872,7 +871,7 @@ set(regress_0_tests
   regress0/seq/seq-nth.smt2
   regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-uf-z.smt2
-  regress0/seq/seq-nth-undef.smt2        
+  regress0/seq/seq-nth-undef.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 30c87333e..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --fewer-preprocessing-holes
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)
diff --git a/test/regress/regress0/options/invalid_option_inc_proofs.smt2 b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
deleted file mode 100644
index f63dbd27f..000000000
--- a/test/regress/regress0/options/invalid_option_inc_proofs.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-; REQUIRES: proof
-; COMMAND-LINE: --incremental --proof
-; EXPECT: (error "Error in option parsing: --incremental is not supported with proofs")
-; EXIT: 1
-(set-logic QF_BV)
-(check-sat)
diff --git a/test/regress/regress1/bv/bench_38.delta.smt2 b/test/regress/regress1/bv/bench_38.delta.smt2
index 760614348..3f809716a 100644
--- a/test/regress/regress1/bv/bench_38.delta.smt2
+++ b/test/regress/regress1/bv/bench_38.delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; COMMAND-LINE: --quiet
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress1/non-fatal-errors.smt2 b/test/regress/regress1/non-fatal-errors.smt2
index 1e1865883..ec3d02927 100644
--- a/test/regress/regress1/non-fatal-errors.smt2
+++ b/test/regress/regress1/non-fatal-errors.smt2
@@ -2,11 +2,10 @@
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
+; EXPECT: unsupported
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
-; EXPECT: success
-; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
@@ -22,7 +21,6 @@
 (declare-fun p () Bool)
 (get-unsat-core)
 (get-value (p))
-(get-proof)
 (get-model)
 (get-assignment)
 (assert true)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 9edc4df2b..f900e78a9 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: proof
-; COMMAND-LINE: --dump-instantiations --proof --print-inst-full
+; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
 ; EXPECT: unsat
 ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( 2 )
@@ -21,7 +21,7 @@
 (assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
 (assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
 (assert (S 2))
-; This tests that --proof minimizes the instantiations printed out.
-; This regression should require only the 2 instantiations above, but
-; may try more.
+; This tests that --produce-unsat-cores minimizes the instantiations
+; printed out.  This regression should require only the 2
+; instantiations above, but may try more.
 (check-sat)