formulatree.h

一个基于H.wang的谓词演算公式的机器证明的vc实现

void mystrcpy(char *s1,char *s2){
	int i;
	for(i=0;i<(int)strlen(s2);i++)
		s1[i]=s2[i];
	s1[i]='\0';
}
void mystrncpy(char *s1,char *s2,int n){
	for(int i=0;i<n;i++)
		s1[i]=s2[i];
}
template <class Type> class FormulaTree;	
template <class Type> class TreeNode{
	friend class FormulaTree<Type>;
public:
	TreeNode ( ):leftChild (NULL), rightChild (NULL) {}
    TreeNode ( Type item,int value,TreeNode<Type> *left = NULL, TreeNode<Type> *right = NULL ): data (item),flag(value), leftChild (left), rightChild(right) { }    
	Type GetData ( ) const { return data; } 
private:
    TreeNode<Type> *leftChild, *rightChild;      
    Type data;
	int flag;
};
template <class Type> class FormulaTree {	
public:
    FormulaTree ( ) : root (NULL) { }
	FormulaTree(Type *str);
	FormulaTree(const FormulaTree<Type> &s){ root= Copy(s.root);}
	FormulaTree ( Type value){RefValue =value;  root =NULL;}
    virtual ~FormulaTree ( ) { destroy ( root ); }
	virtual void Insert (Type *s );
	void Add(TreeNode <Type> *&current,Type *s);
	void preorder(TreeNode <Type> *current);
	void inorder(TreeNode <Type>* current);
	void postorder1(TreeNode<Type>* current);
	void postorder2(TreeNode<Type>* current);
	void postorder3(TreeNode<Type>* current);
	void postorder4(TreeNode<Type>* current);
    void postorder(TreeNode<Type>* current);
	void disp ();
	TreeNode<Type> *Copy(TreeNode <Type>* current);
	void ToCNF1(TreeNode <Type> *&current);
	void ToCNF2(TreeNode <Type> *&current);
	void ToCNF3(TreeNode <Type> *&current);
	void ToCNF4(TreeNode <Type> *&current);
	void ToDNF4(TreeNode <Type> *&current);
	char* ToCNF();
	char* ToDNF();
    const TreeNode <Type> *GetRoot ( ) const{ return root; } 
	bool Isalp(char s){ return ((s<='z'&&s>='a')||(s<='Z'&&s>='A'));}
	char *Change1(char *str);
	char *Change2(char *str);
	char * Toinfix1(char *str);
	char * Toinfix2(char *str);
	int number();
 private:
    TreeNode <Type> *root;
	int i;
	Type *Formu;
    Type RefValue; //标志结束符
    void destroy(TreeNode<Type> *current);
	int number(TreeNode <Type> *p);
};
template<class Type>
FormulaTree<Type>::FormulaTree(Type *str){
    RefValue='@'; 
	Type *s=Change2(Change1(str));
	 Insert(s);
}
template<class Type>
void FormulaTree <Type>::postorder1(TreeNode<Type>* current){
	if(current!=NULL){
		postorder1(current->leftChild);
	    postorder1(current->rightChild);
	    ToCNF1(current);
	    if(i!=1)i=0;
	}
}
template<class Type>
void FormulaTree <Type>:: postorder2(TreeNode<Type>* current){ 
	if(current!=NULL){
		postorder2(current->leftChild);
		postorder2(current->rightChild);
		ToCNF2(current);
		if(i!=1)i=0;
	}
}
template<class Type>
void FormulaTree <Type>:: postorder3(TreeNode<Type>* current){
	if(current!=NULL){
		postorder3(current->leftChild);
		postorder3(current->rightChild);
		ToCNF3(current);
		if(i!=1)i=0;
	}
}
template<class Type>
void FormulaTree <Type>:: postorder4(TreeNode<Type>* current){
	if(current!=NULL){
		postorder4(current->leftChild);
		postorder4(current->rightChild);
		ToCNF4(current);
		if(i!=1)i=0;
	}
}
template<class Type>
void FormulaTree <Type>:: postorder(TreeNode<Type>* current){
	 if(current!=NULL){
		 postorder(current->leftChild);
		postorder(current->rightChild);
		ToDNF4(current);
		 if(i!=1)i=0;
	 }
 }
template<class Type>
TreeNode<Type> * FormulaTree <Type>::Copy(TreeNode <Type>* current){
		if(current==NULL) return NULL;
		TreeNode<Type> *temp=new TreeNode<Type>;
		temp->data=current->data;
		temp->leftChild=Copy(current->leftChild);
		temp->rightChild=Copy(current->rightChild);
		return temp;
}

