From 940b85ac80d62f0f84e02b123a97a550782ea074 Mon Sep 17 00:00:00 2001 From: xiaoh105 Date: Wed, 21 May 2025 16:56:46 +0800 Subject: [PATCH] initial commit --- .gitignore | 31 ++++ Makefile | 76 ++++++++++ README.md | 3 + projects/task1/mini-gmp.c | 275 +++++++++++++++++++++++++++++++++++ projects/task1/mini-gmp.h | 66 +++++++++ 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 +++++++++ 12 files changed, 1023 insertions(+) create mode 100755 .gitignore create mode 100755 Makefile create mode 100755 README.md create mode 100755 projects/task1/mini-gmp.c create mode 100755 projects/task1/mini-gmp.h create mode 100755 projects/task2/cnf_trans.c create mode 100755 projects/task2/cnf_trans.h create mode 100755 projects/task2/smt_lang.h create mode 100755 projects/task3/alpha_equiv.c create mode 100755 projects/task3/ast.h create mode 100755 projects/task3/subst.c create mode 100755 projects/task3/thm_apply.c diff --git a/.gitignore b/.gitignore new file mode 100755 index 0000000..17c9381 --- /dev/null +++ b/.gitignore @@ -0,0 +1,31 @@ +# config file +CONFIGURE +SUB_CONFIGURE + +# Object files, in general +*.glob +*.vo +*.vo[ks] +.*.aux + +# Generated files +.depend + +# Generated by MacOS +.DS_Store + +# Coq caches +.lia.cache +.nia.cache +.nra.cache +.csdp.cache + +assignments +compcert_lib +monadlib +pv +qcp +qualifiedcprogramming +sets +.gitmodules +_CoqProject \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100755 index 0000000..fec44ab --- /dev/null +++ b/Makefile @@ -0,0 +1,76 @@ +CURRENT_DIR=. +SETS_DIR = sets +COMPCERT_DIR = compcert_lib +PV_DIR = pv +COQBIN= + +-include CONFIGURE + +COQC=$(COQBIN)coqc +COQDEP=$(COQBIN)coqdep + +PV_FLAG = -R $(PV_DIR) PV -R $(SETS_DIR) SetsClass -R $(COMPCERT_DIR) compcert.lib + +SETS_FLAG = -R $(SETS_DIR) SetsClass + +COMPCERT_FLAG = -R $(COMPCERT_DIR) compcert.lib + +DEP_FLAG = -R $(PV_DIR) PV -R $(SETS_DIR) SetsClass -R $(COMPCERT_DIR) compcert.lib + +SETS_FILE_NAMES = \ + SetsClass.v SetsDomain.v SetElement.v RelsDomain.v SetElementProperties.v SetProd.v SetsClass_AxiomFree.v SetsDomain_Classic.v + +SETS_FILES=$(SETS_FILE_NAMES:%.v=$(SETS_DIR)/%.v) + +COMPCERT_FILE_NAMES = \ + Coqlib.v Integers.v Zbits.v + +COMPCERT_FILES=$(COMPCERT_FILE_NAMES:%.v=$(COMPCERT_DIR)/%.v) + +PV_FILE_NAMES = \ + Intro.v SimpleProofsAndDefs.v InductiveType.v \ + Syntax.v RecurProp.v ExprIntDenotation.v ExprBoolDenotation.v BuiltInNat.v \ + Logic.v RelsAsDenotations.v FixedPoint.v \ + HoareLogic.v Monad.v BuiltInList.v + +PV_FILES=$(PV_FILE_NAMES:%.v=$(PV_DIR)/%.v) + +FILES = $(PV_FILES) \ + $(SETS_FILES) \ + $(COMPCERT_FILES) + +$(SETS_FILES:%.v=%.vo): %.vo: %.v + @echo COQC $< + @$(COQC) $(SETS_FLAG) $< + +$(COMPCERT_FILES:%.v=%.vo): %.vo: %.v + @echo COQC $< + @$(COQC) $(COMPCERT_FLAG) $< + +$(PV_FILES:%.v=%.vo): %.vo: %.v + @echo COQC $( _CoqProject + +depend: $(FILES) + $(COQDEP) $(DEP_FLAG) $(FILES) > .depend + +.depend: $(FILES) + @$(COQDEP) $(DEP_FLAG) $(FILES) > .depend + +clean: + @rm -f *.glob */*.glob + @rm -f *.vo */*.vo + @rm -f *.vok */*.vok + @rm -f *.vos */*.vos + @rm -f .*.aux */.*.aux + @rm -f .depend + +.PHONY: clean depend +.DEFAULT_GOAL := all + +-include .depend diff --git a/README.md b/README.md new file mode 100755 index 0000000..e5903ba --- /dev/null +++ b/README.md @@ -0,0 +1,3 @@ +# README + +小组作业 minigmp. \ No newline at end of file diff --git a/projects/task1/mini-gmp.c b/projects/task1/mini-gmp.c new file mode 100755 index 0000000..1d03734 --- /dev/null +++ b/projects/task1/mini-gmp.c @@ -0,0 +1,275 @@ +#include "mini-gmp.h" + +mp_size_t gmp_abs(mp_size_t x) { + return x >= 0 ? x : -x; +} + +mp_size_t gmp_max(mp_size_t a, mp_size_t b) { + return a > b ? a : b; +} + +int gmp_cmp(mp_size_t a, mp_size_t b) { + return (a > b) - (a < b); +} + +/* MPN interface */ + +/* 从 低地址向高地址 顺序复制 */ +void +mpn_copyi (mp_ptr d, mp_srcptr s, mp_size_t n) +{ + mp_size_t i; + for (i = 0; i < n; i++) + d[i] = s[i]; +} + +/* 大于返回1，小于返回-1，等于返回0 */ +int +mpn_cmp (mp_srcptr ap, mp_srcptr bp, mp_size_t n) +{ + while (--n >= 0) + { + if (ap[n] != bp[n]) + return ap[n] > bp[n] ? 1 : -1; + } + return 0; +} + +/*处理位数不同的情况*/ +static int +mpn_cmp4 (mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +{ + if (an != bn) + return an < bn ? -1 : 1; + else + return mpn_cmp (ap, bp, an); +} + +/*返回非0的位数*/ +static mp_size_t +mpn_normalized_size (mp_srcptr xp, mp_size_t n) +{ + while (n > 0 && xp[n-1] == 0) + --n; + return n; +} + +/* 多精度数ap 加上单精度数b，返回最后产生的进位 */ +mp_limb_t +mpn_add_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) +{ + mp_size_t i; + //assert (n > 0); + i = 0; + do + { + mp_limb_t r = ap[i] + b; + /* Carry out */ + b = (r < b); + rp[i] = r; + } + while (++i < n); + + return b; +} + +/* 位数相同的多精度数ap 加上多精度数bp，返回最后产生的进位 */ +mp_limb_t +mpn_add_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) +{ + mp_size_t i; + mp_limb_t cy; + + for (i = 0, cy = 0; i < n; i++) + { + mp_limb_t a, b, r; + a = ap[i]; b = bp[i]; + r = a + cy; + cy = (r < cy); + r += b; + cy += (r < b); + rp[i] = r; + } + return cy; +} + +/*不同位数的多精度数相加，返回最后的进位*/ +mp_limb_t +mpn_add (mp_ptr rp, mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +{ + mp_limb_t cy; + //assert (an >= bn); + cy = mpn_add_n (rp, ap, bp, bn); + if (an > bn) + cy = mpn_add_1 (rp + bn, ap + bn, an - bn, cy); + return cy; +} + +mp_limb_t +mpn_sub_1 (mp_ptr rp, mp_srcptr ap, mp_size_t n, mp_limb_t b) +{ + mp_size_t i; + //assert (n > 0); + i = 0; + do + { + mp_limb_t a = ap[i]; + /* Carry out */ + mp_limb_t cy = a < b; + rp[i] = a - b; + b = cy; + } + while (++i < n); + + return b; +} + +mp_limb_t +mpn_sub_n (mp_ptr rp, mp_srcptr ap, mp_srcptr bp, mp_size_t n) +{ + mp_size_t i; + mp_limb_t cy; + + for (i = 0, cy = 0; i < n; i++) + { + mp_limb_t a, b; + a = ap[i]; b = bp[i]; + b += cy; + cy = (b < cy); + cy += (a < b); + rp[i] = a - b; + } + return cy; +} + +mp_limb_t +mpn_sub (mp_ptr rp, mp_srcptr ap, mp_size_t an, mp_srcptr bp, mp_size_t bn) +{ + mp_limb_t cy; + //assert (an >= bn); + cy = mpn_sub_n (rp, ap, bp, bn); + if (an > bn) + cy = mpn_sub_1 (rp + bn, ap + bn, an - bn, cy); + return cy; +} + +/* MPZ interface */ + +void +mpz_clear (mpz_t r) +{ + if (r->_mp_alloc) + gmp_free_limbs (r->_mp_d, r->_mp_alloc); +} + +static mp_ptr +mpz_realloc (mpz_t r, mp_size_t size) +{ + size = gmp_max (size, 1); + + if (r->_mp_alloc) + r->_mp_d = gmp_realloc_limbs (r->_mp_d, r->_mp_alloc, size); + else + r->_mp_d = gmp_alloc_limbs (size); + r->_mp_alloc = size; + + if (gmp_abs (r->_mp_size) > size) + r->_mp_size = 0; + + return r->_mp_d; +} + +/* Realloc for an mpz_t WHAT if it has less than NEEDED limbs. */ +mp_ptr mrz_realloc_if(mpz_t z,mp_size_t n) { + return n > z->_mp_alloc ? mpz_realloc(z, n) : z->_mp_d; +} + +/* MPZ comparisons and the like. */ +int +mpz_sgn (const mpz_t u) +{ + return gmp_cmp (u->_mp_size, 0); +} + +void +mpz_swap (mpz_t u, mpz_t v) +{ + mp_size_t_swap (u->_mp_alloc, v->_mp_alloc); + mp_ptr_swap(u->_mp_d, v->_mp_d); + mp_size_t_swap (u->_mp_size, v->_mp_size); +} + +/* MPZ addition and subtraction */ + +static mp_size_t +mpz_abs_add (mpz_t r, const mpz_t a, const mpz_t b) +{ + mp_size_t an = gmp_abs (a->_mp_size); + mp_size_t bn = gmp_abs (b->_mp_size); + mp_ptr rp; + mp_limb_t cy; + + if (an < bn) + { + mpz_srcptr_swap (a, b); + mp_size_t_swap (an, bn); + } + + rp = mrz_realloc_if (r, an + 1); + cy = mpn_add (rp, a->_mp_d, an, b->_mp_d, bn); + + rp[an] = cy; + + return an + cy; +} + +static mp_size_t +mpz_abs_sub (mpz_t r, const mpz_t a, const mpz_t b) +{ + mp_size_t an = gmp_abs (a->_mp_size); + mp_size_t bn = gmp_abs (b->_mp_size); + int cmp; + mp_ptr rp; + + cmp = mpn_cmp4 (a->_mp_d, an, b->_mp_d, bn); + if (cmp > 0) + { + rp = mrz_realloc_if (r, an); + mpn_sub (rp, a->_mp_d, an, b->_mp_d, bn); + return mpn_normalized_size (rp, an); + } + else if (cmp < 0) + { + rp = mrz_realloc_if (r, bn); + mpn_sub (rp, b->_mp_d, bn, a->_mp_d, an); + return -mpn_normalized_size (rp, bn); + } + else + return 0; +} + +void +mpz_add (mpz_t r, const mpz_t a, const mpz_t b) +{ + mp_size_t rn; + + if ( (a->_mp_size ^ b->_mp_size) >= 0) + rn = mpz_abs_add (r, a, b); + else + rn = mpz_abs_sub (r, a, b); + + r->_mp_size = a->_mp_size >= 0 ? rn : - rn; +} + +void +mpz_sub (mpz_t r, const mpz_t a, const mpz_t b) +{ + mp_size_t rn; + + if ( (a->_mp_size ^ b->_mp_size) >= 0) + rn = mpz_abs_sub (r, a, b); + else + rn = mpz_abs_add (r, a, b); + + r->_mp_size = a->_mp_size >= 0 ? rn : - rn; +} diff --git a/projects/task1/mini-gmp.h b/projects/task1/mini-gmp.h new file mode 100755 index 0000000..ba16619 --- /dev/null +++ b/projects/task1/mini-gmp.h @@ -0,0 +1,66 @@ +typedef unsigned long mp_limb_t; +typedef long mp_size_t; +typedef unsigned long mp_bitcnt_t; + +typedef mp_limb_t *mp_ptr; +typedef const mp_limb_t *mp_srcptr; + +typedef struct +{ + int _mp_alloc; /* Number of *limbs* allocated and pointed + to by the _mp_d field. */ + int _mp_size; /* abs(_mp_size) is the number of limbs the + last field points to. If _mp_size is + negative this is a negative number. */ + mp_limb_t *_mp_d; /* Pointer to the limbs. */ +} __mpz_struct; + +/* mpz_t is an array type that contains a single element of __mpz_struct, acting as a reference. */ +typedef __mpz_struct mpz_t[1]; +typedef __mpz_struct *mpz_ptr; +typedef const __mpz_struct *mpz_srcptr; + +/* BEGIN Given Functions */ + +/* Swap functions. */ +void mp_size_t_swap(mp_size_t x, mp_size_t y); + +void mp_ptr_swap(mp_ptr x, mp_ptr y); + +void mpz_srcptr_swap(mpz_srcptr x, mpz_srcptr y); + +/* Memory allocation functions. */ +static mp_ptr +gmp_alloc_limbs (mp_size_t size); + +static mp_ptr +gmp_realloc_limbs (mp_ptr old, mp_size_t old_size, mp_size_t size); + +static void +gmp_free_limbs (mp_ptr old, mp_size_t size); + +/* END Given Functions */ + +void mpn_copyi (mp_ptr, mp_srcptr, mp_size_t); + +int mpn_cmp (mp_srcptr, mp_srcptr, mp_size_t); + +mp_limb_t mpn_add_1 (mp_ptr, mp_srcptr, mp_size_t, mp_limb_t); +mp_limb_t mpn_add_n (mp_ptr, mp_srcptr, mp_srcptr, mp_size_t); +mp_limb_t mpn_add (mp_ptr, mp_srcptr, mp_size_t, mp_srcptr, mp_size_t); + +mp_limb_t mpn_sub_1 (mp_ptr, mp_srcptr, mp_size_t, mp_limb_t); +mp_limb_t mpn_sub_n (mp_ptr, mp_srcptr, mp_srcptr, mp_size_t); +mp_limb_t mpn_sub (mp_ptr, mp_srcptr, mp_size_t, mp_srcptr, mp_size_t); + +void mpz_clear (mpz_t); + +int mpz_sgn (const mpz_t); + +void mpz_neg (mpz_t, const mpz_t); +void mpz_swap (mpz_t, mpz_t); + +void mpz_add (mpz_t, const mpz_t, const mpz_t); +void mpz_sub (mpz_t, const mpz_t, const mpz_t); + +void mpz_set (mpz_t, const mpz_t); diff --git a/projects/task2/cnf_trans.c b/projects/task2/cnf_trans.c new file mode 100755 index 0000000..609ba5e --- /dev/null +++ b/projects/task2/cnf_trans.c @@ -0,0 +1,225 @@ +#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 new file mode 100755 index 0000000..ea78a44 --- /dev/null +++ b/projects/task2/cnf_trans.h @@ -0,0 +1,14 @@ +#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 new file mode 100755 index 0000000..894badb --- /dev/null +++ b/projects/task2/smt_lang.h @@ -0,0 +1,42 @@ +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 new file mode 100755 index 0000000..3cf6bf1 --- /dev/null +++ b/projects/task3/alpha_equiv.c @@ -0,0 +1,39 @@ +#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 new file mode 100755 index 0000000..ac7d9cf --- /dev/null +++ b/projects/task3/ast.h @@ -0,0 +1,120 @@ +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 new file mode 100755 index 0000000..88154b1 --- /dev/null +++ b/projects/task3/subst.c @@ -0,0 +1,65 @@ +#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 new file mode 100755 index 0000000..5aa1589 --- /dev/null +++ b/projects/task3/thm_apply.c @@ -0,0 +1,67 @@ +#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