谓词逻辑归结原理源代码

#include #include #include #define null 0 typedef 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

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;i0;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 <>num;

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() {

cout <<\ for(int i=1;i