Adding support for Dimacs input to &satoko.

3 files changed, 108 insertions, 30 deletions

diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c
index aaf9daaa..dad3bcc4 100644
--- a/src/aig/gia/giaSatoko.c
+++ b/src/aig/gia/giaSatoko.c
@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "sat/cnf/cnf.h"
+#include "misc/extra/extra.h"
 #include "sat/satoko/satoko.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -79,22 +80,6 @@ Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts )
-{
-    satoko_t * pSat = satoko_create();
-    int i;
-    //sat_solver_setnvars( pSat, p->nVars );
-    for ( i = 0; i < pCnf->nClauses; i++ )
-    {
-        if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
-        {
-            satoko_destroy( pSat );
-            return NULL;
-        }
-    }
-    satoko_configure(pSat, opts);
-    return pSat;
-}
 void Gia_ManSatokoReport( int iOutput, int status, abctime clk )
 {
     if ( iOutput >= 0 )
@@ -111,6 +96,95 @@ void Gia_ManSatokoReport( int iOutput, int status, abctime clk )
 
     Abc_PrintTime( 1, "Time", clk );
 }
+satoko_t * Gia_ManSatokoFromDimacs( char * pFileName, satoko_opts_t * opts )
+{
+    satoko_t * pSat = satoko_create();
+    char * pBuffer = Extra_FileReadContents( pFileName );
+    Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+    char * pTemp; int fComp, Var, VarMax = 0;
+    for ( pTemp = pBuffer; *pTemp; pTemp++ )
+    {
+        if ( *pTemp == 'c' || *pTemp == 'p' ) 
+        {
+            while ( *pTemp != '\n' )
+                pTemp++;
+            continue;
+        }
+        while ( *pTemp == ' ' || *pTemp == '\t' || *pTemp == '\r' || *pTemp == '\n' )
+            pTemp++;
+        fComp = 0;
+        if ( *pTemp == '-' )
+            fComp = 1, pTemp++;
+        if ( *pTemp == '+' )
+            pTemp++;
+        Var = atoi( pTemp );
+        if ( Var == 0 ) {
+            if ( Vec_IntSize(vLits) > 0 ) 
+            {
+                satoko_setnvars( pSat, VarMax+1 );
+                if ( !satoko_add_clause( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ) )
+                {
+                    satoko_destroy(pSat);
+                    Vec_IntFree( vLits );
+                    ABC_FREE( pBuffer );
+                    return NULL;
+                }
+                Vec_IntClear( vLits );
+            }
+        }
+        else 
+        {
+            Var--;
+            VarMax = Abc_MaxInt( VarMax, Var );
+            Vec_IntPush( vLits, Abc_Var2Lit(Var, fComp) );
+        }
+        while ( *pTemp >= '0' && *pTemp <= '9' )
+            pTemp++;
+    }
+    ABC_FREE( pBuffer );
+    Vec_IntFree( vLits );
+    return pSat;
+}
+void Gia_ManSatokoDimacs( char * pFileName, satoko_opts_t * opts )
+{
+    abctime clk = Abc_Clock();  
+    int status = SATOKO_UNSAT;
+    satoko_t * pSat = Gia_ManSatokoFromDimacs( pFileName, opts );
+    if ( pSat )
+    {
+        status = satoko_solve( pSat );
+        satoko_destroy( pSat );
+    }
+    Gia_ManSatokoReport( -1, status, Abc_Clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts )
+{
+    satoko_t * pSat = satoko_create();
+    int i;
+    //sat_solver_setnvars( pSat, p->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
+        {
+            satoko_destroy( pSat );
+            return NULL;
+        }
+    }
+    satoko_configure(pSat, opts);
+    return pSat;
+}
 satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts )
 {
     Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
@@ -126,8 +200,7 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
 {
     abctime clk = Abc_Clock();
     satoko_t * pSat;
-    int status, Cost = 0;
-
+    int status = SATOKO_UNSAT, Cost = 0;
     pSat = Gia_ManSatokoCreate( p, opts );
     if ( pSat )
     {
@@ -135,9 +208,6 @@ int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput )
         Cost = satoko_stats(pSat)->n_conflicts;
         satoko_destroy( pSat );
     }
-    else 
-        status = SATOKO_UNSAT;
-
     Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk );
     return Cost;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 025d9963..520af9fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23795,6 +23795,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern void Gia_ManSatokoDimacs( char * pFileName, satoko_opts_t * opts );
     extern void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem );
     int c, fSplit = 0, fIncrem = 0;
 
@@ -23832,6 +23833,11 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
+    if ( argc == globalUtilOptind + 1 )
+    {
+        Gia_ManSatokoDimacs( argv[globalUtilOptind], &opts );
+        return 0;
+    }
     if ( pAbc->pGia == NULL )
     {
         Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
@@ -23841,12 +23847,14 @@ int Abc_CommandAbc9Satoko( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &satoko [-C num] [-sivh]\n" );
-    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
-    Abc_Print( -2, "\t-s     : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
-    Abc_Print( -2, "\t-i     : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" );
-    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "usage: &satoko [-C num] [-sivh] <file.cnf>\n" );
+    Abc_Print( -2, "\t             run Satoko by Bruno Schmitt\n" );
+    Abc_Print( -2, "\t-C num     : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
+    Abc_Print( -2, "\t-s         : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
+    Abc_Print( -2, "\t-i         : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" );
+    Abc_Print( -2, "\t-v         : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
+    Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n");
+    Abc_Print( -2, "\t-h         : print the command usage\n");
     return 1;
 }
 
diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp
index bcff4165..74a58c33 100644
--- a/src/sat/glucose/AbcGlucoseCmd.cpp
+++ b/src/sat/glucose/AbcGlucoseCmd.cpp
@@ -50,7 +50,7 @@ extern "C" {
 
 void Glucose_Init(Abc_Frame_t *pAbc)
 {
-    Cmd_CommandAdd( pAbc, "ABC9", "&gluco",  Abc_CommandGlucose,  0 );
+    Cmd_CommandAdd( pAbc, "ABC9", "&glucose",  Abc_CommandGlucose,  0 );
 }
 
 void Glucose_End( Abc_Frame_t * pAbc )
@@ -127,8 +127,8 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
     
 usage:
-    Abc_Print( -2, "usage: &gluco [-C num] [-pvh] <file.cnf>\n" );
-    Abc_Print( -2, "\t             run glucose\n" );
+    Abc_Print( -2, "usage: &glucose [-C num] [-pvh] <file.cnf>\n" );
+    Abc_Print( -2, "\t             run Glucose 3.0 by Gilles Audemard and Laurent Simon\n" );
     Abc_Print( -2, "\t-C num     : conflict limit [default = %d]\n",  nConfls );
     Abc_Print( -2, "\t-p         : enable preprocessing [default = %d]\n",pre);
     Abc_Print( -2, "\t-v         : verbosity [default = %d]\n",verb);