[proofs] [alethe] Fix Alethe post-processor (#8525)

Previously the Alethe post-processor was merging subproofs, which should not be done at this stage. As a consequence some post-processed proofs were becoming open.

diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 3e182f882d7b55421a869c447dffb68cd653322c..f6a0fa6198b3f78ae9cfb87abf35c402b5605203 100644 (file)
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -1831,7 +1831,7 @@ AletheProofPostprocess::~AletheProofPostprocess() {}
 void AletheProofPostprocess::process(std::shared_ptr<ProofNode> pf)
 {
   // Translate proof node
-  ProofNodeUpdater updater(d_pnm, d_cb, true, false);
+  ProofNodeUpdater updater(d_pnm, d_cb, false, false);
   updater.process(pf->getChildren()[0]);
 
   // In the Alethe proof format the final step has to be (cl). However, after

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 54676cfe9be8de37e8eab5f092dd36e1b88c1e5f..c58f0948d9cd561a19f1c7c18374e2a2414d98ac 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -952,6 +952,7 @@ set(regress_0_tests
   regress0/proofs/cyclic-ucp.smt2
   regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/lfsc-test-1.smt2
+  regress0/proofs/nomerge-alethe-pf.smt2
   regress0/proofs/open-pf-datatypes.smt2
   regress0/proofs/open-pf-if-unordered-iff.smt2
   regress0/proofs/open-pf-rederivation.smt2
@@ -1052,7 +1053,7 @@ set(regress_0_tests
   regress0/quantifiers/issue8001-mem-leak.smt2
   regress0/quantifiers/issue8159-3-qext-nterm.smt2
   regress0/quantifiers/issue8227-subs-shadow.smt2
-  regress0/quantifiers/issue8466-syqi-bool.smt2 
+  regress0/quantifiers/issue8466-syqi-bool.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2

diff --git a/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2
new file mode 100644 (file)
index 0000000..f8c1a3f
--- /dev/null
+++ b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2
@@ -0,0 +1,73 @@
+; COMMAND-LINE: --dump-proofs --proof-format-mode=alethe --dag-thresh=0 --simplification=none --proof-granularity=theory-rewrite
+; EXIT: 0
+; SCRUBBER: grep -v -E '.*'
+(set-logic AUFLIA)
+(declare-sort S$ 0)
+(declare-sort Nat$ 0)
+(declare-sort Enat$ 0)
+(declare-sort Hmultiset$ 0)
+(declare-sort S_enat_fun$ 0)
+(declare-sort V_enat_fun$ 0)
+(declare-sort V_s_set_fun$ 0)
+(declare-sort S_hmultiset_fun$ 0)
+(declare-sort S_s_bool_fun_fun$ 0)
+(declare-sort Hmultiset_multiset$ 0)
+(declare-sort S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$ 0)
+(declare-fun f$ () S$)
+(declare-fun one$ () Hmultiset$)
+(declare-fun enat$ (Nat$) Enat$)
+(declare-fun extf$ () S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$)
+(declare-fun less$ (Enat$ Enat$) Bool)
+(declare-fun zero$ () Enat$)
+(declare-fun delta$ () Nat$)
+(declare-fun hMSet$ (Hmultiset_multiset$) Hmultiset$)
+(declare-fun less$a (Nat$ Nat$) Bool)
+(declare-fun less$b (Hmultiset$ Hmultiset$) Bool)
+(declare-fun minus$ (Nat$ Nat$) Nat$)
+(declare-fun times$ (Enat$ Enat$) Enat$)
+(declare-fun zero$a () Nat$)
+(declare-fun zero$b () Hmultiset_multiset$)
+(declare-fun zero$c () Hmultiset$)
+(declare-fun gt_sym$ () S_s_bool_fun_fun$)
+(declare-fun minus$a (Hmultiset$ Hmultiset$) Hmultiset$)
+(declare-fun of_nat$ (Nat$) Hmultiset$)
+(declare-fun times$a (Nat$ Nat$) Nat$)
+(declare-fun times$b (Hmultiset$ Hmultiset$) Hmultiset$)
+(declare-fun wt_sym$ () S_hmultiset_fun$)
+(declare-fun epsilon$ () Nat$)
+(declare-fun fun_app$ (S_enat_fun$ S$) Enat$)
+(declare-fun less_eq$ (Hmultiset$ Hmultiset$) Bool)
+(declare-fun of_nat$a (Nat$) Enat$)
+(declare-fun of_nat$b (Nat$) Nat$)
+(declare-fun add_mset$ (Hmultiset$ Hmultiset_multiset$) Hmultiset_multiset$)
+(declare-fun fun_app$a (S_hmultiset_fun$ S$) Hmultiset$)
+(declare-fun infinity$ () Enat$)
+(declare-fun the_enat$ (Enat$) Nat$)
+(declare-fun arity_sym$ () S_enat_fun$)
+(declare-fun arity_var$ () V_enat_fun$)
+(declare-fun hmset_of_enat$ (Enat$) Hmultiset$)
+(declare-fun kbo_std_basis$ (V_s_set_fun$ S_s_bool_fun_fun$ S_enat_fun$ V_enat_fun$ S_hmultiset_fun$ Nat$ Nat$ S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) Bool)
+(declare-fun ground_heads_var$ () V_s_set_fun$)
+(assert (forall ((?v0 Enat$)) (=> (=> (= ?v0 zero$) false) (less$ zero$ ?v0))))
+(assert (forall ((?v0 Nat$)) (=> (=> (= ?v0 zero$a) false) (less$a zero$a ?v0))))
+(assert (forall ((?v0 Nat$)) (= (hmset_of_enat$ (enat$ ?v0)) (of_nat$ ?v0))))
+(assert (forall ((?v0 Enat$) (?v1 Enat$)) (= (= (hmset_of_enat$ ?v0) (hmset_of_enat$ ?v1)) (= ?v0 ?v1))))
+(assert (forall ((?v0 Enat$)) (= (less$b (hmset_of_enat$ ?v0) (hMSet$ (add_mset$ one$ zero$b))) (not (= ?v0 infinity$)))))
+(assert (forall ((?v0 V_s_set_fun$) (?v1 S_s_bool_fun_fun$) (?v2 S_enat_fun$) (?v3 V_enat_fun$) (?v4 S_hmultiset_fun$) (?v5 Nat$) (?v6 Nat$) (?v7 S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) (?v8 S$)) (=> (and (kbo_std_basis$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5 ?v6 ?v7) (less$a zero$a ?v6)) (not (= (fun_app$ ?v2 ?v8) infinity$)))))
+(assert (forall ((?v0 V_s_set_fun$) (?v1 S_s_bool_fun_fun$) (?v2 S_enat_fun$) (?v3 V_enat_fun$) (?v4 S_hmultiset_fun$) (?v5 Nat$) (?v6 Nat$) (?v7 S_s_v_tm_s_v_tm_bool_fun_fun_s_v_tm_list_s_v_tm_list_bool_fun_fun_fun_fun$) (?v8 S$)) (=> (kbo_std_basis$ ?v0 ?v1 ?v2 ?v3 ?v4 ?v5 ?v6 ?v7) (less_eq$ (of_nat$ (minus$ ?v5 (the_enat$ (times$ (of_nat$a ?v6) (fun_app$ ?v2 ?v8))))) (fun_app$a ?v4 ?v8)))))
+(assert (kbo_std_basis$ ground_heads_var$ gt_sym$ arity_sym$ arity_var$ wt_sym$ epsilon$ delta$ extf$))
+(assert (forall ((?v0 Hmultiset$)) (=> (less$b ?v0 (hMSet$ (add_mset$ one$ zero$b))) (exists ((?v1 Nat$)) (= ?v0 (of_nat$ ?v1))))))
+(assert (forall ((?v0 Enat$) (?v1 Enat$)) (= (= (times$ ?v0 ?v1) zero$) (or (= ?v0 zero$) (= ?v1 zero$)))))
+(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$a ?v0 ?v1) zero$a) (or (= ?v0 zero$a) (= ?v1 zero$a)))))
+(assert (forall ((?v0 Hmultiset$) (?v1 Hmultiset$)) (= (= (times$b ?v0 ?v1) zero$c) (or (= ?v0 zero$c) (= ?v1 zero$c)))))
+(assert (= (of_nat$b zero$a) zero$a))
+(assert (= (of_nat$ zero$a) zero$c))
+(assert (= (of_nat$a zero$a) zero$))
+(assert (forall ((?v0 Nat$)) (= (of_nat$a ?v0) (enat$ ?v0))))
+(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$ (minus$ ?v0 ?v1)) (minus$a (of_nat$ ?v0) (of_nat$ ?v1)))))
+(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$b (times$a ?v0 ?v1)) (times$a (of_nat$b ?v0) (of_nat$b ?v1)))))
+(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$ (times$a ?v0 ?v1)) (times$b (of_nat$ ?v0) (of_nat$ ?v1)))))
+(assert (forall ((?v0 Nat$) (?v1 Nat$)) (= (of_nat$a (times$a ?v0 ?v1)) (times$ (of_nat$a ?v0) (of_nat$a ?v1)))))
+(assert (forall ((?v0 Nat$)) (= (the_enat$ (enat$ ?v0)) ?v0)))
+(assert (not (less_eq$ (minus$a (of_nat$ epsilon$) (times$b (of_nat$ delta$) (hmset_of_enat$ (fun_app$ arity_sym$ f$)))) (fun_app$a wt_sym$ f$))))
+(check-sat)