// Asynch_Multilevel.cpp : Defines the entry point for the console application.
//
#include "stdafx.h"

#include <time.h>

using namespace std;

#include "../../Kernel/kernelincludes.h"
#include "../../Multilevel/Blif.h"
#include "../../Multilevel/Node.h"
#include "../../Multilevel/Signal.h"
#include "../../Multilevel/Network.h"
#include "../../Kernel/orthogonalize.h"
#include "../../Kernel/Complement.h"

void Help()
{
	cout << "Syntax: Asynch_Multilevel source.blif" << endl;
	cout << "Options:" << endl;
	cout << "   -ortho        Produce orthogonal terms" << endl;
	cout << "   -ext_ortho    Use external orthogonalization tool" << endl;
	cout << "   -ext_min      Use external minimization tool (internal minimization not implemented yet)" << endl;
	cout << "   -dc           Extract node don't cares" << endl;
	cout << "   -odc          Use observability DCs as well" << endl;
	cout << "   -SIS_min      Minimize by repeating full_simplify" << endl;
	cout << "   -onsetmin     Minimize on-set using DCs" << endl;
	cout << "   -offsetmin    Minimize off-set using DCs" << endl;
	cout << "   -orthodcs     Use DCs for orthogonalization" << endl;
	cout << "   -shared       Detect shared terms" << endl;
	cout << "   -report       Report to stderr" << endl;
	cout << "                    source_file; source_inputs; source_outputs; source_nodes; source_non_trivial_nodes; source_andor_nodes; source_nontriv_inputs; source_terms; source_non_triv_terms; source_andor_terms; source_literals; source_GEs; source_levels; source_DCnodes; onset_terms; onset_nontriv_terms; onset_andor_terms; onset_literals; onset_GEs;  offset_nontriv_terms; offset_andor_terms; offset_literals; offset_GEs; shared_terms; shared_GEs; effective_DC_nodes " << endl;
}

Blif *InvertOffsetNodes( Blif &offset )
//  Appends inverters to all gates, making the off-set node functionally equivalent to the on-set
{
	list<SoPLA>::iterator ni, ni1;
	string oname, newoname;
	SoPLA inv("0");			// inverter
	Blif *res;

	res = new Blif(&offset);
	for ( ni = offset.getData()->begin(); ni != offset.getData()->end(); ni++ ) {
		res->AppendPLA(&*ni);
		ni1 = res->getData()->end(); ni1--;
		oname = ni1->getName();
		newoname = oname + "_neg";
		ni1->setName(newoname);
		inv.setIName(0, newoname);
		inv.setName(oname);
		res->AppendPLA(&inv);
	}
	return res;
}

PLA *Make_ortho(PLA *pla, bool ext, bool DCs)
{
	PLA *res;
	PLA placopy;
	unsigned int i;

	if ( pla->inputs() == 1 || pla->getTerms() == 1 || ( !DCs && pla->getTerms() == pla->getLiterals() )) {
		res = new PLA(*pla);
		return res;
	}
	if (!ext) return Ortho(pla).Run(4);
	placopy = *pla;
	placopy.StripNames();
	placopy.SavePLA("to_ortho.pla");
	system(RUNSCRIPT("ortho.bat") );
	res = new PLA();
	res->LoadPLA("from_ortho.pla");
	for ( i = 0; i < pla->inputs(); i++ )
		res->setIName(i, pla->getIName(i));
	for ( i = 0; i < pla->outputs(); i++ )
		res->setOName(i, pla->getOName(i));
	return res;
}

SoPLA *Make_ortho(SoPLA *pla, bool ext, bool DCs)
{
	SoPLA *res;
	PLA *res2;
	PLA placopy;
	unsigned int i;

	if ( (*pla).inputs() == 1 || (*pla).getTerms() == 1 || ( !DCs && (*pla).getLiterals() == (*pla).getTerms() )) {
		res = new SoPLA(*pla);
		return res;
	}
	placopy = *pla;
	if (!ext) res2 = Ortho(&placopy).Run(4);
	else {
		placopy.StripNames();
		placopy.setType(PLA_type("fd"));
		placopy.SavePLA("to_ortho.pla");
		system(RUNSCRIPT("ortho.bat") );
		res2 = new PLA();
		res2->LoadPLA("from_ortho.pla");
		for ( i = 0; i < pla->inputs(); i++ )
			res2->setIName(i, pla->getIName(i));
		res2->setOName(0, pla->getName());
	}

	res = res2->ToSoPLA( 0, res2->getData()->front().isOM_1(0) );

	delete res2;
	return res;
}

