diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 20d0f0c38..a343c6789 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -66,6 +66,7 @@ static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int CmdCommandSolver ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -121,6 +122,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "capo", CmdCommandCapo, 0 ); Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 ); Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 ); + Cmd_CommandAdd( pAbc, "Various", "&solver", CmdCommandSolver, 0 ); Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 ); } @@ -2806,6 +2808,125 @@ usage: return 1; } +/**Function******************************************************************** + + Synopsis [Calls Capo internally.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int CmdCommandSolver( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine ); + FILE * pFile; + char Command[1000]; + char TempFileName[100]; + unsigned int RandomNum; + int i; + + // Check for help flags + if ( argc > 1 ) + { + if ( strcmp( argv[1], "-h" ) == 0 ) + goto usage; + if ( strcmp( argv[1], "-?" ) == 0 ) + goto usage; + } + + // Check if AIG is available + if ( pAbc->pGia == NULL ) + { + fprintf( pAbc->Err, "The current AIG is not available.\n" ); + goto usage; + } + + // Check if solver binary exists in current directory or PATH + char * pSolverName; + if ( (pFile = fopen( "./solver", "r" )) != NULL ) + { + pSolverName = "./solver"; + fclose( pFile ); + } + else + { + // Check if solver exists in PATH + char CheckCommand[100]; + sprintf( CheckCommand, "which solver > /dev/null 2>&1" ); + if ( system( CheckCommand ) == 0 ) + { + pSolverName = "solver"; + } + else + { + fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" ); + goto usage; + } + } + + // Generate random 8-hex-character temporary filename + RandomNum = (unsigned int)(ABC_PTRUINT_T)pAbc ^ + (unsigned int)(ABC_PTRUINT_T)pAbc->pGia ^ + (unsigned int)time(NULL) ^ + (unsigned int)getpid(); + sprintf( TempFileName, "%08X.aig", RandomNum ); + + // Write the current AIG to the temporary file + Gia_AigerWrite( pAbc->pGia, TempFileName, 0, 0, 1 ); + + // Verify the file was created successfully + if ( (pFile = fopen( TempFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Failed to create temporary AIG file \"%s\".\n", TempFileName ); + return 1; + } + fclose( pFile ); + + // Build the command string + sprintf( Command, "%s", pSolverName ); + + // Add all user arguments + for ( i = 1; i < argc; i++ ) + { + strcat( Command, " " ); + strcat( Command, argv[i] ); + } + + // Add the AIG filename at the end + strcat( Command, " " ); + strcat( Command, TempFileName ); + + // Debug: Show what command is being executed + fprintf( pAbc->Out, "Executing command: %s\n", Command ); + + // Execute the solver command + if ( system( Command ) == -1 ) + { + fprintf( pAbc->Err, "The following command has failed:\n" ); + fprintf( pAbc->Err, "\"%s\"\n", Command ); + unlink( TempFileName ); + return 1; + } + + // Clean up the temporary file + unlink( TempFileName ); + + return 0; + +usage: + fprintf( pAbc->Err, "\tusage: &solver \n"); + fprintf( pAbc->Err, "\t run the external solver binary on the current AIG\n" ); + fprintf( pAbc->Err, "\t-h : print the command usage\n" ); + fprintf( pAbc->Err, "\t : arguments to pass to the solver\n" ); + fprintf( pAbc->Err, "\t The current AIG will be written to a temporary file\n" ); + fprintf( pAbc->Err, "\t and passed as the last argument to the solver.\n" ); + fprintf( pAbc->Err, "\t Example: solver -h\n" ); + return 1; +} + /**Function******************************************************************** Synopsis [Print the version string.]