summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/cut/Abc_NtkFindCi.c988
-rw-r--r--src/opt/cut/cutMan.c5
-rw-r--r--src/opt/cut/cutPre22.c2
-rw-r--r--src/opt/cut/cutTruth.c3
-rw-r--r--src/opt/dec/decAbc.c36
-rw-r--r--src/opt/dec/decFactor.c7
-rw-r--r--src/opt/fxu/fxu.h2
-rw-r--r--src/opt/rwr/rwr.h1
-rw-r--r--src/opt/rwr/rwrEva.c9
-rw-r--r--src/opt/rwr/rwrMan.c22
-rw-r--r--src/opt/rwr/rwrTemp.c121
-rw-r--r--src/opt/sim/sim.h4
-rw-r--r--src/opt/xyz/module.make8
-rw-r--r--src/opt/xyz/xyz.h110
-rw-r--r--src/opt/xyz/xyzBuild.c379
-rw-r--r--src/opt/xyz/xyzCore.c1025
-rw-r--r--src/opt/xyz/xyzInt.h642
-rw-r--r--src/opt/xyz/xyzMan.c144
-rw-r--r--src/opt/xyz/xyzMinEsop.c299
-rw-r--r--src/opt/xyz/xyzMinMan.c113
-rw-r--r--src/opt/xyz/xyzMinSop.c615
-rw-r--r--src/opt/xyz/xyzMinUtil.c277
-rw-r--r--src/opt/xyz/xyzTest.c417
23 files changed, 1192 insertions, 4037 deletions
diff --git a/src/opt/cut/Abc_NtkFindCi.c b/src/opt/cut/Abc_NtkFindCi.c
new file mode 100644
index 00000000..203f9e6f
--- /dev/null
+++ b/src/opt/cut/Abc_NtkFindCi.c
@@ -0,0 +1,988 @@
+/**CFile****************************************************************
+
+ FileName [cutPre22.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Precomputes truth tables for the 2x2 macro cell.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: cutPre22.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cutInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define CUT_CELL_MVAR 9
+
+typedef struct Cut_Cell_t_ Cut_Cell_t;
+typedef struct Cut_CMan_t_ Cut_CMan_t;
+
+struct Cut_Cell_t_
+{
+ Cut_Cell_t * pNext; // pointer to the next cell in the table
+ Cut_Cell_t * pNextVar; // pointer to the next cell of this support size
+ Cut_Cell_t * pParent; // pointer to the cell used to derive this one
+ int nUsed; // the number of times the cell is used
+ char Box[4]; // functions in the boxes
+ unsigned nVars : 4; // the number of variables
+ unsigned CrossBar0 : 4; // the variable set equal
+ unsigned CrossBar1 : 4; // the variable set equal
+ unsigned CrossBarPhase : 2; // the phase of the cross bar (0, 1, or 2)
+ unsigned CanonPhase : 18; // the canonical phase
+ char CanonPerm[CUT_CELL_MVAR+3]; // semicanonical permutation
+ short Store[2*CUT_CELL_MVAR]; // minterm counts in the cofactors
+ unsigned uTruth[1<<(CUT_CELL_MVAR-5)]; // the current truth table
+};
+
+struct Cut_CMan_t_
+{
+ // storage for canonical cells
+ Extra_MmFixed_t * pMem;
+ st_table * tTable;
+ Cut_Cell_t * pSameVar[CUT_CELL_MVAR+1];
+ // elementary truth tables
+ unsigned uInputs[CUT_CELL_MVAR][1<<(CUT_CELL_MVAR-5)];
+ // temporary truth tables
+ unsigned uTemp1[22][1<<(CUT_CELL_MVAR-5)];
+ unsigned uTemp2[22][1<<(CUT_CELL_MVAR-5)];
+ unsigned uTemp3[22][1<<(CUT_CELL_MVAR-5)];
+ unsigned uFinal[1<<(CUT_CELL_MVAR-5)];
+ unsigned puAux[1<<(CUT_CELL_MVAR-5)];
+ // statistical variables
+ int nTotal;
+ int nGood;
+ int nVarCounts[CUT_CELL_MVAR+1];
+ int nSymGroups[CUT_CELL_MVAR+1];
+ int nSymGroupsE[CUT_CELL_MVAR+1];
+ int timeCanon;
+ int timeSupp;
+ int timeTable;
+ int nCellFound;
+ int nCellNotFound;
+};
+
+// NP-classes of functions of 3 variables (22)
+static char * s_NP3[22] = {
+ " 0\n", // 00 const 0 // 0 vars
+ " 1\n", // 01 const 1 // 0 vars
+ "1 1\n", // 02 a // 1 vars
+ "11 1\n", // 03 ab // 2 vars
+ "11 0\n", // 04 (ab)' // 2 vars
+ "10 1\n01 1\n", // 05 a<+>b // 2 vars
+ "111 1\n", // 06 0s abc // 3 vars
+ "111 0\n", // 07 (abc)' //
+ "11- 1\n1-1 1\n", // 08 1p a(b+c) //
+ "11- 0\n1-1 0\n", // 09 (a(b+c))' //
+ "111 1\n100 1\n010 1\n001 1\n", // 10 2s a<+>b<+>c //
+ "10- 0\n1-0 0\n011 0\n", // 11 3p a<+>bc //
+ "101 1\n110 1\n", // 12 4p a(b<+>c) //
+ "101 0\n110 0\n", // 13 (a(b<+>c))' //
+ "11- 1\n1-1 1\n-11 1\n", // 14 5s ab+bc+ac //
+ "111 1\n000 1\n", // 15 6s abc+a'b'c' //
+ "111 0\n000 0\n", // 16 (abc+a'b'c')' //
+ "11- 1\n-11 1\n0-1 1\n", // 17 7 ab+bc+a'c //
+ "011 1\n101 1\n110 1\n", // 18 8s a'bc+ab'c+abc' //
+ "011 0\n101 0\n110 0\n", // 19 (a'bc+ab'c+abc')' //
+ "100 1\n-11 1\n", // 20 9p ab'c'+bc //
+ "100 0\n-11 0\n" // 21 (ab'c'+bc)' //
+};
+
+// NP-classes of functions of 3 variables (22)
+static char * s_NP3Names[22] = {
+ " const 0 ",
+ " const 1 ",
+ " a ",
+ " ab ",
+ " (ab)' ",
+ " a<+>b ",
+ "0s abc ",
+ " (abc)' ",
+ "1p a(b+c) ",
+ " (a(b+c))' ",
+ "2s a<+>b<+>c ",
+ "3p a<+>bc ",
+ "4p a(b<+>c) ",
+ " (a(b<+>c))' ",
+ "5s ab+bc+ac ",
+ "6s abc+a'b'c' ",
+ " (abc+a'b'c')' ",
+ "7 ab+bc+a'c ",
+ "8s a'bc+ab'c+abc' ",
+ " (a'bc+ab'c+abc')' ",
+ "9p ab'c'+bc ",
+ " (ab'c'+bc)' "
+};
+
+// the number of variables in each function
+static int s_NP3VarNums[22] = { 0, 0, 1, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };
+
+// NPN classes of functions of exactly 3 inputs (10)
+static int s_NPNe3[10] = { 6, 8, 10, 11, 12, 14, 15, 17, 18, 20 };
+
+// NPN classes of functions of exactly 3 inputs that are symmetric (5)
+static int s_NPNe3s[10] = { 6, 10, 14, 15, 18 };
+
+// NPN classes of functions of exactly 3 inputs (4)
+static int s_NPNe3p[10] = { 8, 11, 12, 20 };
+
+static Cut_CMan_t * Cut_CManStart();
+static void Cut_CManStop( Cut_CMan_t * p );
+static void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type );
+static void Cut_CellCanonicize( Cut_CMan_t * p, Cut_Cell_t * pCell );
+static int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell );
+static void Cut_CellSuppMin( Cut_Cell_t * pCell );
+static void Cut_CellCrossBar( Cut_Cell_t * pCell );
+
+
+static Cut_CMan_t * s_pCMan = NULL;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Start the precomputation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellLoad()
+{
+ FILE * pFile;
+ char * pFileName = "cells22_daomap_iwls.txt";
+ char pString[1000];
+ Cut_CMan_t * p;
+ Cut_Cell_t * pCell;
+ int Length; //, i;
+ pFile = fopen( pFileName, "r" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file \"%s\".\n", pFileName );
+ return;
+ }
+ // start the manager
+ p = Cut_CManStart();
+ // load truth tables
+ while ( fgets(pString, 1000, pFile) )
+ {
+ Length = strlen(pString);
+ pString[Length--] = 0;
+ if ( Length == 0 )
+ continue;
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = Extra_Base2Log(Length*4);
+ pCell->nUsed = 1;
+// Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
+ Extra_ReadHexadecimal( pCell->uTruth, pString, pCell->nVars );
+ Cut_CellSuppMin( pCell );
+/*
+ // set the elementary permutation
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ pCell->CanonPerm[i] = i;
+ // canonicize
+ pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+*/
+ // add to the table
+ p->nTotal++;
+
+// Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars ); printf( "\n" );
+// if ( p->nTotal == 500 )
+// break;
+
+ if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
+ p->nGood++;
+ }
+ printf( "Read %d cells from file \"%s\". Added %d cells to the table.\n", p->nTotal, pFileName, p->nGood );
+ fclose( pFile );
+// return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Precomputes truth tables for the 2x2 macro cell.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellPrecompute()
+{
+ Cut_CMan_t * p;
+ Cut_Cell_t * pCell, * pTemp;
+ int i1, i2, i3, i, j, k, c, clk = clock(), clk2 = clock();
+
+ p = Cut_CManStart();
+
+ // precompute truth tables
+ for ( i = 0; i < 22; i++ )
+ Cut_CellTruthElem( p->uInputs[0], p->uInputs[1], p->uInputs[2], p->uTemp1[i], 9, i );
+ for ( i = 0; i < 22; i++ )
+ Cut_CellTruthElem( p->uInputs[3], p->uInputs[4], p->uInputs[5], p->uTemp2[i], 9, i );
+ for ( i = 0; i < 22; i++ )
+ Cut_CellTruthElem( p->uInputs[6], p->uInputs[7], p->uInputs[8], p->uTemp3[i], 9, i );
+/*
+ if ( k == 8 && ((i1 == 6 && i2 == 14 && i3 == 20) || (i1 == 20 && i2 == 6 && i3 == 14)) )
+ {
+ Extra_PrintBinary( stdout, &pCell->CanonPhase, pCell->nVars+1 ); printf( " : " );
+ for ( i = 0; i < pCell->nVars; i++ )
+ printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+ Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars );
+ printf( "\n" );
+ }
+*/
+/*
+ // go through symmetric roots
+ for ( k = 0; k < 5; k++ )
+ for ( i1 = 0; i1 < 22; i1++ )
+ for ( i2 = i1; i2 < 22; i2++ )
+ for ( i3 = i2; i3 < 22; i3++ )
+ {
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = 9;
+ pCell->Box[0] = s_NPNe3s[k];
+ pCell->Box[1] = i1;
+ pCell->Box[2] = i2;
+ pCell->Box[3] = i3;
+ // fill in the truth table
+ Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3s[k] );
+ // canonicize
+ Cut_CellCanonicize( pCell );
+
+ // add to the table
+ p->nTotal++;
+ if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+ Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+ else
+ p->nGood++;
+ }
+
+ // go through partially symmetric roots
+ for ( k = 0; k < 4; k++ )
+ for ( i1 = 0; i1 < 22; i1++ )
+ for ( i2 = 0; i2 < 22; i2++ )
+ for ( i3 = i2; i3 < 22; i3++ )
+ {
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = 9;
+ pCell->Box[0] = s_NPNe3p[k];
+ pCell->Box[1] = i1;
+ pCell->Box[2] = i2;
+ pCell->Box[3] = i3;
+ // fill in the truth table
+ Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3p[k] );
+ // canonicize
+ Cut_CellCanonicize( pCell );
+
+ // add to the table
+ p->nTotal++;
+ if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+ Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+ else
+ p->nGood++;
+ }
+
+ // go through non-symmetric functions
+ for ( i1 = 0; i1 < 22; i1++ )
+ for ( i2 = 0; i2 < 22; i2++ )
+ for ( i3 = 0; i3 < 22; i3++ )
+ {
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = 9;
+ pCell->Box[0] = 17;
+ pCell->Box[1] = i1;
+ pCell->Box[2] = i2;
+ pCell->Box[3] = i3;
+ // fill in the truth table
+ Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, 17 );
+ // canonicize
+ Cut_CellCanonicize( pCell );
+
+ // add to the table
+ p->nTotal++;
+ if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+ Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+ else
+ p->nGood++;
+ }
+*/
+
+ // go through non-symmetric functions
+ for ( k = 0; k < 10; k++ )
+ for ( i1 = 0; i1 < 22; i1++ )
+ for ( i2 = 0; i2 < 22; i2++ )
+ for ( i3 = 0; i3 < 22; i3++ )
+ {
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = 9;
+ pCell->Box[0] = s_NPNe3[k];
+ pCell->Box[1] = i1;
+ pCell->Box[2] = i2;
+ pCell->Box[3] = i3;
+ // set the elementary permutation
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ pCell->CanonPerm[i] = i;
+ // fill in the truth table
+ Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3[k] );
+ // minimize the support
+ Cut_CellSuppMin( pCell );
+
+ // canonicize
+ pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+
+ // add to the table
+ p->nTotal++;
+ if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+ Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+ else
+ {
+ p->nGood++;
+ p->nVarCounts[pCell->nVars]++;
+
+ if ( pCell->nVars )
+ for ( i = 0; i < (int)pCell->nVars-1; i++ )
+ {
+ if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
+ continue;
+ // i and i+1 can be symmetric
+ // find the end of this group
+ for ( j = i+1; j < (int)pCell->nVars; j++ )
+ if ( pCell->Store[2*i] != pCell->Store[2*j] )
+ break;
+
+ if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
+ p->nSymGroupsE[j-i]++;
+ else
+ p->nSymGroups[j-i]++;
+ i = j - 1;
+ }
+/*
+ if ( pCell->nVars == 3 )
+ {
+ Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+ printf( "\n" );
+ }
+*/
+ }
+ }
+
+ printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
+ PRT( "Time", clock() - clk );
+ printf( "Cells: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nVarCounts[i] );
+ printf( "\nDiffs: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nSymGroups[i] );
+ printf( "\nEquals: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nSymGroupsE[i] );
+ printf( "\n" );
+
+ // continue adding new cells using support
+ for ( k = CUT_CELL_MVAR; k > 3; k-- )
+ {
+ for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+ for ( i1 = 0; i1 < k; i1++ )
+ for ( i2 = i1+1; i2 < k; i2++ )
+ for ( c = 0; c < 3; c++ )
+ {
+ // derive the cell
+ pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = pTemp->nVars;
+ pCell->pParent = pTemp;
+ // set the elementary permutation
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ pCell->CanonPerm[i] = i;
+ // fill in the truth table
+ Extra_TruthCopy( pCell->uTruth, pTemp->uTruth, pTemp->nVars );
+ // create the cross-bar
+ pCell->CrossBar0 = i1;
+ pCell->CrossBar1 = i2;
+ pCell->CrossBarPhase = c;
+ Cut_CellCrossBar( pCell );
+ // minimize the support
+//clk2 = clock();
+ Cut_CellSuppMin( pCell );
+//p->timeSupp += clock() - clk2;
+ // canonicize
+//clk2 = clock();
+ pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+//p->timeCanon += clock() - clk2;
+
+ // add to the table
+//clk2 = clock();
+ p->nTotal++;
+ if ( Cut_CellTableLookup( p, pCell ) ) // already exists
+ Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
+ else
+ {
+ p->nGood++;
+ p->nVarCounts[pCell->nVars]++;
+
+ for ( i = 0; i < (int)pCell->nVars-1; i++ )
+ {
+ if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
+ continue;
+ // i and i+1 can be symmetric
+ // find the end of this group
+ for ( j = i+1; j < (int)pCell->nVars; j++ )
+ if ( pCell->Store[2*i] != pCell->Store[2*j] )
+ break;
+
+ if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
+ p->nSymGroupsE[j-i]++;
+ else
+ p->nSymGroups[j-i]++;
+ i = j - 1;
+ }
+/*
+ if ( pCell->nVars == 3 )
+ {
+ Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
+ printf( "\n" );
+ }
+*/
+ }
+//p->timeTable += clock() - clk2;
+ }
+
+ printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, sizeof(Cut_Cell_t) );
+ PRT( "Time", clock() - clk );
+ printf( "Cells: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nVarCounts[i] );
+ printf( "\nDiffs: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nSymGroups[i] );
+ printf( "\nEquals: " );
+ for ( i = 0; i <= 9; i++ )
+ printf( "%d=%d ", i, p->nSymGroupsE[i] );
+ printf( "\n" );
+ }
+// printf( "\n" );
+ PRT( "Supp ", p->timeSupp );
+ PRT( "Canon", p->timeCanon );
+ PRT( "Table", p->timeTable );
+// Cut_CManStop( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check the table.]
+
+ Description [Returns 1 if such a truth table already exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell )
+{
+ Cut_Cell_t ** pSlot, * pTemp;
+ unsigned Hash;
+ Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum( pCell->nVars ) );
+ if ( !st_find_or_add( p->tTable, (char *)Hash, (char ***)&pSlot ) )
+ *pSlot = NULL;
+ for ( pTemp = *pSlot; pTemp; pTemp = pTemp->pNext )
+ {
+ if ( pTemp->nVars != pCell->nVars )
+ continue;
+ if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
+ return 1;
+ }
+ // the entry is new
+ pCell->pNext = *pSlot;
+ *pSlot = pCell;
+ // add it to the variable support list
+ pCell->pNextVar = p->pSameVar[pCell->nVars];
+ p->pSameVar[pCell->nVars] = pCell;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellSuppMin( Cut_Cell_t * pCell )
+{
+ static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
+ unsigned * pIn, * pOut, * pTemp;
+ int i, k, Counter, Temp;
+
+ // go backward through the support variables and remove redundant
+ for ( k = pCell->nVars - 1; k >= 0; k-- )
+ if ( !Extra_TruthVarInSupport(pCell->uTruth, pCell->nVars, k) )
+ {
+ // shift all the variables above this one
+ Counter = 0;
+ pIn = pCell->uTruth; pOut = uTemp;
+ for ( i = k; i < (int)pCell->nVars - 1; i++ )
+ {
+ Extra_TruthSwapAdjacentVars( pOut, pIn, pCell->nVars, i );
+ pTemp = pIn; pIn = pOut; pOut = pTemp;
+ // swap the support vars
+ Temp = pCell->CanonPerm[i];
+ pCell->CanonPerm[i] = pCell->CanonPerm[i+1];
+ pCell->CanonPerm[i+1] = Temp;
+ Counter++;
+ }
+ // return the function back into its place
+ if ( Counter & 1 )
+ Extra_TruthCopy( pOut, pIn, pCell->nVars );
+ // remove one variable
+ pCell->nVars--;
+// Extra_PrintBinary( stdout, pCell->uTruth, (1<<pCell->nVars) ); printf( "\n" );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellCrossBar( Cut_Cell_t * pCell )
+{
+ static unsigned uTemp0[1<<(CUT_CELL_MVAR-5)];
+ static unsigned uTemp1[1<<(CUT_CELL_MVAR-5)];
+ Extra_TruthCopy( uTemp0, pCell->uTruth, pCell->nVars );
+ Extra_TruthCopy( uTemp1, pCell->uTruth, pCell->nVars );
+ if ( pCell->CanonPhase == 0 )
+ {
+ Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
+ Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
+ }
+ else if ( pCell->CanonPhase == 1 )
+ {
+ Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
+ Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
+ }
+ else if ( pCell->CanonPhase == 2 )
+ {
+ Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar1 );
+ Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
+ Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
+ }
+ else assert( 0 );
+ Extra_TruthCombine( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type )
+{
+ int nWords = Extra_TruthWordNum( nVars );
+ int i;
+
+ assert( Type < 22 );
+ switch ( Type )
+ {
+ // " 0\n", // 00 const 0
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = 0;
+ return;
+ // " 1\n", // 01 const 1
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = 0xFFFFFFFF;
+ return;
+ // "1 1\n", // 02 a
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i];
+ return;
+ // "11 1\n", // 03 ab
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] & InB[i];
+ return;
+ // "11 0\n", // 04 (ab)'
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~(InA[i] & InB[i]);
+ return;
+ // "10 1\n01 1\n", // 05 a<+>b
+ case 5:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] ^ InB[i];
+ return;
+ // "111 1\n", // 06 + abc
+ case 6:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] & InB[i] & InC[i];
+ return;
+ // "111 0\n", // 07 (abc)'
+ case 7:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~(InA[i] & InB[i] & InC[i]);
+ return;
+ // "11- 1\n1-1 1\n", // 08 + a(b+c)
+ case 8:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] & (InB[i] | InC[i]);
+ return;
+ // "11- 0\n1-1 0\n", // 09 (a(b+c))'
+ case 9:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~(InA[i] & (InB[i] | InC[i]));
+ return;
+ // "111 1\n100 1\n010 1\n001 1\n", // 10 + a<+>b<+>c
+ case 10:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] ^ InB[i] ^ InC[i];
+ return;
+ // "10- 0\n1-0 0\n011 0\n", // 11 + a<+>bc
+ case 11:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] ^ (InB[i] & InC[i]);
+ return;
+ // "101 1\n110 1\n", // 12 + a(b<+>c)
+ case 12:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = InA[i] & (InB[i] ^ InC[i]);
+ return;
+ // "101 0\n110 0\n", // 13 (a(b<+>c))'
+ case 13:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~(InA[i] & (InB[i] ^ InC[i]));
+ return;
+ // "11- 1\n1-1 1\n-11 1\n", // 14 + ab+bc+ac
+ case 14:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (InA[i] & InC[i]);
+ return;
+ // "111 1\n000 1\n", // 15 + abc+a'b'c'
+ case 15:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]);
+ return;
+ // "111 0\n000 0\n", // 16 (abc+a'b'c')'
+ case 16:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~((InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]));
+ return;
+ // "11- 1\n-11 1\n0-1 1\n", // 17 + ab+bc+a'c
+ case 17:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (~InA[i] & InC[i]);
+ return;
+ // "011 1\n101 1\n110 1\n", // 18 + a'bc+ab'c+abc'
+ case 18:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]);
+ return;
+ // "011 0\n101 0\n110 0\n", // 19 (a'bc+ab'c+abc')'
+ case 19:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~((~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]));
+ return;
+ // "100 1\n-11 1\n", // 20 + ab'c'+bc
+ case 20:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = (InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]);
+ return;
+ // "100 0\n-11 0\n" // 21 (ab'c'+bc)'
+ case 21:
+ for ( i = 0; i < nWords; i++ )
+ pOut[i] = ~((InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]));
+ return;
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Start the precomputation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Cut_CMan_t * Cut_CManStart()
+{
+ Cut_CMan_t * p;
+ int i, k;
+ // start the manager
+ assert( sizeof(unsigned) == 4 );
+ p = ALLOC( Cut_CMan_t, 1 );
+ memset( p, 0, sizeof(Cut_CMan_t) );
+ // start the table and the memory manager
+ p->tTable = st_init_table(st_ptrcmp,st_ptrhash);
+ p->pMem = Extra_MmFixedStart( sizeof(Cut_Cell_t) );
+ // set elementary truth tables
+ for ( k = 0; k < CUT_CELL_MVAR; k++ )
+ for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
+ if ( i & (1 << k) )
+ p->uInputs[k][i>>5] |= (1 << (i&31));
+ s_pCMan = p;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CManStop( Cut_CMan_t * p )
+{
+ st_free_table( p->tTable );
+ Extra_MmFixedStop( p->pMem, 0 );
+ free( p );
+}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_CellIsRunning()
+{
+ return s_pCMan != NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cut_CellDumpToFile()
+{
+ FILE * pFile;
+ Cut_CMan_t * p = s_pCMan;
+ Cut_Cell_t * pTemp;
+ char * pFileName = "celllib22.txt";
+ int NumUsed[10][5] = {{0}};
+ int BoxUsed[22][5] = {{0}};
+ int i, k, Counter;
+ int clk = clock();
+
+ if ( p == NULL )
+ {
+ printf( "Cut_CellDumpToFile: Cell manager is not defined.\n" );
+ return;
+ }
+
+ // count the number of cells used
+ for ( k = CUT_CELL_MVAR; k >= 0; k-- )
+ {
+ for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+ {
+ if ( pTemp->nUsed == 0 )
+ NumUsed[k][0]++;
+ else if ( pTemp->nUsed < 10 )
+ NumUsed[k][1]++;
+ else if ( pTemp->nUsed < 100 )
+ NumUsed[k][2]++;
+ else if ( pTemp->nUsed < 1000 )
+ NumUsed[k][3]++;
+ else
+ NumUsed[k][4]++;
+
+ for ( i = 0; i < 4; i++ )
+ if ( pTemp->nUsed == 0 )
+ BoxUsed[ pTemp->Box[i] ][0]++;
+ else if ( pTemp->nUsed < 10 )
+ BoxUsed[ pTemp->Box[i] ][1]++;
+ else if ( pTemp->nUsed < 100 )
+ BoxUsed[ pTemp->Box[i] ][2]++;
+ else if ( pTemp->nUsed < 1000 )
+ BoxUsed[ pTemp->Box[i] ][3]++;
+ else
+ BoxUsed[ pTemp->Box[i] ][4]++;
+ }
+ }
+
+ printf( "Functions found = %10d. Functions not found = %10d.\n", p->nCellFound, p->nCellNotFound );
+ for ( k = 0; k <= CUT_CELL_MVAR; k++ )
+ {
+ printf( "%3d : ", k );
+ for ( i = 0; i < 5; i++ )
+ printf( "%8d ", NumUsed[k][i] );
+ printf( "\n" );
+ }
+ printf( "Box usage:\n" );
+ for ( k = 0; k < 22; k++ )
+ {
+ printf( "%3d : ", k );
+ for ( i = 0; i < 5; i++ )
+ printf( "%8d ", BoxUsed[k][i] );
+ printf( " %s", s_NP3Names[k] );
+ printf( "\n" );
+ }
+
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Cut_CellDumpToFile: Cannout open output file.\n" );
+ return;
+ }
+
+ Counter = 0;
+ for ( k = 0; k <= CUT_CELL_MVAR; k++ )
+ {
+ for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
+ if ( pTemp->nUsed > 0 )
+ {
+ Extra_PrintHexadecimal( pFile, pTemp->uTruth, (k <= 5? 5 : k) );
+ fprintf( pFile, "\n" );
+ Counter++;
+ }
+ fprintf( pFile, "\n" );
+ }
+ fclose( pFile );
+
+ printf( "Library composed of %d functions is written into file \"%s\". ", Counter, pFileName );
+
+ PRT( "Time", clock() - clk );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Looks up if the given function exists in the hash table.]
+
+ Description [If the function exists, returns 1, meaning that it can be
+ implemented using two levels of 3-input LUTs. If the function does not
+ exist, return 0.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Cut_CellTruthLookup( unsigned * pTruth, int nVars )
+{
+ Cut_CMan_t * p = s_pCMan;
+ Cut_Cell_t * pTemp;
+ Cut_Cell_t Cell, * pCell = &Cell;
+ unsigned Hash;
+ int i;
+
+ // cell manager is not defined
+ if ( p == NULL )
+ {
+ printf( "Cut_CellTruthLookup: Cell manager is not defined.\n" );
+ return 0;
+ }
+
+ // canonicize
+ memset( pCell, 0, sizeof(Cut_Cell_t) );
+ pCell->nVars = nVars;
+ Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
+ Cut_CellSuppMin( pCell );
+ // set the elementary permutation
+ for ( i = 0; i < (int)pCell->nVars; i++ )
+ pCell->CanonPerm[i] = i;
+ // canonicize
+ pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
+
+
+ // check if the cell exists
+ Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum(pCell->nVars) );
+ if ( st_lookup( p->tTable, (char *)Hash, (char **)&pTemp ) )
+ {
+ for ( ; pTemp; pTemp = pTemp->pNext )
+ {
+ if ( pTemp->nVars != pCell->nVars )
+ continue;
+ if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
+ {
+ pTemp->nUsed++;
+ p->nCellFound++;
+ return 1;
+ }
+ }
+ }
+ p->nCellNotFound++;
+ return 0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c
index 0cd01bc9..22ea1cb6 100644
--- a/src/opt/cut/cutMan.c
+++ b/src/opt/cut/cutMan.c
@@ -45,6 +45,8 @@ Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
{
Cut_Man_t * p;
int clk = clock();
+// extern int nTruthDsd;
+// nTruthDsd = 0;
assert( pParams->nVarsMax >= 3 && pParams->nVarsMax <= CUT_SIZE_MAX );
p = ALLOC( Cut_Man_t, 1 );
memset( p, 0, sizeof(Cut_Man_t) );
@@ -114,6 +116,9 @@ void Cut_ManStop( Cut_Man_t * p )
{
Cut_Cut_t * pCut;
int i;
+// extern int nTruthDsd;
+// printf( "Decomposable cuts = %d.\n", nTruthDsd );
+
Vec_PtrForEachEntry( p->vCutsNew, pCut, i )
if ( pCut != NULL )
{
diff --git a/src/opt/cut/cutPre22.c b/src/opt/cut/cutPre22.c
index 693978d6..203f9e6f 100644
--- a/src/opt/cut/cutPre22.c
+++ b/src/opt/cut/cutPre22.c
@@ -779,7 +779,7 @@ Cut_CMan_t * Cut_CManStart()
for ( k = 0; k < CUT_CELL_MVAR; k++ )
for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
if ( i & (1 << k) )
- p->uInputs[k][i/32] |= (1 << (i%32));
+ p->uInputs[k][i>>5] |= (1 << (i&31));
s_pCMan = p;
return p;
}
diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c
index 2e36c9e1..c3514ad7 100644
--- a/src/opt/cut/cutTruth.c
+++ b/src/opt/cut/cutTruth.c
@@ -189,6 +189,9 @@ void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_C
Extra_TruthNand( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
else
Extra_TruthAnd( Cut_CutReadTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nVarsMax );
+
+// Ivy_TruthTestOne( *Cut_CutReadTruth(pCut) );
+
// quit if no fancy computation is needed
if ( !p->pParams->fFancy )
return;
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index af76cd84..1b23bb53 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -19,6 +19,7 @@
#include "abc.h"
#include "dec.h"
//#include "aig.h"
+#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -238,6 +239,41 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
}
*/
+/**Function*************************************************************
+
+ Synopsis [Transforms the decomposition graph into the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+ Dec_Node_t * pNode;
+ Ivy_Obj_t * pAnd0, * pAnd1;
+ int i;
+ // check for constant function
+ if ( Dec_GraphIsConst(pGraph) )
+ return Ivy_NotCond( Ivy_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+ // check for a literal
+ if ( Dec_GraphIsVar(pGraph) )
+ return Ivy_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+ // build the AIG nodes corresponding to the AND gates of the graph
+ Dec_GraphForEachNode( pGraph, pNode, i )
+ {
+ pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+ }
+ // complement the result if necessary
+ return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index 210b69e5..dca422ea 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -258,16 +258,15 @@ Dec_Edge_t Dec_FactorTrivial( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover )
***********************************************************************/
Dec_Edge_t Dec_FactorTrivialCube( Dec_Graph_t * pFForm, Mvc_Cover_t * pCover, Mvc_Cube_t * pCube, Vec_Int_t * vEdgeLits )
{
-// Dec_Edge_t eNode;
+ Dec_Edge_t eNode;
int iBit, Value;
// create the factored form for each literal
Vec_IntClear( vEdgeLits );
Mvc_CubeForEachBit( pCover, pCube, iBit, Value )
if ( Value )
{
-// eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
-// Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
- Vec_IntPush( vEdgeLits, iBit );
+ eNode = Dec_EdgeCreate( iBit/2, iBit%2 ); // CST
+ Vec_IntPush( vEdgeLits, Dec_EdgeToInt_(eNode) );
}
// balance the factored forms
return Dec_FactorTrivialTree_rec( pFForm, (Dec_Edge_t *)vEdgeLits->pArray, vEdgeLits->nSize, 0 );
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index 6a1bb5e3..7025d019 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -37,9 +37,11 @@ extern "C" {
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
+#ifndef __cplusplus
#ifndef bool
#define bool int
#endif
+#endif
typedef struct FxuDataStruct Fxu_Data_t;
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 8de225e8..f8c40a7c 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -135,6 +135,7 @@ extern void Rwr_ManStop( Rwr_Man_t * p );
extern void Rwr_ManPrintStats( Rwr_Man_t * p );
extern void Rwr_ManPrintStatsFile( Rwr_Man_t * p );
extern void * Rwr_ManReadDecs( Rwr_Man_t * p );
+extern Vec_Ptr_t * Rwr_ManReadLeaves( Rwr_Man_t * p );
extern int Rwr_ManReadCompl( Rwr_Man_t * p );
extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
extern void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time );
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 55132a75..9ae9c18c 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -100,9 +100,16 @@ clk = clock();
p->nCutsGood++;
clk2 = clock();
+/*
+ printf( "Considering: (" );
+ Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
+ printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pFanin)) );
+ printf( ")\n" );
+*/
// mark the fanin boundary
Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
Abc_ObjRegular(pFanin)->vFanouts.nSize++;
+
// label MFFC with current ID
Abc_NtkIncrementTravId( pNode->pNtk );
nNodesSaved = Abc_NodeMffcLabel( pNode );
@@ -136,6 +143,8 @@ p->timeRes += clock() - clk;
if ( GainBest == -1 )
return -1;
+// printf( "%d", nNodesSaveCur - GainBest );
+
// copy the leaves
Vec_PtrForEachEntry( p->vFanins, pFanin, i )
Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index 115065f5..b6d58d99 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -163,7 +163,11 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
printf( "The scores are:\n" );
for ( i = 0; i < 222; i++ )
if ( p->nScores[i] > 0 )
- printf( "%3d = %8d canon = %5d\n", i, p->nScores[i], p->pMapInv[i] );
+ {
+ extern void Ivy_TruthDsdComputePrint( unsigned uTruth );
+ printf( "%3d = %8d canon = %5d ", i, p->nScores[i], p->pMapInv[i] );
+ Ivy_TruthDsdComputePrint( (unsigned)p->pMapInv[i] | ((unsigned)p->pMapInv[i] << 16) );
+ }
printf( "\n" );
}
@@ -218,6 +222,22 @@ void * Rwr_ManReadDecs( Rwr_Man_t * p )
SeeAlso []
***********************************************************************/
+Vec_Ptr_t * Rwr_ManReadLeaves( Rwr_Man_t * p )
+{
+ return p->vFanins;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the resynthesis manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Rwr_ManReadCompl( Rwr_Man_t * p )
{
return p->fCompl;
diff --git a/src/opt/rwr/rwrTemp.c b/src/opt/rwr/rwrTemp.c
new file mode 100644
index 00000000..3ffbd408
--- /dev/null
+++ b/src/opt/rwr/rwrTemp.c
@@ -0,0 +1,121 @@
+/**CFile****************************************************************
+
+ FileName [rwrCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis [Cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int pTruths[13719];
+static int pFreqs[13719];
+static int pPerm[13719];
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwr_TempCompare( int * pNum1, int * pNum2 )
+{
+ int Freq1 = pFreqs[*pNum1];
+ int Freq2 = pFreqs[*pNum2];
+ if ( Freq1 < Freq2 )
+ return 1;
+ if ( Freq1 > Freq2 )
+ return -1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_Temp()
+{
+ char Buffer[32];
+ int nFuncs = 13719;
+ int nEntries = 100;
+ unsigned uTruth;
+ int i, k;
+ FILE * pFile;
+
+ pFile = fopen( "nnclass_stats5.txt", "r" );
+ for ( i = 0; i < 13719; i++ )
+ {
+ fscanf( pFile, "%s%d", Buffer, &pFreqs[i] );
+ Extra_ReadHexadecimal( &uTruth, Buffer+2, 5 );
+ pTruths[i] = uTruth;
+ }
+ fclose( pFile );
+
+ for ( i = 0; i < 13719; i++ )
+ pPerm[i] = i;
+
+ qsort( (void *)pPerm, 13719, sizeof(int),
+ (int (*)(const void *, const void *)) Rwr_TempCompare );
+
+
+ pFile = fopen( "5npn_100.blif", "w" );
+ fprintf( pFile, "# Most frequent NPN classes of 5 vars.\n" );
+ fprintf( pFile, ".model 5npn\n" );
+ fprintf( pFile, ".inputs a b c d e\n" );
+ fprintf( pFile, ".outputs" );
+ for ( i = 0; i < nEntries; i++ )
+ fprintf( pFile, " %02d", i );
+ fprintf( pFile, "\n" );
+
+ for ( i = 0; i < nEntries; i++ )
+ {
+ fprintf( pFile, ".names a b c d e %02d\n", i );
+ uTruth = pTruths[pPerm[i]];
+ for ( k = 0; k < 32; k++ )
+ if ( uTruth & (1 << k) )
+ {
+ Extra_PrintBinary( pFile, &k, 5 );
+ fprintf( pFile, " 1\n" );
+ }
+ }
+ fprintf( pFile, ".end\n" );
+ fclose( pFile );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 7f32fc34..7fcf5ae6 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -143,8 +143,8 @@ struct Sim_Pat_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#define SIM_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0))
-#define SIM_LAST_BITS(n) ((((n)%32) > 0)? (n)%32 : 32)
+#define SIM_NUM_WORDS(n) (((n)>>5) + (((n)&31) > 0))
+#define SIM_LAST_BITS(n) ((((n)&31) > 0)? (n)&31 : 32)
#define SIM_MASK_FULL (0xFFFFFFFF)
#define SIM_MASK_BEG(n) (SIM_MASK_FULL >> (32-n))
diff --git a/src/opt/xyz/module.make b/src/opt/xyz/module.make
deleted file mode 100644
index ae7dab0f..00000000
--- a/src/opt/xyz/module.make
+++ /dev/null
@@ -1,8 +0,0 @@
-SRC += src/opt/xyz/xyzBuild.c \
- src/opt/xyz/xyzCore.c \
- src/opt/xyz/xyzMan.c \
- src/opt/xyz/xyzMinEsop.c \
- src/opt/xyz/xyzMinMan.c \
- src/opt/xyz/xyzMinSop.c \
- src/opt/xyz/xyzMinUtil.c \
- src/opt/xyz/xyzTest.c
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
deleted file mode 100644
index 4fec2150..00000000
--- a/src/opt/xyz/xyz.h
+++ /dev/null
@@ -1,110 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyz.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [External declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyz.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __XYZ_H__
-#define __XYZ_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-#include "abc.h"
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Xyz_Man_t_ Xyz_Man_t;
-typedef struct Xyz_Obj_t_ Xyz_Obj_t;
-
-// storage for node information
-struct Xyz_Obj_t_
-{
- Min_Cube_t * pCover[3]; // pos/neg/esop
- Vec_Int_t * vSupp; // computed support (all nodes except CIs)
-};
-
-// storage for additional information
-struct Xyz_Man_t_
-{
- // general characteristics
- int nFaninMax; // the number of vars
- int nCubesMax; // the limit on the number of cubes in the intermediate covers
- int nWords; // the number of words
- Vec_Int_t * vFanCounts; // fanout counts
- Vec_Ptr_t * vObjStrs; // object structures
- void * pMemory; // memory for the internal data strctures
- Min_Man_t * pManMin; // the cub manager
- int fUseEsop; // enables ESOPs
- int fUseSop; // enables SOPs
- // arrays to map local variables
- Vec_Int_t * vComTo0; // mapping of common variables into first fanin
- Vec_Int_t * vComTo1; // mapping of common variables into second fanin
- Vec_Int_t * vPairs0; // the first var in each pair of common vars
- Vec_Int_t * vPairs1; // the second var in each pair of common vars
- Vec_Int_t * vTriv0; // trival support of the first node
- Vec_Int_t * vTriv1; // trival support of the second node
- // statistics
- int nSupps; // supports created
- int nSuppsMax; // the maximum number of supports
- int nBoundary; // the boundary size
- int nNodes; // the number of nodes processed
-};
-
-static inline Xyz_Obj_t * Abc_ObjGetStr( Abc_Obj_t * pObj ) { return Vec_PtrEntry(((Xyz_Man_t *)pObj->pNtk->pManCut)->vObjStrs, pObj->Id); }
-
-static inline void Abc_ObjSetSupp( Abc_Obj_t * pObj, Vec_Int_t * vVec ) { Abc_ObjGetStr(pObj)->vSupp = vVec; }
-static inline Vec_Int_t * Abc_ObjGetSupp( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->vSupp; }
-
-static inline void Abc_ObjSetCover2( Abc_Obj_t * pObj, Min_Cube_t * pCov ) { Abc_ObjGetStr(pObj)->pCover[2] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover2( Abc_Obj_t * pObj ) { return Abc_ObjGetStr(pObj)->pCover[2]; }
-
-static inline void Abc_ObjSetCover( Abc_Obj_t * pObj, Min_Cube_t * pCov, int Pol ) { Abc_ObjGetStr(pObj)->pCover[Pol] = pCov; }
-static inline Min_Cube_t * Abc_ObjGetCover( Abc_Obj_t * pObj, int Pol ) { return Abc_ObjGetStr(pObj)->pCover[Pol]; }
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== xyzBuild.c ==========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk );
-/*=== xyzCore.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-/*=== xyzMan.c ============================================================*/
-extern Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax );
-extern void Xyz_ManFree( Xyz_Man_t * p );
-extern void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
-/*=== xyzTest.c ===========================================================*/
-extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-
diff --git a/src/opt/xyz/xyzBuild.c b/src/opt/xyz/xyzBuild.c
deleted file mode 100644
index e32721e7..00000000
--- a/src/opt/xyz/xyzBuild.c
+++ /dev/null
@@ -1,379 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzBuild.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Network construction procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzBuild.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
-{
- Vec_Int_t * vLits;
- Abc_Obj_t * pNodeNew, * pFanin;
- int i, iFanin, Lit;
- // create empty cube
- if ( pCube->nLits == 0 )
- return Abc_NodeCreateConst1(pNtkNew);
- // get the literals of this cube
- vLits = Vec_IntAlloc( 10 );
- Min_CubeGetLits( pCube, vLits );
- assert( pCube->nLits == (unsigned)vLits->nSize );
- // create special case when there is only one literal
- if ( pCube->nLits == 1 )
- {
- iFanin = Vec_IntEntry(vLits,0);
- pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
- Lit = Min_CubeGetVar(pCube, iFanin);
- assert( Lit == 1 || Lit == 2 );
- Vec_IntFree( vLits );
- if ( Lit == 1 )// negative
- return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
- return pFanin->pCopy;
- }
- assert( pCube->nLits > 1 );
- // create the AND cube
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- for ( i = 0; i < vLits->nSize; i++ )
- {
- iFanin = Vec_IntEntry(vLits,i);
- pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
- Lit = Min_CubeGetVar(pCube, iFanin);
- assert( Lit == 1 || Lit == 2 );
- Vec_IntWriteEntry( vLits, i, Lit==1 );
- Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
- }
- pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
- Vec_IntFree( vLits );
- return pNodeNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveNode_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int Level )
-{
- Min_Cube_t * pCover, * pCube;
- Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
- Vec_Int_t * vSupp;
- int Entry, nCubes, i;
-
- if ( Abc_ObjIsCi(pObj) )
- return pObj->pCopy;
- assert( Abc_ObjIsNode(pObj) );
- // skip if already computed
- if ( pObj->pCopy )
- return pObj->pCopy;
-
- // get the support and the cover
- vSupp = Abc_ObjGetSupp( pObj );
- pCover = Abc_ObjGetCover2( pObj );
- assert( vSupp );
-/*
- if ( pCover && pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) > 0 )
- {
- printf( "%d\n ", pCover->nVars - Min_CoverSuppVarNum(p->pManMin, pCover) );
- Min_CoverWrite( stdout, pCover );
- }
-*/
-/*
- // print the support of this node
- printf( "{ " );
- Vec_IntForEachEntry( vSupp, Entry, i )
- printf( "%d ", Entry );
- printf( "} cubes = %d\n", Min_CoverCountCubes( pCover ) );
-*/
- // process the fanins
- Vec_IntForEachEntry( vSupp, Entry, i )
- {
- pFanin = Abc_NtkObj(pObj->pNtk, Entry);
- Abc_NtkXyzDeriveNode_rec( p, pNtkNew, pFanin, Level+1 );
- }
-
- // for each cube, construct the node
- nCubes = Min_CoverCountCubes( pCover );
- if ( nCubes == 0 )
- pNodeNew = Abc_NodeCreateConst0(pNtkNew);
- else if ( nCubes == 1 )
- pNodeNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCover, vSupp );
- else
- {
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- Min_CoverForEachCube( pCover, pCube )
- {
- pFaninNew = Abc_NtkXyzDeriveCube( pNtkNew, pObj, pCube, vSupp );
- Abc_ObjAddFanin( pNodeNew, pFaninNew );
- }
- pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
- }
-/*
- printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
- Vec_IntForEachEntry( vSupp, Entry, i )
- {
- pFanin = Abc_NtkObj(pObj->pNtk, Entry);
- printf( "%d(%d) ", pFanin->pCopy->Id, pFanin->Id );
- }
- printf( "\n" );
- Min_CoverWrite( stdout, pCover );
-*/
- pObj->pCopy = pNodeNew;
- return pNodeNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzDerive( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
-{
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObj;
- int i;
- assert( Abc_NtkIsStrash(pNtk) );
- // perform strashing
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
- // reconstruct the network
- Abc_NtkForEachCo( pNtk, pObj, i )
- {
- Abc_NtkXyzDeriveNode_rec( p, pNtkNew, Abc_ObjFanin0(pObj), 0 );
-// printf( "*** CO %s : %d -> %d \n", Abc_ObjName(pObj), pObj->pCopy->Id, Abc_ObjFanin0(pObj)->pCopy->Id );
- }
- // add the COs
- Abc_NtkFinalize( pNtk, pNtkNew );
- Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
- // make sure everything is okay
- if ( !Abc_NtkCheck( pNtkNew ) )
- {
- printf( "Abc_NtkXyzDerive: The network check has failed.\n" );
- Abc_NtkDelete( pNtkNew );
- return NULL;
- }
- return pNtkNew;
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
-{
- assert( pObj->pCopy );
- if ( !fCompl )
- return pObj->pCopy;
- if ( pObj->pCopy->pCopy == NULL )
- pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
- return pObj->pCopy->pCopy;
- }
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cube_t * pCube, Vec_Int_t * vSupp )
-{
- Vec_Int_t * vLits;
- Abc_Obj_t * pNodeNew, * pFanin;
- int i, iFanin, Lit;
- // create empty cube
- if ( pCube->nLits == 0 )
- return Abc_NodeCreateConst1(pNtkNew);
- // get the literals of this cube
- vLits = Vec_IntAlloc( 10 );
- Min_CubeGetLits( pCube, vLits );
- assert( pCube->nLits == (unsigned)vLits->nSize );
- // create special case when there is only one literal
- if ( pCube->nLits == 1 )
- {
- iFanin = Vec_IntEntry(vLits,0);
- pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
- Lit = Min_CubeGetVar(pCube, iFanin);
- assert( Lit == 1 || Lit == 2 );
- Vec_IntFree( vLits );
-// if ( Lit == 1 )// negative
-// return Abc_NodeCreateInv( pNtkNew, pFanin->pCopy );
-// return pFanin->pCopy;
- return Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 );
- }
- assert( pCube->nLits > 1 );
- // create the AND cube
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- for ( i = 0; i < vLits->nSize; i++ )
- {
- iFanin = Vec_IntEntry(vLits,i);
- pFanin = Abc_NtkObj( pObj->pNtk, Vec_IntEntry(vSupp, iFanin) );
- Lit = Min_CubeGetVar(pCube, iFanin);
- assert( Lit == 1 || Lit == 2 );
- Vec_IntWriteEntry( vLits, i, Lit==1 );
-// Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
- Abc_ObjAddFanin( pNodeNew, Abc_NtkXyzDeriveInv( pNtkNew, pFanin, Lit==1 ) );
- }
-// pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
- pNodeNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, vLits->nSize, NULL );
- Vec_IntFree( vLits );
- return pNodeNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t * Abc_NtkXyzDeriveNodeInv_rec( Xyz_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCompl )
-{
- Min_Cube_t * pCover, * pCube;
- Abc_Obj_t * pFaninNew, * pNodeNew, * pFanin;
- Vec_Int_t * vSupp;
- int Entry, nCubes, i;
-
- // skip if already computed
- if ( pObj->pCopy )
- return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
- assert( Abc_ObjIsNode(pObj) );
-
- // get the support and the cover
- vSupp = Abc_ObjGetSupp( pObj );
- pCover = Abc_ObjGetCover2( pObj );
- assert( vSupp );
-
- // process the fanins
- Vec_IntForEachEntry( vSupp, Entry, i )
- {
- pFanin = Abc_NtkObj(pObj->pNtk, Entry);
- Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, pFanin, 0 );
- }
-
- // for each cube, construct the node
- nCubes = Min_CoverCountCubes( pCover );
- if ( nCubes == 0 )
- pNodeNew = Abc_NodeCreateConst0(pNtkNew);
- else if ( nCubes == 1 )
- pNodeNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCover, vSupp );
- else
- {
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- Min_CoverForEachCube( pCover, pCube )
- {
- pFaninNew = Abc_NtkXyzDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
- Abc_ObjAddFanin( pNodeNew, pFaninNew );
- }
- pNodeNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nCubes );
- }
-
- pObj->pCopy = pNodeNew;
- return Abc_NtkXyzDeriveInv( pNtkNew, pObj, fCompl );
-}
-
-/**Function*************************************************************
-
- Synopsis [Derives the decomposed network.]
-
- Description [The resulting network contains only pure AND/OR/EXOR gates
- and inverters. This procedure is usedful to generate Verilog.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyzDeriveClean( Xyz_Man_t * p, Abc_Ntk_t * pNtk )
-{
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pObj, * pNodeNew;
- int i;
- assert( Abc_NtkIsStrash(pNtk) );
- // perform strashing
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
- // reconstruct the network
- Abc_NtkForEachCo( pNtk, pObj, i )
- {
- pNodeNew = Abc_NtkXyzDeriveNodeInv_rec( p, pNtkNew, Abc_ObjFanin0(pObj), Abc_ObjFaninC0(pObj) );
- Abc_ObjAddFanin( pObj->pCopy, pNodeNew );
- }
- // add the COs
- Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
- // make sure everything is okay
- if ( !Abc_NtkCheck( pNtkNew ) )
- {
- printf( "Abc_NtkXyzDeriveInv: The network check has failed.\n" );
- Abc_NtkDelete( pNtkNew );
- return NULL;
- }
- return pNtkNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzCore.c b/src/opt/xyz/xyzCore.c
deleted file mode 100644
index e5089788..00000000
--- a/src/opt/xyz/xyzCore.c
+++ /dev/null
@@ -1,1025 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzCore.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Core procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
-static int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose );
-static void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary );
-/*
-static int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
-static int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 );
-static int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
-static int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
-static int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
-static int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp );
-*/
-
-static int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj );
-static Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
-static Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp );
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Performs decomposition.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose )
-{
- Abc_Ntk_t * pNtkNew;
- Xyz_Man_t * p;
-
- assert( Abc_NtkIsStrash(pNtk) );
-
- // create the manager
- p = Xyz_ManAlloc( pNtk, nFaninMax );
- p->fUseEsop = fUseEsop;
- p->fUseSop = 1;//fUseSop;
- pNtk->pManCut = p;
-
- // perform mapping
- Abc_NtkXyzCovers( p, pNtk, fVerbose );
-
- // derive the final network
- if ( fUseInvs )
- pNtkNew = Abc_NtkXyzDeriveClean( p, pNtk );
- else
- pNtkNew = Abc_NtkXyzDerive( p, pNtk );
-// pNtkNew = NULL;
-
-
- Xyz_ManFree( p );
- pNtk->pManCut = NULL;
-
- // make sure that everything is okay
- if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
- {
- printf( "Abc_NtkXyz: The network check has failed.\n" );
- Abc_NtkDelete( pNtkNew );
- return NULL;
- }
- return pNtkNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Compute the supports.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkXyzCovers( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
-{
- Abc_Obj_t * pObj;
- int i, clk = clock();
-
- // start the manager
- p->vFanCounts = Abc_NtkFanoutCounts(pNtk);
-
- // set trivial cuts for the constant and the CIs
- pObj = Abc_NtkConst1(pNtk);
- pObj->fMarkA = 1;
- Abc_NtkForEachCi( pNtk, pObj, i )
- pObj->fMarkA = 1;
-
- // perform iterative decomposition
- for ( i = 0; ; i++ )
- {
- if ( fVerbose )
- printf( "Iter %d : ", i+1 );
- if ( Abc_NtkXyzCoversOne(p, pNtk, fVerbose) )
- break;
- }
-
- // clean the cut-point markers
- Abc_NtkForEachObj( pNtk, pObj, i )
- pObj->fMarkA = 0;
-
-if ( fVerbose )
-{
-PRT( "Total", clock() - clk );
-}
-}
-
-/**Function*************************************************************
-
- Synopsis [Compute the supports.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NtkXyzCoversOne( Xyz_Man_t * p, Abc_Ntk_t * pNtk, bool fVerbose )
-{
- ProgressBar * pProgress;
- Abc_Obj_t * pObj;
- Vec_Ptr_t * vBoundary;
- int i, clk = clock();
- int Counter = 0;
- int fStop = 1;
-
- // array to collect the nodes in the new boundary
- vBoundary = Vec_PtrAlloc( 100 );
-
- // start from the COs and mark visited nodes using pObj->fMarkB
- pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
- Abc_NtkForEachCo( pNtk, pObj, i )
- {
- Extra_ProgressBarUpdate( pProgress, i, NULL );
- // skip the solved nodes (including the CIs)
- pObj = Abc_ObjFanin0(pObj);
- if ( pObj->fMarkA )
- {
- Counter++;
- continue;
- }
-
- // traverse the cone starting from this node
- if ( Abc_ObjGetSupp(pObj) == NULL )
- Abc_NtkXyzCovers_rec( p, pObj, vBoundary );
-
- // count the number of solved cones
- if ( Abc_ObjGetSupp(pObj) == NULL )
- fStop = 0;
- else
- Counter++;
-
-/*
- printf( "%-15s : ", Abc_ObjName(pObj) );
- printf( "lev = %5d ", pObj->Level );
- if ( Abc_ObjGetSupp(pObj) == NULL )
- {
- printf( "\n" );
- continue;
- }
- printf( "supp = %3d ", Abc_ObjGetSupp(pObj)->nSize );
- printf( "esop = %3d ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) );
- printf( "\n" );
-*/
- }
- Extra_ProgressBarStop( pProgress );
-
- // clean visited nodes
- Abc_NtkForEachObj( pNtk, pObj, i )
- pObj->fMarkB = 0;
-
- // create the new boundary
- p->nBoundary = 0;
- Vec_PtrForEachEntry( vBoundary, pObj, i )
- {
- if ( !pObj->fMarkA )
- {
- pObj->fMarkA = 1;
- p->nBoundary++;
- }
- }
- Vec_PtrFree( vBoundary );
-
-if ( fVerbose )
-{
- printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d Bound = %4d ",
- Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary );
-PRT( "T", clock() - clk );
-}
- return fStop;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkXyzCovers_rec( Xyz_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vBoundary )
-{
- Abc_Obj_t * pObj0, * pObj1;
- // return if the support is already computed
- if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
- return;
- // mark as visited
- pObj->fMarkB = 1;
- // get the fanins
- pObj0 = Abc_ObjFanin0(pObj);
- pObj1 = Abc_ObjFanin1(pObj);
- // solve for the fanins
- Abc_NtkXyzCovers_rec( p, pObj0, vBoundary );
- Abc_NtkXyzCovers_rec( p, pObj1, vBoundary );
- // skip the node that spaced out
- if ( !pObj0->fMarkA && !Abc_ObjGetSupp(pObj0) || // fanin is not ready
- !pObj1->fMarkA && !Abc_ObjGetSupp(pObj1) || // fanin is not ready
- !Abc_NodeXyzPropagate( p, pObj ) ) // node's support or covers cannot be computed
- {
- // save the nodes of the future boundary
- if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
- Vec_PtrPush( vBoundary, pObj0 );
- if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) )
- Vec_PtrPush( vBoundary, pObj1 );
- return;
- }
- // consider dropping the fanin supports
-// Abc_NodeXyzDropData( p, pObj0 );
-// Abc_NodeXyzDropData( p, pObj1 );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Abc_NodeXyzSupport( Xyz_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1 )
-{
- Vec_Int_t * vSupp;
- int k0, k1;
-
- assert( vSupp0 && vSupp1 );
- Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
- Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
- Vec_IntClear( p->vPairs0 );
- Vec_IntClear( p->vPairs1 );
-
- vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize );
- for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
- {
- if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
- {
- Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
- Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
- Vec_IntPush( p->vPairs0, k0 );
- Vec_IntPush( p->vPairs1, k1 );
- Vec_IntPush( vSupp, vSupp0->pArray[k0] );
- k0++; k1++;
- }
- else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
- {
- Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
- Vec_IntPush( vSupp, vSupp0->pArray[k0] );
- k0++;
- }
- else
- {
- Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
- Vec_IntPush( vSupp, vSupp1->pArray[k1] );
- k1++;
- }
- }
- for ( ; k0 < vSupp0->nSize; k0++ )
- {
- Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
- Vec_IntPush( vSupp, vSupp0->pArray[k0] );
- }
- for ( ; k1 < vSupp1->nSize; k1++ )
- {
- Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
- Vec_IntPush( vSupp, vSupp1->pArray[k1] );
- }
-/*
- printf( "Zero : " );
- for ( k0 = 0; k0 < vSupp0->nSize; k0++ )
- printf( "%d ", vSupp0->pArray[k0] );
- printf( "\n" );
-
- printf( "One : " );
- for ( k1 = 0; k1 < vSupp1->nSize; k1++ )
- printf( "%d ", vSupp1->pArray[k1] );
- printf( "\n" );
-
- printf( "Sum : " );
- for ( k0 = 0; k0 < vSupp->nSize; k0++ )
- printf( "%d ", vSupp->pArray[k0] );
- printf( "\n" );
- printf( "\n" );
-*/
- return vSupp;
-}
-
-/**Function*************************************************************
-
- Synopsis [Propagates all types of covers.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzPropagate( Xyz_Man_t * p, Abc_Obj_t * pObj )
-{
- Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
- Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
- Vec_Int_t * vSupp, * vSupp0, * vSupp1;
- Abc_Obj_t * pObj0, * pObj1;
- int fCompl0, fCompl1;
-
- pObj0 = Abc_ObjFanin0( pObj );
- pObj1 = Abc_ObjFanin1( pObj );
-
- if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
- if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
-
- // get the resulting support
- vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
- vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
- vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
-
- // quit if support if too large
- if ( vSupp->nSize > p->nFaninMax )
- {
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // get the complemented attributes
- fCompl0 = Abc_ObjFaninC0( pObj );
- fCompl1 = Abc_ObjFaninC1( pObj );
-
- // propagate ESOP
- if ( p->fUseEsop )
- {
- // get the covers
- pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
- pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
- if ( pCov0 && pCov1 )
- {
- // complement the first if needed
- if ( !fCompl0 )
- pCover0 = pCov0;
- else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
- pCover0 = pCov0->pNext;
- else
- pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
-
- // complement the second if needed
- if ( !fCompl1 )
- pCover1 = pCov1;
- else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
- pCover1 = pCov1->pNext;
- else
- pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
-
- // derive the new cover
- pCoverX = Abc_NodeXyzProduct( p, pCover0, pCover1, 1, vSupp->nSize );
- }
- }
- // propagate SOPs
- if ( p->fUseSop )
- {
- // get the covers for the direct polarity
- pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
- pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
- // derive the new cover
- if ( pCover0 && pCover1 )
- pCoverP = Abc_NodeXyzProduct( p, pCover0, pCover1, 0, vSupp->nSize );
-
- // get the covers for the inverse polarity
- pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
- pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
- // derive the new cover
- if ( pCover0 && pCover1 )
- pCoverN = Abc_NodeXyzSum( p, pCover0, pCover1, 0, vSupp->nSize );
- }
-
- // if none of the covers can be computed quit
- if ( !pCoverX && !pCoverP && !pCoverN )
- {
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // set the covers
- assert( Abc_ObjGetSupp(pObj) == NULL );
- Abc_ObjSetSupp( pObj, vSupp );
- Abc_ObjSetCover( pObj, pCoverP, 0 );
- Abc_ObjSetCover( pObj, pCoverN, 1 );
- Abc_ObjSetCover2( pObj, pCoverX );
-//printf( "%3d : %4d %4d %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );
-
- // count statistics
- p->nSupps++;
- p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
- return 1;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeXyzProduct( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
-{
- Min_Cube_t * pCube, * pCube0, * pCube1;
- Min_Cube_t * pCover;
- int i, Val0, Val1;
- assert( pCover0 && pCover1 );
-
- // clean storage
- Min_ManClean( p->pManMin, nSupp );
- // go through the cube pairs
- Min_CoverForEachCube( pCover0, pCube0 )
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- // go through the support variables of the cubes
- for ( i = 0; i < p->vPairs0->nSize; i++ )
- {
- Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
- Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
- if ( (Val0 & Val1) == 0 )
- break;
- }
- // check disjointness
- if ( i < p->vPairs0->nSize )
- continue;
-
- if ( p->pManMin->nCubes > p->nCubesMax )
- {
- pCover = Min_CoverCollect( p->pManMin, nSupp );
-//Min_CoverWriteFile( pCover, "large", 1 );
- Min_CoverRecycle( p->pManMin, pCover );
- return NULL;
- }
-
- // create the product cube
- pCube = Min_CubeAlloc( p->pManMin );
-
- // add the literals
- pCube->nLits = 0;
- for ( i = 0; i < nSupp; i++ )
- {
- if ( p->vComTo0->pArray[i] == -1 )
- Val0 = 3;
- else
- Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
-
- if ( p->vComTo1->pArray[i] == -1 )
- Val1 = 3;
- else
- Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
-
- if ( (Val0 & Val1) == 3 )
- continue;
-
- Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
- pCube->nLits++;
- }
- // add the cube to storage
- if ( fEsop )
- Min_EsopAddCube( p->pManMin, pCube );
- else
- Min_SopAddCube( p->pManMin, pCube );
- }
-
- // minimize the cover
- if ( fEsop )
- Min_EsopMinimize( p->pManMin );
- else
- Min_SopMinimize( p->pManMin );
- pCover = Min_CoverCollect( p->pManMin, nSupp );
-
- // quit if the cover is too large
- if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
- {
-/*
-Min_CoverWriteFile( pCover, "large", 1 );
- Min_CoverExpand( p->pManMin, pCover );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- Min_EsopMinimize( p->pManMin );
- pCover = Min_CoverCollect( p->pManMin, nSupp );
-*/
- Min_CoverRecycle( p->pManMin, pCover );
- return NULL;
- }
- return pCover;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeXyzSum( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int fEsop, int nSupp )
-{
- Min_Cube_t * pCube, * pCube0, * pCube1;
- Min_Cube_t * pCover;
- int i, Val0, Val1;
- assert( pCover0 && pCover1 );
-
- // clean storage
- Min_ManClean( p->pManMin, nSupp );
- Min_CoverForEachCube( pCover0, pCube0 )
- {
- // create the cube
- pCube = Min_CubeAlloc( p->pManMin );
- pCube->nLits = 0;
- for ( i = 0; i < p->vComTo0->nSize; i++ )
- {
- if ( p->vComTo0->pArray[i] == -1 )
- continue;
- Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
- if ( Val0 == 3 )
- continue;
- Min_CubeXorVar( pCube, i, Val0 ^ 3 );
- pCube->nLits++;
- }
- if ( p->pManMin->nCubes > p->nCubesMax )
- {
- pCover = Min_CoverCollect( p->pManMin, nSupp );
- Min_CoverRecycle( p->pManMin, pCover );
- return NULL;
- }
- // add the cube to storage
- if ( fEsop )
- Min_EsopAddCube( p->pManMin, pCube );
- else
- Min_SopAddCube( p->pManMin, pCube );
- }
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- // create the cube
- pCube = Min_CubeAlloc( p->pManMin );
- pCube->nLits = 0;
- for ( i = 0; i < p->vComTo1->nSize; i++ )
- {
- if ( p->vComTo1->pArray[i] == -1 )
- continue;
- Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
- if ( Val1 == 3 )
- continue;
- Min_CubeXorVar( pCube, i, Val1 ^ 3 );
- pCube->nLits++;
- }
- if ( p->pManMin->nCubes > p->nCubesMax )
- {
- pCover = Min_CoverCollect( p->pManMin, nSupp );
- Min_CoverRecycle( p->pManMin, pCover );
- return NULL;
- }
- // add the cube to storage
- if ( fEsop )
- Min_EsopAddCube( p->pManMin, pCube );
- else
- Min_SopAddCube( p->pManMin, pCube );
- }
-
- // minimize the cover
- if ( fEsop )
- Min_EsopMinimize( p->pManMin );
- else
- Min_SopMinimize( p->pManMin );
- pCover = Min_CoverCollect( p->pManMin, nSupp );
-
- // quit if the cover is too large
- if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
- {
- Min_CoverRecycle( p->pManMin, pCover );
- return NULL;
- }
- return pCover;
-}
-
-
-
-
-
-
-
-#if 0
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzPropagateEsop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
-{
- Min_Cube_t * pCover, * pCover0, * pCover1, * pCov0, * pCov1;
- Vec_Int_t * vSupp, * vSupp0, * vSupp1;
-
- if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
- if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
-
- // get the resulting support
- vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
- vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
- vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
-
- // quit if support if too large
- if ( vSupp->nSize > p->nFaninMax )
- {
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // get the covers
- pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
- pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
-
- // complement the first if needed
- if ( !Abc_ObjFaninC0(pObj) )
- pCover0 = pCov0;
- else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
- pCover0 = pCov0->pNext;
- else
- pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;
-
- // complement the second if needed
- if ( !Abc_ObjFaninC1(pObj) )
- pCover1 = pCov1;
- else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
- pCover1 = pCov1->pNext;
- else
- pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;
-
- // derive and minimize the cover (quit if too large)
- if ( !Abc_NodeXyzProductEsop( p, pCover0, pCover1, vSupp->nSize ) )
- {
- pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
- Min_CoverRecycle( p->pManMin, pCover );
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // minimize the cover
- Min_EsopMinimize( p->pManMin );
- pCover = Min_CoverCollect( p->pManMin, vSupp->nSize );
-
- // quit if the cover is too large
- if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
- {
- Min_CoverRecycle( p->pManMin, pCover );
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // count statistics
- p->nSupps++;
- p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
-
- // set the covers
- assert( Abc_ObjGetSupp(pObj) == NULL );
- Abc_ObjSetSupp( pObj, vSupp );
- Abc_ObjSetCover2( pObj, pCover );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzPropagateSop( Xyz_Man_t * p, Abc_Obj_t * pObj, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
-{
- Min_Cube_t * pCoverP, * pCoverN, * pCover0, * pCover1;
- Vec_Int_t * vSupp, * vSupp0, * vSupp1;
- int fCompl0, fCompl1;
-
- if ( pObj0->fMarkA ) Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
- if ( pObj1->fMarkA ) Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
-
- // get the resulting support
- vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
- vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
- vSupp = Abc_NodeXyzSupport( p, vSupp0, vSupp1 );
-
- // quit if support if too large
- if ( vSupp->nSize > p->nFaninMax )
- {
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // get the complemented attributes
- fCompl0 = Abc_ObjFaninC0(pObj);
- fCompl1 = Abc_ObjFaninC1(pObj);
-
- // prepare the positive cover
- pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
- pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
-
- // derive and minimize the cover (quit if too large)
- if ( !pCover0 || !pCover1 )
- pCoverP = NULL;
- else if ( !Abc_NodeXyzProductSop( p, pCover0, pCover1, vSupp->nSize ) )
- {
- pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
- Min_CoverRecycle( p->pManMin, pCoverP );
- pCoverP = NULL;
- }
- else
- {
- Min_SopMinimize( p->pManMin );
- pCoverP = Min_CoverCollect( p->pManMin, vSupp->nSize );
- // quit if the cover is too large
- if ( Min_CoverCountCubes(pCoverP) > p->nFaninMax )
- {
- Min_CoverRecycle( p->pManMin, pCoverP );
- pCoverP = NULL;
- }
- }
-
- // prepare the negative cover
- pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
- pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
-
- // derive and minimize the cover (quit if too large)
- if ( !pCover0 || !pCover1 )
- pCoverN = NULL;
- else if ( !Abc_NodeXyzUnionSop( p, pCover0, pCover1, vSupp->nSize ) )
- {
- pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
- Min_CoverRecycle( p->pManMin, pCoverN );
- pCoverN = NULL;
- }
- else
- {
- Min_SopMinimize( p->pManMin );
- pCoverN = Min_CoverCollect( p->pManMin, vSupp->nSize );
- // quit if the cover is too large
- if ( Min_CoverCountCubes(pCoverN) > p->nFaninMax )
- {
- Min_CoverRecycle( p->pManMin, pCoverN );
- pCoverN = NULL;
- }
- }
-
- if ( pCoverP == NULL && pCoverN == NULL )
- {
- Vec_IntFree( vSupp );
- return 0;
- }
-
- // count statistics
- p->nSupps++;
- p->nSuppsMax = ABC_MAX( p->nSuppsMax, p->nSupps );
-
- // set the covers
- assert( Abc_ObjGetSupp(pObj) == NULL );
- Abc_ObjSetSupp( pObj, vSupp );
- Abc_ObjSetCover( pObj, pCoverP, 0 );
- Abc_ObjSetCover( pObj, pCoverN, 1 );
- return 1;
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzProductEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
- Min_Cube_t * pCube, * pCube0, * pCube1;
- int i, Val0, Val1;
-
- // clean storage
- Min_ManClean( p->pManMin, nSupp );
- if ( pCover0 == NULL || pCover1 == NULL )
- return 1;
-
- // go through the cube pairs
- Min_CoverForEachCube( pCover0, pCube0 )
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- // go through the support variables of the cubes
- for ( i = 0; i < p->vPairs0->nSize; i++ )
- {
- Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
- Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
- if ( (Val0 & Val1) == 0 )
- break;
- }
- // check disjointness
- if ( i < p->vPairs0->nSize )
- continue;
-
- if ( p->pManMin->nCubes >= p->nCubesMax )
- return 0;
-
- // create the product cube
- pCube = Min_CubeAlloc( p->pManMin );
-
- // add the literals
- pCube->nLits = 0;
- for ( i = 0; i < nSupp; i++ )
- {
- if ( p->vComTo0->pArray[i] == -1 )
- Val0 = 3;
- else
- Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
-
- if ( p->vComTo1->pArray[i] == -1 )
- Val1 = 3;
- else
- Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
-
- if ( (Val0 & Val1) == 3 )
- continue;
-
- Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
- pCube->nLits++;
- }
- // add the cube to storage
- Min_EsopAddCube( p->pManMin, pCube );
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzProductSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
- return 1;
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzUnionEsop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
- Min_Cube_t * pCube, * pCube0, * pCube1;
- int i, Val0, Val1;
-
- // clean storage
- Min_ManClean( p->pManMin, nSupp );
- if ( pCover0 )
- {
- Min_CoverForEachCube( pCover0, pCube0 )
- {
- // create the cube
- pCube = Min_CubeAlloc( p->pManMin );
- pCube->nLits = 0;
- for ( i = 0; i < p->vComTo0->nSize; i++ )
- {
- if ( p->vComTo0->pArray[i] == -1 )
- continue;
- Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
- if ( Val0 == 3 )
- continue;
- Min_CubeXorVar( pCube, i, Val0 ^ 3 );
- pCube->nLits++;
- }
- if ( p->pManMin->nCubes >= p->nCubesMax )
- return 0;
- // add the cube to storage
- Min_EsopAddCube( p->pManMin, pCube );
- }
- }
- if ( pCover1 )
- {
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- // create the cube
- pCube = Min_CubeAlloc( p->pManMin );
- pCube->nLits = 0;
- for ( i = 0; i < p->vComTo1->nSize; i++ )
- {
- if ( p->vComTo1->pArray[i] == -1 )
- continue;
- Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
- if ( Val1 == 3 )
- continue;
- Min_CubeXorVar( pCube, i, Val1 ^ 3 );
- pCube->nLits++;
- }
- if ( p->pManMin->nCubes >= p->nCubesMax )
- return 0;
- // add the cube to storage
- Min_EsopAddCube( p->pManMin, pCube );
- }
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeXyzUnionSop( Xyz_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1, int nSupp )
-{
- return 1;
-}
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzInt.h b/src/opt/xyz/xyzInt.h
deleted file mode 100644
index 656612aa..00000000
--- a/src/opt/xyz/xyzInt.h
+++ /dev/null
@@ -1,642 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzInt.h]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Internal declarations.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Min_Man_t_ Min_Man_t;
-typedef struct Min_Cube_t_ Min_Cube_t;
-
-struct Min_Man_t_
-{
- int nVars; // the number of vars
- int nWords; // the number of words
- Extra_MmFixed_t * pMemMan; // memory manager for cubes
- // temporary cubes
- Min_Cube_t * pOne0; // tautology cube
- Min_Cube_t * pOne1; // tautology cube
- Min_Cube_t * pTriv0[2]; // trivial cube
- Min_Cube_t * pTriv1[2]; // trivial cube
- Min_Cube_t * pTemp; // cube for computing the distance
- Min_Cube_t * pBubble; // cube used as a separator
- // temporary storage for the new cover
- int nCubes; // the number of cubes
- Min_Cube_t ** ppStore; // storage for cubes by number of literals
-};
-
-struct Min_Cube_t_
-{
- Min_Cube_t * pNext; // the pointer to the next cube in the cover
- unsigned nVars : 10; // the number of variables
- unsigned nWords : 12; // the number of machine words
- unsigned nLits : 10; // the number of literals in the cube
- unsigned uData[1]; // the bit-data for the cube
-};
-
-
-// iterators through the entries in the linked lists of cubes
-#define Min_CoverForEachCube( pCover, pCube ) \
- for ( pCube = pCover; \
- pCube; \
- pCube = pCube->pNext )
-#define Min_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \
- for ( pCube = pCover, \
- pCube2 = pCube? pCube->pNext: NULL; \
- pCube; \
- pCube = pCube2, \
- pCube2 = pCube? pCube->pNext: NULL )
-#define Min_CoverForEachCubePrev( pCover, pCube, ppPrev ) \
- for ( pCube = pCover, \
- ppPrev = &(pCover); \
- pCube; \
- ppPrev = &pCube->pNext, \
- pCube = pCube->pNext )
-
-// macros to get hold of bits and values in the cubes
-static inline int Min_CubeHasBit( Min_Cube_t * p, int i ) { return (p->uData[(i)>>5] & (1<<((i) & 31))) > 0; }
-static inline void Min_CubeSetBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] |= (1<<((i) & 31)); }
-static inline void Min_CubeXorBit( Min_Cube_t * p, int i ) { p->uData[(i)>>5] ^= (1<<((i) & 31)); }
-static inline int Min_CubeGetVar( Min_Cube_t * p, int Var ) { return 3 & (p->uData[(2*Var)>>5] >> ((2*Var) & 31)); }
-static inline void Min_CubeXorVar( Min_Cube_t * p, int Var, int Value ) { p->uData[(2*Var)>>5] ^= (Value<<((2*Var) & 31)); }
-
-/*=== xyzMinEsop.c ==========================================================*/
-extern void Min_EsopMinimize( Min_Man_t * p );
-extern void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
-/*=== xyzMinSop.c ==========================================================*/
-extern void Min_SopMinimize( Min_Man_t * p );
-extern void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube );
-/*=== xyzMinMan.c ==========================================================*/
-extern Min_Man_t * Min_ManAlloc( int nVars );
-extern void Min_ManClean( Min_Man_t * p, int nSupp );
-extern void Min_ManFree( Min_Man_t * p );
-/*=== xyzMinUtil.c ==========================================================*/
-extern void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube );
-extern void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover );
-extern void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p );
-extern void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop );
-extern void Min_CoverCheck( Min_Man_t * p );
-extern int Min_CubeCheck( Min_Cube_t * pCube );
-extern Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize );
-extern void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover );
-extern int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Creates the cube.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeAlloc( Min_Man_t * p )
-{
- Min_Cube_t * pCube;
- pCube = (Min_Cube_t *)Extra_MmFixedEntryFetch( p->pMemMan );
- pCube->pNext = NULL;
- pCube->nVars = p->nVars;
- pCube->nWords = p->nWords;
- pCube->nLits = 0;
- memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords );
- return pCube;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the cube representing elementary var.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeAllocVar( Min_Man_t * p, int iVar, int fCompl )
-{
- Min_Cube_t * pCube;
- pCube = Min_CubeAlloc( p );
- Min_CubeXorBit( pCube, iVar*2+fCompl );
- pCube->nLits = 1;
- return pCube;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the cube.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubeDup( Min_Man_t * p, Min_Cube_t * pCopy )
-{
- Min_Cube_t * pCube;
- pCube = Min_CubeAlloc( p );
- memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords );
- pCube->nLits = pCopy->nLits;
- return pCube;
-}
-
-/**Function*************************************************************
-
- Synopsis [Recycles the cube.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CubeRecycle( Min_Man_t * p, Min_Cube_t * pCube )
-{
- Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
-}
-
-/**Function*************************************************************
-
- Synopsis [Recycles the cube cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CoverRecycle( Min_Man_t * p, Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube, * pCube2;
- Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- Extra_MmFixedEntryRecycle( p->pMemMan, (char *)pCube );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of cubes in the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubeCountLits( Min_Cube_t * pCube )
-{
- unsigned uData;
- int Count = 0, i, w;
- for ( w = 0; w < (int)pCube->nWords; w++ )
- {
- uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
- for ( i = 0; i < 32; i += 2 )
- if ( uData & (1 << i) )
- Count++;
- }
- return Count;
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of cubes in the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CubeGetLits( Min_Cube_t * pCube, Vec_Int_t * vLits )
-{
- unsigned uData;
- int i, w;
- Vec_IntClear( vLits );
- for ( w = 0; w < (int)pCube->nWords; w++ )
- {
- uData = pCube->uData[w] ^ (pCube->uData[w] >> 1);
- for ( i = 0; i < 32; i += 2 )
- if ( uData & (1 << i) )
- Vec_IntPush( vLits, w*16 + i/2 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Counts the number of cubes in the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CoverCountCubes( Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube;
- int Count = 0;
- Min_CoverForEachCube( pCover, pCube )
- Count++;
- return Count;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Checks if two cubes are disjoint.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubesDisjoint( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
- unsigned uData;
- int i;
- assert( pCube0->nVars == pCube1->nVars );
- for ( i = 0; i < (int)pCube0->nWords; i++ )
- {
- uData = pCube0->uData[i] & pCube1->uData[i];
- uData = (uData | (uData >> 1)) & 0x55555555;
- if ( uData != 0x55555555 )
- return 1;
- }
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects the disjoint variables of the two cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CoverGetDisjVars( Min_Cube_t * pThis, Min_Cube_t * pCube, Vec_Int_t * vVars )
-{
- unsigned uData;
- int i, w;
- Vec_IntClear( vVars );
- for ( w = 0; w < (int)pCube->nWords; w++ )
- {
- uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555;
- uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1));
- if ( uData == 0 )
- continue;
- for ( i = 0; i < 32; i += 2 )
- if ( uData & (1 << i) )
- Vec_IntPush( vVars, w*16 + i/2 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks if two cubes are disjoint.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubesDistOne( Min_Cube_t * pCube0, Min_Cube_t * pCube1, Min_Cube_t * pTemp )
-{
- unsigned uData;
- int i, fFound = 0;
- for ( i = 0; i < (int)pCube0->nWords; i++ )
- {
- uData = pCube0->uData[i] ^ pCube1->uData[i];
- if ( uData == 0 )
- {
- if ( pTemp ) pTemp->uData[i] = 0;
- continue;
- }
- if ( fFound )
- return 0;
- uData = (uData | (uData >> 1)) & 0x55555555;
- if ( (uData & (uData-1)) > 0 ) // more than one 1
- return 0;
- if ( pTemp ) pTemp->uData[i] = uData | (uData << 1);
- fFound = 1;
- }
- if ( fFound == 0 )
- {
- printf( "\n" );
- Min_CubeWrite( stdout, pCube0 );
- Min_CubeWrite( stdout, pCube1 );
- printf( "Error: Min_CubesDistOne() looks at two equal cubes!\n" );
- }
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Checks if two cubes are disjoint.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubesDistTwo( Min_Cube_t * pCube0, Min_Cube_t * pCube1, int * pVar0, int * pVar1 )
-{
- unsigned uData;//, uData2;
- int i, k, Var0 = -1, Var1 = -1;
- for ( i = 0; i < (int)pCube0->nWords; i++ )
- {
- uData = pCube0->uData[i] ^ pCube1->uData[i];
- if ( uData == 0 )
- continue;
- if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s
- return 0;
- uData = (uData | (uData >> 1)) & 0x55555555;
- if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 )
- return 0;
- for ( k = 0; k < 32; k += 2 )
- if ( uData & (1 << k) )
- {
- if ( Var0 == -1 )
- Var0 = 16 * i + k/2;
- else if ( Var1 == -1 )
- Var1 = 16 * i + k/2;
- else
- return 0;
- }
- /*
- if ( Var0 >= 0 )
- {
- uData &= 0xFFFF;
- uData2 = (uData >> 16);
- if ( uData && uData2 )
- return 0;
- if ( uData )
- {
- }
- uData }= uData2;
- uData &= 0x
- }
- */
- }
- if ( Var0 >= 0 && Var1 >= 0 )
- {
- *pVar0 = Var0;
- *pVar1 = Var1;
- return 1;
- }
- if ( Var0 == -1 || Var1 == -1 )
- {
- printf( "\n" );
- Min_CubeWrite( stdout, pCube0 );
- Min_CubeWrite( stdout, pCube1 );
- printf( "Error: Min_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" );
- }
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Makes the produce of two cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubesProduct( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
- Min_Cube_t * pCube;
- int i;
- assert( pCube0->nVars == pCube1->nVars );
- pCube = Min_CubeAlloc( p );
- for ( i = 0; i < p->nWords; i++ )
- pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i];
- pCube->nLits = Min_CubeCountLits( pCube );
- return pCube;
-}
-
-/**Function*************************************************************
-
- Synopsis [Makes the produce of two cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline Min_Cube_t * Min_CubesXor( Min_Man_t * p, Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
- Min_Cube_t * pCube;
- int i;
- assert( pCube0->nVars == pCube1->nVars );
- pCube = Min_CubeAlloc( p );
- for ( i = 0; i < p->nWords; i++ )
- pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i];
- pCube->nLits = Min_CubeCountLits( pCube );
- return pCube;
-}
-
-/**Function*************************************************************
-
- Synopsis [Makes the produce of two cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubesAreEqual( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
- int i;
- for ( i = 0; i < (int)pCube0->nWords; i++ )
- if ( pCube0->uData[i] != pCube1->uData[i] )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CubeIsContained( Min_Cube_t * pCube0, Min_Cube_t * pCube1 )
-{
- int i;
- for ( i = 0; i < (int)pCube0->nWords; i++ )
- if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Transforms the cube into the result of merging.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CubesTransform( Min_Cube_t * pCube, Min_Cube_t * pDist, Min_Cube_t * pMask )
-{
- int w;
- for ( w = 0; w < (int)pCube->nWords; w++ )
- {
- pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w];
- pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]);
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Transforms the cube into the result of distance-1 merging.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CubesTransformOr( Min_Cube_t * pCube, Min_Cube_t * pDist )
-{
- int w;
- for ( w = 0; w < (int)pCube->nWords; w++ )
- pCube->uData[w] |= pDist->uData[w];
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis [Sorts the cover in the increasing number of literals.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Min_CoverExpandRemoveEqual( Min_Man_t * p, Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube, * pCube2, * pThis;
- if ( pCover == NULL )
- {
- Min_ManClean( p, p->nVars );
- return;
- }
- Min_ManClean( p, pCover->nVars );
- Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- {
- // go through the linked list
- Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
- if ( Min_CubesAreEqual( pCube, pThis ) )
- {
- Min_CubeRecycle( p, pCube );
- break;
- }
- if ( pThis != NULL )
- continue;
- pCube->pNext = p->ppStore[pCube->nLits];
- p->ppStore[pCube->nLits] = pCube;
- p->nCubes++;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int Min_CoverContainsCube( Min_Man_t * p, Min_Cube_t * pCube )
-{
- Min_Cube_t * pThis;
- int i;
-/*
- // this cube cannot be equal to any cube
- Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
- {
- if ( Min_CubesAreEqual( pCube, pThis ) )
- {
- Min_CubeWrite( stdout, pCube );
- assert( 0 );
- }
- }
-*/
- // try to find a containing cube
- for ( i = 0; i <= (int)pCube->nLits; i++ )
- Min_CoverForEachCube( p->ppStore[i], pThis )
- {
- // skip the bubble
- if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
- return 1;
- }
- return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzMan.c b/src/opt/xyz/xyzMan.c
deleted file mode 100644
index 844e8c13..00000000
--- a/src/opt/xyz/xyzMan.c
+++ /dev/null
@@ -1,144 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzMan.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Decomposition manager.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Xyz_Man_t * Xyz_ManAlloc( Abc_Ntk_t * pNtk, int nFaninMax )
-{
- Xyz_Man_t * pMan;
- Xyz_Obj_t * pMem;
- Abc_Obj_t * pObj;
- int i;
- assert( pNtk->pManCut == NULL );
-
- // start the manager
- pMan = ALLOC( Xyz_Man_t, 1 );
- memset( pMan, 0, sizeof(Xyz_Man_t) );
- pMan->nFaninMax = nFaninMax;
- pMan->nCubesMax = 2 * pMan->nFaninMax;
- pMan->nWords = Abc_BitWordNum( nFaninMax * 2 );
-
- // get the cubes
- pMan->vComTo0 = Vec_IntAlloc( 2*nFaninMax );
- pMan->vComTo1 = Vec_IntAlloc( 2*nFaninMax );
- pMan->vPairs0 = Vec_IntAlloc( nFaninMax );
- pMan->vPairs1 = Vec_IntAlloc( nFaninMax );
- pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 );
- pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 );
-
- // allocate memory for object structures
- pMan->pMemory = pMem = ALLOC( Xyz_Obj_t, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
- memset( pMem, 0, sizeof(Xyz_Obj_t) * Abc_NtkObjNumMax(pNtk) );
- // allocate storage for the pointers to the memory
- pMan->vObjStrs = Vec_PtrAlloc( Abc_NtkObjNumMax(pNtk) );
- Vec_PtrFill( pMan->vObjStrs, Abc_NtkObjNumMax(pNtk), NULL );
- Abc_NtkForEachObj( pNtk, pObj, i )
- Vec_PtrWriteEntry( pMan->vObjStrs, i, pMem + i );
- // create the cube manager
- pMan->pManMin = Min_ManAlloc( nFaninMax );
- return pMan;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Xyz_ManFree( Xyz_Man_t * p )
-{
- Vec_Int_t * vSupp;
- int i;
- for ( i = 0; i < p->vObjStrs->nSize; i++ )
- {
- vSupp = ((Xyz_Obj_t *)p->vObjStrs->pArray[i])->vSupp;
- if ( vSupp ) Vec_IntFree( vSupp );
- }
-
- Min_ManFree( p->pManMin );
- Vec_PtrFree( p->vObjStrs );
- Vec_IntFree( p->vFanCounts );
- Vec_IntFree( p->vTriv0 );
- Vec_IntFree( p->vTriv1 );
- Vec_IntFree( p->vComTo0 );
- Vec_IntFree( p->vComTo1 );
- Vec_IntFree( p->vPairs0 );
- Vec_IntFree( p->vPairs1 );
- free( p->pMemory );
- free( p );
-}
-
-/**Function*************************************************************
-
- Synopsis [Drop the covers at the node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj )
-{
- int nFanouts;
- assert( p->vFanCounts );
- nFanouts = Vec_IntEntry( p->vFanCounts, pObj->Id );
- assert( nFanouts > 0 );
- if ( --nFanouts == 0 )
- {
- Vec_IntFree( Abc_ObjGetSupp(pObj) );
- Abc_ObjSetSupp( pObj, NULL );
- Min_CoverRecycle( p->pManMin, Abc_ObjGetCover2(pObj) );
- Abc_ObjSetCover2( pObj, NULL );
- p->nSupps--;
- }
- Vec_IntWriteEntry( p->vFanCounts, pObj->Id, nFanouts );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzMinEsop.c b/src/opt/xyz/xyzMinEsop.c
deleted file mode 100644
index 839e2410..00000000
--- a/src/opt/xyz/xyzMinEsop.c
+++ /dev/null
@@ -1,299 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzMinEsop.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [ESOP manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzMinEsop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static void Min_EsopRewrite( Min_Man_t * p );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_EsopMinimize( Min_Man_t * p )
-{
- int nCubesInit, nCubesOld, nIter;
- if ( p->nCubes < 3 )
- return;
- nIter = 0;
- nCubesInit = p->nCubes;
- do {
- nCubesOld = p->nCubes;
- Min_EsopRewrite( p );
- nIter++;
- }
- while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
-
-// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs one round of rewriting using distance 2 cubes.]
-
- Description [The weakness of this procedure is that it tries each cube
- with only one distance-2 cube. If this pair does not lead to improvement
- the cube is inserted into the cover anyhow, and we try another pair.
- A possible improvement would be to try this cube with all distance-2
- cubes, until an improvement is found, or until all such cubes are tried.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_EsopRewrite( Min_Man_t * p )
-{
- Min_Cube_t * pCube, ** ppPrev;
- Min_Cube_t * pThis, ** ppPrevT;
- int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
- int nPairs = 0;
-
- // insert the bubble before the first cube
- p->pBubble->pNext = p->ppStore[0];
- p->ppStore[0] = p->pBubble;
- p->pBubble->nLits = 0;
-
- // go through the cubes
- while ( 1 )
- {
- // get the index of the bubble
- Index = p->pBubble->nLits;
-
- // find the bubble
- Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
- if ( pCube == p->pBubble )
- break;
- assert( pCube == p->pBubble );
-
- // remove the bubble, get the next cube after the bubble
- *ppPrev = p->pBubble->pNext;
- pCube = p->pBubble->pNext;
- if ( pCube == NULL )
- for ( Index++; Index <= p->nVars; Index++ )
- if ( p->ppStore[Index] )
- {
- ppPrev = &(p->ppStore[Index]);
- pCube = p->ppStore[Index];
- break;
- }
- // stop if there is no more cubes
- if ( pCube == NULL )
- break;
-
- // find the first dist2 cube
- Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
- if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
- break;
- if ( pThis == NULL && Index < p->nVars )
- Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
- if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
- break;
- if ( pThis == NULL && Index < p->nVars - 1 )
- Min_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
- if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
- break;
- // continue if there is no dist2 cube
- if ( pThis == NULL )
- {
- // insert the bubble after the cube
- p->pBubble->pNext = pCube->pNext;
- pCube->pNext = p->pBubble;
- p->pBubble->nLits = pCube->nLits;
- continue;
- }
- nPairs++;
-
- // remove the cubes, insert the bubble instead of pCube
- *ppPrevT = pThis->pNext;
- *ppPrev = p->pBubble;
- p->pBubble->pNext = pCube->pNext;
- p->pBubble->nLits = pCube->nLits;
- p->nCubes -= 2;
-
- // Exorlink-2:
- // A{v00} B{v01} + A{v10} B{v11} =
- // A{v00+v10} B{v01} + A{v10} B{v01+v11} =
- // A{v00} B{v01+v11} + A{v00+v10} B{v11}
-
- // save the dist2 parameters
- v00 = Min_CubeGetVar( pCube, Var0 );
- v01 = Min_CubeGetVar( pCube, Var1 );
- v10 = Min_CubeGetVar( pThis, Var0 );
- v11 = Min_CubeGetVar( pThis, Var1 );
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
- // derive the first pair of resulting cubes
- Min_CubeXorVar( pCube, Var0, v10 );
- pCube->nLits -= (v00 != 3);
- pCube->nLits += ((v00 ^ v10) != 3);
- Min_CubeXorVar( pThis, Var1, v01 );
- pThis->nLits -= (v11 != 3);
- pThis->nLits += ((v01 ^ v11) != 3);
-
- // add the cubes
- nCubesOld = p->nCubes;
- Min_EsopAddCube( p, pCube );
- Min_EsopAddCube( p, pThis );
- // check if the cubes were absorbed
- if ( p->nCubes < nCubesOld + 2 )
- continue;
-
- // pull out both cubes
- assert( pThis == p->ppStore[pThis->nLits] );
- p->ppStore[pThis->nLits] = pThis->pNext;
- assert( pCube == p->ppStore[pCube->nLits] );
- p->ppStore[pCube->nLits] = pCube->pNext;
- p->nCubes -= 2;
-
- // derive the second pair of resulting cubes
- Min_CubeXorVar( pCube, Var0, v10 );
- pCube->nLits -= ((v00 ^ v10) != 3);
- pCube->nLits += (v00 != 3);
- Min_CubeXorVar( pCube, Var1, v11 );
- pCube->nLits -= (v01 != 3);
- pCube->nLits += ((v01 ^ v11) != 3);
-
- Min_CubeXorVar( pThis, Var0, v00 );
- pThis->nLits -= (v10 != 3);
- pThis->nLits += ((v00 ^ v10) != 3);
- Min_CubeXorVar( pThis, Var1, v01 );
- pThis->nLits -= ((v01 ^ v11) != 3);
- pThis->nLits += (v11 != 3);
-
- // add them anyhow
- Min_EsopAddCube( p, pCube );
- Min_EsopAddCube( p, pThis );
- }
-// printf( "Pairs = %d ", nPairs );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds the cube to storage.]
-
- Description [Returns 0 if the cube is added or removed. Returns 1
- if the cube is glued with some other cube and has to be added again.
- Do not forget to clean the storage!]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Min_EsopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
-{
- Min_Cube_t * pThis, ** ppPrev;
- // try to find the identical cube
- Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
- {
- if ( Min_CubesAreEqual( pCube, pThis ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubeRecycle( p, pCube );
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- return 0;
- }
- }
- // find a distance-1 cube if it exists
- if ( pCube->nLits < pCube->nVars )
- Min_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
- {
- if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubesTransform( pCube, pThis, p->pTemp );
- pCube->nLits++;
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- return 1;
- }
- }
- Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
- {
- if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubesTransform( pCube, pThis, p->pTemp );
- pCube->nLits--;
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- return 1;
- }
- }
- if ( pCube->nLits > 0 )
- Min_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
- {
- if ( Min_CubesDistOne( pCube, pThis, p->pTemp ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubesTransform( pCube, pThis, p->pTemp );
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- return 1;
- }
- }
- // add the cube
- pCube->pNext = p->ppStore[pCube->nLits];
- p->ppStore[pCube->nLits] = pCube;
- p->nCubes++;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds the cube to storage.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_EsopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
-{
- assert( pCube != p->pBubble );
- assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
- while ( Min_EsopAddCubeInt( p, pCube ) );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzMinMan.c b/src/opt/xyz/xyzMinMan.c
deleted file mode 100644
index 20314698..00000000
--- a/src/opt/xyz/xyzMinMan.c
+++ /dev/null
@@ -1,113 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzMinMan.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [SOP manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzMinMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Starts the minimization manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Man_t * Min_ManAlloc( int nVars )
-{
- Min_Man_t * pMan;
- // start the manager
- pMan = ALLOC( Min_Man_t, 1 );
- memset( pMan, 0, sizeof(Min_Man_t) );
- pMan->nVars = nVars;
- pMan->nWords = Abc_BitWordNum( nVars * 2 );
- pMan->pMemMan = Extra_MmFixedStart( sizeof(Min_Cube_t) + sizeof(unsigned) * (pMan->nWords - 1) );
- // allocate storage for the temporary cover
- pMan->ppStore = ALLOC( Min_Cube_t *, pMan->nVars + 1 );
- // create tautology cubes
- Min_ManClean( pMan, nVars );
- pMan->pOne0 = Min_CubeAlloc( pMan );
- pMan->pOne1 = Min_CubeAlloc( pMan );
- pMan->pTemp = Min_CubeAlloc( pMan );
- pMan->pBubble = Min_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0;
- // create trivial cubes
- Min_ManClean( pMan, 1 );
- pMan->pTriv0[0] = Min_CubeAllocVar( pMan, 0, 0 );
- pMan->pTriv0[1] = Min_CubeAllocVar( pMan, 0, 1 );
- pMan->pTriv1[0] = Min_CubeAllocVar( pMan, 0, 0 );
- pMan->pTriv1[1] = Min_CubeAllocVar( pMan, 0, 1 );
- Min_ManClean( pMan, nVars );
- return pMan;
-}
-
-/**Function*************************************************************
-
- Synopsis [Cleans the minimization manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_ManClean( Min_Man_t * p, int nSupp )
-{
- // set the size of the cube manager
- p->nVars = nSupp;
- p->nWords = Abc_BitWordNum(2*nSupp);
- // clean the storage
- memset( p->ppStore, 0, sizeof(Min_Cube_t *) * (nSupp + 1) );
- p->nCubes = 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Stops the minimization manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_ManFree( Min_Man_t * p )
-{
- Extra_MmFixedStop ( p->pMemMan, 0 );
- free( p->ppStore );
- free( p );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzMinSop.c b/src/opt/xyz/xyzMinSop.c
deleted file mode 100644
index a5d57c66..00000000
--- a/src/opt/xyz/xyzMinSop.c
+++ /dev/null
@@ -1,615 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzMinSop.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [SOP manipulation.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzMinSop.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static void Min_SopRewrite( Min_Man_t * p );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_SopMinimize( Min_Man_t * p )
-{
- int nCubesInit, nCubesOld, nIter;
- if ( p->nCubes < 3 )
- return;
- nIter = 0;
- nCubesInit = p->nCubes;
- do {
- nCubesOld = p->nCubes;
- Min_SopRewrite( p );
- nIter++;
-// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
- }
- while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
-// printf( "\n" );
-
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_SopRewrite( Min_Man_t * p )
-{
- Min_Cube_t * pCube, ** ppPrev;
- Min_Cube_t * pThis, ** ppPrevT;
- Min_Cube_t * pTemp;
- int v00, v01, v10, v11, Var0, Var1, Index, fCont0, fCont1, nCubesOld;
- int nPairs = 0;
-/*
- {
- Min_Cube_t * pCover;
- pCover = Min_CoverCollect( p, p->nVars );
-printf( "\n\n" );
-Min_CoverWrite( stdout, pCover );
- Min_CoverExpand( p, pCover );
- }
-*/
-
- // insert the bubble before the first cube
- p->pBubble->pNext = p->ppStore[0];
- p->ppStore[0] = p->pBubble;
- p->pBubble->nLits = 0;
-
- // go through the cubes
- while ( 1 )
- {
- // get the index of the bubble
- Index = p->pBubble->nLits;
-
- // find the bubble
- Min_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
- if ( pCube == p->pBubble )
- break;
- assert( pCube == p->pBubble );
-
- // remove the bubble, get the next cube after the bubble
- *ppPrev = p->pBubble->pNext;
- pCube = p->pBubble->pNext;
- if ( pCube == NULL )
- for ( Index++; Index <= p->nVars; Index++ )
- if ( p->ppStore[Index] )
- {
- ppPrev = &(p->ppStore[Index]);
- pCube = p->ppStore[Index];
- break;
- }
- // stop if there is no more cubes
- if ( pCube == NULL )
- break;
-
- // find the first dist2 cube
- Min_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
- if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
- break;
- if ( pThis == NULL && Index < p->nVars )
- Min_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
- if ( Min_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
- break;
- // continue if there is no dist2 cube
- if ( pThis == NULL )
- {
- // insert the bubble after the cube
- p->pBubble->pNext = pCube->pNext;
- pCube->pNext = p->pBubble;
- p->pBubble->nLits = pCube->nLits;
- continue;
- }
- nPairs++;
-/*
-printf( "\n" );
-Min_CubeWrite( stdout, pCube );
-Min_CubeWrite( stdout, pThis );
-*/
- // remove the cubes, insert the bubble instead of pCube
- *ppPrevT = pThis->pNext;
- *ppPrev = p->pBubble;
- p->pBubble->pNext = pCube->pNext;
- p->pBubble->nLits = pCube->nLits;
- p->nCubes -= 2;
-
- assert( pCube != p->pBubble && pThis != p->pBubble );
-
-
- // save the dist2 parameters
- v00 = Min_CubeGetVar( pCube, Var0 );
- v01 = Min_CubeGetVar( pCube, Var1 );
- v10 = Min_CubeGetVar( pThis, Var0 );
- v11 = Min_CubeGetVar( pThis, Var1 );
- assert( v00 != v10 && v01 != v11 );
- assert( v00 != 3 || v01 != 3 );
- assert( v10 != 3 || v11 != 3 );
-
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
-
- // consider the case when both cubes have non-empty literals
- if ( v00 != 3 && v01 != 3 && v10 != 3 && v11 != 3 )
- {
- assert( v00 == (v10 ^ 3) );
- assert( v01 == (v11 ^ 3) );
- // create the temporary cube equal to the first corner
- Min_CubeXorVar( pCube, Var0, 3 );
- // check if this cube is contained
- fCont0 = Min_CoverContainsCube( p, pCube );
- // create the temporary cube equal to the first corner
- Min_CubeXorVar( pCube, Var0, 3 );
- Min_CubeXorVar( pCube, Var1, 3 );
-//printf( "\n" );
-//Min_CubeWrite( stdout, pCube );
-//Min_CubeWrite( stdout, pThis );
- // check if this cube is contained
- fCont1 = Min_CoverContainsCube( p, pCube );
- // undo the change
- Min_CubeXorVar( pCube, Var1, 3 );
-
- // check if the cubes can be overwritten
- if ( fCont0 && fCont1 )
- {
- // one of the cubes can be recycled, the other expanded and added
- Min_CubeRecycle( p, pThis );
- // remove the literals
- Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
- Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
- pCube->nLits -= 2;
- Min_SopAddCube( p, pCube );
- }
- else if ( fCont0 )
- {
- // expand both cubes and add them
- Min_CubeXorVar( pCube, Var0, v00 ^ 3 );
- pCube->nLits--;
- Min_SopAddCube( p, pCube );
- Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
- pThis->nLits--;
- Min_SopAddCube( p, pThis );
- }
- else if ( fCont1 )
- {
- // expand both cubes and add them
- Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
- pCube->nLits--;
- Min_SopAddCube( p, pCube );
- Min_CubeXorVar( pThis, Var0, v10 ^ 3 );
- pThis->nLits--;
- Min_SopAddCube( p, pThis );
- }
- else
- {
- Min_SopAddCube( p, pCube );
- Min_SopAddCube( p, pThis );
- }
- // otherwise, no change is possible
- continue;
- }
-
- // if one of them does not have DC lit, move it
- if ( v00 != 3 && v01 != 3 )
- {
- assert( v10 == 3 || v11 == 3 );
- pTemp = pCube; pCube = pThis; pThis = pTemp;
- Index = v00; v00 = v10; v10 = Index;
- Index = v01; v01 = v11; v11 = Index;
- }
-
- // make sure the first cube has first var DC
- if ( v00 != 3 )
- {
- assert( v01 == 3 );
- Index = Var0; Var0 = Var1; Var1 = Index;
- Index = v00; v00 = v01; v01 = Index;
- Index = v10; v10 = v11; v11 = Index;
- }
-
- // consider both cases: both have DC lit
- if ( v00 == 3 && v11 == 3 )
- {
- assert( v01 != 3 && v10 != 3 );
- // try the remaining minterm
- // create the temporary cube equal to the first corner
- Min_CubeXorVar( pCube, Var0, v10 );
- Min_CubeXorVar( pCube, Var1, 3 );
- pCube->nLits++;
- // check if this cube is contained
- fCont0 = Min_CoverContainsCube( p, pCube );
- // undo the cube transformations
- Min_CubeXorVar( pCube, Var0, v10 );
- Min_CubeXorVar( pCube, Var1, 3 );
- pCube->nLits--;
- // check the case when both are covered
- if ( fCont0 )
- {
- // one of the cubes can be recycled, the other expanded and added
- Min_CubeRecycle( p, pThis );
- // remove the literals
- Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
- pCube->nLits--;
- Min_SopAddCube( p, pCube );
- }
- else
- {
- // try two reduced cubes
- Min_CubeXorVar( pCube, Var0, v10 );
- pCube->nLits++;
- // remember the cubes
- nCubesOld = p->nCubes;
- Min_SopAddCube( p, pCube );
- // check if the cube is absorbed
- if ( p->nCubes < nCubesOld + 1 )
- { // absorbed - add the second cube
- Min_SopAddCube( p, pThis );
- }
- else
- { // remove this cube, and try another one
- assert( pCube == p->ppStore[pCube->nLits] );
- p->ppStore[pCube->nLits] = pCube->pNext;
- p->nCubes--;
-
- // return the cube to the previous state
- Min_CubeXorVar( pCube, Var0, v10 );
- pCube->nLits--;
-
- // generate another reduced cube
- Min_CubeXorVar( pThis, Var1, v01 );
- pThis->nLits++;
-
- // add both cubes
- Min_SopAddCube( p, pCube );
- Min_SopAddCube( p, pThis );
- }
- }
- }
- else // the first cube has DC lit
- {
- assert( v01 != 3 && v10 != 3 && v11 != 3 );
- // try the remaining minterm
- // create the temporary cube equal to the minterm
- Min_CubeXorVar( pThis, Var0, 3 );
- // check if this cube is contained
- fCont0 = Min_CoverContainsCube( p, pThis );
- // undo the cube transformations
- Min_CubeXorVar( pThis, Var0, 3 );
- // check the case when both are covered
- if ( fCont0 )
- {
- // one of the cubes can be recycled, the other expanded and added
- Min_CubeRecycle( p, pThis );
- // remove the literals
- Min_CubeXorVar( pCube, Var1, v01 ^ 3 );
- pCube->nLits--;
- Min_SopAddCube( p, pCube );
- }
- else
- {
- // try reshaping the cubes
- // reduce the first cube
- Min_CubeXorVar( pCube, Var0, v10 );
- pCube->nLits++;
- // expand the second cube
- Min_CubeXorVar( pThis, Var1, v11 ^ 3 );
- pThis->nLits--;
- // add both cubes
- Min_SopAddCube( p, pCube );
- Min_SopAddCube( p, pThis );
- }
- }
- }
-// printf( "Pairs = %d ", nPairs );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds cube to the SOP cover stored in the manager.]
-
- Description [Returns 0 if the cube is added or removed. Returns 1
- if the cube is glued with some other cube and has to be added again.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Min_SopAddCubeInt( Min_Man_t * p, Min_Cube_t * pCube )
-{
- Min_Cube_t * pThis, * pThis2, ** ppPrev;
- int i;
- // try to find the identical cube
- Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
- {
- if ( Min_CubesAreEqual( pCube, pThis ) )
- {
- Min_CubeRecycle( p, pCube );
- return 0;
- }
- }
- // try to find a containing cube
- for ( i = 0; i < (int)pCube->nLits; i++ )
- Min_CoverForEachCube( p->ppStore[i], pThis )
- {
- if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
- {
- Min_CubeRecycle( p, pCube );
- return 0;
- }
- }
- // try to find distance one in the same bin
- Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
- {
- if ( Min_CubesDistOne( pCube, pThis, NULL ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubesTransformOr( pCube, pThis );
- pCube->nLits--;
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- return 1;
- }
- }
-
- // clean the other cubes using this one
- for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
- {
- ppPrev = &p->ppStore[i];
- Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
- {
- if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
- {
- *ppPrev = pThis->pNext;
- Min_CubeRecycle( p, pThis );
- p->nCubes--;
- }
- else
- ppPrev = &pThis->pNext;
- }
- }
-
- // add the cube
- pCube->pNext = p->ppStore[pCube->nLits];
- p->ppStore[pCube->nLits] = pCube;
- p->nCubes++;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds the cube to storage.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_SopAddCube( Min_Man_t * p, Min_Cube_t * pCube )
-{
- assert( Min_CubeCheck( pCube ) );
- assert( pCube != p->pBubble );
- assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
- while ( Min_SopAddCubeInt( p, pCube ) );
-}
-
-
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_SopContain( Min_Man_t * p )
-{
- Min_Cube_t * pCube, * pCube2, ** ppPrev;
- int i, k;
- for ( i = 0; i <= p->nVars; i++ )
- {
- Min_CoverForEachCube( p->ppStore[i], pCube )
- Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
- {
- if ( !Min_CubesAreEqual( pCube, pCube2 ) )
- continue;
- *ppPrev = pCube2->pNext;
- Min_CubeRecycle( p, pCube2 );
- p->nCubes--;
- }
- for ( k = i + 1; k <= p->nVars; k++ )
- Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
- {
- if ( !Min_CubeIsContained( pCube, pCube2 ) )
- continue;
- *ppPrev = pCube2->pNext;
- Min_CubeRecycle( p, pCube2 );
- p->nCubes--;
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_SopDist1Merge( Min_Man_t * p )
-{
- Min_Cube_t * pCube, * pCube2, * pCubeNew;
- int i;
- for ( i = p->nVars; i >= 0; i-- )
- {
- Min_CoverForEachCube( p->ppStore[i], pCube )
- Min_CoverForEachCube( pCube->pNext, pCube2 )
- {
- assert( pCube->nLits == pCube2->nLits );
- if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
- continue;
- pCubeNew = Min_CubesXor( p, pCube, pCube2 );
- assert( pCubeNew->nLits == pCube->nLits - 1 );
- pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
- p->ppStore[pCubeNew->nLits] = pCubeNew;
- p->nCubes++;
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Min_SopComplement( Min_Man_t * p, Min_Cube_t * pSharp )
-{
- Vec_Int_t * vVars;
- Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
- int Num, Value, i;
-
- // get the variables
- vVars = Vec_IntAlloc( 100 );
- // create the tautology cube
- pCover = Min_CubeAlloc( p );
- // sharp it with all cubes
- Min_CoverForEachCube( pSharp, pCube )
- Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
- {
- if ( Min_CubesDisjoint( pThis, pCube ) )
- continue;
- // remember the next pointer
- pNext = pThis->pNext;
- // get the variables, in which pThis is '-' while pCube is fixed
- Min_CoverGetDisjVars( pThis, pCube, vVars );
- // generate the disjoint cubes
- pReady = pThis;
- Vec_IntForEachEntryReverse( vVars, Num, i )
- {
- // correct the literal
- Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
- if ( i == 0 )
- break;
- // create the new cube and clean this value
- Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
- pReady = Min_CubeDup( p, pReady );
- Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
- // add to the cover
- *ppPrev = pReady;
- ppPrev = &pReady->pNext;
- }
- pThis = pReady;
- pThis->pNext = pNext;
- }
- Vec_IntFree( vVars );
-
- // perform dist-1 merge and contain
- Min_CoverExpandRemoveEqual( p, pCover );
- Min_SopDist1Merge( p );
- Min_SopContain( p );
- return Min_CoverCollect( p, p->nVars );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Min_SopCheck( Min_Man_t * p )
-{
- Min_Cube_t * pCube, * pThis;
- int i;
-
- pCube = Min_CubeAlloc( p );
- Min_CubeXorBit( pCube, 2*0+1 );
- Min_CubeXorBit( pCube, 2*1+1 );
- Min_CubeXorBit( pCube, 2*2+0 );
- Min_CubeXorBit( pCube, 2*3+0 );
- Min_CubeXorBit( pCube, 2*4+0 );
- Min_CubeXorBit( pCube, 2*5+1 );
- Min_CubeXorBit( pCube, 2*6+1 );
- pCube->nLits = 7;
-
-// Min_CubeWrite( stdout, pCube );
-
- // check that the cubes contain it
- for ( i = 0; i <= p->nVars; i++ )
- Min_CoverForEachCube( p->ppStore[i], pThis )
- if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
- {
- Min_CubeRecycle( p, pCube );
- return 1;
- }
- Min_CubeRecycle( p, pCube );
- return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzMinUtil.c b/src/opt/xyz/xyzMinUtil.c
deleted file mode 100644
index 9ec5f83f..00000000
--- a/src/opt/xyz/xyzMinUtil.c
+++ /dev/null
@@ -1,277 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzMinUtil.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Utilities.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzMinUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyzInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CubeWrite( FILE * pFile, Min_Cube_t * pCube )
-{
- int i;
- assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
- for ( i = 0; i < (int)pCube->nVars; i++ )
- if ( Min_CubeHasBit(pCube, i*2) )
- {
- if ( Min_CubeHasBit(pCube, i*2+1) )
- fprintf( pFile, "-" );
- else
- fprintf( pFile, "0" );
- }
- else
- {
- if ( Min_CubeHasBit(pCube, i*2+1) )
- fprintf( pFile, "1" );
- else
- fprintf( pFile, "?" );
- }
- fprintf( pFile, " 1\n" );
-// fprintf( pFile, " %d\n", pCube->nLits );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CoverWrite( FILE * pFile, Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube;
- Min_CoverForEachCube( pCover, pCube )
- Min_CubeWrite( pFile, pCube );
- printf( "\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CoverWriteStore( FILE * pFile, Min_Man_t * p )
-{
- Min_Cube_t * pCube;
- int i;
- for ( i = 0; i <= p->nVars; i++ )
- {
- Min_CoverForEachCube( p->ppStore[i], pCube )
- {
- printf( "%2d : ", i );
- if ( pCube == p->pBubble )
- {
- printf( "Bubble\n" );
- continue;
- }
- Min_CubeWrite( pFile, pCube );
- }
- }
- printf( "\n" );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CoverWriteFile( Min_Cube_t * pCover, char * pName, int fEsop )
-{
- char Buffer[1000];
- Min_Cube_t * pCube;
- FILE * pFile;
- int i;
- sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
- for ( i = strlen(Buffer) - 1; i >= 0; i-- )
- if ( Buffer[i] == '<' || Buffer[i] == '>' )
- Buffer[i] = '_';
- pFile = fopen( Buffer, "w" );
- fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
- fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
- fprintf( pFile, ".o %d\n", 1 );
- fprintf( pFile, ".p %d\n", Min_CoverCountCubes(pCover) );
- if ( fEsop ) fprintf( pFile, ".type esop\n" );
- Min_CoverForEachCube( pCover, pCube )
- Min_CubeWrite( pFile, pCube );
- fprintf( pFile, ".e\n" );
- fclose( pFile );
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CoverCheck( Min_Man_t * p )
-{
- Min_Cube_t * pCube;
- int i;
- for ( i = 0; i <= p->nVars; i++ )
- Min_CoverForEachCube( p->ppStore[i], pCube )
- assert( i == (int)pCube->nLits );
-}
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Min_CubeCheck( Min_Cube_t * pCube )
-{
- int i;
- for ( i = 0; i < (int)pCube->nVars; i++ )
- if ( Min_CubeGetVar( pCube, i ) == 0 )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Converts the cover from the sorted structure.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Min_CoverCollect( Min_Man_t * p, int nSuppSize )
-{
- Min_Cube_t * pCov = NULL, ** ppTail = &pCov;
- Min_Cube_t * pCube, * pCube2;
- int i;
- for ( i = 0; i <= nSuppSize; i++ )
- {
- Min_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
- {
- assert( i == (int)pCube->nLits );
- *ppTail = pCube;
- ppTail = &pCube->pNext;
- assert( pCube->uData[0] ); // not a bubble
- }
- }
- *ppTail = NULL;
- return pCov;
-}
-
-/**Function*************************************************************
-
- Synopsis [Sorts the cover in the increasing number of literals.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Min_CoverExpand( Min_Man_t * p, Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube, * pCube2;
- Min_ManClean( p, p->nVars );
- Min_CoverForEachCubeSafe( pCover, pCube, pCube2 )
- {
- pCube->pNext = p->ppStore[pCube->nLits];
- p->ppStore[pCube->nLits] = pCube;
- p->nCubes++;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Sorts the cover in the increasing number of literals.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Min_CoverSuppVarNum( Min_Man_t * p, Min_Cube_t * pCover )
-{
- Min_Cube_t * pCube;
- int i, Counter;
- if ( pCover == NULL )
- return 0;
- // clean the cube
- for ( i = 0; i < (int)pCover->nWords; i++ )
- p->pTemp->uData[i] = ~((unsigned)0);
- // add the bit data
- Min_CoverForEachCube( pCover, pCube )
- for ( i = 0; i < (int)pCover->nWords; i++ )
- p->pTemp->uData[i] &= pCube->uData[i];
- // count the vars
- Counter = 0;
- for ( i = 0; i < (int)pCover->nVars; i++ )
- Counter += ( Min_CubeGetVar(p->pTemp, i) != 3 );
- return Counter;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/xyz/xyzTest.c b/src/opt/xyz/xyzTest.c
deleted file mode 100644
index 38580790..00000000
--- a/src/opt/xyz/xyzTest.c
+++ /dev/null
@@ -1,417 +0,0 @@
-/**CFile****************************************************************
-
- FileName [xyzTest.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Cover manipulation package.]
-
- Synopsis [Testing procedures.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: xyzTest.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "xyz.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeDeriveCoverPro( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
-{
- Min_Cube_t * pCover;
- Min_Cube_t * pCube0, * pCube1, * pCube;
- if ( pCover0 == NULL || pCover1 == NULL )
- return NULL;
- // clean storage
- Min_ManClean( p, p->nVars );
- // go through the cube pairs
- Min_CoverForEachCube( pCover0, pCube0 )
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- if ( Min_CubesDisjoint( pCube0, pCube1 ) )
- continue;
- pCube = Min_CubesProduct( p, pCube0, pCube1 );
- // add the cube to storage
- Min_SopAddCube( p, pCube );
- }
- Min_SopMinimize( p );
- pCover = Min_CoverCollect( p, p->nVars );
- assert( p->nCubes == Min_CoverCountCubes(pCover) );
- return pCover;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeDeriveCoverSum( Min_Man_t * p, Min_Cube_t * pCover0, Min_Cube_t * pCover1 )
-{
- Min_Cube_t * pCover;
- Min_Cube_t * pThis, * pCube;
- if ( pCover0 == NULL || pCover1 == NULL )
- return NULL;
- // clean storage
- Min_ManClean( p, p->nVars );
- // add the cubes to storage
- Min_CoverForEachCube( pCover0, pThis )
- {
- pCube = Min_CubeDup( p, pThis );
- Min_SopAddCube( p, pCube );
- }
- Min_CoverForEachCube( pCover1, pThis )
- {
- pCube = Min_CubeDup( p, pThis );
- Min_SopAddCube( p, pCube );
- }
- Min_SopMinimize( p );
- pCover = Min_CoverCollect( p, p->nVars );
- assert( p->nCubes == Min_CoverCountCubes(pCover) );
- return pCover;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeDeriveSops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
-{
- Min_Cube_t * pCov0[2], * pCov1[2];
- Min_Cube_t * pCoverP, * pCoverN;
- Abc_Obj_t * pObj;
- int i, nCubes, fCompl0, fCompl1;
-
- // set elementary vars
- Vec_PtrForEachEntry( vSupp, pObj, i )
- {
- pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
- pObj->pNext = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 1 );
- }
-
- // get the cover for each node in the array
- Vec_PtrForEachEntry( vNodes, pObj, i )
- {
- // get the complements
- fCompl0 = Abc_ObjFaninC0(pObj);
- fCompl1 = Abc_ObjFaninC1(pObj);
- // get the covers
- pCov0[0] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy;
- pCov0[1] = (Min_Cube_t *)Abc_ObjFanin0(pObj)->pNext;
- pCov1[0] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy;
- pCov1[1] = (Min_Cube_t *)Abc_ObjFanin1(pObj)->pNext;
- // compute the covers
- pCoverP = Abc_NodeDeriveCoverPro( p, pCov0[ fCompl0], pCov1[ fCompl1] );
- pCoverN = Abc_NodeDeriveCoverSum( p, pCov0[!fCompl0], pCov1[!fCompl1] );
- // set the covers
- pObj->pCopy = (Abc_Obj_t *)pCoverP;
- pObj->pNext = (Abc_Obj_t *)pCoverN;
- }
-
- nCubes = ABC_MIN( Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverP) );
-
-/*
-printf( "\n\n" );
-Min_CoverWrite( stdout, pCoverP );
-printf( "\n\n" );
-Min_CoverWrite( stdout, pCoverN );
-*/
-
-// printf( "\n" );
-// Min_CoverWrite( stdout, pCoverP );
-
-// Min_CoverExpand( p, pCoverP );
-// Min_SopMinimize( p );
-// pCoverP = Min_CoverCollect( p, p->nVars );
-
-// printf( "\n" );
-// Min_CoverWrite( stdout, pCoverP );
-
-// nCubes = Min_CoverCountCubes(pCoverP);
-
- // clean the copy fields
- Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = pObj->pNext = NULL;
- Vec_PtrForEachEntry( vSupp, pObj, i )
- pObj->pCopy = pObj->pNext = NULL;
-
-// Min_CoverWriteFile( pCoverP, Abc_ObjName(pRoot), 0 );
-// printf( "\n" );
-// Min_CoverWrite( stdout, pCoverP );
-
-// printf( "\n" );
-// Min_CoverWrite( stdout, pCoverP );
-// printf( "\n" );
-// Min_CoverWrite( stdout, pCoverN );
- return nCubes;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkTestSop( Abc_Ntk_t * pNtk )
-{
- Min_Man_t * p;
- Vec_Ptr_t * vSupp, * vNodes;
- Abc_Obj_t * pObj;
- int i, nCubes;
- assert( Abc_NtkIsStrash(pNtk) );
-
- Abc_NtkCleanCopy(pNtk);
- Abc_NtkCleanNext(pNtk);
- Abc_NtkForEachCo( pNtk, pObj, i )
- {
- if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
- {
- printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
- continue;
- }
-
- vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
- vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
-
- printf( "%20s : Cone = %5d. Supp = %5d. ",
- Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
-// if ( vSupp->nSize <= 128 )
- {
- p = Min_ManAlloc( vSupp->nSize );
- nCubes = Abc_NodeDeriveSops( p, pObj, vSupp, vNodes );
- printf( "Cubes = %5d. ", nCubes );
- Min_ManFree( p );
- }
- printf( "\n" );
-
-
- Vec_PtrFree( vNodes );
- Vec_PtrFree( vSupp );
- }
-}
-
-
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Min_Cube_t * Abc_NodeDeriveCover( Min_Man_t * p, Min_Cube_t * pCov0, Min_Cube_t * pCov1, int fComp0, int fComp1 )
-{
- Min_Cube_t * pCover0, * pCover1, * pCover;
- Min_Cube_t * pCube0, * pCube1, * pCube;
-
- // complement the first if needed
- if ( !fComp0 )
- pCover0 = pCov0;
- else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
- pCover0 = pCov0->pNext;
- else
- pCover0 = p->pOne0, p->pOne0->pNext = pCov0;
-
- // complement the second if needed
- if ( !fComp1 )
- pCover1 = pCov1;
- else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
- pCover1 = pCov1->pNext;
- else
- pCover1 = p->pOne1, p->pOne1->pNext = pCov1;
-
- if ( pCover0 == NULL || pCover1 == NULL )
- return NULL;
-
- // clean storage
- Min_ManClean( p, p->nVars );
- // go through the cube pairs
- Min_CoverForEachCube( pCover0, pCube0 )
- Min_CoverForEachCube( pCover1, pCube1 )
- {
- if ( Min_CubesDisjoint( pCube0, pCube1 ) )
- continue;
- pCube = Min_CubesProduct( p, pCube0, pCube1 );
- // add the cube to storage
- Min_EsopAddCube( p, pCube );
- }
-
- if ( p->nCubes > 10 )
- {
-// printf( "(%d,", p->nCubes );
- Min_EsopMinimize( p );
-// printf( "%d) ", p->nCubes );
- }
-
- pCover = Min_CoverCollect( p, p->nVars );
- assert( p->nCubes == Min_CoverCountCubes(pCover) );
-
-// if ( p->nCubes > 1000 )
-// printf( "%d ", p->nCubes );
- return pCover;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_NodeDeriveEsops( Min_Man_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vSupp, Vec_Ptr_t * vNodes )
-{
- Min_Cube_t * pCover, * pCube;
- Abc_Obj_t * pObj;
- int i;
-
- // set elementary vars
- Vec_PtrForEachEntry( vSupp, pObj, i )
- pObj->pCopy = (Abc_Obj_t *)Min_CubeAllocVar( p, i, 0 );
-
- // get the cover for each node in the array
- Vec_PtrForEachEntry( vNodes, pObj, i )
- {
- pCover = Abc_NodeDeriveCover( p,
- (Min_Cube_t *)Abc_ObjFanin0(pObj)->pCopy,
- (Min_Cube_t *)Abc_ObjFanin1(pObj)->pCopy,
- Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
- pObj->pCopy = (Abc_Obj_t *)pCover;
- if ( p->nCubes > 3000 )
- return -1;
- }
-
- // add complement if needed
- if ( Abc_ObjFaninC0(pRoot) )
- {
- if ( pCover && pCover->nLits == 0 ) // topmost one is the tautology cube
- {
- pCube = pCover;
- pCover = pCover->pNext;
- Min_CubeRecycle( p, pCube );
- p->nCubes--;
- }
- else
- {
- pCube = Min_CubeAlloc( p );
- pCube->pNext = pCover;
- p->nCubes++;
- }
- }
-/*
- Min_CoverExpand( p, pCover );
- Min_EsopMinimize( p );
- pCover = Min_CoverCollect( p, p->nVars );
-*/
- // clean the copy fields
- Vec_PtrForEachEntry( vNodes, pObj, i )
- pObj->pCopy = NULL;
- Vec_PtrForEachEntry( vSupp, pObj, i )
- pObj->pCopy = NULL;
-
-// Min_CoverWriteFile( pCover, Abc_ObjName(pRoot), 1 );
-// Min_CoverWrite( stdout, pCover );
- return p->nCubes;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkTestEsop( Abc_Ntk_t * pNtk )
-{
- Min_Man_t * p;
- Vec_Ptr_t * vSupp, * vNodes;
- Abc_Obj_t * pObj;
- int i, nCubes;
- assert( Abc_NtkIsStrash(pNtk) );
-
- Abc_NtkCleanCopy(pNtk);
- Abc_NtkForEachCo( pNtk, pObj, i )
- {
- if ( !Abc_NodeIsAigAnd(Abc_ObjFanin0(pObj)) )
- {
- printf( "%-20s : Trivial.\n", Abc_ObjName(pObj) );
- continue;
- }
-
- vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
- vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
-
- printf( "%20s : Cone = %5d. Supp = %5d. ",
- Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
-// if ( vSupp->nSize <= 128 )
- {
- p = Min_ManAlloc( vSupp->nSize );
- nCubes = Abc_NodeDeriveEsops( p, pObj, vSupp, vNodes );
- printf( "Cubes = %5d. ", nCubes );
- Min_ManFree( p );
- }
- printf( "\n" );
-
-
- Vec_PtrFree( vNodes );
- Vec_PtrFree( vSupp );
- }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 10:04:01 +0000