summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h2
-rw-r--r--src/aig/aig/aigPart.c6
-rw-r--r--src/aig/aig/aigRepr.c2
-rw-r--r--src/aig/dar/dar.h2
-rw-r--r--src/aig/dar/darScript.c4
-rw-r--r--src/aig/fra/fra.h3
-rw-r--r--src/aig/fra/fraCore.c12
-rw-r--r--src/aig/fra/fraSec.c4
-rw-r--r--src/aig/ivy/ivyFraig.c6
-rw-r--r--src/base/abci/abc.c35
-rw-r--r--src/base/abci/abcDar.c4
11 files changed, 58 insertions, 22 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1124c2fb..9d9bf22a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -522,7 +522,7 @@ extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
-extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose );
+extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index edf51a2e..9afc5f91 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -904,11 +904,11 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
SeeAlso []
***********************************************************************/
-Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose )
+Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose )
{
// extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
// extern void * Abc_FrameGetGlobalFrame();
- extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
+ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
Vec_Ptr_t * vOutsTotal, * vOuts;
Aig_Man_t * pAigTotal, * pAigPart, * pAig;
@@ -972,7 +972,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVer
i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart),
Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
// compute equivalence classes (to be stored in pNew->pReprs)
- pAig = Fra_FraigChoice( pAigPart, 1000 );
+ pAig = Fra_FraigChoice( pAigPart, nConfMax, nLevelMax );
Aig_ManStop( pAig );
// reset the pData pointers
Aig_ManForEachObj( pAigPart, pObj, k )
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 5ee6c9af..3a7e382c 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -429,7 +429,6 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
pRepr = Aig_ObjFindRepr( p, pObj );
if ( pRepr == NULL )
continue;
- assert( pObj->nRefs == 0 );
// skip constant and PI classes
if ( !Aig_ObjIsNode(pRepr) )
{
@@ -444,6 +443,7 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
}
//printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
// add choice to the choice node
+ assert( pObj->nRefs == 0 );
p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
p->pEquivs[pRepr->Id] = pObj;
}
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 72e7d3d1..c4c7db0a 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -92,7 +92,7 @@ extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig );
extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
-extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
#ifdef __cplusplus
}
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 530e913e..e690a61b 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -353,7 +353,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
SeeAlso []
***********************************************************************/
-Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Vec_Ptr_t * vAigs;
@@ -374,7 +374,7 @@ if ( fVerbose )
PRT( "Synthesis time", clock() - clk );
}
clk = clock();
- pMan = Aig_ManChoicePartitioned( vAigs, 300, fVerbose );
+ pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
Vec_PtrForEachEntry( vAigs, pTemp, i )
Aig_ManStop( pTemp );
Vec_PtrFree( vAigs );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 64268358..2ee84f39 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
int fConeBias; // bias variables in the cone (good for unsat runs)
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
+ int nLevelMax; // the max level to consider seriously
int nFramesP; // the number of timeframes to in the prefix
int nFramesK; // the number of timeframes to unroll
int nMaxImps; // the maximum number of implications to consider
@@ -266,7 +267,7 @@ extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
+extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraHot.c ========================================================*/
extern Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0157421b..0a81105b 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -303,6 +303,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
// Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i, Pos = 0;
+ int nBTracksOld;
// fraig latch outputs
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
{
@@ -315,6 +316,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
// fraig internal nodes
// if ( !p->pPars->fDontShowBar )
// pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
+ nBTracksOld = p->pPars->nBTLimitNode;
Aig_ManForEachNode( p->pManAig, pObj, i )
{
// if ( pProgress )
@@ -327,7 +329,12 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pManFraig->pData )
continue;
// perform fraiging
+ if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+ p->pPars->nBTLimitNode = 5;
Fra_FraigNode( p, pObj );
+ if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+ p->pPars->nBTLimitNode = nBTracksOld;
+ // check implications
if ( p->pPars->fUseImps )
Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
}
@@ -382,7 +389,7 @@ clk = clock();
// finalize the fraiged manager
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
- {
+ {
int clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
@@ -419,7 +426,7 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
@@ -430,6 +437,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
pPars->fProve = 0;
pPars->fVerbose = 0;
pPars->fDontShowBar = 1;
+ pPars->nLevelMax = nLevelMax;
return Fra_FraigPerform( pManAig, pPars );
}
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 3e0fca6a..a43d83b1 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -211,8 +211,8 @@ PRT( "Time", clock() - clk );
}
// perform retiming
-// if ( fRetimeFirst && pNew->nRegs )
- if ( pNew->nRegs )
+ if ( fRetimeFirst && pNew->nRegs )
+// if ( pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 4079b6ed..46dddab2 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2009,9 +2009,9 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
(!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
{
- assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
- assert( pObjNew != Ivy_Regular(pFanin0New) );
- assert( pObjNew != Ivy_Regular(pFanin1New) );
+// assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
+// assert( pObjNew != Ivy_Regular(pFanin0New) );
+// assert( pObjNew != Ivy_Regular(pFanin1New) );
return pObjNew;
}
// get the fraiged representative
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4b872aa3..31c09fd2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7675,8 +7675,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int fBalance, fVerbose, fUpdateLevel, c;
+ int nConfMax, nLevelMax;
- extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -7685,12 +7686,36 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fBalance = 1;
fUpdateLevel = 1;
+ nConfMax = 1000;
+ nLevelMax = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF )
{
switch ( c )
{
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfMax < 0 )
+ goto usage;
+ break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLevelMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLevelMax < 0 )
+ goto usage;
+ break;
case 'b':
fBalance ^= 1;
break;
@@ -7716,7 +7741,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
- pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
+ pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -7727,8 +7752,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dchoice [-blvh]\n" );
+ fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" );
fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" );
+ fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d703cfc4..6c5cabce 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -720,7 +720,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -728,7 +728,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
pMan = Abc_NtkToDar( pNtk, 0 );
if ( pMan == NULL )
return NULL;
- pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+ pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
Aig_ManStop( pMan );
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-27 23:12:31 +0000