实验二 王浩算法的实现.docx

实验二 王浩算法的实现学号：2220103430班级：计科二班姓名：刘俊峰一、 实验内容：实现命题逻辑框架内的王浩算法。 将命题逻辑中的王浩算法推广至下述命题语言的情形之下: 命题变量符号：， 逻辑连接符：， 间隔符：， 在上述中所定义的命题语言中实现王浩算法。二、实验目的熟练掌握命题逻辑中的王浩算法。三、实验原理王浩算法实质上是一个反向推理的过程，它吧给定的公式化成合取范式，然后通过判断每个字句是否恒真的来判定给定的公式是否是恒真的。设X1，Xm，Y1，Yn是的公式，则相继式X1，Xm Y1，Yn的直观含义可以理解为（X1 Xm）（Y1Yn），X1XmY1Yn。四、实验源代码#include#include#include#define MAX_L 5int i=0;int stepcount=1;enum typeand,or,detrusion,equal,level,variable;struct nodechar *s;type kind;int polar;node *next;node *child;int start;struct stepstep *child;step *brother;node *lhead;node *rhead;int count;char name30;int inite(char *s,node *head)int len=strlen(s);int j=0,polar=1;node *current=NULL;node *last=NULL;if(s=NULL)return 0;last=head;while(ilen)if(si=|)if(!(si+1=A|si+1=a)&si+1!=1&si+1!=0&si+1!=(&si+1!=!|i=0)return 0;current=(node*)malloc(sizeof(node);current-kind=or;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i+;else if(si=&)if(!(si+1=A|si+1=a)&si+1!=1&si+1!=0&si+1!=(&si+1!=!|i=0)return 0;current=(node*)malloc(sizeof(node);current-kind=and;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i+;else if(si=!)if(!(si+1=A|si+1=a)&si+1!=1&si+1!=0&si+1!=(&si+1!=!)return 0;polar=1-polar;i+;else if(si=-)if(si+1!=|(si+2!=!&si+2!=(&!(si+2=A|si+2=a)|i=0)return 0;current=(node*)malloc(sizeof(node);current-kind=detrusion;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i=i+2;else if(si=)|(si+3!=!&si+3!=(&!(si+3=A|si+3=a)|i=0)&si+3!=1&si+3!=0)return 0;current=(node*)malloc(sizeof(node);current-kind=equal;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i=i+3;else if(si=A|si=a)current=(node*)malloc(sizeof(node);current-kind=variable;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;current-s=(char*)malloc(MAX_L*sizeof(char);if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;j=0;while(si=A|si=a)|(si=0)(current-s)j=si;i+;j+;if(si!=|&si!=&si!=-&si!=s)j=0;polar=1;else if(si=1|si=0)if(si+1!=kind=equal;current-s=(char*)malloc(2*sizeof(char);(current-s)0=si;(current-s)1=0;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i+;else if(si=()if(!(si+1=A|si+1=a)&si+1!=1&si+1!=0&si+1!=!&si+1!=()return 0;current=(node*)malloc(sizeof(node);current-kind=level;current-s=NULL;current-next=NULL;current-child=NULL;current-polar=polar;current-start=0;if(last-kind=level&last-child=NULL)last-child=current;elselast-next=current;last=current;i+;polar=1;if(!inite(s,last)return 0;else if(si=)if(si+1!=P&si+1!=1&si+1!=0&si+1!=-&si+1!=kind=parent-kind;son-polar=parent-polar;son-s=parent-s;son-start=parent-start;if(parent-next!=NULL)son-next=clone(parent-next);elseson-next=NULL;if(parent-child!=NULL)son-child=clone(parent-child);elseson-child=NULL;return son;void remove(node *head)node *current=NULL;current=head;if(current=NULL)return;if(current-kind=level¤t-child-kind=variable¤t-child-next=NULL)current-polar=(current-child-polar=current-polar);current-child-polar=1;while(current-kind=level¤t-child-kind=level¤t-child-next=NULL)current-polar=(current-polar=current-child-polar);current-child=current-child-child;if(current-next!=NULL)remove(current-next);if(current-child!=NULL)remove(current-child);void restruct(node* head)node *current=NULL;node *last=NULL;node *newone=NULL,*newtwo=NULL,*newthree=NULL,*newfour=NULL,*newcurrent=NULL;int order=1;while(orderchild;while(current!=NULL)if(current-kind=variable|current-kind=level)&order=1)if(current-next!=NULL¤t-next-kind=and)newone=(node*)malloc(sizeof(node);newone-child=NULL;newone-kind=level;newone-next=NULL;newone-polar=0;newone-s=NULL;newone-start=0;if(last-kind=level)last-child=newone;elselast-next=newone;newone-next=current-next-next-next;newone-child=current;current-next-next-polar=1-current-next-next-polar;current-next-kind=detrusion;current-next-next-next=NULL;current=newone;elselast=current;current=current-next;else if(current-kind=variable|current-kind=level)&order=2)if(current-next!=NULL¤t-next-kind=or) newone=(node*)malloc(sizeof(node);newone-child=NULL;newone-kind=level;newone-next=NULL;newone-polar=1;newone-s=NULL;newone-start=0;if(last-kind=level)last-child=newone;elselast-next=newone;newone-next=current-next-next-next;newone-child=current;current-polar=1-current-polar;current-next-kind=detrusion;current-next-next-next=NULL;current=newone;elselast=current;current=current-next;else if(current-kind=variable|current-kind=level)&order=3)if(current-next!=NULL¤t-next-kind=equal)newone=(node*)malloc(sizeof(node);newone-child=NULL;newone-kind=level;newone-next=NULL;newone-polar=0;newone-s=NULL;newone-start=0;newtwo=(node*)malloc(sizeof(node);newtwo-child=NULL;newtwo-kind=level;newtwo-next=NULL;newtwo-polar=1;newtwo-s=NULL;newtwo-start=0;newthree=(node*)malloc(sizeof(node);newthree-child=NULL;newthree-kind=detrusion;newthree-next=NULL;newthree-polar=1;newthree-s=NULL;newthree-start=0;newfour=(node*)malloc(sizeof(node);newfour-child=NULL;newfour-kind=level;newfour-next=NULL;newfour-polar=0;newfour-s=NULL;newfour-start=0;if(last-kind=level)last-child=newone;elselast-next=newone;newone-next=current-next-next-next;newone-child=newtwo;current-next-kind=detrusion;newtwo-child=current;current-next-next-next=NULL;newtwo-next=newthree;newthree-next=newfour;newfour-next=NULL;newcurrent=clone(current);newcurrent-next-kind=detrusion;newfour-child=newcurrent-next-next;newcurrent-next-next-next=newcurrent-next;newcurrent-next-next=newcurrent;newcurrent-next=NULL;current=newone;elselast=current;current=current-next;else if(current-kind=level&order=4)restruct(current);last=current;current=current-next;elselast=current;current=current-next;order+;void show(node *head)node *current=NULL;current=head;while(current!=NULL)if(current-kind=level)if(current-polar=0)printf(!);if(current-start!=1|(current-polar=0¤t-child-next!=NULL)printf();show(current-child);if(current-start!=1|(current-polar=0¤t-child-next!=NULL)printf();current=current-next;if(current!=NULL¤t-start=1)putchar(,);else if(current-kind=and)printf(&);current=current-next;else if(current-kind=or)printf(|);current=current-next;else if(current-kind=detrusion)printf(-);current=current-next;else if(current-kind=equal)printf();current=current-next;else if(current-kind=variable)if(current-polar=0)printf(!);printf(%s,current-s);current=current-next;return;int searching(step *one)node *current=NULL;node *last=NULL;node *newlev=NULL;node *ncurrent=NULL;node *nlast=NULL;step *nextone=NULL;step *nexttwo=NULL;int key=0;int mark=0;int re1=1;int re2=1;nextone=(step*)malloc(sizeof(step);nextone-brother=NULL;nextone-child=NULL;nextone-lhead=NULL;nextone-rhead=clone(one-rhead);nextone-lhead=clone(one-lhead);strcpy(nextone-name,);one-child=nextone; current=nextone-rhead;last=current;while(current!=NULL)if(current-polar=0)if(current=nextone-rhead)nextone-rhead=current-next;else last-next=current-next;current-next=NULL;remove(current);current-next=nextone-lhead;nextone-lhead=current;current-polar=1-current-polar;current-start=1;current=last-next;strcpy(one-name,根据规则1);mark=1;key=1;break;else if(current-child-next!=NULL¤t-child-next-kind=detrusion)nlast=current-child;ncurrent=current-child-next;while(ncurrent-next-next!=NULL&ncurrent-next-next-kind=detrusion)nlast=ncurrent-next;ncurrent=ncurrent-next-next;current-polar=1-current-polar;newlev=(node*)malloc(sizeof(node);newlev-child=ncurrent-next;newlev-kind=level;newlev-polar=1;newlev-next=NULL;newlev-start=1;nlast-next=NULL;remove(newlev);newlev-next=current-next;current-next=NULL;remove(current);current-next=newlev;strcpy(one-name,根据规则4);mark=1;key=1;break;elselast=current;current=current-next;current=nextone-lhead;last=current;while(current!=NULL&key!=1)if(current-polar=0)if(current=nextone-lhead)nextone-lhead=current-next;else last-next=current-next;current-next=NULL;remove(current);current-next=nextone-rhead;nextone-rhead=current;current-polar=1-current-polar;current-start=1;current=last-next;strcpy(one-name,根据规则2);mark=1;key=1;break;else if(current-child-next!=NULL¤t-child-next-kind=detrusion)nexttwo=(step*)malloc(sizeof(step);nexttwo-brother=NULL;nexttwo-child=NULL;nexttwo-lhead=NULL;nexttwo-rhead=clone(nextone-rhead);nexttwo-lhead=clone(nextone-lhead);strcpy(nexttwo-name,);nlast=current-child;ncurrent=current-child-next;while(ncurrent-next-next!=NULL&ncurrent-next-next-kind=detrusion)nlast=ncurrent-next;ncurrent=ncurrent-next-next;current-polar=1-current-polar;current-start=1;nlast-next=NULL;remove(current);current=nexttwo-lhead;last=current;while(current-child-next=NULL|current-child-next-kind!=detrusion)last=current;current=current-next;nlast=current-child;ncurrent=current-child-next;while(ncurrent-next-next!=NULL&ncurrent-next-next-kind=detrusion)nlast=ncurrent-next;ncurrent=ncurrent-next-next;newlev=(node*)malloc(sizeof(node);newlev-child=ncurrent-next;newlev-kind=level;newlev-polar=1;newlev-next=NULL;newlev-start=1;nlast-next=NULL;if(current=nexttwo-lhead)newlev-next=current-next;nexttwo-lhead=newlev;elsenewlev-next=current-next;last-next=newlev;remove(newlev);nextone-brother=nexttwo;strcpy(one-name,根据规则3);mark=1;key=1;break;elselast=current;current=current-next;if(mark=0)one-child=NULL;current=one-lhead;ncurrent=one-rhead;while(current!=NULL)ncurrent=one-rhead;while(ncurrent!=NULL)if(!strcmp(current-child-s,ncurrent-child-s)break;ncurrent=ncurrent-next;if(ncurrent!=NULL)break;current=current-next;if(current=NULL)return 0;elsereturn 1;re1=searching(nextone);if(nextone-brother!=NULL)re2=searching(nextone-brother);if(re1&re2)return 1;elsereturn 0;void output(step *one)if(one-child!=NULL)output(one-child);if(o