/*
  Name:			實現(xiàn)一般表示式的合一算法(50分)
  Author:		WXQ
  Date:			22-11-05 00:52
  Discription:	UNIFY
*/

#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))
    {
		transform t=dif(f1,f2);
		//cout<<t.t_f1<<"\t"<<t.t_f2<<endl;
		int flag=legal(t);			
		if(flag==0)
			return false;
		else
		{
			mgu.push_back(t);
			//if(flag==1)
			{
				f1=change(f1,mgu.back());
				f2=change(f2,mgu.back());
				cout<<"after change:"<<endl;
				cout<<"f1:"<<f1<<endl;
				cout<<"f2:"<<f2<<endl;
			}
			/*else
			{
				f2=change(f2,mgu.back());
				//cout<<t.t_f1<<endl;
				if(var(t.t_f1))
					f1=change(f1,mgu.back());
				
			}
			*/
			
			if(same(f1,f2)) break;
		}
    }
	return true;
}

bool same(const string f1, const string 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)
{
	int i=0;
	transform t;
	while(f1.at(i)==f2.at(i))
		i++;
	int j1=i;
	while(j1<f1.length()-1&&f1.at(j1)!=',')
		j1++;
	if(j1-i==0)	return t;
	t.t_f1=f1.substr(i,j1-i);
	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);
	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)
{
	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))
		return 0;
	string temp;
	temp=t.t_f1;
	t.t_f1=t.t_f2;
	t.t_f2=temp;
	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++;
		/*
		if(i==s.length())
			cout<<"why here i"<<endl;
			*/
		int j=i;
		while(j<s.length()&&s.at(j)!=')')
			j++;
		/*
		if(j==s.length())
			cout<<"why here j"<<endl;
			*/
		string ss=s.substr(i+1,j-i-1);
		return varData(ss);
	}
	else 
	{
		//cout<<"wrong here1"<<endl;
		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++;
		/*
		if(i==s.length())
			cout<<"why here i"<<endl;
			*/
		int j=i;
		while(j<s.length()&&s.at(j)!=')')
			j++;
		/*
		if(j==s.length())
			cout<<"why here j"<<endl;
			*/
		string ss=s.substr(i+1,j-i-1);
		return var(ss);
	}
	else 
	{
		//cout<<"wrong"<<endl;
		return true;
	}
}




string change(string f,transform q)
{
	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;
}