ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaJf.c File Reference
#include "gia.h"
#include "misc/vec/vecSet.h"
#include "misc/vec/vecMem.h"
#include "misc/extra/extra.h"
#include "bool/kit/kit.h"
#include "misc/util/utilTruth.h"
#include "opt/dau/dau.h"
#include "sat/cnf/cnf.h"
Include dependency graph for giaJf.c:

Go to the source code of this file.

Classes

struct  Jf_Cut_t_
 
struct  Jf_Man_t_
 

Macros

#define JF_LEAF_MAX   8
 DECLARATIONS ///.
 
#define JF_WORD_MAX   ((JF_LEAF_MAX > 6) ? 1 << (JF_LEAF_MAX-6) : 1)
 
#define JF_CUT_MAX   16
 
#define JF_EPSILON   0.005
 
#define Jf_ObjForEachCut(pList, pCut, i)
 
#define Jf_CutForEachLit(pCut, Lit, i)
 
#define Jf_CutForEachVar(pCut, Var, i)
 

Typedefs

typedef struct Jf_Cut_t_ Jf_Cut_t
 
typedef struct Jf_Man_t_ Jf_Man_t
 

Functions

int Kit_TruthToGia (Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
 DECLARATIONS ///.
 
void Jf_ManGenCnf (word uTruth, int iLitOut, Vec_Int_t *vLeaves, Vec_Int_t *vLits, Vec_Int_t *vClas, Vec_Int_t *vCover)
 FUNCTION DEFINITIONS ///.
 
Cnf_Dat_tJf_ManCreateCnfRemap (Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas, int fAddOrCla)
 
Cnf_Dat_tJf_ManCreateCnf (Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas)
 
float * Jf_ManInitRefs (Jf_Man_t *pMan)
 
void Jf_ManProfileClasses (Jf_Man_t *p)
 
Jf_Man_tJf_ManAlloc (Gia_Man_t *pGia, Jf_Par_t *pPars)
 
void Jf_ManFree (Jf_Man_t *p)
 
int Jf_ObjCutFilterBoth (Jf_Man_t *p, Jf_Cut_t **pSto, int c)
 
int Jf_ObjCutFilter (Jf_Man_t *p, Jf_Cut_t **pSto, int c)
 
int Jf_CutRef_rec (Jf_Man_t *p, int *pCut)
 
int Jf_CutDeref_rec (Jf_Man_t *p, int *pCut)
 
int Jf_CutAreaRef_rec (Jf_Man_t *p, int *pCut)
 
int Jf_CutAreaRefEdge_rec (Jf_Man_t *p, int *pCut)
 
int Jf_CutCheckMffc_rec (Jf_Man_t *p, int *pCut, int Limit)
 
float Jf_CutCompareDelay (Jf_Cut_t *pOld, Jf_Cut_t *pNew)
 
float Jf_CutCompareArea (Jf_Cut_t *pOld, Jf_Cut_t *pNew)
 
int Jf_TtComputeForCut (Jf_Man_t *p, int iFuncLit0, int iFuncLit1, int *pCut0, int *pCut1, int *pCutOut)
 
void Jf_ObjComputeCuts (Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge)
 
void Jf_ManComputeCuts (Jf_Man_t *p, int fEdge)
 
int Jf_ManComputeDelay (Jf_Man_t *p, int fEval)
 
int Jf_ManComputeRefs (Jf_Man_t *p)
 
void Jf_ObjComputeBestCut (Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge, int fEla)
 
void Jf_ManPropagateFlow (Jf_Man_t *p, int fEdge)
 
void Jf_ManPropagateEla (Jf_Man_t *p, int fEdge)
 
Gia_Man_tJf_ManDeriveMappingGia (Jf_Man_t *p)
 
void Jf_ManDeriveMapping (Jf_Man_t *p)
 
Gia_Man_tJf_ManDeriveGia (Jf_Man_t *p)
 
void Jf_ManSetDefaultPars (Jf_Par_t *pPars)
 
void Jf_ManPrintStats (Jf_Man_t *p, char *pTitle)
 
Gia_Man_tJf_ManPerformMapping (Gia_Man_t *pGia, Jf_Par_t *pPars)
 
Gia_Man_tJf_ManDeriveCnf (Gia_Man_t *p, int fCnfObjIds)
 
Gia_Man_tJf_ManDeriveCnfMiter (Gia_Man_t *p, int fVerbose)
 
void Jf_ManDumpCnf (Gia_Man_t *p, char *pFileName, int fVerbose)
 
void Jf_ManTestCnf (Gia_Man_t *p)
 

Macro Definition Documentation

◆ JF_CUT_MAX

#define JF_CUT_MAX   16

Definition at line 38 of file giaJf.c.

◆ Jf_CutForEachLit

#define Jf_CutForEachLit ( pCut,
Lit,
i )
Value:
for ( i = 1; i <= Jf_CutSize(pCut) && (Lit = Jf_CutLit(pCut, i)); i++ )

Definition at line 109 of file giaJf.c.

◆ Jf_CutForEachVar

#define Jf_CutForEachVar ( pCut,
Var,
i )
Value:
for ( i = 1; i <= Jf_CutSize(pCut) && (Var = Jf_CutVar(pCut, i)); i++ )
int Var
Definition exorList.c:228

Definition at line 110 of file giaJf.c.

◆ JF_EPSILON

#define JF_EPSILON   0.005

Definition at line 39 of file giaJf.c.

◆ JF_LEAF_MAX

#define JF_LEAF_MAX   8

DECLARATIONS ///.

CFile****************************************************************

FileName [giaJf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
giaJf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 36 of file giaJf.c.

◆ Jf_ObjForEachCut

#define Jf_ObjForEachCut ( pList,
pCut,
i )
Value:
for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Jf_CutSize(pCut) + 1 )

Definition at line 108 of file giaJf.c.

◆ JF_WORD_MAX

#define JF_WORD_MAX   ((JF_LEAF_MAX > 6) ? 1 << (JF_LEAF_MAX-6) : 1)

Definition at line 37 of file giaJf.c.

Typedef Documentation

◆ Jf_Cut_t

typedef struct Jf_Cut_t_ Jf_Cut_t

Definition at line 41 of file giaJf.c.

◆ Jf_Man_t

typedef struct Jf_Man_t_ Jf_Man_t

Definition at line 52 of file giaJf.c.

Function Documentation

◆ Jf_CutAreaRef_rec()

int Jf_CutAreaRef_rec ( Jf_Man_t * p,
int * pCut )

Definition at line 870 of file giaJf.c.

871{
872 int i, Var, Count = Jf_CutCost(pCut);
873 Jf_CutForEachVar( pCut, Var, i )
874 {
875 if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
876 Count += Jf_CutAreaRef_rec( p, Jf_ObjCutBest(p, Var) );
877 Vec_IntPush( p->vTemp, Var );
878 }
879 return Count;
880}
Cube * p
Definition exorList.c:222
int Jf_CutAreaRef_rec(Jf_Man_t *p, int *pCut)
Definition giaJf.c:870
#define Jf_CutForEachVar(pCut, Var, i)
Definition giaJf.c:110
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_CutAreaRefEdge_rec()

int Jf_CutAreaRefEdge_rec ( Jf_Man_t * p,
int * pCut )

Definition at line 881 of file giaJf.c.

882{
883 int i, Var, Count = (Jf_CutCost(pCut) << 4) | Jf_CutSize(pCut);
884 Jf_CutForEachVar( pCut, Var, i )
885 {
886 if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
887 Count += Jf_CutAreaRefEdge_rec( p, Jf_ObjCutBest(p, Var) );
888 Vec_IntPush( p->vTemp, Var );
889 }
890 return Count;
891}
int Jf_CutAreaRefEdge_rec(Jf_Man_t *p, int *pCut)
Definition giaJf.c:881
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_CutCheckMffc_rec()

int Jf_CutCheckMffc_rec ( Jf_Man_t * p,
int * pCut,
int Limit )

Definition at line 905 of file giaJf.c.

906{
907 int i, Var;
908 Jf_CutForEachVar( pCut, Var, i )
909 {
910 int fRecur = (!Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var));
911 Vec_IntPush( p->vTemp, Var );
912 if ( Vec_IntSize(p->vTemp) >= Limit )
913 return 0;
914 if ( fRecur && !Jf_CutCheckMffc_rec( p, Jf_ObjCutBest(p, Var), Limit ) )
915 return 0;
916 }
917 return 1;
918}
int Jf_CutCheckMffc_rec(Jf_Man_t *p, int *pCut, int Limit)
Definition giaJf.c:905
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_CutCompareArea()

float Jf_CutCompareArea ( Jf_Cut_t * pOld,
Jf_Cut_t * pNew )

Definition at line 949 of file giaJf.c.

950{
951// if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow;
952 if ( pOld->Flow < pNew->Flow - JF_EPSILON ) return -1;
953 if ( pOld->Flow > pNew->Flow + JF_EPSILON ) return 1;
954 if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0];
955 if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time;
956 return 0;
957}
#define JF_EPSILON
Definition giaJf.c:39
int Time
Definition giaJf.c:46
float Flow
Definition giaJf.c:45
int pCut[JF_LEAF_MAX+2]
Definition giaJf.c:49
Here is the caller graph for this function:

◆ Jf_CutCompareDelay()

float Jf_CutCompareDelay ( Jf_Cut_t * pOld,
Jf_Cut_t * pNew )

Function*************************************************************

Synopsis [Comparison procedures.]

Description [Return positive value if the new cut is better than the old cut.]

SideEffects []

SeeAlso []

Definition at line 940 of file giaJf.c.

941{
942 if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time;
943 if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0];
944// if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow;
945 if ( pOld->Flow < pNew->Flow - JF_EPSILON ) return -1;
946 if ( pOld->Flow > pNew->Flow + JF_EPSILON ) return 1;
947 return 0;
948}
Here is the caller graph for this function:

◆ Jf_CutDeref_rec()

int Jf_CutDeref_rec ( Jf_Man_t * p,
int * pCut )

Definition at line 853 of file giaJf.c.

854{
855 int i, Var, Count = Jf_CutCost(pCut);
856 Jf_CutForEachVar( pCut, Var, i )
857 if ( !Gia_ObjRefDecId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
858 Count += Jf_CutDeref_rec( p, Jf_ObjCutBest(p, Var) );
859 return Count;
860}
int Jf_CutDeref_rec(Jf_Man_t *p, int *pCut)
Definition giaJf.c:853
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_CutRef_rec()

int Jf_CutRef_rec ( Jf_Man_t * p,
int * pCut )

Function*************************************************************

Synopsis [Reference counting.]

Description []

SideEffects []

SeeAlso []

Definition at line 845 of file giaJf.c.

846{
847 int i, Var, Count = Jf_CutCost(pCut);
848 Jf_CutForEachVar( pCut, Var, i )
849 if ( !Gia_ObjRefIncId(p->pGia, Var) && !Jf_CutIsTriv(Jf_ObjCutBest(p, Var), Var) )
850 Count += Jf_CutRef_rec( p, Jf_ObjCutBest(p, Var) );
851 return Count;
852}
int Jf_CutRef_rec(Jf_Man_t *p, int *pCut)
Definition giaJf.c:845
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManAlloc()

Jf_Man_t * Jf_ManAlloc ( Gia_Man_t * pGia,
Jf_Par_t * pPars )

Function*************************************************************

Synopsis [Manager manipulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file giaJf.c.

366{
367 Jf_Man_t * p;
368 assert( pPars->nLutSize <= JF_LEAF_MAX );
369 assert( pPars->nCutNum <= JF_CUT_MAX );
370 Vec_IntFreeP( &pGia->vMapping );
371 p = ABC_CALLOC( Jf_Man_t, 1 );
372 p->pGia = pGia;
373 p->pPars = pPars;
374 if ( pPars->fCutMin && !pPars->fFuncDsd )
375 p->vTtMem = Vec_MemAllocForTT( pPars->nLutSize, 0 );
376 else if ( pPars->fCutMin && pPars->fFuncDsd )
377 {
378 p->pDsd = Sdm_ManRead();
379 if ( pPars->fGenCnf )
380 {
381 p->vCnfs = Vec_IntStart( 595 );
382 Sdm_ManReadCnfCosts( p->pDsd, Vec_IntArray(p->vCnfs), Vec_IntSize(p->vCnfs) );
383 }
384 }
385 Vec_IntFill( &p->vCuts, Gia_ManObjNum(pGia), 0 );
386 Vec_IntFill( &p->vArr, Gia_ManObjNum(pGia), 0 );
387 Vec_IntFill( &p->vDep, Gia_ManObjNum(pGia), 0 );
388 Vec_FltFill( &p->vFlow, Gia_ManObjNum(pGia), 0 );
389 p->vRefs.nCap = p->vRefs.nSize = Gia_ManObjNum(pGia);
390 p->vRefs.pArray = Jf_ManInitRefs( p );
391 Vec_SetAlloc_( &p->pMem, 20 );
392 p->vTemp = Vec_IntAlloc( 1000 );
393 p->clkStart = Abc_Clock();
394 return p;
395}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
void Sdm_ManReadCnfCosts(Sdm_Man_t *p, int *pCosts, int nCosts)
Sdm_Man_t * Sdm_ManRead()
#define JF_CUT_MAX
Definition giaJf.c:38
float * Jf_ManInitRefs(Jf_Man_t *pMan)
Definition giaJf.c:245
struct Jf_Man_t_ Jf_Man_t
Definition giaJf.c:52
#define JF_LEAF_MAX
DECLARATIONS ///.
Definition giaJf.c:36
Vec_Int_t * vMapping
Definition gia.h:136
int fGenCnf
Definition gia.h:360
int fFuncDsd
Definition gia.h:359
int nCutNum
Definition gia.h:337
int nLutSize
Definition gia.h:336
int fCutMin
Definition gia.h:358
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManComputeCuts()

void Jf_ManComputeCuts ( Jf_Man_t * p,
int fEdge )

Definition at line 1240 of file giaJf.c.

1241{
1242 Gia_Obj_t * pObj; int i;
1243 if ( p->pPars->fVerbose )
1244 {
1245 printf( "Aig: CI = %d CO = %d AND = %d ", Gia_ManCiNum(p->pGia), Gia_ManCoNum(p->pGia), Gia_ManAndNum(p->pGia) );
1246 printf( "LutSize = %d CutMax = %d Rounds = %d\n", p->pPars->nLutSize, p->pPars->nCutNum, p->pPars->nRounds );
1247 printf( "Computing cuts...\r" );
1248 fflush( stdout );
1249 }
1250 Gia_ManForEachObj( p->pGia, pObj, i )
1251 {
1252 if ( Gia_ObjIsCi(pObj) || Gia_ObjIsBuf(pObj) )
1253 Jf_ObjAssignCut( p, pObj );
1254 if ( Gia_ObjIsBuf(pObj) )
1255 Jf_ObjPropagateBuf( p, pObj, 0 );
1256 else if ( Gia_ObjIsAnd(pObj) )
1257 Jf_ObjComputeCuts( p, pObj, fEdge );
1258 }
1259 if ( p->pPars->fVerbose )
1260 {
1261 printf( "CutPair = %lu ", (long)p->CutCount[0] );
1262 printf( "Merge = %lu ", (long)p->CutCount[1] );
1263 printf( "Eval = %lu ", (long)p->CutCount[2] );
1264 printf( "Cut = %lu ", (long)p->CutCount[3] );
1265 Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1266 printf( "Memory: " );
1267 printf( "Gia = %.2f MB ", Gia_ManMemory(p->pGia) / (1<<20) );
1268 printf( "Man = %.2f MB ", 6.0 * sizeof(int) * Gia_ManObjNum(p->pGia) / (1<<20) );
1269 printf( "Cuts = %.2f MB", Vec_ReportMemory(&p->pMem) / (1<<20) );
1270 if ( p->nCoarse )
1271 printf( " Coarse = %d (%.1f %%)", p->nCoarse, 100.0 * p->nCoarse / Gia_ManObjNum(p->pGia) );
1272 printf( "\n" );
1273 fflush( stdout );
1274 }
1275}
void Jf_ObjComputeCuts(Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge)
Definition giaJf.c:1127
double Gia_ManMemory(Gia_Man_t *p)
Definition giaMan.c:194
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManComputeDelay()

int Jf_ManComputeDelay ( Jf_Man_t * p,
int fEval )

Function*************************************************************

Synopsis [Computing delay/area.]

Description []

SideEffects []

SeeAlso []

Definition at line 1289 of file giaJf.c.

1290{
1291 Gia_Obj_t * pObj;
1292 int i, Delay = 0;
1293 if ( fEval )
1294 {
1295 Gia_ManForEachObj( p->pGia, pObj, i )
1296 if ( Gia_ObjIsBuf(pObj) )
1297 Jf_ObjPropagateBuf( p, pObj, 0 );
1298 else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1299 Vec_IntWriteEntry( &p->vArr, i, Jf_CutArr(p, Jf_ObjCutBest(p, i)) );
1300 }
1301 Gia_ManForEachCoDriver( p->pGia, pObj, i )
1302 {
1303 assert( Gia_ObjRefNum(p->pGia, pObj) > 0 );
1304 Delay = Abc_MaxInt( Delay, Jf_ObjArr(p, Gia_ObjId(p->pGia, pObj)) );
1305 }
1306 return Delay;
1307}
#define Gia_ManForEachCoDriver(p, pObj, i)
Definition gia.h:1244
Here is the caller graph for this function:

◆ Jf_ManComputeRefs()

int Jf_ManComputeRefs ( Jf_Man_t * p)

Definition at line 1308 of file giaJf.c.

1309{
1310 Gia_Obj_t * pObj;
1311 float nRefsNew; int i, * pCut;
1312 float * pRefs = Vec_FltArray(&p->vRefs);
1313 float * pFlow = Vec_FltArray(&p->vFlow);
1314 assert( p->pGia->pRefs != NULL );
1315 memset( p->pGia->pRefs, 0, sizeof(int) * Gia_ManObjNum(p->pGia) );
1316 p->pPars->Area = p->pPars->Edge = 0;
1317 Gia_ManForEachObjReverse( p->pGia, pObj, i )
1318 {
1319 if ( Gia_ObjIsCo(pObj) || Gia_ObjIsBuf(pObj) )
1320 Gia_ObjRefInc( p->pGia, Gia_ObjFanin0(pObj) );
1321 else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1322 {
1323 assert( Jf_ObjIsUnit(pObj) );
1324 pCut = Jf_ObjCutBest(p, i);
1325 Jf_CutRef( p, pCut );
1326 if ( p->pPars->fGenCnf )
1327 p->pPars->Clause += Jf_CutCnfSize(p, pCut);
1328 p->pPars->Edge += Jf_CutSize(pCut);
1329 p->pPars->Area++;
1330 }
1331 }
1332 // blend references and normalize flow
1333 for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
1334 {
1335 if ( p->pPars->fOptEdge )
1336 nRefsNew = Abc_MaxFloat( 1, 0.8 * pRefs[i] + 0.2 * p->pGia->pRefs[i] );
1337 else
1338 nRefsNew = Abc_MaxFloat( 1, 0.2 * pRefs[i] + 0.8 * p->pGia->pRefs[i] );
1339 pFlow[i] = pFlow[i] * pRefs[i] / nRefsNew;
1340 pRefs[i] = nRefsNew;
1341 assert( pFlow[i] >= 0 );
1342 }
1343 // compute delay
1344 p->pPars->Delay = Jf_ManComputeDelay( p, 1 );
1345 return p->pPars->Area;
1346}
int Jf_ManComputeDelay(Jf_Man_t *p, int fEval)
Definition giaJf.c:1289
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition gia.h:1206
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManCreateCnf()

Cnf_Dat_t * Jf_ManCreateCnf ( Gia_Man_t * p,
Vec_Int_t * vLits,
Vec_Int_t * vClas )

Definition at line 199 of file giaJf.c.

200{
201 Cnf_Dat_t * pCnf;
202 int i, Entry, iOut;
203 // generate CNF
204 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
205 pCnf->pMan = (Aig_Man_t *)p;
206 pCnf->nVars = Gia_ManObjNum(p);
207 pCnf->nLiterals = Vec_IntSize(vLits);
208 pCnf->nClauses = Vec_IntSize(vClas);
209 pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
210 pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
211 Vec_IntForEachEntry( vClas, Entry, i )
212 pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
213 pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
214 // create mapping of objects into their clauses
215 pCnf->pObj2Clause = ABC_FALLOC( int, Gia_ManObjNum(p) );
216 pCnf->pObj2Count = ABC_FALLOC( int, Gia_ManObjNum(p) );
217 for ( i = 0; i < pCnf->nClauses; i++ )
218 {
219 iOut = Abc_Lit2Var(pCnf->pClauses[i][0]);
220 if ( pCnf->pObj2Clause[iOut] == -1 )
221 {
222 pCnf->pObj2Clause[iOut] = i;
223 pCnf->pObj2Count[iOut] = 1;
224 }
225 else
226 {
227 assert( pCnf->pObj2Count[iOut] > 0 );
228 pCnf->pObj2Count[iOut]++;
229 }
230 }
231 return pCnf;
232}
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
int nVars
Definition cnf.h:59
int * pObj2Count
Definition cnf.h:65
int * pObj2Clause
Definition cnf.h:64
int nLiterals
Definition cnf.h:60
int ** pClauses
Definition cnf.h:62
int nClauses
Definition cnf.h:61
Aig_Man_t * pMan
Definition cnf.h:58
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Jf_ManCreateCnfRemap()

Cnf_Dat_t * Jf_ManCreateCnfRemap ( Gia_Man_t * p,
Vec_Int_t * vLits,
Vec_Int_t * vClas,
int fAddOrCla )

Definition at line 163 of file giaJf.c.

164{
165 Cnf_Dat_t * pCnf;
166 Gia_Obj_t * pObj;
167 int i, Entry, * pMap, nVars = 0;
168 if ( fAddOrCla )
169 {
170 Vec_IntPush( vClas, Vec_IntSize(vLits) );
171 Gia_ManForEachPo( p, pObj, i )
172 Vec_IntPush( vLits, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) );
173 }
174 // label nodes present in the mapping
175 Vec_IntForEachEntry( vLits, Entry, i )
176 Gia_ManObj(p, Abc_Lit2Var(Entry))->fMark0 = 1;
177 // create variable map
178 pMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
179 Gia_ManForEachObjReverse( p, pObj, i )
180 if ( pObj->fMark0 )
181 pObj->fMark0 = 0, pMap[i] = nVars++;
182 // relabel literals
183 Vec_IntForEachEntry( vLits, Entry, i )
184 Vec_IntWriteEntry( vLits, i, Abc_Lit2LitV(pMap, Entry) );
185 // generate CNF
186 pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
187 pCnf->pMan = (Aig_Man_t *)p;
188 pCnf->nVars = nVars;
189 pCnf->nLiterals = Vec_IntSize(vLits);
190 pCnf->nClauses = Vec_IntSize(vClas);
191 pCnf->pClauses = ABC_ALLOC( int *, pCnf->nClauses+1 );
192 pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
193 Vec_IntForEachEntry( vClas, Entry, i )
194 pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
195 pCnf->pClauses[i] = pCnf->pClauses[0] + pCnf->nLiterals;
196 pCnf->pVarNums = pMap;
197 return pCnf;
198}
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
int * pVarNums
Definition cnf.h:63
unsigned fMark0
Definition gia.h:81
Here is the caller graph for this function:

◆ Jf_ManDeriveCnf()

Gia_Man_t * Jf_ManDeriveCnf ( Gia_Man_t * p,
int fCnfObjIds )

Definition at line 1749 of file giaJf.c.

1750{
1751 Jf_Par_t Pars, * pPars = &Pars;
1752 Jf_ManSetDefaultPars( pPars );
1753 pPars->fGenCnf = 1;
1754 pPars->fCnfObjIds = fCnfObjIds;
1755 return Jf_ManPerformMapping( p, pPars );
1756}
void Jf_ManSetDefaultPars(Jf_Par_t *pPars)
Definition giaJf.c:1682
Gia_Man_t * Jf_ManPerformMapping(Gia_Man_t *pGia, Jf_Par_t *pPars)
Definition giaJf.c:1715
struct Jf_Par_t_ Jf_Par_t
Definition gia.h:333
int fCnfObjIds
Definition gia.h:362
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManDeriveCnfMiter()

Gia_Man_t * Jf_ManDeriveCnfMiter ( Gia_Man_t * p,
int fVerbose )

Definition at line 1757 of file giaJf.c.

1758{
1759 Jf_Par_t Pars, * pPars = &Pars;
1760 Jf_ManSetDefaultPars( pPars );
1761 pPars->fGenCnf = 1;
1762 pPars->fCnfObjIds = 0;
1763 pPars->fAddOrCla = 1;
1764 pPars->fVerbose = fVerbose;
1765 return Jf_ManPerformMapping( p, pPars );
1766}
int fVerbose
Definition gia.h:370
int fAddOrCla
Definition gia.h:363
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManDeriveGia()

Gia_Man_t * Jf_ManDeriveGia ( Jf_Man_t * p)

Function*************************************************************

Synopsis [Derive GIA without mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 1580 of file giaJf.c.

1581{
1582 Gia_Man_t * pNew, * pTemp;
1583 Gia_Obj_t * pObj;
1584 Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
1585 Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
1586 Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
1587 int i, k, iLit, Class, * pCut;
1588 int nWords = Abc_Truth6WordNum(p->pPars->nLutSize);
1589 word uTruth = 0, * pTruth = &uTruth, Truth[JF_WORD_MAX];
1590 // create new manager
1591 pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
1592 pNew->pName = Abc_UtilStrsav( p->pGia->pName );
1593 pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
1594 pNew->vLevels = Vec_IntStart( 6*Gia_ManObjNum(p->pGia)/5 + 100 );
1595 // map primary inputs
1596 Vec_IntWriteEntry( vCopies, 0, 0 );
1597 Gia_ManForEachCi( p->pGia, pObj, i )
1598 Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
1599 // iterate through nodes used in the mapping
1600 if ( !p->pPars->fCutMin )
1601 Gia_ObjComputeTruthTableStart( p->pGia, p->pPars->nLutSize );
1602 Gia_ManHashStart( pNew );
1603 Gia_ManForEachAnd( p->pGia, pObj, i )
1604 {
1605 if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1606 continue;
1607 pCut = Jf_ObjCutBest( p, i );
1608// printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut);
1609 // get the truth table
1610 if ( p->pPars->fCutMin )
1611 {
1612 Class = Jf_CutFuncClass( pCut );
1613 if ( Jf_CutSize(pCut) == 0 )
1614 {
1615 assert( Class == 0 );
1616 Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
1617 continue;
1618 }
1619 if ( Jf_CutSize(pCut) == 1 )
1620 {
1621 assert( Class == 1 );
1622 iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
1623 iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
1624 Vec_IntWriteEntry( vCopies, i, iLit );
1625 continue;
1626 }
1627 if ( p->pPars->fFuncDsd )
1628 uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class);
1629 else
1630 Abc_TtCopy( (pTruth = Truth), Vec_MemReadEntry(p->vTtMem, Class), nWords, 0 );
1631 assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
1632 }
1633 else
1634 {
1635 Vec_IntClear( vLeaves );
1636 Jf_CutForEachLit( pCut, iLit, k )
1637 Vec_IntPush( vLeaves, Abc_Lit2Var(iLit) );
1638 pTruth = Gia_ObjComputeTruthTableCut( p->pGia, pObj, vLeaves );
1639 }
1640 // collect incoming literals
1641 Vec_IntClear( vLeaves );
1642 Jf_CutForEachLit( pCut, iLit, k )
1643 Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
1644 // create GIA
1645 iLit = Dsm_ManTruthToGia( pNew, pTruth, vLeaves, vCover );
1646 iLit = Abc_LitNotCond( iLit, (p->pPars->fCutMin && Jf_CutFuncCompl(pCut)) );
1647 Vec_IntWriteEntry( vCopies, i, iLit );
1648 }
1649 Gia_ManForEachCo( p->pGia, pObj, i )
1650 {
1651 iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
1652 Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1653 }
1654 if ( !p->pPars->fCutMin )
1656 Vec_IntFree( vCopies );
1657 Vec_IntFree( vLeaves );
1658 Vec_IntFree( vCover );
1659 Gia_ManHashStop( pNew );
1660 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
1661// Dsm_ManReportStats();
1662 // perform cleanup
1663 if ( !p->pPars->fCutMin )
1664 {
1665 pNew = Gia_ManCleanup( pTemp = pNew );
1666 Gia_ManStop( pTemp );
1667 }
1668 return pNew;
1669}
int nWords
Definition abcNpn.c:127
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
int Dsm_ManTruthToGia(void *p, word *pTruth, Vec_Int_t *vLeaves, Vec_Int_t *vCover)
Definition dauGia.c:441
int Sdm_ManReadDsdVarNum(Sdm_Man_t *p, int iDsd)
word Sdm_ManReadDsdTruth(Sdm_Man_t *p, int iDsd)
#define Jf_CutForEachLit(pCut, Lit, i)
Definition giaJf.c:109
#define JF_WORD_MAX
Definition giaJf.c:37
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
word * Gia_ObjComputeTruthTableCut(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves)
Definition giaTruth.c:628
void Gia_ManHashStart(Gia_Man_t *p)
Definition giaHash.c:125
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
void Gia_ObjComputeTruthTableStart(Gia_Man_t *p, int nVarsMax)
Definition giaTruth.c:552
void Gia_ObjComputeTruthTableStop(Gia_Man_t *p)
Definition giaTruth.c:568
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Vec_Int_t * vLevels
Definition gia.h:120
char * pSpec
Definition gia.h:100
char * pName
Definition gia.h:99
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManDeriveMapping()

void Jf_ManDeriveMapping ( Jf_Man_t * p)

Definition at line 1544 of file giaJf.c.

1545{
1546 Vec_Int_t * vMapping;
1547 Gia_Obj_t * pObj;
1548 int i, k, * pCut;
1549 assert( !p->pPars->fCutMin );
1550 vMapping = Vec_IntAlloc( Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + (int)p->pPars->Area * 2 );
1551 Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
1552 Gia_ManForEachAnd( p->pGia, pObj, i )
1553 {
1554 if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1555 continue;
1556 pCut = Jf_ObjCutBest( p, i );
1557 Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
1558 assert( !p->pPars->fCutMin || Jf_CutSize(pCut) <= 6 );
1559 Vec_IntPush( vMapping, Jf_CutSize(pCut) );
1560 for ( k = 1; k <= Jf_CutSize(pCut); k++ )
1561 Vec_IntPush( vMapping, Jf_CutVar(pCut, k) );
1562 Vec_IntPush( vMapping, i );
1563 }
1564 assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
1565 p->pGia->vMapping = vMapping;
1566// Gia_ManMappingVerify( p->pGia );
1567}
Here is the caller graph for this function:

◆ Jf_ManDeriveMappingGia()

Gia_Man_t * Jf_ManDeriveMappingGia ( Jf_Man_t * p)

Function*************************************************************

Synopsis [Derives the result of mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 1431 of file giaJf.c.

1432{
1433 Gia_Man_t * pNew;
1434 Gia_Obj_t * pObj;
1435 Vec_Int_t * vCopies = Vec_IntStartFull( Gia_ManObjNum(p->pGia) );
1436 Vec_Int_t * vMapping = Vec_IntStart( 2 * Gia_ManObjNum(p->pGia) + (int)p->pPars->Edge + 2 * (int)p->pPars->Area );
1437 Vec_Int_t * vMapping2 = Vec_IntStart( (int)p->pPars->Edge + 2 * (int)p->pPars->Area + 1000 );
1438 Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
1439 Vec_Int_t * vLeaves = Vec_IntAlloc( 16 );
1440 Vec_Int_t * vLits = NULL, * vClas = NULL;
1441 int i, k, iLit, Class, * pCut;
1442 word uTruth = 0, * pTruth = &uTruth;
1443 assert( p->pPars->fCutMin );
1444 if ( p->pPars->fGenCnf )
1445 {
1446 vLits = Vec_IntAlloc( 1000 );
1447 vClas = Vec_IntAlloc( 1000 );
1448 Vec_IntPush( vClas, Vec_IntSize(vLits) );
1449 Vec_IntPush( vLits, 1 );
1450 }
1451 // create new manager
1452 pNew = Gia_ManStart( Gia_ManObjNum(p->pGia) );
1453 pNew->pName = Abc_UtilStrsav( p->pGia->pName );
1454 pNew->pSpec = Abc_UtilStrsav( p->pGia->pSpec );
1455 // map primary inputs
1456 Vec_IntWriteEntry( vCopies, 0, 0 );
1457 Gia_ManForEachCi( p->pGia, pObj, i )
1458 Vec_IntWriteEntry( vCopies, Gia_ObjId(p->pGia, pObj), Gia_ManAppendCi(pNew) );
1459 // iterate through nodes used in the mapping
1460 Gia_ManForEachAnd( p->pGia, pObj, i )
1461 {
1462 if ( Gia_ObjIsBuf(pObj) || Gia_ObjRefNum(p->pGia, pObj) == 0 )
1463 continue;
1464 pCut = Jf_ObjCutBest( p, i );
1465// printf( "Best cut of node %d: ", i ); Jf_CutPrint(pCut);
1466 Class = Jf_CutFuncClass( pCut );
1467 if ( Jf_CutSize(pCut) == 0 )
1468 {
1469 assert( Class == 0 );
1470 Vec_IntWriteEntry( vCopies, i, Jf_CutFunc(pCut) );
1471 continue;
1472 }
1473 if ( Jf_CutSize(pCut) == 1 )
1474 {
1475 assert( Class == 1 );
1476 iLit = Abc_LitNotCond( Jf_CutLit(pCut, 1) , Jf_CutFuncCompl(pCut) );
1477 iLit = Abc_Lit2LitL( Vec_IntArray(vCopies), iLit );
1478 Vec_IntWriteEntry( vCopies, i, iLit );
1479 continue;
1480 }
1481 if ( p->pPars->fFuncDsd )
1482 uTruth = Sdm_ManReadDsdTruth(p->pDsd, Class);
1483 else
1484 pTruth = Vec_MemReadEntry(p->vTtMem, Class);
1485 assert( p->pDsd == NULL || Sdm_ManReadDsdVarNum(p->pDsd, Class) == Jf_CutSize(pCut) );
1486 // collect leaves
1487 Vec_IntClear( vLeaves );
1488 Jf_CutForEachLit( pCut, iLit, k )
1489 Vec_IntPush( vLeaves, Abc_Lit2LitL(Vec_IntArray(vCopies), iLit) );
1490 // create GIA
1491 iLit = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vLeaves), vCover, vLeaves, 0 );
1492 if ( p->pPars->fGenCnf )
1493 Jf_ManGenCnf( uTruth, iLit, vLeaves, vLits, vClas, vCover );
1494 iLit = Abc_LitNotCond( iLit, Jf_CutFuncCompl(pCut) );
1495 Vec_IntWriteEntry( vCopies, i, iLit );
1496 // create mapping
1497 Vec_IntSetEntry( vMapping, Abc_Lit2Var(iLit), Vec_IntSize(vMapping2) );
1498 Vec_IntPush( vMapping2, Vec_IntSize(vLeaves) );
1499 Vec_IntForEachEntry( vLeaves, iLit, k )
1500 Vec_IntPush( vMapping2, Abc_Lit2Var(iLit) );
1501 Vec_IntPush( vMapping2, Abc_Lit2Var(Vec_IntEntry(vCopies, i)) );
1502 }
1503 Gia_ManForEachCo( p->pGia, pObj, i )
1504 {
1505 if ( p->pPars->fGenCnf )
1506 Vec_IntClear( vLeaves );
1507 iLit = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) );
1508 if ( p->pPars->fGenCnf )
1509 Vec_IntPush( vLeaves, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1510 iLit = Gia_ManAppendCo( pNew, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
1511 if ( p->pPars->fGenCnf )
1512 Jf_ManGenCnf( ABC_CONST(0xAAAAAAAAAAAAAAAA), iLit, vLeaves, vLits, vClas, vCover );
1513 }
1514 Vec_IntFree( vCopies );
1515 Vec_IntFree( vCover );
1516 Vec_IntFree( vLeaves );
1517 // finish mapping
1518 if ( Vec_IntSize(vMapping) > Gia_ManObjNum(pNew) )
1519 Vec_IntShrink( vMapping, Gia_ManObjNum(pNew) );
1520 else
1521 Vec_IntFillExtra( vMapping, Gia_ManObjNum(pNew), 0 );
1522 assert( Vec_IntSize(vMapping) == Gia_ManObjNum(pNew) );
1523 Vec_IntForEachEntry( vMapping, iLit, i )
1524 if ( iLit > 0 )
1525 Vec_IntAddToEntry( vMapping, i, Gia_ManObjNum(pNew) );
1526 Vec_IntAppend( vMapping, vMapping2 );
1527 Vec_IntFree( vMapping2 );
1528 // attach mapping and packing
1529 assert( pNew->vMapping == NULL );
1530 pNew->vMapping = vMapping;
1531 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p->pGia) );
1532 // derive CNF
1533 if ( p->pPars->fGenCnf )
1534 {
1535 if ( p->pPars->fCnfObjIds )
1536 pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
1537 else
1538 pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas, p->pPars->fAddOrCla );
1539 }
1540 Vec_IntFreeP( &vLits );
1541 Vec_IntFreeP( &vClas );
1542 return pNew;
1543}
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
void Jf_ManGenCnf(word uTruth, int iLitOut, Vec_Int_t *vLeaves, Vec_Int_t *vLits, Vec_Int_t *vClas, Vec_Int_t *vCover)
FUNCTION DEFINITIONS ///.
Definition giaJf.c:129
Cnf_Dat_t * Jf_ManCreateCnfRemap(Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas, int fAddOrCla)
Definition giaJf.c:163
int Kit_TruthToGia(Gia_Man_t *pMan, unsigned *pTruth, int nVars, Vec_Int_t *vMemory, Vec_Int_t *vLeaves, int fHash)
DECLARATIONS ///.
Definition kitHop.c:80
Cnf_Dat_t * Jf_ManCreateCnf(Gia_Man_t *p, Vec_Int_t *vLits, Vec_Int_t *vClas)
Definition giaJf.c:199
void * pData
Definition gia.h:198
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManDumpCnf()