template <class Type> void FormulaTree <Type>:: destroy ( TreeNode<Type> *current ){
	if (current != NULL&&current->flag==0 ) 
	{  //current->flag++;
       destroy ( current->leftChild );
       destroy ( current->rightChild );
	   delete current;
    }
}
template <class Type> void FormulaTree <Type> ::Insert(Type *s){
	i=0;
	Add(root,s);
}
template <class Type> void FormulaTree<Type> ::Add(TreeNode <Type> *&current,Type* s ){
     Type item;item=s[i];i++;int value=0;
	 if( item != RefValue)
	 {current=new TreeNode <Type> (item,value);
	           if ( current == NULL ) exit (1); 
            Add ( current->leftChild,s);
			Add ( current->rightChild,s);
        }
        else current = NULL; 
}	
template <class Type> void FormulaTree<Type>::ToCNF1(TreeNode<Type> *&p){ 
	TreeNode<Type> *temp=new TreeNode<Type>;temp->flag=0;
	TreeNode<Type> *q=new TreeNode<Type>;q->flag=0;
	TreeNode<Type> *l=new TreeNode<Type>;l->flag=0;
	TreeNode<Type> *r=new TreeNode<Type>;r->flag=0;
	Type t=p->data;
	switch(t)
	{ 
	case '>':
		p->data='+';
		temp->data='!';temp->leftChild=NULL;
		temp->rightChild=p->leftChild;
		p->leftChild=temp;
		i=1;break;
	case '=':
		p->data='*';
		temp->data=q->data='+';
		l->data='!';l->leftChild=NULL;l->rightChild=p->leftChild;
		temp->leftChild=l;temp->rightChild=p->rightChild;
		r->data='!';r->leftChild=NULL;r->rightChild=p->rightChild;
		q->rightChild=r;q->leftChild=p->leftChild;
		p->leftChild=temp;p->rightChild=q;
		i=1;
		break;
	default: break;
	}
}
template <class Type> void FormulaTree<Type>::ToCNF2(TreeNode<Type> *&p){
	TreeNode<Type>*temp=p->rightChild;
	TreeNode<Type> *l=new TreeNode<Type>;l->flag=0;
	TreeNode<Type> *r=new TreeNode<Type>;r->flag=0;
	 if(p->data=='!'&&temp->data=='+')
	 {p->data='*';
	 l->data=r->data='!';
	 l->leftChild=r->leftChild=NULL;
	 l->rightChild=temp->leftChild;r->rightChild=temp->rightChild;
	 p->leftChild=l;p->rightChild=r;
	 i=1;
	 }
	 else if(p->data=='!'&&temp->data=='*')
	 {p->data='+';
	 l->data=r->data='!';
	 l->leftChild=r->leftChild=NULL;
	 l->rightChild=temp->leftChild;r->rightChild=temp->rightChild;
	 p->leftChild=l;p->rightChild=r;
	 i=1;
	 }
}

template <class Type> void FormulaTree<Type>::ToCNF3(TreeNode<Type> *&p){
	TreeNode<Type>*temp=p->rightChild; 
	if(p->data=='!'&&temp->data=='!')
	{TreeNode<Type>*q=temp->rightChild;p->data=q->data;
	p->leftChild=q->leftChild;
	p->rightChild=q->rightChild;
	i=1;
	}
}
template <class Type> void FormulaTree<Type>::ToCNF4(TreeNode<Type> *&p){
	TreeNode<Type>*temp1=p->rightChild;
	if(p->data=='+'&&temp1->data=='*'){ 
		TreeNode<Type>*q=new TreeNode<Type>;q->flag=0;
	    q->data='+';q->leftChild=p->leftChild;
	    q->rightChild=temp1->leftChild;
		TreeNode<Type>*ptr=new TreeNode<Type>;
		ptr->data='+';ptr->flag=0;
		ptr->leftChild=p->leftChild;ptr->rightChild=temp1->rightChild;
		p->data='*';p->leftChild=q;p->rightChild=ptr;
		i=1;
	  }
	TreeNode<Type> *temp2=p->leftChild;
	if(p->data=='+'&&temp2->data=='*'){
		TreeNode<Type>*q=new TreeNode<Type>;q->flag=0;
		q->data='+';q->rightChild=p->rightChild;
	    q->leftChild=temp2->rightChild;
		TreeNode<Type>*ptr=new TreeNode<Type>;
		ptr->data='+';ptr->flag=0;
		ptr->rightChild=p->rightChild;ptr->leftChild=temp2->leftChild;
		p->data='*';p->leftChild=ptr;p->rightChild=q;
		i=1;
	}
}
  
