#include <string>
#include <stack>
#include <list>
#include <vector>


using namespace std;
#define  OPERNUM 5
#define  UNOPER 1
#define  BINOPER 2
#define  MIN_OPER_LENGTH 1
#define  MAX_OPER_LENGTH 3

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

const string strOperator[OPERNUM] =
{
	"~","&","|","=>","<=>"
};
const bool ifTruthTable[]  = {true,true,false,true}; //"=>"的真值表
const bool iffTruthTable[] = {true,false,false,true};//"<=>"的的真值表

//判斷是否是操作符
static bool IsOperator(string strOper,int& operType,int& pos)
{
      for(int i = 0;i < OPERNUM;i++)
	  {
		  if ( strOper == strOperator[i]) 
		  {
			  operType = (i == 0?UNOPER:BINOPER);
			  pos += strOperator[i].size();
			  return true;
		  }
	  }
	  return false;
}

//還應該增加一個保存所有變量的池，變量池
//還應該有保存一個簡化后的后序表達式
class PropositionVistor;
class Proposition
{
public:
	 Proposition* parse(const string&);
	virtual std::string getPostfix() ;
	virtual void accept(PropositionVistor& ) const ;
	virtual bool equivalent(const Proposition& ) const;
	virtual bool implied_by(const vector<const Proposition*>) const;
    vector<string> getVariant() const;
	GrammarProposition* grammarTree;//語法樹
	virtual ~Proposition();
	Proposition();
	Proposition(const string& );
protected:
	vector<string> varPool;//變量池

	void postfixTraverse(LGrammarProposition T,string& postfixString);//后序訪問
	void DestroyTree(LGrammarProposition T);
	void TrimVarPool();//去掉相同變量的程序
};

/*
class Var:public Proposition
{
public:
    Var();
    void accept(PropositionVistor& prop) const {  prop.visit(this) };
protected:
private:
};

class UnaryExp:public Proposition
{
public:
    UnaryExp();
	void accept(PropositionVistor& prop) const {  prop.visit(this) };
protected:
private:
};

class BinaryExp:public Proposition
{
public:
    BinaryExp();
    void accept(PropositionVistor& prop) const {  prop.visit(this) };
protected:
private:
};*/

class PropositionVistor
{
public:
	virtual void visit(const Proposition&){};
};

class PrefixVistor: public PropositionVistor
{
public:
     void visit(const Proposition& prop);
	 void prefixTraverse(LGrammarProposition T,string& prefixString);//前序訪問
};

class InfixVistor: public PropositionVistor
{
public:
	void visit(const Proposition& prop);
	void infixTraverse(LGrammarProposition T,string& infixString);//中序訪問
};

class TruthtableVistor: public PropositionVistor
{
public:
    void visit(const Proposition& prop);
	vector<bool> getTruthTable() const;
private:
	vector<bool>   assignPool;//變量賦值之后的存儲
	vector<bool>   truthTable;//真值表
	int serchVariant(string str,const Proposition& prop);//返回所要查找的變量的位置	
	bool ComputeTruthTable(LGrammarProposition T,const Proposition& prop);//構建真值表的一項
	void buildTruthTable(const Proposition& prop);//根據變量池來構建真值表
};

class CnfcheckVistor: public PropositionVistor
{
public:
	bool getResult(){return false;};
};

class DnfcheckVistor: public PropositionVistor
{
public:
	bool getResult(){return false;};
};

class CnfVistor: public PropositionVistor
{
public:
	Proposition* getResult(){return NULL;};
};

class DnfVistor: public PropositionVistor
{
public:
	Proposition* getResult(){return NULL;};
};