#include "stdafx.h"

#ifdef _MSC_VER
#pragma hdrstop
#endif

using namespace std;

#include "kernelincludes.h"

#include "PLA_operations.h"

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

SoPLA *PLA_op::Sharp( const Cube& t1, const Cube& t2 )
/* performs t1 # t2
	I.e., returns a list of terms covered by t1 and not not by t2
*/
{
	unsigned int i;
	SoPLA *res;		// the result
	Cube newterm;
	string om;

	if ( t1.inputs() != t2.inputs() ) throw RuntimeException( "TermSharp: Different term sizes" );
	res = new SoPLA( t1.inputs() );
	if ( res == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
	if ( !t1.intersects(t2) ) {
		res->AppendTerm(t1);
		return res;
	}

	for ( i = 0; i < t1.inputs(); i++ )
		if ( t1.isLit_dc(i) && !t2.isLit_dc(i) ) {
			newterm = t1;
			if ( t2.isLit_0(i) ) newterm.setLit_1(i);
			else newterm.setLit_0(i);
			res->AppendTerm(newterm);
		}
	return res;
}

PLA *PLA_op::Sharp( const Term& t1, const Term& t2 )
/* performs t1 # t2
	I.e., returns a list of terms covered by t1 and not not by t2
	Resolves outputs as well
*/
{
	unsigned int i, j;
	PLA *res;		// the result
	Term newterm;
	bool copies;
	string om;

	if ( t1.inputs() != t2.inputs() || t1.outputs() != t2.outputs() ) throw RuntimeException( "TermSharp: Different term sizes" );
	res = new PLA( t1.inputs(), t1.outputs(), PLA_type("f") );
	if ( res == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
	if ( !t1.intersects(t2) ) {
		res->AppendTerm(t1);
		return res;
	}
	
	copies = false;			// if contained in t1 and not in t2, copy it to the result for the resp. output variable
	om.assign( t1.getOMSize(), '~' );
	for ( j = 0; j < t1.getOMSize(); j++ )
		if ( t1.isOM_1(j) && !t2.isOM_1(j) ) {
			copies = true;
			om[j] = '1';
		}
	if ( copies ) {
		newterm = t1;
		newterm.setOM(om);
		res->AppendTerm(newterm);
	}

	for ( i = 0; i < t1.inputs(); i++ )
		if ( t1.isLit_dc(i) && !t2.isLit_dc(i) ) {
			newterm = t1;
			if ( t2.isLit_0(i) ) newterm.setLit_1(i);
			else newterm.setLit_0(i);
			res->AppendTerm(newterm);
		}
	return res;
}

PLA *PLA_op::Sharp( const PLA &pla, const Term &t )
/* returns PLA obtained as pla # t
	I.e., in the resulting pla are terms in pla and not in t
*/
{
	PLA *res;
	TermList::const_iterator ti;
	PLA *terms;

	res = new PLA(&pla);
	if ( res == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
	for ( ti = pla.getConstDataRef().begin(); ti != pla.getConstDataRef().end(); ++ti ) {
		terms = Sharp(*ti, t);
		res->Splice(*terms);
		delete terms;
	}
	return res;
}

SoPLA *PLA_op::Sharp( const SoPLA &pla, const Cube &t )
/* returns PLA obtained as pla # t
	I.e., in the resulting pla are terms in pla and not in t
*/
{
	SoPLA *res;
	CubeList::const_iterator ti;
	SoPLA *terms;

	res = new SoPLA(&pla);
	if ( res == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
	for ( ti = pla.getConstDataRef().begin(); ti != pla.getConstDataRef().end(); ++ti++ ) {
		terms = Sharp(*ti, t);
		res->Splice(*terms);
		delete terms;
	}
	return res;
}

PLA *PLA_op::Sharp( const PLA &pla1, const PLA &pla2 )
/* // Returns PLA obtained as pla1 # pla2
	I.e., in the resulting pla are terms that are in pla1 and not in pla2
*/
{
	PLA *res, *res2 = NULL;
	TermList::const_iterator ti, ti1;
	TermList terms;
	unsigned int i, j;
	bool discard;
	Term t;

	if ( pla1.getTerms() == 0 ) return new PLA(&pla1);	// empty PLA
	if ( pla2.getTerms() == 0 ) return new PLA(pla1);	// copying constructor

	//bool b = pla1.getOName(0) == "n36";
	t.assign(pla1.inputs(), DC);
	res = new PLA(pla1);
	res->setType(PLA_type("f"));
	for ( ti1 = pla2.getConstDataRef().begin(); ti1 != pla2.getConstDataRef().end(); ++ti1 ) {
		t.setOM(ti1->getOM());
		j = 0;
		discard = false;
		for ( i = 0; i < pla1.inputs(); i++ ) {
			if ( pla1.getIName(i) == pla2.getIName(j) ) t.setLit(i, ti1->getLit(j));
			else if ( ti1->getLit(j) != '-' ) {
				discard = true;
				break;
			}
			else j++;
			j++;
			if ( j == pla2.inputs() ) break;
		}
		if ( discard ) continue;
		res2 = Sharp(*res, t);
		delete res;
		res = res2;
		res->RemoveAbsorbed();
//		res->MergeTerms();
//		res->MergeNeighbors();
	}
	return res;
}

SoPLA *PLA_op::Sharp( const SoPLA &pla1, const SoPLA &pla2 )
/* // Returns PLA obtained as pla1 # pla2
	I.e., in the resulting pla are terms that are in pla1 and not in pla2
*/
{
	SoPLA *res, *res2 = NULL;
	CubeList::const_iterator ti, ti1;
	CubeList terms;

	if ( pla1.getTerms() == 0 ) return new SoPLA(&pla1);	// empty PLA
	if ( pla2.getTerms() == 0 ) return new SoPLA(pla1);	// copying constructor

	res = new SoPLA(pla1);
	for ( ti1 = pla2.getConstDataRef().begin(); ti1 != pla2.getConstDataRef().end(); ++ti1 ) {
		res2 = Sharp(*res, *ti1);
		if ( res != &pla1 ) delete res;
		res = res2;
		res->RemoveAbsorbed();
//		res->MergeTerms();
//		res->MergeNeighbors();
	}
	return res2;
}

PLA *PLA_op::Sharp_Complement( const PLA &pla )
//	Returns a complement of a PLA, computed by Sharp
{
	PLA *tautology;
	PLA *res;
	string iv, ov;
	TermList::const_iterator ti;

	if ( pla.getType().r && !pla.getType().f && pla.outputs() == 1 ) {	// just temporary, for Blif r nodes
		res = new PLA(&pla);
		res->setType(PLA_type("f"));
		for ( ti = pla.getConstDataRef().begin(); ti != pla.getConstDataRef().end(); ++ti ) {
			res->AppendTerm((*ti));
			res->getData()->back().setOM("1");
		}
	}
	else {
		tautology = new PLA(&pla);
		if ( tautology == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
		iv.assign(pla.inputs(), '-');
		ov.assign(pla.outputs(), '1');
		tautology->AppendTerm(iv, ov);

		res = Sharp(*tautology, pla );
		delete tautology;
	}
	return res;
}

SoPLA *PLA_op::Sharp_Complement( const SoPLA &pla )
//	Returns a complement of a PLA, computed by Sharp
{
	SoPLA *tautology;
	SoPLA *res;
	string iv;

	tautology = new SoPLA(&pla);
	if ( tautology == NULL) throw RuntimeException( "PLA_operations: Not enough memory" );
	iv.assign(pla.inputs(), '-');
	tautology->AppendTerm(iv);

	res = Sharp(*tautology, pla );
	delete tautology;
	return res;
}
