summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abc.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-07-30 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-07-30 08:01:00 -0700
commitfefd8b901d89ad0d977db8896c12123cc747e3d7 (patch)
tree1e35b5d52cafdff284e08163136d9a61e1a09235 /src/base/abci/abc.c
parenta8a80d9a1a84c2c5f605f6630dc804f3631e7a9f (diff)
downloadabc-fefd8b901d89ad0d977db8896c12123cc747e3d7.tar.gz
abc-fefd8b901d89ad0d977db8896c12123cc747e3d7.tar.bz2
abc-fefd8b901d89ad0d977db8896c12123cc747e3d7.zip
Version abc70730
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r--src/base/abci/abc.c21
1 files changed, 10 insertions, 11 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1df13db8..8ae5bb9e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6187,7 +6187,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk4VarTable( pNtk );
// Dar_NtkGenerateArrays( pNtk );
// Dar_ManDeriveCnfTest2();
-
+/*
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Network should be strashed. Command has failed.\n" );
@@ -6195,7 +6195,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
-// pNtkRes = NULL;
+*/
+ pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -10732,7 +10733,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
- int nFrames;
+ int nFramesK;
int fExdc;
int fImp;
int fVerbose;
@@ -10742,13 +10743,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
- printf( "This command is not implemented\n" );
-
// set defaults
- nFrames = 1;
+ nFramesK = 1;
fExdc = 1;
fImp = 0;
- fVerbose = 1;
+ fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF )
{
@@ -10760,9 +10759,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
- nFrames = atoi(argv[globalUtilOptind]);
+ nFramesK = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nFrames <= 0 )
+ if ( nFramesK <= 0 )
goto usage;
break;
case 'e':
@@ -10800,7 +10799,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
- pNtkRes = Abc_NtkSeqSweep( pNtk, nFrames, fVerbose );
+ pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -10813,7 +10812,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" );
- fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
// fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );