diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-05 21:43:11 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-10-05 21:43:11 -0700 |
| commit | 6de48109f3271bcca4196b7691ce47f6b1d150a2 (patch) | |
| tree | 78afb728af648f33310ba0557c506603b8b2fb75 /src | |
| parent | 369b5f479ae28ed67b29ce524c58d2dee8733c7e (diff) | |
| download | abc-6de48109f3271bcca4196b7691ce47f6b1d150a2.tar.gz abc-6de48109f3271bcca4196b7691ce47f6b1d150a2.tar.bz2 abc-6de48109f3271bcca4196b7691ce47f6b1d150a2.zip | |
Allow for binary input file in 'testdec' and 'testnpn'.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 15 | ||||
| -rw-r--r-- | src/base/abci/abcDec.c | 3 |
2 files changed, 15 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d515fb5c..d1acef62 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -818,6 +818,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Liveness", "l3s", Abc_CommandAbcLivenessToSafetyWithLTL, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); + { extern void Dar_LibStart(); Dar_LibStart(); @@ -4802,7 +4803,12 @@ int Abc_CommandTestDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc != globalUtilOptind + 1 ) { printf( "Input file is not given.\n" ); - goto usage; + return 0; + } + if ( nVarNum >= 0 && nVarNum < 6 ) + { + printf( "The number of variables cannot be less than 6.\n" ); + return 0; } // get the output file name pFileName = argv[globalUtilOptind]; @@ -4889,7 +4895,12 @@ int Abc_CommandTestNpn( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc != globalUtilOptind + 1 ) { printf( "Input file is not given.\n" ); - goto usage; + return 0; + } + if ( nVarNum >= 0 && nVarNum < 6 ) + { + printf( "The number of variables cannot be less than 6.\n" ); + return 0; } // get the output file name pFileName = argv[globalUtilOptind]; diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c index 7e49beb1..309c6a50 100644 --- a/src/base/abci/abcDec.c +++ b/src/base/abci/abcDec.c @@ -402,10 +402,11 @@ Abc_TtStore_t * Abc_TtStoreLoad( char * pFileName, int nVarNum ) { char * pBuffer; int nFileSize = Abc_FileSize( pFileName ); - int nBytes = (1 << nVarNum); + int nBytes = (1 << (nVarNum-3)); int nTruths = nFileSize / nBytes; if ( nFileSize == -1 ) return NULL; + assert( nVarNum >= 6 ); if ( nFileSize % nBytes != 0 ) Abc_Print( 0, "The file size (%d) is divided by the truth table size (%d) with remainder (%d).\n", nFileSize, nBytes, nFileSize % nBytes ); |