abc70930: src/aig/kit/kit.h Source File

00001 
00021 #ifndef __KIT_H__
00022 #define __KIT_H__
00023 
00024 #ifdef __cplusplus
00025 extern "C" {
00026 #endif
00027 
00031 
00032 #include <stdio.h>
00033 #include <stdlib.h>
00034 #include <string.h>
00035 #include <assert.h>
00036 #include <time.h>
00037 #include "vec.h"
00038 #include "extra.h"
00039 #include "cloud.h"
00040 
00044 
00048 
00049 typedef struct Kit_Sop_t_ Kit_Sop_t;
00050 struct Kit_Sop_t_
00051 {
00052     int               nCubes;         // the number of cubes
00053     unsigned *        pCubes;         // the storage for cubes
00054 };
00055 
00056 typedef struct Kit_Edge_t_ Kit_Edge_t;
00057 struct Kit_Edge_t_
00058 {
00059     unsigned          fCompl   :  1;   // the complemented bit
00060     unsigned          Node     : 30;   // the decomposition node pointed by the edge
00061 };
00062 
00063 typedef struct Kit_Node_t_ Kit_Node_t;
00064 struct Kit_Node_t_
00065 {
00066     Kit_Edge_t        eEdge0;          // the left child of the node
00067     Kit_Edge_t        eEdge1;          // the right child of the node
00068     // other info
00069     void *            pFunc;           // the function of the node (BDD or AIG)
00070     unsigned          Level    : 14;   // the level of this node in the global AIG
00071     // printing info 
00072     unsigned          fNodeOr  :  1;   // marks the original OR node
00073     unsigned          fCompl0  :  1;   // marks the original complemented edge
00074     unsigned          fCompl1  :  1;   // marks the original complemented edge
00075     // latch info
00076     unsigned          nLat0    :  5;   // the number of latches on the first edge
00077     unsigned          nLat1    :  5;   // the number of latches on the second edge
00078     unsigned          nLat2    :  5;   // the number of latches on the output edge
00079 };
00080 
00081 typedef struct Kit_Graph_t_ Kit_Graph_t;
00082 struct Kit_Graph_t_
00083 {
00084     int               fConst;          // marks the constant 1 graph
00085     int               nLeaves;         // the number of leaves
00086     int               nSize;           // the number of nodes (including the leaves) 
00087     int               nCap;            // the number of allocated nodes
00088     Kit_Node_t *      pNodes;          // the array of leaves and internal nodes
00089     Kit_Edge_t        eRoot;           // the pointer to the topmost node
00090 };
00091 
00092 
00093 // DSD node types
00094 typedef enum { 
00095     KIT_DSD_NONE  = 0,  // 0: unknown
00096     KIT_DSD_CONST1,     // 1: constant 1
00097     KIT_DSD_VAR,        // 2: elementary variable
00098     KIT_DSD_AND,        // 3: multi-input AND
00099     KIT_DSD_XOR,        // 4: multi-input XOR
00100     KIT_DSD_PRIME       // 5: arbitrary function of 3+ variables
00101 } Kit_Dsd_t;
00102 
00103 // DSD node
00104 typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
00105 struct Kit_DsdObj_t_
00106 { 
00107     unsigned       Id         : 6;  // the number of this node
00108     unsigned       Type       : 3;  // none, const, var, AND, XOR, MUX, PRIME
00109     unsigned       fMark      : 1;  // finished checking output
00110     unsigned       Offset     : 8;  // offset to the truth table
00111     unsigned       nRefs      : 8;  // offset to the truth table
00112     unsigned       nFans      : 6;  // the number of fanins of this node
00113     unsigned char  pFans[0];        // the fanin literals
00114 };
00115 
00116 // DSD network
00117 typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
00118 struct Kit_DsdNtk_t_
00119 {
00120     unsigned char  nVars;           // at most 16 (perhaps 18?)
00121     unsigned char  nNodesAlloc;     // the number of allocated nodes (at most nVars)
00122     unsigned char  nNodes;          // the number of nodes
00123     unsigned char  Root;            // the root of the tree
00124     unsigned *     pMem;            // memory for the truth tables (memory manager?)
00125     unsigned *     pSupps;          // supports of the nodes
00126     Kit_DsdObj_t** pNodes;          // the nodes
00127 };
00128 
00129 // DSD manager
00130 typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
00131 struct Kit_DsdMan_t_
00132 {
00133     int            nVars;           // the maximum number of variables
00134     int            nWords;          // the number of words in TTs
00135     Vec_Ptr_t *    vTtElems;        // elementary truth tables
00136     Vec_Ptr_t *    vTtNodes;        // the node truth tables
00137     // BDD representation
00138     CloudManager * dd;              // BDD package
00139     Vec_Ptr_t *    vTtBdds;         // the node truth tables
00140     Vec_Int_t *    vNodes;          // temporary array for BDD nodes
00141 };
00142 
00143 static inline int             Kit_DsdVar2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
00144 static inline int             Kit_DsdLit2Var( int Lit )              { return Lit >> 1;           }
00145 static inline int             Kit_DsdLitIsCompl( int Lit )           { return Lit & 1;            }
00146 static inline int             Kit_DsdLitNot( int Lit )               { return Lit ^ 1;            }
00147 static inline int             Kit_DsdLitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
00148 static inline int             Kit_DsdLitRegular( int Lit )           { return Lit & 0xfe;         }
00149  
00150 static inline unsigned        Kit_DsdObjOffset( int nFans )          { return (nFans >> 2) + ((nFans & 3) > 0);                    }
00151 static inline unsigned *      Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
00152 static inline int             Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
00153 static inline Kit_DsdObj_t *  Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id )      { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
00154 static inline Kit_DsdObj_t *  Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk )             { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) );                      }
00155 static inline int             Kit_DsdLitIsLeaf( Kit_DsdNtk_t * pNtk, int Lit )   { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars; }
00156 static inline unsigned        Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )  { int Id = Kit_DsdLit2Var(Lit); assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return pNtk->pSupps? (Id < pNtk->nVars? (1 << Id) : pNtk->pSupps[Id - pNtk->nVars]) : 0; }
00157 
00158 #define Kit_DsdNtkForEachObj( pNtk, pObj, i )                                      \
00159     for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
00160 #define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )                              \
00161     for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
00162 
00166 
00167 #define KIT_MIN(a,b)       (((a) < (b))? (a) : (b))
00168 #define KIT_MAX(a,b)       (((a) > (b))? (a) : (b))
00169 #define KIT_INFINITY       (100000000)
00170 
00171 #ifndef ALLOC
00172 #define ALLOC(type, num)         ((type *) malloc(sizeof(type) * (num)))
00173 #endif
00174 
00175 #ifndef FREE
00176 #define FREE(obj)                    ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
00177 #endif
00178 
00179 #ifndef REALLOC
00180 #define REALLOC(type, obj, num) \
00181         ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
00182              ((type *) malloc(sizeof(type) * (num))))
00183 #endif
00184 
00185 static inline int          Kit_CubeHasLit( unsigned uCube, int i )                        { return(uCube &  (unsigned)(1<<i)) > 0;  }
00186 static inline unsigned     Kit_CubeSetLit( unsigned uCube, int i )                        { return uCube |  (unsigned)(1<<i);       }
00187 static inline unsigned     Kit_CubeXorLit( unsigned uCube, int i )                        { return uCube ^  (unsigned)(1<<i);       }
00188 static inline unsigned     Kit_CubeRemLit( unsigned uCube, int i )                        { return uCube & ~(unsigned)(1<<i);       }
00189 
00190 static inline int          Kit_CubeContains( unsigned uLarge, unsigned uSmall )           { return (uLarge & uSmall) == uSmall;     }
00191 static inline unsigned     Kit_CubeSharp( unsigned uCube, unsigned uMask )                { return uCube & ~uMask;                  }
00192 static inline unsigned     Kit_CubeMask( int nVar )                                       { return (~(unsigned)0) >> (32-nVar);     }
00193 
00194 static inline int          Kit_CubeIsMarked( unsigned uCube )                             { return Kit_CubeHasLit( uCube, 31 );     }
00195 static inline unsigned     Kit_CubeMark( unsigned uCube )                                 { return Kit_CubeSetLit( uCube, 31 );     }
00196 static inline unsigned     Kit_CubeUnmark( unsigned uCube )                               { return Kit_CubeRemLit( uCube, 31 );     }
00197 
00198 static inline int          Kit_SopCubeNum( Kit_Sop_t * cSop )                             { return cSop->nCubes;                    }
00199 static inline unsigned     Kit_SopCube( Kit_Sop_t * cSop, int i )                         { return cSop->pCubes[i];                 }
00200 static inline void         Kit_SopShrink( Kit_Sop_t * cSop, int nCubesNew )               { cSop->nCubes = nCubesNew;               }
00201 static inline void         Kit_SopPushCube( Kit_Sop_t * cSop, unsigned uCube )            { cSop->pCubes[cSop->nCubes++] = uCube;   }
00202 static inline void         Kit_SopWriteCube( Kit_Sop_t * cSop, unsigned uCube, int i )    { cSop->pCubes[i] = uCube;                }
00203 
00204 static inline Kit_Edge_t   Kit_EdgeCreate( int Node, int fCompl )                         { Kit_Edge_t eEdge = { fCompl, Node }; return eEdge;  }
00205 static inline unsigned     Kit_EdgeToInt( Kit_Edge_t eEdge )                              { return (eEdge.Node << 1) | eEdge.fCompl;            }
00206 static inline Kit_Edge_t   Kit_IntToEdge( unsigned Edge )                                 { return Kit_EdgeCreate( Edge >> 1, Edge & 1 );       }
00207 static inline unsigned     Kit_EdgeToInt_( Kit_Edge_t eEdge )                             { return *(unsigned *)&eEdge;                         }
00208 static inline Kit_Edge_t   Kit_IntToEdge_( unsigned Edge )                                { return *(Kit_Edge_t *)&Edge;                        }
00209 
00210 static inline int          Kit_GraphIsConst( Kit_Graph_t * pGraph )                       { return pGraph->fConst;                              }
00211 static inline int          Kit_GraphIsConst0( Kit_Graph_t * pGraph )                      { return pGraph->fConst && pGraph->eRoot.fCompl;      }
00212 static inline int          Kit_GraphIsConst1( Kit_Graph_t * pGraph )                      { return pGraph->fConst && !pGraph->eRoot.fCompl;     }
00213 static inline int          Kit_GraphIsComplement( Kit_Graph_t * pGraph )                  { return pGraph->eRoot.fCompl;                        }
00214 static inline int          Kit_GraphIsVar( Kit_Graph_t * pGraph )                         { return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves; }
00215 static inline void         Kit_GraphComplement( Kit_Graph_t * pGraph )                    { pGraph->eRoot.fCompl ^= 1;                          }
00216 static inline void         Kit_GraphSetRoot( Kit_Graph_t * pGraph, Kit_Edge_t eRoot )     { pGraph->eRoot = eRoot;                              }
00217 static inline int          Kit_GraphLeaveNum( Kit_Graph_t * pGraph )                      { return pGraph->nLeaves;                             }
00218 static inline int          Kit_GraphNodeNum( Kit_Graph_t * pGraph )                       { return pGraph->nSize - pGraph->nLeaves;             }
00219 static inline Kit_Node_t * Kit_GraphNode( Kit_Graph_t * pGraph, int i )                   { return pGraph->pNodes + i;                          }
00220 static inline Kit_Node_t * Kit_GraphNodeLast( Kit_Graph_t * pGraph )                      { return pGraph->pNodes + pGraph->nSize - 1;          }
00221 static inline int          Kit_GraphNodeInt( Kit_Graph_t * pGraph, Kit_Node_t * pNode )   { return pNode - pGraph->pNodes;                      }
00222 static inline int          Kit_GraphNodeIsVar( Kit_Graph_t * pGraph, Kit_Node_t * pNode ) { return Kit_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves; }
00223 static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )                           { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNode( pGraph, pGraph->eRoot.Node );      }
00224 static inline int          Kit_GraphVarInt( Kit_Graph_t * pGraph )                        { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
00225 static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node);     }
00226 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);     }
00227 static inline int          Kit_GraphRootLevel( Kit_Graph_t * pGraph )                     { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level;                                        }
00228 
00229 static inline int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
00230 static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }
00231 static inline int          Kit_BitWordNum( int nBits )    { return nBits/(8*sizeof(unsigned)) + ((nBits%(8*sizeof(unsigned))) > 0); }
00232 static inline int          Kit_TruthWordNum( int nVars )  { return nVars <= 5 ? 1 : (1 << (nVars - 5));                             }
00233 static inline unsigned     Kit_BitMask( int nBits )       { assert( nBits <= 32 ); return ~((~(unsigned)0) << nBits);               }
00234 
00235 static inline void         Kit_TruthSetBit( unsigned * p, int Bit )   { p[Bit>>5] |= (1<<(Bit & 31));               }
00236 static inline void         Kit_TruthXorBit( unsigned * p, int Bit )   { p[Bit>>5] ^= (1<<(Bit & 31));               }
00237 static inline int          Kit_TruthHasBit( unsigned * p, int Bit )   { return (p[Bit>>5] & (1<<(Bit & 31))) > 0;   }
00238 
00239 static inline int Kit_WordFindFirstBit( unsigned uWord )
00240 {
00241     int i;
00242     for ( i = 0; i < 32; i++ )
00243         if ( uWord & (1 << i) )
00244             return i;
00245     return -1;
00246 }
00247 static inline int Kit_WordHasOneBit( unsigned uWord )
00248 {
00249     return (uWord & (uWord - 1)) == 0;
00250 }
00251 static inline int Kit_WordCountOnes( unsigned uWord )
00252 {
00253     uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
00254     uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
00255     uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
00256     uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
00257     return  (uWord & 0x0000FFFF) + (uWord>>16);
00258 }
00259 static inline int Kit_TruthCountOnes( unsigned * pIn, int nVars )
00260 {
00261     int w, Counter = 0;
00262     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00263         Counter += Kit_WordCountOnes(pIn[w]);
00264     return Counter;
00265 }
00266 static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
00267 {
00268     int w;
00269     for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
00270         if ( pIn[w] )
00271             return 32*w + Kit_WordFindFirstBit(pIn[w]);
00272     return -1;
00273 }
00274 static inline int Kit_TruthFindFirstZero( unsigned * pIn, int nVars )
00275 {
00276     int w;
00277     for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
00278         if ( ~pIn[w] )
00279             return 32*w + Kit_WordFindFirstBit(~pIn[w]);
00280     return -1;
00281 }
00282 static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
00283 {
00284     int w;
00285     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00286         if ( pIn0[w] != pIn1[w] )
00287             return 0;
00288     return 1;
00289 }
00290 static inline int Kit_TruthIsOpposite( unsigned * pIn0, unsigned * pIn1, int nVars )
00291 {
00292     int w;
00293     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00294         if ( pIn0[w] != ~pIn1[w] )
00295             return 0;
00296     return 1;
00297 }
00298 static inline int Kit_TruthIsEqualWithPhase( unsigned * pIn0, unsigned * pIn1, int nVars )
00299 {
00300     int w;
00301     if ( (pIn0[0] & 1) == (pIn1[0] & 1) )
00302     {
00303         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00304             if ( pIn0[w] != pIn1[w] )
00305                 return 0;
00306     }
00307     else
00308     {
00309         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00310             if ( pIn0[w] != ~pIn1[w] )
00311                 return 0;
00312     }
00313     return 1;
00314 }
00315 static inline int Kit_TruthIsConst0( unsigned * pIn, int nVars )
00316 {
00317     int w;
00318     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00319         if ( pIn[w] )
00320             return 0;
00321     return 1;
00322 }
00323 static inline int Kit_TruthIsConst1( unsigned * pIn, int nVars )
00324 {
00325     int w;
00326     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00327         if ( pIn[w] != ~(unsigned)0 )
00328             return 0;
00329     return 1;
00330 }
00331 static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
00332 {
00333     int w;
00334     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00335         if ( pIn1[w] & ~pIn2[w] )
00336             return 0;
00337     return 1;
00338 }
00339 static inline int Kit_TruthIsDisjoint( unsigned * pIn1, unsigned * pIn2, int nVars )
00340 {
00341     int w;
00342     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00343         if ( pIn1[w] & pIn2[w] )
00344             return 0;
00345     return 1;
00346 }
00347 static inline int Kit_TruthIsDisjoint3( unsigned * pIn1, unsigned * pIn2, unsigned * pIn3, int nVars )
00348 {
00349     int w;
00350     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00351         if ( pIn1[w] & pIn2[w] & pIn3[w] )
00352             return 0;
00353     return 1;
00354 }
00355 static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
00356 {
00357     int w;
00358     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00359         pOut[w] = pIn[w];
00360 }
00361 static inline void Kit_TruthClear( unsigned * pOut, int nVars )
00362 {
00363     int w;
00364     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00365         pOut[w] = 0;
00366 }
00367 static inline void Kit_TruthFill( unsigned * pOut, int nVars )
00368 {
00369     int w;
00370     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00371         pOut[w] = ~(unsigned)0;
00372 }
00373 static inline void Kit_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
00374 {
00375     int w;
00376     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00377         pOut[w] = ~pIn[w];
00378 }
00379 static inline void Kit_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00380 {
00381     int w;
00382     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00383         pOut[w] = pIn0[w] & pIn1[w];
00384 }
00385 static inline void Kit_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00386 {
00387     int w;
00388     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00389         pOut[w] = pIn0[w] | pIn1[w];
00390 }
00391 static inline void Kit_TruthXor( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00392 {
00393     int w;
00394     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00395         pOut[w] = pIn0[w] ^ pIn1[w];
00396 }
00397 static inline void Kit_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00398 {
00399     int w;
00400     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00401         pOut[w] = pIn0[w] & ~pIn1[w];
00402 }
00403 static inline void Kit_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
00404 {
00405     int w;
00406     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00407         pOut[w] = ~(pIn0[w] & pIn1[w]);
00408 }
00409 static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars, int fCompl0, int fCompl1 )
00410 {
00411     int w;
00412     if ( fCompl0 && fCompl1 )
00413     {
00414         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00415             pOut[w] = ~(pIn0[w] | pIn1[w]);
00416     }
00417     else if ( fCompl0 && !fCompl1 )
00418     {
00419         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00420             pOut[w] = ~pIn0[w] & pIn1[w];
00421     }
00422     else if ( !fCompl0 && fCompl1 )
00423     {
00424         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00425             pOut[w] = pIn0[w] & ~pIn1[w];
00426     }
00427     else // if ( !fCompl0 && !fCompl1 )
00428     {
00429         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00430             pOut[w] = pIn0[w] & pIn1[w];
00431     }
00432 }
00433 static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars )
00434 {
00435     int w;
00436     for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00437         pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
00438 }
00439 static inline void Kit_TruthMuxPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars, int fComp0 )
00440 {
00441     int w;
00442     if ( fComp0 )
00443         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00444             pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
00445     else
00446         for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
00447             pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]);
00448 }
00449 static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar )
00450 {
00451     unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
00452     int k, nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
00453     if ( iVar < 5 )
00454     {
00455         for ( k = 0; k < nWords; k++ )
00456             pTruth[k] = Masks[iVar];
00457     }
00458     else
00459     {
00460         for ( k = 0; k < nWords; k++ )
00461             if ( k & (1 << (iVar-5)) )
00462                 pTruth[k] = ~(unsigned)0;
00463             else
00464                 pTruth[k] = 0;
00465     }
00466 }
00467 
00468 
00472 
00473 #define Kit_SopForEachCube( cSop, uCube, i )                                      \
00474     for ( i = 0; (i < Kit_SopCubeNum(cSop)) && ((uCube) = Kit_SopCube(cSop, i)); i++ )
00475 #define Kit_CubeForEachLiteral( uCube, Lit, nLits, i )                            \
00476     for ( i = 0; (i < (nLits)) && ((Lit) = Kit_CubeHasLit(uCube, i)); i++ )
00477 
00478 #define Kit_GraphForEachLeaf( pGraph, pLeaf, i )                                              \
00479     for ( i = 0; (i < (pGraph)->nLeaves) && (((pLeaf) = Kit_GraphNode(pGraph, i)), 1); i++ )
00480 #define Kit_GraphForEachNode( pGraph, pAnd, i )                                               \
00481     for ( i = (pGraph)->nLeaves; (i < (pGraph)->nSize) && (((pAnd) = Kit_GraphNode(pGraph, i)), 1); i++ )
00482 
00486 
00487 /*=== kitBdd.c ==========================================================*/
00488 extern DdNode *        Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
00489 extern DdNode *        Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
00490 extern DdNode *        Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
00491 /*=== kitCloud.c ==========================================================*/
00492 extern CloudNode *     Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars );
00493 extern unsigned *      Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv );
00494 extern int             Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes );
00495 extern int             Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes );
00496 extern unsigned *      Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes );
00497 extern void            Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps );
00498 /*=== kitDsd.c ==========================================================*/
00499 extern Kit_DsdMan_t *  Kit_DsdManAlloc( int nVars, int nNodes );
00500 extern void            Kit_DsdManFree( Kit_DsdMan_t * p );
00501 extern Kit_DsdNtk_t *  Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
00502 extern unsigned *      Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
00503 extern void            Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
00504 extern void            Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
00505 extern void            Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec );
00506 extern void            Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
00507 extern void            Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
00508 extern void            Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
00509 extern Kit_DsdNtk_t *  Kit_DsdDecompose( unsigned * pTruth, int nVars );
00510 extern Kit_DsdNtk_t *  Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars );
00511 extern Kit_DsdNtk_t *  Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
00512 extern void            Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
00513 extern void            Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
00514 extern int             Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
00515 extern unsigned        Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
00516 extern unsigned        Kit_DsdGetSupports( Kit_DsdNtk_t * p );
00517 extern Kit_DsdNtk_t *  Kit_DsdExpand( Kit_DsdNtk_t * p );
00518 extern Kit_DsdNtk_t *  Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
00519 extern void            Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] );
00520 extern int             Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit, int fVerbose );
00521 /*=== kitFactor.c ==========================================================*/
00522 extern Kit_Graph_t *   Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
00523 /*=== kitGraph.c ==========================================================*/
00524 extern Kit_Graph_t *   Kit_GraphCreate( int nLeaves );   
00525 extern Kit_Graph_t *   Kit_GraphCreateConst0();   
00526 extern Kit_Graph_t *   Kit_GraphCreateConst1();   
00527 extern Kit_Graph_t *   Kit_GraphCreateLeaf( int iLeaf, int nLeaves, int fCompl );   
00528 extern void            Kit_GraphFree( Kit_Graph_t * pGraph );   
00529 extern Kit_Node_t *    Kit_GraphAppendNode( Kit_Graph_t * pGraph );   
00530 extern Kit_Edge_t      Kit_GraphAddNodeAnd( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
00531 extern Kit_Edge_t      Kit_GraphAddNodeOr( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1 );
00532 extern Kit_Edge_t      Kit_GraphAddNodeXor( Kit_Graph_t * pGraph, Kit_Edge_t eEdge0, Kit_Edge_t eEdge1, int Type );
00533 extern Kit_Edge_t      Kit_GraphAddNodeMux( Kit_Graph_t * pGraph, Kit_Edge_t eEdgeC, Kit_Edge_t eEdgeT, Kit_Edge_t eEdgeE, int Type );
00534 extern unsigned        Kit_GraphToTruth( Kit_Graph_t * pGraph );
00535 extern Kit_Graph_t *   Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
00536 extern int             Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf );
00537 /*=== kitHop.c ==========================================================*/
00538 //extern Hop_Obj_t *     Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
00539 //extern Hop_Obj_t *     Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
00540 //extern Hop_Obj_t *     Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
00541 /*=== kitIsop.c ==========================================================*/
00542 extern int             Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
00543 /*=== kitSop.c ==========================================================*/
00544 extern void            Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
00545 extern void            Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
00546 extern void            Kit_SopDup( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
00547 extern void            Kit_SopDivideByLiteralQuo( Kit_Sop_t * cSop, int iLit );
00548 extern void            Kit_SopDivideByCube( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
00549 extern void            Kit_SopDivideInternal( Kit_Sop_t * cSop, Kit_Sop_t * cDiv, Kit_Sop_t * vQuo, Kit_Sop_t * vRem, Vec_Int_t * vMemory );
00550 extern void            Kit_SopMakeCubeFree( Kit_Sop_t * cSop );
00551 extern int             Kit_SopIsCubeFree( Kit_Sop_t * cSop );
00552 extern void            Kit_SopCommonCubeCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, Vec_Int_t * vMemory );
00553 extern int             Kit_SopAnyLiteral( Kit_Sop_t * cSop, int nLits );
00554 extern int             Kit_SopDivisor( Kit_Sop_t * cResult, Kit_Sop_t * cSop, int nLits, Vec_Int_t * vMemory );
00555 extern void            Kit_SopBestLiteralCover( Kit_Sop_t * cResult, Kit_Sop_t * cSop, unsigned uCube, int nLits, Vec_Int_t * vMemory );
00556 /*=== kitTruth.c ==========================================================*/
00557 extern void            Kit_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int Start );
00558 extern void            Kit_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
00559 extern void            Kit_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn );
00560 extern int             Kit_TruthVarInSupport( unsigned * pTruth, int nVars, int iVar );
00561 extern int             Kit_TruthSupportSize( unsigned * pTruth, int nVars );
00562 extern unsigned        Kit_TruthSupport( unsigned * pTruth, int nVars );
00563 extern void            Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
00564 extern void            Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
00565 extern void            Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
00566 extern void            Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
00567 extern void            Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
00568 extern void            Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
00569 extern void            Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
00570 extern void            Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
00571 extern void            Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
00572 extern void            Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
00573 extern void            Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
00574 extern void            Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
00575 extern void            Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 );
00576 extern void            Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
00577 extern int             Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
00578 extern int             Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
00579 extern void            Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
00580 extern void            Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
00581 extern unsigned        Kit_TruthHash( unsigned * pIn, int nWords );
00582 extern unsigned        Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
00583 extern char *          Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
00584 
00585 #ifdef __cplusplus
00586 }
00587 #endif
00588 
00589 #endif
00590 
00594