ass2.cpp

离散数学中---------一阶谓词演算源代码

#include "ass2.h"
#include "math.h"
#include <iostream>
#include <string>

//typedef struct _GrammarProposition
//{
//	struct _GrammarProposition* lChild;
//	struct _GrammarProposition* rChild;
//	int attribution;
//	string strKey;
//}GrammarProposition,*LGrammarProposition;
using namespace std;

struct node {
     string  nodeChar;
     int     attribution;
};

Proposition::~Proposition()
{
	 DestroyTree(grammarTree);
}

Proposition::Proposition()
{
   grammarTree = NULL;
}

Proposition::Proposition(const string& strProp)
{
   parse(strProp);
}

void Proposition::DestroyTree(LGrammarProposition T)
{
     if (T)
	 {
			if ( T->lChild ) DestroyTree(T->lChild);
			if ( T->rChild ) DestroyTree(T->rChild);
			if (T->lChild == NULL && T->rChild == NULL) 
			{
				delete T;
				return;
			}
     }
}

bool Proposition::equivalent(const Proposition& prop) const
{
	 unsigned int i;
	 unsigned int nItems; 
	 TruthtableVistor localVistor,otherVistor;
     vector<bool> localTruthTable,otherTruthTable;
	 if (varPool.size() != prop.getVariant().size()) 
		 return false;
	 nItems = pow(2,varPool.size());
	 localVistor.visit(*this);
	 otherVistor.visit(prop);
     localTruthTable = localVistor.getTruthTable();
	 otherTruthTable = otherVistor.getTruthTable();
	 for(i=0;i<nItems;i++)
	 {
         if(localTruthTable[i] != otherTruthTable[i])
			 return false;
	 }    
}

void Proposition::accept(PropositionVistor& vistor) const 
{
     vistor.visit(*this);
}

bool Proposition::implied_by(const vector<const Proposition*>) const
{
	return false;
}

