Experiments with recent ideas.

7 files changed, 503 insertions, 280 deletions

diff --git a/abclib.dsp b/abclib.dsp
index ace73806..02fba9dc 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1419,6 +1419,10 @@ SOURCE=.\src\sat\bmc\bmcBmcAnd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcBmci.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcCexCut.c
 # End Source File
 # Begin Source File
@@ -1447,7 +1451,7 @@ SOURCE=.\src\sat\bmc\bmcICheck.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\bmc\bmcLilac.c
+SOURCE=.\src\sat\bmc\bmcInse.c
 # End Source File
 # Begin Source File
 
@@ -1455,11 +1459,11 @@ SOURCE=.\src\sat\bmc\bmcLoad.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\bmc\bmcMulti.c
+SOURCE=.\src\sat\bmc\bmcMaxi.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\bmc\bmcTulip.c
+SOURCE=.\src\sat\bmc\bmcMulti.c
 # End Source File
 # Begin Source File
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index d3ee3f48..36be9e49 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -305,12 +305,16 @@ void Gia_ManPrintTents( Gia_Man_t * p )
 void Gia_ManPrintInitClasses( Vec_Int_t * vInits )
 {
     int i, Value;
-    int Counts[4] = {0};
+    int Counts[6] = {0};
     Vec_IntForEachEntry( vInits, Value, i )
         Counts[Value]++;
-    for ( i = 0; i < 4; i++ )
-        printf( "%d = %d  ", i, Counts[i] );
-    printf( "X = %d\n", Counts[2] + Counts[3] );
+    for ( i = 0; i < 6; i++ )
+        if ( Counts[i] )
+            printf( "%d = %d  ", i, Counts[i] );
+    printf( "  " );
+    printf( "B = %d  ", Counts[0] + Counts[1] );
+    printf( "X = %d  ", Counts[2] + Counts[3] );
+    printf( "Q = %d\n", Counts[4] + Counts[5] );
     Vec_IntForEachEntry( vInits, Value, i )
     {
         Counts[Value]++;
@@ -319,9 +323,13 @@ void Gia_ManPrintInitClasses( Vec_Int_t * vInits )
         else if ( Value == 1 )
             printf( "1" );
         else if ( Value == 2 )
-            printf( "x" );
+            printf( "2" );
         else if ( Value == 3 )
-            printf( "X" );
+            printf( "3" );
+        else if ( Value == 4 )
+            printf( "4" );
+        else if ( Value == 5 )
+            printf( "5" );
         else assert( 0 );
     }
     printf( "\n" );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9138d212..05200336 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -399,8 +399,9 @@ static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9FunFaTest          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Tulip              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Lilac              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Inse               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Maxi               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Bmci               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -964,8 +965,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&funfatest",    Abc_CommandAbc9FunFaTest,    0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&tulip",        Abc_CommandAbc9Tulip,        0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&lilac",        Abc_CommandAbc9Lilac,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&inse",         Abc_CommandAbc9Inse,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&maxi",        Abc_CommandAbc9Maxi,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&bmci",        Abc_CommandAbc9Bmci,        0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -32751,9 +32753,104 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9Inse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
+    extern Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
+    int c, nFrames = 10, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 )
+                goto usage;
+            break;
+        case 's':
+            fSim ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Inse(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Inse(): AIG is combinational.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vInitClasses != NULL )
+    {
+        Abc_Print( 1, "Abc_CommandAbc9Inse(): All-0 initial state is assumed.\n" );
+        Vec_IntFreeP( &pAbc->pGia->vInitClasses );
+    }
+    pAbc->pGia->vInitClasses = Gia_ManInseTest( pAbc->pGia, NULL, nFrames, nWords, nTimeOut, fSim, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &inse [-FWT num] [-svh]\n" );
+    Abc_Print( -2, "\t         experimental procedure\n" );
+    Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
+    Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
+    Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
+    Abc_Print( -2, "\t-s     : toggles using ternary simulation [default = %s]\n",            fSim?     "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");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Maxi( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
     Vec_Int_t * vTemp;
     int c, nFrames = 5, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
@@ -32808,20 +32905,20 @@ int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Tulip(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Maxi(): There is no AIG.\n" );
         return 0;
     }
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Tulip(): AIG is combinational.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Maxi(): AIG is combinational.\n" );
         return 0;
     }
-    pAbc->pGia->vInitClasses = Gia_ManTulipTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
+    pAbc->pGia->vInitClasses = Gia_ManMaxiTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
     Vec_IntFreeP( &vTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &tulip [-FWT num] [-svh]\n" );
+    Abc_Print( -2, "usage: &maxi [-FWT num] [-svh]\n" );
     Abc_Print( -2, "\t         experimental procedure\n" );
     Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
     Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
@@ -32843,9 +32940,9 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9Bmci( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
+    extern int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
     int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
@@ -32899,24 +32996,24 @@ int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Lilac(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
         return 0;
     }
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Lilac(): AIG is combinational.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Bmci(): AIG is combinational.\n" );
         return 0;
     }
     if ( pAbc->pGia->vInitClasses == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Lilac(): Init array is not given.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Bmci(): Init array is not given.\n" );
         return 0;
     }
-    Gia_ManLilacTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
+    Gia_ManBmciTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &lilac [-FWT num] [-svh]\n" );
+    Abc_Print( -2, "usage: &bmci [-FWT num] [-svh]\n" );
     Abc_Print( -2, "\t         experimental procedure\n" );
     Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
     Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
diff --git a/src/sat/bmc/bmcLilac.c b/src/sat/bmc/bmcBmci.c
index f09d0b66..ff0fb393 100644
--- a/src/sat/bmc/bmcLilac.c
+++ b/src/sat/bmc/bmcBmci.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [bmcLilac.c]
+  FileName    [bmcBmci.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: bmcLilac.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -88,7 +88,7 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse )
+void Bmc_BmciUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse )
 {
     Gia_Obj_t * pObj;
     int i;
@@ -115,7 +115,7 @@ void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
+int Bmc_BmciPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
 {
     Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); 
     int iLitPart0, iLitPart1, iRes;
@@ -129,8 +129,8 @@ int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Ma
         return iRes;
     }
     assert( Gia_ObjIsAnd(pObj) );
-    iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
-    iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
+    iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
+    iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
     iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) );
     iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) );
     Vec_IntPush( vPartMap, iIdNew );
