/*
最一般合一(mgu)算法實現
*/
#include <iostream>
#include <string>
#include <vector>
using namespace std;
struct transform //一組置換
{
string t_f1;
string t_f2;
};
//函數聲明
bool same(const string f1,const string f2) ;
transform dif(const string f1,const string f2);
string change(string f,transform q);
string change2(string f,transform q);
bool syncretism(const string f1,const string f2, vector<transform> & );
int legal(transform &);
bool var(const string s);
string varData(string s);
int main()
{
cout<<"const:capital\t"<<"varible:lowercase."<<endl;
//輸入兩個謂詞公式
string f1,f2;
cout<<"intput F1:";
cin>>f1;
cout<<"intput F2:";
cin>>f2;
vector <transform> mgu;
if(syncretism(f1,f2,mgu))//存在最一般合一，並輸出結果
{
cout<<"mgu={ ";
int i=0;
for(i=0;i<mgu.size()-1;i++)
cout<<mgu[i].t_f1<<"/"<<mgu[i].t_f2<<", ";
cout<<mgu[i].t_f1<<"/"<<mgu[i].t_f2<<" }"<<endl;
}
else //不存在最一般合一
{
cout<<"cannot be syncretized"<<endl;
}
return 0;
}
bool syncretism (const string tf1,const string tf2,vector<transform> &mgu)//合一方法，判斷是否可進行合一
{
string f1=tf1, f2=tf2;
while(!same(f1,f2))//f1與f2中的符號不完全相同時才進入while循環
{
transform t=dif(f1,f2);//得到f1和f2的一個差異集，並把它賦給t
int flag=legal(t);
if(flag==0)
return false;
else
{
mgu.push_back(t);
f1=change(f1,mgu.back());
f2=change(f2,mgu.back());
cout<<"after change:"<<endl;
cout<<"f1:"<<f1<<endl;
cout<<"f2:"<<f2<<endl;
if(same(f1,f2)) break;//f1和f2相同時就停止循環
}
}
return true;
}
bool same(const string f1, const string f2) //判斷兩個謂詞f1和f2是否相同
{
if(f1.length()==f2.length())
{
int i=0;
while(i<f1.length()&&f1.at(i)==f2.at(i))
i++;
if(i==f1.length())
return true;
else
{
return false;
}
}
else return false;
}
transform dif(const string f1,const string f2)//求解f1和f2的差異集
{
int i=0;
transform t;
while(f1.at(i)==f2.at(i))//第i個相等時就轉向比較i+1，直到遇到不相等時就跳出while循環
i++;
int j1=i;
while(j1<f1.length()-1&&f1.at(j1)!=',')//從不相等的部分開始，直到遇到‘，’或到達結尾時跳出while循環
j1++;
if(j1-i==0) return t;
t.t_f1=f1.substr(i,j1-i);//將f1中的不相同的項截取出來放入變量t.t_f1中
int j2=i;
while(j2<f2.length()-1&&f2.at(j2)!=',')
j2++;
if(j2-i==0) return t;
t.t_f2=f2.substr(i,j2-i);//將f2中的不相同的項截取出來放入變量t.t_f2中
while(t.t_f1[j1-i-1]==t.t_f2[j2-i-1])//去除相同的部分
{
t.t_f1.erase(j1-1-i);
t.t_f2.erase(j2-i-1);
j1--;
j2--;
}
return t;
}
int legal(transform &t)//判斷置換t是否合法
{
if(t.t_f1.length()==0||t.t_f2.length()==0)
return 0;
if(var(t.t_f2))
{
if(var(t.t_f1)&&(varData(t.t_f1)==varData(t.t_f2)))//不能代換合一
return 0;
else
return 2;
}
if(!var(t.t_f1))//若t_f1和t_f2都不是變量，也不能合一
return 0;
string temp;
temp=t.t_f1;
t.t_f1=t.t_f2;
t.t_f2=temp;//在t_f1是變量而t_f2不是變量的情況下，交換t_f1和t_f2
return 1;
}
string varData(string s)//該函數是剝去外層括號
{
if(s.length()==1||s.length()==0)
return s;
if(s.length()>1)
{
int i=0;
while(i<s.length()&&s.at(i)!='(')
i++;
int j=i;
while(j<s.length()&&s.at(j)!=')')
j++;
string ss=s.substr(i+1,j-i-1);
return varData(ss);
}
else
{
return false;
}
}
bool var(const string s)
{
if(s.length()==0) return false;
if(s.length()==1&&s[0]>='A'&&s[0]<='Z')
return false;
if(s.length()>1)
{
int i=0;
while(i<s.length()&&s.at(i)!='(')//略過不是'('的字符
i++;
int j=i;
while(j<s.length()&&s.at(j)!=')')//略過')'前的字符
j++;
string ss=s.substr(i+1,j-i-1);//取出'('和')'之間的串
return var(ss);//遞歸調用var
}
else
{
return true;
}
}
string change(string f,transform q)//該函數查找t_f2在f中的位置並用t_f1替代f中相應的t_f2
{
int i=f.find(q.t_f2);
while(i<f.length())
{
i=f.find(q.t_f2);
if(i<f.length())
f=f.replace(i,q.t_f2.length(),q.t_f1);
}
return f;
}
