Adding programmable call to Kissat in command &kissat.

src/base/abci/abc.c

@@ -28148,11 +28148,11 @@ int Abc_CommandAbc9Kissat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
     extern void Gia_ManKissatCall( Abc_Frame_t * pAbc, char * pFileName, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
-    int c, nConfs = 0, nTimeLimit = 0, fSat = 0, fUnsat = 0, fPrintCex = 0, fVerbose = 0;
+    int c, nConfs = 0, nTimeLimit = 0, fSat = 0, fUnsat = 0, fPrintCex = 0, fKissat = 1, fVerbose = 0;
     char * pArgs = NULL;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTAsucvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTAsuckvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28196,6 +28196,9 @@ int Abc_CommandAbc9Kissat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fPrintCex ^= 1;
             break;
+        case 'k':
+            fKissat ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -28216,6 +28219,18 @@ int Abc_CommandAbc9Kissat( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Satoko(): There is no AIG.\n" );
         return 1;
     }
+    else if ( fKissat )
+    {
+        extern Vec_Int_t * kissat_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
+        extern void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose );
+        int nLutSize    = 8;
+        int fCnfObjIds  = 0;        
+        int fAddOrCla   = 1;
+        Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pAbc->pGia, nLutSize, fCnfObjIds, fAddOrCla, 0, fVerbose );
+        Vec_Int_t * vRes = kissat_solve_cnf( pCnf, pArgs, nConfs, nTimeLimit, fSat, fUnsat, fPrintCex, 1 );
+        Vec_IntFreeP( &vRes );
+        Cnf_DataFree(pCnf);
+    }
     else
     {
         int nLutSize    = 8;
@@ -28229,18 +28244,20 @@ int Abc_CommandAbc9Kissat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &kissat [-CT num] [-sucvh] [-A string] <file.cnf>\n" );
+    Abc_Print( -2, "usage: &kissat [-CT num] [-suckvh] [-A string] <file.cnf>\n" );
-    Abc_Print( -2, "\t             run SAT solver Kissat, by Armin Biere (https://github.com/arminbiere/kissat)\n" );
+    Abc_Print( -2, "\t             run SAT solver Kissat 4.0.2, by Armin Biere (https://github.com/arminbiere/kissat)\n" );
     Abc_Print( -2, "\t-C num     : limit on the number of conflicts [default = %d]\n", nConfs );
     Abc_Print( -2, "\t-T num     : runtime limit in seconds [default = %d]\n", nTimeLimit );
     Abc_Print( -2, "\t-s         : expect a satisfiable problem [default = %s]\n", fSat ? "yes": "no" );
     Abc_Print( -2, "\t-u         : expect an unsatisfiable problem [default = %s]\n", fUnsat ? "yes": "no" );
     Abc_Print( -2, "\t-c         : prints satisfying assignment if satisfiable [default = %s]\n", fPrintCex ? "yes": "no" );
+    Abc_Print( -2, "\t-k         : calls Kissat through programmable APIs [default = %s]\n", fKissat ? "yes": "no" );
     Abc_Print( -2, "\t-v         : prints verbose information [default = %s]\n", fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-A num     : string containing additional command-line args for the Kissat binary [default = %s]\n", pArgs ? pArgs : "unused" );
     Abc_Print( -2, "\t             (in particular, <&kissat -A \"--help\"> prints all command-line args of Kissat)\n" );
     Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n");
     Abc_Print( -2, "\t-h         : print the command usage\n");
+    Abc_Print( -2, "\n\t             The solver was integrated into ABC by Yukio Miyasaka\n");
     return 1;
 }
 

src/sat/kissat/kissatSolver.c

@@ -4,11 +4,11 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName []
+  PackageName [SAT solver Kissat by Armin Biere, University of Freiburg]
 
-  Synopsis    []
+  Synopsis    [https://github.com/arminbiere/kissat]
 
-  Author      [Alan Mishchenko]
+  Author      [Integrated into ABC by Yukio Miyasaka]
   
   Affiliation [UC Berkeley]
 
@@ -191,6 +191,53 @@ int kissat_solver_get_var_value(kissat_solver* s, int v) {
   return kissat_value((kissat*)s->p, v + 1) > 0;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Solves the given CNF using kissat.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * kissat_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vRes = NULL;
+    int i, * pBeg, * pEnd, RetValue;    
+    if ( fVerbose )
+        printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+    kissat_solver *pSat = kissat_solver_new();
+    kissat_solver_setnvars(pSat, pCnf->nVars);
+    assert(kissat_solver_nvars(pSat) == pCnf->nVars);
+    Cnf_CnfForClause( pCnf, pBeg, pEnd, i ) {
+        if ( !kissat_solver_addclause(pSat, pBeg, pEnd) )
+        {
+            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
+            return NULL;
+        }    
+    }
+    RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
+    if ( RetValue == 1 )
+      printf( "Result: Satisfiable.  " );
+    else if ( RetValue == -1 )
+      printf( "Result: Unsatisfiable.  " );
+    else
+      printf( "Result: Undecided.  " );
+    if ( RetValue == 1 ) {
+        vRes = Vec_IntAlloc( pCnf->nVars );
+        for ( i = 0; i < pCnf->nVars; i++ )
+          Vec_IntPush( vRes, kissat_solver_get_var_value(pSat, 1) );
+    }
+    kissat_solver_delete(pSat);
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return vRes;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/kissat/kissatSolver.h

@@ -4,11 +4,11 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName []
+  PackageName [SAT solver Kissat by Armin Biere, University of Freiburg]
 
-  Synopsis    []
+  Synopsis    [https://github.com/arminbiere/kissat]
 
-  Author      [Alan Mishchenko]
+  Author      [Integrated into ABC by Yukio Miyasaka]
   
   Affiliation [UC Berkeley]
 
@@ -26,6 +26,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig/gia/gia.h"
+#include "sat/cnf/cnf.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -61,6 +62,7 @@ extern int             kissat_solver_nvars(kissat_solver* s);
 extern int             kissat_solver_addvar(kissat_solver* s);
 extern void            kissat_solver_setnvars(kissat_solver* s,int n);
 extern int             kissat_solver_get_var_value(kissat_solver* s, int v);
+extern Vec_Int_t *     kissat_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
 
 ABC_NAMESPACE_HEADER_END