From ba69519d736763531d141859caffcca887b664f7 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 8 Mar 2026 10:26:27 -0700
Subject: [PATCH] Adding command for calling external solvers.

---
 src/base/cmd/cmd.c | 75 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 75 insertions(+)

diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 0bb4b412b..bbe3b7d8e 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -67,6 +67,7 @@ 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 );
+static int CmdCommandSolver2       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -123,6 +124,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     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", "&solver2",    CmdCommandSolver2,         0 );
 
     Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn,  0 );
 }
@@ -2971,6 +2973,79 @@ usage:
     return 1;
 }
 
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int CmdCommandSolver2( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    FILE * pFile;
+    char Command[2000];
+    int i;
+
+    if ( argc > 1 )
+    {
+        if ( strcmp( argv[1], "-h" ) == 0 )
+            goto usage;
+        if ( strcmp( argv[1], "-?" ) == 0 )
+            goto usage;
+    }
+
+#if defined(__wasm)
+    fprintf( pAbc->Err, "Unsupported command.\n" );
+    return 1;
+#else
+    // Check if solver binary exists in current directory or PATH
+    if ( (pFile = fopen( "./solver", "r" )) != NULL )
+    {
+        sprintf( Command, "%s", "./solver" );
+        fclose( pFile );
+    }
+    else
+    {
+        char CheckCommand[100];
+        sprintf( CheckCommand, "which solver > /dev/null 2>&1" );
+        if ( system( CheckCommand ) != 0 )
+        {
+            fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" );
+            goto usage;
+        }
+        sprintf( Command, "%s", "solver" );
+    }
+
+    // Append user-provided arguments as-is: solver <args>
+    for ( i = 1; i < argc; i++ )
+    {
+        strcat( Command, " " );
+        strcat( Command, argv[i] );
+    }
+
+    fprintf( pAbc->Out, "Executing command: %s\n", Command );
+    if ( system( Command ) == -1 )
+    {
+        fprintf( pAbc->Err, "The following command has failed:\n" );
+        fprintf( pAbc->Err, "\"%s\"\n", Command );
+        return 1;
+    }
+#endif
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "\tusage: &solver2 <args>\n");
+    fprintf( pAbc->Err, "\t           run the external solver as \"solver <args>\"\n" );
+    fprintf( pAbc->Err, "\t-h      :  print the command usage\n" );
+    fprintf( pAbc->Err, "\t<args>  :  all arguments passed directly to solver\n" );
+    return 1;
+}
+
 /**Function********************************************************************
 
   Synopsis    [Print the version string.]