From b40f7ed10656c6ddd2d334bdb972130375d7312c Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 1 Apr 2022 17:29:41 -0300 Subject: [PATCH] Replace regression by minimized one via ddSMT (#8531) --- .../regress0/proofs/nomerge-alethe-pf.smt2 | 102 ++++++------------ 1 file changed, 34 insertions(+), 68 deletions(-) diff --git a/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 index f8c1a3fbc..ae03cb50b 100644 --- a/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 +++ b/test/regress/cli/regress0/proofs/nomerge-alethe-pf.smt2 @@ -2,72 +2,38 @@ ; 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$)))) +(declare-const x Bool) +(declare-sort S 0) +(declare-sort N 0) +(declare-sort E 0) +(declare-sort H 0) +(declare-sort S_ 0) +(declare-sort V 0) +(declare-sort h 0) +(declare-fun f () S) +(declare-fun d () N) +(declare-fun m (N N) N) +(declare-fun r () N) +(declare-fun m (H H) H) +(declare-fun o (N) H) +(declare-fun t (N N) N) +(declare-fun t (H H) H) +(declare-fun w () h) +(declare-fun p () N) +(declare-fun u (S_ S) E) +(declare-fun l (H H) Bool) +(declare-fun of (N) E) +(declare-fun u (h S) H) +(declare-fun t (E) N) +(declare-fun a () S_) +(declare-fun h (E) H) +(assert (forall ((? N)) (= (o d) (h (of r))))) +(assert (forall ((? E) (v E)) (= (h ?) (h v)))) +(assert (forall ((? V)) (or (l (u w f) (o (m p (t (of r)))))))) +(assert (forall ((v H)) (= x (= (o r) (t v v))))) +(assert (forall ((v N)) (= (o (m p v)) (m (o p) (o v))))) +(assert (forall ((v N)) (= (o (t r v)) (t (o v) (o v))))) +(assert (forall ((v N)) (= (of r) (of (t r v))))) +(assert (forall ((? N)) (= ? (t (of ?))))) +(assert (not (l (u w f) (m (o p) (t (o d) (h (u a f))))))) (check-sat) -- 2.30.2