summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h5
-rw-r--r--src/aig/gia/giaBalance.c70
-rw-r--r--src/aig/gia/giaUtil.c1
-rw-r--r--src/base/abci/abc.c164
-rw-r--r--src/sat/bmc/bmcBmcAnd.c3
5 files changed, 236 insertions, 7 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4d1e2f26..122e5025 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -937,6 +937,9 @@ extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFile
/*=== giaBalance.c ===========================================================*/
extern Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
extern Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
/*=== giaBidec.c ===========================================================*/
extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@@ -1062,6 +1065,8 @@ extern Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFram
/*=== giaFront.c ==========================================================*/
extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p );
extern void Gia_ManFrontTest( Gia_Man_t * p );
+/*=== giaFx.c ==========================================================*/
+extern Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
/*=== giaHash.c ===========================================================*/
extern void Gia_ManHashAlloc( Gia_Man_t * p );
extern void Gia_ManHashStart( Gia_Man_t * p );
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index d3bb8407..cae652e9 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -965,7 +965,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
pNew1 = Dam_ManAreaBalanceInt( pNew, vCiLevels, nNewNodesMax, fVerbose, fVeryVerbose );
if ( fVerbose ) Gia_ManPrintStats( pNew1, NULL );
Gia_ManStop( pNew );
- Vec_IntFree( vCiLevels );
+ Vec_IntFreeP( &vCiLevels );
// derive the final result
pNew2 = Gia_ManDupNoMuxes( pNew1 );
if ( fVerbose ) Gia_ManPrintStats( pNew2, NULL );
@@ -984,7 +984,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
SeeAlso []
***********************************************************************/
-Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
@@ -1003,6 +1003,72 @@ Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManStop( pTemp );
return pNew;
}
+Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Jf_Par_t Pars, * pPars = &Pars;
+ Jf_ManSetDefaultPars( pPars );
+ if ( fVerbose ) Gia_ManPrintStats( p, NULL );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ // perform mapping
+ pPars->nLutSize = 6;
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+// Gia_ManStop( pTemp );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ // perform mapping
+ pPars->nLutSize = 4;
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+// Gia_ManStop( pTemp );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Jf_Par_t Pars, * pPars = &Pars;
+ Jf_ManSetDefaultPars( pPars );
+ if ( fVerbose ) Gia_ManPrintStats( p, NULL );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ // perform mapping
+ pPars->nLutSize = 7;
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+// Gia_ManStop( pTemp );
+ // perform extraction
+ pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ // perform mapping
+ pPars->nLutSize = 5;
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+// Gia_ManStop( pTemp );
+ // perform extraction
+ pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 353edb86..08136e7d 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -535,6 +535,7 @@ int Gia_ManSetLevels( Gia_Man_t * p, Vec_Int_t * vCiLevels )
int i;
if ( vCiLevels == NULL )
return Gia_ManLevelNum( p );
+ assert( Vec_IntSize(vCiLevels) == Gia_ManCiNum(p) );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
p->nLevels = 0;
Gia_ManForEachCi( p, pObj, i )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 73ddcc97..21ace6d8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -352,6 +352,9 @@ static int Abc_CommandAbc9Bidec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Shrink ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fx ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -912,6 +915,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&shrink", Abc_CommandAbc9Shrink, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fx", Abc_CommandAbc9Fx, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&b", Abc_CommandAbc9Balance, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter", Abc_CommandAbc9Miter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter2", Abc_CommandAbc9Miter2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&append", Abc_CommandAbc9Append, 0 );
@@ -992,8 +998,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Dau_DsdTest();
}
-// if ( Sdm_ManCanRead() )
-// Sdm_ManRead();
+ if ( Sdm_ManCanRead() )
+ Sdm_ManRead();
}
/**Function*************************************************************
@@ -27442,7 +27448,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Fx( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
Gia_Man_t * pTemp;
int nNewNodesMax = 1000000;
int LitCountMax = 0;
@@ -27615,6 +27620,159 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Gia_Man_t * pTemp;
+ int c, fVerbose = 0;
+ int fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Syn2(): There is no AIG.\n" );
+ return 1;
+ }
+ pTemp = Gia_ManAigSyn2( pAbc->pGia, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &syn2 [-lvh]\n" );
+ Abc_Print( -2, "\t performs AIG optimization\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Syn3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Gia_Man_t * pTemp;
+ int c, fVerbose = 0;
+ int fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Syn3(): There is no AIG.\n" );
+ return 1;
+ }
+ pTemp = Gia_ManAigSyn3( pAbc->pGia, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &syn3 [-lvh]\n" );
+ Abc_Print( -2, "\t performs AIG optimization\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Syn4( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Gia_Man_t * pTemp;
+ int c, fVerbose = 0;
+ int fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Syn4(): There is no AIG.\n" );
+ return 1;
+ }
+ pTemp = Gia_ManAigSyn4( pAbc->pGia, fVerbose, fVeryVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &syn4 [-lvh]\n" );
+ Abc_Print( -2, "\t performs AIG optimization\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pFile;
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 38d19a61..1172227c 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -769,7 +769,6 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
- extern Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock();
@@ -784,7 +783,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fUseSynth )
{
Gia_Man_t * pTemp = p->pFrames;
- p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
+ p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-10 15:44:05 +0000