发布时间 : 星期二 文章谓词逻辑归结原理源代码更新完毕开始阅读0e411767f5335a8102d2206a
#include
char var; char *s; }mgu;
void strreplace(char *string,char *str1,char *str2) {
char *p;
while(p=strstr(string,str1)) {
int i=strlen(string); int j=strlen(str2); *(string+i+j-1)='\\0';
for(int k=i-1;(string+k)!=p;k--) *(string+k+j-1)=*(string+k); for(i=0;i void sort(mgu *u,int count) { int j=count; int k=j; if(count==1)return; for(int i=1;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(int i=1;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<<\} class unifier { char *string; mgu unit[50]; int count; public: int num; unifier(); void input(); int differ(int n); int change(int i,int j,int n); void print(); ~unifier(){delete string;} }; unifier::unifier() { count=0; unit[0].s=null; } void unifier::input() { cout < string=new char[num*50]; cout<<\请注意:公式的输入不能出错!\ for(int j=1;j<=num;j++) { cout << \请输入第\个原子谓词公式(字符个数不超过50个)\ cin>>(string+(j-1)*50); } } int unifier::change(int i,int j,int n) { char temp[2][10]; temp[0][0]=string[i++]; temp[1][0]=string[j++]; if(string[i]!='(') temp[0][1]='\\0'; else { int k=1,flag=1; temp[0][k++]=string[i++]; while((flag!=0)&&k<10) { if(string[i]=='(') flag++; else if(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])) return 2; strreplace(string+n*50,temp[1],temp[0]); strreplace(string+(n+1)*50,temp[1],temp[0]); count++; int m=count; unit[m].var=temp[1][0]; char *p=new char[strlen(temp[0])+1]; unit[m].s=p; strcpy(p,temp[0]); } return 1; } int unifier::differ(int n) { int i=n*50,j=(n+1)*50; while((string[i]!='\\0')&&(string[j]!='\\0')&&(string[i]==string[j])) {i++;j++;} if(string[i]=='\\0'||string[j]=='\\0') return 1; int k; if(string[i+1]=='(') k=change(i,j,n); else if(string[j+1]=='(') k=change(j,i,n); else if(string[j]=='x'||string[j]=='y'||string[j]=='z'||string[j]=='u'|| string[j]=='v'||string[j]=='w') k=change(i,j,n); else k=change(j,i,n); if(k==2) return k; j=count; char c[2],*p; for(i=1;i c[0]=unit[j].var; c[1]='\\0'; if(!strstr(unit[i].s,c)) continue; p=new char[strlen(unit[j].s)+strlen(unit[i].s)+1]; strcpy(p,unit[i].s); strreplace(p,c,unit[j].s); delete unit[i].s; unit[i].s=p; } sort(unit,count); return 0; } void unifier::print() {