From c5d2f79e86d460addd922649a64a57eeb10ec059 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 1 Apr 2022 16:22:42 -0300 Subject: [PATCH] [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. --- src/proof/alethe/alethe_post_processor.cpp | 2 +- test/regress/cli/CMakeLists.txt | 3 +- .../regress0/proofs/nomerge-alethe-pf.smt2 | 73 +++++++++++++++++++ 3 files changed, 76 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 3e182f882..f6a0fa619 100644 --- 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 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 54676cfe9..c58f0948d 100644 --- 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 index 000000000..f8c1a3fbc --- /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) -- 2.30.2