#ifndef __COMPLEMENT__

#define __COMPLEMENT__

#include "../../Kernel/kernelincludes.h"
#include "../../Multilevel/Blif.h"

class Complement
{
	public:
		Complement();													// constructor
		PLA * PLAComplement(PLA * pla, int dc_man);						// function for compuping complement of PLA
		bool  GetContainment() const;									// getter for 'containment' settings
		void  SetContainment(bool c);									// setter for 'containment' settings 
		bool  GetMergeShared() const;									// getter for 'merge_shared' settings 
		void  SetMergeShared(bool ms);									// setter for 'merge_shared' settings 
		bool  GetVerbose() const;										// getter for verbose mode
		void  SetVerbose(bool v);										// setter for verbose mode
		int   GetTimeLimit() const;									    // getter for time limit
		void  SetTimeLimit(int l);										// setter for time limit
		bool  IsLimitExceeded() const;									// getter for limit_exceeded
		void printHelp() const;											// prints hepl
		~Complement();													// destructor
	private:
		class MultiResult												// this class is used as a return typ of CheckSpecialCases function
		{
			public:
				MultiResult(Cube * c, int s, bool all2s);				// constructor
				~MultiResult();											// destructor
				Cube * mapa;											// indicates columns of all 1s (by '1' value in the j-th position) and columns of all 0s (by '0' value in the j-th position)
				int split_var;											// says which variable should be chosen as a splitting variable
				bool all2s;												// indicates that a row of all 2s (or '-') was found - in other words it's a tautology
		};  
		int BinateSelect(SoPLA * pla);									// says which variable should be chosen as splitting variable - but CheckSpecialCases is used instead
		SoPLA * MergeWithContainment(SoPLA* pla0, SoPLA* pla1, int ind);// merges two parts of splitted function with respect to the i-th variable
		void PrintPersonalityMatrix(SoPLA * pers_m);					// prints the personality matrix to the output - used only for testing
		void PrintTranslationMatrix(const Cube * V);					// prints the translation matrix to the output - used only for testing
		int UnateComplement_SplitSelect(SoPLA * pers_mat);				// complutes the splitting variable for splitting the personality matrix of a unate function - this splitting variable is only used while computing unate (while computing unate complement)
		SoPLA * PersCofactors(SoPLA * pers_mat, int j, int sign);		// computes the cofactors of persoality matrix (!! not PLA !!) with respect to j-th variable
		SoPLA * DemorganForUC(CubeList::const_iterator term_ti);		// Demorgan's Law - but only for personality matrix (unate complementation)
		SoPLA * Pers_Unate_Complement(SoPLA * pers_mat);				
		SoPLA * GeneratePersonalMatrix(SoPLA * pla);					// computes the personality matrix of SoPLA
		Cube * Monotone(SoPLA * pla);									// says in which variables is given function monotone (increasing or decreasing)
		SoPLA * Translate(SoPLA * pers_mat, Cube * V);					// translation from personality matrix back to SoPLA
		SoPLA * UnateComplement(SoPLA * pla);							// computes the comlement of a unate function
		Complement::MultiResult * CheckSpecialCases(SoPLA * pla);		// checks the three special cases in SingleOutputComplement - is used instead of (IsUnate + searching for a column of all 1s or 0s + BinateSelect)
		SoPLA * SingleOutputComplement(SoPLA * fd);						// complutes the comlement of a Single-output function
		SoPLA * ExtractOnsetAndDcSet(PLA * pla, int i, int dc_man);		// return the OnSet (and DCset - depends on dc_man) of i-th output function
		int JoinInd(string a, string b);
		bool IsUnate(SoPLA * pla);										// says whether given SoPLA is unate or not
		bool containment;												// settings for MergeWithContainment function
		bool merge_shared;												// says whether equal terms contained in several output functions should be merged
		bool verbose;													// verbose mode
		int time_limit;													// time limit for complement computing
		bool time_limit_exceeded;										// indicates that the time limit was exceeded
};

#endif