PLA *Minimize( PLA &pla, bool ext, bool DCs )
{
	PLA *res;
	
	if ( pla.inputs() == 1 || pla.getTerms() == 1  || ( !DCs && pla.getLiterals() == pla.getTerms() ) ) {
		res = new PLA(pla);
	}
	else if (!ext) {			// not supported yet
		res = new PLA(pla);
	} else {
//		pla.StripNames();
		system(DELFILE("from_min.pla"));
		pla.SavePLA("to_min.pla");
		system(RUNSCRIPT("min.bat"));
		res = new PLA();
		res->LoadPLA("from_min.pla");
	}
	return res;
}

unsigned int CountInputs(Blif *blif)
{
	unsigned int cnt = 0;
	list<SoPLA>::iterator pla_it;

	for ( pla_it = blif->getData()->begin(); pla_it != blif->getData()->end(); pla_it++ )
		if ( (*pla_it).inputs() > 1 ) cnt += (*pla_it).inputs();
	return cnt;
}

unsigned int CountNonTrivTerms(Blif *blif)
{
	unsigned int cnt = 0;
	list<SoPLA>::iterator pla_it;

	for ( pla_it = blif->getData()->begin(); pla_it != blif->getData()->end(); pla_it++ )
		if ( (*pla_it).inputs() > 1 ) cnt += (*pla_it).getTerms();
	return cnt;
}

unsigned int CountTerms(Blif *blif)
{
	unsigned int cnt = 0;
	list<SoPLA>::iterator pla_it;

	for ( pla_it = blif->getData()->begin(); pla_it != blif->getData()->end(); pla_it++ )
		cnt += (*pla_it).getTerms();
	return cnt;
}

unsigned int CountANDORTerms(Blif *blif)
{
	unsigned int cnt = 0;
	list<SoPLA>::iterator pla_it;

	for ( pla_it = blif->getData()->begin(); pla_it != blif->getData()->end(); pla_it++ )
		if ( (*pla_it).inputs() > 1 && (*pla_it).getTerms() > 1 && (*pla_it).getTerms() != (*pla_it).getLiterals() ) cnt += (*pla_it).getTerms();
	return cnt;
}

unsigned int CountANDORNodes(Blif *blif)
{
	unsigned int cnt = 0;
	list<SoPLA>::iterator pla_it;

	for ( pla_it = blif->getData()->begin(); pla_it != blif->getData()->end(); pla_it++ )
		if ( (*pla_it).inputs() > 1 && (*pla_it).getTerms() > 1 && (*pla_it).getTerms() != (*pla_it).getLiterals() ) cnt++;
	return cnt;
}

unsigned int CountSharedTerms( PLA &pla )
{
	TermList::iterator ti;
	unsigned int count = 0;

	for ( ti = pla.getData()->begin(); ti != pla.getData()->end(); ti++ )
		if ( (*ti).getOM() == "11" ) count++;
	return count;
}

