summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abci/abc.c352
-rw-r--r--src/base/abci/abcDar.c471
-rw-r--r--src/base/abci/abcPart.c143
-rw-r--r--src/base/abci/abcRewrite.c7
-rw-r--r--src/base/abci/abcSat.c4
-rw-r--r--src/base/abci/abcStrash.c3
-rw-r--r--src/base/abci/abcTiming.c8
-rw-r--r--src/base/abci/abcVerify.c2
9 files changed, 824 insertions, 167 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index faa2fe2e..bda8781c 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -234,6 +234,7 @@ struct Abc_Lib_t_
// maximum/minimum operators
#define ABC_MIN(a,b) (((a) < (b))? (a) : (b))
#define ABC_MAX(a,b) (((a) > (b))? (a) : (b))
+#define ABC_ABS(a) (((a) >= 0)? (a) :-(a))
#define ABC_INFINITY (100000000)
// transforming floats into ints and back
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6b32cd43..1dd9b65e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -92,6 +92,7 @@ static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -113,6 +114,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -169,6 +171,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -252,6 +255,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 );
Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
@@ -273,6 +277,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
@@ -329,6 +334,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
@@ -5032,6 +5038,95 @@ usage:
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandTopmost( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c, nLevels;
+ extern Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nLevels = 10;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLevels = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLevels < 0 )
+ goto usage;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ {
+ fprintf( stdout, "Currently can only works for combinational circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "Currently expects a single-output miter.\n" );
+ return 0;
+ }
+
+ pNtkRes = Abc_NtkTopmost( pNtk, nLevels );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "The command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: topmost [-N num] [-h]\n" );
+ fprintf( pErr, "\t replaces the current network by several of its topmost levels\n" );
+ fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\tname : the node name\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -6098,9 +6193,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Network should be strashed. Command has failed.\n" );
return 1;
}
- pNtkRes = Abc_NtkDar( pNtk );
-// pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
- pNtkRes = NULL;
+// pNtkRes = Abc_NtkDar( pNtk );
+ pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
+// pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -6635,7 +6730,7 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Dar_ManDefaultRwrParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CNflzvwh" ) ) != EOF )
{
switch ( c )
{
@@ -6661,6 +6756,9 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nSubgMax < 0 )
goto usage;
break;
+ case 'f':
+ pPars->fFanout ^= 1;
+ break;
case 'l':
pPars->fUpdateLevel ^= 1;
break;
@@ -6695,10 +6793,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" );
+ fprintf( pErr, "usage: drw [-C num] [-N num] [-flzvwh]\n" );
fprintf( pErr, "\t performs combinational AIG rewriting\n" );
fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax );
fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+ fprintf( pErr, "\t-f : toggle representing fanouts [default = %s]\n", pPars->fFanout? "yes": "no" );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -6842,21 +6941,29 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int fVerbose, c;
+ int fBalance, fVerbose, fUpdateLevel, c;
- extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fBalance = 0;
fVerbose = 0;
+ fUpdateLevel = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
{
switch ( c )
{
+ case 'b':
+ fBalance ^= 1;
+ break;
+ case 'l':
+ fUpdateLevel ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -6871,7 +6978,7 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- pNtkRes = Abc_NtkDCompress2( pNtk, fVerbose );
+ pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -6882,8 +6989,77 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dcompress2 [-vh]\n" );
+ fprintf( pErr, "usage: dcompress2 [-blvh]\n" );
fprintf( pErr, "\t performs combinational AIG optimization\n" );
+ 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" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int fBalance, fVerbose, c;
+
+ extern Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fBalance = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'b':
+ fBalance ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: drwsat [-bvh]\n" );
+ fprintf( pErr, "\t performs combinational AIG optimization for SAT\n" );
+ fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -7212,10 +7388,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int c, fProve, fVerbose, fDoSparse, fSpeculate;
- int nConfLimit;
+ int c, nConfLimit, fDoSparse, fProve, fSpeculate, fChoicing, fVerbose;
- extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -7223,12 +7398,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nConfLimit = 100;
- fSpeculate = 0;
fDoSparse = 1;
fProve = 0;
+ fSpeculate = 0;
+ fChoicing = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Csprcvh" ) ) != EOF )
{
switch ( c )
{
@@ -7252,6 +7428,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'r':
fSpeculate ^= 1;
break;
+ case 'c':
+ fChoicing ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -7267,7 +7446,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose );
+ pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -7278,12 +7457,13 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dfraig [-C num] [-sprvh]\n" );
+ fprintf( pErr, "usage: dfraig [-C num] [-sprcvh]\n" );
fprintf( pErr, "\t performs fraiging using a new method\n" );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
fprintf( pErr, "\t-r : toggle speculative reduction [default = %s]\n", fSpeculate? "yes": "no" );
+ fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", fChoicing? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -7836,7 +8016,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fFuncRed = 1; // performs only one level hashing
pParams->fFeedBack = 1; // enables solver feedback
pParams->fDist1Pats = 1; // enables distance-1 patterns
- pParams->fDoSparse = 0; // performs equiv tests for sparse functions
+ pParams->fDoSparse = 1; // performs equiv tests for sparse functions
pParams->fChoicing = 0; // enables recording structural choices
pParams->fTryProve = 0; // tries to solve the final miter
pParams->fVerbose = 0; // the verbosiness flag
@@ -11327,6 +11507,142 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int RetValue;
+ int fVerbose;
+ int nConfLimit;
+ int nInsLimit;
+ int clk;
+
+ extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose );
+
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ nConfLimit = 100000;
+ nInsLimit = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nConfLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nConfLimit < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nInsLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nInsLimit < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkLatchNum(pNtk) > 0 )
+ {
+ fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ {
+ fprintf( stdout, "Currently expects a single-output miter.\n" );
+ return 0;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+
+ clk = clock();
+ RetValue = Abc_NtkDSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fVerbose );
+ // verify that the pattern is correct
+ if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
+ {
+ //int i;
+ //Abc_Obj_t * pObj;
+ int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
+ if ( pSimInfo[0] != 1 )
+ printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
+ free( pSimInfo );
+ /*
+ // print model
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ printf( "%d", (int)(pNtk->pModel[i] > 0) );
+ if ( i == 70 )
+ break;
+ }
+ printf( "\n" );
+ */
+ }
+
+ if ( RetValue == -1 )
+ printf( "UNDECIDED " );
+ else if ( RetValue == 0 )
+ printf( "SATISFIABLE " );
+ else
+ printf( "UNSATISFIABLE " );
+ //printf( "\n" );
+ PRT( "Time", clock() - clk );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dsat [-C num] [-I num] [-vh]\n" );
+ fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
+ fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" );
+ fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+ fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index bc47e2dc..f04f3d97 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -123,6 +123,69 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Aig_Obj_t * pObj, * pTemp;
+ int i;
+ assert( pMan->pReprs != NULL );
+ assert( Aig_ManBufNum(pMan) == 0 );
+ // perform strashing
+ pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+ Aig_ManForEachPi( pMan, pObj, i )
+ pObj->pData = Abc_NtkCi(pNtkNew, i);
+ // rebuild the AIG
+ vNodes = Aig_ManDfsChoices( pMan );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
+ if ( pTemp = pMan->pReprs[pObj->Id] )
+ {
+ Abc_Obj_t * pAbcRepr, * pAbcObj;
+ assert( pTemp->pData != NULL );
+ pAbcRepr = pObj->pData;
+ pAbcObj = pTemp->pData;
+ pAbcObj->pData = pAbcRepr->pData;
+ pAbcRepr->pData = pAbcObj;
+ }
+ }
+printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) );
+ Vec_PtrFree( vNodes );
+/*
+ {
+ Abc_Obj_t * pNode;
+ int k, Counter = 0;
+ Abc_NtkForEachNode( pNtkNew, pNode, k )
+ if ( pNode->pData != 0 )
+ {
+ int x = 0;
+ Counter++;
+ }
+ printf( "Choices = %d.\n", Counter );
+ }
+*/
+ // connect the PO nodes
+ Aig_ManForEachPo( pMan, pObj, i )
+ Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
{
Vec_Ptr_t * vNodes;
@@ -291,7 +354,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
*/
// Aig_ManDumpBlif( pMan, "aig_temp.blif" );
-// pMan->pPars = Dar_ManDefaultRwrParams();
+// pMan->pPars = Dar_ManDefaultRwrPars();
Dar_ManRewrite( pMan, NULL );
Aig_ManPrintStats( pMan );
// Dar_ManComputeCuts( pMan );
@@ -336,120 +399,31 @@ Aig_CnfFree( pCnf );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fChoicing, int fVerbose )
{
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pNode, * pNodeNew;
- Aig_Obj_t * pObj, * pLeaf;
- Cnf_Cut_t * pCut;
- Vec_Int_t * vCover;
- unsigned uTruth;
- int i, k, nDupGates;
- // create the new network
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
- // make the mapper point to the new network
- Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
- Abc_NtkForEachCi( pNtk, pNode, i )
- Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
- // process the nodes in topological order
- vCover = Vec_IntAlloc( 1 << 16 );
- Vec_PtrForEachEntry( vMapped, pObj, i )
- {
- // create new node
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- // add fanins according to the cut
- pCut = pObj->pData;
- Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
- Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
- // add logic function
- if ( pCut->nFanins < 5 )
- {
- uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
- Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
- pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
- }
- else
- pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
- // save the node
- pObj->pData = pNodeNew;
- }
- Vec_IntFree( vCover );
- // add the CO drivers
- Abc_NtkForEachCo( pNtk, pNode, i )
- {
- pObj = Aig_ManPo(p->pManAig, i);
- pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
- Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
- }
-
- // remove the constant node if not used
- pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
- if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
- Abc_NtkDeleteObj( pNodeNew );
- // minimize the node
-// Abc_NtkSweep( pNtkNew, 0 );
- // decouple the PO driver nodes to reduce the number of levels
- nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-// if ( nDupGates && If_ManReadVerbose(pIfMan) )
-// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
- if ( !Abc_NtkCheck( pNtkNew ) )
- fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
- return pNtkNew;
-}
-
-/**Function*************************************************************
-
- Synopsis [Gives the current ABC network to AIG manager for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
-{
- Abc_Ntk_t * pNtkNew = NULL;
- Cnf_Man_t * pCnf;
- Aig_Man_t * pMan;
- Cnf_Dat_t * pData;
- assert( Abc_NtkIsStrash(pNtk) );
- // convert to the AIG manager
+ Fra_Par_t Pars, * pPars = &Pars;
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
- if ( !Aig_ManCheck( pMan ) )
- {
- printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
- Aig_ManStop( pMan );
- return NULL;
- }
- // perform balance
- Aig_ManPrintStats( pMan );
-
- // derive CNF
- pCnf = Cnf_ManStart();
- pData = Cnf_Derive( pCnf, pMan );
-
- {
- Vec_Ptr_t * vMapped;
- vMapped = Cnf_ManScanMapping( pCnf, 1 );
- pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped );
- Vec_PtrFree( vMapped );
- }
-
+ Fra_ParamsDefault( pPars );
+ pPars->nBTLimitNode = nConfLimit;
+ pPars->fVerbose = fVerbose;
+ pPars->fProve = fProve;
+ pPars->fDoSparse = fDoSparse;
+ pPars->fSpeculate = fSpeculate;
+ pPars->fChoicing = fChoicing;
+ pMan = Fra_Perform( pTemp = pMan, pPars );
+ if ( fChoicing )
+ pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
+ else
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Aig_ManStop( pTemp );
Aig_ManStop( pMan );
- Cnf_ManStop( pCnf );
-
- // write CNF into a file
-// Cnf_DataWriteIntoFile( pData, pFileName );
- Cnf_DataFree( pData );
-
- return pNtkNew;
+ return pNtkAig;
}
-
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@@ -461,21 +435,15 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose )
+Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
{
- Fra_Par_t Params, * pParams = &Params;
+ extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
- Fra_ParamsDefault( pParams );
- pParams->nBTLimitNode = nConfLimit;
- pParams->fVerbose = fVerbose;
- pParams->fProve = fProve;
- pParams->fDoSparse = fDoSparse;
- pParams->fSpeculate = fSpeculate;
- pMan = Fra_Perform( pTemp = pMan, pParams );
+ pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pTemp );
Aig_ManStop( pMan );
@@ -493,17 +461,35 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
{
- extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
- Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
+ Abc_Ntk_t * pNtkAig;
+ int clk;
+ assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
- pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
- pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+// Aig_ManPrintStats( pMan );
+
+// Aig_ManSupports( pMan );
+ {
+ Vec_Vec_t * vParts;
+ vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
+ Vec_VecFree( vParts );
+ }
+
+ Dar_ManRewrite( pMan, pPars );
+// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+// Aig_ManStop( pTemp );
+
+clk = clock();
+ pMan = Aig_ManDup( pTemp = pMan, 0 );
Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+// Aig_ManPrintStats( pMan );
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -519,7 +505,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
+Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -530,7 +516,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
return NULL;
// Aig_ManPrintStats( pMan );
- Dar_ManRewrite( pMan, pPars );
+ Dar_ManRefactor( pMan, pPars );
// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
// Aig_ManStop( pTemp );
@@ -556,9 +542,9 @@ clk = clock();
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
+Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
{
- Aig_Man_t * pMan, * pTemp;
+ Aig_Man_t * pMan;//, * pTemp;
Abc_Ntk_t * pNtkAig;
int clk;
assert( Abc_NtkIsStrash(pNtk) );
@@ -567,13 +553,9 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
return NULL;
// Aig_ManPrintStats( pMan );
- Dar_ManRefactor( pMan, pPars );
-// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
-// Aig_ManStop( pTemp );
-
clk = clock();
- pMan = Aig_ManDup( pTemp = pMan, 0 );
- Aig_ManStop( pTemp );
+ pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose );
+// Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
// Aig_ManPrintStats( pMan );
@@ -593,7 +575,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
{
Aig_Man_t * pMan;//, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -605,7 +587,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose )
// Aig_ManPrintStats( pMan );
clk = clock();
- pMan = Dar_ManCompress2( pMan, fVerbose );
+ pMan = Dar_ManRwsat( pMan, fBalance, fVerbose );
// Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
@@ -615,6 +597,227 @@ clk = clock();
return pNtkAig;
}
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped )
+{
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pNode, * pNodeNew;
+ Aig_Obj_t * pObj, * pLeaf;
+ Cnf_Cut_t * pCut;
+ Vec_Int_t * vCover;
+ unsigned uTruth;
+ int i, k, nDupGates;
+ // create the new network
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
+ // make the mapper point to the new network
+ Aig_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew);
+ Abc_NtkForEachCi( pNtk, pNode, i )
+ Aig_ManPi(p->pManAig, i)->pData = pNode->pCopy;
+ // process the nodes in topological order
+ vCover = Vec_IntAlloc( 1 << 16 );
+ Vec_PtrForEachEntry( vMapped, pObj, i )
+ {
+ // create new node
+ pNodeNew = Abc_NtkCreateNode( pNtkNew );
+ // add fanins according to the cut
+ pCut = pObj->pData;
+ Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k )
+ Abc_ObjAddFanin( pNodeNew, pLeaf->pData );
+ // add logic function
+ if ( pCut->nFanins < 5 )
+ {
+ uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
+ Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
+ pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover );
+ }
+ else
+ pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+ // save the node
+ pObj->pData = pNodeNew;
+ }
+ Vec_IntFree( vCover );
+ // add the CO drivers
+ Abc_NtkForEachCo( pNtk, pNode, i )
+ {
+ pObj = Aig_ManPo(p->pManAig, i);
+ pNodeNew = Abc_ObjNotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+ Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+ }
+
+ // remove the constant node if not used
+ pNodeNew = (Abc_Obj_t *)Aig_ManConst1(p->pManAig)->pData;
+ if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
+ Abc_NtkDeleteObj( pNodeNew );
+ // minimize the node
+// Abc_NtkSweep( pNtkNew, 0 );
+ // decouple the PO driver nodes to reduce the number of levels
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+// if ( nDupGates && If_ManReadVerbose(pIfMan) )
+// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ Vec_Ptr_t * vMapped;
+ Aig_Man_t * pMan;
+ Cnf_Man_t * pManCnf;
+ Cnf_Dat_t * pCnf;
+ Abc_Ntk_t * pNtkNew = NULL;
+ assert( Abc_NtkIsStrash(pNtk) );
+
+ // convert to the AIG manager
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+ if ( !Aig_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkDarToCnf: AIG check has failed.\n" );
+ Aig_ManStop( pMan );
+ return NULL;
+ }
+ // perform balance
+ Aig_ManPrintStats( pMan );
+
+ // derive CNF
+ pCnf = Cnf_Derive( pMan );
+ pManCnf = Cnf_ManRead();
+
+ // write the network for verification
+ vMapped = Cnf_ManScanMapping( pManCnf, 1, 0 );
+ pNtkNew = Abc_NtkConstructFromCnf( pNtk, pManCnf, vMapped );
+ Vec_PtrFree( vMapped );
+
+ // write CNF into a file
+ Cnf_DataWriteIntoFile( pCnf, pFileName );
+ Cnf_DataFree( pCnf );
+ Cnf_ClearMemory();
+
+ Aig_ManStop( pMan );
+ return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Solves combinational miter using a SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVerbose )
+{
+ sat_solver * pSat;
+ Aig_Man_t * pMan;
+ Cnf_Dat_t * pCnf;
+ int status, RetValue, clk = clock();
+ Vec_Int_t * vCiIds;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ assert( Abc_NtkLatchNum(pNtk) == 0 );
+ assert( Abc_NtkPoNum(pNtk) == 1 );
+
+ // conver to the manager
+ pMan = Abc_NtkToDar( pNtk );
+ // derive CNF
+ pCnf = Cnf_Derive( pMan );
+ // convert into the SAT solver
+ pSat = Cnf_DataWriteIntoSolver( pCnf );
+ vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+ Aig_ManStop( pMan );
+ Cnf_DataFree( pCnf );
+ // solve SAT
+ if ( pSat == NULL )
+ {
+ Vec_IntFree( vCiIds );
+// printf( "Trivially unsat\n" );
+ return 1;
+ }
+
+
+// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+ PRT( "Time", clock() - clk );
+
+ // simplify the problem
+ clk = clock();
+ status = sat_solver_simplify(pSat);
+// printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
+// PRT( "Time", clock() - clk );
+ if ( status == 0 )
+ {
+ Vec_IntFree( vCiIds );
+ sat_solver_delete( pSat );
+// printf( "The problem is UNSATISFIABLE after simplification.\n" );
+ return 1;
+ }
+
+ // solve the miter
+ clk = clock();
+ if ( fVerbose )
+ pSat->verbosity = 1;
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit, (sint64)0, (sint64)0 );
+ if ( status == l_Undef )
+ {
+// printf( "The problem timed out.\n" );
+ RetValue = -1;
+ }
+ else if ( status == l_True )
+ {
+// printf( "The problem is SATISFIABLE.\n" );
+ RetValue = 0;
+ }
+ else if ( status == l_False )
+ {
+// printf( "The problem is UNSATISFIABLE.\n" );
+ RetValue = 1;
+ }
+ else
+ assert( 0 );
+// PRT( "SAT sat_solver time", clock() - clk );
+// printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
+
+ // if the problem is SAT, get the counterexample
+ if ( status == l_True )
+ {
+ pNtk->pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+ }
+ // free the sat_solver
+ if ( fVerbose )
+ Sat_SolverPrintStats( stdout, pSat );
+//sat_solver_store_write( pSat, "trace.cnf" );
+//sat_solver_store_free( pSat );
+ sat_solver_delete( pSat );
+ Vec_IntFree( vCiIds );
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 787e3f88..f0989b23 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -45,13 +45,17 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
Vec_Int_t * vSuppI;
Abc_Obj_t * pObj, * pTemp;
int i, k;
+ // set the PI numbers
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->pCopy = (void *)i;
+ // save hte CI numbers
vSupports = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pObj, i )
{
vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
vSuppI = (Vec_Int_t *)vSupp;
Vec_PtrForEachEntry( vSupp, pTemp, k )
- Vec_IntWriteEntry( vSuppI, k, pTemp->Id );
+ Vec_IntWriteEntry( vSuppI, k, (int)pTemp->pCopy );
Vec_IntSort( vSuppI, 0 );
// append the number of this output
Vec_IntPush( vSuppI, i );
@@ -65,6 +69,71 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Start char-bases support representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Abc_NtkSuppCharStart( Vec_Int_t * vOne, int nPis )
+{
+ char * pBuffer;
+ int i, Entry;
+ pBuffer = ALLOC( char, nPis );
+ memset( pBuffer, 0, sizeof(char) * nPis );
+ Vec_IntForEachEntry( vOne, Entry, i )
+ {
+ assert( Entry < nPis );
+ pBuffer[Entry] = 1;
+ }
+ return pBuffer;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Add to char-bases support representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkSuppCharAdd( char * pBuffer, Vec_Int_t * vOne, int nPis )
+{
+ int i, Entry;
+ Vec_IntForEachEntry( vOne, Entry, i )
+ {
+ assert( Entry < nPis );
+ pBuffer[Entry] = 1;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find the common variables using char-bases support representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkSuppCharCommon( char * pBuffer, Vec_Int_t * vOne )
+{
+ int i, Entry, nCommon = 0;
+ Vec_IntForEachEntry( vOne, Entry, i )
+ nCommon += pBuffer[Entry];
+ return nCommon;
+}
+
+/**Function*************************************************************
+
Synopsis [Find the best partition.]
Description []
@@ -74,8 +143,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne )
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsChar, int nPartSizeLimit, Vec_Int_t * vOne )
{
+/*
Vec_Int_t * vPartSupp, * vPart;
double Attract, Repulse, Cost, CostBest;
int i, nCommon, iBest;
@@ -83,12 +153,12 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
CostBest = 0.0;
Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
{
+ vPart = Vec_PtrEntry( vPartsAll, i );
+ if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit )
+ continue;
nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
if ( nCommon == 0 )
continue;
- vPart = Vec_PtrEntry( vPartsAll, i );
- if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit )
- continue;
if ( nCommon == Vec_IntSize(vOne) )
return i;
Attract = 1.0 * nCommon / Vec_IntSize(vOne);
@@ -106,6 +176,41 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
if ( CostBest < 0.6 )
return -1;
return iBest;
+*/
+
+ Vec_Int_t * vPartSupp, * vPart;
+ int Attract, Repulse, Value, ValueBest;
+ int i, nCommon, iBest;
+// int nCommon2;
+ iBest = -1;
+ ValueBest = 0;
+ Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
+ {
+ vPart = Vec_PtrEntry( vPartsAll, i );
+ if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) >= nPartSizeLimit )
+ continue;
+// nCommon2 = Vec_IntTwoCountCommon( vPartSupp, vOne );
+ nCommon = Abc_NtkSuppCharCommon( Vec_PtrEntry(vPartSuppsChar, i), vOne );
+// assert( nCommon2 == nCommon );
+ if ( nCommon == 0 )
+ continue;
+ if ( nCommon == Vec_IntSize(vOne) )
+ return i;
+ Attract = 1000 * nCommon / Vec_IntSize(vOne);
+ if ( Vec_IntSize(vPartSupp) < 100 )
+ Repulse = 1;
+ else
+ Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100);
+ Value = Attract/Repulse;
+ if ( ValueBest < Value )
+ {
+ ValueBest = Value;
+ iBest = i;
+ }
+ }
+ if ( ValueBest < 75 )
+ return -1;
+ return iBest;
}
/**Function*************************************************************
@@ -222,9 +327,10 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
***********************************************************************/
Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose )
{
+ Vec_Ptr_t * vPartSuppsChar;
Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
- int i, iPart, iOut, clk;
+ int i, iPart, iOut, clk, clk2, timeFind = 0;
// compute the supports for all outputs
clk = clock();
@@ -233,6 +339,8 @@ if ( fVerbose )
{
PRT( "Supps", clock() - clk );
}
+ // start char-based support representation
+ vPartSuppsChar = Vec_PtrAlloc( 1000 );
// create partitions
clk = clock();
@@ -243,7 +351,10 @@ clk = clock();
// get the output number
iOut = Vec_IntPop(vOne);
// find closely matching part
- iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne );
+clk2 = clock();
+ iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, vPartSuppsChar, nPartSizeLimit, vOne );
+timeFind += clock() - clk2;
+//printf( "%4d->%4d ", i, iPart );
if ( iPart == -1 )
{
// create new partition
@@ -254,6 +365,8 @@ clk = clock();
// add this partition and its support
Vec_PtrPush( vPartsAll, vPart );
Vec_PtrPush( vPartSuppsAll, vPartSupp );
+
+ Vec_PtrPush( vPartSuppsChar, Abc_NtkSuppCharStart(vOne, Abc_NtkPiNum(pNtk)) );
}
else
{
@@ -266,11 +379,21 @@ clk = clock();
Vec_IntFree( vTemp );
// reinsert new support
Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
+
+ Abc_NtkSuppCharAdd( Vec_PtrEntry(vPartSuppsChar, iPart), vOne, Abc_NtkPiNum(pNtk) );
}
}
+
+ // stop char-based support representation
+ Vec_PtrForEachEntry( vPartSuppsChar, vTemp, i )
+ free( vTemp );
+ Vec_PtrFree( vPartSuppsChar );
+
+//printf( "\n" );
if ( fVerbose )
{
PRT( "Parts", clock() - clk );
+//PRT( "Find ", timeFind );
}
clk = clock();
@@ -290,7 +413,9 @@ clk = clock();
// Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
if ( fVerbose )
- Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
+// Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
+ printf( "Created %d partitions.\n", Vec_PtrSize(vPartsAll) );
+
if ( fVerbose )
{
PRT( "Comps", clock() - clk );
@@ -676,7 +801,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
// perform partitioning
assert( Abc_NtkIsStrash(pNtk) );
// vParts = Abc_NtkPartitionNaive( pNtk, 20 );
- vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
+ vParts = Abc_NtkPartitionSmart( pNtk, 0, 1 );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index cbbea1be..2376b72c 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -70,6 +70,13 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
// cleanup the AIG
Abc_AigCleanup(pNtk->pManFunc);
+ {
+ Vec_Vec_t * vParts;
+ vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 );
+ Vec_VecFree( vParts );
+ }
+
+
// start placement package
if ( fPlaceEnable )
{
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index d9cae254..aafa6530 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -49,7 +49,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
sat_solver * pSat;
lbool status;
int RetValue, clk;
-
+
if ( pNumConfs )
*pNumConfs = 0;
if ( pNumInspects )
@@ -70,7 +70,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
//return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
-// PRT( "Time", clock() - clk );
+ PRT( "Time", clock() - clk );
// simplify the problem
clk = clock();
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index b1a0dc5b..978b7cdb 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -351,7 +351,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int fReco
***********************************************************************/
Abc_Obj_t * Abc_NtkTopmost_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int LevelCut )
{
- assert( Abc_ObjIsComplement(pNode) );
+ assert( !Abc_ObjIsComplement(pNode) );
if ( pNode->pCopy )
return pNode->pCopy;
if ( pNode->Level <= (unsigned)LevelCut )
@@ -388,6 +388,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels )
// create PIs below the cut and nodes above the cut
Abc_NtkCleanCopy( pNtk );
pObjNew = Abc_NtkTopmost_rec( pNtkNew, Abc_ObjFanin0(Abc_NtkPo(pNtk, 0)), LevelCut );
+ pObjNew = Abc_ObjNotCond( pObjNew, Abc_ObjFaninC0(Abc_NtkPo(pNtk, 0)) );
// add the PO node and name
pPoNew = Abc_NtkCreatePo(pNtkNew);
Abc_ObjAddFanin( pPoNew, pObjNew );
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 5d5e6e93..967e4617 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -819,6 +819,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
{
+ assert( Abc_ObjLevel(pFanout) >= Lev );
Vec_VecPush( vLevels, Abc_ObjLevel(pFanout), pFanout );
pFanout->fMarkA = 1;
}
@@ -840,7 +841,7 @@ void Abc_NtkUpdateLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pFanin, * pTemp;
- int LevelOld, Lev, k, m;
+ int LevelOld, LevFanin, Lev, k, m;
// check if level has changed
LevelOld = Abc_ObjReverseLevel(pObjNew);
if ( LevelOld == Abc_ObjReverseLevelNew(pObjNew) )
@@ -866,7 +867,9 @@ void Abc_NtkUpdateReverseLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
if ( !Abc_ObjIsCi(pFanin) && !pFanin->fMarkA )
{
- Vec_VecPush( vLevels, Abc_ObjReverseLevel(pFanin), pFanin );
+ LevFanin = Abc_ObjReverseLevel( pFanin );
+ assert( LevFanin >= Lev );
+ Vec_VecPush( vLevels, LevFanin, pFanin );
pFanin->fMarkA = 1;
}
}
@@ -891,6 +894,7 @@ void Abc_NtkUpdate( Abc_Obj_t * pObj, Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
Abc_ObjReplace( pObj, pObjNew );
// update the level of the node
Abc_NtkUpdateLevel( pObjNew, vLevels );
+ Abc_ObjSetReverseLevel( pObjNew, 0 );
Abc_NtkUpdateReverseLevel( pObjNew, vLevels );
}
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 6ab2c552..63ba4843 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -368,7 +368,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
// partition the outputs
- vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 );
+ vParts = Abc_NtkPartitionSmart( pMiter, 50, 1 );
// fraig each partition
Status = 1;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 03:32:11 +0000