summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2005-10-01 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2005-10-01 08:01:00 -0700
commit78fbd336aa584c4d285123ad18617aa9277016b4 (patch)
tree5d65fe6b080dc85b1456320f60555ba33bab9b09 /src/misc
parent0af9acd0cd07dcb37c195c6a0832b82c0eca1193 (diff)
downloadabc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.gz
abc-78fbd336aa584c4d285123ad18617aa9277016b4.tar.bz2
abc-78fbd336aa584c4d285123ad18617aa9277016b4.zip
Version abc51001
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h2
-rw-r--r--src/misc/extra/extraUtilMisc.c31
-rw-r--r--src/misc/npn/npn.c202
-rw-r--r--src/misc/npn/npn.h105
-rw-r--r--src/misc/npn/npnGenStr.c473
-rw-r--r--src/misc/npn/npnTruth.c137
-rw-r--r--src/misc/npn/npnUtil.c78
7 files changed, 1028 insertions, 0 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 904d550f..5305ae31 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -261,6 +261,8 @@ extern int Extra_Power3( int Num );
/* the number of combinations of k elements out of n */
extern int Extra_NumCombinations( int k, int n );
extern int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits );
+/* counts the number of 1s in the bitstring */
+extern int Extra_CountOnes( unsigned char * pBytes, int nBytes );
/* the factorial of number */
extern int Extra_Factorial( int n );
/* the permutation of the given number of elements */
diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c
index 6d771990..75e91cbc 100644
--- a/src/misc/extra/extraUtilMisc.c
+++ b/src/misc/extra/extraUtilMisc.c
@@ -209,6 +209,37 @@ int * Extra_DeriveRadixCode( int Number, int Radix, int nDigits )
return Code;
}
+/**Function*************************************************************
+
+ Synopsis [Counts the number of ones in the bitstring.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_CountOnes( unsigned char * pBytes, int nBytes )
+{
+ static int bit_count[256] = {
+ 0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+ 3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+ };
+
+ int i, Counter;
+ Counter = 0;
+ for ( i = 0; i < nBytes; i++ )
+ Counter += bit_count[ *(pBytes+i) ];
+ return Counter;
+}
+
/**Function********************************************************************
Synopsis [Computes the factorial.]
diff --git a/src/misc/npn/npn.c b/src/misc/npn/npn.c
new file mode 100644
index 00000000..ad4b4de6
--- /dev/null
+++ b/src/misc/npn/npn.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+ FileName [npn.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: npn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static int Npn_CompareVecs( void ** p0, void ** p1 );
+static Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars );
+static void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec );
+static int Npn_VecProperty( Vec_Int_t * vVec );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_Experiment()
+{
+ Vec_Int_t ** pVecs;
+ FILE * pFile;
+ int nFuncs, Num, i;
+
+ pFile = fopen( "npn5.txt", "r" );
+ pVecs = ALLOC( Vec_Int_t *, 1000000 );
+ for ( i = 0; ; i++ )
+ {
+ if ( fscanf( pFile, "%x", &Num ) != 1 )
+ break;
+ pVecs[i] = Npn_GetSignature( Num, 5 );
+ if ( Npn_VecProperty( pVecs[i] ) )
+ {
+ printf( "1s = %2d. ", Extra_CountOnes((unsigned char *)&Num, (1 << 5) / 8) );
+ Extra_PrintHex( stdout, Num, 5 ); fprintf( stdout, "\n" );
+ }
+
+ }
+ nFuncs = i;
+ printf( "Read %d numbers.\n", nFuncs );
+ fclose( pFile );
+ /*
+ // sort the vectors
+ qsort( (void *)pVecs, nFuncs, sizeof(void *),
+ (int (*)(const void *, const void *)) Npn_CompareVecs );
+ pFile = fopen( "npn5ar.txt", "w" );
+ for ( i = 0; i < nFuncs; i++ )
+ {
+ Npn_VecPrint( pFile, pVecs[i] );
+ Vec_IntFree( pVecs[i] );
+ }
+ fclose( pFile );
+ */
+
+ free( pVecs );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Npn_GetSignature( unsigned uTruth, int nVars )
+{
+ // elementary truth tables
+ static unsigned Signs[5] = {
+ 0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010
+ 0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000
+ 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000
+ 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000
+ };
+ Vec_Int_t * vVec;
+ unsigned uCofactor;
+ int Count0, Count1, i;
+ int nBytes = (1 << nVars) / 8;
+
+ // collect the number of 1s in each cofactor
+ vVec = Vec_IntAlloc( 5 );
+ for ( i = 0; i < nVars; i++ )
+ {
+ uCofactor = uTruth & ~Signs[i];
+ Count0 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
+ uCofactor = uTruth & Signs[i];
+ Count1 = Extra_CountOnes( (unsigned char *)&uCofactor, nBytes );
+ if ( Count0 < Count1 )
+ Vec_IntPush( vVec, Count0 );
+ else
+ Vec_IntPush( vVec, Count1 );
+ }
+ // sort them
+ Vec_IntSort( vVec, 0 );
+ return vVec;
+
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_CompareVecs( void ** p0, void ** p1 )
+{
+ Vec_Int_t * vVec0 = *p0;
+ Vec_Int_t * vVec1 = *p1;
+ int i;
+ assert( vVec0->nSize == vVec1->nSize );
+ for ( i = 0; i < vVec0->nSize; i++ )
+ if ( vVec0->pArray[i] < vVec1->pArray[i] )
+ return -1;
+ else if ( vVec0->pArray[i] > vVec1->pArray[i] )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_VecPrint( FILE * pFile, Vec_Int_t * vVec )
+{
+ int i;
+ for ( i = 0; i < vVec->nSize; i++ )
+ fprintf( pFile, "%2d ", vVec->pArray[i] );
+ fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_VecProperty( Vec_Int_t * vVec )
+{
+ int i;
+ for ( i = 0; i < vVec->nSize; i++ )
+ if ( vVec->pArray[i] != i + 1 )
+ return 0;
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npn.h b/src/misc/npn/npn.h
new file mode 100644
index 00000000..61aa6297
--- /dev/null
+++ b/src/misc/npn/npn.h
@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+ FileName [npn.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: npn.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __NPN_H__
+#define __NPN_H__
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define EXTRA_WORD_VARS 5
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Extra_BitCharNum( int nVars ) { if ( nVars <= 3 ) return 1; return 1 << (nVars - 3); }
+static inline int Extra_BitWordNum( int nVars ) { if ( nVars <= EXTRA_WORD_VARS ) return 1; return 1 << (nVars - EXTRA_WORD_VARS); }
+
+static inline int Extra_BitRead( uint8 * pBits, int iBit ) { return ( (pBits[iBit/8] & (1 << (iBit%8))) > 0 ); }
+static inline void Extra_BitSet( uint8 * pBits, int iBit ) { pBits[iBit/8] |= (1 << (iBit%8)); }
+static inline void Extra_BitXor( uint8 * pBits, int iBit ) { pBits[iBit/8] ^= (1 << (iBit%8)); }
+
+static inline void Extra_BitClean( int nVars, uint8 * pBits )
+{
+ unsigned * pWords = (unsigned *)pBits;
+ int i;
+ for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+ pWords[i] = 0;
+}
+static inline void Extra_BitNot( int nVars, uint8 * pBits )
+{
+ unsigned * pWords = (unsigned *)pBits;
+ int i;
+ for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+ pWords[i] = ~pWords[i];
+}
+static inline void Extra_BitCopy( int nVars, uint8 * pBits1, uint8 * pBits )
+{
+ unsigned * pWords = (unsigned *)pBits;
+ unsigned * pWords1 = (unsigned *)pBits1;
+ int i;
+ for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+ pWords[i] = pWords1[i];
+}
+static inline void Extra_BitAnd( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
+{
+ unsigned * pWords = (unsigned *)pBits;
+ unsigned * pWords1 = (unsigned *)pBits1;
+ unsigned * pWords2 = (unsigned *)pBits2;
+ int i;
+ for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+ pWords[i] = pWords1[i] & pWords2[i];
+}
+static inline void Extra_BitSharp( int nVars, uint8 * pBits1, uint8 * pBits2, uint8 * pBits )
+{
+ unsigned * pWords = (unsigned *)pBits;
+ unsigned * pWords1 = (unsigned *)pBits1;
+ unsigned * pWords2 = (unsigned *)pBits2;
+ int i;
+ for ( i = Extra_BitWordNum(nVars) - 1; i >= 0; i-- )
+ pWords[i] = pWords1[i] & ~pWords2[i];
+}
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== zzz.c ==========================================================*/
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
diff --git a/src/misc/npn/npnGenStr.c b/src/misc/npn/npnGenStr.c
new file mode 100644
index 00000000..adbfdcdf
--- /dev/null
+++ b/src/misc/npn/npnGenStr.c
@@ -0,0 +1,473 @@
+/**CFile****************************************************************
+
+ FileName [npnUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold );
+static void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec );
+static void Npn_GenerateFree( Vec_Ptr_t * vVec );
+static Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec );
+static void Npn_GenerateEmbed( Vec_Ptr_t * vVec );
+static void Npn_GeneratePrint( Vec_Ptr_t * vVec );
+
+
+static void Npn_RewritePrint( Vec_Ptr_t * vVec );
+static Vec_Ptr_t * Npn_Rewrite( char * pStruct );
+
+static int Npn_RewriteNumEntries( char * pString );
+static int Npn_RewriteLastAnd( char * pBeg, char * pString );
+static int Npn_RewriteLastExor( char * pBeg, char * pString );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_Generate()
+{
+ Vec_Ptr_t * vVec;
+ vVec = Npn_Generate_rec( 7, 1 );
+ Npn_GenerateEmbed( vVec );
+ Npn_GeneratePrint( vVec );
+ Npn_GenerateFree( vVec );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_Generate_rec( int nVars, int fFold )
+{
+ char Buffer[20], * pChar;
+ Vec_Ptr_t * vVec, * vVec1, * vVec2, * pTemp;
+ int i;
+
+ vVec = Vec_PtrAlloc( 100 );
+
+ // generate the combination
+ pChar = Buffer;
+ for ( i = 0; i < nVars; i++ )
+ *pChar++ = '.';
+ *pChar++ = 0;
+
+ Vec_PtrPush( vVec, util_strsav(Buffer) );
+ if ( nVars == 2 || !fFold )
+ return vVec;
+
+ assert( nVars > 2 );
+ for ( i = 2; i < nVars; i++ )
+ {
+ vVec1 = Npn_Generate_rec( i, 1 );
+ vVec1 = Npn_GenerateFold( pTemp = vVec1 );
+ Npn_GenerateFree( pTemp );
+ // add folded pairs
+ if ( nVars - i > 1 )
+ {
+ vVec2 = Npn_Generate_rec( nVars - i, 1 );
+ vVec2 = Npn_GenerateFold( pTemp = vVec2 );
+ Npn_GenerateFree( pTemp );
+ Npn_GenerateMerge( vVec1, vVec2, vVec );
+ Npn_GenerateFree( vVec2 );
+ }
+ // add unfolded pairs
+ vVec2 = Npn_Generate_rec( nVars - i, 0 );
+ Npn_GenerateMerge( vVec1, vVec2, vVec );
+ Npn_GenerateFree( vVec2 );
+ Npn_GenerateFree( vVec1 );
+ }
+ return vVec;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_GenerateMerge( Vec_Ptr_t * vVec1, Vec_Ptr_t * vVec2, Vec_Ptr_t * vVec )
+{
+ char Buffer[100];
+ char * pEntry1, * pEntry2, * pEntry;
+ int i, k, m;
+ Vec_PtrForEachEntry( vVec1, pEntry1, i )
+ Vec_PtrForEachEntry( vVec2, pEntry2, k )
+ {
+ if ( *pEntry1 == '(' && *pEntry2 == '(' )
+ if ( strcmp( pEntry1, pEntry2 ) > 0 )
+ continue;
+
+ // get the new entry
+ sprintf( Buffer, "%s%s", pEntry1, pEntry2 );
+ // skip duplicates
+ Vec_PtrForEachEntry( vVec, pEntry, m )
+ if ( strcmp( pEntry, Buffer ) == 0 )
+ break;
+ if ( m != Vec_PtrSize(vVec) )
+ continue;
+ // add the new entry
+ Vec_PtrPush( vVec, util_strsav(Buffer) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_GenerateFree( Vec_Ptr_t * vVec )
+{
+ char * pEntry;
+ int i;
+ Vec_PtrForEachEntry( vVec, pEntry, i )
+ free( pEntry );
+ Vec_PtrFree( vVec );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_GenerateFold( Vec_Ptr_t * vVec )
+{
+ Vec_Ptr_t * vVecR;
+ char Buffer[100];
+ char * pEntry;
+ int i;
+ vVecR = Vec_PtrAlloc( 10 );
+ Vec_PtrForEachEntry( vVec, pEntry, i )
+ {
+ // add entry without folding if the second part is folded
+ if ( pEntry[strlen(pEntry) - 1] == ')' )
+ Vec_PtrPush( vVecR, util_strsav(pEntry) );
+ // add the entry with folding
+ sprintf( Buffer, "(%s)", pEntry );
+ Vec_PtrPush( vVecR, util_strsav(Buffer) );
+ }
+ return vVecR;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_GenerateEmbed( Vec_Ptr_t * vVec )
+{
+ char Buffer[100];
+ char * pEntry;
+ int i;
+ Vec_PtrForEachEntry( vVec, pEntry, i )
+ {
+ sprintf( Buffer, "(%s)", pEntry );
+ Vec_PtrWriteEntry( vVec, i, util_strsav(Buffer) );
+ free( pEntry );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_GeneratePrint( Vec_Ptr_t * vVec )
+{
+ char * pEntry;
+ int i;
+ Vec_PtrForEachEntry( vVec, pEntry, i )
+ {
+ printf( "%5d : %s\n", i, pEntry );
+
+ {
+ Vec_Ptr_t * vFuncs;
+ vFuncs = Npn_Rewrite( pEntry );
+ Npn_RewritePrint( vFuncs );
+ Vec_PtrFree( vFuncs );
+ }
+ }
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_RewritePrint( Vec_Ptr_t * vVec )
+{
+ char * pEntry;
+ int i;
+ Vec_PtrForEachEntry( vVec, pEntry, i )
+ printf( " %3d : %s\n", i, pEntry );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_Rewrite_rec( char * pStruct, Vec_Ptr_t * vVec, Vec_Str_t * vForm )
+{
+ int nSizeOld;
+ char * pCur;
+ // find the next opening paranthesis
+ for ( pCur = pStruct; *pCur; pCur++ )
+ {
+ if ( *pCur == '(' )
+ break;
+ Vec_StrPush( vForm, *pCur );
+ }
+ // the paranthesis is not found quit
+ if ( *pCur == 0 )
+ {
+ Vec_StrPush( vForm, 0 );
+ Vec_PtrPush( vVec, util_strsav( vForm->pArray ) );
+ return;
+ }
+ assert( *pCur == '(' );
+ pCur++;
+ // remember the current size
+ nSizeOld = vForm->nSize;
+ // add different types
+ if ( Npn_RewriteLastAnd(vForm->pArray, vForm->pArray+vForm->nSize) )
+ {
+ Vec_StrPush( vForm, 'N' );
+ Vec_StrPush( vForm, '(' );
+ Npn_Rewrite_rec( pCur, vVec, vForm );
+ Vec_StrShrink( vForm, nSizeOld );
+ }
+ else
+ {
+ Vec_StrPush( vForm, 'A' );
+ Vec_StrPush( vForm, '(' );
+ Npn_Rewrite_rec( pCur, vVec, vForm );
+ Vec_StrShrink( vForm, nSizeOld );
+ }
+ // add different types
+ if ( Npn_RewriteNumEntries(pCur) == 3 )
+ {
+ Vec_StrPush( vForm, 'P' );
+ Vec_StrPush( vForm, '(' );
+ Npn_Rewrite_rec( pCur, vVec, vForm );
+ Vec_StrShrink( vForm, nSizeOld );
+ }
+ // add different types
+ if ( !Npn_RewriteLastExor(vForm->pArray, vForm->pArray+vForm->nSize) )
+ {
+ Vec_StrPush( vForm, 'X' );
+ Vec_StrPush( vForm, '(' );
+ Npn_Rewrite_rec( pCur, vVec, vForm );
+ Vec_StrShrink( vForm, nSizeOld );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Npn_Rewrite( char * pStruct )
+{
+ Vec_Ptr_t * vVec;
+ Vec_Str_t * vForm;
+ vVec = Vec_PtrAlloc( 10 );
+ vForm = Vec_StrAlloc( 10 );
+ Npn_Rewrite_rec( pStruct, vVec, vForm );
+ Vec_StrFree( vForm );
+ return vVec;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_RewriteNumEntries( char * pString )
+{
+ char * pCur;
+ int Counter = 0;
+ int nPars = 0;
+ for ( pCur = pString; *pCur; pCur++ )
+ {
+ if ( nPars == 0 )
+ {
+ if ( *pCur == '.' )
+ Counter++;
+ else if ( *pCur == '(' )
+ {
+ Counter++;
+ nPars++;
+ }
+ else if ( *pCur == ')' )
+ nPars--;
+ }
+ else if ( nPars > 0 )
+ {
+ if ( *pCur == '(' )
+ nPars++;
+ else if ( *pCur == ')' )
+ nPars--;
+ }
+ else
+ break;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the last was EXOR.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_RewriteLastAnd( char * pBeg, char * pEnd )
+{
+ char * pCur;
+ int nPars = 1;
+ for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
+ {
+ if ( *pCur == ')' )
+ nPars++;
+ else if ( *pCur == '(' )
+ nPars--;
+
+ if ( nPars == 0 && *pCur == 'A' )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the last was EXOR.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_RewriteLastExor( char * pBeg, char * pEnd )
+{
+ char * pCur;
+ int nPars = 1;
+ for ( pCur = pEnd - 1; pCur >= pBeg; pCur-- )
+ {
+ if ( *pCur == ')' )
+ nPars++;
+ else if ( *pCur == '(' )
+ nPars--;
+
+ if ( nPars == 0 && *pCur == 'X' )
+ return 1;
+ }
+ return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npnTruth.c b/src/misc/npn/npnTruth.c
new file mode 100644
index 00000000..b6be775b
--- /dev/null
+++ b/src/misc/npn/npnTruth.c
@@ -0,0 +1,137 @@
+/**CFile****************************************************************
+
+ FileName [npnUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the variable belongs to the support.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_TruthCofactors( int nVars, uint8 * puTruth, uint8 * puElem[][32],
+ uint8 * puTruthCofs0[][32], uint8 * puTruthCofs1[][32] )
+{
+ int v;
+ for ( v = 0; v < nVars; v++ )
+ {
+ Extra_BitSharp( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs0[v] );
+ Extra_BitAnd ( nVars, puTruth, puElem[v], (uint8 *)puTruthCofs1[v] );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the variable belongs to the support.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Extra_TruthCountCofactorOnes( int nVars, uint8 * puTruthCofs[][32], int * pCounts )
+{
+ int v, nBytes;
+ nBytes = Extra_BitCharNum( nVars );
+ for ( v = 0; v < nVars; v++ )
+ pCounts[v] = Extra_CountOnes( puTruthCofs[v], nBytes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the variable belongs to the support.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Extra_TruthHasVar( int nVars, uint8 * puTruth, int iVar )
+{
+ // elementary truth tables
+ static uint8 Signs[3] = {
+ 0xAA, // 1010 1010
+ 0xCC, // 1100 1100
+ 0xF0 // 1111 0000
+ };
+ int nChars, nShift, i;
+ assert( iVar < nVars );
+ nChars = Extra_BitCharNum( nVars );
+ if ( iVar < 3 )
+ {
+ nShift = (1 << iVar);
+ for ( i = 0; i < nChars; i++ )
+ if ( ((puTruth[i] & Signs[iVar]) >> nShift) != (puTruth[i] & ~Signs[iVar]) )
+ return 1;
+ }
+ else
+ {
+ nShift = (1 << (iVar-3));
+ for ( i = 0; i < nChars; i++, i = (i % nShift)? i : i + nShift )
+ if ( puTruth[i] != puTruth[i+nShift] )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the variable belongs to the support.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Npn_VarsTest( int nVars, uint8 * puTruth )
+{
+ int v;
+ int Counter = 0;
+ for ( v = 0; v < nVars; v++ )
+ Counter += Extra_TruthHasVar( nVars, puTruth, v );
+ return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/misc/npn/npnUtil.c b/src/misc/npn/npnUtil.c
new file mode 100644
index 00000000..b12ad092
--- /dev/null
+++ b/src/misc/npn/npnUtil.c
@@ -0,0 +1,78 @@
+/**CFile****************************************************************
+
+ FileName [npnUtil.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: npnUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "extra.h"
+#include "npn.h"
+#include "vec.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Npn_StartTruth8( uint8 uTruths[][32] )
+{
+ // elementary truth tables
+ static uint8 Signs[3] = {
+ 0xAA, // 1010 1010
+ 0xCC, // 1100 1100
+ 0xF0 // 1111 0000
+ };
+ int v, i, nShift;
+ for ( v = 0; v < 3; v++ )
+ for ( i = 0; i < 32; i++ )
+ uTruths[v][i] = Signs[v];
+ for ( v = 3; v < 8; v++ )
+ {
+ nShift = (1 << (v-3));
+ for ( i = 0; i < 32; i++, i = (i % nShift)? i : i + nShift )
+ {
+ uTruths[v][i] = 0;
+ uTruths[v][i + nShift] = 0xFF;
+ }
+ }
+/*
+ for ( v = 0; v < 8; v++ )
+ {
+ Extra_PrintBinary( stdout, (unsigned int*)uTruths[v], 90 );
+ printf( "\n" );
+ }
+*/
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+