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

#include "stdafx.h"

#define MAXLINE 10000

using namespace std;

#ifdef _MSC_VER
#pragma hdrstop
#endif

#include "myExcept.h"
#include "PLA_type.h"
#include "bitvector.h"
#include "Cube.h"
#include "SoPLA.h"
#include "Term.h"
#include "utils.h"
#include "TTree.h"
#include "PLA_operations.h"
#include "Complement.h"

#include "PLA.h"
#include <deque>

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

void PLA::Init(void)
{
    inps = 0;
    outs = 0;
    indexed = false;
    uniq = false;
	keep_TT = false;
}

PLA::PLA(void)
{
    Init();
}

PLA::PLA( const PLA *_pla )
{
    Init();
	inps = _pla->inps;
	outs = _pla->outs;
	type = _pla->type;
	inames = _pla->inames;
	onames = _pla->onames;
}

void PLA::setType(const PLA_type v)
{
    type = v;
}

void PLA::setType(const string v)
{
    type = PLA_type(v);
}

PLA::PLA( const unsigned int inp, const unsigned int out, const PLA_type _type )
{
    Init();
    inps = inp;
    outs = out;
    type = _type;
}

PLA::PLA( const unsigned int inp, const unsigned int out )
{
    Init();
    inps = inp;
    outs = out;
}

PLA::PLA(const list<Term>& _data, const PLA_type _type)
//      Data is copied
{
    Init();
    inps = _data.front().inputs();
    outs = _data.front().outputs();
    this->data = _data;
    this->type = _type;
}

PLA::PLA( const SoPLA &sopla )
//	Data is copied
{
	list<Cube>::const_iterator ti;
	Term t;

	Init();
	inps = sopla.inputs();
	outs = 1;
	if ( sopla.getType() ) {
		this->type = PLA_type("f");
		t.setOM("1");
	}
	else {
		this->type = PLA_type("r");
		t.setOM("0");
	}
	for ( ti = sopla.getConstDataRef().begin(); ti != sopla.getConstDataRef().end(); ++ti) {
		t.setCube(ti->getCube());
		this->AppendTerm(t);
	}
	this->inames = sopla.getINames();
	this->onames.push_back(sopla.getName());
}

/*PLA::~PLA(void)
{
	pthread_mutex_destroy(&OnSetLock);
	pthread_mutex_destroy(&OffSetLock);
	pthread_mutex_destroy(&DCSetLock);
}*/

void PLA::clear(void)
// Clears all the PLA, deallocates all the structures
{
	data.clear();
    indexed = false;
    F.clear();
    D.clear();
    R.clear();
    inames.clear();
    onames.clear();
    TT.clear();
	indexterm.clear();
	inps = 0;
	outs = 0;
}

void PLA::setInputs( unsigned int v )
{
//	if ( inps != 0 && inps != v ) throw RuntimeException("PLA::SetInputs: Changing the number of PLA inputs");
	inps = v;
}

void PLA::setOutputs( unsigned int v )
{
	if ( outs != 0 && outs != v ) throw RuntimeException("PLA::SetOutputs: Changing the number of PLA outputs");
	outs = v;
}

TermList::iterator PLA::AppendTerm( const Term &t )
// Appends a term to the PLA. Returns the iterator pointing to this term
{
    TTreeNode *node;
	TermList::iterator ti;
	unsigned int i;

	if ( inps == 0 && outs == 0 ) {
		inps = t.inputs();
		outs = t.outputs();
	}
	else if ( inps != t.inputs() || outs != t.outputs() ) throw RuntimeException( "PLA::AppendTerm: incompatible terms" );
	
	if ( !uniq ) {
        data.push_back(t);
		ti = data.end();
		--ti;
		if ( indexed ) {
			indexterm.push_back(ti);
			ti->setIndex( data.size()-1 );
		}
        return ti;
    } else {
        node = TT.InsertTerm( t.getCube() );
		if ( node->IsTerm() ) {
			ti = node->getTerm();
			for ( i = 0; i < this->outs; i++)
				if ( t.isOM_1(i) ) ti->setOM_1(i);
			ti->origin |= t.origin;
			return ti;
		}
        else {
            data.push_back(t);
			ti = data.end();
			--ti;
			if ( indexed ) {
				indexterm.push_back(ti);
				ti->setIndex( data.size()-1 );
			}
            node->SetTerm(ti);
            if ( TT.getTerms() != data.size() && !keep_TT ) throw RuntimeException( "PLA:AppendTerm: Inconsistency between PLA and TT" );
            return ti;
        }
    }
}

list<Term>::iterator PLA::AppendTerm( const string iv, const string ov )
// Creates and appends the term. Returns the iterator pointing to this term
{
	Term t;

	t.setCube(iv);
	t.setOM(ov);
	return AppendTerm(t);		// consistency check is performed here
}

void PLA::AppendPLA(const PLA &_pla)
// appends a given PLA to this. The terms are copied.
{
	TermList::const_iterator ti;
	
	for ( ti = _pla.data.begin(); ti != _pla.data.end(); ++ti )
		AppendTerm(*ti);	// consistency check is performed here
}

void PLA::AppendTermList( const TermList &terms )
// appends a given list of terms to this. The terms are copied.
{
	TermList::const_iterator ti;

	for ( ti = terms.begin(); ti != terms.end(); ++ti )
		AppendTerm(*ti);
}

