From 839f3e18ddbc46d694b4a1832abda2999c0c1aff Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 14 Mar 2025 20:24:08 -0700
Subject: [PATCH] Experiments with mapping.

---
 src/aig/gia/giaSatLut.c | 23 +++++++++++++++--------
 src/base/abci/abc.c     |  2 +-
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index 7ca3ae4c8..716566cae 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -1539,7 +1539,7 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
 int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctime Time, int Status )
 {
     Vec_Str_t * vFileName = Vec_StrAlloc( 100 ); int c;
-    Vec_StrPrintF( vFileName, "%s", argv[0] );
+    Vec_StrPrintF( vFileName, "%s", argv[0] + (argv[0][0] == '&') );
     for ( c = 1; c < argc; c++ )
         Vec_StrPrintF( vFileName, "_%s", argv[c] + (argv[c][0] == '-') );
     Vec_StrPrintF( vFileName, ".cnf" );
@@ -1547,19 +1547,19 @@ int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctim
     FILE * pFile = fopen( Vec_StrArray(vFileName), "wb" );
     if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", Vec_StrArray(vFileName) ); Vec_StrFree(vFileName); return 0; }
     Vec_StrFree(vFileName);
-    fprintf( pFile, "c ABC command line: \"" );
+    fprintf( pFile, "c This file was generated by ABC command: \"" );
     fprintf( pFile, "%s", argv[0] );
     for ( c = 1; c < argc; c++ )
         fprintf( pFile, " %s", argv[c] );
-    fprintf( pFile, "\"  " );
+    fprintf( pFile, "\" on %s\n", Gia_TimeStamp() );
+    fprintf( pFile, "c Cardinality CDCL (https://github.com/jreeves3/Cardinality-CDCL) found it to be " );
     if ( Status == 1 )
-        fprintf( pFile, "UNSAT after " );
+        fprintf( pFile, "UNSAT" );
     if ( Status == 0 )
-        fprintf( pFile, "SAT after " );
+        fprintf( pFile, "SAT" );
     if ( Status == -1 )
-        fprintf( pFile, "UNDECIDED after " );
-    fprintf( pFile, "%.2f sec by CaDiCal on ", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
-    fprintf( pFile, "%s\n", Gia_TimeStamp() );
+        fprintf( pFile, "UNDECIDED" );
+    fprintf( pFile, " in %.2f sec\n", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
     fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
     fclose( pFile );
     return 1;
@@ -1687,16 +1687,23 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fM
     // fanins are connected once
     for ( n = nIns; n < nIns+nNodes; n++ )
     for ( f = 0; f < 2; f++ ) {
+
         nLits = 0;
         for ( i = 0; i < n; i++ )
             pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 0 );
         Gia_SatDumpClause( vStr, pLits, nLits );
+/*        
         for ( i = 0; i < n; i++ )
         for ( j = 0; j < i; j++ ) {
             pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
             pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 );
             Gia_SatDumpClause(  vStr, pLits, 2 );
         }
+*/        
+        Vec_StrPrintF( vStr, "k %d ", n-1 );
+        for ( i = 0; i < n; i++ )
+            pLits[i] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
+        Gia_SatDumpClause( vStr, pLits, n );
     }
     for ( n = nIns; n < nIns+nNodes; n++ ) {
         // fanins are equal
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 630f66aa2..a4078d54c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -55359,7 +55359,7 @@ usage:
     Abc_Print( -2, "\t          generates Boolean relation for the given logic window\n" );
     Abc_Print( -2, "\t-I list : comma-separated list of window inputs [default = undefined]\n" );
     Abc_Print( -2, "\t-O list : comma-separated list of window outputs [default = undefined]\n" );
-    Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" );
+    Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     Abc_Print( -2, "\t<file>  : the output file name (PLA format extended to represented Boolean relations)\n");
     return 1;