myset.h

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

template<class T> class mylist;
class myset;
template<class T> class mylistNode{
	friend class mylist<T>;
	friend class myset;
private:
	 T data;
	 mylistNode<T> *link;
	 mylistNode(T d,mylistNode<T> *l=NULL){data=d;link=l;}
};

template<class T> class mylist{
		friend class myset;
public:
	mylist():first(NULL),last(NULL){}
	~mylist();
	void push(const T item);
	void MakeEmpty();
	void SetFirst(){ current=first;}
	void Next(){current=current->link;}
	bool IsEnd(){ return current==NULL;};
	T GetData(){ return current->data;}
	mylistNode<T> *Getcurrent(){return current;}
	void Deletecurrent();
	void Delete(mylistNode<T> *p);
	int IsEmpty()const{return first==NULL;}
	bool Isin(const T &item);
	private:
	mylistNode<T> *first,*last,*current;
};
template<class T> mylist<T>::~mylist(){
	MakeEmpty();
}
template<class T> void mylist<T>::push(const T item){
	if(first==NULL)first=last=new mylistNode<T>(item,NULL);
	else {last->link=new mylistNode<T>(item,NULL);
	last=last->link;}
}

template<class T> void mylist<T>::MakeEmpty(){
	mylistNode<T> *p;
	while(first!=NULL){	p=first;first=first->link;delete p;}
	first=last=NULL;
}

template<class T> void mylist<T>::Deletecurrent(){
	mylistNode<T> *p,*q;
	p=first;
	while(p!=NULL&&p!=current){
		q=p;
		p=p->link;
	}
	q->link=p->link;
	delete current;
	current=q->link;
}

template<class T> bool mylist<T>::Isin(const T &item){
	mylistNode<T> *p=first;
	while(p!=NULL&&(p->data)!=item)p=p->link;
	if(p!=NULL)return true;
	return false;
}

template<class T> void mylist<T>::Delete(mylistNode<T> *p){
	mylistNode<T> *p1,*p2;
	p1=first;
	if(p==first){first=first->link;delete p1;return;}
	while(p1!=NULL&&p1!=p){
		p2=p1;
		p1=p1->link;
	}
	if(p1!=NULL){
		p2->link=p1->link;
		delete p1;
	}
}

struct atomic{
public:
	atomic(){flag=0;}
	atomic(const atomic &t){flag=t.flag;c=t.c;}
	int flag;
	char c;
	bool operator==(atomic &t){return flag==t.flag&&c==t.c;}
	bool operator!=(atomic &t){return flag!=t.flag||c!=t.c;}
};
class myset {
public:					
    myset( ){}
	void push(const atomic item){ l.push(item); }
	void Simple();
	void MakeEmpty(){l.MakeEmpty();}
	void SetFirst(){ l.current=l.first;}
	void Next(){ l.current=l.current->link;}
	bool IsEnd(){ return l.current==NULL;};
	atomic GetData(){ return l.current->data;}
	void Deletecurrent(){ l.Deletecurrent(); }
	int IsEmpty()const{ return l.IsEmpty(); }
	int cnf();
	int dnf();
	bool Isat(){return l.first->link==NULL;}
private:
    mylist<atomic> l;
};
int myset::cnf(){
	mylistNode<atomic> *p[58];
	for(int i=0;i<58;i++)
		p[i]=NULL;
	l.SetFirst();
	while(!l.IsEnd()){
		char c=l.GetData().c;
		int k=int(c-'A'); 
		if(p[k]==NULL){
			p[k]=l.Getcurrent();l.Next();
			}
		else{
			if((p[k]->data.flag)==(l.Getcurrent()->data.flag))
				l.Deletecurrent();
			else{
				return 1;
			   }
		   }
	}
	return 0;
}

int myset::dnf(){
mylistNode<atomic> *p[58];
	for(int i=0;i<58;i++)
		p[i]=NULL;
	l.SetFirst();
	while(!l.IsEnd()){
		char c=l.GetData().c;
		int k=int(c-'A'); 
		if(p[k]==NULL){
			p[k]=l.Getcurrent();l.Next();
			}
		else{
			if((p[k]->data.flag)==(l.Getcurrent()->data.flag))
				l.Deletecurrent();
			else{
				return 0;
			    }
		}
	}
	return 1;
}