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

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

《实验二王浩算法的实现.docx》由会员分享，可在线阅读，更多相关《实验二王浩算法的实现.docx（27页珍藏版）》请在冰点文库上搜索。

实验二王浩算法的实现

实验二王浩算法的实现

学号：

**********

班级：

计科二班

姓名：

***

一、实验内容：

实现命题逻辑框架内的王浩算法。

⑴将命题逻辑中的王浩算法推广至下述命题语言的情形之下:

ⅰ命题变量符号：

，

，

，

ⅱ逻辑连接符：

，

，

，

，

ⅲ间隔符：

，

⑵在上述⑴中所定义的命题语言中实现王浩算法。

二、实验目的

熟练掌握命题逻辑中的王浩算法。

三、实验原理

王浩算法实质上是一个反向推理的过程，它吧给定的公式化成合取范式，然后通过判断每个字句是否恒真的来判定给定的公式是否是恒真的。

设X1，…，Xm，Y1，…Yn是的公式，则相继式X1，…，Xm→Y1，…，Yn的直观含义可以理解为

（X1^…^Xm）→（Y1ˇ…ˇYn），

┌X1ˇ…ˇ┌XmˇY1ˇ…ˇYn。

四、实验源代码

#include

#include

#include

#defineMAX_L5

inti=0;

intstepcount=1;

enumtype{

and,or,detrusion,equal,level,variable

};

structnode{

char*s;

typekind;

intpolar;

node*next;

node*child;

intstart;

};

structstep{

step*child;

step*brother;

node*lhead;

node*rhead;

intcount;

charname[30];

};

intinite（char*s,node*head）{

intlen=strlen（s）;

intj=0,polar=1;

node*current=NULL;

node*last=NULL;

if（s==NULL）return0;

last=head;

while（i

if（s[i]=='|'）{

if（!

（s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a'）&&s[i+1]!

='1'&&s[i+1]!

='0'&&s[i+1]!

='（'&&s[i+1]!

='!

'||i==0）return0;

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;

}

else{

last->next=current;

}

last=current;

i++;

}

elseif（s[i]=='&'）{

if（!

（s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a'）&&s[i+1]!

='1'&&s[i+1]!

='0'&&s[i+1]!

='（'&&s[i+1]!

='!

'||i==0）return0;

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;

}

else{

last->next=current;

}

last=current;

i++;

}

elseif（s[i]=='!

'）{

if（!

（s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a'）&&s[i+1]!

='1'&&s[i+1]!

='0'&&s[i+1]!

='（'&&s[i+1]!

='!

'）return0;

polar=1-polar;

i++;

}

elseif（s[i]=='-'）{

if（s[i+1]!

='>'||（s[i+2]!

='!

'&&s[i+2]!

='（'&&!

（s[i+2]<='Z'&&s[i+2]>='A'||s[i+2]<='z'&&s[i+2]>='a'））||i==0）return0;

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;

}

else{

last->next=current;

}

last=current;

i=i+2;

}

elseif（s[i]=='<'）{

if（（s[i+1]!

='-'||s[i+2]!

='>'）||（s[i+3]!

='!

'&&s[i+3]!

='（'&&!

（s[i+3]<='Z'&&s[i+3]>='A'||s[i+3]<='z'&&s[i+3]>='a'）||i==0）&&s[i+3]!

='1'&&s[i+3]!

='0'）return0;

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;

}

else{

last->next=current;

}

last=current;

i=i+3;

}

elseif（s[i]<='Z'&&s[i]>='A'||s[i]<='z'&&s[i]>='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;

}

else{

last->next=current;

}

last=current;

j=0;

while（（s[i]<='Z'&&s[i]>='A'||s[i]<='z'&&s[i]>='a'）||（s[i]<='9'&&s[i]>='0'））{

（current->s）[j]=s[i];

i++;

j++;

}

if（s[i]!

='|'&&s[i]!

='&'&&s[i]!

='-'&&s[i]!

='<'&&s[i]!

='\0'&&s[i]!

='）'）return0;

（current->s）[j]='\0';

polar=1;

}

elseif（s[i]=='1'||s[i]=='0'）{

if（s[i+1]!

='<'&&s[i+1]!

='-'&&s[i+1]!

='&'&&s[i+1]!

='|'&&s[i+1]!

='）'&&s[i+1]!

='\0'）return0;

current=（node*）malloc（sizeof（node））;

current->kind=equal;

current->s=（char*）malloc（2*sizeof（char））;

（current->s）[0]=s[i];

（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;

}

else{

last->next=current;

}

last=current;

i++;

}

elseif（s[i]=='（'）{

if（!

（s[i+1]<='Z'&&s[i+1]>='A'||s[i+1]<='z'&&s[i+1]>='a'）&&s[i+1]!

='1'&&s[i+1]!

='0'&&s[i+1]!

='!

'&&s[i+1]!

='（'）return0;

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;

}

else{

last->next=current;

}

last=current;

i++;

polar=1;

if（!

inite（s,last））return0;

}

elseif（s[i]=='）'）{

if（s[i+1]!

='P'&&s[i+1]!

='1'&&s[i+1]!

='0'&&s[i+1]!

='-'&&s[i+1]!

='<'&&s[i+1]!

='&'&&s[i+1]!

='|'&&s[i+1]!

='\0'&&s[i+1]!

='）'）return0;

i++;

return1;

}

elsereturn0;

}

return1;

}

node*clone（node*parent）{

node*son=NULL;

if（parent==NULL）returnNULL;

son=（node*）malloc（sizeof（node））;

son->kind=parent->kind;

son->polar=parent->polar;

son->s=parent->s;

son->start=parent->start;

if（parent->next!

=NULL）{

son->next=clone（parent->next）;

}

else{

son->next=NULL;

}

if（parent->child!

=NULL）{

son->child=clone（parent->child）;

}

else{

son->child=NULL;

}

returnson;

}

voidremove（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）;

}

voidrestruct（node*head）{

node*current=NULL;

node*last=NULL;

node*newone=NULL,*newtwo=NULL,*newthree=NULL,*newfour=NULL,*newcurrent=NULL;

intorder=1;

while（order<=4）{

last=head;

current=last->child;

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;

}

else{

last->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;

}

else{

last=current;

current=current->next;

}

}

elseif（（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;

}

else{

last->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;

}

else{

last=current;

current=current->next;

}

}

elseif（（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;

}

else{

last->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;

}

else{

last=current;

current=current->next;

}

}

elseif（current->kind==level&&order==4）{

restruct（current）;

last=current;

current=current->next;

}

else{

last=current;

current=current->next;

}

}

order++;

}

}

voidshow（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->p