//---------------------------------------------------------------------------

#ifndef TAUTOLOGYH
#define TAUTOLOGYH

/**
*  Classes definitions for tautology detection tool
*
*  author:    Bc. Jan Schindler
*  project:   DP, CVUT, FEL, 2009
*/



/**
*  Class: Cover - represents analyzing cover
*/
class Cover{

friend class TautologyDetector;

private:
        
	SoPLA *sopla;                // PLA representation in memory	

	// support fields
	char *configuration;         // confuguration of input variables
	int  *count2InRow;			 // number of DC per row
	int  **count01InColumn;      // number of '0' and '1' per column
	int  *indexesOfUnatesColumns;// indexes of unates columns
	int  *indexesOfUnatesRows;   // indexes of rows being used in unate reductant
	int  *selectedRows;          // selected rows for cofactor
	int  *selectedColumns;       // selected columns for cofactor
	int  *totalComponentedRows;  // is row in any component
	int  *selectedRowIndexes;    // indexes of rows being used in founded component
	int  *selectedColumnsIndexes;// indexes od columns being used in founded component
	
	int  countVariables;         // number of variables 	
	int  countTerms;             // number of terms
    int	 totalDCnumber;          // number of DC in cover  
	bool isCover;                // is F tautology  
	
public: 
              
	Cover(){                 // constructor
		countVariables = 0;
		countTerms = 0;
        totalDCnumber = 0; 
	};

	~Cover();                // desctructor
		
private:	
	void destroyFields();                  // dealocate memory
	void initSupportFields();              // init support fields
	void write();                          // write matrix 


	// metod create cofactor of most binate variable bz given flag ('0' or '1')
	Cover* createCofactor(int mostBinateJ, char flag);
	
	// metod create unate reductant if exists 
	Cover* unateReduction(int numberOfUnateColumns);
	
	// metod find non-trivial component of given row
	Cover* findComponentWithRow(int rowIndex);
	
	// metod returns all components
	vector<Cover*> findComponents();
	


	void searchTruthTable(int index);   // recursive brute force (variables < 7)
	void writeConfiguration();          // write configuration
    void preScanPLA();                  // scan for counts of 0, 1, DC

	bool containsRowOf2s();             // is in matrix row of only DC
	bool containsColumnOf0sOr1s();      // is in matrix column of only '0' or '1' 
	bool containsDeficientVertexCount();// is number of vertexes high enought
	bool isCoverByTruthTable();         // brute force (variables < 7)
	bool isConfigurationTrue();         // is configuration true
	bool isColumnUnate(int columnIndex);// is given column unate

	int specialCases();                 // analysis of matrix for special cases
	int binateSelect();                 // selection of most binate variable
	int detectUnateColumns();	        // return number of unate columns and set indexes
    int getTotalDCnumber();
};



/**
*  Class: TautologyDetector - wrapper class cooperative with the kernel of BOOM II
*/
class TautologyDetector{
  
private: 
    Cover *cover;
         
public:
       
    TautologyDetector(){}                // constructor
	
	~TautologyDetector(){}               // desctructor

                                         // INTERFACE
    int isPLAtautology(PLA* pla);        // is given PLA tautology
	int isSoPLAtautology(SoPLA* sopla);  // is given PLA tautology
	
private:
                
    int tautology();                      // main recursive loop       
};


//---------------------------------------------------------------------------
#endif
