Started experiments with a new solver.

4 files changed, 20 insertions, 14 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 32ed17eb..ac0f26dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -17038,7 +17038,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fPartition;
     int fMiter;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -17143,7 +17143,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat && fMiter )
-        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
+        Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose );
     else
         Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
 
@@ -18250,20 +18250,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int RetValue;
     int fAlignPol;
     int fAndOuts;
+    int fNewSolver;
     int fVerbose;
     int nConfLimit;
     int nInsLimit;
     int clk;
 
-    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+    extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
     // set defaults
     fAlignPol  = 0;
     fAndOuts   = 0;
+    fNewSolver = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
     nInsLimit  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18295,6 +18297,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fAndOuts ^= 1;
             break;
+        case 'n':
+            fNewSolver ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -18329,7 +18334,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     clk = clock();
-    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fVerbose );
+    RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
@@ -18351,13 +18356,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-pavh]\n" );
+    Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" );
     Abc_Print( -2, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     Abc_Print( -2, "\t         derives CNF from the current network and leave it unchanged\n" );
     Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     Abc_Print( -2, "\t-p     : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );  
     Abc_Print( -2, "\t-a     : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );  
+    Abc_Print( -2, "\t-n     : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );  
     Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dc090791..0bfd515e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1240,7 +1240,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose )
+int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;//, clk = clock();
@@ -1248,7 +1248,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 //    assert( Abc_NtkPoNum(pNtk) == 1 );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fVerbose ); 
+    RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); 
     pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
     Aig_ManStop( pMan );
     return RetValue;
@@ -1910,7 +1910,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
             if ( Aig_ManRegNum(pTemp) == 0 )
             {
                 pTemp->pSeqModel = NULL;
-                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0 ); 
+                RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 ); 
                 if ( pTemp->pData )
                     pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
 //                pNtk->pModel = pTemp->pData, pTemp->pData = NULL;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 52ac5192..28ff0ee6 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 
 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 extern void   Aig_ManStop( Aig_Man_t * pMan );
-//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
+//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
 extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
 extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
 
@@ -532,7 +532,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
     // if SAT only, solve without iteration
 //    RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
     pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
-    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0 ); 
+    RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); 
     pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
     Aig_ManStop( pMan2 );
 //    pNtk->pModel = Aig_ManReleaseData( pMan2 );
@@ -582,7 +582,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
             Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
             printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
         }
-        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, pParams->fVerbose ); 
+        RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose ); 
         pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
         Aig_ManStop( pMan2 );
     }
diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c
index 90cc0146..e6395ef3 100644
--- a/src/base/abci/abcQbf.c
+++ b/src/base/abci/abcQbf.c
@@ -41,7 +41,7 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
 static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
 static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
 
-extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
+extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
         // solve the synthesis instance
 clkS = clock();
 //        RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
-        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0 );
+        RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 );
 clkS = clock() - clkS;
         if ( RetValue == 0 )
             Abc_NtkModelToVector( pNtkSyn, vPiValues );