diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 9 | ||||
-rw-r--r-- | src/base/abci/abcDarUnfold2.c | 2 | ||||
-rw-r--r-- | src/base/abci/abciUnfold2.c | 67 |
3 files changed, 72 insertions, 6 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 63cc04b8..37d0a014 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -294,8 +294,9 @@ static int Abc_CommandTempor ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandInduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUnfold2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandFold2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSaucy ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -871,9 +872,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "ind", Abc_CommandInduction, 0 ); Cmd_CommandAdd( pAbc, "Verification", "constr", Abc_CommandConstr, 0 ); Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); - - Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "unfold2", Abc_CommandUnfold2, 1 ); // jlong + Cmd_CommandAdd( pAbc, "Verification", "fold2", Abc_CommandFold2, 1 ); // jlong Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm2", Abc_CommandBm2, 1 ); Cmd_CommandAdd( pAbc, "Verification", "saucy3", Abc_CommandSaucy, 1 ); @@ -35350,5 +35351,5 @@ usage: /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -#include "abciUnfold2.c" + ABC_NAMESPACE_IMPL_END diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c index bacda407..7ebc316c 100644 --- a/src/base/abci/abcDarUnfold2.c +++ b/src/base/abci/abcDarUnfold2.c @@ -32,7 +32,7 @@ Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nP pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec); Aig_ManStop( pMan ); - return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt); + return pNtkAig;//Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt); //return pNtkAig; } diff --git a/src/base/abci/abciUnfold2.c b/src/base/abci/abciUnfold2.c index ec5047d2..c3780c15 100644 --- a/src/base/abci/abciUnfold2.c +++ b/src/base/abci/abciUnfold2.c @@ -110,7 +110,7 @@ int Abc_CommandUnfold2( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: - Abc_Print( -2, "usage: unfold [-FCP num] [-savh]\n" ); + Abc_Print( -2, "usage: unfold2 [-FCP num] [-savh]\n" ); Abc_Print( -2, "\t unfold hidden constraints as separate outputs\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs ); Abc_Print( -2, "\t-P num : the max number of constraint propagations [default = %d]\n", nProps ); @@ -119,3 +119,68 @@ usage: return 1; } + + +int Abc_CommandFold2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk, * pNtkRes; + int fCompl; + int fVerbose; + int c; + extern Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int); + pNtk = Abc_FrameReadNtk(pAbc); + // set defaults + fCompl = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF ) + { + switch ( c ) + { + /* case 'c': */ + /* fCompl ^= 1; */ + /* break; */ + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + if ( Abc_NtkConstrNum(pNtk) == 0 ) + { + Abc_Print( 0, "The network has no constraints.\n" ); + return 0; + } + if ( Abc_NtkIsComb(pNtk) ) + Abc_Print( 0, "The network is combinational.\n" ); + // modify the current network + pNtkRes = Abc_NtkDarFold2( pNtk, fCompl, fVerbose ,0); + if ( pNtkRes == NULL ) + { + Abc_Print( 1,"Transformation has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; +usage: + Abc_Print( -2, "usage: fold [-cvh]\n" ); + Abc_Print( -2, "\t folds constraints represented as separate outputs\n" ); + // Abc_Print( -2, "\t-c : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} |