From 47ca3e72bd9d4fd935d6a6cee9ab2104d80c1d08 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Tue, 27 May 2025 16:09:30 +0800 Subject: [PATCH] feat: Add definitions for basic structures. --- projects/lib/gmp_aux.v | 63 +++++++ projects/lib/gmp_number.v | 289 ++++++++++++++++++++++++++++++++ projects/{task1 => }/mini-gmp.c | 0 projects/{task1 => }/mini-gmp.h | 0 projects/task2/cnf_trans.c | 225 ------------------------- projects/task2/cnf_trans.h | 14 -- projects/task2/smt_lang.h | 42 ----- projects/task3/alpha_equiv.c | 39 ----- projects/task3/ast.h | 120 ------------- projects/task3/subst.c | 65 ------- projects/task3/thm_apply.c | 67 -------- 11 files changed, 352 insertions(+), 572 deletions(-) create mode 100644 projects/lib/gmp_aux.v create mode 100644 projects/lib/gmp_number.v rename projects/{task1 => }/mini-gmp.c (100%) rename projects/{task1 => }/mini-gmp.h (100%) delete mode 100755 projects/task2/cnf_trans.c delete mode 100755 projects/task2/cnf_trans.h delete mode 100755 projects/task2/smt_lang.h delete mode 100755 projects/task3/alpha_equiv.c delete mode 100755 projects/task3/ast.h delete mode 100755 projects/task3/subst.c delete mode 100755 projects/task3/thm_apply.c diff --git a/projects/lib/gmp_aux.v b/projects/lib/gmp_aux.v new file mode 100644 index 0000000..54a2317 --- /dev/null +++ b/projects/lib/gmp_aux.v @@ -0,0 +1,63 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Bool.Bool. +Require Import Coq.Lists.List. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.micromega.Psatz. +Require Import Permutation. +Require Import String. +From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. +Require Import SetsClass.SetsClass. Import SetsNotation. +From SimpleC.SL Require Import CommonAssertion Mem SeparationLogic IntLib. +Require Import Logic.LogicGenerator.demo932.Interface. +Local Open Scope Z_scope. +Local Open Scope sets. +Import ListNotations. +Local Open Scope list. +Require Import String. +Local Open Scope string. +Import naive_C_Rules. +Local Open Scope sac. + +Module Aux. + +Lemma Zpow_add_1: forall (a b: Z), + a >= 0 -> b >= 0 -> + a ^ (b + 1) = a ^ b * a. +Proof. + intros. + rewrite (Z.pow_add_r a b 1); lia. +Qed. + +Lemma Z_of_nat_succ: forall (n: nat), + Z.of_nat (S n) = Z.of_nat n + 1. + +Lemma Zdiv_mod_pow: forall (n a b: Z), + a > 0 -> b >= 0 -> n >= 0 -> + (n / a) mod (a ^ b) = (n mod (a ^ (b + 1))) / a. +Proof. + intros. + pose proof (Z_div_mod_eq_full n (a ^ (b + 1))). + remember (n / (a ^ (b + 1))) as q eqn:Hq. + remember (n mod a ^ (b + 1)) as rem eqn:Hrem. + assert (n / a = a ^ b * q + rem / a). { + rewrite H2. + rewrite Zpow_add_1; try lia. + pose proof (Z_div_plus_full_l (a ^ b * q) a rem ltac:(lia)). + assert (a ^ b * q * a + rem = a ^ b * a * q + rem). { lia. } + rewrite H4 in H3. + tauto. + } + apply Znumtheory.Zdivide_mod_minus. + + pose proof (Z.mod_bound_pos n (a ^ (b + 1)) ltac:(lia) (Z.pow_pos_nonneg a (b + 1) ltac:(lia) ltac:(lia))). + rewrite <-Hrem in H4. + rewrite Zpow_add_1 in H4; try lia. + pose proof (Z.div_lt_upper_bound rem a (a ^ b) ltac:(lia) ltac:(lia)). + split; try lia. + apply (Z_div_pos rem a ltac:(lia) ltac:(lia)). + + unfold Z.divide. + exists q. + lia. +Qed. + +End Aux. \ No newline at end of file diff --git a/projects/lib/gmp_number.v b/projects/lib/gmp_number.v new file mode 100644 index 0000000..93bd34c --- /dev/null +++ b/projects/lib/gmp_number.v @@ -0,0 +1,289 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.Bool.Bool. +Require Import Coq.Lists.List. +Require Import Coq.Classes.RelationClasses. +Require Import Coq.Classes.Morphisms. +Require Import Coq.micromega.Psatz. +Require Import Permutation. +Require Import String. +From AUXLib Require Import int_auto Axioms Feq Idents List_lemma VMap. +Require Import SetsClass.SetsClass. Import SetsNotation. +From SimpleC.SL Require Import CommonAssertion Mem SeparationLogic IntLib. +Require Import Logic.LogicGenerator.demo932.Interface. +Local Open Scope Z_scope. +Local Open Scope sets. +Import ListNotations. +Local Open Scope list. +Require Import String. +Local Open Scope string. +Import naive_C_Rules. +Local Open Scope sac. + +Notation "'UINT_MOD'" := (4294967296). + +Module Aux. + +Lemma Z_of_nat_succ: forall (n: nat), + Z.of_nat (S n) = Z.of_nat n + 1. +Proof. lia. Qed. + +Lemma Zpow_add_1: forall (a b: Z), + a >= 0 -> b >= 0 -> + a ^ (b + 1) = a ^ b * a. +Proof. + intros. + rewrite (Z.pow_add_r a b 1); lia. +Qed. + +Lemma Zdiv_mod_pow: forall (n a b: Z), + a > 0 -> b >= 0 -> n >= 0 -> + (n / a) mod (a ^ b) = (n mod (a ^ (b + 1))) / a. +Proof. + intros. + pose proof (Z_div_mod_eq_full n (a ^ (b + 1))). + remember (n / (a ^ (b + 1))) as q eqn:Hq. + remember (n mod a ^ (b + 1)) as rem eqn:Hrem. + assert (n / a = a ^ b * q + rem / a). { + rewrite H2. + rewrite Zpow_add_1; try lia. + pose proof (Z_div_plus_full_l (a ^ b * q) a rem ltac:(lia)). + assert (a ^ b * q * a + rem = a ^ b * a * q + rem). { lia. } + rewrite H4 in H3. + tauto. + } + apply Znumtheory.Zdivide_mod_minus. + + pose proof (Z.mod_bound_pos n (a ^ (b + 1)) ltac:(lia) (Z.pow_pos_nonneg a (b + 1) ltac:(lia) ltac:(lia))). + rewrite <-Hrem in H4. + rewrite Zpow_add_1 in H4; try lia. + pose proof (Z.div_lt_upper_bound rem a (a ^ b) ltac:(lia) ltac:(lia)). + split; try lia. + apply (Z_div_pos rem a ltac:(lia) ltac:(lia)). + + unfold Z.divide. + exists q. + lia. +Qed. + +End Aux. + +Module Internal. + +Definition mpd_store_list (ptr: addr) (data: list Z) (cap: Z): Assertion := + [| Zlength data <= cap |] && + store_uint_array ptr (Zlength data) data && + store_undef_uint_array_rec ptr ((Zlength data) + 1) cap. + +Fixpoint list_store_Z (data: list Z) (n: Z): Assertion := + match data with + | nil => [| n = 0 |] + | a :: l0 => [| (n mod UINT_MOD) = a |] && list_store_Z l0 (n / UINT_MOD) + end. + +Definition mpd_store_Z (ptr: addr) (n: Z) (size: Z) (cap: Z): Assertion := + EX data, + mpd_store_list ptr data cap && list_store_Z data n && [| size = Zlength data |]. + +Fixpoint list_store_Z_pref (data: list Z) (n: Z) (len: nat): Assertion := + match len with + | O => [| n = 0 |] + | S len' => + EX a l0, + [| data = a :: l0 |] && [| (n mod UINT_MOD) = a |] && list_store_Z_pref l0 (n / UINT_MOD) len' + end. + +Definition mpd_store_Z_pref (ptr: addr) (n: Z) (size: Z) (cap: Z) (len: nat): Assertion := + EX data, + mpd_store_list ptr data cap && list_store_Z_pref data n len && [| size = Zlength data |]. + +Lemma list_store_Z_split: forall (data: list Z) (n: Z) (len: nat), + n >= 0 -> + Z.of_nat len < Zlength data -> + list_store_Z data n |-- + list_store_Z_pref data (n mod (UINT_MOD ^ Z.of_nat len)) len. +Proof. + intros. + revert n H data H0. + induction len. + + intros. + simpl. + entailer!. + apply Z.mod_1_r. + + intros. + assert (Zlength data >= 1); [ lia | ]. + destruct data; [ unfold Zlength, Zlength_aux in H1; lia | ]. + simpl. + Exists z data. + entailer!. + sep_apply IHlen; try tauto. + - pose proof (Aux.Zdiv_mod_pow n UINT_MOD (Z.of_nat len) ltac:(lia) ltac:(lia) ltac:(lia)). + rewrite H5. + pose proof (Aux.Z_of_nat_succ len). + rewrite <-H6. + reflexivity. + - pose proof (Aux.Z_of_nat_succ len). + pose proof (Zlength_cons z data). + lia. + - pose proof (Z.div_pos n UINT_MOD ltac:(lia) ltac:(lia)). + lia. + - rewrite <-H2. + pose proof (Znumtheory.Zmod_div_mod UINT_MOD (Z.pow_pos UINT_MOD (Pos.of_succ_nat len)) n ltac:(lia) ltac:(lia)). + rewrite H3; try tauto. + unfold Z.divide. + destruct len. + * exists 1. + simpl. + lia. + * exists (Z.pow_pos UINT_MOD (Pos.of_succ_nat len)). + assert (Pos.of_succ_nat (S len) = Pos.add (Pos.of_succ_nat len) xH). { lia. } + rewrite H4. + apply Zpower_pos_is_exp. +Qed. + +Lemma list_store_Z_pref_full: forall (data: list Z) (n: Z), + list_store_Z_pref data n (Z.to_nat (Zlength data)) --||-- list_store_Z data n. +Proof. + intros. + revert n. + induction data. + + intros. + simpl. + split; entailer!. + + intros. + pose proof (Zlength_cons a data). + rewrite H. + pose proof (Z2Nat.inj_succ (Zlength data) (Zlength_nonneg data)). + rewrite H0. + simpl. + split. + - Intros a0 l0. + injection H1; intros. + subst. + specialize (IHdata (n / UINT_MOD)). + destruct IHdata. + sep_apply H2. + entailer!. + - Exists a data. + entailer!. + specialize (IHdata (n / UINT_MOD)). + destruct IHdata. + sep_apply H3. + entailer!. +Qed. + +Lemma list_store_Z_pref_extend_data: forall (data: list Z) (a: Z) (n: Z) (len: nat), + list_store_Z_pref data n len |-- + list_store_Z_pref (data ++ (a :: nil)) n len. +Proof. + intros. + revert data n. + induction len. + + intros. + simpl. + entailer!. + + intros. + simpl. + Intros a0 l0. + Exists a0 (app l0 (cons a nil)). + entailer!. + subst. + reflexivity. +Qed. + +Search list. + +Lemma list_store_Z_pref_extend: forall (data: list Z) (a: Z) (n: Z) (len: nat), + n >= 0 -> + Zlength data = Z.of_nat len -> + list_store_Z_pref data (n mod (UINT_MOD ^ Z.of_nat len)) len && + [| a = (n / (UINT_MOD ^ Z.of_nat len)) mod UINT_MOD |] |-- + list_store_Z_pref (data ++ (cons a nil)) (n mod (UINT_MOD ^ (Z.of_nat len + 1))) (S len). +Proof. + intros. + entailer!. + simpl. + revert a data H0 H1. + induction len. + + intros. + Exists a nil. + simpl. + entailer!. + - intros. + unfold Z.pow_pos, Pos.iter; simpl. + apply Z.mod_div; lia. + - unfold Z.pow_pos, Pos.iter; simpl. + simpl in H1; rewrite Z.div_1_r in H1. + rewrite Z.mod_mod; lia. + - pose proof (Zlength_nil_inv data H0). + rewrite H2. + reflexivity. + + intros. + simpl. + Intros a0 l0. + Exists a0 (app l0 [a]). + assert (Zlength l0 = Z.of_nat len). { + rewrite H2 in H0. + rewrite Zlength_cons in H0. + lia. + } + specialize (IHlen ((n / UINT_MOD ^ (Z.of_nat len)) mod UINT_MOD) l0 H4 ltac:(lia)). + sep_apply IHlen. + Admitted. (* Unfinished. *) + +Lemma mpd_store_Z_split: forall (ptr: addr) (n: Z) (size: Z) (cap: Z) (len: nat), + n >= 0 -> + Z.of_nat len < size -> + mpd_store_Z ptr n size cap |-- + mpd_store_Z_pref ptr (n mod (UINT_MOD ^ Z.of_nat len)) size cap len. +Proof. + intros. + unfold mpd_store_Z, mpd_store_Z_pref. + Intros data. + Exists data. + unfold mpd_store_list. + Intros. + entailer!. + sep_apply (list_store_Z_split data n len). + + entailer!. + + lia. + + lia. +Qed. + +Lemma mpd_store_Z_pref_full: forall (ptr: addr) (n: Z) (size: Z) (cap: Z), + mpd_store_Z ptr n size cap --||-- mpd_store_Z_pref ptr n size cap (Z.to_nat size). +Proof. + intros. + unfold mpd_store_Z, mpd_store_Z_pref. + pose proof list_store_Z_pref_full. + split; Intros data; Exists data; entailer!; specialize (H data n); destruct H. + + sep_apply H1. + subst. + entailer!. + + subst. + sep_apply H. + entailer!. +Qed. + +End Internal. + +Record bigint_ent: Type := { + cap: Z; + data: list Z; + sign: Prop; +}. + +Definition store_bigint_ent (x: addr) (n: bigint_ent): Assertion := + EX size, + &(x # "__mpz_struct" ->ₛ "_mp_size") # Int |-> size && + ([| size < 0 |] && [| sign n |] && [| size = -Zlength (data n) |] || + [| size >= 0 |] && [| ~(sign n) |] && [| size = Zlength (data n) |]) ** + &(x # "__mpz_struct" ->ₛ "_mp_alloc") # Int |-> cap n ** + EX p, + &(x # "__mpz_struct" ->ₛ "_mp_d") # Ptr |-> p ** + Internal.mpd_store_list p (data n) (cap n). + +Definition bigint_ent_store_Z (n: bigint_ent) (x: Z): Assertion := + [| sign n |] && Internal.list_store_Z (data n) (-x) || + [| ~(sign n) |] && Internal.list_store_Z (data n) x. + +Definition store_Z (x: addr) (n: Z): Assertion := + EX ent, + store_bigint_ent x ent && bigint_ent_store_Z ent n. \ No newline at end of file diff --git a/projects/task1/mini-gmp.c b/projects/mini-gmp.c similarity index 100% rename from projects/task1/mini-gmp.c rename to projects/mini-gmp.c diff --git a/projects/task1/mini-gmp.h b/projects/mini-gmp.h similarity index 100% rename from projects/task1/mini-gmp.h rename to projects/mini-gmp.h diff --git a/projects/task2/cnf_trans.c b/projects/task2/cnf_trans.c deleted file mode 100755 index 609ba5e..0000000 --- a/projects/task2/cnf_trans.c +++ /dev/null @@ -1,225 +0,0 @@ -#include "cnf_trans.h" - -/* BEGIN Given Functions */ - -// 分配一个大小为size的全零的int数组 -int* malloc_int_array(int size); - -// 释放int数组 -void free_int_array(int* array); - -// 分配一个初始全零 cnf_list 结构体 -cnf_list* malloc_cnf_list(); - -// 释放 cnf_list 结构体 -void free_cnf_list(cnf_list* list); - -/* END Given Functions */ - - -//生成p3<->(p1 op p2)对应的cnf中的clause -//p3<->not p2 (op为 not时， 此时p1缺省为0) -void clause_gen(int p1, int p2, int p3, int op, PreData* data){ - int size = 3; - int *clause1 = malloc_int_array(size); - int *clause2 = malloc_int_array(size); - int *clause3 = malloc_int_array(size); - int *clause4 = malloc_int_array(size); - // 完成 SET_PROP: p3<->(p1 op p2) / p3<->not p2 - int cnt = 0; - switch (op) - { - case SMTPROP_OR: - { - // p3\/非p1 - clause1[0] = -p1; - clause1[1] = p3; - // p3\/非p2 - clause2[0] = -p2; - clause2[1] = p3; - if (p1 != p2) - { - // 非p3\/p1\/p2 - clause3[0] = p1; - clause3[1] = p2; - clause3[2] = -p3; - } - else - { - clause3[0] = p1; - clause3[1] = -p3; - } - cnt += 3; - break; - } - case SMTPROP_AND: - { - // 非p3\/p1 - clause1[0] = p1; - clause1[1] = -p3; - // 非p3\/p2 - clause2[0] = p2; - clause2[1] = -p3; - if (p1 != p2) - { - // p3\/非p1\/非p2 - clause3[0] = -p1; - clause3[1] = -p2; - clause3[2] = p3; - } - else - { - clause3[0] = -p1; - clause3[1] = p3; - } - cnt += 3; - break; - } - case SMTPROP_IMPLY: - { - if (p1 != p2) - { - // p3\/p1 - clause1[0] = p1; - clause1[1] = p3; - // p3\/非p2 - clause2[0] = -p2; - clause2[1] = p3; - // 非p3\/非p1\/p2 - clause3[0] = -p1; - clause3[1] = p2; - clause3[2] = -p3; - cnt += 3; - } - else - { - clause1[0] = p3; - cnt += 1; - } - break; - } - case SMTPROP_IFF: - { - if (p1 != p2) - { - // p3\/p1\/p2 - clause1[0] = p1; - clause1[1] = p2; - clause1[2] = p3; - // p3\/非p1\/非p2 - clause2[0] = -p1; - clause2[1] = -p2; - clause2[2] = p3; - // 非p3\/p1\/非p2 - clause3[0] = p1; - clause3[1] = -p2; - clause3[2] = -p3; - // 非p3\/非p1\/p2 - clause4[0] = -p1; - clause4[1] = p2; - clause4[2] = -p3; - cnt += 4; - } - else - { - clause1[0] = p3; - cnt += 1; - } - break; - } - case SMTPROP_NOT: - { - // p3\/p2 - clause1[0] = p2; - clause1[1] = p3; - // 非p3\/非p2 - clause2[0] = -p2; - clause2[1] = -p3; - cnt += 2; - break; - } - default: - { - //unreachable - } - } - cnf_list *list1 = malloc_cnf_list(); - cnf_list *list2 = malloc_cnf_list(); - cnf_list *list3 = malloc_cnf_list(); - cnf_list *list4 = malloc_cnf_list(); - list1->size = size; - list2->size = size; - list3->size = size; - list4->size = size; - list1->clause = clause1; - list2->clause = clause2; - list3->clause = clause3; - list4->clause = clause4; - if (cnt == 1) - { - list1->next = data->cnf_res; - data->cnf_res = list1; - data->clause_cnt += 1; - free_int_array(clause2); - free_int_array(clause3); - free_int_array(clause4); - free_cnf_list(list2); - free_cnf_list(list3); - free_cnf_list(list4); - } - else if (cnt == 2) - { - list1->next = list2; - list2->next = data->cnf_res; - data->cnf_res = list1; - data->clause_cnt += 2; - free_int_array(clause3); - free_int_array(clause4); - free_cnf_list(list3); - free_cnf_list(list4); - } - else if (cnt == 3) - { - list1->next = list2; - list2->next = list3; - list3->next = data->cnf_res; - data->cnf_res = list1; - data->clause_cnt += 3; - free_int_array(clause4); - free_cnf_list(list4); - } - else - { - list1->next = list2; - list2->next = list3; - list3->next = list4; - list4->next = data->cnf_res; - data->cnf_res = list1; - data->clause_cnt += 4; - } -} - -int prop2cnf(SmtProp* p, PreData* data){ - int res = 0; - switch(p->type){ - case SMTB_PROP: { - int p1 = prop2cnf(p->prop.Binary_prop.prop1, data); - int p2 = prop2cnf(p->prop.Binary_prop.prop2, data); - res = ++(data->prop_cnt); - clause_gen(p1, p2, res, p->prop.Binary_prop.op, data); - break; - } - case SMTU_PROP: { - int p1 = prop2cnf(p->prop.Unary_prop.prop1, data); - res = ++(data->prop_cnt); - clause_gen(0, p1, res, p->prop.Binary_prop.op, data); - break; - } - case SMT_PROPVAR: - res = p->prop.Propvar; - break; - default: - //unreachable - } - return res; -} diff --git a/projects/task2/cnf_trans.h b/projects/task2/cnf_trans.h deleted file mode 100755 index ea78a44..0000000 --- a/projects/task2/cnf_trans.h +++ /dev/null @@ -1,14 +0,0 @@ -#include "smt_lang.h" - -struct cnf_list{ - int size; //变量数量 - int* clause; //clause[i]存储命题变元的编号 - struct cnf_list* next; -}; -typedef struct cnf_list cnf_list; - -typedef struct{ - cnf_list* cnf_res; - int prop_cnt; //命题变元数量 - int clause_cnt; //转成cnf后clause的数量 -} PreData; diff --git a/projects/task2/smt_lang.h b/projects/task2/smt_lang.h deleted file mode 100755 index 894badb..0000000 --- a/projects/task2/smt_lang.h +++ /dev/null @@ -1,42 +0,0 @@ -enum SmtPropBop{ - SMTPROP_AND , - SMTPROP_OR, SMTPROP_IMPLY, SMTPROP_IFF -}; -typedef enum SmtPropBop SmtPropBop; - -enum SmtPropUop{ - SMTPROP_NOT = 4 -}; -typedef enum SmtPropUop SmtPropUop; - -enum SmtPropType { - SMTB_PROP = 5, - SMTU_PROP, - SMT_PROPVAR -}; -typedef enum SmtPropType SmtPropType; - -struct SmtProp { - SmtPropType type; - union { - struct { - SmtPropBop op; - struct SmtProp * prop1; - struct SmtProp * prop2; - } Binary_prop; - struct { - SmtPropUop op; - struct SmtProp *prop1; - } Unary_prop; - int Propvar; //表示将原子命题抽象成的命题变元对应的编号 - } prop; -}; - -typedef struct SmtProp SmtProp; - -struct SmtProplist { - SmtProp* prop; - struct SmtProplist* next; -}; - -typedef struct SmtProplist SmtProplist; diff --git a/projects/task3/alpha_equiv.c b/projects/task3/alpha_equiv.c deleted file mode 100755 index 3cf6bf1..0000000 --- a/projects/task3/alpha_equiv.c +++ /dev/null @@ -1,39 +0,0 @@ -#include "ast.h" - -bool alpha_equiv(term *t1, term *t2) -{ - if (t1 == (void*) 0 || t2 == (void*) 0) - return false; - if (t1->type != t2->type) - return false; - switch (t1->type){ - case Var: { - return strcmp(t1->content.Var, t2->content.Var) == 0; - } - case Const: { - if (t1->content.Const.type != t2->content.Const.type) - return false; - if (t1->content.Const.type == Num){ - return t1->content.Const.content == t2->content.Const.content; - } - return true; - } - case Apply: { - return alpha_equiv(t1->content.Apply.left, t2->content.Apply.left) && - alpha_equiv(t1->content.Apply.right, t2->content.Apply.right); - } - case Quant: { - if (t1->content.Quant.type != t2->content.Quant.type) - return false; - if (strcmp(t1->content.Quant.var, t2->content.Quant.var) == 0){ - return alpha_equiv(t1->content.Quant.body, t2->content.Quant.body); - } - else{ - term *t21 = subst_var(t1->content.Quant.var, t2->content.Quant.var, copy_term(t2->content.Quant.body)); - bool result = alpha_equiv(t1->content.Quant.body, t21); - free_term(t21); - return result; - } - } - } -} \ No newline at end of file diff --git a/projects/task3/ast.h b/projects/task3/ast.h deleted file mode 100755 index ac7d9cf..0000000 --- a/projects/task3/ast.h +++ /dev/null @@ -1,120 +0,0 @@ -typedef enum {false, true} bool; - -enum const_type -{ - Num = 0, - // oper - Add, - Mul, - // pred - Eq, - Le, - // connect - And, - Or, - Impl -}; -typedef enum const_type const_type; - -enum quant_type -{ - Forall, - Exists -}; -typedef enum quant_type quant_type; - -enum term_type -{ - Var, - Const, - Apply, - Quant -}; -typedef enum term_type term_type; - -struct term -{ - term_type type; - union { - char *Var; - struct - { - const_type type; - int content; - } Const; - struct - { - struct term *left; - struct term *right; - } Apply; - struct - { - quant_type type; - char *var; - struct term *body; - } Quant; - } content; -}; -typedef struct term term; - -struct term_list -{ - term *element; - struct term_list *next; -}; -typedef struct term_list term_list; - -typedef struct var_sub -{ - char *var; - term *sub_term; -} var_sub; - -typedef struct var_sub_list -{ - var_sub *cur; - struct var_sub_list *next; -} var_sub_list; - -typedef enum {bool_res, termlist} res_type; -typedef struct{ - res_type type; - union{ - bool ans; - term_list* list; - } d; -} solve_res; - -typedef struct{ - term *assum; - term *concl; -} ImplyProp; - -/* BEGIN Given Functions */ - -// malloc 函数，内存均初始为全0 -term_list *malloc_term_list(); -solve_res *malloc_solve_res(); - -// 构造函数 -ImplyProp *createImplyProp(term *t1, term *t2); - -// 深拷贝函数 -term *copy_term(term *t); -term_list *copy_term_list(term_list *list); - -// free 函数 -void free_str(char *s); -void free_imply_prop(ImplyProp *p); -void free_term(term *t); -void free_term_list(term_list *list); - -// string 相关函数 -char *strdup(const char *s); -int strcmp(const char *s1, const char *s2); - -/* END Given Functions */ - -term *subst_var(char *den, char *src, term *t); -term* subst_term(term* den, char* src, term* t); -bool alpha_equiv(term *t1, term *t2); diff --git a/projects/task3/subst.c b/projects/task3/subst.c deleted file mode 100755 index 88154b1..0000000 --- a/projects/task3/subst.c +++ /dev/null @@ -1,65 +0,0 @@ -#include "ast.h" - -term *subst_var(char *den, char *src, term *t) -{ - switch (t->type) - { - case Var: { - if (!strcmp(t->content.Var, src)) - { - free_str(t->content.Var); - t->content.Var = strdup(den); - } - break; - } - case Const:{ - break; - } - case Apply: { - t->content.Apply.left = subst_var(den, src, t->content.Apply.left); - t->content.Apply.right = subst_var(den, src, t->content.Apply.right); - break; - } - case Quant: { - if (strcmp(t->content.Quant.var, src)) - { - t->content.Quant.body = subst_var(den, src, t->content.Quant.body); - } - break; - } - default:{ - break; - } - } - return t; -} - -term* subst_term(term* den, char* src, term* t){ - switch(t->type){ - case Var:{ - if(!strcmp(t->content.Var, src)){ - free_term(t); - t = copy_term(den); - } - break; - } - case Const:{ - break; - } - case Apply:{ - t->content.Apply.left = subst_term(den, src, t->content.Apply.left); - t->content.Apply.right = subst_term(den, src, t->content.Apply.right); - break; - } - case Quant:{ - if(strcmp(t->content.Quant.var,src)){ - t->content.Quant.body = subst_term(den, src, t->content.Quant.body); - } - break; - } - default:{ - break; - } - } - return t; -} \ No newline at end of file diff --git a/projects/task3/thm_apply.c b/projects/task3/thm_apply.c deleted file mode 100755 index 5aa1589..0000000 --- a/projects/task3/thm_apply.c +++ /dev/null @@ -1,67 +0,0 @@ -#include "ast.h" - -term* sub_thm(term* thm, var_sub_list* list){ - if(list == (void*) 0) return copy_term(thm); - if(thm->type == Quant){ - term* den = list->cur->sub_term; - return sub_thm(subst_term(den, list->cur->var, thm->content.Quant.body), list->next); - } - else return (void*) 0; -} - -// apply (apply (impl) h1) (h2) -//不是imply形式时返回(void*) 0 -ImplyProp *separate_imply(term *t) -{ - if (t->type != Apply || t->content.Apply.left->type != Apply || - t->content.Apply.left->content.Apply.left->type != Const || - t->content.Apply.left->content.Apply.left->content.Const.type != Impl) - return (void*) 0; - else - return createImplyProp(t->content.Apply.left->content.Apply.right, t->content.Apply.right); -} - -//根据定理形式，匹配结论，得出要检验的前提 -term_list* check_list_gen(term* thm, term* target) { - if (thm == (void*) 0 || target == (void*) 0) { - return (void*) 0; - } - term_list* check_list = (void*) 0; - term_list** tail_ptr = &check_list; - while (thm != (void*) 0 && !alpha_equiv(thm, target)) { - ImplyProp* p = separate_imply(thm); - if (p == (void*) 0) { - free_term_list(check_list); - return (void*) 0; - } - // 添加新节点到链表 - term_list* new_node = malloc_term_list(); - new_node->element = p->assum; // 转移所有权 - new_node->next = (void*) 0; - - *tail_ptr = new_node; - tail_ptr = &(new_node->next); - thm = p->concl; - free_imply_prop(p); // 释放ImplyProp结构体（不释放其成员） - } - return check_list; -} - - -solve_res* thm_apply(term* thm, var_sub_list* list, term* goal){ - term* thm_ins = sub_thm(thm, list); - solve_res* res = malloc_solve_res(); - if(thm_ins == (void*) 0) { - res->type = bool_res; - res->d.ans = false; - } - else if(alpha_equiv(thm_ins, goal)){ - res->type = bool_res; - res->d.ans = true; - } - else{ - res->type = termlist; - res->d.list = check_list_gen(thm_ins, goal); - } - return res; -} \ No newline at end of file