unsigned int CountShared( Blif &on_blif, Blif &off_blif, unsigned int &GEs )
// Computes shared terms and # of shared GEs
// Extracts terms (in terms of AND gates) from the BLIFs PLAs and compares them wrt. any permutation of variables
{
	list<SoPLA>::iterator pla_it1, pla_it2;
	CubeList::iterator ti1, ti2;
	unsigned int i, j;
	string inp1, inp2;
	vector<string> inames1, inames2;
	unsigned int cnt;
	Blif tmpblif;
	bool equal;
	list<string> inames1_s, inames2_s;

	tmpblif = on_blif;
	tmpblif.AppendBlif(&off_blif);
	// tmpblif.SaveBlif("all.blif");
	
	for ( pla_it1 = tmpblif.getData()->begin(); pla_it1 != tmpblif.getData()->end(); pla_it1++ )
		for ( ti1 = (*pla_it1).getData()->begin(); ti1 != (*pla_it1).getData()->end(); ti1++ )
			(*ti1).tmp = 0;
	GEs = 0;
	cnt = 0;
	for ( pla_it1 = tmpblif.getData()->begin(); pla_it1 != tmpblif.getData()->end(); pla_it1++ )
	  for ( ti1 = (*pla_it1).getData()->begin(); ti1 != (*pla_it1).getData()->end(); ti1++ )
		  if ( (*ti1).tmp == 0 ) {
		  // extract 1st term
			inames1.clear();
			inp1.clear();
			if ( (*ti1).inputs() != 1 && (*ti1).getDim() != (*ti1).inputs()-1 ) {
				for ( i = 0; i < (*pla_it1).inputs(); i++ )
					if ( !(*ti1).isLit_dc(i) ) {
						inp1.push_back((*ti1).getLit(i));
						inames1.push_back( (*pla_it1).getIName(i) );
					}
				pla_it2 = pla_it1;
				pla_it2++;
				while ( pla_it2 != tmpblif.getData()->end() ) {
					for ( ti2 = (*pla_it2).getData()->begin(); ti2 != (*pla_it2).getData()->end(); ti2++ )
						if ( (*ti2).tmp == 0 ) {
							// extract 2nd term
							inames2.clear();
							inp2.clear();
							if ( (*ti2).inputs() != 1 && (*ti2).getDim() != (*ti2).inputs()-1 ) {
								for ( i = 0; i < (*pla_it2).inputs(); i++ )
									if ( !(*ti2).isLit_dc(i) ) {
										inp2.push_back((*ti2).getLit(i));
										inames2.push_back( (*pla_it2).getIName(i) );
									}
							}
							// compare them
							equal = true;
							if ( inames1.size() != inames2.size() ) equal = false;
							else {
								inames1_s.clear();
								inames2_s.clear();
								for ( i = 0; i < inames1.size(); i++ ) {
									inames1_s.push_back(inames1[i]);
									inames2_s.push_back(inames2[i]);
								}
								inames1_s.sort();
								inames2_s.sort();
								if ( inames1_s != inames2_s ) equal = false;
								else for ( i = 0; i < inames1.size(); i++ )
									if ( equal ) 
										for ( j = 0; j < inames2.size(); j++ )
											if ( inames1[i] == inames2[j] && inp1[i] != inp2[j] ) {
												equal = false;
												break;
											}
							}
							if ( equal ) {
								cnt++;
								GEs += inp1.size();
								(*ti2).tmp = 1;
								break;
							}
						}
					pla_it2++;
				}
			}
		}
	return cnt;
}

void ExtractDCs( char *src_file, bool SIS_min, bool odc )
{
	Blif simpDCs;
	
	// full_simplify the initial network
	system(DELFILE("simp_dc.blif") );
	system(DELFILE("simplified.blif") );
	system(DELFILE("all_dc.blif") );
	system(DELFILE("all_DCs.blif") );
	system(DELFILE("SDCs.blif") );
	system(DELFILE("ODCs.blif") );
	if ( odc ) {
		system(RUNSCRIPT(((string)("sis_dc -c \"full_simplify\" -o tmp.blif " + (string)src_file)).c_str()));
		system(RENAME("all_dc.blif all_DCs.blif") );
	}
	system(RUNSCRIPT(((string)("sis_dc -c \"full_simplify -d\" -o tmp.blif " + (string)src_file)).c_str()));
	system(RENAME("all_dc.blif SDCs.blif") );

	try {
		simpDCs.LoadBlif("simp_dc.blif");
	} catch (IOException e) {
			cerr << e.GetMsg() << endl;
			exit(1);
	}
	// full_simplify, while it can be simplified
	while ( simpDCs.GetNodes() != 0 && SIS_min ) {
		system(DELFILE("simp_dc.blif") );
		system(DELFILE("all_dc.blif") );
		system( "sis_dc -c 'full_simplify' -o tmp.blif simplified.blif" );
		try {
			simpDCs.LoadBlif("simp_dc.blif");
		} catch (IOException e) {
				cerr << e.GetMsg() << endl;
				exit(1);
		}
	}
}

bool AppendDCs3( PLA *pla, Network *DCs)
// Appends DCs to the node. pla and DC nodes must have equal variables
{
	pair<bool, list<Signal>::iterator> findres;
	PLA *DC_pla;
	list<Term>::iterator ti;

	system(DELFILE("to_ortho.pla2") );
	findres = DCs->FindSignal(pla->getOName(0));
	if ( !findres.first ) return false;			// no don't cares
	if ( findres.second->IsConstant() ) return false;	// no don't cares
	DC_pla = findres.second->GetSource()->first->getData();
	if ( pla->inputs() != DC_pla->inputs() ) return false; // throw RuntimeException( "Different number of inputs of on- and dc- node" );
	pla->Sort();
	DC_pla->Sort();
	if ( pla->getINames() != DC_pla->getINames() ) return false; // throw RuntimeException( "Different on- and dc- node names" );
	for ( ti = DC_pla->getData()->begin(); ti != DC_pla->getData()->end(); ti++ )
		ti->setOM_dc(0);
	pla->setType("fd");
	pla->AppendTermList(*DC_pla->getData());
	DC_pla->StripNames();
	DC_pla->setType("d");
	DC_pla->SavePLA("to_ortho.pla2");
	DC_pla->setINames(pla->getINames());
	return true;
}

bool AppendDCs2( PLA *pla, Network *DCs)
// Appends DCs to the node. pla and DC nodes are merged, regardless the inputs
{
	pair<bool, list<Signal>::iterator> findres;
	PLA *DC_pla;
	PLA DC_pla2;
	list<Term>::iterator ti;

	system(DELFILE("to_ortho.pla2") );
	findres = DCs->FindSignal(pla->getOName(0));
	if ( !findres.first ) return false;			// no don't cares
	if ( findres.second->IsConstant() ) return false;	// no don't cares
	DC_pla = findres.second->GetSource()->first->getData();
	if ( DC_pla->getLiterals() == 0 ) return false;		// filter tautologies. Bug in SIS?
	for ( ti = DC_pla->getData()->begin(); ti != DC_pla->getData()->end(); ti++ )
		ti->setOM_dc(0);
	pla->setType("fd");
	pla->MergePLAs(*DC_pla);

	DC_pla2 = *pla;
	DC_pla2.setType("d");
	ti = DC_pla2.getData()->begin();
	while ( ti != DC_pla2.getData()->end() )
		if ( ti->getOM(0) != '-' ) ti = DC_pla2.DeleteTerm(ti);
		else ti++;
	DC_pla2.StripNames();
	DC_pla2.SavePLA("to_ortho.pla2");
	return true;
}

bool AppendSubsetPLA( PLA &src, PLA &_pla )
// Appends a subset of terms of _pla into src.
// Only terms having all their support in the src support are appended
// Returns true, if at least one term was appended
{
	unsigned int i;
	list<Term>::iterator ti1;
	bool valid;
	bool res = false;
	Term *t;
	string s;

	t = new Term(src.inputs(), 1);
	for ( ti1 = _pla.getData()->begin(); ti1 != _pla.getData()->end(); ti1++ ) {
		// may be the term appended? Check the support	
		valid = true;
		for ( i = 0; i < _pla.inputs(); i++ ) {
			if ( !ti1->isLit_dc(i) ) {
				if ( src.FindIName(_pla.getIName(i)) == -1 ) {
					valid = false;
					break;
				}
			}
		}
		if ( valid ) {			// append term
			s.assign(src.inputs(), '-');
			t->setCube(s);
			t->setOM(ti1->getOM());
			for ( i = 0; i < _pla.inputs(); i++ )
				if ( !ti1->isLit_dc(i) )
					t->setLit(src.FindIName(_pla.getIName(i)), ti1->getLit(i) );
			src.AppendTerm(*t);
			res = true;
		}
	}
	return res;
}

bool AppendDCs( PLA *pla, Network *DCs)
// Appends DCs to the node. Only completely included terms are appended
{
	pair<bool, list<Signal>::iterator> findres;
	PLA *DC_pla;
	PLA DC_pla2;
	list<Term>::iterator ti;

	system(DELFILE("to_ortho.pla2") );
	findres = DCs->FindSignal(pla->getOName(0));
	if ( !findres.first ) return false;			// no don't cares
	if ( findres.second->IsConstant() ) return false;	// no don't cares
	DC_pla = findres.second->GetSource()->first->getData();
	if ( DC_pla->getLiterals() == 0 ) return false;		// filter tautologies. Bug in SIS?
	for ( ti = DC_pla->getData()->begin(); ti != DC_pla->getData()->end(); ti++ )
		ti->setOM_dc(0);
	pla->setType("fd");
	if ( !AppendSubsetPLA(*pla, *DC_pla) ) return false;

	DC_pla2 = *pla;
	DC_pla2.setType("d");
	ti = DC_pla2.getData()->begin();
	while ( ti != DC_pla2.getData()->end() )
		if ( ti->getOM(0) != '-' ) ti = DC_pla2.DeleteTerm(ti);
		else ti++;
	DC_pla2.StripNames();
	DC_pla2.SavePLA("to_ortho.pla2");
	return true;
}

Network *SubtractSDCs( Network *DCs, Network *All_DCs )
{
	PLA *DC_pla;
	list<Node>::iterator ni;
	list<Term>::iterator ti;
	pair<bool, list<Signal>::iterator> findres;
	Network *ODCs;

	ODCs = new Network(All_DCs);
	for ( ni = All_DCs->getData()->begin(); ni != All_DCs->getData()->end(); ++ni ) {
		findres = DCs->FindSignal(ni->getData()->getOName(0));
		if ( findres.first ) {
			DC_pla = PLA_op().Sharp( *(ni->getData()), *(findres.second->GetSource()->first->getData()) );
			if ( DC_pla->getTerms() != 0 ) {
				ODCs->AddNode(Node(*DC_pla));
				delete DC_pla;
			}
		}
	}
	ODCs->ToBlif()->SaveBlif("ODCs.blif");
	return ODCs;
}