Proposition* Proposition::parse(const string& strProp)
{
    char ch;
	int i;
	int operType;
	//int operLength;
	int length;
	int status;
	int find = 0;
	int prePos,postPos;
	list<node> characterList;
	list<node>::iterator iter;
	stack<node> computeStack;
	stack<LGrammarProposition> tempNodeAddressStack;//处理中间节点,在从栈到语法树的过程中这要产生Ｐ｜Ｑ和　P|R  
	//等中间结点在栈中，每个中间节点都有一个树结构，所以要保存这些子二叉树的根节点的地址才行，所以又用了一个栈来辅助
	prePos = postPos = 0;
	ch = strProp[prePos++];
	node nodeTemp;
	while ( ch == '\t' || ch == '\n' || ch == ' ') ch = strProp[prePos++];
	prePos--;
	postPos = prePos;
    
	length = strProp.size();
	status = 0;
	//check if valid  词法分析
	do 
	{ 		
		ch = strProp[postPos];

		//0----处理变量   1----处理操作符
        if ( status == 0) 
		{
			if (isalpha(ch)) 
			{
				postPos++;
			}
			else if ( ch == ' ') 
			{
				if ( prePos == postPos) 
				{
					return NULL;
				}
				else
				{
					nodeTemp.nodeChar.assign(strProp,prePos,postPos-prePos);
					nodeTemp.attribution = 0;
					characterList.push_back(nodeTemp);
					nodeTemp.nodeChar="";
				}
				prePos = postPos;
				ch = strProp[prePos++];
				while ( ch == '\t' || ch == '\n' || ch == ' ') ch = strProp[prePos++];
				prePos--;
				postPos =  prePos;
				//开始进入操作符状态转化
				find = 0;
				if (!isalpha(ch)) 
				{
					for( i = MIN_OPER_LENGTH;i <= MAX_OPER_LENGTH;i++)
					{
                         nodeTemp.nodeChar.assign( strProp ,prePos,i);
						 if (IsOperator( nodeTemp.nodeChar,operType,postPos))
						 {
							 status = 1;
							 //nodeTemp.nodeChar.assign(strProp,prePos,postPos-prePos);
							 nodeTemp.attribution = operType;
							 characterList.push_back(nodeTemp);
							 nodeTemp.nodeChar="";
							 prePos = postPos;
							 find = 1;
							 break;
						 }
					}
					//没有这样的操作符
                    if (find == 0) return NULL;
				}//if (!isalpha(ch))
			}//else if ( ch == ' ')
			else
			{
                return NULL;
			}
        }//if ( status == 0)
		if (status == 1) 
		{
			if (postPos >= length) break;
			ch = strProp[prePos++];
			while ( ch == '\t' || ch == '\n' || ch == ' ') ch = strProp[prePos++];
			prePos--;
			postPos =  prePos;
			if (isalpha(ch)) 
			{
				postPos++;
				status = 0;
				continue;
			}
			find = 0;
			if (!isalpha(ch)) 
			{
				for( i = MIN_OPER_LENGTH;i <= MAX_OPER_LENGTH;i++)
				{
					nodeTemp.nodeChar.assign( strProp ,prePos,i);
					if (IsOperator( nodeTemp.nodeChar,operType,postPos))
					{
						status = 1;
						//nodeTemp.nodeChar.assign(strProp,prePos,postPos-prePos);
						nodeTemp.attribution = operType;
						characterList.push_back(nodeTemp);
						nodeTemp.nodeChar="";
						prePos = postPos;
						find = 1;
						break;
					}
				}
				//没有这样的操作符
				if (find == 0) return NULL;
			}//end for
		}//if (status == 1)	
	} while( postPos <= length);

	//Check grammar and generate grammar tree 语法分析
	node tempNode;
	LGrammarProposition pNode;

	LGrammarProposition pTreeNode = NULL;
	LGrammarProposition plChildNode = NULL;
	LGrammarProposition prChildNode = NULL;

	for(iter = characterList.begin();iter != characterList.end();iter++)
	{
        switch( iter->attribution) 
		{
			case 0:
				varPool.push_back(iter->nodeChar);
                //varPool.push_back(*iter.nodeChar);
				computeStack.push(*iter);
        		break;
			case 1:
				if (computeStack.empty())
				{
					return NULL;
                }
                tempNode = computeStack.top();
				//4---表示临时节点,#---表示临时节点的符号
				if ( tempNode.attribution == 4 && tempNode.nodeChar == "#") 
				{
					pNode = tempNodeAddressStack.top();
					pTreeNode = new GrammarProposition;
					pTreeNode->attribution = 1;
					pTreeNode->lChild = NULL;
					pTreeNode->rChild = pNode;
					pTreeNode->strKey = iter->nodeChar;
					tempNodeAddressStack.pop();
				}
				else
				{
					plChildNode = new GrammarProposition;
					plChildNode->attribution = tempNode.attribution;
					plChildNode->strKey = tempNode.nodeChar;
					plChildNode->lChild = NULL;
					plChildNode->rChild = NULL;	
					pTreeNode = new GrammarProposition;
					pTreeNode->attribution = 1;
					pTreeNode->lChild = plChildNode;
					pTreeNode->rChild = NULL;
					pTreeNode->strKey = iter->nodeChar;
				}
				computeStack.pop();
				tempNode.attribution = 4;
				tempNode.nodeChar = "#";
				computeStack.push(tempNode);
				tempNodeAddressStack.push(pTreeNode);
        		break;
			case 2:
				if (computeStack.empty())
				{
					return NULL;
                }
				//右孩子
				tempNode = computeStack.top();
				if ( tempNode.attribution == 4 && tempNode.nodeChar == "#") 
				{
					pNode = tempNodeAddressStack.top();
					pTreeNode = new GrammarProposition;
					pTreeNode->attribution = 2;
					pTreeNode->lChild = NULL;
					pTreeNode->rChild = pNode;//指向临时保存的子语法树（中间结点）
					pTreeNode->strKey = iter->nodeChar;
					tempNodeAddressStack.pop();//中间结点出栈
				}
				else
				{
					prChildNode = new GrammarProposition;
					prChildNode->attribution = tempNode.attribution;
					prChildNode->strKey = tempNode.nodeChar;
					prChildNode->lChild = NULL;
					prChildNode->rChild = NULL;	
					pTreeNode = new GrammarProposition;
					pTreeNode->attribution = 2;
					pTreeNode->lChild = NULL;
					pTreeNode->rChild = prChildNode;
					pTreeNode->strKey = iter->nodeChar;
				}
				computeStack.pop();
				//左孩子
				tempNode = computeStack.top();
				if ( tempNode.attribution == 4 && tempNode.nodeChar == "#") 
				{
					pNode = tempNodeAddressStack.top();
					pTreeNode->lChild = pNode;
					tempNodeAddressStack.pop();
				}
				else
				{
					plChildNode = new GrammarProposition;
					plChildNode->attribution = tempNode.attribution;
					plChildNode->strKey = tempNode.nodeChar;
					plChildNode->lChild = NULL;
					plChildNode->rChild = NULL;	

					pTreeNode->lChild = plChildNode;
				}
				computeStack.pop();
				//tempNode = computeStack.top();

				tempNode.attribution = 4;
				tempNode.nodeChar = "#";
				computeStack.push(tempNode);
                tempNodeAddressStack.push(pTreeNode);
				break;
        }
	}
	//清空栈
	tempNodeAddressStack.pop();
	grammarTree = pTreeNode;
	//int varSize;
	//varSize = varPool.size();
	//整理变量池,去掉重复的部分
	TrimVarPool();
	return this;
}

