summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h1
-rw-r--r--src/misc/extra/extraUtilFile.c17
-rw-r--r--src/misc/extra/extraUtilMaj.c386
-rw-r--r--src/misc/extra/extraUtilPath.c607
-rw-r--r--src/misc/extra/module.make2
-rw-r--r--src/misc/util/utilTruth.h97
-rw-r--r--src/misc/vec/vecMem.h14
7 files changed, 1124 insertions, 0 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 3dee5f4e..6c0fd74a 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -119,6 +119,7 @@ extern char * Extra_StringAppend( char * pStrGiven, char * pStrAdd );
extern void Extra_StringClean( char * pStrGiven, char * pCharKeep );
extern unsigned Extra_ReadBinary( char * Buffer );
extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
+extern void Extra_PrintBinary2( FILE * pFile, unsigned Sign[], int nBits );
extern int Extra_ReadHex( unsigned Sign[], char * pString, int nDigits );
extern int Extra_ReadHexadecimal( unsigned Sign[], char * pString, int nVars );
extern void Extra_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars );
diff --git a/src/misc/extra/extraUtilFile.c b/src/misc/extra/extraUtilFile.c
index 6568c305..8f60f421 100644
--- a/src/misc/extra/extraUtilFile.c
+++ b/src/misc/extra/extraUtilFile.c
@@ -508,6 +508,23 @@ void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits )
// fprintf( pFile, "\n" );
}
+void Extra_PrintBinary2( FILE * pFile, unsigned Sign[], int nBits )
+{
+ int Remainder, nWords;
+ int w, i;
+
+ Remainder = (nBits%(sizeof(unsigned)*8));
+ nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
+
+ for ( w = 0; w < nWords; w++ )
+ {
+ int Limit = w == nWords-1 ? Remainder : 32;
+ for ( i = 0; i < Limit; i++ )
+ fprintf( pFile, "%c", '0' + (int)((Sign[w] & (1<<i)) > 0) );
+ }
+
+// fprintf( pFile, "\n" );
+}
/**Function*************************************************************
diff --git a/src/misc/extra/extraUtilMaj.c b/src/misc/extra/extraUtilMaj.c
new file mode 100644
index 00000000..8bdb0818
--- /dev/null
+++ b/src/misc/extra/extraUtilMaj.c
@@ -0,0 +1,386 @@
+/**CFile****************************************************************
+
+ FileName [extraUtilMaj.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [extra]
+
+ Synopsis [Path enumeration.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: extraUtilMaj.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "misc/vec/vecMem.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
+#include "opt/dau/dau.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Gem_Man_t_ Gem_Man_t;
+typedef struct Gem_Obj_t_ Gem_Obj_t;
+
+struct Gem_Man_t_
+{
+ int nVars; // max variable count
+ int nWords; // truth tabel word count
+ int nObjsAlloc; // allocated objects
+ int nObjs; // used objects
+ Gem_Obj_t * pObjs; // function objects
+ Vec_Mem_t * vTtMem; // truth table memory and hash table
+ word ** pTtElems; // elementary truth tables
+ int fVerbose;
+};
+
+struct Gem_Obj_t_ // 8 bytes
+{
+ unsigned nVars : 4; // variable count
+ unsigned nNodes : 4; // node count
+ unsigned History : 8; // (i < j) ? {vi, vj} : {vi, 0}
+ unsigned Groups : 16; // mask with last vars in each symmetric group
+ int Predec; // predecessor
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gem_PrintNode( Gem_Man_t * p, int f, char * pLabel, int fUpdate )
+{
+ Gem_Obj_t * pObj = p->pObjs + f;
+ int GroupsMod = pObj->Groups;
+ if ( !p->fVerbose )
+ return;
+ printf( "Node %6d : %s Pred = %6d Vars = %d Nodes = %d History = %d%d Profile: ",
+ f, pLabel, pObj->Predec, pObj->nVars, pObj->nNodes, pObj->History & 0xF, pObj->History >> 4 );
+ Extra_PrintBinary2( stdout, (unsigned*)&GroupsMod, p->nVars ); printf("%s\n", fUpdate?" *":"");
+}
+Gem_Man_t * Gem_ManAlloc( int nVars, int fVerbose )
+{
+ Gem_Man_t * p;
+ assert( nVars <= 16 );
+ p = ABC_CALLOC( Gem_Man_t, 1 );
+ p->nVars = nVars;
+ p->nWords = Abc_TtWordNum( nVars );
+ p->nObjsAlloc = 10000000;
+ p->nObjs = 2;
+ p->pObjs = ABC_CALLOC( Gem_Obj_t, p->nObjsAlloc );
+ p->pObjs[1].nVars = p->pObjs[1].Groups = 1; // buffer
+ p->vTtMem = Vec_MemAllocForTT( nVars, 0 );
+ p->pTtElems = (word **)Extra_ArrayAlloc( nVars + 4, p->nWords, sizeof(word) );
+ p->fVerbose = fVerbose;
+ Abc_TtElemInit( p->pTtElems, nVars );
+ Gem_PrintNode( p, 1, "Original", 0 );
+ return p;
+}
+int Gem_ManFree( Gem_Man_t * p )
+{
+ Vec_MemHashFree( p->vTtMem );
+ Vec_MemFree( p->vTtMem );
+ ABC_FREE( p->pTtElems );
+ ABC_FREE( p->pObjs );
+ ABC_FREE( p );
+ return 1;
+}
+void Gem_ManRealloc( Gem_Man_t * p )
+{
+ int nObjNew = Abc_MinInt( 2 * p->nObjsAlloc, 0x7FFFFFFF );
+ assert( p->nObjs == p->nObjsAlloc );
+ if ( p->nObjs == 0x7FFFFFFF )
+ printf( "Hard limit on the number of nodes (0x7FFFFFFF) is reached. Quitting...\n" ), exit(1);
+ assert( p->nObjs < nObjNew );
+ printf("Extending object storage: %d -> %d.\n", p->nObjsAlloc, nObjNew );
+ p->pObjs = ABC_REALLOC( Gem_Obj_t, p->pObjs, nObjNew );
+ memset( p->pObjs + p->nObjsAlloc, 0, sizeof(Gem_Obj_t) * (nObjNew - p->nObjsAlloc) );
+ p->nObjsAlloc = nObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derive groups using symmetry info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gem_GroupsDerive( word * pTruth, int nVars, word * pCof0, word * pCof1 )
+{
+ int v, Res = 1 << (nVars-1);
+ for ( v = 0; v < nVars-1; v++ )
+ if ( !Abc_TtVarsAreSymmetric(pTruth, nVars, v, v+1, pCof0, pCof1) )
+ Res |= (1 << v);
+ return Res;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extends function f by replacing var i with a new gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gem_GroupVarRemove( int Groups, int i ) // remove i-th var
+{
+ int Mask = i ? Abc_InfoMask( i ) : 0;
+ assert( i >= 0 );
+ assert( (Groups >> i) & 1 );
+ return (Groups & Mask) | ((Groups & ~Mask) >> 1);
+}
+int Gem_GroupVarsInsert1( int Groups, int i, int fGroup ) // insert one bit after i
+{
+ int Mask = i+1 ? Abc_InfoMask( i+1 ) : 0;
+ assert( i+1 >= 0 );
+ assert( !fGroup || i == -1 || ((Groups >> i) & 1) );
+ assert( fGroup == 0 || fGroup == 1 );
+ return (Groups & Mask) | ((Groups & ~Mask) << 1) | (fGroup << (i+1));
+}
+int Gem_GroupVarsInsert3( int Groups, int i ) // insert group of 3 bits after i
+{
+ int Mask = i+1 ? Abc_InfoMask( i+1 ) : 0;
+ assert( i+1 >= 0 );
+ assert( i == -1 || (Groups >> i) & 1 );
+ return (Groups & Mask) | ((Groups & ~Mask) << 3) | (0x4 << (i+1));
+}
+int Gem_GroupUnpack( int Groups, int * pVars )
+{
+ int v, nGroups = 0;
+ for ( v = 0; Groups; v++, Groups >>= 1 )
+ if ( Groups & 1 )
+ pVars[nGroups++] = v;
+ return nGroups;
+}
+int Gem_FuncFindPlace( word * pTruth, int nWords, int Groups, word * pBest, int fOneVar )
+{
+ int pLast[16], nGroups = Gem_GroupUnpack( Groups, pLast );
+ int g, v, Value, BestPlace = nGroups ? pLast[nGroups - 1] : -1;
+ assert( nGroups >= 0 );
+ Abc_TtCopy( pBest, pTruth, nWords, 0 );
+ for ( g = nGroups - 1; g >= 0; g-- )
+ {
+ int Limit = g ? pLast[g-1] : -1;
+ for ( v = pLast[g]; v > Limit; v-- )
+ {
+ Abc_TtSwapAdjacent( pTruth, nWords, v+0 );
+ if ( fOneVar )
+ continue;
+ Abc_TtSwapAdjacent( pTruth, nWords, v+1 );
+ Abc_TtSwapAdjacent( pTruth, nWords, v+2 );
+ }
+ Value = memcmp(pBest, pTruth, sizeof(word)*nWords);
+ if ( Value < 0 )
+ {
+ Abc_TtCopy( pBest, pTruth, nWords, 0 );
+ BestPlace = Limit;
+ }
+ }
+ return BestPlace;
+}
+void Gem_FuncExpand( Gem_Man_t * p, int f, int i )
+{
+ Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
+ word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
+ word * pResult = p->pTtElems[p->nVars];
+ word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
+ int v, iFunc;
+ char pCanonPermC[16];
+ assert( i < (int)pObj->nVars );
+ assert( (int)pObj->nVars + 2 <= p->nVars );
+ Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
+ // move i variable to the end
+ for ( v = i; v < (int)pObj->nVars-1; v++ )
+ Abc_TtSwapAdjacent( pResult, p->nWords, v );
+ // create new symmetric group
+ assert( v == (int)pObj->nVars-1 );
+ Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v );
+ Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v );
+ Abc_TtMaj( pResult, p->pTtElems[v], p->pTtElems[v+1], p->pTtElems[v+2], p->nWords );
+ Abc_TtMux( pResult, pResult, pCofs[1], pCofs[0], p->nWords );
+ // canonicize
+ //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n");
+ Abc_TtCanonicizePerm( pResult, pObj->nVars + 2, pCanonPermC );
+ Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars+2), p->nVars );
+ //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars + 2 ); printf("\n\n");
+ iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
+ if ( iFunc < p->nObjs )
+ return;
+ assert( iFunc == p->nObjs );
+ pNew->nVars = pObj->nVars + 2;
+ pNew->nNodes = pObj->nNodes + 1;
+ pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
+ pNew->Predec = f;
+ pNew->History = i;
+ Gem_PrintNode( p, iFunc, "Expand ", 0 );
+
+ assert( p->nObjs < p->nObjsAlloc );
+ if ( ++p->nObjs == p->nObjsAlloc )
+ Gem_ManRealloc( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduces function f by crossbaring variables i and j.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gem_FuncCheckMajority( Gem_Man_t * p, int f )
+{
+ Gem_Obj_t * pObj = p->pObjs + f;
+ word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
+ int Polar = Abc_TtIsFullySymmetric( pTruth, pObj->nVars );
+ if ( Polar != -1 )
+ {
+ int nHalfVars = (pObj->nVars+1) >> 1;
+ int Mask = Abc_Tt6Mask( nHalfVars );
+ printf( "Found symmetric %d-variable function: ", pObj->nVars );
+ Extra_PrintBinary2( stdout, (unsigned *)&Polar, pObj->nVars + 1 );
+ printf( " " );
+ if ( (pObj->nVars & 1) && Polar == (Mask << nHalfVars) )
+ {
+ printf( "This is majority-%d.\n", pObj->nVars );
+ return 0;
+ }
+ printf( "\n" );
+ }
+ return 0;
+}
+int Gem_FuncReduce( Gem_Man_t * p, int f, int i, int j )
+{
+ Gem_Obj_t * pNew = p->pObjs + p->nObjs, * pObj = p->pObjs + f;
+ word * pTruth = Vec_MemReadEntry( p->vTtMem, f );
+ word * pResult = p->pTtElems[p->nVars];
+ word * pCofs[2] = { p->pTtElems[p->nVars+2], p->pTtElems[p->nVars+3] };
+ int v, iFunc;
+ char pCanonPermC[16];
+ assert( i < j && j < 16 );
+ Abc_TtCopy( pResult, pTruth, p->nWords, 0 );
+ // move j variable to the end
+ for ( v = j; v < (int)pObj->nVars-1; v++ )
+ Abc_TtSwapAdjacent( pResult, p->nWords, v );
+ assert( v == (int)pObj->nVars-1 );
+ // move i variable to the end
+ for ( v = i; v < (int)pObj->nVars-2; v++ )
+ Abc_TtSwapAdjacent( pResult, p->nWords, v );
+ assert( v == (int)pObj->nVars-2 );
+ // create new variable
+ Abc_TtCofactor0p( pCofs[0], pResult, p->nWords, v+1 );
+ Abc_TtCofactor1p( pCofs[1], pResult, p->nWords, v+1 );
+ Abc_TtCofactor0( pCofs[0], p->nWords, v );
+ Abc_TtCofactor1( pCofs[1], p->nWords, v );
+ Abc_TtMux( pResult, p->pTtElems[v], pCofs[1], pCofs[0], p->nWords );
+ // canonicize
+ //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n");
+ Abc_TtCanonicizePerm( pResult, pObj->nVars - 1, pCanonPermC );
+ Abc_TtStretch6( pResult, Abc_MaxInt(6, pObj->nVars-1), p->nVars );
+ //Extra_PrintHex( stdout, (unsigned*)pResult, pObj->nVars - 1 ); printf("\n\n");
+ iFunc = Vec_MemHashInsert( p->vTtMem, pResult );
+ if ( iFunc < p->nObjs )
+ return 0;
+ assert( iFunc == p->nObjs );
+ pNew->nVars = pObj->nVars - 1;
+ pNew->nNodes = pObj->nNodes;
+ pNew->Groups = Gem_GroupsDerive( pResult, pNew->nVars, pCofs[0], pCofs[1] );
+ pNew->Predec = f;
+ pNew->History = (j << 4) | i;
+ Gem_PrintNode( p, iFunc, "Crossbar", 0 );
+ Gem_FuncCheckMajority( p, iFunc );
+
+ assert( p->nObjs < p->nObjsAlloc );
+ if ( ++p->nObjs == p->nObjsAlloc )
+ Gem_ManRealloc( p );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gem_Enumerate( int nVars, int fDump, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ Gem_Man_t * p = Gem_ManAlloc( nVars, fVerbose );
+ int v, f, i, j, nObjsStop = 1;
+ for ( v = 1; v <= nVars-2; v++ )
+ {
+ // expand functions by adding a gate
+ int nObjsStopPrev = nObjsStop;
+ nObjsStop = p->nObjs;
+ printf( "Expanding var %2d (functions = %10d) ", v, p->nObjs );
+ Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
+ for ( f = 0; f < nObjsStop; f++ )
+ if ( v == (int)p->pObjs[f].nVars || (v > (int)p->pObjs[f].nVars && f >= nObjsStopPrev) )
+ for ( i = 0; i < v; i++ )
+ if ( (int)p->pObjs[f].Groups & (1 << i) )
+ Gem_FuncExpand( p, f, i );
+ // reduce functions by adding a crossbar
+ printf( "Connecting var %2d (functions = %10d) ", v, p->nObjs );
+ Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
+ for ( f = nObjsStop; f < p->nObjs; f++ )
+ for ( i = 0; i < (int)p->pObjs[f].nVars; i++ )
+ if ( (int)p->pObjs[f].Groups & (1 << i) )
+ for ( j = i+1; j < (int)p->pObjs[f].nVars; j++ )
+ if ( (int)p->pObjs[f].Groups & (1 << j) )
+ if ( Gem_FuncReduce( p, f, i, j ) )
+ return Gem_ManFree( p );
+ }
+ printf( "Finished (functions = %10d) ", p->nObjs );
+ Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
+ if ( fDump ) Vec_MemDumpTruthTables( p->vTtMem, "enum", nVars );
+ Gem_ManFree( p );
+ return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/extraUtilPath.c b/src/misc/extra/extraUtilPath.c
new file mode 100644
index 00000000..c7231a05
--- /dev/null
+++ b/src/misc/extra/extraUtilPath.c
@@ -0,0 +1,607 @@
+/**CFile****************************************************************
+
+ FileName [extraUtilPath.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [extra]
+
+ Synopsis [Path enumeration.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: extraUtilPath.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include "aig/gia/gia.h"
+#include "misc/vec/vecHsh.h"
+
+#include <math.h>
+#include "sat/bmc/bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "misc/extra/extra.h"
+
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Computes AIG representing the set of all paths in the graph.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NodeVarX( int nSize, int y, int x )
+{
+ return Abc_Var2Lit( nSize * y + x, 0 );
+}
+int Abc_NodeVarY( int nSize, int y, int x )
+{
+ return Abc_Var2Lit( nSize * (nSize + 1) + nSize * x + y, 0 );
+}
+
+Gia_Man_t * Abc_EnumeratePaths( int nSize )
+{
+ Gia_Man_t * pTemp, * pGia = Gia_ManStart( 10000 );
+ int * pNodes = ABC_CALLOC( int, nSize+1 );
+ int x, y, nVars = 2*nSize*(nSize+1);
+ for ( x = 0; x < nVars; x++ )
+ Gia_ManAppendCi( pGia );
+ Gia_ManHashAlloc( pGia );
+ // y = 0; x = 0;
+ pNodes[0] = 1;
+ // y = 0; x > 0
+ for ( x = 1; x <= nSize; x++ )
+ pNodes[x] = Gia_ManHashAnd( pGia, pNodes[x-1], Abc_NodeVarX(nSize, 0, x) );
+ // y > 0; x >= 0
+ for ( y = 1; y <= nSize; y++ )
+ {
+ // y > 0; x = 0
+ pNodes[0] = Gia_ManHashAnd( pGia, pNodes[0], Abc_NodeVarY(nSize, y, 0) );
+ // y > 0; x > 0
+ for ( x = 1; x <= nSize; x++ )
+ {
+ int iHor = Gia_ManHashAnd( pGia, pNodes[x-1], Abc_NodeVarX(nSize, y, x) );
+ int iVer = Gia_ManHashAnd( pGia, pNodes[x], Abc_NodeVarY(nSize, y, x) );
+ pNodes[x] = Gia_ManHashOr( pGia, iHor, iVer );
+ }
+ }
+ Gia_ManAppendCo( pGia, pNodes[nSize] );
+ pGia = Gia_ManCleanup( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ ABC_FREE( pNodes );
+ return pGia;
+}
+void Abc_EnumeratePathsTest()
+{
+ int nSize = 2;
+ Gia_Man_t * pGia = Abc_EnumeratePaths( nSize );
+ Gia_AigerWrite( pGia, "testpath.aig", 0, 0 );
+ Gia_ManStop( pGia );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Generate NxN grid.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_GraphGrid( int n )
+{
+ Vec_Int_t * vEdges = Vec_IntAlloc( 4*n*(n-1) ); // two nodes per edge
+ int i, k;
+ for ( i = 0; i < n; i++ )
+ {
+ for ( k = 0; k < n-1; k++ )
+ Vec_IntPushTwo( vEdges, i*n+k, i*n+k+1 );
+ if ( i == n-1 ) break;
+ for ( k = 0; k < n; k++ )
+ Vec_IntPushTwo( vEdges, i*n+k, i*n+k+n );
+ }
+ //Vec_IntPrint( vEdges );
+ return vEdges;
+}
+Vec_Int_t * Abc_GraphNodeLife( Vec_Int_t * vEdges, int n )
+{
+ Vec_Int_t * vLife = Vec_IntStartFull( 2*n*n ); // start/stop per node
+ int One, Two, i;
+ Vec_IntForEachEntryDouble( vEdges, One, Two, i )
+ {
+ if ( Vec_IntEntry(vLife, 2*One) == -1 )
+ Vec_IntWriteEntry(vLife, 2*One, i/2);
+ if ( Vec_IntEntry(vLife, 2*Two) == -1 )
+ Vec_IntWriteEntry(vLife, 2*Two, i/2);
+ Vec_IntWriteEntry(vLife, 2*One+1, i/2);
+ Vec_IntWriteEntry(vLife, 2*Two+1, i/2);
+ }
+ //Vec_IntPrint( vLife );
+ return vLife;
+}
+Vec_Wec_t * Abc_GraphFrontiers( Vec_Int_t * vEdges, Vec_Int_t * vLife )
+{
+ Vec_Wec_t * vFronts = Vec_WecAlloc( Vec_IntSize(vEdges)/2 ); // front for each edge
+ Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vLife)/2 );
+ int e, n;
+ Vec_WecPushLevel(vFronts);
+ for ( e = 0; e < Vec_IntSize(vEdges)/2; e++ )
+ {
+ int * pNodes = Vec_IntEntryP(vEdges, 2*e);
+ for ( n = 0; n < 2; n++ )
+ if ( Vec_IntEntry(vLife, 2*pNodes[n]) == e ) // first time
+ Vec_IntPush( vTemp, pNodes[n] );
+ else if ( Vec_IntEntry(vLife, 2*pNodes[n]+1) == e ) // last time
+ Vec_IntRemove( vTemp, pNodes[n] );
+ Vec_IntAppend( Vec_WecPushLevel(vFronts), vTemp );
+ }
+ //Vec_WecPrint( vFronts, 0 );
+ Vec_IntFree( vTemp );
+ return vFronts;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print grid.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_GraphPathPrint4( int * pBuffer, Vec_Int_t * vEdges )
+{
+ char Box[13][13];
+ int x, y;
+ int e, nEdges = Vec_IntSize(vEdges)/2;
+ for ( y = 0; y < 13; y++ )
+ for ( x = 0; x < 13; x++ )
+ if ( y % 4 == 0 && x % 4 == 0 )
+ Box[y][x] = '*';
+ else
+ Box[y][x] = ' ';
+ for ( e = 0; e < nEdges; e++ )
+ {
+ int * pNodes = Vec_IntEntryP(vEdges, 2*e);
+ int y0 = 4*(pNodes[0]/4);
+ int x0 = 4*(pNodes[0]%4);
+ int y1 = 4*(pNodes[1]/4);
+ int x1 = 4*(pNodes[1]%4);
+ if ( !pBuffer[e] )
+ continue;
+ if ( y0 == y1 )
+ {
+ for ( x = x0+1; x < x1; x++ )
+ Box[y0][x] = '-';
+ }
+ else if ( x0 == x1 )
+ {
+ for ( y = y0+1; y < y1; y++ )
+ Box[y][x0] = '|';
+ }
+ else assert( 0 );
+ }
+ for ( y = 0; y < 13; y++, printf("\n") )
+ for ( x = 0; x < 13; x++ )
+ printf( "%c", Box[y][x] );
+ printf( "\n\n=================================\n\n" );
+}
+void Abc_GraphPathPrint5( int * pBuffer, Vec_Int_t * vEdges )
+{
+ char Box[17][17];
+ int x, y;
+ int e, nEdges = Vec_IntSize(vEdges)/2;
+ for ( y = 0; y < 17; y++ )
+ for ( x = 0; x < 17; x++ )
+ if ( y % 4 == 0 && x % 4 == 0 )
+ Box[y][x] = '*';
+ else
+ Box[y][x] = ' ';
+ for ( e = 0; e < nEdges; e++ )
+ {
+ int * pNodes = Vec_IntEntryP(vEdges, 2*e);
+ int y0 = 4*(pNodes[0]/5);
+ int x0 = 4*(pNodes[0]%5);
+ int y1 = 4*(pNodes[1]/5);
+ int x1 = 4*(pNodes[1]%5);
+ if ( !pBuffer[e] )
+ continue;
+ if ( y0 == y1 )
+ {
+ for ( x = x0+1; x < x1; x++ )
+ Box[y0][x] = '-';
+ }
+ else if ( x0 == x1 )
+ {
+ for ( y = y0+1; y < y1; y++ )
+ Box[y][x0] = '|';
+ }
+ else assert( 0 );
+ }
+ for ( y = 0; y < 17; y++, printf("\n") )
+ for ( x = 0; x < 17; x++ )
+ printf( "%c", Box[y][x] );
+ printf( "\n\n=================================\n\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count paths.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+double Abc_GraphCountPaths_rec( int Lev, int Node, Vec_Wec_t * vNodes, double ** pCache, int * pBuffer, Vec_Int_t * vEdges )
+{
+ double Res0, Res1;
+// if ( Node == -2 ) Abc_GraphPathPrint4( pBuffer, vEdges );
+ if ( Node == -2 )
+ return 1;
+ if ( Node == -1 )
+ return 0;
+ if ( pCache[Lev][Node] != -1.0 )
+ return pCache[Lev][Node];
+ pBuffer[Lev] = 0;
+ Res0 = Abc_GraphCountPaths_rec( Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node ), vNodes, pCache, pBuffer, vEdges );
+ pBuffer[Lev] = 1;
+ Res1 = Abc_GraphCountPaths_rec( Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node+1 ), vNodes, pCache, pBuffer, vEdges );
+ return (pCache[Lev][Node] = Res0 + Res1);
+}
+double Abc_GraphCountPaths( Vec_Wec_t * vNodes, Vec_Int_t * vEdges )
+{
+ int i, k, pBuffer[1000] = {0};
+ double ** pCache = ABC_ALLOC( double *, Vec_WecSize(vNodes) );
+ Vec_Int_t * vLevel; double Value;
+ Vec_WecForEachLevel( vNodes, vLevel, i )
+ {
+ pCache[i] = ABC_ALLOC( double, Vec_IntSize(vLevel) );
+ for ( k = 0; k < Vec_IntSize(vLevel); k++ )
+ pCache[i][k] = -1.0;
+ }
+ Value = Abc_GraphCountPaths_rec( 0, 0, vNodes, pCache, pBuffer, vEdges );
+ for ( i = 0; i < Vec_WecSize(vNodes); i++ )
+ ABC_FREE( pCache[i] );
+ ABC_FREE( pCache );
+ return Value;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Build AIG for paths.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_GraphDeriveGia_rec( Gia_Man_t * p, int Lev, int Node, Vec_Wec_t * vNodes, int ** pCache, int * pBuffer, Vec_Int_t * vEdges )
+{
+ int Res0, Res1;
+ if ( Node == -2 )
+ return 1;
+ if ( Node == -1 )
+ return 0;
+ if ( pCache[Lev][Node] != -1 )
+ return pCache[Lev][Node];
+ pBuffer[Lev] = 0;
+ Res0 = Abc_GraphDeriveGia_rec( p, Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node ), vNodes, pCache, pBuffer, vEdges );
+ pBuffer[Lev] = 1;
+ Res1 = Abc_GraphDeriveGia_rec( p, Lev+1, Vec_IntEntry( Vec_WecEntry(vNodes, Lev), 2*Node+1 ), vNodes, pCache, pBuffer, vEdges );
+ return ( pCache[Lev][Node] = Gia_ManHashMux(p, Gia_Obj2Lit(p, Gia_ManCi(p, Lev)), Res1, Res0) );
+}
+Gia_Man_t * Abc_GraphDeriveGia( Vec_Wec_t * vNodes, Vec_Int_t * vEdges )
+{
+ int ** pCache;
+ int i, Value, pBuffer[1000] = {0};
+ Vec_Int_t * vLevel;
+ // start AIG
+ Gia_Man_t * pTemp, * p = Gia_ManStart( 1000 );
+ p->pName = Abc_UtilStrsav("paths");
+ for ( i = 0; i < Vec_IntSize(vEdges)/2; i++ )
+ Gia_ManAppendCi(p);
+ Gia_ManHashAlloc(p);
+ // alloc cache
+ pCache = ABC_ALLOC( int *, Vec_WecSize(vNodes) );
+ Vec_WecForEachLevel( vNodes, vLevel, i )
+ pCache[i] = ABC_FALLOC( int, Vec_IntSize(vLevel) );
+ Value = Abc_GraphDeriveGia_rec( p, 0, 0, vNodes, pCache, pBuffer, vEdges );
+ for ( i = 0; i < Vec_WecSize(vNodes); i++ )
+ ABC_FREE( pCache[i] );
+ ABC_FREE( pCache );
+ // cleanup
+ Gia_ManAppendCo( p, Value );
+ p = Gia_ManCleanup( pTemp = p );
+ Gia_ManStop( pTemp );
+ return p;
+}
+void Abc_GraphDeriveGiaDump( Vec_Wec_t * vNodes, Vec_Int_t * vEdges, int Size )
+{
+ char pFileName[100];
+ Gia_Man_t * pGia = Abc_GraphDeriveGia( vNodes, vEdges );
+ sprintf( pFileName, "grid_%dx%d_e%03d.aig", Size, Size, Vec_IntSize(vEdges)/2 );
+ Gia_AigerWrite( pGia, pFileName, 0, 0 );
+ Gia_ManStop( pGia );
+ printf( "Finished dumping AIG into file \"%s\".\n", pFileName );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Build frontier.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_GraphBuildState( Vec_Int_t * vState, int e, int x, Vec_Int_t * vEdges, Vec_Int_t * vLife, Vec_Wec_t * vFronts, int * pFront, Vec_Int_t * vStateNew, int fVerbose )
+{
+ Vec_Int_t * vFront = Vec_WecEntry( vFronts, e );
+ Vec_Int_t * vFront2 = Vec_WecEntry( vFronts, e+1 );
+ int * pNodes = Vec_IntEntryP(vEdges, 2*e);
+ int nNodes = Vec_IntSize(vLife)/2;
+ int i, n, Node, First, pEquivs[2];
+ assert( pNodes[0] < pNodes[1] );
+ if ( fVerbose ) printf( "Edge = %d. Arc = %d.\nCurrent state: ", e, x );
+ Vec_IntForEachEntry( vFront, Node, i )
+ {
+ pFront[Node] = Vec_IntEntry(vState, i);
+ if ( fVerbose ) printf( "%d(%d) ", pFront[Node] & 0xFFFF, pFront[Node] >> 16 );
+ }
+ if ( fVerbose ) printf( "\n" );
+ for ( n = 0; n < 2; n++ )
+ if ( Vec_IntEntry(vLife, 2*pNodes[n]) == e ) // first time
+ pFront[pNodes[n]] = pNodes[n]; // degree = 0; comp = singleton
+ if ( x )
+ {
+ if ( (pFront[pNodes[0]] & 0xFFFF) == (pFront[pNodes[1]] & 0xFFFF) ) // the same comp
+ return -1; // const 0
+ for ( n = 0; n < 2; n++ )
+ {
+ int Degree = pFront[pNodes[n]] >> 16;
+ if ( (pNodes[n] == 0 || pNodes[n] == nNodes-1) ? Degree >= 1 : Degree >= 2 )
+ return -1; // const 0
+ pFront[pNodes[n]] += (1 << 16); // degree++
+ }
+ }
+ // remember equivalence classes
+ pEquivs[0] = pFront[pNodes[0]] & 0xFFFF;
+ pEquivs[1] = pFront[pNodes[1]] & 0xFFFF;
+ // remove some nodes from the frontier
+ for ( n = 0; n < 2; n++ )
+ if ( Vec_IntEntry(vLife, 2*pNodes[n]+1) == e ) // last time
+ {
+ int Degree = pFront[pNodes[n]] >> 16;
+ if ( (pNodes[n] == 0 || pNodes[n] == nNodes-1) ? Degree != 1 : Degree != 0 && Degree != 2 )
+ return -1; // const 0
+ // if it is part of the comp, update
+ First = -1;
+ Vec_IntForEachEntry( vFront2, Node, i )
+ {
+ assert( Node != pNodes[n] );
+ if ( (pFront[Node] & 0xFFFF) == pEquivs[n] )
+ {
+ if ( First == -1 )
+ First = Node;
+ pFront[Node] = (pFront[Node] & 0xFFFF0000) | First;
+ }
+ }
+ if ( First != -1 )
+ pEquivs[n] = First;
+ }
+ if ( x )
+ {
+ // union comp
+ int First = -1;
+ Vec_IntForEachEntry( vFront2, Node, i )
+ if ( (pFront[Node] & 0xFFFF) == pEquivs[0] || (pFront[Node] & 0xFFFF) == pEquivs[1] )
+ {
+ if ( First == -1 )
+ First = Node;
+ pFront[Node] = (pFront[Node] & 0xFFFF0000) | First;
+ }
+ }
+ // create next state
+ Vec_IntClear( vStateNew );
+ if ( fVerbose ) printf( "Next state: " );
+ Vec_IntForEachEntry( vFront2, Node, i )
+ {
+ Vec_IntPush( vStateNew, pFront[Node] );
+ if ( fVerbose ) printf( "%d(%d) ", pFront[Node] & 0xFFFF, pFront[Node] >> 16 );
+ }
+ if ( fVerbose ) printf( "\n\n" );
+ return 1;
+}
+void Abc_GraphBuildFrontier( int nSize, Vec_Int_t * vEdges, Vec_Int_t * vLife, Vec_Wec_t * vFronts, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ double nPaths;
+ int nEdges = Vec_IntSize(vEdges)/2;
+ int nNodes = Vec_IntSize(vLife)/2;
+ Vec_Wec_t * vNodes = Vec_WecAlloc( nEdges );
+ Vec_Int_t * vStateNew = Vec_IntAlloc( nNodes );
+ Vec_Int_t * vStateCount = Vec_IntAlloc( nEdges );
+ int e, s, x, Next, * pFront = ABC_CALLOC( int, nNodes );
+ Hsh_VecMan_t * pThis = Hsh_VecManStart( 1000 );
+ Hsh_VecMan_t * pNext = Hsh_VecManStart( 1000 );
+ Hsh_VecManAdd( pThis, vStateNew );
+ for ( e = 0; e < nEdges; e++ )
+ {
+ Vec_Int_t * vNode = Vec_WecPushLevel(vNodes);
+ int nStates = Hsh_VecSize( pThis );
+ Vec_IntPush( vStateCount, nStates );
+ if ( fVerbose )
+ {
+ printf( "\n" );
+ printf( "Processing edge %d = {%d %d}\n", e, Vec_IntEntry(vEdges, 2*e), Vec_IntEntry(vEdges, 2*e+1) );
+ printf( "Frontier: " ); Vec_IntPrint( Vec_WecEntry(vFronts, e) );
+ printf( "\n" );
+ }
+ for ( s = 0; s < nStates; s++ )
+ {
+ Vec_Int_t * vState = Hsh_VecReadEntry(pThis, s);
+ for ( x = 0; x < 2; x++ )
+ {
+ Next = Abc_GraphBuildState(vState, e, x, vEdges, vLife, vFronts, pFront, vStateNew, fVerbose);
+ if ( Next == 1 )
+ {
+ if ( e == nEdges - 1 ) // last edge
+ Next = -2; // const1
+ else
+ Next = Hsh_VecManAdd( pNext, vStateNew );
+ }
+ if ( fVerbose ) printf( "Return value = %d\n", Next );
+ Vec_IntPush( vNode, Next );
+ }
+ }
+ Hsh_VecManStop( pThis );
+ pThis = pNext;
+ pNext = Hsh_VecManStart( 1000 );
+ }
+ nPaths = Abc_GraphCountPaths(vNodes, vEdges);
+ printf( "States = %8d Paths = %24.0f ", Vec_IntSum(vStateCount), nPaths );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVerbose )
+ Vec_IntPrint( vStateCount );
+ Abc_GraphDeriveGiaDump( vNodes, vEdges, nSize );
+ ABC_FREE( pFront );
+ Vec_WecFree( vNodes );
+ Vec_IntFree( vStateNew );
+ Vec_IntFree( vStateCount );
+ Hsh_VecManStop( pThis );
+ Hsh_VecManStop( pNext );
+}
+void Abc_EnumerateFrontierTest( int nSize )
+{
+ //int nSize = 3;
+ int fVerbose = 0;
+ Vec_Int_t * vEdges = Abc_GraphGrid( nSize );
+ Vec_Int_t * vLife = Abc_GraphNodeLife( vEdges, nSize );
+ Vec_Wec_t * vFronts = Abc_GraphFrontiers( vEdges, vLife );
+
+ Abc_GraphBuildFrontier( nSize, vEdges, vLife, vFronts, fVerbose );
+
+ Vec_WecFree( vFronts );
+ Vec_IntFree( vLife );
+ Vec_IntFree( vEdges );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Performs SAT-based path enumeration.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+double Abc_Word2Double( word w )
+{
+ double Res = 0; int i;
+ for ( i = 0; i < 64; i++ )
+ if ( (w >> i) & 1 )
+ Res += pow(2,i);
+ return Res;
+}
+void Abc_GraphSolve( Gia_Man_t * pGia )
+{
+ int nIters = 1000;
+ Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 );
+ sat_solver * pSat; Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+ int i, k, iLit, nVars = Gia_ManCiNum(pGia);
+ int iCiVarBeg = pCnf->nVars - nVars;
+ word Total = 0;
+ word Mint1 = 0;
+ word Mint2 = 0;
+
+ // restart the SAT solver
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, pCnf->nVars );
+ // add timeframe clauses
+ for ( i = 0; i < pCnf->nClauses; i++ )
+ if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+ assert( 0 );
+ // create trivial assignment
+ Vec_IntClear( vLits );
+ for ( k = 0; k < nVars; k++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(iCiVarBeg+k, 1) );
+ // generate random assignment
+ for ( i = 0; i < nIters; i++ )
+ {
+ int Status = sat_solver_solve_lexsat( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) );
+ if ( Status != l_True )
+ break;
+ assert( Status == l_True );
+ // block this assignment
+ Vec_IntForEachEntry( vLits, iLit, k )
+ Vec_IntWriteEntry( vLits, k, Abc_LitNot(iLit) );
+ if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ) )
+ break;
+ Vec_IntForEachEntry( vLits, iLit, k )
+ Vec_IntWriteEntry( vLits, k, Abc_LitNot(iLit) );
+ // collect new minterm
+ Mint2 = 0;
+ Vec_IntForEachEntry( vLits, iLit, k )
+ if ( !Abc_LitIsCompl(iLit) )
+ Mint2 |= ((word)1) << (nVars-1-k);
+ if ( Mint1 == 0 )
+ Mint1 = Mint2;
+ // report
+ //printf( "Iter %3d : ", i );
+ //Extra_PrintBinary( stdout, (unsigned *)&Mint2, Abc_MinInt(64, nVars) ); printf( "\n" );
+ }
+ //Mint1 = 0;
+ Total = (Mint2-Mint1)/nIters;
+ printf( "Vars = %d Iters = %d Ave = %.0f Total = %.0f ", nVars, nIters, Abc_Word2Double(Mint2-Mint1), Abc_Word2Double(Total) );
+ printf( "Estimate = %.0f\n", (pow(2,nVars)-Abc_Word2Double(Mint1))/Abc_Word2Double((Mint2-Mint1)/nIters) );
+
+ sat_solver_delete( pSat );
+ Cnf_DataFree( pCnf );
+ Vec_IntFree( vLits );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index c8d70f26..9db290e5 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -4,9 +4,11 @@ SRC += src/misc/extra/extraUtilBitMatrix.c \
src/misc/extra/extraUtilDsd.c \
src/misc/extra/extraUtilEnum.c \
src/misc/extra/extraUtilFile.c \
+ src/misc/extra/extraUtilMaj.c \
src/misc/extra/extraUtilMemory.c \
src/misc/extra/extraUtilMisc.c \
src/misc/extra/extraUtilMult.c \
+ src/misc/extra/extraUtilPath.c \
src/misc/extra/extraUtilPerm.c \
src/misc/extra/extraUtilProgress.c \
src/misc/extra/extraUtilReader.c \
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index 36da1271..3d3f80b8 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1154,6 +1154,10 @@ static inline int Abc_Tt6HasVar( word t, int iVar )
{
return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) != (t & s_Truths6Neg[iVar]);
}
+static inline int Abc_Tt6XorVar( word t, int iVar )
+{
+ return ((t >> (1<<iVar)) & s_Truths6Neg[iVar]) == ~(t & s_Truths6Neg[iVar]);
+}
static inline int Abc_TtHasVar( word * t, int nVars, int iVar )
{
assert( iVar < nVars );
@@ -3094,6 +3098,99 @@ static inline int Abc_Tt4Check( int t )
return 0;
}
+
+/**Function*************************************************************
+
+ Synopsis [Returns symmetry profile of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_Tt6VarsAreSymmetric( word t, int iVar, int jVar )
+{
+ word * s_PMasks = s_PPMasks[iVar][jVar];
+ int shift = (1 << jVar) - (1 << iVar);
+ assert( iVar < jVar );
+ return ((t & s_PMasks[1]) << shift) == (t & s_PMasks[2]);
+}
+static inline int Abc_Tt6VarsAreAntiSymmetric( word t, int iVar, int jVar )
+{
+ word * s_PMasks = s_PPMasks[iVar][jVar];
+ int shift = (1 << jVar) + (1 << iVar);
+ assert( iVar < jVar );
+ return ((t & (s_PMasks[1] >> (1 << iVar))) << shift) == (t & (s_PMasks[2] << (1 << iVar)));
+}
+static inline int Abc_TtVarsAreSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ assert( i < nVars && j < nVars );
+ Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
+ Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
+ Abc_TtCofactor1( pCof0, nWords, j );
+ Abc_TtCofactor0( pCof1, nWords, j );
+ return Abc_TtEqual( pCof0, pCof1, nWords );
+}
+static inline int Abc_TtVarsAreAntiSymmetric( word * pTruth, int nVars, int i, int j, word * pCof0, word * pCof1 )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ assert( i < nVars && j < nVars );
+ Abc_TtCofactor0p( pCof0, pTruth, nWords, i );
+ Abc_TtCofactor1p( pCof1, pTruth, nWords, i );
+ Abc_TtCofactor0( pCof0, nWords, j );
+ Abc_TtCofactor1( pCof1, nWords, j );
+ return Abc_TtEqual( pCof0, pCof1, nWords );
+}
+static inline int Abc_TtIsFullySymmetric( word * pTruth, int nVars )
+{
+ int m, v, Polar = 0, Seen = 0;
+ for ( m = 0; m < (1<<nVars); m++ )
+ {
+ int Count = 0;
+ int Value = Abc_TtGetBit( pTruth, m );
+ for ( v = 0; v < nVars; v++ )
+ Count += ((m >> v) & 1);
+ if ( (Seen >> Count) & 1 ) // seen this count
+ {
+ if ( Value != ((Polar >> Count) & 1) )
+ return -1;
+ }
+ else // new count
+ {
+ Seen |= 1 << Count;
+ if ( Value )
+ Polar |= 1 << Count;
+ }
+ }
+ return Polar;
+}
+static inline void Abc_TtGenFullySymmetric( word * pTruth, int nVars, int Polar )
+{
+ int m, v, nWords = Abc_TtWordNum( nVars );
+ Abc_TtClear( pTruth, nWords );
+ for ( m = 0; m < (1<<nVars); m++ )
+ {
+ int Count = 0;
+ for ( v = 0; v < nVars; v++ )
+ Count += ((m >> v) & 1);
+ if ( (Polar >> Count) & 1 )
+ Abc_TtSetBit( pTruth, m );
+ }
+}
+static inline void Abc_TtTestFullySymmetric()
+{
+ word pTruth[4]; // 8-var function
+ int PolarOut, PolarIn = 271;
+ Abc_TtGenFullySymmetric( pTruth, 8, PolarIn );
+ //Abc_TtXorBit( pTruth, 171 );
+ PolarOut = Abc_TtIsFullySymmetric( pTruth, 8 );
+ assert( PolarIn == PolarOut );
+}
+
+
/*=== utilTruth.c ===========================================================*/
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index 72b653b7..c2bd06f0 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -341,10 +341,24 @@ static int * Vec_MemHashLookup( Vec_Mem_t * p, word * pEntry )
return pSpot;
return pSpot;
}
+static void Vec_MemHashProfile( Vec_Mem_t * p )
+{
+ int e;
+ for ( e = 0; e < 1000; e++ )
+ {
+ int Count = 0;
+ int * pSpot = Vec_IntEntryP( p->vTable, e );
+ for ( ; *pSpot != -1; pSpot = Vec_IntEntryP(p->vNexts, *pSpot) )
+ Count++;
+ printf( "%d ", Count );
+ }
+ printf( "\n" );
+}
static void Vec_MemHashResize( Vec_Mem_t * p )
{
word * pEntry;
int i, * pSpot;
+ //Vec_MemHashProfile( p );
Vec_IntFill( p->vTable, Abc_PrimeCudd(2 * Vec_IntSize(p->vTable)), -1 );
Vec_IntClear( p->vNexts );
Vec_MemForEachEntry( p, pEntry, i )
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-13 20:12:15 +0000