void Jf_ManDumpCnf ( Gia_Man_t * p,
char * pFileName,
int fVerbose )

Definition at line 1767 of file giaJf.c.

1768{
1769 abctime clk = Abc_Clock();
1770 Gia_Man_t * pNew;
1771 Cnf_Dat_t * pCnf;
1772 pNew = Jf_ManDeriveCnfMiter( p, fVerbose );
1773 pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
1774 Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
1775 Gia_ManStop( pNew );
1776// if ( fVerbose )
1777 {
1778 printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
1779 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1780 }
1781 Cnf_DataFree(pCnf);
1782}
ABC_INT64_T abctime
Definition abc_global.h:332
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
void Cnf_DataWriteIntoFile(Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
Definition cnfMan.c:387
Gia_Man_t * Jf_ManDeriveCnfMiter(Gia_Man_t *p, int fVerbose)
Definition giaJf.c:1757
Here is the call graph for this function:

◆ Jf_ManFree()

void Jf_ManFree ( Jf_Man_t * p)

Definition at line 396 of file giaJf.c.

397{
398 if ( p->pPars->fVerbose && p->pDsd )
399 Sdm_ManPrintDsdStats( p->pDsd, 0 );
400 if ( p->pPars->fVerbose && p->vTtMem )
401 {
402 printf( "Unique truth tables = %d. Memory = %.2f MB ", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
403 Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
404 }
405 if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && p->pPars->fFuncDsd )
407 if ( p->pPars->fCoarsen )
408 Gia_ManCleanMark0( p->pGia );
409 ABC_FREE( p->pGia->pRefs );
410 ABC_FREE( p->vCuts.pArray );
411 ABC_FREE( p->vArr.pArray );
412 ABC_FREE( p->vDep.pArray );
413 ABC_FREE( p->vFlow.pArray );
414 ABC_FREE( p->vRefs.pArray );
415 if ( p->pPars->fCutMin && !p->pPars->fFuncDsd )
416 {
417 Vec_MemHashFree( p->vTtMem );
418 Vec_MemFree( p->vTtMem );
419 }
420 Vec_IntFreeP( &p->vCnfs );
421 Vec_SetFree_( &p->pMem );
422 Vec_IntFreeP( &p->vTemp );
423 ABC_FREE( p );
424}
#define ABC_FREE(obj)
Definition abc_global.h:267
void Sdm_ManPrintDsdStats(Sdm_Man_t *p, int fVerbose)
FUNCTION DEFINITIONS ///.
void Jf_ManProfileClasses(Jf_Man_t *p)
Definition giaJf.c:308
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManGenCnf()

void Jf_ManGenCnf ( word uTruth,
int iLitOut,
Vec_Int_t * vLeaves,
Vec_Int_t * vLits,
Vec_Int_t * vClas,
Vec_Int_t * vCover )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Derives CNF for the mapped GIA.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file giaJf.c.

130{
131 if ( uTruth == 0 || ~uTruth == 0 )
132 {
133 Vec_IntPush( vClas, Vec_IntSize(vLits) );
134 Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, (uTruth == 0)) );
135 }
136 else
137 {
138 int i, k, c, Literal, Cube;
139 assert( Vec_IntSize(vLeaves) > 0 );
140 for ( c = 0; c < 2; c ++ )
141 {
142 int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, Vec_IntSize(vLeaves), vCover, 0 );
143 assert( RetValue == 0 );
144 Vec_IntForEachEntry( vCover, Cube, i )
145 {
146 Vec_IntPush( vClas, Vec_IntSize(vLits) );
147 Vec_IntPush( vLits, Abc_LitNotCond(iLitOut, c) );
148 for ( k = 0; k < Vec_IntSize(vLeaves); k++ )
149 {
150 Literal = 3 & (Cube >> (k << 1));
151 if ( Literal == 1 ) // '0' -> pos lit
152 Vec_IntPush( vLits, Abc_LitNotCond(Vec_IntEntry(vLeaves, k), 0) );
153 else if ( Literal == 2 ) // '1' -> neg lit
154 Vec_IntPush( vLits, Abc_LitNotCond(Vec_IntEntry(vLeaves, k), 1) );
155 else if ( Literal != 0 )
156 assert( 0 );
157 }
158 }
159 uTruth = ~uTruth;
160 }
161 }
162}
struct cube Cube
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManInitRefs()