void Proposition::TrimVarPool()
{
    vector<string>::iterator  iter_i,iter_j;
    for(iter_i = varPool.begin();iter_i != varPool.end();iter_i++)
	{
		for(iter_j = iter_i + 1;iter_j != varPool.end();iter_j++)
		{
			if (*iter_i == *iter_j)
			{
				varPool.erase(iter_j);
				if ( iter_j == varPool.end()) break;
			}
		}
	}
	cout<<"变量集合:"<<endl;
	for(iter_i = varPool.begin();iter_i != varPool.end();iter_i++)
	{
		cout<<*iter_i<<endl;
	}
}


//没弹出一个根节点就先输出一个(，然后在它左右孩子节点访问完后就输出)
void Proposition::postfixTraverse(LGrammarProposition T,string& postfixString)
{
	if (T) 
	{
		postfixTraverse(T->lChild,postfixString);
		postfixTraverse(T->rChild,postfixString);
        postfixString += T->strKey;
		postfixString += " ";
	}
}



string Proposition::getPostfix() 
{
	string postfixString;
    postfixTraverse(grammarTree,postfixString);
	return postfixString;
}

vector<string> Proposition::getVariant() const
{
	return varPool;
}


void InfixVistor::visit(const Proposition& prop)
{
	
	string infixStr = "";
	infixTraverse(prop.grammarTree,infixStr);
	cout<<infixStr<<endl;	
}

void PrefixVistor::visit(const Proposition& prop)
{
	
	string prefixStr = "";
	prefixTraverse(prop.grammarTree,prefixStr);
	cout<<prefixStr<<endl;	
}

void TruthtableVistor::visit(const Proposition& prop)
{
	buildTruthTable(prop);	
}

int TruthtableVistor::serchVariant(string str,const Proposition& prop)
{
	int index ;
    vector<string>::iterator  iter;
	vector<string> varPool;
	varPool = prop.getVariant();
	for(iter = varPool.begin(),index = 0;iter != varPool.end();iter++,index++)
	{
		if (str == *iter) {
			return  index;
		}
	}
	return -1;
}

