diff options
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 49 |
1 files changed, 36 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 71b76cf6..70cd2e6c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2868,6 +2868,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); return 0; } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); + return 0; + } + +/* if ( !Abc_NtkIsLogic(pNtk) ) { fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); @@ -2877,19 +2884,35 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkUnmap(pNtk); if ( Abc_NtkIsSopLogic(pNtk) ) Abc_NtkSopToBdd(pNtk); - - RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); - if ( RetValue == -1 ) - printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); - else if ( RetValue == 0 ) - printf( "The miter is SATISFIABLE.\n" ); +*/ + if ( Abc_NtkIsStrash(pNtk) ) + { + RetValue = Abc_NtkMiterSat2( pNtk, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + } else - printf( "The miter is UNSATISFIABLE.\n" ); + { + Abc_Ntk_t * pTemp; + pTemp = Abc_NtkStrash( pNtk, 0, 0 ); + RetValue = Abc_NtkMiterSat2( pTemp, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); + else + printf( "The miter is UNSATISFIABLE.\n" ); + Abc_NtkDelete( pTemp ); + } return 0; usage: fprintf( pErr, "usage: sat [-T num] [-vh]\n" ); - fprintf( pErr, "\t solves the miter\n" ); + fprintf( pErr, "\t solves the combinational miter\n" ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -3722,11 +3745,11 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) } // run the command - pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose ); + pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); - return 1; + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -3788,9 +3811,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } -// Abc_NtkDeriveEsops( pNtk ); -// Abc_NtkXyz( pNtk, 128, 0, 0, 0 ); - printf( "This command is currently not used.\n" ); + Abc_NtkTestEsop( pNtk ); +// Abc_NtkTestSop( pNtk ); +// printf( "This command is currently not used.\n" ); /* // run the command |