template <class Type>void FormulaTree<Type>::ToDNF4(TreeNode<Type> *&p){
	TreeNode<Type>*temp1=p->rightChild;
    if(p->data=='*'&&temp1->data=='+'){
		TreeNode<Type>*q=new TreeNode<Type>;
		q->data='*';q->flag=0;q->leftChild=p->leftChild;
	    q->rightChild=temp1->leftChild;
        TreeNode<Type>*ptr=new TreeNode<Type>;
		ptr->data='*';ptr->flag=0;
		ptr->leftChild=p->leftChild;ptr->rightChild=temp1->rightChild;
		p->data='+';p->leftChild=q;p->rightChild=ptr;
		i=1;
	} 
    TreeNode<Type> *temp2=p->leftChild;
    if(p->data=='*'&&temp2->data=='+'){
		TreeNode<Type>*q=new TreeNode<Type>;
		q->data='*';q->flag=0;q->rightChild=p->rightChild;
	    q->leftChild=temp2->rightChild;
		TreeNode<Type>*ptr=new TreeNode<Type>;
		ptr->data='*';ptr->flag=0;ptr->rightChild=p->rightChild;ptr->leftChild=temp2->leftChild;
		p->data='+';p->leftChild=ptr;p->rightChild=q;
		i=1;
  }
}
 template <class Type>void FormulaTree<Type> ::preorder (TreeNode <Type>* p){
	 if(p!=NULL){
		 Formu[i]=p->data;
		 i++;
		 preorder(p->leftChild);
		 preorder(p->rightChild);
	 }
 }
 template <class Type>void FormulaTree<Type> ::inorder(TreeNode <Type>* current){
      mystack < TreeNode <Type>* >mystack;
      TreeNode <Type>*p = current;
	  while (p!= NULL || !mystack.IsEmpty ()){
		 while (p != NULL){
			 mystack.push(p);
             p = p->leftChild;
		 }
		 if (!mystack.IsEmpty ()){
			 p = mystack.top ();
             mystack.pop ();
             p= p->rightChild;        
		 }
	  }
 }
 template <class Type> char* FormulaTree<Type> ::ToCNF(){ 
	 i=2;while(i!=0){ i=2;postorder1(root);}
     i=2;while(i!=0){ i=2;postorder2(root);}
	 i=2;while(i!=0){ i=2;postorder3(root);}
	 i=2;while(i!=0){ i=2;postorder4(root);}
	 int num=number();
	  Formu=new Type[num*2];
	  preorder (root);
	  Formu[i]='\0';
	  char *s;s=new char[strlen(Formu)];
	  s=Toinfix1(Formu);
	  delete []Formu;
	  return s;
 }
 template <class Type> char* FormulaTree<Type>::ToDNF(){
	 i=2;while(i!=0){ i=2;postorder1(root);}
     i=2;while(i!=0){ i=2;postorder2(root);}
	 i=2;while(i!=0){ i=2;postorder3(root);}
	 i=2;while(i!=0){ i=2;postorder(root);}
	  int num=number();
	  Formu=new Type[num*2];
      preorder (root);
	  Formu[i]='\0';
	  char *s;s=new char[strlen(Formu)];
	  s=Toinfix2(Formu);
	  delete []Formu;
	  return s;
 }
 template <class Type> void FormulaTree<Type> ::disp(){
      inorder(root);
 }