vector<bool> TruthtableVistor::getTruthTable() const
{
    return truthTable;
}

bool TruthtableVistor::ComputeTruthTable(LGrammarProposition T,const Proposition& prop)
{
	int distance,index;
	bool bLeftRet,bRightRet,bRet;
	if (T) 
	{
        switch(T->attribution) {
        case 0:
			distance = serchVariant(T->strKey,prop);
			bRet =  assignPool[distance];
			break;
        case 1:
			bLeftRet = ComputeTruthTable(T->lChild,prop);
			bRet = ~bLeftRet;
			break;
		case 2:
			bLeftRet = ComputeTruthTable(T->lChild,prop);
			bRightRet = ComputeTruthTable(T->rChild,prop);
			if (T->strKey == "&" )   bRet = bLeftRet & bRightRet;
			if (T->strKey == "|" )   bRet = bLeftRet | bRightRet; 
			if (T->strKey == "=>" )  
			{
				index = ((int)bLeftRet) << 1 | ((int)bRightRet);
				bRet = ifTruthTable[index];
			}
			if (T->strKey == "<=>") 
			{
				index = ((int)bLeftRet) << 1 | ((int)bRightRet);
				bRet = iffTruthTable[index];		
			}
			break;
        }
	}
	return bRet;
}

void TruthtableVistor::buildTruthTable(const Proposition& prop)
{
	//初始化真值表的变量
	int i;
	vector<string>::iterator  var_iter;
	vector<bool>::iterator  iter;
	unsigned int count = 0,nBit,nMask;
	vector<string> varPool = prop.getVariant();
	int varSize;
	varSize = varPool.size();
	unsigned int nItems = pow(2,varSize);
	truthTable.clear();
	for(var_iter = varPool.begin();var_iter != varPool.end();var_iter++)
	{
	    cout<<*var_iter<<"    ";	
	} 
	for(i = 0;i<varSize;i++) assignPool.push_back(false);
	cout<<endl;
	bool truthRet;
	while (count<nItems) 
	{
		for(iter = assignPool.begin(),nBit = 0;iter != assignPool.end();iter++,nBit++)
		{
			nMask = 1 << nBit;
			*iter = (count & nMask) == 0 ?false:true;
			cout<<*iter<<"    ";
		}
		truthRet = ComputeTruthTable(prop.grammarTree,prop);
		cout<< truthRet<<endl;
		truthTable.push_back( truthRet );
		count++;
	}	
}


//没弹出一个根节点就先输出一个(，然后在它左右孩子节点访问完后就输出)
void PrefixVistor::prefixTraverse(LGrammarProposition T,string& prefixString)
{
	static PrefixEntry = 0;
	if (T) 
	{
		PrefixEntry++;
		if (T->attribution>0) {
			if ( PrefixEntry > 1) {
				prefixString += " ";
			}

			prefixString += "(";
			prefixString += " ";
		}
		if (T->attribution == 0) {
			prefixString += " ";
		}
        prefixString += T->strKey;		
        prefixTraverse(T->lChild,prefixString);
        prefixTraverse(T->rChild,prefixString);
		if (T->attribution>0) {
			if ( PrefixEntry > 1) {
				prefixString += " ";
			}
			prefixString += ")";
		}

	}
}

//没弹出一个根节点就先输出一个(，然后在它左右孩子节点访问完后就输出)
void InfixVistor::infixTraverse(LGrammarProposition T,string& infixString)
{
	static infixEntry = 0;

	if (T) 
	{
		infixEntry++;
		if (T->attribution>0) {
			if (infixEntry > 1) infixString += " ";
		    infixString += "(";
		
		}
		infixTraverse(T->lChild,infixString);
		infixString += " ";
        infixString += T->strKey;
        infixTraverse(T->rChild,infixString);
		
		if (T->attribution>0) {
		   if (infixEntry > 1)	infixString += " ";
		   infixString += ")";
		}
	}
}