ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
darInt.h File Reference
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "dar.h"
Include dependency graph for darInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Dar_Cut_t_
 
struct  Dar_Man_t_
 

Macros

#define Dar_ObjForEachCutAll(pObj, pCut, i)
 MACRO DEFINITIONS ///.
 
#define Dar_ObjForEachCut(pObj, pCut, i)
 
#define Dar_CutForEachLeaf(p, pCut, pLeaf, i)
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
 INCLUDES ///.
 
typedef struct Dar_Cut_t_ Dar_Cut_t
 

Functions

void Dar_ManCutsRestart (Dar_Man_t *p, Aig_Obj_t *pRoot)
 FUNCTION DECLARATIONS ///.
 
void Dar_ManCutsFree (Dar_Man_t *p)
 
Dar_Cut_tDar_ObjPrepareCuts (Dar_Man_t *p, Aig_Obj_t *pObj)
 
Dar_Cut_tDar_ObjComputeCuts_rec (Dar_Man_t *p, Aig_Obj_t *pObj)
 
Dar_Cut_tDar_ObjComputeCuts (Dar_Man_t *p, Aig_Obj_t *pObj, int fSkipTtMin)
 
void Dar_ObjCutPrint (Aig_Man_t *p, Aig_Obj_t *pObj)
 
Vec_Int_tDar_LibReadNodes ()
 
Vec_Int_tDar_LibReadOuts ()
 
Vec_Int_tDar_LibReadPrios ()
 
void Dar_LibStart ()
 MACRO DEFINITIONS ///.
 
void Dar_LibStop ()
 
void Dar_LibReturnCanonicals (unsigned *pCanons)
 
void Dar_LibEval (Dar_Man_t *p, Aig_Obj_t *pRoot, Dar_Cut_t *pCut, int Required, int *pnMffcSize)
 
Aig_Obj_tDar_LibBuildBest (Dar_Man_t *p)
 
Dar_Man_tDar_ManStart (Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
 DECLARATIONS ///.
 
void Dar_ManStop (Dar_Man_t *p)
 
void Dar_ManPrintStats (Dar_Man_t *p)
 
char ** Dar_Permutations (int n)
 
void Dar_Truth4VarNPN (unsigned short **puCanons, char **puPhases, char **puPerms, unsigned char **puMap)
 

Macro Definition Documentation

◆ Dar_CutForEachLeaf

#define Dar_CutForEachLeaf ( p,
pCut,
pLeaf,
i )
Value:
for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )
Cube * p
Definition exorList.c:222

Definition at line 124 of file darInt.h.

124#define Dar_CutForEachLeaf( p, pCut, pLeaf, i ) \
125 for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )

◆ Dar_ObjForEachCut

#define Dar_ObjForEachCut ( pObj,
pCut,
i )
Value:
for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else

Definition at line 121 of file darInt.h.

121#define Dar_ObjForEachCut( pObj, pCut, i ) \
122 for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else

◆ Dar_ObjForEachCutAll

#define Dar_ObjForEachCutAll ( pObj,
pCut,
i )
Value:
for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 119 of file darInt.h.

119#define Dar_ObjForEachCutAll( pObj, pCut, i ) \
120 for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ )

Typedef Documentation

◆ Dar_Cut_t

typedef struct Dar_Cut_t_ Dar_Cut_t

Definition at line 52 of file darInt.h.

◆ Dar_Man_t

typedef typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t

INCLUDES ///.

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