void PLA::Splice(PLA &_pla)
// appends a given PLA to this, the argument PLA is emptied
{
	TermList::iterator ti, ti1;
	TTreeNode *node;
	unsigned int i, j;

	if ( inps == 0 && outs == 0 ) {
		inps = _pla.inputs();
		outs = _pla.outputs();
	}
	else if ( inps != _pla.inputs() || outs != _pla.outputs() ) throw RuntimeException( "PLA::Splice: incompatible PLAs" );

	if ( !data.empty() ) {
		ti = data.end();
		--ti;
	}
	j = data.size();
	data.splice(data.end(), _pla.data);

	if ( uniq ) {
		if ( j != 0 ) ++ti;
		else ti = data.begin();
		while ( ti != data.end() ) {
			node = TT.InsertTerm( ti->getCube() );
			if ( node->IsTerm() ) {
				ti1 = node->getTerm();
				for ( i = 0; i < this->outs; i++)
					if ( ti->isOM_1(i) )
						ti1->setOM_1(i);
				ti1->origin |= ti->origin;
				ti = data.erase(ti);
			} else {
				node->SetTerm(ti);
				if ( indexed ) ti->setIndex(j++);
				++ti;
			}
		}
	} else if ( indexed ) {
		if ( j != 0 ) ++ti;
		else ti = data.begin();
		while ( ti != data.end() ) {
			(*ti).setIndex(j++);
			++ti;
		}
	}
	_pla.indexed = false;
}

void PLA::Splice( TermList &terms )
// appends a given list of terms to this, the argument list is emptied
{
	if ( inps == 0 && outs == 0 && !terms.empty()) {
		inps = terms.front().inputs();
		outs = terms.front().outputs();
	}
	else if ( inps != terms.front().inputs() || outs != terms.front().outputs() ) throw RuntimeException( "PLA::Splice: incompatible PLAs" );

	data.splice(data.end(), terms);
}

TermList::iterator PLA::DeleteTerm(const TermList::iterator ti)
// Deletes a term pointed by an iterator. Returns an iterator to the next term
{
	indexed = false;
	if ( uniq ) {
		if ( !keep_TT ) {
			if ( !TT.DeleteTerm( ti->getCube() ) ) throw RuntimeException( "PLA::DeleteTerm: Inconsistency between PLA and TT. Deleting term which is not in TT." );;
			if ( TT.getTerms() != data.size()-1 ) throw RuntimeException( "PLA::DeleteTerm: Inconsistency between PLA and TT" );
		}
		else if ( !TT.DeleteTerm_Keep( ti->getCube() ) ) throw RuntimeException( "PLA::DeleteTerm: Inconsistency between PLA and TT. Deleting term which is not in TT." );;
	}
    return data.erase(ti);
}

void PLA::NameVars(void)
// Names the PLA variables (x, y), if the names are missing
{
    unsigned int i;
    stringstream ss;
	string s;
    
    if ( inames.empty() )
      for ( i = 0; i < inps; i++ ) {
        ss.clear();
        ss << "x" << i;
		ss >> s;
        inames.push_back(s);
      }
    if ( onames.empty() )
      for ( i = 0; i < outs; i++ ) {
        ss.clear();
        ss << "y" << i;
		ss >> s;
        onames.push_back(s);
      }
}

void PLA::Reindex(void)
// Reindexes the PLA, if not indexed
{
    list<Term>::iterator ti;
    unsigned int i = 0;

    if ( indexed ) return;
	indexterm.clear();
	for ( ti = data.begin(); ti != data.end(); ++ti ) {
        indexterm.push_back(ti);
		ti->setIndex(i++);
	}
    indexed = true;
}

void PLA::LoadPLA( const char *fn )
// clears the PLA structure and loads a PLA from a file
{
    unsigned int pos;
    ifstream f;
    string s, s1;
    char line[MAXLINE];
    Term t;
    unsigned int p = 0;
    unsigned int i;

    this->clear();

    f.open(fn);
    if (!f.is_open()) throw IOException( "Cannot open file: " + string(fn) );

    while ( !f.eof() ) {
        f.getline(line, MAXLINE);
        pos = 0;
        if ( line[0] == '#' ) continue;
        if ( line[0] == '.' ) {
           s = GetToken(line, pos);
           if ( s == ".i" ) {
                s = GetToken(line, pos);
                inps = atoi(s.c_str());
                if ( inps == 0 ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
           } else if ( s == ".o" ) {
                s = GetToken(line, pos);
                outs = atoi(s.c_str());
                if ( inps == 0 ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
           } else if ( s == ".p" ) {
                s = GetToken(line, pos);
                p = atoi(s.c_str());
                if ( inps == 0 ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
           } else if ( s == ".ilb" ) {
				s = GetToken(line, pos);
                while ( !s.empty() ) {
                    inames.push_back(s);
                    s = GetToken(line, pos);
                }
           } else if ( s == ".ob" ) {
				s = GetToken(line, pos);
                while ( !s.empty() ) {
                    onames.push_back(s);
                    s = GetToken(line, pos);
                }
           } else if ( s == ".type" ) {
                s = GetToken(line, pos);
                for ( i = 0; i < s.length(); i++ )
                    if ( s[i] == 'f' ) type.f = true;
                    else if ( s[i] == 'd' ) type.d = true;
                    else if ( s[i] == 'r' ) type.r = true;
                    else throw IOException( "Bad or damaged PLA file: " + string(fn) );
                
           } else if ( s == ".e" || s == ".end" ) { break;
           } else throw IOException( "Bad or damaged PLA file: " + string(fn) );
        } else {
            s = GetToken(line, pos);
            if ( s.length() != 0 ) {
              if ( s.length() != inps ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
              if ( !(type.f || type.d || type.r) ) {
					type.f = true;
					type.d = true;
			  }
			  s1.clear();
              for ( i = 0; i < inps; i++ )
                  if ( s[i] == '0' || s[i] == '1' ) s1 += s[i];
                  else if ( s[i] == '-' || s[i] == '2' ) s1 += '-';
                  else throw IOException( "Bad or damaged PLA file: " + string(fn) );

              t.setCube(s1);

			  do {							// for a case of output vectors being on a separate line
				  s = GetToken(line, pos);
				  if ( s.empty() ) {
					  f.getline(line, MAXLINE);
					  pos = 0;
				  }
			  } while ( s.empty() && !f.eof() );
              if ( s.length() != outs ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
              s1.clear();
			  for ( i = 0; i < outs; i++ ) {
				  if ( s[i] == '2' ) s[i] = '-';
				  else if ( s[i] == '3' ) s[i] = '~';
				  else if ( s[i] == '4' ) s[i] = '1';
				  if ( s[i] == '~' ) s1 += '~';
				  else if ( s[i] == '1' && type.f ) s1 += '1';
				  else if ( s[i] == '0' && type.r ) s1 += '0';
				  else if ( s[i] == '-' && type.d ) s1 += '-';
				  else if ( s[i] == '1' && !type.f ) s1 += '~';
				  else if ( s[i] == '0' && !type.r ) s1 += '~';
				  else if ( s[i] == '-' && !type.d ) s1 += '~';
                  else throw IOException( "Bad or damaged PLA file: " + string(fn) );
			  }
              t.setOM(s1);
              AppendTerm(t);
            }
        }
    }
    if ( p != 0 && p != data.size() ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
	if ( !inames.empty() && inames.size() != inps ) throw IOException( "Bad or damaged PLA file: " + string(fn) );
	if ( !onames.empty() && onames.size() != outs ) throw IOException( "Bad or damaged PLA file: " + string(fn) );

    f.close();
}

void PLA::SavePLA( const char *fn ) const
// Saves the PLA
{
    ofstream f;
    Term t;
    list<Term>::const_iterator ti;
    unsigned int i;
    string s;

    f.open(fn);
    if (!f.is_open()) throw IOException( "Cannot create a file: " + string(fn) );

	f << ".i " << inps << endl;
    f << ".o " << outs << endl;
    f << ".p " << data.size() << endl;
    f << ".type ";
    if ( type.f ) f << "f";
    if ( type.d ) f << "d";
    if ( type.r ) f << "r";
    f << endl;

    if ( !inames.empty() ) {
        f << ".ilb";
        for ( i = 0; i < inps; i++ ) {
            f << " " << inames[i];
        }
        f << endl;
    }
    if ( !onames.empty() ) {
        f << ".ob";
        for ( i = 0; i < outs; i++ )
            f << " " << onames[i];
        f << endl;
    }
    for ( ti = data.begin(); ti != data.end(); ++ti )
        f << (*ti).getCube() << " " << (*ti).getOM() << endl;
    f << ".e" << endl;

    f.close();
}

void PLA::SaveVHDL( const char *fn )
// Saves the on-set only. Others are ignored
// The entitity name is extracted from the filename
// PLA is indexed
{
    ofstream f;
    Term t;
    list<Term>::iterator ti;
    unsigned int i;
    string s, s1;
    bool beg;

    if ( !type.f ) throw RuntimeException( "On-set is not specified. Cannot export to VHDL." );
    this->NameVars();
    this->Reindex();
    f.open(fn);
    if (!f.is_open()) throw IOException( "Cannot create a file: " + string(fn) );
    f << "library IEEE;" << endl;
    f << "use IEEE.std_logic_1164.all;" << endl << endl;
    s = fn;
    s1 = s.substr(0, s.find(".", 1));
    f << "entity " << s1 << " is" << endl;
    f << "   port( ";
    for ( i = 0; i < inps; i++ ) {
        if ( i != 0 ) f << ", ";
        f << inames[i];
    }
    f << ": in std_logic;" << endl;
    f << "         ";
    for ( i = 0; i < outs; i++ ) {
        if ( i != 0 ) f << ", ";
        f << onames[i];
    }
    f << ": out std_logic);" << endl;
    f << "end " << s1 <<";" << endl << endl;

    f << "architecture PLA of " << s1 << " is" << endl;
    f << "   signal ";
    for ( i = 0; i < data.size(); i++ ) {
        if ( i != 0 ) f << ", ";
        f << "t_" << i;
    }
    f << ": std_logic;" << endl;
    f << "   signal ";
    for ( i = 0; i < inps; i++ ) {
        if ( i != 0 ) f << ", ";
        f << "n_" << inames[i];
    }
    f << ": std_logic;" << endl << endl;

    f << "begin" << endl;
    for ( i = 0; i < inps; i++ )
        f << "   n_" << inames[i] << " <= not " << inames[i] << ";" << endl;
    f << endl;
    for ( ti = data.begin(); ti != data.end(); ++ti ) {
        f << "   t_" << this->getIndex(ti) << " <= ";
        beg = true;
        for ( i = 0; i < inps; i++ )
            if ( !(*ti).isLit_dc(i) ) {
                if ( !beg ) f << " and ";
                beg = false;
                if ( (*ti).isLit_1(i) ) f << inames[i];
                else f << "n_" << inames[i];
            }
        f << ";" << endl;

    }
    f << endl;
    for ( i = 0; i < outs; i++ ) {
        f << "   " << onames[i] << " <= ";
        beg = true;
        for ( ti = data.begin(); ti != data.end(); ++ti ) {
            if ( (*ti).isOM_1(i) ) {
               if ( !beg ) f << " or ";
               beg = false;
               f << "t_" << this->getIndex(ti);
            }
        }
        f << ";" << endl;
    }
    f << "end PLA;" << endl;
    f.close();
}

unsigned int PLA::getLiterals(void)
// Returns the number of PLA literals
{
    unsigned int l = 0;
    list<Term>::iterator ti;

    for ( ti = data.begin(); ti != data.end(); ++ti )
        l += inps-(*ti).getDim();
    return l;
}

unsigned int PLA::getOC(void) const
// returns the PLA output cost
{
    unsigned int l = 0;
    list<Term>::const_iterator ti;

    for ( ti = data.begin(); ti != data.end(); ++ti )
        l += (*ti).getOC();
    return l;
}

unsigned int PLA::getGEs(void)
// Returns GEs*2
{
	unsigned int ge = 0;
	list<Term>::iterator ti;
	unsigned int i;
	bool flag;
	
	for ( ti = data.begin(); ti != data.end(); ++ti )
		if ( inps-ti->getDim() > 1 ) ge += inps-ti->getDim();
	ge += getOC();
	for ( i = 0; i < outs; i++ ) {
		flag = false;
		for ( ti = data.begin(); ti != data.end(); ++ti )
			if ( ti->isOM_1(i) ) {
				if ( !flag ) flag = true;
				else break;
			}
		if ( flag && ti == data.end() ) ge--;
	}
	return ge;
}

SoPLA *PLA::getOnSet( const unsigned int output )
// Returns a pointer to the given ON-set. If not present, it is computed (even by complementing)
{
	if ( output >= outs ) throw RuntimeException( "PLA::getOnSet: Wrong output index" );
	if ( F.empty() ) GenerateOnSet(output);
	else if ( F[output].getData()->empty() ) GenerateOnSet(output);
    return &F[output];
}

SoPLA *PLA::getOffSet( const unsigned int output )
// Returns a pointer to the given OFF-set. If not present, it is computed (even by complementing)
{
	if ( output >= outs ) throw RuntimeException( "PLA::getOffSet: Wrong output index" );
    if ( R.empty() ) GenerateOffSet(output);
    else if ( R[output].getData()->empty() ) GenerateOffSet(output);
    return &R[output];
}

SoPLA *PLA::getDCSet(const unsigned int output)
// Returns a pointer to the given DC-set. If not present, it is computed (even by complementing)
{
	if ( output >= outs ) throw RuntimeException( "PLA::getDCSet: Wrong output index" );
    if ( D.empty() ) GenerateDCSet(output);
    else if ( D[output].getData()->empty() ) GenerateDCSet(output);
    return &D[output];
}

void PLA::GenerateOnSet(const unsigned int output)
// Generates the given ON-set. If not present, it is computed (even by complementing)
{
    list<Term>::iterator ti;
	SoPLA rest;
	SoPLA *complement;
	//cout << "onset lock" << endl;
	//pthread_mutex_lock(&OnSetLock);
	if ( output >= outs ) throw RuntimeException( "PLA::GenerateOnSet: Wrong output index" );
	if ( !F.empty() && F.size() != outs ) throw RuntimeException( "PLA::GenerateOnSet: Wrong on-set size" );
    if ( F.empty() ) F.resize( outs );
    F[output].clear();
	if ( !type.f ) {
		if ( !type.r && !type.d ) throw RuntimeException( "PLA::GenerateOnSet: Cannot generate" );
		if ( type.r ) rest.AppendPLA(*getOffSet(output));
		if ( type.d ) rest.AppendPLA(*getDCSet(output));
//		complement = PLA_op().Sharp_Complement(rest);
		complement = Complement().PLAComplement(&rest);
		F[output].Splice(*complement->getData());
		delete complement;
	}
	else for ( ti = data.begin(); ti != data.end(); ++ti )
        if ( ti->isOM_1(output) ) F[output].AppendTerm(ti->getCube());
	//pthread_mutex_unlock(&OnSetLock);
}

void PLA::GenerateOffSet( const unsigned int output)
// Generates the given OFF-set. If not present, it is computed (even by complementing)
{
    list<Term>::iterator ti;
	SoPLA rest;
	SoPLA *complement;
	//cout << "offset lock" << endl;
	//pthread_mutex_lock(&OffSetLock);
	if ( output >= outs ) throw RuntimeException( "PLA::GenerateOffSet: Wrong output index" );
	if ( !R.empty() && R.size() != outs ) throw RuntimeException( "PLA::GenerateOffSet: Wrong off-set size" );
	if ( R.empty() ) R.resize( outs );
    R[output].clear();
	if ( !type.r ) {
		if ( !type.f && !type.d ) throw RuntimeException( "PLA::GenerateOffSet: Cannot generate" );
		if ( type.f ) rest.AppendPLA(*getOnSet(output));
		if ( type.d ) rest.AppendPLA(*getDCSet(output));
//		complement = PLA_op().Sharp_Complement(rest);
		complement = Complement().PLAComplement(&rest);
		R[output].Splice(*complement->getData());
		delete complement;
	}
    else for ( ti = data.begin(); ti != data.end(); ++ti )
        if ( ti->isOM_0(output) ) R[output].AppendTerm(ti->getCube());
	//pthread_mutex_unlock(&OffSetLock);
}

void PLA::GenerateDCSet( const unsigned int output)
// Generates the given DC-set. If not present, it is computed (even by complementing)
{
    list<Term>::iterator ti;
	SoPLA rest;
	SoPLA *complement;
	//cout << "dcset lock" << endl;
	//pthread_mutex_lock(&DCSetLock);
	if ( output >= outs ) throw RuntimeException( "PLA::GenerateDCSet: Wrong output index" );
	if ( !D.empty() && D.size() != outs ) throw RuntimeException( "PLA::GenerateDCSet: Wrong dc-set size" );
    if ( D.empty() ) D.resize( outs );
	D[output].clear();
	if ( !type.d ) {
		if ( !type.f && !type.r ) throw RuntimeException( "PLA::GenerateDCSet: Cannot generate" );
		if ( type.f ) rest.AppendPLA(*getOnSet(output));
		if ( type.r ) rest.AppendPLA(*getOffSet(output));
//		complement = PLA_op().Sharp_Complement(rest);
		complement = Complement().PLAComplement(&rest);
		D[output].Splice(*complement->getData());
		delete complement;
	}
	else for ( ti = data.begin(); ti != data.end(); ++ti )
		if ( ti->isOM_dc(output) ) D[output].AppendTerm(ti->getCube());
	//pthread_mutex_unlock(&DCSetLock);
}

bool PLA::isImplicantNoOMCheck( const Term& t, const unsigned int output )
/*
    Returns true if t is an implicant of PLA.
*/
{
    list<Cube>::const_iterator ti;
//	SoPLA *to_taut;
	SoPLA FD;

	if ( t.inputs() != inps ) throw RuntimeException( "PLA::isImplicantNoOMCheck: Comparing terms of different sizes" );
    if ( R.empty() ) GenerateOffSet( output );
        else if ( R[output].empty() ) GenerateOffSet( output );
	for ( ti = R[output].getData()->begin(); ti != R[output].getData()->end(); ++ti )
		if ( ti->Cube::intersects(t) ) return false;
	
		// for tautology generation only
/*
	int i = 0;
	FD.AppendPLA(*getOnSet(output));
	FD.AppendPLA(*getDCSet(output));
	to_taut = Cofactor(FD, t);
	to_taut->RemoveAbsorbed();
	if ( to_taut->getTerms() > 1000 ) {
		PLA *pla = new PLA(*to_taut);
		pla->SavePLA("tautology.pla");
		delete pla;
	}
*/
	return true;
}

bool PLA::isImplicant( const Term& t, const unsigned int output )
/*
    Returns true if t is an implicant of PLA.
    If t.OM[output] is 0, returns false
*/
{
    if ( t.isOM_0(output) ) return false;
	return isImplicantNoOMCheck( t, output );
}

bool PLA::isImplicant( const Term& t )
/*
    Returns true if t is an implicant of the PLA for all outputs set to '1'.
*/
{
	unsigned int i;

	for ( i = 0; i < outs; i++ )
		if ( t.isOM_1(i) )
			if ( !isImplicantNoOMCheck(t, i) ) return false;
	return true;
}

void PLA::setUnique(void)
// Sets the "unique" attribute. TT is created and being updated during term insertion
{
	TermList::const_iterator ti;

	if ( uniq ) return;
	uniq = true;
    TT.setInputs( inps );
	for ( ti = data.begin(); ti != data.end(); ++ti )
		TT.InsertTerm( ti->getCube() );
}

void PLA::setNonUnique(void)
// Unsets the "unique" attribute. TT is cleared
{
	uniq = false;
	TT.clear();
}

void PLA::ToF(void)
// Converts PLA to F-type. DC-set is discarded
{
	TermList::iterator ti;
	unsigned int i;

	for ( ti = data.begin(); ti != data.end(); ++ti )
		for ( i = 0; i < outs; i++ )
			if ( !ti->isOM_1(i) ) ti->setOM_undef(i);
}

list<Term>::iterator PLA::getTermByIndex( const unsigned int i )
// Returns an iterator to an indexed term. If not indexed, Reindex is called
{
	if ( !indexed ) Reindex();
	return indexterm[i];
}

void PLA::Purge(void)
// Deletes terms marked as "unwanted"
{
	TermList::iterator ti;

	ti = data.begin();
	while ( ti != data.end() ) 
		if ( ti->unwanted ) ti = this->DeleteTerm(ti);
		else ++ti;
}

unsigned int PLA::getIndex( const list<Term>::iterator ti )
// Returns index of a term pointed by an iterator
{
	if ( !indexed ) Reindex();
	return ti->getIndex();
}

void PLA::MergeTerms(void)
// Merges terms having equal input matrices, joins output matrices
{
    list<Term>::iterator ti1, ti2;

	if ( type.r ) throw RuntimeException("PLA::MergeTerms:: r-type PLA cannot be processed");
    if ( data.size() < 2 ) return;
	for ( ti1 = data.begin(); ti1 != data.end(); ++ti1 ) {
       ti2 = ti1;
       do {
            ti2++;
            if ( ti2 == data.end() ) break;
       } while ( ti1->getCube() != ti2->getCube() );
       if ( ti2 != data.end() ) {
            ti1->Merge(*ti2);
            DeleteTerm(ti2);
       }
    }
}

void PLA::MergeNeighbors(void)
/*
    Repetitively merges neighboring terms (terms differing in one variable only and having equal OM)
*/
{
    list<Term>::iterator ti1, ti2;
    int diff;
    unsigned int i;
	bool dirty;

	if ( data.size() < 2 ) return;
	ti1 = data.begin();
	do {
		dirty = false;
		ti2 = ti1;
		ti2++;
		if ( ti2 == data.end() ) return;
		do { 
			if ( ti1->getOM() == ti2->getOM() ) {
			   diff = -1;
			   for ( i = 0; i < inps; i++ )
				   if ( ti1->getLit(i) != ti2->getLit(i) && (ti1->isLit_dc(i) || ti2->isLit_dc(i) )) break;
				   else if ( ti1->getLit(i) != ti2->getLit(i) &&  diff == -1 ) diff = i;
				   else if ( ti1->getLit(i) != ti2->getLit(i) &&  diff != -1 ) break;
			   if ( i == inps && diff != -1 ) {
				   ti1->setLit_dc(diff);
				   DeleteTerm(ti2);
				   ti1 = data.begin();
				   dirty = true;
				   break;
			   } else ++ti2;
			} else ++ti2;
		} while ( ti2 != data.end() );
		if ( !dirty ) ++ti1;
	} while ( ti1 != data.end() );
}

/*void PLA::RemoveAbsorbed(void)
// Removes absorbed terms
{
    TermList::iterator ti, ti1;
	bool deleted;
	if ( data.size() < 2 ) return;
	ti = data.begin();
	do {
		ti1 = ti;
		++ti1;
		deleted = false;
		while ( ti1 != data.end() ) {
			if ( ti->contains( *ti1 ) ) ti1 = DeleteTerm(ti1);
			else if ( ti1->contains( *ti ) ) {
				ti = DeleteTerm(ti);
				deleted = true;
				break;
			} else ++ti1;
		}
		if ( !deleted ) ++ti;
	} while ( ti != data.end() );
}*/

void PLA::RemoveAbsorbed(void)
	// Removes absorbed terms
{
	TermList::iterator ti;
	if ( data.size() < 2 ) return;
	vector<Term *> v;
	v.reserve(data.size());
	for (ti = data.begin(); ti != data.end(); ++ti)
		v.push_back(&(*ti));
	int n = v.size(), i, j;
	#pragma omp parallel for default(none) schedule(static, 10) \
	shared(v, n) private(i, j)
	for (i = 0; i < n; i++) {
		if (v[i]->invalid()) continue;
		for (j = i + 1; j < n; j++) {
			if (v[i]->invalid()) break;
			if (v[j]->invalid()) continue;
			if (v[i]->contains(*v[j]))
				v[j]->invalidate();
			else if (v[j]->contains(*v[i])) {
				v[i]->invalidate();
				break;
			}
		}
	}
	for (i = 0, ti = data.begin(); i < n && ti != data.end(); ++i)
		if (v[i]->invalid()) ti = DeleteTerm(ti);
		else ++ti;
}

void PLA::RemoveAbsorbed(TermQueue * in, TermQueue * tq_rabc)
	// Removes absorbed terms
{
	Term t;
	TermList::iterator ti, ti1;
	bool deleted;
	deque<Term *> d;
	int n, i;
	while (true) {
		in->pop(t);
		if (t.invalid()) break;
		deleted = false;
		n = d.size();
		#pragma omp parallel for default(none) \
			shared(n, d, deleted, t) private(i)
		for (i = 0; i < n; i++) {
			#pragma omp flush(deleted)
			if (!deleted) {
				if (d[i]->isUnwanted())
					continue;
				if (t.contains(*d[i])) {
					d[i]->setUnwanted();
				} else if (d[i]->contains(t)) {
					deleted = true;
					#pragma omp flush(deleted)
				}
			}
		}
		if (!deleted) {
			ti = AppendTerm(t);
			d.push_back(&(*ti));
		}
	}
	for (i = 0, ti = data.begin(); i < n && ti != data.end(); i++)
		if (d[i]->isUnwanted()) ti = DeleteTerm(ti);
		else ++ti;
	/*Term t;
	TermList::iterator ti, ti1;
	bool deleted;
	while (true) {
		in->pop(t);
		if (t.invalid()) break;
		deleted = false;
		for (ti = data.begin();	ti != data.end(); ) {
			if (t.contains(*ti)) {
				ti = DeleteTerm(ti);
				continue;
			} else if (ti->contains(t)) {
				deleted = true;
				break;
			}
			++ti;
		}
		if (!deleted) {
			AppendTerm(t);
			if (!useIR)
				tq_rabc->push(t);
		}
	}*/
	/*	if ( data.size() < 2 ) return;
		ti = data.begin();
		do {
			ti1 = ti;
			++ti1;
			deleted = false;
			while ( ti1 != data.end() ) {
				if ( ti->contains( *ti1 ) ) ti1 = DeleteTerm(ti1);
				else if ( ti1->contains( *ti ) ) {
					ti = DeleteTerm(ti);
					deleted = true;
					break;
				} else ++ti1;
			}
			if ( !deleted ) ++ti;
		} while ( ti != data.end() );
	}*/
}

list<Term>::iterator PLA::FindTerm( const string t )
// finds a term with equal IM. If not found, returns data.end();
// first occurence is considered
{
	TermList::iterator ti;

	for ( ti = data.begin(); ti != data.end(); ++ti )
		if ( ti->getCube() == t ) break;
	return ti;
}

string PLA::getIName(const unsigned int i) const
// Returns a given input name
{
	if ( inames.empty() ) return "";
	else if ( i >= inames.size() ) throw RuntimeException( "PLA::getIName: Wrong name index" );
	else return inames[i];
}

string PLA::getOName(const unsigned int i) const
// Returns a given output name
{
	if ( onames.empty() ) return "";
	else if ( i >= onames.size() ) throw RuntimeException( "PLA::getOName: Wrong name index" );
	else return onames[i];
}

void PLA::setIName(const unsigned int i, const string name)
// Sets an input name
{
	if ( inames.empty() ) inames.resize( inps, "" );
	else if ( i >= inps || inames.size() != inps ) throw RuntimeException( "PLA::setIName: Incorrect index" );
	inames[i] = name;
}

void PLA::setOName(const unsigned int i, const string name)
// Sets an output name
{
	if ( onames.empty() ) onames.resize( outs, "" );
	else if ( i >= outs || onames.size() != outs  ) throw RuntimeException( "PLA::setOName: Incorrect index" );
	onames[i] = name;
}

void PLA::RemoveUselessTerms()
// Removes terms having all ~ in the output matrix
{
	TermList::iterator ti;
	unsigned int i;

	ti = data.begin();
	do {
		for ( i = 0; i < outs; i++ )
			if ( !ti->isOM_undef(i) ) break;
		if ( i == outs )
			ti = this->DeleteTerm(ti);
		else ++ti;
	} while ( ti != data.end() );
}

void PLA::ClearData()
	// deletes all terms, but they remain in the (possible) TT.
	// not functionous because of keepTT problems!
{
	data.clear();
	indexterm.clear();
	TT.clear();
}

void PLA::StripNames(void)
	// removes the names
{
	inames.clear();
	onames.clear();
}

bool PLA::empty(void) const
{
	return ( data.empty() );
}

SoPLA *PLA::ToSoPLA( const unsigned int out, const bool _type ) const
// Generates SoPLA from one PLA output.
{
	SoPLA *res;
	TermList::const_iterator ti;

	if ( _type && !type.f ) throw RuntimeException("PLA::ToSoPLA: SoPLA cannot be generated" );
	if ( !_type && !type.r ) throw RuntimeException("PLA::ToSoPLA: SoPLA cannot be generated" );
	res = new SoPLA(this->inps, _type);
	for ( ti = data.begin(); ti != data.end(); ++ti ) 
		if ( !ti->isOM_undef(out) ) {
			if ( ti->isOM_dc(out) ) throw RuntimeException("PLA::ToSoPLA: incompletely specified function");
			else if ( (ti->isOM_1(out) && res->getType()) || (ti->isOM_0(out) && !res->getType()) ) res->AppendTerm(ti->getCube()); 
		}
	if ( !inames.empty() ) res->setINames(inames);
	if ( !onames.empty() ) res->setName(onames[out]);

	return res;
}

SoPLA *PLA::ToSoPLA( const unsigned int out ) const
// Generates SoPLA for one PLA output.
{
	SoPLA *res;
	string s;

	if ( this->type.f ) return ToSoPLA( out, true );
	else if ( this->type.r ) return ToSoPLA( out, false );
	else if ( data.empty() ) {
		res = new SoPLA(this->inps, false);
		s.assign(inputs(), '-');
		res->AppendTerm(s);
		res->setType(false);
		res->setINames(this->getINames());
		res->setName(this->getOName(out));
		return res;
	} else throw RuntimeException("PLA::ToSoPLA: SoPLA cannot be generated" );
}

void PLA::RemoveAllDCCols(void)
{
	list<Term>::iterator ti;
	unsigned int i;
	vector<bool> alldc;
	unsigned int cnt = 0;
	vector<Literal> new_IM;
	vector<string> new_names;
	string old_OM;

	if ( data.empty() ) return;
	alldc.resize( inps, false );
	for ( i = 0; i < inps; i++ ) {
		for ( ti = data.begin(); ti != data.end(); ++ti )
			if ( !ti->isLit_dc(i) ) break;
		if ( ti == data.end() ) {
			alldc[i] = true;
			cnt++;
		}
	}
	if ( cnt == 0 ) return;
	if ( cnt != this->inputs() ) {
		for ( ti = data.begin(); ti != data.end(); ++ti ) {
			new_IM.clear();
			for ( i = 0; i < inps; i++ )
				if ( !alldc[i] ) new_IM.push_back( ti->getLit2(i) );
			old_OM = this->getData()->front().getOM();
			ti->clear();
			ti->setCube(new_IM);
			ti->setOM( old_OM );
			if ( ti->dim != -1 ) ti->dim -= cnt;
		}
		new_names.clear();
		for ( i = 0; i < inps; i++ )
			if ( !alldc[i] ) new_names.push_back( inames[i] );
		inames = new_names;
		setInputs( inputs()-cnt );
	}
	else {				// for const 0 or 1
		old_OM = this->getData()->front().getOM();
		ClearData();
		this->inames.clear();
		setInputs(1);
		AppendTerm("-", old_OM);
	}
	F.clear();
	D.clear();
	R.clear();
	TT.clear();
}

int PLA::FindIName( const string name ) const
// returns index of the name, or -1, if not found
{
	unsigned int i;

	if ( inames.empty() ) return -1;
	for ( i = 0; i < inps; i++ )
		if ( getIName(i) == name ) return i;
	return -1;
}

int PLA::FindOName( const string name ) const
// returns index of the name, or -1, if not found
{
	unsigned int i;

	if ( onames.empty() ) return -1;
	for ( i = 0; i < outs; i++ )
		if ( getOName(i) == name ) return i;
	return -1;
}

bool PLA::emptyNames(void) const
{
	return inames.empty();
}

bool PLA::isConsistent(void)
// is the PLA consistent? (doesn't the on-set intersect the off-set?)
{
	unsigned int i;
	list<Cube> *on, *off;
	list<Cube>::iterator it1, it2;

	for ( i = 0; i < outs; i++ ) {
		on = this->getOnSet(i)->getData();
		off = this->getOffSet(i)->getData();
		for ( it1 = on->begin(); it1 != on->end(); ++it1 )
			for ( it2 = off->begin(); it2 != off->end(); ++it2 )
				if ( it1->intersects(*it2) ) return false;
	}
	return true;
}

void PLA::Sort(void)
// sorts the PLA lexicographically, by input and output names
{
	unsigned int i, j;
	list<string> name_list;
	list<string>::iterator name_list_it;
	PLA backup;
	TermList::iterator it1, it2;

	if ( inames.size() > 1 || onames.size() > 1 ) {
		TT.clear();
		F.clear();
		D.clear();
		R.clear();
	}

	if ( inames.size() > 1 ) {
		for ( i = 0; i < this->inps; i++ ) name_list.push_back(inames[i]);
		name_list.sort();
			// isn't it already sorted?
		i = 0;
		for ( name_list_it = name_list.begin(); name_list_it != name_list.end(); ++name_list_it )
			if ( *name_list_it != inames[i++] ) break;
		if ( name_list_it != name_list.end() ) {		// reorder
			backup = *this;
			i = 0;
			for ( name_list_it = name_list.begin(); name_list_it != name_list.end(); ++name_list_it ) {
				if ( *name_list_it != inames[i] ) {
					this->inames[i] = *name_list_it;
					// find old position
					for ( j = 0; j < inps; j++ )
						if ( *name_list_it == backup.inames[j] ) break;
					it1 = this->data.begin();
					for ( it2 = backup.data.begin(); it2 != backup.data.end(); ++it2 ) {
						it1->setLit(i, it2->getLit2(j));
						++it1;
					}
				}
				i++;
			}
		}
	}

	if ( onames.size() > 1 ) {
		for ( i = 0; i < this->outs; i++ ) name_list.push_back(onames[i]);
		name_list.sort();
			// isn't it already sorted?
		i = 0;
		for ( name_list_it = name_list.begin(); name_list_it != name_list.end(); ++name_list_it )
			if ( *name_list_it != onames[i++] ) break;
		if ( name_list_it != name_list.end() ) {		// reorder
			if ( backup.inps == 0 ) backup = *this;		// make backup, if it already wasn't made
			i = 0;
			for ( name_list_it = name_list.begin(); name_list_it != name_list.end(); ++name_list_it ) {
				if ( *name_list_it != onames[i] ) {
					this->onames[i] = *name_list_it;
					// find old position
					for ( j = 0; j < outs; j++ )
						if ( *name_list_it == backup.onames[j] ) break;
					it1 = this->data.begin();
					for ( it2 = backup.data.begin(); it2 != backup.data.end(); ++it2 ) {
						it1->setOM(i, it2->getOM(j));
						++it1;
					}
				}
				i++;
			}
		}
	}
}

void PLA::MergePLAs( const PLA &_pla )
// merges two PLAs, regardless their numbers of inputs, outputs, terms. If possible, inputs are matched by input names.
// If input names are not present, different variables are considered
// If only one of the PLAs has names defined, no names will be present (there's no better way)
{
	unsigned int i, i_last = 0, o_last = 0, i_last1, o_last1;
	int pos;
	PLA old;

	old = *this;
	this->clear();
	Term *t;
	TermList::const_iterator ti;

	// create new names
	if ( !old.inames.empty() && !_pla.inames.empty() ) {
		inames = old.inames;
		this->inps = inames.size();
		for ( i = 0; i < _pla.inputs(); i++ )
			if ( this->FindIName(_pla.inames[i]) == -1 ) inames.push_back(_pla.inames[i]);
	}
	if ( !old.onames.empty() && !_pla.onames.empty() ) {
		onames = old.onames;
		this->outs = onames.size();
		for ( i = 0; i < _pla.outputs(); i++ )
			if ( this->FindOName(_pla.onames[i]) == -1 ) onames.push_back(_pla.onames[i]);
	}

	// derive numbers of inputs and outputs
	if ( !inames.empty() ) this->inps = inames.size();
	else this->inps = old.inputs() + _pla.inputs();
	if ( !onames.empty() ) this->outs = onames.size();
	else this->outs = old.outputs() + _pla.outputs();

	// construct data
	t = new Term(inps, outs);
	for ( ti = old.data.begin(); ti != old.data.end(); ++ti ) {
		t->assign(inps, DC);
		t->assignOM(outs, UNDEF);
		for ( i = 0; i < old.inputs(); i++ ) t->setLit(i, ti->getLit(i) );
		i_last = i;
		for ( i = 0; i < old.outputs(); i++ ) t->setOM(i, ti->getOM(i) );
		o_last = i;
		this->AppendTerm(*t);
	}
	for ( ti = _pla.data.begin(); ti != _pla.data.end(); ++ti ) {
		i_last1 = i_last;
		o_last1 = o_last;
		t->assign(inps, DC);
		t->assignOM(outs, UNDEF);
		for ( i = 0; i < _pla.inputs(); i++ ) {
			if ( !_pla.inames.empty() ) pos = this->FindIName(_pla.inames[i]);
			else pos = -1;
			if ( pos == -1 ) t->setLit( i_last1++, ti->getLit(i) );
			else t->setLit(pos, ti->getLit(i) );
		}
		for ( i = 0; i < _pla.outputs(); i++ ) {
			if ( !_pla.onames.empty() ) pos = this->FindOName(_pla.onames[i]);
			else pos = -1;
			if ( pos == -1 ) t->setOM( o_last1++, ti->getOM(i) );
			else t->setOM(pos, ti->getOM(i) );
		}
		this->AppendTerm(*t);
	}
	delete t;
	this->type += _pla.type;
	TT.clear();
	F.clear();
	D.clear();
	R.clear();
}

bool PLA::isConstant(void)
{
	unsigned int i;

	if ( this->empty() ) return true;
	if ( this->getTerms() > 1 ) return false;
	for ( i = 0; i < this->inputs(); i++ )
		if ( !this->getData()->front().isLit_dc(i) ) return false;
	return true;
}

void PLA::DumpOrigin( const char *fn ) const
// for debug purposes.
// Dumps origins of the terms into a file
{
	ofstream f;
	list<Term>::const_iterator ti1;

	f.open(fn);
	f << "CD-S; FC-Min; IE; IR" << endl;
	for ( ti1 = data.begin(); ti1 != data.end(); ti1++ )
		f << ((*ti1).origin & 1) << "; " << ((*ti1).origin & 2) << "; " << ((*ti1).origin & 4) << "; " << ((*ti1).origin & 8) << endl;
	f.close();
}