float * Jf_ManInitRefs ( Jf_Man_t * pMan)

Function*************************************************************

Synopsis [Computing references while discounting XOR/MUX.]

Description []

SideEffects []

SeeAlso []

Definition at line 245 of file giaJf.c.

246{
247 Gia_Man_t * p = pMan->pGia;
248 Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
249 float * pRes; int i;
250 assert( p->pRefs == NULL );
251 p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
252 Gia_ManForEachAnd( p, pObj, i )
253 {
254 Gia_ObjRefFanin0Inc( p, pObj );
255 if ( Gia_ObjIsBuf(pObj) )
256 continue;
257 Gia_ObjRefFanin1Inc( p, pObj );
258 if ( !Gia_ObjIsMuxType(pObj) )
259 continue;
260 // discount XOR/MUX
261 pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
262 Gia_ObjRefDec( p, Gia_Regular(pCtrl) );
263 if ( Gia_Regular(pData1) == Gia_Regular(pData0) )
264 Gia_ObjRefDec( p, Gia_Regular(pData1) );
265 }
266 Gia_ManForEachCo( p, pObj, i )
267 Gia_ObjRefFanin0Inc( p, pObj );
268 // mark XOR/MUX internal nodes, which are not used elsewhere
269 if ( pMan->pPars->fCoarsen )
270 {
271 pMan->nCoarse = 0;
272 Gia_ManForEachAnd( p, pObj, i )
273 {
274 if ( !Gia_ObjIsMuxType(pObj) )
275 continue;
276 if ( Gia_ObjRefNum(p, Gia_ObjFanin0(pObj)) == 1 )
277 {
278 Jf_ObjSetUnit(Gia_ObjFanin0(Gia_ObjFanin0(pObj)));
279 Jf_ObjSetUnit(Gia_ObjFanin0(Gia_ObjFanin1(pObj)));
280 Jf_ObjCleanUnit(Gia_ObjFanin0(pObj)), pMan->nCoarse++;
281 }
282 if ( Gia_ObjRefNum(p, Gia_ObjFanin1(pObj)) == 1 )
283 {
284 Jf_ObjSetUnit(Gia_ObjFanin1(Gia_ObjFanin0(pObj)));
285 Jf_ObjSetUnit(Gia_ObjFanin1(Gia_ObjFanin1(pObj)));
286 Jf_ObjCleanUnit(Gia_ObjFanin1(pObj)), pMan->nCoarse++;
287 }
288 }
289 }
290 // multiply by factor
291 pRes = ABC_ALLOC( float, Gia_ManObjNum(p) );
292 for ( i = 0; i < Gia_ManObjNum(p); i++ )
293 pRes[i] = Abc_MaxInt( 1, p->pRefs[i] );
294 return pRes;
295}
Gia_Obj_t * Gia_ObjRecognizeMux(Gia_Obj_t *pNode, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition giaUtil.c:1056
int Gia_ObjIsMuxType(Gia_Obj_t *pNode)
Definition giaUtil.c:982
int nCoarse
Definition giaJf.c:70
Gia_Man_t * pGia
Definition giaJf.c:55
Jf_Par_t * pPars
Definition giaJf.c:56
int fCoarsen
Definition gia.h:357
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManPerformMapping()

Gia_Man_t * Jf_ManPerformMapping ( Gia_Man_t * pGia,
Jf_Par_t * pPars )

Definition at line 1715 of file giaJf.c.

1716{
1717 Gia_Man_t * pNew = pGia;
1718 Jf_Man_t * p; int i;
1719 assert( !Gia_ManBufNum(pGia) );
1720 assert( !pPars->fCutMin || !pPars->fFuncDsd || pPars->nLutSize <= 6 );
1721 if ( pPars->fGenCnf )
1722 pPars->fCutMin = 1, pPars->fFuncDsd = 1, pPars->fOptEdge = 0;
1723 if ( pPars->fCutMin && !pPars->fFuncDsd )
1724 pPars->fCoarsen = 0;
1725 p = Jf_ManAlloc( pGia, pPars );
1726 p->pCutCmp = pPars->fAreaOnly ? Jf_CutCompareArea : Jf_CutCompareDelay;
1727 Jf_ManComputeCuts( p, 0 );
1728 Jf_ManComputeRefs( p ); Jf_ManPrintStats( p, "Start" );
1729 for ( i = 0; i < pPars->nRounds; i++ )
1730 {
1731 if ( !p->pPars->fGenCnf )
1732 {
1733 Jf_ManPropagateFlow( p, pPars->fOptEdge ); Jf_ManPrintStats( p, "Flow " );
1734 }
1735 Jf_ManPropagateEla( p, 0 ); Jf_ManPrintStats( p, "Area " );
1736 Jf_ManPropagateEla( p, 1 ); Jf_ManPrintStats( p, "Edge " );
1737 }
1738 if ( p->pPars->fVeryVerbose && p->pPars->fCutMin && !p->pPars->fFuncDsd )
1739 Vec_MemDumpTruthTables( p->vTtMem, Gia_ManName(p->pGia), p->pPars->nLutSize );
1740 if ( p->pPars->fPureAig )
1741 pNew = Jf_ManDeriveGia(p);
1742 else if ( p->pPars->fCutMin )
1743 pNew = Jf_ManDeriveMappingGia(p);
1744 else
1746 Jf_ManFree( p );
1747 return pNew;
1748}
Gia_Man_t * Jf_ManDeriveMappingGia(Jf_Man_t *p)
Definition giaJf.c:1431
Gia_Man_t * Jf_ManDeriveGia(Jf_Man_t *p)
Definition giaJf.c:1580
void Jf_ManPrintStats(Jf_Man_t *p, char *pTitle)
Definition giaJf.c:1702
Jf_Man_t * Jf_ManAlloc(Gia_Man_t *pGia, Jf_Par_t *pPars)
Definition giaJf.c:365
int Jf_ManComputeRefs(Jf_Man_t *p)
Definition giaJf.c:1308
void Jf_ManDeriveMapping(Jf_Man_t *p)
Definition giaJf.c:1544
void Jf_ManComputeCuts(Jf_Man_t *p, int fEdge)
Definition giaJf.c:1240
float Jf_CutCompareArea(Jf_Cut_t *pOld, Jf_Cut_t *pNew)
Definition giaJf.c:949
float Jf_CutCompareDelay(Jf_Cut_t *pOld, Jf_Cut_t *pNew)
Definition giaJf.c:940
void Jf_ManPropagateEla(Jf_Man_t *p, int fEdge)
Definition giaJf.c:1392
void Jf_ManPropagateFlow(Jf_Man_t *p, int fEdge)
Definition giaJf.c:1381
void Jf_ManFree(Jf_Man_t *p)
Definition giaJf.c:396
int nRounds
Definition gia.h:339
int fOptEdge
Definition gia.h:354
int fAreaOnly
Definition gia.h:350
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManPrintStats()

void Jf_ManPrintStats ( Jf_Man_t * p,
char * pTitle )

Definition at line 1702 of file giaJf.c.

1703{
1704 if ( !p->pPars->fVerbose )
1705 return;
1706 printf( "%s : ", pTitle );
1707 printf( "Level =%6lu ", (long)p->pPars->Delay );
1708 printf( "Area =%9lu ", (long)p->pPars->Area );
1709 printf( "Edge =%9lu ", (long)p->pPars->Edge );
1710 if ( p->pPars->fGenCnf )
1711 printf( "Cnf =%9lu ", (long)p->pPars->Clause );
1712 Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
1713 fflush( stdout );
1714}
Here is the caller graph for this function:

◆ Jf_ManProfileClasses()

void Jf_ManProfileClasses ( Jf_Man_t * p)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file giaJf.c.

309{
310 Gia_Obj_t * pObj;
311 int Counts[595] = {0}, Costs[595] = {0};
312 int i, iFunc, Total = 0, CostTotal = 0, Other = 0, CostOther = 0;
313 printf( "DSD classes that appear in more than %.1f %% of mapped nodes:\n", 0.1 * p->pPars->nVerbLimit );
314 Gia_ManForEachAnd( p->pGia, pObj, i )
315 if ( !Gia_ObjIsBuf(pObj) && Gia_ObjRefNumId(p->pGia, i) )
316 {
317 iFunc = Jf_CutFuncClass( Jf_ObjCutBest(p, i) );
318 assert( iFunc < 595 );
319 if ( p->pPars->fGenCnf )
320 {
321 Costs[iFunc] += Jf_CutCnfSizeF(p, iFunc);
322 CostTotal += Jf_CutCnfSizeF(p, iFunc);
323 }
324 Counts[iFunc]++;
325 Total++;
326 }
327 CostTotal = Abc_MaxInt(CostTotal, 1);
328 Total = Abc_MaxInt(Total, 1);
329 for ( i = 0; i < 595; i++ )
330 if ( Counts[i] && 100.0 * Counts[i] / Total >= 0.1 * p->pPars->nVerbLimit )
331 {
332 printf( "%5d : ", i );
333 printf( "%-20s ", Sdm_ManReadDsdStr(p->pDsd, i) );
334 printf( "%8d ", Counts[i] );
335 printf( "%5.1f %% ", 100.0 * Counts[i] / Total );
336 printf( "%8d ", Costs[i] );
337 printf( "%5.1f %%", 100.0 * Costs[i] / CostTotal );
338 printf( "\n" );
339 }
340 else
341 {
342 Other += Counts[i];
343 CostOther += Costs[i];
344 }
345 printf( "Other : " );
346 printf( "%-20s ", "" );
347 printf( "%8d ", Other );
348 printf( "%5.1f %% ", 100.0 * Other / Total );
349 printf( "%8d ", CostOther );
350 printf( "%5.1f %%", 100.0 * CostOther / CostTotal );
351 printf( "\n" );
352}
char * Sdm_ManReadDsdStr(Sdm_Man_t *p, int iDsd)
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManPropagateEla()

void Jf_ManPropagateEla ( Jf_Man_t * p,
int fEdge )

Definition at line 1392 of file giaJf.c.

1393{
1394 Gia_Obj_t * pObj;
1395 int i, CostBef, CostAft;
1396 p->pPars->Area = p->pPars->Edge = p->pPars->Clause = 0;
1397 Gia_ManForEachObjReverse( p->pGia, pObj, i )
1398 if ( Gia_ObjIsBuf(pObj) )
1399 Jf_ObjPropagateBuf( p, pObj, 1 );
1400 else if ( Gia_ObjIsAnd(pObj) && Gia_ObjRefNum(p->pGia, pObj) > 0 )
1401 {
1402 assert( Jf_ObjIsUnit(pObj) );
1403 if ( Jf_CutCheckMffc(p, Jf_ObjCutBest(p, i), 50) )
1404 {
1405 CostBef = Jf_CutDeref_rec( p, Jf_ObjCutBest(p, i) );
1406 Jf_ObjComputeBestCut( p, pObj, fEdge, 1 );
1407 CostAft = Jf_CutRef_rec( p, Jf_ObjCutBest(p, i) );
1408 // if ( CostBef != CostAft ) printf( "%d -> %d ", CostBef, CostAft );
1409 assert( CostBef >= CostAft ); // does not hold because of JF_EDGE_LIM
1410 }
1411 if ( p->pPars->fGenCnf )
1412 p->pPars->Clause += Jf_CutCnfSize(p, Jf_ObjCutBest(p, i));
1413 p->pPars->Edge += Jf_CutSize(Jf_ObjCutBest(p, i));
1414 p->pPars->Area++;
1415 }
1416 p->pPars->Delay = Jf_ManComputeDelay( p, 1 );
1417// printf( "\n" );
1418}
void Jf_ObjComputeBestCut(Jf_Man_t *p, Gia_Obj_t *pObj, int fEdge, int fEla)
Definition giaJf.c:1359
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManPropagateFlow()

void Jf_ManPropagateFlow ( Jf_Man_t * p,
int fEdge )

Definition at line 1381 of file giaJf.c.

1382{
1383 Gia_Obj_t * pObj;
1384 int i;
1385 Gia_ManForEachObj( p->pGia, pObj, i )
1386 if ( Gia_ObjIsBuf(pObj) )
1387 Jf_ObjPropagateBuf( p, pObj, 0 );
1388 else if ( Gia_ObjIsAnd(pObj) && Jf_ObjIsUnit(pObj) )
1389 Jf_ObjComputeBestCut( p, pObj, fEdge, 0 );
1391}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManSetDefaultPars()

void Jf_ManSetDefaultPars ( Jf_Par_t * pPars)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1682 of file giaJf.c.

1683{
1684 memset( pPars, 0, sizeof(Jf_Par_t) );
1685 pPars->nLutSize = 6;
1686 pPars->nCutNum = 8;
1687 pPars->nRounds = 1;
1688 pPars->nVerbLimit = 5;
1689 pPars->DelayTarget = -1;
1690 pPars->fAreaOnly = 1;
1691 pPars->fOptEdge = 1;
1692 pPars->fCoarsen = 0;
1693 pPars->fCutMin = 0;
1694 pPars->fFuncDsd = 0;
1695 pPars->fGenCnf = 0;
1696 pPars->fPureAig = 0;
1697 pPars->fVerbose = 0;
1698 pPars->fVeryVerbose = 0;
1699 pPars->nLutSizeMax = JF_LEAF_MAX;
1700 pPars->nCutNumMax = JF_CUT_MAX;
1701}
int nCutNumMax
Definition gia.h:373
int nLutSizeMax
Definition gia.h:372
int fVeryVerbose
Definition gia.h:371
int fPureAig
Definition gia.h:365
int nVerbLimit
Definition gia.h:345
int DelayTarget
Definition gia.h:349
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ManTestCnf()

void Jf_ManTestCnf ( Gia_Man_t * p)

Definition at line 1784 of file giaJf.c.

1785{
1786 Gia_Man_t * pNew;
1787 Cnf_Dat_t * pCnf;
1788 int i;
1789// Cnf_Dat_t * pCnf = Cnf_DeriveGia( p );
1790 pNew = Jf_ManDeriveCnf( p, 1 );
1791 pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
1792 Cnf_DataWriteIntoFile( pCnf, "test.cnf", 0, NULL, NULL );
1793 for ( i = 0; i < pCnf->nVars; i++ )
1794 printf( "%d : %d %d\n", i, pCnf->pObj2Count[i], pCnf->pObj2Clause[i] );
1795 Gia_ManStop( pNew );
1796 Cnf_DataFree(pCnf);
1797}
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition giaJf.c:1749
Here is the call graph for this function:

◆ Jf_ObjComputeBestCut()

void Jf_ObjComputeBestCut ( Jf_Man_t * p,
Gia_Obj_t * pObj,
int fEdge,
int fEla )

Function*************************************************************

Synopsis [Mapping rounds.]

Description []

SideEffects []

SeeAlso []

Definition at line 1359 of file giaJf.c.

1360{
1361 int i, iObj = Gia_ObjId( p->pGia, pObj );
1362 int * pCuts = Jf_ObjCuts( p, iObj );
1363 int * pCut, * pCutBest = NULL;
1364 int Time = ABC_INFINITY, TimeBest = ABC_INFINITY;
1365 float Area, AreaBest = ABC_INFINITY;
1366 Jf_ObjForEachCut( pCuts, pCut, i )
1367 {
1368 if ( Jf_CutIsTriv(pCut, iObj) ) continue;
1369 if ( fEdge && !fEla )
1370 Jf_CutSetCost(pCut, Jf_CutSize(pCut));
1371 Area = fEla ? Jf_CutArea(p, pCut, fEdge) : Jf_CutFlow(p, pCut) + Jf_CutCost(pCut);
1372 if ( pCutBest == NULL || AreaBest > Area + JF_EPSILON || (AreaBest > Area - JF_EPSILON && TimeBest > (Time = Jf_CutArr(p, pCut))) )
1373 pCutBest = pCut, AreaBest = Area, TimeBest = Time;
1374 }
1375 Vec_IntWriteEntry( &p->vArr, iObj, Jf_CutArr(p, pCutBest) );
1376 if ( !fEla )
1377 Vec_FltWriteEntry( &p->vFlow, iObj, AreaBest / Jf_ObjRefs(p, iObj) );
1378 Jf_ObjSetBestCut( pCuts, pCutBest, p->vTemp );
1379// Jf_CutPrint( Jf_ObjCutBest(p, iObj) ); printf( "\n" );
1380}
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250
#define Jf_ObjForEachCut(pList, pCut, i)
Definition giaJf.c:108
Here is the caller graph for this function:

◆ Jf_ObjComputeCuts()

void Jf_ObjComputeCuts ( Jf_Man_t * p,
Gia_Obj_t * pObj,
int fEdge )

Definition at line 1127 of file giaJf.c.

1128{
1129 int LutSize = p->pPars->nLutSize;
1130 int CutNum = p->pPars->nCutNum;
1131 int iObj = Gia_ObjId(p->pGia, pObj);
1132 word Sign0[JF_CUT_MAX+2]; // signatures of the first cut
1133 word Sign1[JF_CUT_MAX+2]; // signatures of the second cut
1134 Jf_Cut_t Sto[JF_CUT_MAX+2]; // cut storage
1135 Jf_Cut_t * pSto[JF_CUT_MAX+2]; // pointers to cut storage
1136 int * pCut0, * pCut1, * pCuts0, * pCuts1;
1137 int nOldSupp, Config, i, k, c = 0;
1138 // prepare cuts
1139 for ( i = 0; i <= CutNum+1; i++ )
1140 pSto[i] = Sto + i, pSto[i]->Cost = 0, pSto[i]->iFunc = ~0;
1141 // compute signatures
1142 pCuts0 = Jf_ObjCuts( p, Gia_ObjFaninId0(pObj, iObj) );
1143 Jf_ObjForEachCut( pCuts0, pCut0, i )
1144 Sign0[i] = Jf_CutGetSign( pCut0 );
1145 // compute signatures
1146 pCuts1 = Jf_ObjCuts( p, Gia_ObjFaninId1(pObj, iObj) );
1147 Jf_ObjForEachCut( pCuts1, pCut1, i )
1148 Sign1[i] = Jf_CutGetSign( pCut1 );
1149 // merge cuts
1150 p->CutCount[0] += pCuts0[0] * pCuts1[0];
1151 Jf_ObjForEachCut( pCuts0, pCut0, i )
1152 Jf_ObjForEachCut( pCuts1, pCut1, k )
1153 {
1154 if ( Jf_CountBits(Sign0[i] | Sign1[k]) > LutSize )
1155 continue;
1156 p->CutCount[1]++;
1157 if ( !p->pPars->fCutMin )
1158 {
1159 if ( !Jf_CutMergeOrder(pCut0, pCut1, pSto[c]->pCut, LutSize) )
1160 continue;
1161 pSto[c]->Sign = Sign0[i] | Sign1[k];
1162 }
1163 else if ( p->pPars->fFuncDsd )
1164 {
1165 if ( !(Config = Jf_CutMerge2(pCut0, pCut1, pSto[c]->pCut, LutSize)) )
1166 continue;
1167 pSto[c]->Sign = Sign0[i] | Sign1[k];
1168 nOldSupp = pSto[c]->pCut[0];
1169 pSto[c]->iFunc = Sdm_ManComputeFunc( p->pDsd, Jf_ObjFunc0(pObj, pCut0), Jf_ObjFunc1(pObj, pCut1), pSto[c]->pCut, Config, 0 );
1170 if ( pSto[c]->iFunc == -1 )
1171 continue;
1172 if ( p->pPars->fGenCnf && Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[c]->iFunc)) >= 12 ) // no more than 15
1173 continue;
1174 assert( pSto[c]->pCut[0] <= nOldSupp );
1175 if ( pSto[c]->pCut[0] < nOldSupp )
1176 pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut );
1177 }
1178 else
1179 {
1180 if ( !Jf_CutMergeOrder(pCut0, pCut1, pSto[c]->pCut, LutSize) )
1181 continue;
1182 pSto[c]->Sign = Sign0[i] | Sign1[k];
1183 nOldSupp = pSto[c]->pCut[0];
1184 pSto[c]->iFunc = Jf_TtComputeForCut( p, Jf_ObjFunc0(pObj, pCut0), Jf_ObjFunc1(pObj, pCut1), pCut0, pCut1, pSto[c]->pCut );
1185 assert( pSto[c]->pCut[0] <= nOldSupp );
1186 if ( pSto[c]->pCut[0] < nOldSupp )
1187 pSto[c]->Sign = Jf_CutGetSign( pSto[c]->pCut );
1188 if ( pSto[c]->iFunc >= (1 << 24) )
1189 printf( "Hard limit on the number of different Boolean functions (2^23) is reached. Quitting...\n" ), exit(1);
1190 }
1191 p->CutCount[2]++;
1192 pSto[c]->Time = p->pPars->fAreaOnly ? 0 : Jf_CutArr(p, pSto[c]->pCut);
1193 pSto[c]->Flow = Jf_CutFlow(p, pSto[c]->pCut);
1194 c = Jf_ObjAddCutToStore( p, pSto, c, CutNum );
1195 assert( c <= CutNum );
1196 }
1197// Jf_ObjPrintStore( p, pSto, c );
1198// Jf_ObjCheckStore( p, pSto, c, iObj );
1199 // add two variable cut
1200 if ( !Jf_ObjIsUnit(pObj) && !Jf_ObjHasCutWithSize(pSto, c, 2) )
1201 {
1202 assert( Jf_ObjIsUnit(Gia_ObjFanin0(pObj)) && Jf_ObjIsUnit(Gia_ObjFanin1(pObj)) );
1203 if ( p->pPars->fCutMin ) pSto[c]->iFunc = 4; // set function (DSD only!)
1204 pSto[c]->pCut[0] = 2;
1205 pSto[c]->pCut[1] = Jf_ObjLit(Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj));
1206 pSto[c]->pCut[2] = Jf_ObjLit(Gia_ObjFaninId1(pObj, iObj), Gia_ObjFaninC1(pObj));
1207 c++;
1208 }
1209 // add elementary cut
1210 if ( Jf_ObjIsUnit(pObj) && !(p->pPars->fCutMin && Jf_ObjHasCutWithSize(pSto, c, 1)) )
1211 {
1212 if ( p->pPars->fCutMin ) pSto[c]->iFunc = 2; // set function
1213 pSto[c]->pCut[0] = 1;
1214 pSto[c]->pCut[1] = Jf_ObjLit(iObj, 0);
1215 c++;
1216 }
1217 // reorder cuts
1218// Jf_ObjSortCuts( pSto + 1, c - 1 );
1219// Jf_ObjCheckPtrs( pSto, CutNum );
1220 // find cost of the best cut
1221 pSto[0]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[0]->iFunc)) : 1;
1222 assert( pSto[0]->Cost >= 0 );
1223 // save best info
1224 assert( pSto[0]->Flow >= 0 );
1225 Vec_IntWriteEntry( &p->vArr, iObj, pSto[0]->Time );
1226 Vec_FltWriteEntry( &p->vFlow, iObj, (pSto[0]->Flow + (fEdge ? pSto[0]->pCut[0] : pSto[0]->Cost)) / Jf_ObjRefs(p, iObj) );
1227 // add cuts to storage cuts
1228 Vec_IntClear( p->vTemp );
1229 Vec_IntPush( p->vTemp, c );
1230 for ( i = 0; i < c; i++ )
1231 {
1232 pSto[i]->Cost = p->pPars->fGenCnf ? Jf_CutCnfSizeF(p, Abc_Lit2Var(pSto[i]->iFunc)) : 1;
1233 Vec_IntPush( p->vTemp, Jf_CutSetAll(pSto[i]->iFunc, pSto[i]->Cost, pSto[i]->pCut[0]) );
1234 for ( k = 1; k <= pSto[i]->pCut[0]; k++ )
1235 Vec_IntPush( p->vTemp, pSto[i]->pCut[k] );
1236 }
1237 Vec_IntWriteEntry( &p->vCuts, iObj, Vec_SetAppend(&p->pMem, Vec_IntArray(p->vTemp), Vec_IntSize(p->vTemp)) );
1238 p->CutCount[3] += c;
1239}
int Sdm_ManComputeFunc(Sdm_Man_t *p, int iDsdLit0, int iDsdLit1, int *pCut, int uMask, int fXor)
int Jf_TtComputeForCut(Jf_Man_t *p, int iFuncLit0, int iFuncLit1, int *pCut0, int *pCut1, int *pCutOut)
Definition giaJf.c:1070
struct Jf_Cut_t_ Jf_Cut_t
Definition giaJf.c:41
int iFunc
Definition giaJf.c:47
int Cost
Definition giaJf.c:48
word Sign
Definition giaJf.c:44
VOID_HACK exit()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Jf_ObjCutFilter()

