summaryrefslogtreecommitdiffstats
path: root/src/aig/kit
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit')
-rw-r--r--src/aig/kit/cloud.c5
-rw-r--r--src/aig/kit/cloud.h17
-rw-r--r--src/aig/kit/kit.h70
-rw-r--r--src/aig/kit/kitAig.c13
-rw-r--r--src/aig/kit/kitBdd.c11
-rw-r--r--src/aig/kit/kitCloud.c34
-rw-r--r--src/aig/kit/kitDec.c343
-rw-r--r--src/aig/kit/kitDsd.c265
-rw-r--r--src/aig/kit/kitFactor.c5
-rw-r--r--src/aig/kit/kitGraph.c5
-rw-r--r--src/aig/kit/kitHop.c13
-rw-r--r--src/aig/kit/kitIsop.c5
-rw-r--r--src/aig/kit/kitPla.c191
-rw-r--r--src/aig/kit/kitSop.c7
-rw-r--r--src/aig/kit/kitTruth.c403
-rw-r--r--src/aig/kit/kit_.c5
16 files changed, 1309 insertions, 83 deletions
diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
index dc57e2b7..fd372970 100644
--- a/src/aig/kit/cloud.c
+++ b/src/aig/kit/cloud.c
@@ -18,6 +18,9 @@
#include "cloud.h"
+ABC_NAMESPACE_IMPL_START
+
+
// the number of operators using cache
static int CacheOperNum = 4;
@@ -985,3 +988,5 @@ void Cloud_PrintHashTable( CloudManager * dd )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h
index 6f6a1eae..c48b55de 100644
--- a/src/aig/kit/cloud.h
+++ b/src/aig/kit/cloud.h
@@ -19,15 +19,18 @@
#ifndef __CLOUD_H__
#define __CLOUD_H__
+
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <time.h>
+
#include "abc_global.h"
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
#ifdef _WIN32
#define inline __inline // compatible with MS VS 6.0
@@ -239,9 +242,11 @@ extern CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode *
extern void Cloud_PrintInfo( CloudManager * dd );
extern void Cloud_PrintHashTable( CloudManager * dd );
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 3b564da5..f1075c2f 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -21,6 +21,7 @@
#ifndef __KIT_H__
#define __KIT_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -38,9 +39,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
@@ -197,8 +199,10 @@ static inline void Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, i
static inline Kit_Edge_t Kit_EdgeCreate( int Node, int fCompl ) { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge; }
static inline unsigned Kit_EdgeToInt( Kit_Edge_t eEdge ) { return (eEdge.Node << 1) | eEdge.fCompl; }
static inline Kit_Edge_t Kit_IntToEdge( unsigned Edge ) { return Kit_EdgeCreate( Edge >> 1, Edge & 1 ); }
-static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; }
-static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; }
+//static inline unsigned Kit_EdgeToInt_( Kit_Edge_t eEdge ) { return *(unsigned *)&eEdge; }
+//static inline Kit_Edge_t Kit_IntToEdge_( unsigned Edge ) { return *(Kit_Edge_t *)&Edge; }
+static inline unsigned Kit_EdgeToInt_( Kit_Edge_t m ) { union { Kit_Edge_t x; unsigned y; } v; v.x = m; return v.y; }
+static inline Kit_Edge_t Kit_IntToEdge_( unsigned m ) { union { Kit_Edge_t x; unsigned y; } v; v.y = m; return v.x; }
static inline int Kit_GraphIsConst( Kit_Graph_t * pGraph ) { return pGraph->fConst; }
static inline int Kit_GraphIsConst0( Kit_Graph_t * pGraph ) { return pGraph->fConst && pGraph->eRoot.fCompl; }
@@ -219,8 +223,12 @@ static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t
static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node); }
static inline int Kit_GraphRootLevel( Kit_Graph_t * pGraph ) { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level; }
-static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
-static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
+static inline int Kit_SuppIsMinBase( int Supp ) { return (Supp & (Supp+1)) == 0; }
+
+//static inline int Kit_Float2Int( float Val ) { return *((int *)&Val); }
+//static inline float Kit_Int2Float( int Num ) { return *((float *)&Num); }
+static inline int Kit_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
+static inline float Kit_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
static inline int Kit_BitWordNum( int nBits ) { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); }
static inline unsigned Kit_BitMask( int nBits ) { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits); }
@@ -280,6 +288,14 @@ static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars
return 0;
return 1;
}
+static inline int Kit_TruthIsEqualWithCare( unsigned * pIn0, unsigned * pIn1, unsigned * pCare, int nVars )
+{
+ int w;
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ if ( (pIn0[w] & pCare[w]) != (pIn1[w] & pCare[w]) )
+ return 0;
+ return 1;
+}
static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
@@ -423,6 +439,30 @@ static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned
pOut[w] = pIn0[w] & pIn1[w];
}
}
+static inline void Kit_TruthOrPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
+{
+ int w;
+ if ( fCompl0 && fCompl1 )
+ {
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = ~(pIn0[w] & pIn1[w]);
+ }
+ else if ( fCompl0 && !fCompl1 )
+ {
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = ~pIn0[w] | pIn1[w];
+ }
+ else if ( !fCompl0 && fCompl1 )
+ {
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = pIn0[w] | ~pIn1[w];
+ }
+ else // if ( !fCompl0 && !fCompl1 )
+ {
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = pIn0[w] | pIn1[w];
+ }
+}
static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars )
{
int w;
@@ -547,7 +587,10 @@ extern char * Kit_PlaStart( void * p, int nCubes, int nVars );
extern char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover );
extern void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover );
extern char * Kit_PlaStoreSop( void * p, char * pSop );
-extern ABC_DLL char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
+extern char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
+extern char * Kit_PlaFromTruthNew( unsigned * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vStr );
+extern ABC_UINT64_T Kit_PlaToTruth6( char * pSop, int nVars );
+extern void Kit_PlaToTruth( char * pSop, int nVars, Vec_Ptr_t * vVars, unsigned * pTemp, unsigned * pTruth );
/*=== kitSop.c ==========================================================*/
extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
@@ -584,6 +627,8 @@ extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, i
extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
+extern int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 );
+extern int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
@@ -592,10 +637,13 @@ extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVar
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
+extern void Kit_TruthPrintProfile( unsigned * pTruth, int nVars );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
-#ifdef __cplusplus
-}
-#endif
#endif
diff --git a/src/aig/kit/kitAig.c b/src/aig/kit/kitAig.c
index 83012a8c..88f17fc2 100644
--- a/src/aig/kit/kitAig.c
+++ b/src/aig/kit/kitAig.c
@@ -21,6 +21,9 @@
#include "kit.h"
#include "aig.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -50,16 +53,16 @@ Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph )
return Aig_NotCond( Aig_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
- return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+ return Aig_NotCond( (Aig_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Kit_GraphForEachNode( pGraph, pNode, i )
{
- pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
- pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pAnd0 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
- return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+ return Aig_NotCond( (Aig_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
@@ -119,3 +122,5 @@ Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * p
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitBdd.c b/src/aig/kit/kitBdd.c
index 75caf949..1b24ac24 100644
--- a/src/aig/kit/kitBdd.c
+++ b/src/aig/kit/kitBdd.c
@@ -21,6 +21,9 @@
#include "kit.h"
#include "extra.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -111,13 +114,13 @@ DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph )
{
bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
- pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( pNode->pFunc );
+ pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 ); Cudd_Ref( (DdNode *)pNode->pFunc );
}
// deref the intermediate results
- bFunc = pNode->pFunc; Cudd_Ref( bFunc );
+ bFunc = (DdNode *)pNode->pFunc; Cudd_Ref( bFunc );
Kit_GraphForEachNode( pGraph, pNode, i )
- Cudd_RecursiveDeref( dd, pNode->pFunc );
+ Cudd_RecursiveDeref( dd, (DdNode *)pNode->pFunc );
Cudd_Deref( bFunc );
// complement the result if necessary
@@ -229,3 +232,5 @@ int Kit_SopFactorVerify( Vec_Int_t * vCover, Kit_Graph_t * pFForm, int nVars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c
index 525f89f5..dea56749 100644
--- a/src/aig/kit/kitCloud.c
+++ b/src/aig/kit/kitCloud.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -35,6 +38,9 @@ struct Kit_Mux_t_
unsigned i : 1; // complemented attr of top node
};
+static inline int Kit_Mux2Int( Kit_Mux_t m ) { union { Kit_Mux_t x; int y; } v; v.x = m; return v.y; }
+static inline Kit_Mux_t Kit_Int2Mux( int m ) { union { Kit_Mux_t x; int y; } v; v.y = m; return v.x; }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -180,7 +186,7 @@ int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e);
Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
// put the MUX into the array
- Vec_IntPush( vNodes, *((int *)&Mux) );
+ Vec_IntPush( vNodes, Kit_Mux2Int(Mux) );
}
assert( Vec_IntSize(vNodes) == nNodes );
// reset signatures
@@ -226,15 +232,15 @@ unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore,
Kit_Mux_t Mux;
int i, Entry;
assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
- pThis = Vec_PtrEntry( vStore, 0 );
+ pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
Kit_TruthFill( pThis, nVars );
Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
{
- Mux = *((Kit_Mux_t *)&Entry);
+ Mux = Kit_Int2Mux(Entry);
assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );
- pFan0 = Vec_PtrEntry( vStore, Mux.e );
- pFan1 = Vec_PtrEntry( vStore, Mux.t );
- pThis = Vec_PtrEntry( vStore, i );
+ pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
+ pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
+ pThis = (unsigned *)Vec_PtrEntry( vStore, i );
Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
}
// complement the result
@@ -274,14 +280,14 @@ unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars,
// printf( "Failed!\n" );
// compute truth table from the BDD
assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
- pThis = Vec_PtrEntry( vStore, 0 );
+ pThis = (unsigned *)Vec_PtrEntry( vStore, 0 );
Kit_TruthFill( pThis, nVarsAll );
Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
{
- Mux = *((Kit_Mux_t *)&Entry);
- pFan0 = Vec_PtrEntry( vStore, Mux.e );
- pFan1 = Vec_PtrEntry( vStore, Mux.t );
- pThis = Vec_PtrEntry( vStore, i );
+ Mux = Kit_Int2Mux(Entry);
+ pFan0 = (unsigned *)Vec_PtrEntry( vStore, Mux.e );
+ pFan1 = (unsigned *)Vec_PtrEntry( vStore, Mux.t );
+ pThis = (unsigned *)Vec_PtrEntry( vStore, i );
Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
}
// complement the result
@@ -319,7 +325,7 @@ void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars,
// compute supports from nodes
Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
{
- Mux = *((Kit_Mux_t *)&Entry);
+ Mux = Kit_Int2Mux(Entry);
Var = nVars - 1 - Mux.v;
pFan0 = puSuppAll + nSupps * Mux.e;
pFan1 = puSuppAll + nSupps * Mux.t;
@@ -344,7 +350,7 @@ void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars,
// compute supports from nodes
Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
{
- Mux = *((Kit_Mux_t *)&Entry);
+ Mux = Kit_Int2Mux(Entry);
// Var = nVars - 1 - Mux.v;
Var = Mux.v;
pFan0 = puSuppAll + nSupps * Mux.e;
@@ -368,3 +374,5 @@ void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars,
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitDec.c b/src/aig/kit/kitDec.c
new file mode 100644
index 00000000..afc7ef6c
--- /dev/null
+++ b/src/aig/kit/kitDec.c
@@ -0,0 +1,343 @@
+/**CFile****************************************************************
+
+ FileName [kitDec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Computation kit.]
+
+ Synopsis [Decomposition manager.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - November 18, 2009.]
+
+ Revision [$Id: kitDec.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// decomposition manager
+typedef struct Kit_ManDec_t_ Kit_ManDec_t;
+struct Kit_ManDec_t_
+{
+ int nVarsMax; // the max number of variables
+ int nWordsMax; // the max number of words
+ Vec_Ptr_t * vTruthVars; // elementary truth tables
+ Vec_Ptr_t * vTruthNodes; // internal truth tables
+ // current problem
+ int nVarsIn; // the current number of variables
+ Vec_Int_t * vLutsIn; // LUT truth tables
+ Vec_Int_t * vSuppIn; // LUT supports
+ char ATimeIn[64]; // variable arrival times
+ // extracted information
+ unsigned * pTruthIn; // computed truth table
+ unsigned * pTruthOut; // computed truth table
+ int nVarsOut; // the current number of variables
+ int nWordsOut; // the current number of words
+ char Order[32]; // new vars into old vars after supp minimization
+ // computed information
+ Vec_Int_t * vLutsOut; // problem decomposition
+ Vec_Int_t * vSuppOut; // problem decomposition
+ char ATimeOut[64]; // variable arrival times
+};
+
+static inline int Kit_DecOuputArrival( int nVars, Vec_Int_t * vLuts, char ATimes[] ) { return ATimes[nVars + Vec_IntSize(vLuts) - 1]; }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts Decmetry manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_ManDec_t * Kit_ManDecStart( int nVarsMax )
+{
+ Kit_ManDec_t * p;
+ assert( nVarsMax <= 20 );
+ p = ABC_CALLOC( Kit_ManDec_t, 1 );
+ p->nVarsMax = nVarsMax;
+ p->nWordsMax = Kit_TruthWordNum( p->nVarsMax );
+ p->vTruthVars = Vec_PtrAllocTruthTables( p->nVarsMax );
+ p->vTruthNodes = Vec_PtrAllocSimInfo( 64, p->nWordsMax );
+ p->vLutsIn = Vec_IntAlloc( 50 );
+ p->vSuppIn = Vec_IntAlloc( 50 );
+ p->vLutsOut = Vec_IntAlloc( 50 );
+ p->vSuppOut = Vec_IntAlloc( 50 );
+ p->pTruthIn = ABC_ALLOC( unsigned, p->nWordsMax );
+ p->pTruthOut = ABC_ALLOC( unsigned, p->nWordsMax );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops Decmetry manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_ManDecStop( Kit_ManDec_t * p )
+{
+ ABC_FREE( p->pTruthIn );
+ ABC_FREE( p->pTruthOut );
+ Vec_IntFreeP( &p->vLutsIn );
+ Vec_IntFreeP( &p->vSuppIn );
+ Vec_IntFreeP( &p->vLutsOut );
+ Vec_IntFreeP( &p->vSuppOut );
+ Vec_PtrFreeP( &p->vTruthVars );
+ Vec_PtrFreeP( &p->vTruthNodes );
+ ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Deriving timing information for the decomposed structure.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DecComputeOuputArrival( int nVars, Vec_Int_t * vSupps, int LutSize, char ATimesIn[], char ATimesOut[] )
+{
+ int i, v, iVar, nLuts, Delay;
+ nLuts = Vec_IntSize(vSupps) / LutSize;
+ assert( nLuts > 0 );
+ assert( Vec_IntSize(vSupps) % LutSize == 0 );
+ for ( v = 0; v < nVars; v++ )
+ ATimesOut[v] = ATimesIn[v];
+ for ( v = 0; v < nLuts; v++ )
+ {
+ Delay = 0;
+ for ( i = 0; i < LutSize; i++ )
+ {
+ iVar = Vec_IntEntry( vSupps, v * LutSize + i );
+ assert( iVar < nVars + v );
+ Delay = ABC_MAX( Delay, ATimesOut[iVar] );
+ }
+ ATimesOut[nVars + v] = Delay + 1;
+ }
+ return ATimesOut[nVars + nLuts - 1];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DecComputeTruthOne( int LutSize, unsigned * pTruthLut, int nVars, unsigned * pTruths[], unsigned * pTemp, unsigned * pRes )
+{
+ int i, v;
+ Kit_TruthClear( pRes, nVars );
+ for ( i = 0; i < (1<<LutSize); i++ )
+ {
+ if ( !Kit_TruthHasBit( pTruthLut, i ) )
+ continue;
+ Kit_TruthFill( pTemp, nVars );
+ for ( v = 0; v < LutSize; v++ )
+ if ( i & (1<<v) )
+ Kit_TruthAnd( pTemp, pTemp, pTruths[v], nVars );
+ else
+ Kit_TruthSharp( pTemp, pTemp, pTruths[v], nVars );
+ Kit_TruthOr( pRes, pRes, pTemp, nVars );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DecComputeTruth( Kit_ManDec_t * p, int nVars, Vec_Int_t * vSupps, int LutSize, Vec_Int_t * vLuts, unsigned * pRes )
+{
+ unsigned * pResult, * pTruthLuts, * pTruths[17];
+ int nTruthLutWords, i, v, iVar, nLuts;
+ nLuts = Vec_IntSize(vSupps) / LutSize;
+ pTruthLuts = Vec_IntArray( vLuts );
+ nTruthLutWords = Kit_TruthWordNum( LutSize );
+ assert( nLuts > 0 );
+ assert( Vec_IntSize(vSupps) % LutSize == 0 );
+ assert( nLuts * nTruthLutWords == Vec_IntSize(vLuts) );
+ for ( v = 0; v < nLuts; v++ )
+ {
+ for ( i = 0; i < LutSize; i++ )
+ {
+ iVar = Vec_IntEntry( vSupps, v * LutSize + i );
+ assert( iVar < nVars + v );
+ pTruths[i] = (iVar < nVars)? Vec_PtrEntry(p->vTruthVars, iVar) : Vec_PtrEntry(p->vTruthNodes, iVar-nVars);
+ }
+ pResult = (v == nLuts - 1) ? pRes : Vec_PtrEntry(p->vTruthNodes, v);
+ Kit_DecComputeTruthOne( LutSize, pTruthLuts, nVars, pTruths, Vec_PtrEntry(p->vTruthNodes, v+1), pResult );
+ pTruthLuts += nTruthLutWords;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DecComputePattern( int nVars, unsigned * pTruth, int LutSize, int Pattern[] )
+{
+ int nCofs = (1 << LutSize);
+ int i, k, nMyu = 0;
+ assert( LutSize <= 6 );
+ assert( LutSize < nVars );
+ if ( nVars - LutSize <= 5 )
+ {
+ unsigned uCofs[64];
+ int nBits = (1 << (nVars - LutSize));
+ for ( i = 0; i < nCofs; i++ )
+ uCofs[i] = (pTruth[(i*nBits)/32] >> ((i*nBits)%32)) & ((1<<nBits)-1);
+ for ( i = 0; i < nCofs; i++ )
+ {
+ for ( k = 0; k < nMyu; k++ )
+ if ( uCofs[i] == uCofs[k] )
+ {
+ Pattern[i] = k;
+ break;
+ }
+ if ( k == i )
+ Pattern[nMyu++] = i;
+ }
+ }
+ else
+ {
+ unsigned * puCofs[64];
+ int nWords = (1 << (nVars - LutSize - 5));
+ for ( i = 0; i < nCofs; i++ )
+ puCofs[i] = pTruth + nWords;
+ for ( i = 0; i < nCofs; i++ )
+ {
+ for ( k = 0; k < nMyu; k++ )
+ if ( Kit_TruthIsEqual( puCofs[i], puCofs[k], nVars - LutSize - 5 ) )
+ {
+ Pattern[i] = k;
+ break;
+ }
+ if ( k == i )
+ Pattern[nMyu++] = i;
+ }
+ }
+ return nMyu;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of shared variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DecComputeShared_rec( int Pattern[], int Vars[], int nVars, int Shared[], int iVarTry )
+{
+ int Pat0[32], Pat1[32], Shared0[5], Shared1[5], VarsNext[5];
+ int v, u, iVarsNext, iPat0, iPat1, m, nMints = (1 << nVars);
+ int nShared0, nShared1, nShared = 0;
+ for ( v = iVarTry; v < nVars; v++ )
+ {
+ iVarsNext = 0;
+ for ( u = 0; u < nVars; u++ )
+ if ( u == v )
+ VarsNext[iVarsNext++] = Vars[u];
+ iPat0 = iPat1 = 0;
+ for ( m = 0; m < nMints; m++ )
+ if ( m & (1 << v) )
+ Pat1[iPat1++] = m;
+ else
+ Pat0[iPat0++] = m;
+ assert( iPat0 == nMints / 2 );
+ assert( iPat1 == nMints / 2 );
+ nShared0 = Kit_DecComputeShared_rec( Pat0, VarsNext, nVars-1, Shared0, v + 1 );
+ if ( nShared0 == 0 )
+ continue;
+ nShared1 = Kit_DecComputeShared_rec( Pat1, VarsNext, nVars-1, Shared1, v + 1 );
+ if ( nShared1 == 0 )
+ continue;
+ Shared[nShared++] = v;
+ for ( u = 0; u < nShared0; u++ )
+ for ( m = 0; m < nShared1; m++ )
+ if ( Shared0[u] >= 0 && Shared1[m] >= 0 && Shared0[u] == Shared1[m] )
+ {
+ Shared[nShared++] = Shared0[u];
+ Shared0[u] = Shared1[m] = -1;
+ }
+ return nShared;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of shared variables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DecComputeShared( int Pattern[], int LutSize, int Shared[] )
+{
+ int i, Vars[6];
+ assert( LutSize <= 6 );
+ for ( i = 0; i < LutSize; i++ )
+ Vars[i] = i;
+ return Kit_DecComputeShared_rec( Pattern, Vars, LutSize, Shared, 0 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index a85262a9..fbf92e48 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -268,7 +271,7 @@ void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk )
if ( Kit_DsdLitIsCompl(pNtk->Root) )
fprintf( pFile, "!" );
Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) );
- fprintf( pFile, "\n" );
+// fprintf( pFile, "\n" );
}
/**Function*************************************************************
@@ -333,7 +336,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
- pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
+ pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
// special case: literal of an internal node
if ( pObj == NULL )
@@ -434,7 +437,7 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
// assign elementary truth ables
assert( pNtk->nVars <= p->nVars );
for ( i = 0; i < (int)pNtk->nVars; i++ )
- Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+ Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
// complement the truth table if needed
@@ -463,7 +466,7 @@ unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
- pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
+ pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
// special case: literal of an internal node
if ( pObj == NULL )
@@ -597,7 +600,7 @@ unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsign
// assign elementary truth tables
assert( pNtk->nVars <= p->nVars );
for ( i = 0; i < (int)pNtk->nVars; i++ )
- Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+ Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
// complement the truth table if needed
@@ -628,7 +631,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
- pTruthRes = Vec_PtrEntry( p->vTtNodes, Id );
+ pTruthRes = (unsigned *)Vec_PtrEntry( p->vTtNodes, Id );
if ( pObj == NULL )
{
assert( Id < pNtk->nVars );
@@ -812,7 +815,7 @@ unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsign
}
// assign elementary truth tables
for ( i = 0; i < (int)pNtk->nVars; i++ )
- Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
+ Kit_TruthCopy( (unsigned *)Vec_PtrEntry(p->vTtNodes, i), (unsigned *)Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp, iVar, pTruthDec );
// complement the truth table if needed
@@ -1125,7 +1128,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
return iLit;
if ( pObj->Type == KIT_DSD_AND )
{
- Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
+ Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, (int *)&nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
@@ -1134,7 +1137,7 @@ int Kit_DsdExpandNode_rec( Kit_DsdNtk_t * pNew, Kit_DsdNtk_t * p, int iLit )
if ( pObj->Type == KIT_DSD_XOR )
{
int fCompl = Kit_DsdLitIsCompl(iLit);
- Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew );
+ Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, (int *)&nLitsNew );
pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
for ( i = 0; i < pObjNew->nFans; i++ )
{
@@ -2716,8 +2719,252 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
ABC_FREE( ppCofs[0][0] );
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char ** Kit_DsdNpn4ClassNames()
+{
+ static const char * pNames[222] = {
+ "F = 0", /* 0 */
+ "F = (!d*(!c*(!b*!a)))", /* 1 */
+ "F = (!d*(!c*!b))", /* 2 */
+ "F = (!d*(!c*(b+a)))", /* 3 */
+ "F = (!d*(!c*!(b*a)))", /* 4 */
+ "F = (!d*!c)", /* 5 */
+ "F = (!d*16(a,b,c))", /* 6 */
+ "F = (!d*17(a,b,c))", /* 7 */
+ "F = (!d*18(a,b,c))", /* 8 */
+ "F = (!d*19(a,b,c))", /* 9 */
+ "F = (!d*CA(!b,!c,a))", /* 10 */
+ "F = (!d*(c+!(!b*!a)))", /* 11 */
+ "F = (!d*!(c*!(!b*!a)))", /* 12 */
+ "F = (!d*(c+b))", /* 13 */
+ "F = (!d*3D(a,b,c))", /* 14 */
+ "F = (!d*!(c*b))", /* 15 */
+ "F = (!d*(c+(b+!a)))", /* 16 */
+ "F = (!d*6B(a,b,c))", /* 17 */
+ "F = (!d*!(c*!(b+a)))", /* 18 */
+ "F = (!d*7E(a,b,c))", /* 19 */
+ "F = (!d*!(c*(b*a)))", /* 20 */
+ "F = (!d)", /* 21 */
+ "F = 0116(a,b,c,d)", /* 22 */
+ "F = 0117(a,b,c,d)", /* 23 */
+ "F = 0118(a,b,c,d)", /* 24 */
+ "F = 0119(a,b,c,d)", /* 25 */
+ "F = 011A(a,b,c,d)", /* 26 */
+ "F = 011B(a,b,c,d)", /* 27 */
+ "F = 29((!b*!a),c,d)", /* 28 */
+ "F = 2B((!b*!a),c,d)", /* 29 */
+ "F = 012C(a,b,c,d)", /* 30 */
+ "F = 012D(a,b,c,d)", /* 31 */
+ "F = 012F(a,b,c,d)", /* 32 */
+ "F = 013C(a,b,c,d)", /* 33 */
+ "F = 013D(a,b,c,d)", /* 34 */
+ "F = 013E(a,b,c,d)", /* 35 */
+ "F = 013F(a,b,c,d)", /* 36 */
+ "F = 0168(a,b,c,d)", /* 37 */
+ "F = 0169(a,b,c,d)", /* 38 */
+ "F = 016A(a,b,c,d)", /* 39 */
+ "F = 016B(a,b,c,d)", /* 40 */
+ "F = 016E(a,b,c,d)", /* 41 */
+ "F = 016F(a,b,c,d)", /* 42 */
+ "F = 017E(a,b,c,d)", /* 43 */
+ "F = 017F(a,b,c,d)", /* 44 */
+ "F = 0180(a,b,c,d)", /* 45 */
+ "F = 0181(a,b,c,d)", /* 46 */
+ "F = 0182(a,b,c,d)", /* 47 */
+ "F = 0183(a,b,c,d)", /* 48 */
+ "F = 0186(a,b,c,d)", /* 49 */
+ "F = 0187(a,b,c,d)", /* 50 */
+ "F = 0189(a,b,c,d)", /* 51 */
+ "F = 018B(a,b,c,d)", /* 52 */
+ "F = 018F(a,b,c,d)", /* 53 */
+ "F = 0196(a,b,c,d)", /* 54 */
+ "F = 0197(a,b,c,d)", /* 55 */
+ "F = 0198(a,b,c,d)", /* 56 */
+ "F = 0199(a,b,c,d)", /* 57 */
+ "F = 019A(a,b,c,d)", /* 58 */
+ "F = 019B(a,b,c,d)", /* 59 */
+ "F = 019E(a,b,c,d)", /* 60 */
+ "F = 019F(a,b,c,d)", /* 61 */
+ "F = 42(a,(!c*!b),d)", /* 62 */
+ "F = 46(a,(!c*!b),d)", /* 63 */
+ "F = 4A(a,(!c*!b),d)", /* 64 */
+ "F = CA((!c*!b),!d,a)", /* 65 */
+ "F = 01AC(a,b,c,d)", /* 66 */
+ "F = 01AD(a,b,c,d)", /* 67 */
+ "F = 01AE(a,b,c,d)", /* 68 */
+ "F = 01AF(a,b,c,d)", /* 69 */
+ "F = 01BC(a,b,c,d)", /* 70 */
+ "F = 01BD(a,b,c,d)", /* 71 */
+ "F = 01BE(a,b,c,d)", /* 72 */
+ "F = 01BF(a,b,c,d)", /* 73 */
+ "F = 01E8(a,b,c,d)", /* 74 */
+ "F = 01E9(a,b,c,d)", /* 75 */
+ "F = 01EA(a,b,c,d)", /* 76 */
+ "F = 01EB(a,b,c,d)", /* 77 */
+ "F = 25((!b*!a),c,d)", /* 78 */
+ "F = !CA(d,c,(!b*!a))", /* 79 */
+ "F = (d+!(!c*(!b*!a)))", /* 80 */
+ "F = 16(b,c,d)", /* 81 */
+ "F = 033D(a,b,c,d)", /* 82 */
+ "F = 17(b,c,d)", /* 83 */
+ "F = ((!d*!a)+(!c*!b))", /* 84 */
+ "F = !(!(!c*!b)*!(!d*!a))", /* 85 */
+ "F = 0358(a,b,c,d)", /* 86 */
+ "F = 0359(a,b,c,d)", /* 87 */
+ "F = 035A(a,b,c,d)", /* 88 */
+ "F = 035B(a,b,c,d)", /* 89 */
+ "F = 035E(a,b,c,d)", /* 90 */
+ "F = 035F(a,b,c,d)", /* 91 */
+ "F = 0368(a,b,c,d)", /* 92 */
+ "F = 0369(a,b,c,d)", /* 93 */
+ "F = 036A(a,b,c,d)", /* 94 */
+ "F = 036B(a,b,c,d)", /* 95 */
+ "F = 036C(a,b,c,d)", /* 96 */
+ "F = 036D(a,b,c,d)", /* 97 */
+ "F = 036E(a,b,c,d)", /* 98 */
+ "F = 036F(a,b,c,d)", /* 99 */
+ "F = 037C(a,b,c,d)", /* 100 */
+ "F = 037D(a,b,c,d)", /* 101 */
+ "F = 037E(a,b,c,d)", /* 102 */
+ "F = 18(b,c,d)", /* 103 */
+ "F = 03C1(a,b,c,d)", /* 104 */
+ "F = 19(b,c,d)", /* 105 */
+ "F = 03C5(a,b,c,d)", /* 106 */
+ "F = 03C6(a,b,c,d)", /* 107 */
+ "F = 03C7(a,b,c,d)", /* 108 */
+ "F = CA(!c,!d,b)", /* 109 */
+ "F = 03D4(a,b,c,d)", /* 110 */
+ "F = 03D5(a,b,c,d)", /* 111 */
+ "F = 03D6(a,b,c,d)", /* 112 */
+ "F = 03D7(a,b,c,d)", /* 113 */
+ "F = 03D8(a,b,c,d)", /* 114 */
+ "F = 03D9(a,b,c,d)", /* 115 */
+ "F = 03DB(a,b,c,d)", /* 116 */
+ "F = 03DC(a,b,c,d)", /* 117 */
+ "F = 03DD(a,b,c,d)", /* 118 */
+ "F = 03DE(a,b,c,d)", /* 119 */
+ "F = (d+!(!c*!b))", /* 120 */
+ "F = ((d+c)*(b+a))", /* 121 */
+ "F = 0661(a,b,c,d)", /* 122 */
+ "F = 0662(a,b,c,d)", /* 123 */
+ "F = 0663(a,b,c,d)", /* 124 */
+ "F = (!(d*c)*(b+a))", /* 125 */
+ "F = 0667(a,b,c,d)", /* 126 */
+ "F = 29((b+a),c,d)", /* 127 */
+ "F = 066B(a,b,c,d)", /* 128 */
+ "F = 2B((b+a),c,d)", /* 129 */
+ "F = 0672(a,b,c,d)", /* 130 */
+ "F = 0673(a,b,c,d)", /* 131 */
+ "F = 0676(a,b,c,d)", /* 132 */
+ "F = 0678(a,b,c,d)", /* 133 */
+ "F = 0679(a,b,c,d)", /* 134 */
+ "F = 067A(a,b,c,d)", /* 135 */
+ "F = 067B(a,b,c,d)", /* 136 */
+ "F = 067E(a,b,c,d)", /* 137 */
+ "F = 24((b+a),c,d)", /* 138 */
+ "F = 0691(a,b,c,d)", /* 139 */
+ "F = 0693(a,b,c,d)", /* 140 */
+ "F = 26((b+a),c,d)", /* 141 */
+ "F = 0697(a,b,c,d)", /* 142 */
+ "F = !CA(d,c,(b+a))", /* 143 */
+ "F = 06B0(a,b,c,d)", /* 144 */
+ "F = 06B1(a,b,c,d)", /* 145 */
+ "F = 06B2(a,b,c,d)", /* 146 */
+ "F = 06B3(a,b,c,d)", /* 147 */
+ "F = 06B4(a,b,c,d)", /* 148 */
+ "F = 06B5(a,b,c,d)", /* 149 */
+ "F = 06B6(a,b,c,d)", /* 150 */
+ "F = 06B7(a,b,c,d)", /* 151 */
+ "F = 06B9(a,b,c,d)", /* 152 */
+ "F = 06BD(a,b,c,d)", /* 153 */
+ "F = 2C((b+a),c,d)", /* 154 */
+ "F = 06F1(a,b,c,d)", /* 155 */
+ "F = 06F2(a,b,c,d)", /* 156 */
+ "F = CA((b+a),!d,c)", /* 157 */
+ "F = (d+!(!c*!(b+!a)))", /* 158 */
+ "F = 0776(a,b,c,d)", /* 159 */
+ "F = 16((b*a),c,d)", /* 160 */
+ "F = 0779(a,b,c,d)", /* 161 */
+ "F = 077A(a,b,c,d)", /* 162 */
+ "F = 077E(a,b,c,d)", /* 163 */
+ "F = 07B0(a,b,c,d)", /* 164 */
+ "F = 07B1(a,b,c,d)", /* 165 */
+ "F = 07B4(a,b,c,d)", /* 166 */
+ "F = 07B5(a,b,c,d)", /* 167 */
+ "F = 07B6(a,b,c,d)", /* 168 */
+ "F = 07BC(a,b,c,d)", /* 169 */
+ "F = 07E0(a,b,c,d)", /* 170 */
+ "F = 07E1(a,b,c,d)", /* 171 */
+ "F = 07E2(a,b,c,d)", /* 172 */
+ "F = 07E3(a,b,c,d)", /* 173 */
+ "F = 07E6(a,b,c,d)", /* 174 */
+ "F = 07E9(a,b,c,d)", /* 175 */
+ "F = 1C((b*a),c,d)", /* 176 */
+ "F = 07F1(a,b,c,d)", /* 177 */
+ "F = 07F2(a,b,c,d)", /* 178 */
+ "F = (d+!(!c*!(b*a)))", /* 179 */
+ "F = (d+c)", /* 180 */
+ "F = 1668(a,b,c,d)", /* 181 */
+ "F = 1669(a,b,c,d)", /* 182 */
+ "F = 166A(a,b,c,d)", /* 183 */
+ "F = 166B(a,b,c,d)", /* 184 */
+ "F = 166E(a,b,c,d)", /* 185 */
+ "F = 167E(a,b,c,d)", /* 186 */
+ "F = 1681(a,b,c,d)", /* 187 */
+ "F = 1683(a,b,c,d)", /* 188 */
+ "F = 1686(a,b,c,d)", /* 189 */
+ "F = 1687(a,b,c,d)", /* 190 */
+ "F = 1689(a,b,c,d)", /* 191 */
+ "F = 168B(a,b,c,d)", /* 192 */
+ "F = 168E(a,b,c,d)", /* 193 */
+ "F = 1696(a,b,c,d)", /* 194 */
+ "F = 1697(a,b,c,d)", /* 195 */
+ "F = 1698(a,b,c,d)", /* 196 */
+ "F = 1699(a,b,c,d)", /* 197 */
+ "F = 169A(a,b,c,d)", /* 198 */
+ "F = 169B(a,b,c,d)", /* 199 */
+ "F = 169E(a,b,c,d)", /* 200 */
+ "F = 16A9(a,b,c,d)", /* 201 */
+ "F = 16AC(a,b,c,d)", /* 202 */
+ "F = 16AD(a,b,c,d)", /* 203 */
+ "F = 16BC(a,b,c,d)", /* 204 */
+ "F = (d+E9(a,b,c))", /* 205 */
+ "F = 177E(a,b,c,d)", /* 206 */
+ "F = 178E(a,b,c,d)", /* 207 */
+ "F = 1796(a,b,c,d)", /* 208 */
+ "F = 1798(a,b,c,d)", /* 209 */
+ "F = 179A(a,b,c,d)", /* 210 */
+ "F = 17AC(a,b,c,d)", /* 211 */
+ "F = (d+E8(a,b,c))", /* 212 */
+ "F = (d+E7(a,b,c))", /* 213 */
+ "F = 19E1(a,b,c,d)", /* 214 */
+ "F = 19E3(a,b,c,d)", /* 215 */
+ "F = (d+E6(a,b,c))", /* 216 */
+ "F = 1BD8(a,b,c,d)", /* 217 */
+ "F = (d+CA(b,c,a))", /* 218 */
+ "F = (d+(c+(!b*!a)))", /* 219 */
+ "F = (d+(c+!b))", /* 220 */
+ "F = (d+(c+(b+a)))" /* 221 */
+ };
+ return (char **)pNames;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitFactor.c b/src/aig/kit/kitFactor.c
index 273d4821..3982d7a8 100644
--- a/src/aig/kit/kitFactor.c
+++ b/src/aig/kit/kitFactor.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -337,3 +340,5 @@ void Kit_FactorTest( unsigned * pTruth, int nVars )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitGraph.c b/src/aig/kit/kitGraph.c
index 565c000b..f407a93a 100644
--- a/src/aig/kit/kitGraph.c
+++ b/src/aig/kit/kitGraph.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -395,3 +398,5 @@ int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitHop.c b/src/aig/kit/kitHop.c
index 044633bc..0dad6295 100644
--- a/src/aig/kit/kitHop.c
+++ b/src/aig/kit/kitHop.c
@@ -21,6 +21,9 @@
#include "kit.h"
#include "hop.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -50,16 +53,16 @@ Hop_Obj_t * Kit_GraphToHopInternal( Hop_Man_t * pMan, Kit_Graph_t * pGraph )
return Hop_NotCond( Hop_ManConst1(pMan), Kit_GraphIsComplement(pGraph) );
// check for a literal
if ( Kit_GraphIsVar(pGraph) )
- return Hop_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+ return Hop_NotCond( (Hop_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Kit_GraphForEachNode( pGraph, pNode, i )
{
- pAnd0 = Hop_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
- pAnd1 = Hop_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
+ pAnd0 = Hop_NotCond( (Hop_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
+ pAnd1 = Hop_NotCond( (Hop_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Hop_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
- return Hop_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+ return Hop_NotCond( (Hop_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
}
/**Function*************************************************************
@@ -143,3 +146,5 @@ Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitIsop.c b/src/aig/kit/kitIsop.c
index 42fae2ea..18039dc5 100644
--- a/src/aig/kit/kitIsop.c
+++ b/src/aig/kit/kitIsop.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -323,3 +326,5 @@ unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitPla.c b/src/aig/kit/kitPla.c
index 776762c2..df6d4e11 100644
--- a/src/aig/kit/kitPla.c
+++ b/src/aig/kit/kitPla.c
@@ -21,6 +21,9 @@
#include "kit.h"
#include "aig.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -115,7 +118,9 @@ int Kit_PlaIsInv( char * pSop )
int Kit_PlaGetVarNum( char * pSop )
{
char * pCur;
- for ( pCur = pSop; *pCur != '\n'; pCur++ );
+ for ( pCur = pSop; *pCur != '\n'; pCur++ )
+ if ( *pCur == 0 )
+ return -1;
return pCur - pSop - 2;
}
@@ -205,7 +210,7 @@ void Kit_PlaComplement( char * pSop )
***********************************************************************/
char * Kit_PlaStart( void * p, int nCubes, int nVars )
{
- Aig_MmFlex_t * pMan = p;
+ Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
char * pSopCover, * pCube;
int i, Length;
@@ -237,7 +242,7 @@ char * Kit_PlaStart( void * p, int nCubes, int nVars )
***********************************************************************/
char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover )
{
- Aig_MmFlex_t * pMan = p;
+ Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
char * pSop, * pCube;
int i, k, Entry, Literal;
assert( Vec_IntSize(vCover) > 0 );
@@ -311,7 +316,7 @@ void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover )
***********************************************************************/
char * Kit_PlaStoreSop( void * p, char * pSop )
{
- Aig_MmFlex_t * pMan = p;
+ Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
char * pStore;
pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
strcpy( pStore, pSop );
@@ -331,7 +336,7 @@ char * Kit_PlaStoreSop( void * p, char * pSop )
***********************************************************************/
char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
{
- Aig_MmFlex_t * pMan = p;
+ Aig_MmFlex_t * pMan = (Aig_MmFlex_t *)p;
char * pSop;
int RetValue;
if ( Kit_TruthIsConst0(pTruth, nVars) )
@@ -347,8 +352,184 @@ char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCo
}
+/**Function*************************************************************
+
+ Synopsis [Creates the cover from the ISOP computed from TT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaFromIsop( Vec_Str_t * vStr, int nVars, Vec_Int_t * vCover )
+{
+ int i, k, Entry, Literal;
+ assert( Vec_IntSize(vCover) > 0 );
+ if ( Vec_IntSize(vCover) == 0 )
+ return NULL;
+ Vec_StrClear( vStr );
+ Vec_IntForEachEntry( vCover, Entry, i )
+ {
+ for ( k = 0; k < nVars; k++ )
+ {
+ Literal = 3 & (Entry >> (k << 1));
+ if ( Literal == 1 )
+ Vec_StrPush( vStr, '0' );
+ else if ( Literal == 2 )
+ Vec_StrPush( vStr, '1' );
+ else if ( Literal == 0 )
+ Vec_StrPush( vStr, '-' );
+ else
+ assert( 0 );
+ }
+ Vec_StrPush( vStr, ' ' );
+ Vec_StrPush( vStr, '1' );
+ Vec_StrPush( vStr, '\n' );
+ }
+ Vec_StrPush( vStr, '\0' );
+ return Vec_StrArray( vStr );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the SOP from TT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaFromTruthNew( unsigned * pTruth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vStr )
+{
+ char * pResult;
+ // transform truth table into the SOP
+ int RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 1 );
+ assert( RetValue == 0 || RetValue == 1 );
+ // check the case of constant cover
+ if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
+ {
+ assert( RetValue == 0 );
+ Vec_StrClear( vStr );
+ Vec_StrAppend( vStr, (Vec_IntSize(vCover) == 0) ? " 0\n" : " 1\n" );
+ Vec_StrPush( vStr, '\0' );
+ return Vec_StrArray( vStr );
+ }
+ pResult = Kit_PlaFromIsop( vStr, nVars, vCover );
+ if ( RetValue )
+ Kit_PlaComplement( pResult );
+ if ( nVars < 6 )
+ assert( pTruth[0] == (unsigned)Kit_PlaToTruth6(pResult, nVars) );
+ else if ( nVars == 6 )
+ assert( *((ABC_UINT64_T*)pTruth) == Kit_PlaToTruth6(pResult, nVars) );
+ return pResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts SOP into a truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+ABC_UINT64_T Kit_PlaToTruth6( char * pSop, int nVars )
+{
+ static ABC_UINT64_T Truth[8] = {
+ 0xAAAAAAAAAAAAAAAA,
+ 0xCCCCCCCCCCCCCCCC,
+ 0xF0F0F0F0F0F0F0F0,
+ 0xFF00FF00FF00FF00,
+ 0xFFFF0000FFFF0000,
+ 0xFFFFFFFF00000000,
+ 0x0000000000000000,
+ 0xFFFFFFFFFFFFFFFF
+ };
+ ABC_UINT64_T valueAnd, valueOr = Truth[6];
+ int v, lit = 0;
+ assert( nVars < 7 );
+ do {
+ valueAnd = Truth[7];
+ for ( v = 0; v < nVars; v++, lit++ )
+ {
+ if ( pSop[lit] == '1' )
+ valueAnd &= Truth[v];
+ else if ( pSop[lit] == '0' )
+ valueAnd &= ~Truth[v];
+ else if ( pSop[lit] != '-' )
+ assert( 0 );
+ }
+ valueOr |= valueAnd;
+ assert( pSop[lit] == ' ' );
+ lit++;
+ lit++;
+ assert( pSop[lit] == '\n' );
+ lit++;
+ } while ( pSop[lit] );
+ if ( Kit_PlaIsComplement(pSop) )
+ valueOr = ~valueOr;
+ return valueOr;
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Converting SOP into a truth table.]
+
+ Description [The SOP is represented as a C-string, as documented in
+ file "bblif.h". The truth table is returned as a bit-string composed
+ of 2^nVars bits. For functions of less than 6 variables, the full
+ machine word is returned. (The truth table looks as if the function
+ had 5 variables.) The use of this procedure should be limited to
+ Boolean functions with no more than 16 inputs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_PlaToTruth( char * pSop, int nVars, Vec_Ptr_t * vVars, unsigned * pTemp, unsigned * pTruth )
+{
+ int v, c, nCubes, fCompl = 0;
+ assert( pSop != NULL );
+ assert( nVars >= 0 );
+ if ( strlen(pSop) % (nVars + 3) != 0 )
+ {
+ printf( "Kit_PlaToTruth(): SOP is represented incorrectly.\n" );
+ return;
+ }
+ // iterate through the cubes
+ Kit_TruthClear( pTruth, nVars );
+ nCubes = strlen(pSop) / (nVars + 3);
+ for ( c = 0; c < nCubes; c++ )
+ {
+ fCompl = (pSop[nVars+1] == '0');
+ Kit_TruthFill( pTemp, nVars );
+ // iterate through the literals of the cube
+ for ( v = 0; v < nVars; v++ )
+ if ( pSop[v] == '1' )
+ Kit_TruthAnd( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
+ else if ( pSop[v] == '0' )
+ Kit_TruthSharp( pTemp, pTemp, (unsigned *)Vec_PtrEntry(vVars, v), nVars );
+ // add cube to storage
+ Kit_TruthOr( pTruth, pTruth, pTemp, nVars );
+ // go to the next cube
+ pSop += (nVars + 3);
+ }
+ if ( fCompl )
+ Kit_TruthNot( pTruth, pTruth, nVars );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitSop.c b/src/aig/kit/kitSop.c
index 0d1b9e2c..21ea69b8 100644
--- a/src/aig/kit/kitSop.c
+++ b/src/aig/kit/kitSop.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -510,7 +513,7 @@ void Kit_SopDivisorZeroKernel_rec( Kit_Sop_t * cSop, int nLits )
iLit = Kit_SopWorstLiteral( cSop, nLits );
if ( iLit == -1 )
return;
- // derive the cube-ABC_FREE quotient
+ // derive the cube-free quotient
Kit_SopDivideByLiteralQuo( cSop, iLit ); // the same cover
Kit_SopMakeCubeFree( cSop ); // the same cover
// call recursively
@@ -572,3 +575,5 @@ void Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uC
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index 3f9188c7..56f10ac0 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -187,7 +190,7 @@ void Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
Description [The input and output truth tables are in pIn/pOut. The current number
of variables is nVars. The total number of variables in nVarsAll. The last argument
- (Phase) contains shows what variables should remain.]
+ (Phase) shows what variables should remain.]
SideEffects [The input truth table is modified.]
@@ -229,7 +232,7 @@ void Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll,
***********************************************************************/
void Kit_TruthPermute( unsigned * pOut, unsigned * pIn, int nVars, char * pPerm, int fReturnIn )
{
- int * pTemp;
+ unsigned * pTemp;
int i, Temp, fChange, Counter = 0;
do {
fChange = 0;
@@ -404,6 +407,57 @@ void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
/**Function*************************************************************
+ Synopsis [Computes negative cofactor of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthCofactor0Count( unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step, Counter = 0;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x55555555);
+ return Counter;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x33333333);
+ return Counter;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x0F0F0F0F);
+ return Counter;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x00FF00FF);
+ return Counter;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i] & 0x0000FFFF);
+ return Counter;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ Counter += Kit_WordCountOnes(pTruth[i]);
+ pTruth += 2*Step;
+ }
+ return Counter;
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Computes positive cofactor of the function.]
Description []
@@ -598,7 +652,7 @@ int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int
return 1;
case 4:
for ( i = 0; i < nWords; i++ )
- if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
+ if ( ((pOnset[i] & (pOffset[i] >> 16)) | (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
return 0;
return 1;
default:
@@ -911,6 +965,77 @@ void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar
/**Function*************************************************************
+ Synopsis [Returns the number of minterms in the Boolean difference.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthBooleanDiffCount( unsigned * pTruth, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step, Counter = 0;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 1)) & 0x55555555 );
+ return Counter;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 2)) & 0x33333333 );
+ return Counter;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 4)) & 0x0F0F0F0F );
+ return Counter;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >> 8)) & 0x00FF00FF );
+ return Counter;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( (pTruth[i] ^ (pTruth[i] >>16)) & 0x0000FFFF );
+ return Counter;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ Counter += Kit_WordCountOnes( pTruth[i] ^ pTruth[Step+i] );
+ pTruth += 2*Step;
+ }
+ return Counter;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the number of minterms in the Boolean difference.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthXorCount( unsigned * pTruth0, unsigned * pTruth1, int nVars )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, Counter = 0;
+ for ( i = 0; i < nWords; i++ )
+ Counter += Kit_WordCountOnes( pTruth0[i] ^ pTruth1[i] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Universally quantifies the set of variables.]
Description []
@@ -1059,20 +1184,29 @@ void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1,
SeeAlso []
***********************************************************************/
-int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
+int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
{
- static unsigned uTemp0[16], uTemp1[16];
- assert( nVars <= 9 );
+ static unsigned uTemp0[32], uTemp1[32];
+ if ( pCof0 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof0 = uTemp0;
+ }
+ if ( pCof1 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof1 = uTemp1;
+ }
// compute Cof01
- Kit_TruthCopy( uTemp0, pTruth, nVars );
- Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
- Kit_TruthCofactor1( uTemp0, nVars, iVar1 );
+ Kit_TruthCopy( pCof0, pTruth, nVars );
+ Kit_TruthCofactor0( pCof0, nVars, iVar0 );
+ Kit_TruthCofactor1( pCof0, nVars, iVar1 );
// compute Cof10
- Kit_TruthCopy( uTemp1, pTruth, nVars );
- Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
- Kit_TruthCofactor0( uTemp1, nVars, iVar1 );
+ Kit_TruthCopy( pCof1, pTruth, nVars );
+ Kit_TruthCofactor1( pCof1, nVars, iVar0 );
+ Kit_TruthCofactor0( pCof1, nVars, iVar1 );
// compare
- return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
+ return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}
/**Function*************************************************************
@@ -1086,20 +1220,29 @@ int Kit_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
SeeAlso []
***********************************************************************/
-int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 )
+int Kit_TruthVarsAntiSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1, unsigned * pCof0, unsigned * pCof1 )
{
- static unsigned uTemp0[16], uTemp1[16];
- assert( nVars <= 9 );
+ static unsigned uTemp0[32], uTemp1[32];
+ if ( pCof0 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof0 = uTemp0;
+ }
+ if ( pCof1 == NULL )
+ {
+ assert( nVars <= 10 );
+ pCof1 = uTemp1;
+ }
// compute Cof00
- Kit_TruthCopy( uTemp0, pTruth, nVars );
- Kit_TruthCofactor0( uTemp0, nVars, iVar0 );
- Kit_TruthCofactor0( uTemp0, nVars, iVar1 );
+ Kit_TruthCopy( pCof0, pTruth, nVars );
+ Kit_TruthCofactor0( pCof0, nVars, iVar0 );
+ Kit_TruthCofactor0( pCof0, nVars, iVar1 );
// compute Cof11
- Kit_TruthCopy( uTemp1, pTruth, nVars );
- Kit_TruthCofactor1( uTemp1, nVars, iVar0 );
- Kit_TruthCofactor1( uTemp1, nVars, iVar1 );
+ Kit_TruthCopy( pCof1, pTruth, nVars );
+ Kit_TruthCofactor1( pCof1, nVars, iVar0 );
+ Kit_TruthCofactor1( pCof1, nVars, iVar1 );
// compare
- return Kit_TruthIsEqual( uTemp0, uTemp1, nVars );
+ return Kit_TruthIsEqual( pCof0, pCof1, nVars );
}
/**Function*************************************************************
@@ -1691,7 +1834,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
SeeAlso []
***********************************************************************/
-int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytes )
+int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pBytesInit )
{
// the number of 1s if every byte as well as in the 0-cofactors w.r.t. three variables
static unsigned Table[256] = {
@@ -1730,6 +1873,7 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
};
unsigned uSum;
unsigned char * pTruthC, * pLimit;
+ int * pBytes = pBytesInit;
int i, iVar, Step, nWords, nBytes, nTotal;
assert( nVars <= 20 );
@@ -1768,11 +1912,14 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt
for ( iVar = 3, Step = 1; Step < nBytes; Step *= 2, iVar++ )
for ( i = 0; i < nBytes; i += Step + Step )
{
- pRes[iVar] += pBytes[i];
- pBytes[i] += pBytes[i+Step];
+ pRes[iVar] += pBytesInit[i];
+ pBytesInit[i] += pBytesInit[i+Step];
}
- assert( pBytes[0] == nTotal );
+ assert( pBytesInit[0] == nTotal );
assert( iVar == nVars );
+
+ for ( i = 0; i < nVars; i++ )
+ assert( pRes[i] == Kit_TruthCofactor0Count(pTruth, nVars, i) );
return nTotal;
}
@@ -1866,8 +2013,210 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
}
+/**Function*************************************************************
+
+ Synopsis [Dumps truth table into a file.]
+
+ Description [Generates script file for reading into ABC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthPrintProfile_int( unsigned * pTruth, int nVars )
+{
+ int Mints[20];
+ int Mints0[20];
+ int Mints1[20];
+ int Unique1[20];
+ int Total2[20][20];
+ int Unique2[20][20];
+ int Common2[20][20];
+ int nWords = Kit_TruthWordNum( nVars );
+ int * pBytes = ABC_ALLOC( int, nWords * 4 );
+ unsigned * pIn = ABC_ALLOC( unsigned, nWords );
+ unsigned * pOut = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof00 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof01 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof10 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pCof11 = ABC_ALLOC( unsigned, nWords );
+ unsigned * pTemp;
+ int nTotalMints, nTotalMints0, nTotalMints1;
+ int v, u, i, iVar, nMints1;
+ int Cof00, Cof01, Cof10, Cof11;
+ int Coz00, Coz01, Coz10, Coz11;
+ assert( nVars <= 20 );
+ assert( nVars >= 6 );
+
+ nTotalMints = Kit_TruthCountMinterms( pTruth, nVars, Mints, pBytes );
+ for ( v = 0; v < nVars; v++ )
+ Unique1[v] = Kit_TruthBooleanDiffCount( pTruth, nVars, v );
+
+ for ( v = 0; v < nVars; v++ )
+ for ( u = 0; u < nVars; u++ )
+ Total2[v][u] = Unique2[v][u] = Common2[v][u] = -1;
+
+ nMints1 = (1<<(nVars-2));
+ for ( v = 0; v < nVars; v++ )
+ {
+ // move this var to be the first
+ Kit_TruthCopy( pIn, pTruth, nVars );
+// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
+ for ( i = v; i < nVars - 1; i++ )
+ {
+ Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+ pTemp = pIn; pIn = pOut; pOut = pTemp;
+ }
+// Extra_PrintBinary( stdout, pIn, (1<<nVars) ); printf( "\n" );
+// printf( "\n" );
+
+
+ // count minterms in both cofactor
+ nTotalMints0 = Kit_TruthCountMinterms( pIn, nVars-1, Mints0, pBytes );
+ nTotalMints1 = Kit_TruthCountMinterms( pIn+nWords/2, nVars-1, Mints1, pBytes );
+ assert( nTotalMints == nTotalMints0 + nTotalMints1 );
+/*
+ for ( u = 0; u < nVars-1; u++ )
+ printf( "%2d ", Mints0[u] );
+ printf( "\n" );
+
+ for ( u = 0; u < nVars-1; u++ )
+ printf( "%2d ", Mints1[u] );
+ printf( "\n" );
+*/
+ for ( u = 0; u < nVars-1; u++ )
+ {
+ if ( u < v )
+ iVar = u;
+ else
+ iVar = u + 1;
+ assert( v != iVar );
+ // get minter counts in the cofactors
+ Cof00 = Mints0[u]; Coz00 = nMints1 - Cof00;
+ Cof01 = nTotalMints0-Mints0[u]; Coz01 = nMints1 - Cof01;
+ Cof10 = Mints1[u]; Coz10 = nMints1 - Cof10;
+ Cof11 = nTotalMints1-Mints1[u]; Coz11 = nMints1 - Cof11;
+
+ assert( Cof00 >= 0 && Cof00 <= nMints1 );
+ assert( Cof01 >= 0 && Cof01 <= nMints1 );
+ assert( Cof10 >= 0 && Cof10 <= nMints1 );
+ assert( Cof11 >= 0 && Cof11 <= nMints1 );
+
+ assert( Coz00 >= 0 && Coz00 <= nMints1 );
+ assert( Coz01 >= 0 && Coz01 <= nMints1 );
+ assert( Coz10 >= 0 && Coz10 <= nMints1 );
+ assert( Coz11 >= 0 && Coz11 <= nMints1 );
+
+ Common2[v][iVar] = Common2[iVar][v] = Cof00 * Coz11 + Coz00 * Cof11 + Cof01 * Coz10 + Coz01 * Cof10;
+
+ Total2[v][iVar] = Total2[iVar][v] =
+ Cof00 * Coz01 + Coz00 * Cof01 +
+ Cof00 * Coz10 + Coz00 * Cof10 +
+ Cof00 * Coz11 + Coz00 * Cof11 +
+ Cof01 * Coz10 + Coz01 * Cof10 +
+ Cof01 * Coz11 + Coz01 * Cof11 +
+ Cof10 * Coz11 + Coz10 * Cof11 ;
+
+
+ Kit_TruthCofactor0New( pCof00, pIn, nVars-1, u );
+ Kit_TruthCofactor1New( pCof01, pIn, nVars-1, u );
+ Kit_TruthCofactor0New( pCof10, pIn+nWords/2, nVars-1, u );
+ Kit_TruthCofactor1New( pCof11, pIn+nWords/2, nVars-1, u );
+
+ Unique2[v][iVar] = Unique2[iVar][v] =
+ Kit_TruthXorCount( pCof00, pCof01, nVars-1 ) +
+ Kit_TruthXorCount( pCof00, pCof10, nVars-1 ) +
+ Kit_TruthXorCount( pCof00, pCof11, nVars-1 ) +
+ Kit_TruthXorCount( pCof01, pCof10, nVars-1 ) +
+ Kit_TruthXorCount( pCof01, pCof11, nVars-1 ) +
+ Kit_TruthXorCount( pCof10, pCof11, nVars-1 );
+ }
+ }
+
+ printf( "\n" );
+ printf( " V: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8c ", v+'a' );
+ printf( "\n" );
+
+ printf( " M: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Mints[v] );
+ printf( "\n" );
+
+ printf( " U: " );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Unique1[v] );
+ printf( "\n" );
+ printf( "\n" );
+
+ printf( "Unique:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Unique2[i][v] );
+ printf( "\n" );
+ }
+
+ printf( "Common:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Common2[i][v] );
+ printf( "\n" );
+ }
+
+ printf( "Total:\n" );
+ for ( i = 0; i < nVars; i++ )
+ {
+ printf( " %2d ", i );
+ for ( v = 0; v < nVars; v++ )
+ printf( "%8d ", Total2[i][v] );
+ printf( "\n" );
+ }
+
+ ABC_FREE( pIn );
+ ABC_FREE( pOut );
+ ABC_FREE( pCof00 );
+ ABC_FREE( pCof01 );
+ ABC_FREE( pCof10 );
+ ABC_FREE( pCof11 );
+ ABC_FREE( pBytes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dumps truth table into a file.]
+
+ Description [Generates script file for reading into ABC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_TruthPrintProfile( unsigned * pTruth, int nVars )
+{
+ unsigned uTruth[2];
+ if ( nVars >= 6 )
+ {
+ Kit_TruthPrintProfile_int( pTruth, nVars );
+ return;
+ }
+ assert( nVars >= 2 );
+ uTruth[0] = pTruth[0];
+ uTruth[1] = pTruth[0];
+ Kit_TruthPrintProfile( uTruth, 6 );
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/kit/kit_.c b/src/aig/kit/kit_.c
index 5c68ee3c..37be0b49 100644
--- a/src/aig/kit/kit_.c
+++ b/src/aig/kit/kit_.c
@@ -20,6 +20,9 @@
#include "kit.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 06:05:02 +0000