谓词逻辑归结原理源代码.doc

#include<iostream.h>
#include<string.h>
#include<stdio.h>
#definenull0
typedefstruct
{
charvar;
char*s;
}mgu;
voidstrreplace(char*string,char*str1,char*str2)
{
char*p;
while(p=strstr(string,str1))
{
inti=strlen(string);
intj=strlen(str2);
*(string+i+j-1)='\0';
for(intk=i-1;(string+k)!=p;k--)
*(string+k+j-1)=*(string+k);
for(i=0;i<strlen(str2);i++)
*(p++)=*(str2+i);
}
}
voidsort(mgu*u,intcount)
{
intj=count;
intk=j;
if(count==1)return;
for(inti=1;i<count;i++)
{
if(!((u+i)->s))
continue;
if((u+i)->var==(u+j)->var)
{
delete(u+j)->s;
(u+j)->s=null;
k--;
j=i;
}
if(((u+i)->s)&&((u+i)->var==*((u+i)->s)))
{
delete(u+i)->s;
(u+i)->s=null;
k--;
}
}
j=count;
if(k==j)return;
count=k;
for(inti=1;i<j&&k>0;i++)
{
if((u+i)->s)
continue;
while(!((u+j)->s))
j--;
(u+i)->var=(u+j)->var;
(u+i)->s=(u+j)->s;
(u+j)->s=null;
k--;
}
cout<<"gjvjkhllknkln";
}
classunifier
{
char*string;
mguunit[50];
intcount;

public:
intnum;

unifier();
voidinput();
intdiffer(intn);
intchange(inti,intj,intn);
voidprint();
~unifier(){deletestring;}

};
unifier::unifier()
{
count=0;
unit[0].s=null;
}
voidunifier::input()
{
cout<<endl<<"请输入原子谓词公式的个数(输入0退出)";
cin>>num;
string=newchar[num*50];
cout<<"请注意:公式的输入不能出错!"<<endl;
for(intj=1;j<=num;j++)
{
cout<<"请输入第"<<j<<"个原子谓词公式(字符个数不超过50个)"<<endl;
cin>>(string+(j-1)*50);
}
}
intunifier::change(inti,intj,intn)
{
chartemp[2][10];
temp[0][0]=string[i++];
temp[1][0]=string[j++];
if(string[i]!='(')
temp[0][1]='\0';
else
{
intk=1,flag=1;
temp[0][k++]=string[i++];
while((flag!=0)&&k<10)
{
if(string[i]=='(')
flag++;
elseif(string[i]==')')
flag--;
temp[0][k++]=string[i++];
}
temp[0][k]='\0';
}
temp[1][1]='\0';
if(strlen(temp[1])==1)
{
if(strstr(temp[0],temp[1]))
return2;
strreplace(string+n*50,temp[1],temp[0]);
strreplace(string+(n+1)*50,temp[1],temp[0]);
count++;
intm=count;
unit[m].var=temp[1][0];
char*p=newchar[strlen(temp[0])+1];
unit[m].s=p;
strcpy(p,temp[0]);
}
return1;
}
intunifier::differ(intn)
{
inti=n*50,j=(n+1)*50;
while((string[i]!='\0')&&(string[j]