int Jf_ObjCutFilter ( Jf_Man_t * p,
Jf_Cut_t ** pSto,
int c )

Definition at line 788 of file giaJf.c.

789{
790 int k;
791 if ( p->pPars->fCutMin )
792 {
793 for ( k = 0; k < c; k++ )
794 if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
795 (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
796 Jf_CutIsContained1(pSto[c]->pCut, pSto[k]->pCut) )
797 return 0;
798 }
799 else
800 {
801 for ( k = 0; k < c; k++ )
802 if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
803 (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
804 Jf_CutIsContainedOrder(pSto[c]->pCut, pSto[k]->pCut) )
805 return 0;
806 }
807 return 1;
808}

◆ Jf_ObjCutFilterBoth()

int Jf_ObjCutFilterBoth ( Jf_Man_t * p,
Jf_Cut_t ** pSto,
int c )

Function*************************************************************

Synopsis [Cut filtering.]

Description [Returns the number of cuts after filtering and the last cut in the last entry. If the cut is filtered, its size is set to -1.]

SideEffects [This was found to be 15% slower.]

SeeAlso []

Definition at line 761 of file giaJf.c.

762{
763 int k, last;
764 // filter this cut using other cuts
765 for ( k = 0; k < c; k++ )
766 if ( pSto[c]->pCut[0] >= pSto[k]->pCut[0] &&
767 (pSto[c]->Sign & pSto[k]->Sign) == pSto[k]->Sign &&
768 Jf_CutIsContained1(pSto[c]->pCut, pSto[k]->pCut) )
769 {
770 pSto[c]->pCut[0] = -1;
771 return c;
772 }
773 // filter other cuts using this cut
774 for ( k = last = 0; k < c; k++ )
775 if ( !(pSto[c]->pCut[0] < pSto[k]->pCut[0] &&
776 (pSto[c]->Sign & pSto[k]->Sign) == pSto[c]->Sign &&
777 Jf_CutIsContained1(pSto[k]->pCut, pSto[c]->pCut)) )
778 {
779 if ( last++ == k )
780 continue;
781 ABC_SWAP( Jf_Cut_t *, pSto[last-1], pSto[k] );
782 }
783 assert( last <= c );
784 if ( last < c )
785 ABC_SWAP( Jf_Cut_t *, pSto[last], pSto[c] );
786 return last;
787}
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253