int main(int argc, char* argv[])
{
    Blif source;
    Blif *dest_on;
    Blif *dest_off;
	Blif *inv_offset;
    int i;
	char *src_file = NULL;
	char *dest_file = NULL;
	char *ortho_src_file = NULL;
	time_t tim;
	list<SoPLA>::iterator pla_it;
	bool ortho = false;
	PLA *ort_pla;
	PLA *on_pla;
	PLA *off_pla;
	PLA *min_pla;
	bool ext_ortho = false;
	bool ext_min = false;
	bool report = false;
	bool shared = false;
	bool SIS_min = false;
	bool onsetmin = false;
	bool offsetmin = false;
	bool orthodcs = false;
	bool dc = false;
	bool odc = false;
	unsigned int levels;
	unsigned int literals, GEs, sh_terms = 0;
	unsigned int sh_GEs = 0;
	Network *All_DCs = NULL;
	Network *SDCs = NULL;
	Network *ODCs = NULL;
	Blif DCs_blif;
	Blif ODCs_blif;
	unsigned int DCnodes = 0;
	unsigned int eff_DCnodes = 0;
	SoPLA *tmp_sopla1, *tmp_sopla2;
	ofstream repfile, noderepfile;
	unsigned int onterms[3] = {0, 0, 0}, offterms[3] = {0, 0, 0};
	unsigned int onlits[3] = {0, 0, 0}, offlits[3] = {0, 0, 0};
	bool stop;
	bool DCsUsed, thisDCs;
	char simpfile[] = "simplified.blif";

	cout << "Asynch-Multilevel 3.3, (c) August 2010 by Petr Fiser" << endl;
	if ( argc < 3 ) {
        Help();
        exit(1);
    }
    srand((unsigned) time(&tim));
//    srand(3);

	try {
		i = 1;
		while ( i != argc ) {
			if ( argv[i][0] != '-' && src_file == NULL ) src_file = argv[i];
			else if ( argv[i][0] != '-' && !ortho ) dest_file = argv[i];
			else if ( argv[i][0] != '-' && ortho && ortho_src_file == NULL ) ortho_src_file = argv[i];
			else if ( argv[i][0] != '-' && ortho && dest_file == NULL ) dest_file = argv[i];
			else if ( strcmp( argv[i], "-ortho" ) == 0 ) {
				ortho = true;
			}
			else if ( strcmp( argv[i], "-ext_ortho" ) == 0 ) {
				ext_ortho = true;
			}
			else if ( strcmp( argv[i], "-ext_min" ) == 0 ) {
				ext_min = true;
			}
			else if ( strcmp( argv[i], "-shared" ) == 0 ) {
				shared = true;
			}
			else if ( strcmp( argv[i], "-report" ) == 0 ) {
				report = true;
			}
			else if ( strcmp( argv[i], "-dc" ) == 0 ) {
				dc = true;
			}
			else if ( strcmp( argv[i], "-SIS_min" ) == 0 ) {
				SIS_min = true;	
			}
			else if ( strcmp( argv[i], "-onsetmin" ) == 0 ) {
				onsetmin = true;	
			}
			else if ( strcmp( argv[i], "-offsetmin" ) == 0 ) {
				offsetmin = true;	
			}
			else if ( strcmp( argv[i], "-orthodcs" ) == 0 ) {
				orthodcs = true;	
			}
			else if ( strcmp( argv[i], "-odc" ) == 0 ) {
				odc = true;	
			}
			else {
				Help();
				exit(1);
			}
			i++;
		}
	} catch (...) {
        Help();
        exit(1);
    }

	if ( src_file == NULL ) {
        Help();
        exit(1);
    }	

	if ( report ) {
		repfile.open("report.csv", ios::app);
		noderepfile.open("nodes.txt");
	}

	// Run full_simplify. Compatible don't cares will be in all_dc.blif
	
	if ( SIS_min || dc ) ExtractDCs(src_file, SIS_min, odc);
	if ( SIS_min ) src_file = simpfile;
	if ( dc ) {
		try {
			DCs_blif.LoadBlif("SDCs.blif");
			SDCs = new Network(DCs_blif);
			DCnodes = DCs_blif.GetNodes();
			if ( odc ) {
				ODCs_blif.LoadBlif("all_DCs.blif");
				All_DCs = new Network(ODCs_blif);
				ODCs = SubtractSDCs( SDCs, All_DCs );
			}
		} catch (IOException e) {
				cerr << e.GetMsg() << endl;
				exit(1);
		}
	}

	// Load the source function (possibly yet minimized by full_simplify)
	
	try {
		source.LoadBlif(src_file);
	} catch (IOException e) {
			cerr << e.GetMsg() << endl;
			exit(1);
	}

	levels = source.GetLevels();
	cout << "Source inputs: " << source.inputs() << endl;
	cout << "Source outputs: " << source.outputs() << endl;
	cout << "Source nodes: " << source.GetNodes() << endl;
	cout << "Source non-trivial nodes: " << source.GetNonTrivNodes() << endl;
	cout << "Source AND-OR nodes: " << CountANDORNodes(&source) << endl;
	cout << "Source total non-trivial node inputs: " << CountInputs(&source) << endl;
	cout << "Source total node terms: " << CountTerms(&source) << endl;
	cout << "Source total non-trivial node terms: " << CountNonTrivTerms(&source) << endl;
	cout << "Source total AND-OR node terms: " << CountANDORTerms(&source) << endl;
	cout << "Source literals: " << source.getLiterals() << endl;
	cout << "Source GEs: " << (float)source.getGEs()/2 << endl;
	cout << "Source levels: " << levels << endl;
	cout << "Don't care nodes: " << DCnodes << endl;

	if ( report ) {
		// repfile << "source_file; source_inputs; source_outputs; source_nodes; source_non_trivial_nodes; source_andor_nodes; source_nontriv_inputs; source_terms; source_non_triv_terms; source_andor_terms; source_literals; source_GEs; source_levels; source_DCnodes; onset_terms; onset_nontriv_terms; onset_andor_terms; onset_literals; onset_GEs;  offset_nontriv_terms; offset_andor_terms; offset_literals; offset_GEs; shared_terms; shared_GEs; effective_DC_nodes " << endl;
		repfile << src_file << "; " << source.inputs()
		<< "; " << source.outputs()
		<< "; " << source.GetNodes()
		<< "; " << source.GetNonTrivNodes()
		<< "; " << CountANDORNodes(&source)
		<< "; " << CountInputs(&source)
		<< "; " << CountTerms(&source)
		<< "; " << CountNonTrivTerms(&source)
		<< "; " << CountANDORTerms(&source)
		<< "; " << source.getLiterals()
		<< "; " << (float)source.getGEs()/2
		<< "; " << levels
		<< "; " << DCnodes << "; ";
	}

	try {

		literals = 0;
		GEs = 0;
		sh_terms = 0;
		dest_on = new Blif(&source);
		dest_off = new Blif(&source);
		for ( pla_it = source.getData()->begin(); pla_it != source.getData()->end(); ++pla_it ) {
			system(DELFILE("to_ortho.pla2"));
			DCsUsed = false;
			on_pla = new PLA(*pla_it);
			stop = (on_pla->getOName(0) == "n168");
			onterms[0] = on_pla->getTerms();
			onlits[0] = on_pla->getLiterals();
			if ( on_pla->getTerms() == 1 && on_pla->getData()->front().getCube() == "-" ) {	// constants
				off_pla = new PLA(*on_pla);
				onterms[0] = on_pla->getTerms();
				onlits[0] = on_pla->getLiterals();
				onterms[1] = on_pla->getTerms();
				onlits[1] = on_pla->getLiterals();
				onterms[2] = on_pla->getTerms();
				onlits[2] = on_pla->getLiterals();
				offterms[0] = off_pla->getTerms();
				offlits[0] = off_pla->getLiterals();
				offterms[1] = off_pla->getTerms();
				offlits[1] = off_pla->getLiterals();
				offterms[2] = off_pla->getTerms();
				offlits[2] = off_pla->getLiterals();
				if ( on_pla->getData()->front().getOM(0) == '0' ) {
					off_pla->getData()->front().setOM(0, '1');
					off_pla->setType( "f" );
				} else {
					off_pla->getData()->front().setOM(0, '0');
					off_pla->setType( "r" );
				}
			} else {
				if ( onsetmin ) {
					system(DELFILE("to_ortho.pla2"));
					if ( dc ) {
						thisDCs = AppendDCs(on_pla, SDCs);					// append DCs to the on-set
						DCsUsed |= thisDCs;
					} else thisDCs = false;
					min_pla = Minimize( *on_pla, ext_min, thisDCs );	// preliminary minimization
					delete on_pla;
					on_pla = min_pla;
				}
				onterms[1] = on_pla->getTerms();
				onlits[1] = on_pla->getLiterals();
				if ( on_pla->getTerms() != 0 ) {
					tmp_sopla1 = on_pla->ToSoPLA(0, true);
					tmp_sopla2 = Complement().PLAComplement(tmp_sopla1);
					off_pla = new PLA(*tmp_sopla2);
					offterms[0] = off_pla->getTerms();
					offlits[0] = off_pla->getLiterals();
					delete tmp_sopla1;
					delete tmp_sopla2;
				}
				else {
					off_pla = new PLA(1, 1, PLA_type("f"));
					off_pla->AppendTerm("-", "1");
					off_pla->setOName(0, on_pla->getOName(0));
				}
				if ( offsetmin ) {
					system(DELFILE("to_ortho.pla2"));
					if ( dc ) {
						thisDCs = AppendDCs(off_pla, SDCs);					// append DCs to the off-set
						DCsUsed |= thisDCs;
					} else thisDCs = false;
					min_pla = Minimize( *off_pla, ext_min, thisDCs );	// minimize off-set
					delete off_pla;
					off_pla = min_pla;
				}
				offterms[1] = off_pla->getTerms();
				offlits[1] = off_pla->getLiterals();
				if ( ortho ) {
					system(DELFILE("to_ortho.pla2"));
					if ( dc && orthodcs && !on_pla->isConstant() ) {
						thisDCs = AppendDCs(on_pla, SDCs);					// append DCs to the on-set
						DCsUsed |= thisDCs;
					} else thisDCs = false;
					ort_pla = Make_ortho( on_pla, ext_ortho, thisDCs );
					delete on_pla;
					on_pla = ort_pla;
					onterms[2] = on_pla->getTerms();
					onlits[2] = on_pla->getLiterals();
					system(DELFILE("to_ortho.pla2"));
					if ( dc && orthodcs && !off_pla->isConstant() ) {
						thisDCs = AppendDCs(off_pla, SDCs);				// append DCs to the off-set
						DCsUsed |= thisDCs;
					} else thisDCs = false;
					ort_pla = Make_ortho( off_pla, ext_ortho, thisDCs );
					delete off_pla;
					off_pla = ort_pla;
					offterms[2] = off_pla->getTerms();
					offlits[2] = off_pla->getLiterals();
				}
				on_pla->RemoveAllDCCols();
				off_pla->RemoveAllDCCols();
				if ( DCsUsed ) eff_DCnodes++;
			}
			dest_on->AppendPLA(on_pla->ToSoPLA(0));
			dest_off->AppendPLA(off_pla->ToSoPLA(0));

			noderepfile << on_pla->getOName(0) << "; " << onterms[0] << "; " << onlits[0] << "; " << onterms[1] << "; " << onlits[1] << "; " << onterms[2] << "; " << onlits[2] << "; " << offterms[0] << "; " << offlits[0] << "; " << offterms[1] << "; " << offlits[1] << "; " << offterms[2] << "; " << offlits[2] << endl;


			literals += on_pla->getLiterals();
			GEs += on_pla->getGEs();
			literals += off_pla->getLiterals();
			GEs += off_pla->getGEs();
			
			delete on_pla;
			delete off_pla;

		}

	} catch (IOException e) {
			cerr << e.GetMsg() << endl;
			exit(1);
	} catch (RuntimeException e) {
			cerr << e.GetMsg() << endl;
			exit(1);
	}

	if ( shared ) sh_terms = CountShared( *dest_on, *dest_off, sh_GEs );

	inv_offset = InvertOffsetNodes(*dest_off);
	
	dest_on->SaveBlif("on.blif");
	dest_off->SaveBlif("off.blif");
	inv_offset->SaveBlif("inv_off.blif");

	cout << "Result on-set node terms: " << CountTerms(dest_on) << endl;
	cout << "Result on-set non-trivial node terms: " << CountNonTrivTerms(dest_on) << endl;
	cout << "Result on-set AND-OR node terms: " << CountANDORTerms(dest_on) << endl;
	cout << "Result on-set literals: " << dest_on->getLiterals() << endl;
	cout << "Result on-set GEs: " << (float)dest_on->getGEs()/2 << endl;
	cout << "Result off-set node terms: " << CountTerms(dest_off) << endl;
	cout << "Result off-set non-trivial node terms: " << CountNonTrivTerms(dest_off) << endl;
	cout << "Result off-set AND-OR node terms: " << CountANDORTerms(dest_off) << endl;
	cout << "Result off-set literals: " << dest_off->getLiterals() << endl;
	cout << "Result off-set GEs: " << (float)dest_off->getGEs()/2 << endl;
	cout << "Result total node terms: " << CountTerms(dest_on)+CountTerms(dest_off) << endl;
	cout << "Result total non-trivial node terms: " << CountNonTrivTerms(dest_on)+CountNonTrivTerms(dest_off) << endl;
	cout << "Result total AND-OR node terms: " << CountANDORTerms(dest_on)+CountANDORTerms(dest_off) << endl;
	cout << "Result literals: " << dest_on->getLiterals()+dest_off->getLiterals() << endl;
	cout << "Result GEs: " << (float)(dest_on->getGEs()+dest_off->getGEs())/2 << endl;
	if ( shared ) cout << "Shared terms: " << sh_terms << endl;
	if ( shared ) cout << "Shared GEs: " << (float)sh_GEs/2 << endl;
	cout << "Effective DC nodes " << (float)eff_DCnodes << endl;

	if ( report ) {
		repfile << CountTerms(dest_on)
		<< "; " << CountNonTrivTerms(dest_on)
		<< "; " << CountANDORTerms(dest_on)
		<< "; " << dest_on->getLiterals()
		<< "; " << (float)dest_on->getGEs()/2
		<< "; " << CountTerms(dest_off)
		<< "; " << CountNonTrivTerms(dest_off)
		<< "; " << CountANDORTerms(dest_off)
		<< "; " << dest_off->getLiterals()
		<< "; " << (float)dest_off->getGEs()/2
		<< "; " << sh_terms << "; " << (float)sh_GEs/2
		<< "; " << eff_DCnodes;
		repfile << endl;
	}

//	delete dest;
//	if (ortho) delete orth_src;

	delete SDCs;
	delete ODCs;
	delete All_DCs;
	delete dest_on;
	delete dest_off;
	delete inv_offset;
	if ( report ) {
		noderepfile.close();
		repfile.close();
	}

	return 0;
}
