From 484049bee20be95a0e73ce45d3801fa0ce98aff7 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Oct 2023 16:05:55 -0500
Subject: [PATCH] Enable ALF proof printer (#10114)

Changes:

Add the proof option --proof-format=alf
Add the regression tester make regress-alf
Fixes current regressions that don't pass by disabling the above tester (the main cause is smt-lib 2.6 datatypes and naming conflicts), or by eliminating overloading in symbols
Add news entry.
Also removes an experimental proof rule file (Conversions.smt3) which was added by mistake.

Review #10112, #10113 first.
---
 NEWS.md                                       |  9 +++
 contrib/get-alf-checker                       |  4 +-
 proofs/alf/rules/Conversions.smt3             | 48 -------------
 src/options/proof_options.toml                |  3 +
 src/smt/proof_manager.cpp                     | 11 +++
 test/regress/cli/CMakeLists.txt               |  3 +
 .../cli/regress0/datatypes/dt-sel-2.6.smt2    |  1 +
 .../datatypes/issue8883-sort-inf.smt2         |  1 +
 .../datatypes/par-updater-type-rule.smt2      |  5 +-
 .../cli/regress0/proofs/proof-components.smt2 |  1 +
 .../regress0/proofs/t1-difficulty-filter.smt2 |  1 +
 .../quantifiers/dd.german169-ieval.smt2       |  6 +-
 test/regress/cli/regress1/bug296.smt2         |  1 +
 .../regress1/datatypes/cee-prs-small-dd2.smt2 |  6 +-
 .../proj-issue433-tester-merge-pf.smt2        |  2 +-
 test/regress/cli/regress1/fmf/agree467.smt2   |  1 +
 .../cli/regress1/fp/rti_3_5_bug_report.smt2   |  1 +
 .../cli/regress1/quantifiers/bug_743.smt2     |  1 +
 .../cli/regress1/quantifiers/cee-npnt-dd.smt2 |  6 +-
 .../regress1/quantifiers/ddatv-delta2.smt2    |  6 +-
 .../quantifiers/inst-max-level-segf.smt2      |  1 +
 .../quantifiers/issue4400-2-already-conf.smt2 |  1 +
 .../quantifiers/min-ppgt-em-incomplete2.smt2  |  6 +-
 .../quantifiers/parametric-lists.smt2         |  1 +
 .../seqa-unsat-unknown-110921.smt2            |  1 +
 .../cli/regress1/quantifiers/set3.smt2        |  1 +
 .../cli/regress1/quantifiers/set8.smt2        |  1 +
 .../cli/regress1/quantifiers/seu169+1.smt2    |  1 +
 test/regress/cli/regress2/bug812.smt2         |  7 +-
 .../cli/regress2/issue6495-dup-pat-term.smt2  |  1 +
 test/regress/cli/run_regression.py            | 72 ++++++++++++++++++-
 31 files changed, 137 insertions(+), 73 deletions(-)
 delete mode 100644 proofs/alf/rules/Conversions.smt3

diff --git a/NEWS.md b/NEWS.md
index 4a6df14b257..9bc153f5cea 100644
--- a/NEWS.md
+++ b/NEWS.md
@@ -9,6 +9,15 @@ This file contains a summary of important user-visible changes.
        The function `Solver::proofToString(std::vector<Proof> proof,
        modes::ProofFormat format, modes::ProofComponent component)` can be used
        to print proof components to a string with a specified proof format.
+- Support for the AletheLF (ALF) proof format. This format combines the
+  strengths of the Alethe and LFSC proof formats, namely it borrows much of the
+  syntax of Alethe, while being based on a logical framework like LFSC. This
+  proof format is currently under development and is planned to the default
+  proof format used cvc5 in future releases.
+  * API: The option `--proof-format=alf` can be used to print proofs in the
+         AletheLF format.
+  * The ALF proof checker (alfc) is available for download via the script
+    `./contrib/get-alf-checker`.
 - CaDiCaL is now integrated via the IPASIR-UP interface as CDCL(T) SAT solver.
   The CDCL(T) SAT solver can be configured via option `--sat-solver`. Currently,
   MiniSat is still default. Note that CaDiCaL cannot be used as the CDCL(T) SAT
diff --git a/contrib/get-alf-checker b/contrib/get-alf-checker
index ea0eeafa8f3..fd344161d55 100755
--- a/contrib/get-alf-checker
+++ b/contrib/get-alf-checker
@@ -50,10 +50,10 @@ cat << EOF > $BASE_DIR/bin/alfc_gen_and_check.sh
 #!/usr/bin/env bash
 
 echo "=== Generate proof: \$@"
-$BASE_DIR/bin/alfc_gen.sh \$@ > alfc.proof.smt2
+$BASE_DIR/bin/alfc_gen.sh \$@ > alfc.proof.smt3
 
 echo "=== Check proof with ALFC"
-$BASE_DIR/bin/alfc_check.sh alfc.proof.smt2
+$BASE_DIR/bin/alfc_check.sh alfc.proof.smt3
 EOF
 chmod +x $BASE_DIR/bin/alfc_gen_and_check.sh
 
diff --git a/proofs/alf/rules/Conversions.smt3 b/proofs/alf/rules/Conversions.smt3
deleted file mode 100644
index 756ff6ef4cb..00000000000
--- a/proofs/alf/rules/Conversions.smt3
+++ /dev/null
@@ -1,48 +0,0 @@
-(include "../theories/Builtin.smt3")
-(include "../theories/Quantifiers.smt3")
-
-(program run_convert_fixed_point
-  ((T Type) (U Type) (x U) (y U) (f (-> T U)) (a T) (z1 @List) (z2 @List :list) (w T))
-  (U @List) (@Pair U @List)
-  (
-    ((run_convert_fixed_point x (@list (= x y) z2)) (run_convert_fixed_point y z2))
-    ((run_convert_fixed_point (skolem w) z1)        (@pair (skolem w) z1))   ; do not traverse into skolems
-    ((run_convert_fixed_point (f a) (@list z1 z2))  (alf.match ((fr (-> T U)) (zr @List)) (run_convert_fixed_point f (@list z1 z2))
-                                                    ((@pair fr zr)
-                                                        (alf.match ((ar (-> T U)) (zrr @List)) (run_convert_fixed_point a zr)
-                                                          ((@pair ar zrr) (@pair (fr ar) zrr))))))
-    ((run_convert_fixed_point x @list.nil)          (@pair x @list.nil))
-  )
-)
-
-(declare-rule convert_fixed_point ((T Type) (t T))
-  :premise-list E @list
-  :args (t)
-  :conclusion (alf.match ((s T)) (run_convert_fixed_point t E)
-                (
-                  ((@pair s @list.nil) (= t s))
-                ))
-)
-
-(program run_convert_once
-  ((T Type) (U Type) (x U) (y U) (f (-> T U)) (a T) (z1 @List) (z2 @List) (w T))
-  (U @List) (@Pair U @List)
-  (
-    ((run_convert_once x (@list (= x y) z2)) (@pair y z2))
-    ((run_convert_once (skolem w) z2)        (@pair (skolem w) z2))   ; do not traverse into skolems
-    ((run_convert_once (f a) (@list z1 z2))  (alf.match ((fr (-> T U)) (zr @List)) (run_convert_once f (@list z1 z2))
-                                                ((@pair fr zr)
-                                                    (alf.match ((ar (-> T U)) (zrr @List)) (run_convert_once a zr)
-                                                      ((@pair ar zrr) (@pair (fr ar) zrr))))))
-    ((run_convert_once x true)               (@pair x true))
-  )
-)
-
-(declare-rule convert_once ((T Type) (t T))
-  :premise-list E @list
-  :args (t)
-  :conclusion (alf.match ((s T)) (run_convert_once t E)
-                (
-                  ((@pair s @list.nil) (= t s))
-                ))
-)
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index dfb97aa9e30..4b02a694ad4 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -21,6 +21,9 @@ name   = "Proof"
 [[option.mode.ALETHE]]
   name       = "alethe"
   help       = "Output Alethe proof"
+[[option.mode.ALF]]
+  name       = "alf"
+  help       = "Output AletheLF proof"
 
 [[option]]
   name       = "proofPrintConclusion"
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index cc7a3e214aa..47d4a3605b9 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -21,6 +21,8 @@
 #include "proof/alethe/alethe_node_converter.h"
 #include "proof/alethe/alethe_post_processor.h"
 #include "proof/alethe/alethe_printer.h"
+#include "proof/alf/alf_post_processor.h"
+#include "proof/alf/alf_printer.h"
 #include "proof/dot/dot_printer.h"
 #include "proof/lfsc/lfsc_post_processor.h"
 #include "proof/lfsc/lfsc_printer.h"
@@ -242,6 +244,15 @@ void PfManager::printProof(std::ostream& out,
     proof::DotPrinter dotPrinter(d_env);
     dotPrinter.print(out, fp.get());
   }
+  else if (mode == options::ProofFormatMode::ALF)
+  {
+    Assert(fp->getRule() == ProofRule::SCOPE);
+    proof::AlfNodeConverter atp;
+    proof::AlfProofPostprocess alfpp(d_env, atp);
+    alfpp.process(fp);
+    proof::AlfPrinter alfp(d_env, atp);
+    alfp.print(out, fp);
+  }
   else if (mode == options::ProofFormatMode::ALETHE)
   {
     proof::AletheNodeConverter anc;
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 9ff6ec8fdb7..98986fece1f 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -3625,6 +3625,7 @@ set(testers
   abduct
   dump
   dsl-proof
+  alf
 )
 
 foreach(tester ${testers})
@@ -3665,6 +3666,8 @@ macro(cvc5_add_regression_test level file)
     ${RUN_REGRESSION_ARGS}
     --lfsc-binary ${CMAKE_SOURCE_DIR}/deps/bin/lfscc
     --lfsc-sig-dir ${CMAKE_SOURCE_DIR}/proofs/lfsc/signatures
+    --alfc-binary ${CMAKE_SOURCE_DIR}/deps/bin/alfc
+    --alf-sig-dir ${CMAKE_SOURCE_DIR}/proofs/alf
     ${wrapper}
     ${path_to_cvc5}/cvc5${CMAKE_EXECUTABLE_SUFFIX}
     ${CMAKE_CURRENT_LIST_DIR}/${file})
diff --git a/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2 b/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2
index 0fdc0547154..89d63eb0633 100644
--- a/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2
+++ b/test/regress/cli/regress0/datatypes/dt-sel-2.6.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((IntList 0)) (
diff --git a/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2 b/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
index 678b0bd2fca..ea2913eec4a 100644
--- a/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
+++ b/test/regress/cli/regress0/datatypes/issue8883-sort-inf.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --sort-inference
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic ALL)
 (declare-datatypes ((Data 1)) ((par (T) ((data)))))
 (declare-fun p2 () (Data Bool))
diff --git a/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2 b/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2
index 0b4af02877b..c7f2fda2633 100644
--- a/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2
+++ b/test/regress/cli/regress0/datatypes/par-updater-type-rule.smt2
@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alf
 (set-option :global-declarations true)
 (set-logic ALL)
 (set-info :status unsat)
@@ -6,6 +7,6 @@
 (declare-const _x53 Bool)
 (declare-const _x56 _x36)
 (declare-const _x58 _x0)
-(declare-datatype _x176 ( par ( _x178 ) ( (_x186 (_x185 _x178)) (_x184 (_x180 _x0)))) )
-(assert (let ((_let0 ((_ update _x185) (_x184 _x58) _x58)))(distinct _let0 _let0)))
+(declare-datatype D ( par ( A ) ( (c (s A)) (b (_x180 _x0)))) )
+(assert (let ((_let0 ((_ update s) ((as b (D Int)) _x58) _x58)))(distinct _let0 _let0)))
 (check-sat)
diff --git a/test/regress/cli/regress0/proofs/proof-components.smt2 b/test/regress/cli/regress0/proofs/proof-components.smt2
index d7e3dff3db3..fddd1cf3a13 100644
--- a/test/regress/cli/regress0/proofs/proof-components.smt2
+++ b/test/regress/cli/regress0/proofs/proof-components.smt2
@@ -2,6 +2,7 @@
 ; COMMAND-LINE: --simplification=none
 ; EXPECT: unsat
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alf
 (set-logic QF_UFLIA)
 (set-info :smt-lib-version 2.0)
 (set-info :category "crafted")
diff --git a/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2 b/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2
index cdfa7aa0604..32fbad46bdb 100644
--- a/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2
+++ b/test/regress/cli/regress0/proofs/t1-difficulty-filter.smt2
@@ -2,6 +2,7 @@
 ; SCRUBBER: sed 's/(.*//g;s/).*//g'
 ; EXPECT: unsat
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alf
 (set-logic UFLIA)
 (declare-fun f (Int) Int) 
 (declare-fun g (Int) Int) 
diff --git a/test/regress/cli/regress0/quantifiers/dd.german169-ieval.smt2 b/test/regress/cli/regress0/quantifiers/dd.german169-ieval.smt2
index 5265f04f61e..69c919d42d0 100644
--- a/test/regress/cli/regress0/quantifiers/dd.german169-ieval.smt2
+++ b/test/regress/cli/regress0/quantifiers/dd.german169-ieval.smt2
@@ -3,8 +3,8 @@
 (set-logic ALL)
 (declare-sort s 0)
 (declare-datatypes ((ms 0)) (((a))))
-(declare-datatypes ((m 0)) (((c (m ms)))))
-(declare-fun s () s)
+(declare-datatypes ((m 0)) (((c (ml ms)))))
+(declare-fun sf () s)
 (declare-fun h () (Array s m))
-(assert (not (=> (and (forall ((n s)) (not (= a (m (select h n)))))) (= a (m (select h s))) false)))
+(assert (not (=> (and (forall ((n s)) (not (= a (ml (select h n)))))) (= a (ml (select h sf))) false)))
 (check-sat)
diff --git a/test/regress/cli/regress1/bug296.smt2 b/test/regress/cli/regress1/bug296.smt2
index ad1f89b9e90..8b9f9518c40 100644
--- a/test/regress/cli/regress1/bug296.smt2
+++ b/test/regress/cli/regress1/bug296.smt2
@@ -1,4 +1,5 @@
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic QF_ALL)
 (set-info :status unsat)
 (declare-datatypes
diff --git a/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2 b/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2
index fe422d9e404..0e892ecd06f 100644
--- a/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2
+++ b/test/regress/cli/regress1/datatypes/cee-prs-small-dd2.smt2
@@ -3,10 +3,10 @@
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
-(declare-datatypes ((r 0)) (((R (x Int)))))
+(declare-datatypes ((r 0)) (((R1 (x1 Int)))))
 (declare-datatype t ((M (t1 (Array Int Int)) (t2 (Array Int Int)))))
 (declare-datatypes ((q 0)) (((R (x (Array Int r)) (y t)))))
 (declare-fun z () q)
-(assert (= z (R ((as const (Array Int r)) (R 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
-(assert (= (x (select (x z) 0)) (select (t1 (y z)) 1)))
+(assert (= z (R ((as const (Array Int r)) (R1 0)) (M ((as const (Array Int Int)) 1) ((as const (Array Int Int)) 0)))))
+(assert (= (x1 (select (x z) 0)) (select (t1 (y z)) 1)))
 (check-sat)
diff --git a/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2 b/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2
index 9e2a428db9a..7a6fd8a933c 100644
--- a/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2
+++ b/test/regress/cli/regress1/datatypes/proj-issue433-tester-merge-pf.smt2
@@ -1,7 +1,7 @@
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((L 0)) (((i))))
-(declare-datatypes ((O 0)) (((N) (S (i (_ BitVec 3))))))
+(declare-datatypes ((O 0)) (((N) (S (i1 (_ BitVec 3))))))
 (declare-fun m (L) O)
 (declare-fun g ((_ BitVec 3) L) L)
 (assert (exists ((B L) (n (_ BitVec 3))) (not (ite ((_ is S) (m (g n B))) (not ((_ is N) (m (g n B)))) true))))
diff --git a/test/regress/cli/regress1/fmf/agree467.smt2 b/test/regress/cli/regress1/fmf/agree467.smt2
index f2b012c864a..6ff357e44ae 100644
--- a/test/regress/cli/regress1/fmf/agree467.smt2
+++ b/test/regress/cli/regress1/fmf/agree467.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --finite-model-find
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 ; Preamble  --------------
 (set-logic AUFDTLIA)
 (set-info :status unsat)
diff --git a/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2 b/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2
index 146942cecec..2dff469aeaa 100644
--- a/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2
+++ b/test/regress/cli/regress1/fp/rti_3_5_bug_report.smt2
@@ -1,4 +1,5 @@
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alf
 ; COMMAND-LINE: --fp-exp
 ; EXPECT: unsat
 
diff --git a/test/regress/cli/regress1/quantifiers/bug_743.smt2 b/test/regress/cli/regress1/quantifiers/bug_743.smt2
index e2fff8018c5..0432509b218 100644
--- a/test/regress/cli/regress1/quantifiers/bug_743.smt2
+++ b/test/regress/cli/regress1/quantifiers/bug_743.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --lang=smt2.6
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 
 ;; produced by cvc4_14.drv ;;
 (set-logic AUFBVDTNIRA)
diff --git a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2 b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
index 15727589dcc..b497ad688a7 100644
--- a/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
+++ b/test/regress/cli/regress1/quantifiers/cee-npnt-dd.smt2
@@ -5,10 +5,10 @@
 (set-info :status unsat)
 (set-option :fmf-bound true)
 (declare-datatype N ((o) (f) (s)))
-(declare-datatype P ((P)))
+(declare-datatype P ((p)))
 (declare-fun G (N P Int) Bool)
-(declare-datatype c ((c (_p P))))
+(declare-datatype c ((cc (_p P))))
 (declare-fun g (N Int Int) c)
-(assert (forall ((x N)) (not (G x P 0))))
+(assert (forall ((x N)) (not (G x p 0))))
 (assert (forall ((t Int)) (or (< t 0) (> t 1) (and (forall ((p P)) (or (exists ((y N)) (and (G y (_p (g y 0 0)) t)))))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2 b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
index b41b8c9b0ea..7940927ec51 100644
--- a/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
+++ b/test/regress/cli/regress1/quantifiers/ddatv-delta2.smt2
@@ -1,11 +1,11 @@
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort U 0)
-(declare-datatypes ((T 0) (D 0)) (((E) (o (b Bool)) (I (t Int)) (i (v D)) (R (l T) (u T))) ((i (v U)))))
+(declare-datatypes ((T 0) (D 0)) (((E) (o (b Bool)) (I (t Int)) (i (v D)) (R (l T) (u T))) ((ic (vc U)))))
 (declare-datatypes ((H 0)) (((M (h T)))))
 (declare-fun S (U Int) T)
 (declare-fun n () H)
 (assert (and 
-(not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (v (v (S (v (v E)) 0))) (t E))) (t (S (v (v (S (v (v (h n))) 0))) (t E))))))))))))))))
-(b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (v (v (S (v (v (h n))) z))) (t E))) (t (S (v (v (S (v (v (h n))) 0))) (t (I i))))))))))) :qid id))))))))))
+(not (b (o (or (b (o (or (b (o (or (b (o (= (t (S (vc (v (S (vc (v E)) 0))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t E))))))))))))))))
+(b (o (forall ((i Int)) (or (< i (t (u (R E E)))) (b (o (forall ((z Int)) (! (or (b (o (or (b (o (< (t (S (vc (v (S (vc (v (h n))) z))) (t E))) (t (S (vc (v (S (vc (v (h n))) 0))) (t (I i))))))))))) :qid id))))))))))
 (check-sat)
diff --git a/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2 b/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2
index 9bb21cae8e7..37c7beeef56 100644
--- a/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2
+++ b/test/regress/cli/regress1/quantifiers/inst-max-level-segf.smt2
@@ -1,4 +1,5 @@
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alf
 ; COMMAND-LINE: --inst-max-level=0 --simplification=none
 ; EXPECT: unsat
 (set-logic UF)
diff --git a/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2 b/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2
index 1eedb692180..b5dc7a598c6 100644
--- a/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2
+++ b/test/regress/cli/regress1/quantifiers/issue4400-2-already-conf.smt2
@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alf
 (set-logic ALL)
 (set-info :status unsat)
 (declare-datatypes ((ap 0)) (((bp) (cp (p (_ BitVec 2)) (dp (_ BitVec 2))
diff --git a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
index 8f31750b2e6..c34fbbee461 100644
--- a/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
+++ b/test/regress/cli/regress1/quantifiers/min-ppgt-em-incomplete2.smt2
@@ -4,13 +4,13 @@
 (declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int)))))
 (declare-sort V 0)
 (declare-datatypes ((T 0) (TArray 0)) (((E) (b (B Bool)) (A (add Int)) (Vec (vec TArray))) ((Var (R V) (|l#Var| Int)))))
-(declare-sort B 0)
-(declare-datatypes ((M 0)) (((Mem (cm B)))))
+(declare-sort Bb 0)
+(declare-datatypes ((M 0)) (((Mem (cm Bb)))))
 (declare-fun mc (D) U)
 (declare-fun eq (T T) Bool)
 (declare-fun s (V Int) T)
 (declare-fun sto (V Int T) V)
-(declare-fun sel (B T@t Int) T)
+(declare-fun sel (Bb T@t Int) T)
 (declare-fun c () T)
 (declare-fun in () M)
 (declare-fun rdv () T)
diff --git a/test/regress/cli/regress1/quantifiers/parametric-lists.smt2 b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2
index 4fe8221abf8..89744cded09 100644
--- a/test/regress/cli/regress1/quantifiers/parametric-lists.smt2
+++ b/test/regress/cli/regress1/quantifiers/parametric-lists.smt2
@@ -1,3 +1,4 @@
+; DISABLE-TESTER: alf
 ; EXPECT: unsat
 (set-logic ALL)
 (set-info :status unsat)
diff --git a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2 b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2
index eeba7883bf1..b50d6dd25cf 100644
--- a/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2
+++ b/test/regress/cli/regress1/quantifiers/seqa-unsat-unknown-110921.smt2
@@ -1,4 +1,5 @@
 ; DISABLE-TESTER: lfsc
+; DISABLE-TESTER: alf
 ; COMMAND-LINE: --strings-exp --seq-array=eager
 ; EXPECT: unsat
 (set-logic ALL)
diff --git a/test/regress/cli/regress1/quantifiers/set3.smt2 b/test/regress/cli/regress1/quantifiers/set3.smt2
index e612c2f2da7..7582290c274 100644
--- a/test/regress/cli/regress1/quantifiers/set3.smt2
+++ b/test/regress/cli/regress1/quantifiers/set3.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --full-saturate-quant
+; DISABLE-TESTER: alf
 (set-logic AUFLIA)
 (set-info :source | Assertion verification of simple set manipulation programs. |)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/cli/regress1/quantifiers/set8.smt2 b/test/regress/cli/regress1/quantifiers/set8.smt2
index f44e8796c5a..2767cf2c315 100644
--- a/test/regress/cli/regress1/quantifiers/set8.smt2
+++ b/test/regress/cli/regress1/quantifiers/set8.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --ieval=use-learn
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic AUFLIA)
 (set-info :source | Set theory. |)
 (set-info :smt-lib-version 2.6)
diff --git a/test/regress/cli/regress1/quantifiers/seu169+1.smt2 b/test/regress/cli/regress1/quantifiers/seu169+1.smt2
index 0ea6faf271d..e4607f4a54a 100644
--- a/test/regress/cli/regress1/quantifiers/seu169+1.smt2
+++ b/test/regress/cli/regress1/quantifiers/seu169+1.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --relational-triggers
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic UF)
 (declare-sort $$unsorted 0)
 (declare-fun in ($$unsorted $$unsorted) Bool)
diff --git a/test/regress/cli/regress2/bug812.smt2 b/test/regress/cli/regress2/bug812.smt2
index 43ace7b3125..2d63b574f06 100644
--- a/test/regress/cli/regress2/bug812.smt2
+++ b/test/regress/cli/regress2/bug812.smt2
@@ -1,7 +1,8 @@
+; DISABLE-TESTER: alf
 (set-logic UFNIA)
-(set-info :source |
-    VCC and HAVOC benchmarks.  Contributed by Nikolaj Bjorner, Leonardo de Moura,
-    Michal Moskal, and Shaz Qadeer.
+(set-info :source |
+    VCC and HAVOC benchmarks.  Contributed by Nikolaj Bjorner, Leonardo de Moura,
+    Michal Moskal, and Shaz Qadeer.
   |)
 (set-info :smt-lib-version 2.6)
 (set-info :category "industrial")
diff --git a/test/regress/cli/regress2/issue6495-dup-pat-term.smt2 b/test/regress/cli/regress2/issue6495-dup-pat-term.smt2
index c619bb37d96..e7ae8959cf6 100644
--- a/test/regress/cli/regress2/issue6495-dup-pat-term.smt2
+++ b/test/regress/cli/regress2/issue6495-dup-pat-term.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: -i -q
 ; EXPECT: unsat
+; DISABLE-TESTER: alf
 (set-logic ALL)
 (set-info :status unsat)
 (declare-sort |T@[Int]Int| 0)
diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py
index 40c8f014c8a..fbc27770610 100755
--- a/test/regress/cli/run_regression.py
+++ b/test/regress/cli/run_regression.py
@@ -251,6 +251,64 @@ def run_internal(self, benchmark_info):
             print_ok("OK")
         return exit_code
 
+class AlfTester(Tester):
+
+    def __init__(self):
+        super().__init__("alf")
+
+    def applies(self, benchmark_info):
+        return (
+            benchmark_info.benchmark_ext != ".sy"
+            and benchmark_info.expected_output.strip() == "unsat"
+        )
+
+    def run_internal(self, benchmark_info):
+        exit_code = EXIT_OK
+        with tempfile.NamedTemporaryFile() as tmpf:
+            cvc5_args = benchmark_info.command_line_args + [
+                "--dump-proofs",
+                "--proof-format=alf",
+                "--proof-granularity=theory-rewrite",
+                "--proof-print-conclusion",
+            ]
+            output, error, exit_status = run_process(
+                [benchmark_info.cvc5_binary]
+                + cvc5_args
+                + [benchmark_info.benchmark_basename],
+                benchmark_info.benchmark_dir,
+                benchmark_info.timeout,
+            )
+            alf_sig_dir = os.path.abspath(g_args.alf_sig_dir)
+            tmpf.write(("(include \"" + alf_sig_dir + "/Cvc5.smt3\")").encode())
+            tmpf.write(output.strip("unsat\n".encode()))
+            tmpf.flush()
+            output, error = output.decode(), error.decode()
+            exit_code = self.check_exit_status(EXIT_OK, exit_status, output,
+                                               error, cvc5_args)
+            if ("step" not in output) and ("assume" not in output):
+                print_error("Empty proof")
+                print()
+                print_outputs(output, error)
+                return EXIT_FAILURE
+            if exit_code != EXIT_OK:
+                return exit_code
+            output, error, exit_status = run_process(
+                [benchmark_info.alfc_binary] +
+                [tmpf.name],
+                benchmark_info.benchmark_dir,
+                timeout=benchmark_info.timeout,
+            )
+            output, error = output.decode(), error.decode()
+            exit_code = self.check_exit_status(EXIT_OK, exit_status, output,
+                                               error, cvc5_args)
+            if "success" not in output:
+                print_error("Invalid proof")
+                print()
+                print_outputs(output, error)
+                return EXIT_FAILURE
+        if exit_code == EXIT_OK:
+            print_ok("OK")
+        return exit_code
 
 class ModelTester(Tester):
 
@@ -383,7 +441,8 @@ def run_internal(self, benchmark_info):
     "synth": SynthTester(),
     "abduct": AbductTester(),
     "dump": DumpTester(),
-    "dsl-proof": DslProofTester()
+    "dsl-proof": DslProofTester(),
+    "alf": AlfTester()
 }
 
 g_default_testers = [
@@ -408,6 +467,7 @@ def run_internal(self, benchmark_info):
         "cvc5_binary",
         "lfsc_binary",
         "lfsc_sigs",
+        "alfc_binary",
         "benchmark_dir",
         "benchmark_basename",
         "benchmark_ext",
@@ -612,6 +672,7 @@ def run_regression(
     cvc5_binary,
     lfsc_binary,
     lfsc_sigs,
+    alfc_binary,
     benchmark_path,
     timeout,
 ):
@@ -687,6 +748,8 @@ def run_regression(
                     testers.remove("lfsc")
                 if "dsl-proof" in testers:
                     testers.remove("dsl-proof")
+                if "alf" in testers:
+                    testers.remove("alf")
 
     expected_output = expected_output.strip()
     expected_error = expected_error.strip()
@@ -751,6 +814,7 @@ def run_regression(
             cvc5_binary=cvc5_binary,
             lfsc_binary=lfsc_binary,
             lfsc_sigs=lfsc_sigs,
+            alfc_binary=alfc_binary,
             benchmark_dir=benchmark_dir,
             benchmark_basename=benchmark_basename,
             benchmark_ext=benchmark_ext,
@@ -797,6 +861,8 @@ def main():
     parser.add_argument("--tester", choices=tester_choices, action="append")
     parser.add_argument("--lfsc-binary", default="")
     parser.add_argument("--lfsc-sig-dir", default="")
+    parser.add_argument("--alfc-binary", default="")
+    parser.add_argument("--alf-sig-dir", default="")
     parser.add_argument("wrapper", nargs="*")
     parser.add_argument("cvc5_binary")
     parser.add_argument("benchmark")
@@ -810,6 +876,7 @@ def main():
 
     cvc5_binary = os.path.abspath(g_args.cvc5_binary)
     lfsc_binary = os.path.abspath(g_args.lfsc_binary)
+    alfc_binary = os.path.abspath(g_args.alfc_binary)
 
     wrapper = g_args.wrapper
     if os.environ.get("VALGRIND") == "1" and not wrapper:
@@ -834,13 +901,14 @@ def main():
                      "strings_programs", "strings_rules", "quantifiers_rules"]
         lfsc_sigs = [os.path.join(lfsc_sig_dir, sig + ".plf")
                      for sig in lfsc_sigs]
-
+    alf_sig_dir = os.path.abspath(g_args.alf_sig_dir)
     return run_regression(
         testers,
         wrapper,
         cvc5_binary,
         lfsc_binary,
         lfsc_sigs,
+        alfc_binary,
         g_args.benchmark,
         timeout,
     )