#include<iostream.h>#include<string.h>#include<stdio.h>#define null 0typedef struct{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<strlen(str2);i++)*(p++)=*(str2+i);}}void sort(mgu *u,int count){int j=count;int k=j;if(count==1)return;for(int i=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(int i=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";}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 <<endl<< "请输入原子谓词公式的个数(输入0退出) "; cin>>num;string=new char[num*50];cout<<"请注意:公式的输入不能出错!"<<endl;for(int j=1;j<=num;j++){cout << "请输入第" << j << "个原子谓词公式(字符个数不超过50个)" <<endl; 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);elsek=change(j,i,n);if(k==2)return k;j=count;char c[2],*p;for(i=1;i<j;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(){cout <<"The MGU is ";for(int i=1;i<count+1;i++){cout <<(unit[i]).s<<"/"<<unit[i].var;if(i<count)cout<<",";}}int once(){unifier form;form.input();if(form.num<2){cout<<"The MGU is empty!"<<endl;return form.num;}int k=form.differ(0);if(k==1&&form.num==2){cout<<"The MGU is empty!"<<endl;return form.num;}if(k==2){cout<<"The MGU is not exist!"<<endl;return form.num;}else if(k==0&&form.num==2){while(k!=1){k=form.differ(0);if(k==2){cout<<"The MGU is not exist!"<<endl;return form.num;}}form.print();return form.num;}for(k=0;k<form.num-1;k++){if(form.differ(k)==2){cout<<"The MGU do not exist!"<<endl;return form.num;}}form.print(); }int main() {int i=once(); while(i!=0)i=once(); return 0;}。