FileName [darInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
darInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 51 of file darInt.h.

Function Documentation

◆ Dar_LibBuildBest()

Aig_Obj_t * Dar_LibBuildBest ( Dar_Man_t * p)
extern

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

Synopsis [Reconstructs the best cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 1031 of file darLib.c.

1032{
1033 int i, Counter = 4;
1034 for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
1035 s_DarLib->pDatas[i].pFunc = (Aig_Obj_t *)Vec_PtrEntry( p->vLeavesBest, i );
1036 Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
1037 return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
1038}
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Obj_t * Dar_LibBuildBest_rec(Dar_Man_t *p, Dar_LibObj_t *pObj)
Definition darLib.c:1005
void Dar_LibBuildClear_rec(Dar_LibObj_t *pObj, int *pCounter)
Definition darLib.c:984
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_LibEval()

void Dar_LibEval ( Dar_Man_t * p,
Aig_Obj_t * pRoot,
Dar_Cut_t * pCut,
int Required,
int * pnMffcSize )
extern

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

Synopsis [Evaluates one cut.]

Description [Returns the best gain.]

SideEffects []

SeeAlso []

Definition at line 920 of file darLib.c.

921{
922 int fTraining = 0;
923 float PowerSaved, PowerAdded;
924 Dar_LibObj_t * pObj;
925 int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
926 abctime clk = Abc_Clock();
927 if ( pCut->nLeaves != 4 )
928 return;
929 // check if the cut exits and assigns leaves and their levels
930 if ( !Dar_LibCutMatch(p, pCut) )
931 return;
932 // mark MFFC of the node
933 nNodesSaved = Dar_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL );
934 // evaluate the cut
935 Class = s_DarLib->pMap[pCut->uTruth];
936 Dar_LibEvalAssignNums( p, Class, pRoot );
937 // profile outputs by their savings
938 p->nTotalSubgs += s_DarLib->nSubgr0[Class];
939 p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
940 for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
941 {
942 pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
943 if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
944 continue;
945 nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL );
946 nNodesGained = nNodesSaved - nNodesAdded;
947 if ( p->pPars->fPower && PowerSaved < PowerAdded )
948 continue;
949 if ( fTraining && nNodesGained >= 0 )
950 Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
951 if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
952 continue;
953 if ( nNodesGained < p->GainBest ||
954 (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
955 continue;
956 // remember this possibility
957 Vec_PtrClear( p->vLeavesBest );
958 for ( k = 0; k < (int)pCut->nLeaves; k++ )
959 Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
960 p->OutBest = s_DarLib->pSubgr0[Class][Out];
961 p->OutNumBest = Out;
962 p->LevelBest = s_DarLib->pDatas[pObj->Num].Level;
963 p->GainBest = nNodesGained;
964 p->ClassBest = Class;
965 assert( p->LevelBest <= Required );
966 *pnMffcSize = nNodesSaved;
967 }
968clk = Abc_Clock() - clk;
969p->ClassTimes[Class] += clk;
970p->timeEval += clk;
971}
ABC_INT64_T abctime
Definition abc_global.h:332
struct Dar_LibObj_t_ Dar_LibObj_t
Definition darLib.c:33
int Dar_LibCutMatch(Dar_Man_t *p, Dar_Cut_t *pCut)
Definition darLib.c:706
int Dar_LibCutMarkMffc(Aig_Man_t *p, Aig_Obj_t *pRoot, int nLeaves, float *pPower)
Definition darLib.c:752
int Dar_LibEval_rec(Dar_LibObj_t *pObj, int Out, int nNodesSaved, int Required, float *pPower)
Definition darLib.c:863
void Dar_LibIncrementScore(int Class, int Out, int Gain)
Definition darLib.c:633
void Dar_LibEvalAssignNums(Dar_Man_t *p, int Class, Aig_Obj_t *pRoot)
Definition darLib.c:806
unsigned nLeaves
Definition darInt.h:62
unsigned uTruth
Definition darInt.h:58
unsigned Num
Definition darLib.c:44
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_LibReadNodes()

Vec_Int_t * Dar_LibReadNodes ( )
extern

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11094 of file darData.c.

11095{
11096 Vec_Int_t * vResult;
11097 int i;
11098 vResult = Vec_IntAlloc( s_nDataSize1 );
11099 for ( i = 0; i < s_nDataSize1; i++ )
11100 Vec_IntPush( vResult, s_Data1[i] );
11101 return vResult;
11102}
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
ABC_NAMESPACE_IMPL_START const int s_nDataSize1
DECLARATIONS ///.
Definition darData.c:33
unsigned int s_Data1[2 *43906]
Definition darData.c:34
Here is the caller graph for this function:

◆ Dar_LibReadOuts()

Vec_Int_t * Dar_LibReadOuts ( )
extern

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11115 of file darData.c.

11116{
11117 Vec_Int_t * vResult;
11118 int i;
11119 vResult = Vec_IntAlloc( s_nDataSize2 );
11120 for ( i = 0; i < s_nDataSize2; i++ )
11121 Vec_IntPush( vResult, s_Data2[i] );
11122 return vResult;
11123}
const int s_nDataSize2
Definition darData.c:7355
unsigned int s_Data2[24772]
Definition darData.c:7356
Here is the caller graph for this function:

◆ Dar_LibReadPrios()

Vec_Int_t * Dar_LibReadPrios ( )
extern

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

Synopsis [Reads library from array.]

Description []

SideEffects []

SeeAlso []

Definition at line 11136 of file darData.c.

11137{
11138 Vec_Int_t * vResult;
11139 int i;
11140 vResult = Vec_IntAlloc( s_nDataSize3 );
11141 for ( i = 0; i < s_nDataSize3; i++ )
11142 Vec_IntPush( vResult, s_Data3[i] );
11143 return vResult;
11144}
unsigned int s_Data3[24772]
Definition darData.c:9426
const int s_nDataSize3
Definition darData.c:9425
Here is the caller graph for this function:

◆ Dar_LibReturnCanonicals()

void Dar_LibReturnCanonicals ( unsigned * pCanons)
extern

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

Synopsis [Returns canonical truth tables.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file darLib.c.

212{
213 int Visits[222] = {0};
214 int i, k;
215 // find canonical truth tables
216 for ( i = k = 0; i < (1<<16); i++ )
217 if ( !Visits[s_DarLib->pMap[i]] )
218 {
219 Visits[s_DarLib->pMap[i]] = 1;
220 pCanons[k++] = ((i<<16) | i);
221 }
222 assert( k == 222 );
223}
Here is the caller graph for this function:

◆ Dar_LibStart()

void Dar_LibStart ( )
extern

MACRO DEFINITIONS ///.

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

Synopsis [Starts the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 593 of file darLib.c.

594{
595// abctime clk = Abc_Clock();
596 if ( s_DarLib != NULL )
597 return;
598 assert( s_DarLib == NULL );
599 s_DarLib = Dar_LibRead();
600// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );
601// ABC_PRT( "Time", Abc_Clock() - clk );
602}
Dar_Lib_t * Dar_LibRead()
Definition darLib.c:559

◆ Dar_LibStop()

void Dar_LibStop ( )
extern

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

Synopsis [Stops the library.]

Description []

SideEffects []

SeeAlso []

Definition at line 615 of file darLib.c.

616{
617 assert( s_DarLib != NULL );
618 Dar_LibFree( s_DarLib );
619 s_DarLib = NULL;
620}
void Dar_LibFree(Dar_Lib_t *p)
Definition darLib.c:164

◆ Dar_ManCutsFree()

void Dar_ManCutsFree ( Dar_Man_t * p)
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file darCut.c.

649{
650 if ( p->pMemCuts == NULL )
651 return;
652 Aig_MmFixedStop( p->pMemCuts, 0 );
653 p->pMemCuts = NULL;
654// Aig_ManCleanData( p );
655}
void Aig_MmFixedStop(Aig_MmFixed_t *p, int fVerbose)
Definition aigMem.c:132
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ManCutsRestart()

void Dar_ManCutsRestart ( Dar_Man_t * p,
Aig_Obj_t * pRoot )
extern

FUNCTION DECLARATIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 714 of file darCut.c.

715{
716 Aig_Obj_t * pObj;
717 int i;
718 Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
719 Vec_PtrForEachEntry( Aig_Obj_t *, p->vCutNodes, pObj, i )
720 if ( !Aig_ObjIsNone(pObj) )
721 Dar_ObjSetCuts( pObj, NULL );
722 Vec_PtrClear( p->vCutNodes );
723 Aig_MmFixedRestart( p->pMemCuts );
724 Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
725}
void Aig_MmFixedRestart(Aig_MmFixed_t *p)
Definition aigMem.c:232
Dar_Cut_t * Dar_ObjPrepareCuts(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition darCut.c:668
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ManPrintStats()

void Dar_ManPrintStats ( Dar_Man_t * p)
extern

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

Synopsis [Stops the AIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 93 of file darMan.c.

94{
95 unsigned pCanons[222];
96 int Gain, i;
97 extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
98
99 Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
100 printf( "Tried = %8d. Beg = %8d. End = %8d. Gain = %6d. (%6.2f %%). Cut mem = %d MB\n",
101 p->nNodesTried, p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
102 printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n",
103 p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
104 (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
105
106 printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d. Levels = %4d.\n",
107 Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes, Aig_ManLevels(p->pAig) );
108 ABC_PRT( "Cuts ", p->timeCuts );
109 ABC_PRT( "Eval ", p->timeEval );
110 ABC_PRT( "Other ", p->timeOther );
111 ABC_PRT( "TOTAL ", p->timeTotal );
112
113 if ( !p->pPars->fVeryVerbose )
114 return;
115 Dar_LibReturnCanonicals( pCanons );
116 for ( i = 0; i < 222; i++ )
117 {
118 if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
119 continue;
120 printf( "%3d : ", i );
121 printf( "G = %6d (%5.2f %%) ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
122 printf( "S = %8d (%5.2f %%) ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
123 printf( "R = %7d ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
124// Kit_DsdPrintFromTruth( pCanons + i, 4 );
125// ABC_PRTP( "T", p->ClassTimes[i], p->timeEval );
126 printf( "\n" );
127 }
128 fflush( stdout );
129}
#define ABC_PRT(a, t)
Definition abc_global.h:255
int Aig_ManLevels(Aig_Man_t *p)
Definition aigUtil.c:102
void Dar_LibReturnCanonicals(unsigned *pCanons)
Definition darLib.c:211
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ManStart()

Dar_Man_t * Dar_ManStart ( Aig_Man_t * pAig,
Dar_RwrPar_t * pPars )
extern

DECLARATIONS ///.

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

FileName [darMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [AIG manager.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id
darMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Starts the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file darMan.c.

45{
46 Dar_Man_t * p;
47 Aig_ManCleanData( pAig );
48 p = ABC_ALLOC( Dar_Man_t, 1 );
49 memset( p, 0, sizeof(Dar_Man_t) );
50 p->pPars = pPars;
51 p->pAig = pAig;
52 p->vCutNodes = Vec_PtrAlloc( 1000 );
53 p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
54 p->vLeavesBest = Vec_PtrAlloc( 4 );
55 return p;
56}
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Aig_MmFixed_t * Aig_MmFixedStart(int nEntrySize, int nEntriesMax)
FUNCTION DEFINITIONS ///.
Definition aigMem.c:96
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
typedefABC_NAMESPACE_HEADER_START struct Dar_Man_t_ Dar_Man_t
INCLUDES ///.
Definition darInt.h:51
struct Dar_Cut_t_ Dar_Cut_t
Definition darInt.h:52
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ManStop()

void Dar_ManStop ( Dar_Man_t * p)
extern

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

Synopsis [Stops the rewriting manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file darMan.c.

70{
71 if ( p->pPars->fVerbose )
73 if ( p->vCutNodes )
74 Vec_PtrFree( p->vCutNodes );
75 if ( p->pMemCuts )
76 Aig_MmFixedStop( p->pMemCuts, 0 );
77 if ( p->vLeavesBest )
78 Vec_PtrFree( p->vLeavesBest );
79 ABC_FREE( p );
80}
#define ABC_FREE(obj)
Definition abc_global.h:267
void Dar_ManPrintStats(Dar_Man_t *p)
Definition darMan.c:93
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ObjComputeCuts()

Dar_Cut_t * Dar_ObjComputeCuts ( Dar_Man_t * p,
Aig_Obj_t * pObj,
int fSkipTtMin )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file darCut.c.

739{
740 Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
741 Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
742 Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
743 Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
744 Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
745 int i, k;
746
747 assert( !Aig_IsComplement(pObj) );
748 assert( Aig_ObjIsNode(pObj) );
749 assert( Dar_ObjCuts(pObj) == NULL );
750 assert( Dar_ObjCuts(pFaninR0) != NULL );
751 assert( Dar_ObjCuts(pFaninR1) != NULL );
752
753 // set up the first cut
754 pCutSet = Dar_ObjPrepareCuts( p, pObj );
755 // make sure fanins cuts are computed
756 Dar_ObjForEachCut( pFaninR0, pCut0, i )
757 Dar_ObjForEachCut( pFaninR1, pCut1, k )
758 {
759 p->nCutsAll++;
760 // make sure K-feasible cut exists
761 if ( Dar_WordCountOnes(pCut0->uSign | pCut1->uSign) > 4 )
762 continue;
763 // get the next cut of this node
764 pCut = Dar_CutFindFree( p, pObj );
765 // create the new cut
766 if ( !Dar_CutMerge( pCut, pCut0, pCut1 ) )
767 {
768 assert( !pCut->fUsed );
769 continue;
770 }
771 p->nCutsTried++;
772 // check dominance
773 if ( Dar_CutFilter( pObj, pCut ) )
774 {
775 assert( !pCut->fUsed );
776 continue;
777 }
778 // compute truth table
779 pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );
780
781 // minimize support of the cut
782 if ( !fSkipTtMin && Dar_CutSuppMinimize( pCut ) )
783 {
784 int RetValue = Dar_CutFilter( pObj, pCut );
785 assert( !RetValue );
786 }
787
788 // assign the value of the cut
789 pCut->Value = Dar_CutFindValue( p, pCut );
790 // if the cut contains removed node, do not use it
791 if ( pCut->Value == 0 )
792 {
793 p->nCutsSkipped++;
794 pCut->fUsed = 0;
795 }
796 else if ( pCut->nLeaves < 2 )
797 return pCutSet;
798 }
799 // count the number of nontrivial cuts cuts
800 Dar_ObjForEachCut( pObj, pCut, i )
801 p->nCutsUsed += pCut->fUsed;
802 // discount trivial cut
803 p->nCutsUsed--;
804 return pCutSet;
805}
Aig_Obj_t * Aig_ObjReal_rec(Aig_Obj_t *pObj)
Definition aigUtil.c:476
#define Dar_ObjForEachCut(pObj, pCut, i)
Definition darInt.h:121
unsigned fUsed
Definition darInt.h:61
unsigned Value
Definition darInt.h:59
unsigned uSign
Definition darInt.h:57
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ObjComputeCuts_rec()

Dar_Cut_t * Dar_ObjComputeCuts_rec ( Dar_Man_t * p,
Aig_Obj_t * pObj )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 818 of file darCut.c.

819{
820 if ( Dar_ObjCuts(pObj) )
821 return Dar_ObjCuts(pObj);
822 if ( Aig_ObjIsCi(pObj) )
823 return Dar_ObjPrepareCuts( p, pObj );
824 if ( Aig_ObjIsBuf(pObj) )
825 return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
826 Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
827 Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
828 return Dar_ObjComputeCuts( p, pObj, 0 );
829}
Dar_Cut_t * Dar_ObjComputeCuts(Dar_Man_t *p, Aig_Obj_t *pObj, int fSkipTtMin)
Definition darCut.c:738
Dar_Cut_t * Dar_ObjComputeCuts_rec(Dar_Man_t *p, Aig_Obj_t *pObj)
Definition darCut.c:818
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_ObjCutPrint()

void Dar_ObjCutPrint ( Aig_Man_t * p,
Aig_Obj_t * pObj )
extern

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

Synopsis [Prints one cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 65 of file darCut.c.

66{
67 Dar_Cut_t * pCut;
68 int i;
69 printf( "Cuts for node %d:\n", pObj->Id );
70 Dar_ObjForEachCut( pObj, pCut, i )
71 Dar_CutPrint( pCut );
72// printf( "\n" );
73}
ABC_NAMESPACE_IMPL_START void Dar_CutPrint(Dar_Cut_t *pCut)
DECLARATIONS ///.
Definition darCut.c:45
int Id
Definition aig.h:85
Here is the call graph for this function:

◆ Dar_ObjPrepareCuts()

Dar_Cut_t * Dar_ObjPrepareCuts ( Dar_Man_t * p,
Aig_Obj_t * pObj )
extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 668 of file darCut.c.

669{
670 Dar_Cut_t * pCutSet, * pCut;
671 int i;
672 assert( Dar_ObjCuts(pObj) == NULL );
673 pObj->nCuts = p->pPars->nCutsMax;
674 // create the cutset of the node
675 pCutSet = (Dar_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
676 memset( pCutSet, 0, p->pPars->nCutsMax * sizeof(Dar_Cut_t) );
677 Dar_ObjSetCuts( pObj, pCutSet );
678 Dar_ObjForEachCutAll( pObj, pCut, i )
679 pCut->fUsed = 0;
680 Vec_PtrPush( p->vCutNodes, pObj );
681 // add unit cut if needed
682 pCut = pCutSet;
683 pCut->fUsed = 1;
684 if ( Aig_ObjIsConst1(pObj) )
685 {
686 pCut->nLeaves = 0;
687 pCut->uSign = 0;
688 pCut->uTruth = 0xFFFF;
689 }
690 else
691 {
692 pCut->nLeaves = 1;
693 pCut->pLeaves[0] = pObj->Id;
694 pCut->uSign = Aig_ObjCutSign( pObj->Id );
695 pCut->uTruth = 0xAAAA;
696 }
697 pCut->Value = Dar_CutFindValue( p, pCut );
698 if ( p->nCutMemUsed < Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) )
699 p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
700 return pCutSet;
701}
int Aig_MmFixedReadMemUsage(Aig_MmFixed_t *p)
Definition aigMem.c:271
char * Aig_MmFixedEntryFetch(Aig_MmFixed_t *p)
Definition aigMem.c:161
#define Dar_ObjForEachCutAll(pObj, pCut, i)
MACRO DEFINITIONS ///.
Definition darInt.h:119
unsigned nCuts
Definition aig.h:83
int pLeaves[4]
Definition darInt.h:63
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_Permutations()

char ** Dar_Permutations ( int n)
extern

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

Synopsis [Computes the set of all permutations.]

Description [The number of permutations in the array is n!. The number of entries in each permutation is n. Therefore, the resulting array is a two-dimentional array of the size: n! x n. To free the resulting array, call ABC_FREE() on the pointer returned by this procedure.]

SideEffects []

SeeAlso []

Definition at line 144 of file darPrec.c.

145{
146 char Array[50];
147 char ** pRes;
148 int nFact, i;
149 // allocate memory
150 nFact = Dar_Factorial( n );
151 pRes = Dar_ArrayAlloc( nFact, n, sizeof(char) );
152 // fill in the permutations
153 for ( i = 0; i < n; i++ )
154 Array[i] = i;
155 Dar_Permutations_rec( pRes, nFact, n, Array );
156 // print the permutations
157/*
158 {
159 int i, k;
160 for ( i = 0; i < nFact; i++ )
161 {
162 printf( "{" );
163 for ( k = 0; k < n; k++ )
164 printf( " %d", pRes[i][k] );
165 printf( " }\n" );
166 }
167 }
168*/
169 return pRes;
170}
void Dar_Permutations_rec(char **pRes, int nFact, int n, char Array[])
Definition darPrec.c:89
int Dar_Factorial(int n)
Definition darPrec.c:70
ABC_NAMESPACE_IMPL_START char ** Dar_ArrayAlloc(int nCols, int nRows, int Size)
DECLARATIONS ///.
Definition darPrec.c:45
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dar_Truth4VarNPN()

void Dar_Truth4VarNPN ( unsigned short ** puCanons,
char ** puPhases,
char ** puPerms,
unsigned char ** puMap )
extern

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

Synopsis [Computes NPN canonical forms for 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 293 of file darPrec.c.

294{
295 unsigned short * uCanons;
296 unsigned char * uMap;
297 unsigned uTruth, uPhase, uPerm;
298 char ** pPerms4, * uPhases, * uPerms;
299 int nFuncs, nClasses;
300 int i, k;
301
302 nFuncs = (1 << 16);
303 uCanons = ABC_CALLOC( unsigned short, nFuncs );
304 uPhases = ABC_CALLOC( char, nFuncs );
305 uPerms = ABC_CALLOC( char, nFuncs );
306 uMap = ABC_CALLOC( unsigned char, nFuncs );
307 pPerms4 = Dar_Permutations( 4 );
308
309 nClasses = 1;
310 nFuncs = (1 << 15);
311 for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ )
312 {
313 // skip already assigned
314 if ( uCanons[uTruth] )
315 {
316 assert( uTruth > uCanons[uTruth] );
317 uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]];
318 continue;
319 }
320 uMap[uTruth] = nClasses++;
321 for ( i = 0; i < 16; i++ )
322 {
323 uPhase = Dar_TruthPolarize( uTruth, i, 4 );
324 for ( k = 0; k < 24; k++ )
325 {
326 uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
327 if ( uCanons[uPerm] == 0 )
328 {
329 uCanons[uPerm] = uTruth;
330 uPhases[uPerm] = i;
331 uPerms[uPerm] = k;
332 uMap[uPerm] = uMap[uTruth];
333
334 uPerm = ~uPerm & 0xFFFF;
335 uCanons[uPerm] = uTruth;
336 uPhases[uPerm] = i | 16;
337 uPerms[uPerm] = k;
338 uMap[uPerm] = uMap[uTruth];
339 }
340 else
341 assert( uCanons[uPerm] == uTruth );
342 }
343 uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 );
344 for ( k = 0; k < 24; k++ )
345 {
346 uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 );
347 if ( uCanons[uPerm] == 0 )
348 {
349 uCanons[uPerm] = uTruth;
350 uPhases[uPerm] = i;
351 uPerms[uPerm] = k;
352 uMap[uPerm] = uMap[uTruth];
353
354 uPerm = ~uPerm & 0xFFFF;
355 uCanons[uPerm] = uTruth;
356 uPhases[uPerm] = i | 16;
357 uPerms[uPerm] = k;
358 uMap[uPerm] = uMap[uTruth];
359 }
360 else
361 assert( uCanons[uPerm] == uTruth );
362 }
363 }
364 }
365 for ( uTruth = 1; uTruth < 0xffff; uTruth++ )
366 assert( uMap[uTruth] != 0 );
367 uPhases[(1<<16)-1] = 16;
368 assert( nClasses == 222 );
369 ABC_FREE( pPerms4 );
370 if ( puCanons )
371 *puCanons = uCanons;
372 else
373 ABC_FREE( uCanons );
374 if ( puPhases )
375 *puPhases = uPhases;
376 else
377 ABC_FREE( uPhases );
378 if ( puPerms )
379 *puPerms = uPerms;
380 else
381 ABC_FREE( uPerms );
382 if ( puMap )
383 *puMap = uMap;
384 else
385 ABC_FREE( uMap );
386}
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
unsigned Dar_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
Definition darPrec.c:254
unsigned Dar_TruthPermute(unsigned Truth, char *pPerms, int nVars, int fReverse)
Definition darPrec.c:206
char ** Dar_Permutations(int n)
Definition darPrec.c:144
Here is the call graph for this function:
Here is the caller graph for this function: