Enable ALF proof printer (cvc5#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 cvc5#10112, cvc5#10113 first.
ajreynol · Oct 19, 2023 · 484049b · 484049b
1 parent b8a0b6e
commit 484049b
Show file tree

Hide file tree

Showing 31 changed files with 137 additions and 73 deletions.
diff --git 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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)