◆ Jf_TtComputeForCut()

int Jf_TtComputeForCut ( Jf_Man_t * p,
int iFuncLit0,
int iFuncLit1,
int * pCut0,
int * pCut1,
int * pCutOut )

Function*************************************************************

Synopsis [Cut minimization.]

Description []

SideEffects []

SeeAlso []

Definition at line 1070 of file giaJf.c.

1071{
1072 word uTruth[JF_WORD_MAX], uTruth0[JF_WORD_MAX], uTruth1[JF_WORD_MAX];
1073 int fCompl, truthId;
1074 int LutSize = p->pPars->nLutSize;
1075 int nWords = Abc_Truth6WordNum(p->pPars->nLutSize);
1076 word * pTruth0 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit0));
1077 word * pTruth1 = Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(iFuncLit1));
1078 Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(iFuncLit0) );
1079 Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(iFuncLit1) );
1080 Abc_TtExpand( uTruth0, LutSize, pCut0 + 1, Jf_CutSize(pCut0), pCutOut + 1, Jf_CutSize(pCutOut) );
1081 Abc_TtExpand( uTruth1, LutSize, pCut1 + 1, Jf_CutSize(pCut1), pCutOut + 1, Jf_CutSize(pCutOut) );
1082 fCompl = (int)(uTruth0[0] & uTruth1[0] & 1);
1083 Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, fCompl );
1084 pCutOut[0] = Abc_TtMinBase( uTruth, pCutOut + 1, pCutOut[0], LutSize );
1085 assert( (uTruth[0] & 1) == 0 );
1086 truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
1087 return Abc_Var2Lit( truthId, fCompl );
1088}
Here is the caller graph for this function:

◆ Kit_TruthToGia()

int Kit_TruthToGia ( Gia_Man_t * pMan,
unsigned * pTruth,
int nVars,
Vec_Int_t * vMemory,
Vec_Int_t * vLeaves,
int fHash )
extern

DECLARATIONS ///.

CFile****************************************************************

FileName [giaMap.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Manipulation of mapping associated with the AIG.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
giaMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 80 of file kitHop.c.

81{
82 int iLit;
83 Kit_Graph_t * pGraph;
84 // transform truth table into the decomposition tree
85 if ( vMemory == NULL )
86 {
87 vMemory = Vec_IntAlloc( 0 );
88 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
89 Vec_IntFree( vMemory );
90 }
91 else
92 pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory );
93 if ( pGraph == NULL )
94 {
95 printf( "Kit_TruthToGia(): Converting truth table to AIG has failed for function:\n" );
96 Kit_DsdPrintFromTruth( pTruth, nVars ); printf( "\n" );
97 }
98 // derive the AIG for the decomposition tree
99 iLit = Kit_GraphToGia( pMan, pGraph, vLeaves, fHash );
100 Kit_GraphFree( pGraph );
101 return iLit;
102}
int Kit_GraphToGia(Gia_Man_t *pMan, Kit_Graph_t *pGraph, Vec_Int_t *vLeaves, int fHash)
Definition kitHop.c:70
struct Kit_Graph_t_ Kit_Graph_t
Definition kit.h:88
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
void Kit_GraphFree(Kit_Graph_t *pGraph)
Definition kitGraph.c:132
Kit_Graph_t * Kit_TruthToGraph(unsigned *pTruth, int nVars, Vec_Int_t *vMemory)
Definition kitGraph.c:356
Here is the caller graph for this function: