Improvements to the QBF solver.

3 files changed, 59 insertions, 10 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fb25e8ca..f5d93f94 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8170,7 +8170,9 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
-    int nVars;
+    int nVars;    // the number of variables
+    int nLutSize; // the size of LUTs
+    int nLuts;    // the number of LUTs
     int fAdder;
     int fSorter;
     int fMesh;
@@ -8196,7 +8198,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     fRandom = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nasmftrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NKLasmftrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8211,6 +8213,28 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nVars < 0 ) 
                 goto usage;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLuts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLuts < 0 ) 
+                goto usage;
+            break;
         case 'a':
             fAdder ^= 1;
             break;
@@ -8253,7 +8277,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     else if ( fMesh )
         Abc_GenMesh( FileName, nVars );
     else if ( fFpga )
-        Abc_GenFpga( FileName, 4, 3, 10 );
+        Abc_GenFpga( FileName, nLutSize, nLuts, nVars );
 //        Abc_GenFpga( FileName, 2, 2, 3 );
 //        Abc_GenFpga( FileName, 3, 2, 5 );
     else if ( fOneHot )
@@ -8265,9 +8289,11 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: gen [-N num] [-asmftrvh] <file>\n" );
+    Abc_Print( -2, "usage: gen [-NKL num] [-asmftrvh] <file>\n" );
     Abc_Print( -2, "\t         generates simple circuits\n" );
     Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars );  
+    Abc_Print( -2, "\t-K num : the LUT size (to be used with switch -f) [default = %d]\n", nLutSize );  
+    Abc_Print( -2, "\t-L num : the LUT count (to be used with switch -f) [default = %d]\n", nLuts );  
     Abc_Print( -2, "\t-a     : generate ripple-carry adder [default = %s]\n", fAdder? "yes": "no" );  
     Abc_Print( -2, "\t-s     : generate a sorter [default = %s]\n", fSorter? "yes": "no" );  
     Abc_Print( -2, "\t-m     : generate a mesh [default = %s]\n", fMesh? "yes": "no" );  
@@ -11053,8 +11079,8 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     Abc_Print( -2, "usage: qbf [-P num] [-vh]\n" );
-    Abc_Print( -2, "\t         solves a quantified intean formula problem EpVxM(p,x)\n" );
-    Abc_Print( -2, "\t-P num : number of paramters (should be the first PIs) [default = %d]\n", nPars );
+    Abc_Print( -2, "\t         solves QBF problem EpVxM(p,x)\n" );
+    Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index a886949f..a5bfeef5 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -424,6 +424,7 @@ void Abc_WriteKLut( FILE * pFile, int nLutSize )
 ***********************************************************************/
 void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
 {
+    int fGenerateFunc = 1;
     FILE * pFile;
     int nVarsLut = (1 << nLutSize);                     // the number of LUT variables
     int nVarsLog = Extra_Base2Log( nVars + nLuts - 1 ); // the number of encoding vars
@@ -440,7 +441,11 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
 
     fprintf( pFile, ".inputs" );
     for ( i = 0; i < nParsLut; i++ )
+    {
+        if ( i % (1 << nLutSize) == 0 && i != (nLuts - 1) * (1 << nLutSize) )
+            continue;
         fprintf( pFile, " pl%02d", i );
+    }
     fprintf( pFile, "\n" );
 
     fprintf( pFile, ".inputs" );
@@ -454,11 +459,28 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
     fprintf( pFile, "\n" );
 
     fprintf( pFile, ".outputs" );
-    fprintf( pFile, " v%02d", nVars + nLuts - 1 );
+//    fprintf( pFile, " v%02d", nVars + nLuts - 1 );
+    fprintf( pFile, " out" );
     fprintf( pFile, "\n" );
     fprintf( pFile, ".names Gnd\n" ); 
     fprintf( pFile, " 0\n" ); 
 
+    // generate function
+    if ( fGenerateFunc )
+    {
+        fprintf( pFile, ".names v%02d func out\n", nVars + nLuts - 1 );
+        fprintf( pFile, "00 1\n11 1\n" );
+        fprintf( pFile, ".names" );
+        for ( i = 0; i < nVars; i++ )
+            fprintf( pFile, " v%02d", i );
+        fprintf( pFile, " func\n" );
+        for ( i = 0; i < nVars; i++ )
+            fprintf( pFile, "1" );
+        fprintf( pFile, " 1\n" );
+    }
+    else
+        fprintf( pFile, ".names v%02d out\n1 1\n", nVars + nLuts - 1 );
+
     // generate LUTs
     for ( i = 0; i < nLuts; i++ )
     {
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index d246f039..a243c7d5 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -89,7 +89,8 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
     {
         // solve the synthesis instance
 clkS = clock();
-        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
+//        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
+        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 );
 clkS = clock() - clkS;
         if ( RetValue == 0 )
             Abc_NtkModelToVector( pNtkSyn, vPiValues );
@@ -143,8 +144,8 @@ clkV = clock() - clkV;
             printf( "AIG = %6d  ", Abc_NtkNodeNum(pNtkSyn) );
             Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars );
             printf( "  " );
-//            ABC_PRTn( "Syn", clkS );
-            ABC_PRT( "Ver", clkV );
+            ABC_PRT( "Syn", clkS );
+//            ABC_PRT( "Ver", clkV );
         }
     }
     Abc_NtkDelete( pNtkSyn );