@@ -138,7 +138,7 @@ int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Ma
     Vec_IntWriteEntry( vCopies, iIdNew, iRes );
     return iRes;
 }
-Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
+Gia_Man_t * Bmc_BmciPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
 {
     Gia_Man_t * pPart;
     int i, iLit, iLitPart;
@@ -153,7 +153,7 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM
         if ( iLit == -1 )
             continue;
         assert( iLit >= 2 );
-        iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
+        iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
         Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) );
         Vec_IntPush( vPartMap, -1 );
     }
@@ -173,7 +173,7 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose )
+int Bmc_BmciPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose )
 {
     int nSatVars = 1;
     Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies;
@@ -210,8 +210,8 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
     for ( f = 0; f < nFrames; f++ )
     {
         abctime clk = Abc_Clock();
-        Bmc_LilacUnfold( pNew, p, vLits0, 0 );
-        Bmc_LilacUnfold( pNew, p, vLits1, 1 );
+        Bmc_BmciUnfold( pNew, p, vLits0, 0 );
+        Bmc_BmciUnfold( pNew, p, vLits1, 1 );
         assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) );
         nMiters  = 0;
         Vec_IntClear( vMiters );
@@ -228,7 +228,7 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
             break;
         }
         // create new part
-        pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
+        pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
         pCnf = Cnf_DeriveGiaRemapped( pPart );
         Cnf_DataLiftGia( pCnf, pPart, nSatVars );
         nSatVars += pCnf->nVars;
@@ -327,10 +327,10 @@ cleanup:
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
+int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
 {
     Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
-    Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
+    Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
     Vec_IntFree( vInit0 );
     return 1;
 }
diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcInse.c
index 104b3ee4..00cd3df3 100644
--- a/src/sat/bmc/bmcTulip.c
+++ b/src/sat/bmc/bmcInse.c
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [bmcTulip.c]
+  FileName    [bmcInse.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: bmcTulip.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -49,7 +49,7 @@ static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id )       { return (wor
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit )
+void Gia_ManInseInit( Gia_Man_t * p, Vec_Int_t * vInit )
 {
     Gia_Obj_t * pObj;
     word * pData1, * pData0;
@@ -69,7 +69,7 @@ void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit )
                 pData0[i] = pData1[i] = 0;
     }
 }
-void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id )
+void Gia_ManInseSimulateObj( Gia_Man_t * p, int Id )
 {
     Gia_Obj_t * pObj = Gia_ManObj( p, Id );
     word * pData0, * pDataA0, * pDataB0;
@@ -170,7 +170,7 @@ void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id )
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost )
+int Gia_ManInseHighestScore( Gia_Man_t * p, int * pCost )
 {
     Gia_Obj_t * pObj;
     word * pData0, * pData1;
@@ -195,7 +195,7 @@ int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost )
     ABC_FREE( pCounts );
     return iPat;
 }
-void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
+void Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs )
 {
     Gia_Obj_t * pObj;
     word * pData0, * pData1;
@@ -214,6 +214,53 @@ void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
         else 
             Vec_IntPush( vInit, 2 );
     }
+    Gia_ManForEachPi( p, pObj, k )
+    {
+        pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
+        pData1 = pData0 + p->iData;
+        for ( i = 0; i < p->iData; i++ )
+            assert( (pData0[i] & pData1[i]) == 0 );
+        if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
+            Vec_IntPush( vInputs, 0 );
+        else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
+            Vec_IntPush( vInputs, 1 );
+        else 
+            Vec_IntPush( vInputs, 2 );
+    }
+}
+Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit )
+{
+    Vec_Int_t * vRes;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
+    int i, f, iBit = 0;
+    assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
+    assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
+    assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
+    Gia_ManConst0(p)->fMark0 = 0;
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->fMark0 = Vec_IntEntry(vInit0, i);
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachRi( p, pObj, i )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == Vec_IntSize(vInputs) );
+    vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+        assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
+    Gia_ManForEachRo( p, pObj, i )
+        Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fMark0 = 0;
+    return vRes;
 }
 
 /**Function*************************************************************
@@ -227,18 +274,19 @@ void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
+Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
 {
-    Vec_Int_t * vInit;
+    Vec_Int_t * vRes, * vInit, * vInputs;
     Gia_Obj_t * pObj;
     int i, f, iPat, Cost, Cost0;
     abctime clk, clkTotal = Abc_Clock();
     Gia_ManRandomW( 1 );
     if ( fVerbose )
         printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
-    vInit = Vec_IntDup(vInit0);
+    vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
+    vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
     Gia_ParTestAlloc( p, nWords );
-    Gia_ManRoseInit( p, vInit );
+    Gia_ManInseInit( p, vInit );
     Cost0 = 0;
     Vec_IntForEachEntry( vInit, iPat, i )
         Cost0 += ((iPat >> 1) & 1);
@@ -248,233 +296,24 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames,
     {
         clk = Abc_Clock();
         Gia_ManForEachObj( p, pObj, i )
-            Gia_ManRoseSimulateObj( p, i );
-        iPat = Gia_ManRoseHighestScore( p, &Cost );
-        Gia_ManRoseFindStarting( p, vInit, iPat );
-        Gia_ManRoseInit( p, vInit );
+            Gia_ManInseSimulateObj( p, i );
+        iPat = Gia_ManInseHighestScore( p, &Cost );
+        Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
+        Gia_ManInseInit( p, vInit );
         if ( fVerbose )
             printf( "Frame =%6d : Values =%6d (out of %6d)   ", f+1, Cost, Cost0 );
         if ( fVerbose )
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
     Gia_ParTestFree( p );
-    printf( "After %d frames, found a sequence to produce %d x-values (out of %d).  ", f, Cost, Gia_ManRegNum(p) );
-    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
-//    printf( "The resulting init state is invalid.\n" );
+    vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
     Vec_IntFreeP( &vInit );
-    return vInit;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
-{
-    Cnf_Dat_t * pCnf;
-    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
-    pAig->nRegs = 0;
-    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
-    Aig_ManStop( pAig );
-    return pCnf;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
-{
-    Gia_Man_t * pNew, * pTemp;
-    Gia_Obj_t * pObj;
-    int i, f;
-    pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    Gia_ManHashAlloc( pNew );
-    Gia_ManConst0(p)->Value = 0;
-    // control/data variables
-    Gia_ManForEachRo( p, pObj, i )
-        Gia_ManAppendCi( pNew );
-    Gia_ManForEachRo( p, pObj, i )
-        Gia_ManAppendCi( pNew );
-    // build timeframes
-    assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
-    Gia_ManForEachRo( p, pObj, i )
-    {
-        if ( Vec_IntEntry(vInit, i) == 0 )
-            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
-        else if ( Vec_IntEntry(vInit, i) == 1 )
-            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1;
-        else if ( Vec_IntEntry(vInit, i) == 2 )
-            pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
-        else if ( Vec_IntEntry(vInit, i) == 3 )
-            pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
-        else assert( 0 );
-    }
-    for ( f = 0; f < nFrames; f++ )
-    {
-        Gia_ManForEachPi( p, pObj, i )
-            pObj->Value = Gia_ManAppendCi( pNew );
-        Gia_ManForEachAnd( p, pObj, i )
-            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        Gia_ManForEachRi( p, pObj, i )
-            pObj->Value = Gia_ObjFanin0Copy(pObj);
-        Gia_ManForEachRo( p, pObj, i )
-            pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
-    }
-    Gia_ManForEachRi( p, pObj, i )
-        pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
-    assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
-    return pNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
-{
-    int nIterMax = 1000000;
-    int i, iLit, Iter, status;
-    int nLits, * pLits;
-    abctime clkTotal = Abc_Clock();
-    abctime clkSat = 0;
-    Vec_Int_t * vLits, * vMap;
-    sat_solver * pSat;
-    Gia_Obj_t * pObj;
-    Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit );
-    Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit );
-    Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
-    Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
-    Gia_ManStop( p0 );
-    Gia_ManStop( p1 );
-    assert( Gia_ManRegNum(p) > 0 );
-    if ( fVerbose )
-        printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
-
-    pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars );
-    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
-    for ( i = 0; i < pCnf->nClauses; i++ )
-        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            assert( 0 );
-
-    // add one large OR clause
-    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
-    Gia_ManForEachCo( pM, pObj, i )
-        Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
-    sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
-
-    // create assumptions
-    Vec_IntClear( vLits );
-    Gia_ManForEachPi( pM, pObj, i )
-        if ( i == Gia_ManRegNum(p) )
-            break;
-        else if ( !(Vec_IntEntry(vInit, i) & 2) )
-            Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
-
-    if ( fVerbose )
-    {
-        printf( "Iter%6d : ",       0 );
-        printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
-        printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
-        printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
-        printf( "Subset =%6d  ",    Vec_IntSize(vLits) );
-        Abc_PrintTime( 1, "Time", clkSat );
-//      ABC_PRTr( "Solver time", clkSat );
-    }
-    for ( Iter = 0; Iter < nIterMax; Iter++ )
-    {
-        abctime clk = Abc_Clock();
-        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        clkSat += Abc_Clock() - clk;
-        if ( status == l_Undef )
-        {
-//            if ( fVerbose )
-//                printf( "\n" );
-            printf( "Timeout reached after %d seconds and %d iterations.  ", nTimeOut, Iter );
-            break;
-        }
-        if ( status == l_True )
-        {
-//            if ( fVerbose )
-//                printf( "\n" );
-            printf( "The problem is SAT after %d iterations.  ", Iter );
-            break;
-        }
-        assert( status == l_False );
-        nLits = sat_solver_final( pSat, &pLits );
-        if ( fVerbose )
-        {
-            printf( "Iter%6d : ",       Iter+1 );
-            printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
-            printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
-            printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
-            printf( "Subset =%6d  ",    nLits );
-            Abc_PrintTime( 1, "Time", clkSat );
-//            ABC_PRTr( "Solver time", clkSat );
-        }
-        if ( Vec_IntSize(vLits) == nLits )
-        {
-//            if ( fVerbose )
-//                printf( "\n" );
-            printf( "Reached fixed point with %d entries after %d iterations.  ", Vec_IntSize(vLits), Iter+1 );
-            break;
-        }
-        // collect used literals
-        Vec_IntClear( vLits );
-        for ( i = 0; i < nLits; i++ )
-            Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
-    }
-    // create map
-    vMap = Vec_IntStart( pCnf->nVars );
-    Vec_IntForEachEntry( vLits, iLit, i )
-        Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
-
-    // create output
-    Vec_IntFree( vLits );
-    vLits = Vec_IntDup(vInit);
-    Gia_ManForEachPi( pM, pObj, i )
-        if ( i == Gia_ManRegNum(p) )
-            break;
-        else if ( !(Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
-            Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
-    Vec_IntFree( vMap );
-
-    // cleanup
-    sat_solver_delete( pSat );
-    Cnf_DataFree( pCnf );
-    Gia_ManStop( pM );
+    Vec_IntFreeP( &vInputs );
+    printf( "After %d frames, found a sequence to produce %d x-values (out of %d).  ", f, Cost, Gia_ManRegNum(p) );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
-    return vLits;
+    return vRes;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -486,19 +325,11 @@ Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames,
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
+Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
 {
     Vec_Int_t * vRes, * vInit;
-    if ( fSim )
-    {
-        vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
-        vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose );
-    }
-    else
-    {
-        vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
-        vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose );
-    }
+    vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
+    vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
     if ( vInit != vInit0 )
         Vec_IntFree( vInit );
     return vRes;
diff --git a/src/sat/bmc/bmcMaxi.c b/src/sat/bmc/bmcMaxi.c
new file mode 100644
index 00000000..4a088016
--- /dev/null
+++ b/src/sat/bmc/bmcMaxi.c
@@ -0,0 +1,282 @@
+/**CFile****************************************************************
+
+  FileName    [bmcMaxi.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcMaxi.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
+{
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    pAig->nRegs = 0;
+    pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
+    Aig_ManStop( pAig );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManMaxiUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, f;
+    pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    // control/data variables
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ManAppendCi( pNew );
+    Gia_ManForEachRo( p, pObj, i )
+        Gia_ManAppendCi( pNew );
+    // build timeframes
+    assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        int Value = Vec_IntEntry( vInit, i );
+        int iCtrl = Gia_ManCiLit( pNew, i );
+        int iData = Gia_ManCiLit( pNew, Gia_ManRegNum(p)+i );
+        // decide based on Value
+        if ( Value == 0 )
+            pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, iCtrl, iData) : 0;
+        else if ( Value == 1 )
+            pObj->Value = fUseVars ? Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData) : 1;
+        else if ( Value == 2 )
+            pObj->Value = Gia_ManHashAnd(pNew, iCtrl, iData);
+        else if ( Value == 3 )
+            pObj->Value = Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData);
+        else if ( Value == 4 )
+            pObj->Value = 0;
+        else if ( Value == 5 )
+            pObj->Value = 1;
+        else assert( 0 );
+    }
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachRi( p, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        Gia_ManForEachRo( p, pObj, i )
+            pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
+    }
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManMaxiPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
+{
+    int nIterMax = 1000000;
+    int i, iLit, Iter, status;
+    int nLits, * pLits;
+    abctime clkTotal = Abc_Clock();
+    abctime clkSat = 0;
+    Vec_Int_t * vLits, * vMap;
+    sat_solver * pSat;
+    Gia_Obj_t * pObj;
+    Gia_Man_t * p0 = Gia_ManMaxiUnfold( p, nFrames, 0, vInit );
+    Gia_Man_t * p1 = Gia_ManMaxiUnfold( p, nFrames, 1, vInit );
+    Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
+    Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
+    Gia_ManStop( p0 );
+    Gia_ManStop( p1 );
+    assert( Gia_ManRegNum(p) > 0 );
+    if ( fVerbose )
+        printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
+
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
+
+    // add one large OR clause
+    vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
+    Gia_ManForEachCo( pM, pObj, i )
+        Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
+    sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+
+    // create assumptions
+    Vec_IntClear( vLits );
+    Gia_ManForEachPi( pM, pObj, i )
+        if ( i == Gia_ManRegNum(p) )
+            break;
+        else if ( Vec_IntEntry(vInit, i) == 0 || Vec_IntEntry(vInit, i) == 1 )
+            Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
+
+    if ( fVerbose )
+    {
+        printf( "Iter%6d : ",       0 );
+        printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
+        printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+        printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+        printf( "Subset =%6d  ",    Vec_IntSize(vLits) );
+        Abc_PrintTime( 1, "Time", clkSat );
+//      ABC_PRTr( "Solver time", clkSat );
+    }
+    for ( Iter = 0; Iter < nIterMax; Iter++ )
+    {
+        abctime clk = Abc_Clock();
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        clkSat += Abc_Clock() - clk;
+        if ( status == l_Undef )
+        {
+//            if ( fVerbose )
+//                printf( "\n" );
+            printf( "Timeout reached after %d seconds and %d iterations.  ", nTimeOut, Iter );
+            break;
+        }
+        if ( status == l_True )
+        {
+//            if ( fVerbose )
+//                printf( "\n" );
+            printf( "The problem is SAT after %d iterations.  ", Iter );
+            break;
+        }
+        assert( status == l_False );
+        nLits = sat_solver_final( pSat, &pLits );
+        if ( fVerbose )
+        {
+            printf( "Iter%6d : ",       Iter+1 );
+            printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
+            printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+            printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+            printf( "Subset =%6d  ",    nLits );
+            Abc_PrintTime( 1, "Time", clkSat );
+//            ABC_PRTr( "Solver time", clkSat );
+        }
+        if ( Vec_IntSize(vLits) == nLits )
+        {
+//            if ( fVerbose )
+//                printf( "\n" );
+            printf( "Reached fixed point with %d entries after %d iterations.  ", Vec_IntSize(vLits), Iter+1 );
+            break;
+        }
+        // collect used literals
+        Vec_IntClear( vLits );
+        for ( i = 0; i < nLits; i++ )
+            Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
+    }
+    // create map
+    vMap = Vec_IntStart( pCnf->nVars );
+    Vec_IntForEachEntry( vLits, iLit, i )
+        Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
+
+    // create output
+    Vec_IntFree( vLits );
+    vLits = Vec_IntDup(vInit);
+    Gia_ManForEachPi( pM, pObj, i )
+        if ( i == Gia_ManRegNum(p) )
+            break;
+        else if ( Vec_IntEntry(vLits, i) == 4 || Vec_IntEntry(vLits, i) == 5 )
+            Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) );
+        else if ( (Vec_IntEntry(vLits, i) == 0 || Vec_IntEntry(vLits, i) == 1) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
+            Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
+    Vec_IntFree( vMap );
+
+    // cleanup
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pM );
+    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
+    return vLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
+{
+    Vec_Int_t * vRes, * vInit;
+    vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
+    vRes = Gia_ManMaxiPerform( p, vInit, nFrames, nTimeOut, fVerbose );
+    if ( vInit != vInit0 )
+        Vec_IntFree( vInit );
+    return vRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index df8601e7..3ff4b100 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -2,6 +2,7 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc2.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcBmcAnd.c \
+    src/sat/bmc/bmcBmci.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \
@@ -9,8 +10,8 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcCexTools.c \
     src/sat/bmc/bmcFault.c \
     src/sat/bmc/bmcICheck.c \
-    src/sat/bmc/bmcLilac.c \
+    src/sat/bmc/bmcInse.c \
     src/sat/bmc/bmcLoad.c \
+    src/sat/bmc/bmcMaxi.c \
     src/sat/bmc/bmcMulti.c \
-    src/sat/bmc/bmcTulip.c \
     src/sat/bmc/bmcUnroll.c