template <class Type> 
char *FormulaTree<Type> ::Change1(char *str){//将公式转为前缀
	mystack<char> temp,operat;
	for(int i=strlen(str)-1;i>=0;i--){
		if( ('a'<=str[i]&&str[i]<='z')||('A'<=str[i]&&str[i]<='Z') )
			temp.push(str[i]);
		else{
			if(str[i]=='('){
				char c;
				while( ( c=operat.top() )!=')' ){ temp.push(c); operat.pop(); }
				operat.pop(); 
			}
			else if(str[i]=='!')
				temp.push(str[i]);
			else
				operat.push(str[i]);
		}
	}
	while(operat.IsEmpty()==false){
		temp.push(operat.top());
		operat.pop();
	}
	char *s;
	s=new char[strlen(str)+1];
	int j=0;
	while(temp.IsEmpty()==false){
		s[j++]=temp.top();
		temp.pop();
	}
	s[j]='\0';
	return s;
}
template <class Type> 
char *FormulaTree<Type> ::Change2(char *s){  
	int i=0,j=0;
	char *str;str=new char[5*strlen(s)];
		for(i=0;i<(int)strlen(s);i++)
		{
			if(s[i]=='!')
		    {str[j]=s[i];
			str[++j]='@';
			j++;}
			else if(Isalp(s[i]))
			{str[j]=s[i];
			 str[++j]='@';
			 str[++j]='@';
			 j++;
			}
			else
			{	str[j]=s[i]; j++;
			}
		}
		str[j]='\0';
	return str;
}
template <class Type> 
char *FormulaTree<Type> ::Toinfix1(char *str){
	mystack<char *> st;
	for(int i=strlen(str)-1;i>=0;i--){
		if( ('a'<=str[i]&&str[i]<='z')||('A'<=str[i]&&str[i]<='Z') ){
			char *temp=new char[2];
			temp[0]=str[i];
			temp[1]='\0';
			st.push(temp);
		}
		else if(str[i]=='!'){
			char *op=st.top(),*temp;
			st.pop();
			temp=new char[strlen(op)+4];
			temp[0]='!';
			mystrcpy(temp+1,op);
			temp[strlen(op)+1]='\0';
			st.push(temp);
			delete []op;
		}
else if(str[i]=='+')
{			char *op1,*op2;
			op1=st.top(); st.pop();
			op2=st.top(); st.pop();
			char *temp=new char[strlen(op1)+strlen(op2)+6];
			mystrcpy(temp,op1);
			temp[strlen(op1)]=str[i];
			mystrcpy(temp+strlen(op1)+1,op2);
			temp[strlen(op1)+strlen(op2)+1]='\0';
			st.push(temp);
			delete []op1;delete []op2;
		}
		else if(str[i]=='*'){
			int k1=0,k2=0;
			char *op1,*op2;
			op1=st.top(); st.pop();
			op2=st.top(); st.pop();
			char *temp=new char[strlen(op1)+strlen(op2)+6];
			if(strlen(op1)>2&&op1[0]!='(')temp[k1++]='(';
			mystrcpy(temp+k1,op1);
			if(strlen(op1)>2&&op1[0]!='(')temp[strlen(op1)+k1]=')';
			temp[strlen(op1)+k1*2]=str[i];
			if(strlen(op2)>2&&op2[0]!='('){temp[strlen(op1)+2*k1+1]='(';k2++;}
			mystrcpy(temp+strlen(op1)+2*k1+k2+1,op2);
			if(strlen(op2)>2&&op2[0]!='(')temp[strlen(op1)+strlen(op2)+2*k1+k2+1]=')';
			temp[strlen(op1)+strlen(op2)+2*k1+2*k2+1]='\0';
			st.push(temp);
			delete []op1;delete []op2;
		}
	}
	char *temp=st.top();
	return temp;
}
template <class Type>
char *FormulaTree<Type> ::Toinfix2(char *str){
	mystack<char *> st;
	for(int i=strlen(str)-1;i>=0;i--){
		if( ('a'<=str[i]&&str[i]<='z')||('A'<=str[i]&&str[i]<='Z') ){
			char *temp=new char[2];
			temp[0]=str[i];
			temp[1]='\0';
			st.push(temp);
		}
		else if(str[i]=='!'){
			char *op=st.top(),*temp;
			st.pop();
			temp=new char[strlen(op)+4];
			temp[0]='!';
			mystrcpy(temp+1,op);
			temp[strlen(op)+1]='\0';
			st.push(temp);
			delete []op;
		}
else if(str[i]=='*')
{			char *op1,*op2;
			op1=st.top(); st.pop();
			op2=st.top(); st.pop();
			char *temp=new char[strlen(op1)+strlen(op2)+6];
			mystrcpy(temp,op1);
			temp[strlen(op1)]=str[i];
			mystrcpy(temp+strlen(op1)+1,op2);
			temp[strlen(op1)+strlen(op2)+1]='\0';
			st.push(temp);
			delete []op1;delete []op2;
		}
		else if(str[i]=='+'){
			int k1=0,k2=0;
			char *op1,*op2;
			op1=st.top(); st.pop();
			op2=st.top(); st.pop();
			char *temp=new char[strlen(op1)+strlen(op2)+6];
			if(strlen(op1)>2&&op1[0]!='(')temp[k1++]='(';
			mystrcpy(temp+k1,op1);
			if(strlen(op1)>2&&op1[0]!='(')temp[strlen(op1)+k1]=')';
			temp[strlen(op1)+k1*2]=str[i];
			if(strlen(op2)>2&&op2[0]!='('&&op2[1]!='+'&&op2[2]!='+'){temp[strlen(op1)+2*k1+1]='(';k2++;}
			mystrcpy(temp+strlen(op1)+2*k1+k2+1,op2);
			if(strlen(op2)>2&&op2[0]!='('&&op2[1]!='+'&&op2[2]!='+')temp[strlen(op1)+strlen(op2)+2*k1+k2+1]=')';
			temp[strlen(op1)+strlen(op2)+2*k1+2*k2+1]='\0';
			st.push(temp);
			delete []op1;delete []op2;
		}
	}
	char *temp=st.top();
	return temp;
}
template <class Type> 
int FormulaTree<Type> ::number(){
	return number(root);
}
template <class Type> 
int FormulaTree<Type> ::number(TreeNode<Type> *p){
	if(p==NULL)
		return 0;
	else
		return 1+number(p->leftChild)+number(p->rightChild);
}