Version abc80718

18 files changed, 452 insertions, 78 deletions

diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index b0f3b1fb..5f1f724f 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -66,7 +66,7 @@ struct Ntl_Man_t_
     char *             pName;          // the name of this design
     char *             pSpec;          // the name of input file
     Vec_Ptr_t *        vModels;        // the array of all models used to represent boxes
-    int                BoxTypes[15];   // the array of box types among the models
+    int                BoxTypes[32];   // the array of box types among the models
     // memory managers
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Aig_MmFlex_t *     pMemSops;       // memory for SOPs
@@ -225,6 +225,7 @@ static inline int         Ntl_BoxIsWhite( Ntl_Obj_t * p )         { assert( Ntl_
 static inline int         Ntl_BoxIsBlack( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite;   } 
 static inline int         Ntl_BoxIsComb( Ntl_Obj_t * p )          { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb;     } 
 static inline int         Ntl_BoxIsSeq( Ntl_Obj_t * p )           { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb;    } 
+static inline int         Ntl_BoxIsNoMerge( Ntl_Obj_t * p )       { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrNoMerge; } 
 
 static inline int         Ntl_ObjIsMapLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
 static inline int         Ntl_ObjIsMapRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 06a1a51c..dd481537 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -222,7 +222,7 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     printf( "inv/buf = %5d  ", Ntl_ModelLut1Num(pRoot) );
     printf( "box = %4d  ",     Ntl_ModelBoxNum(pRoot) );
     printf( "mod = %3d  ",     Vec_PtrSize(p->vModels) );
-    printf( "net = %d",       Ntl_ModelCountNets(pRoot) );
+    printf( "net = %d",        Ntl_ModelCountNets(pRoot) );
     printf( "\n" );
     fflush( stdout );
     assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
@@ -262,10 +262,11 @@ void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
     Ntl_Mod_t * pModel = pObj->pImplem;
     int Number = 0;
     assert( Ntl_ObjIsBox(pObj) );
-    Number |= (pModel->attrWhite << 0);
-    Number |= (pModel->attrBox   << 1);
-    Number |= (pModel->attrComb  << 2);
-    Number |= (pModel->attrKeep  << 3);
+    Number |= (pModel->attrWhite   << 0);
+    Number |= (pModel->attrBox     << 1);
+    Number |= (pModel->attrComb    << 2);
+    Number |= (pModel->attrKeep    << 3);
+    Number |= (pModel->attrNoMerge << 4);
     pModel->pMan->BoxTypes[Number]++;
 }
 
@@ -291,19 +292,20 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
     printf( "BOX STATISTICS:\n" );
     Ntl_ModelForEachBox( pModel, pObj, i )
         Ntl_ManSaveBoxType( pObj );
-    for ( i = 0; i < 15; i++ )
+    for ( i = 0; i < 32; i++ )
     {
         if ( !p->BoxTypes[i] )
             continue;
         printf( "%5d :", p->BoxTypes[i] );
-        printf( " %s", ((i & 1) > 0)? "white": "black" );
-        printf( " %s", ((i & 2) > 0)? "box  ": "logic" );
-        printf( " %s", ((i & 4) > 0)? "comb ": "seq  " );
-        printf( " %s", ((i & 8) > 0)? "keep ": "sweep" );
+        printf( " %s", ((i &  1) > 0)? "white   ": "black   " );
+        printf( " %s", ((i &  2) > 0)? "box     ": "logic   " );
+        printf( " %s", ((i &  4) > 0)? "comb    ": "seq     " );
+        printf( " %s", ((i &  8) > 0)? "keep    ": "sweep   " );
+        printf( " %s", ((i & 16) > 0)? "no_merge": "merge   " );
         printf( "\n" );
     }
     printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
-    for ( i = 0; i < 15; i++ )
+    for ( i = 0; i < 32; i++ )
         p->BoxTypes[i] = 0;
 }
 
@@ -366,6 +368,11 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    pModelNew->attrWhite   = pModelOld->attrWhite;
+    pModelNew->attrBox       = pModelOld->attrBox;
+    pModelNew->attrComb       = pModelOld->attrComb;
+    pModelNew->attrKeep       = pModelOld->attrKeep;
+    pModelNew->attrNoMerge = pModelOld->attrNoMerge;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
     {
         if ( Ntl_ObjIsNode(pObj) )
@@ -423,10 +430,11 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
-    pModelNew->attrWhite = pModelOld->attrWhite;
-    pModelNew->attrBox     = pModelOld->attrBox;
-    pModelNew->attrComb     = pModelOld->attrComb;
-    pModelNew->attrKeep     = pModelOld->attrKeep;
+    pModelNew->attrWhite   = pModelOld->attrWhite;
+    pModelNew->attrBox       = pModelOld->attrBox;
+    pModelNew->attrComb       = pModelOld->attrComb;
+    pModelNew->attrKeep       = pModelOld->attrKeep;
+    pModelNew->attrNoMerge = pModelOld->attrNoMerge;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
         pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
     Ntl_ModelForEachNet( pModelOld, pNet, i )
@@ -504,10 +512,11 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
     // create model
     sprintf( Name, "%s%d", "latch", Init );
     pModel = Ntl_ModelAlloc( pMan, Name );
-    pModel->attrWhite = 1;
-    pModel->attrBox   = 1;
-    pModel->attrComb  = 0;
-    pModel->attrKeep  = 0;
+    pModel->attrWhite   = 1;
+    pModel->attrBox     = 1;
+    pModel->attrComb    = 0;
+    pModel->attrKeep    = 0;
+    pModel->attrNoMerge = 0;
     // create primary input
     pObj = Ntl_ModelCreatePi( pModel );
     pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" );
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 6eb2cc95..30f972c8 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -878,14 +878,14 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
             p->pNtk->attrBox = 1;
         else if ( strcmp( pToken, "logic" ) == 0 )
             p->pNtk->attrBox = 0;
-        else if ( strcmp( pToken, "white" ) == 0 )
-            p->pNtk->attrWhite = 1;
         else if ( strcmp( pToken, "comb" ) == 0 )
             p->pNtk->attrComb = 1;
         else if ( strcmp( pToken, "seq" ) == 0 )
             p->pNtk->attrComb = 0;
         else if ( strcmp( pToken, "keep" ) == 0 )
             p->pNtk->attrKeep = 1;
+        else if ( strcmp( pToken, "sweep" ) == 0 )
+            p->pNtk->attrKeep = 0;
         else 
         {
             sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName );
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 623fa3a6..9c8d55ae 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -66,6 +66,8 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
 //        fprintf( pFile, " %s", pModel->attrKeep?  "keep" : "sweep" );
         fprintf( pFile, "\n" );
     }
+    if ( pModel->attrNoMerge )
+        fprintf( pFile, ".no_merge\n" );
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 08275ff3..4ae07063 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -85,7 +85,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
index 527f372d..37eb3349 100644
--- a/src/aig/saig/saigInter.c
+++ b/src/aig/saig/saigInter.c
@@ -65,6 +65,8 @@ struct Saig_IntMan_t_
     int              timeTotal;
 };
 
+static int Saig_M144pPerformOneStep( Saig_IntMan_t * p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -331,6 +333,7 @@ sat_solver * Saig_DeriveSatSolver(
     sat_solver_store_mark_roots( pSat );
     // return clauses to the original state
     Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
     return pSat;
 }
 
@@ -727,6 +730,103 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
     free( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Check inductive containment.]
+
+  Description [Given interpolant I and transition relation T, here we
+  check that I(x) * T(x,y) => T(y). ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p )
+{
+    sat_solver * pSat;
+    Aig_Man_t * pInterOld = p->pInter;
+    Aig_Man_t * pInterNew = p->pInterNew;
+    Aig_Man_t * pTrans    = p->pAigTrans;
+    Cnf_Dat_t * pCnfOld   = p->pCnfInter;
+    Cnf_Dat_t * pCnfNew   = Cnf_Derive( p->pInterNew, 0 ); 
+    Cnf_Dat_t * pCnfTrans = p->pCnfAig;
+    Aig_Obj_t * pObj, * pObj2;
+    int status, i, Lits[2];
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars );
+
+    // interpolant
+    for ( i = 0; i < pCnfNew->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
+            assert( 0 );
+    }
+
+    // connector clauses
+    Cnf_DataLift( pCnfTrans, pCnfNew->nVars );
+    Aig_ManForEachPi( pInterNew, pObj, i )
+    {
+        pObj2 = Saig_ManLo( pTrans, i );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfTrans->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfTrans->pClauses[i], pCnfTrans->pClauses[i+1] ) )
+            assert( 0 );
+    }
+
+    // connector clauses
+    Cnf_DataLift( pCnfNew, pCnfNew->nVars + pCnfTrans->nVars );
+    Aig_ManForEachPi( pInterNew, pObj, i )
+    {
+        pObj2 = Saig_ManLi( pTrans, i );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+
+    // complement the last literal
+    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
+    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
+    // add clauses of B
+    for ( i = 0; i < pCnfNew->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // complement the last literal
+    Lits[0] = pCnfNew->pClauses[0][pCnfNew->nLiterals-1];
+    pCnfNew->pClauses[0][pCnfNew->nLiterals-1] = lit_neg(Lits[0]);
+
+    // return clauses to the original state
+    Cnf_DataLift( pCnfTrans, -pCnfNew->nVars );
+    Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars );
+    Cnf_DataFree( pCnfNew );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    sat_solver_delete( pSat );
+    return status == l_False;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Interplates while the number of conflicts is not exceeded.]
@@ -738,7 +838,7 @@ void Saig_ManagerFree( Saig_IntMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fUseIp, int fVerbose, int * pDepth )
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUseIp, int fCheckInd, int fVerbose, int * pDepth )
 {
     Saig_IntMan_t * p;
     Aig_Man_t * pAigTemp;
@@ -809,17 +909,20 @@ p->timeCnf += clock() - clk;
         // iterate the interpolation procedure
         for ( i = 0; ; i++ )
         {
-            if ( p->nFrames + i >= 75 )
+            if ( p->nFrames + i >= nFramesMax )
             {
                 if ( fVerbose )
-                    printf( "Reached limit (%d) on the number of timeframes.\n", 75 );
+                    printf( "Reached limit (%d) on the number of timeframes.\n", nFramesMax );
                 p->timeTotal = clock() - clkTotal;
                 Saig_ManagerFree( p );
                 return -1;
             }
             // perform interplation
             clk = clock();
-            RetValue = Saig_PerformOneStep( p, fUseIp );
+            if ( fUseIp )
+                RetValue = Saig_M144pPerformOneStep( p );
+            else
+                RetValue = Saig_PerformOneStep( p, 0 );
             if ( fVerbose )
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
@@ -859,7 +962,10 @@ clk = clock();
 p->timeRwr += clock() - clk;
             // check containment of interpolants
 clk = clock();
-            Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
+            if ( fCheckInd )
+                Status = Saig_ManCheckInductiveContainment( p );
+            else
+                Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
 p->timeEqu += clock() - clk;
             if ( Status ) // contained
             {
@@ -897,6 +1003,232 @@ p->timeCnf += clock() - clk;
     return RetValue;
 }
 
+
+#include "m114p.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the SAT solver for one interpolation run.]
+
+  Description [pInter is the previous interpolant. pAig is one time frame.
+  pFrames is the unrolled time frames.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+M114p_Solver_t Saig_M144pDeriveSatSolver( 
+    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
+    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
+    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
+    Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
+{
+    M114p_Solver_t pSat;
+    Aig_Obj_t * pObj, * pObj2;
+    int i, Lits[2];
+
+    // sanity checks
+    assert( Aig_ManRegNum(pInter) == 0 );
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pFrames) == 0 );
+    assert( Aig_ManPoNum(pInter) == 1 );
+    assert( Aig_ManPoNum(pFrames) == 1 );
+    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+
+    // prepare CNFs
+    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
+
+    *pvMapRoots = Vec_IntAlloc( 10000 );
+    *pvMapVars = Vec_IntAlloc( 0 );
+    Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
+    for ( i = 0; i < pCnfFrames->nVars; i++ )
+        Vec_IntWriteEntry( *pvMapVars, i, -2 );
+
+    // start the solver
+    pSat = M114p_SolverNew( 1 );
+    M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+    // add clauses of A
+    // interpolant
+    for ( i = 0; i < pCnfInter->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pInter, pObj, i )
+    {
+        pObj2 = Saig_ManLo( pAig, i );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfAig->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pFrames, pObj, i )
+    {
+        if ( i == Aig_ManRegNum(pAig) )
+            break;
+//        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+        Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
+
+        pObj2 = Saig_ManLi( pAig, i );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // add clauses of B
+    for ( i = 0; i < pCnfFrames->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 1 );
+        if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // return clauses to the original state
+    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, iVar;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+    // process root clauses
+    p = Aig_ManStart( 10000 );
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+        {
+            pInter = Aig_ManConst0(p);
+            for ( k = 0; k < nLits; k++ )
+            {
+                iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
+                if ( iVar < 0 ) // var of A or B
+                    continue;
+                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
+                pInter = Aig_Or( p, pInter, pVar );
+            }
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 );
+            else // var of B or C
+                pInter = Aig_And( p, pInter, pInter2 );
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    Vec_PtrFree( vInters );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_M144pPerformOneStep( Saig_IntMan_t * p )
+{
+    M114p_Solver_t pSat;
+    Vec_Int_t * vMapRoots, * vMapVars;
+    int clk, status, RetValue;
+    assert( p->pInterNew == NULL );
+    // derive the SAT solver
+    pSat = Saig_M144pDeriveSatSolver( p->pInter, p->pCnfInter, 
+        p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, 
+        &vMapRoots, &vMapVars );
+    // solve the problem
+clk = clock();
+    status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
+    p->nConfCur = M114p_SolverGetConflictNum( pSat );
+p->timeSat += clock() - clk;
+    if ( status == 0 )
+    {
+        RetValue = 1;
+clk = clock();
+        p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars );
+p->timeInt += clock() - clk;
+    }
+    else if ( status == 1 )
+    {
+        RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+    }
+    M114p_SolverDelete( pSat );
+    Vec_IntFree( vMapRoots );
+    Vec_IntFree( vMapVars );
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d1aa2c82..cb3d2d86 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15343,12 +15343,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int nBTLimit;
+    int nFramesMax;
     int fRewrite;
     int fTransLoop;
     int fUsePudlak;
+    int fCheckInd;
     int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -15356,12 +15358,14 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nBTLimit   = 20000;
+    nFramesMax = 40;
     fRewrite   = 0;
     fTransLoop = 1;
     fUsePudlak = 0;
+    fCheckInd  = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpivh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15376,6 +15380,17 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesMax < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -15385,6 +15400,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fUsePudlak ^= 1;
             break;
+        case 'i':
+            fCheckInd ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -15414,16 +15432,18 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" );
+    fprintf( pErr, "usage: int [-CF num] [-rtpivh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
     fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
+    fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a691a205..e47582e9 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fCheckInd, int fVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth );
+    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fCheckInd, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 6f2e1d11..bfa91ddc 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -55,11 +55,9 @@ int main( int argc, char * argv[] )
     bool fBatch, fInitSource, fInitRead, fFinalWrite;
 
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     
 //    Npn_Experiment();
 //    Npn_Generate();
@@ -256,11 +254,9 @@ void Abc_Start()
 {
     Abc_Frame_t * pAbc;
     // added to detect memory leaks:
-#ifdef _DEBUG
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
     _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
 #endif
-#endif
     // start the glocal frame
     pAbc = Abc_FrameGetGlobalFrame();
     // source the resource file
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/pcm/module.make
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/src/map/ply/module.make
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index f45afcbe..d63ed5d3 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -43,7 +43,7 @@ extern "C" {
 
 // this include should be the first one in the list
 // it is used to catch memory leaks on Windows
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
 #include "leaks.h"
 #endif
 
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 03de79f1..4c19b5ee 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -50,7 +50,7 @@ typedef long long          sint64;
 
 // this include should be the first one in the list
 // it is used to catch memory leaks on Windows
-#ifdef ABC_CHECK_LEAKS
+#if defined(_DEBUG) && defined(_MSC_VER) && (_MSC_VER <= 1200) // 1200 = MSVC 6.0
 #include "leaks.h"       
 #endif
 
diff --git a/src/misc/zlib/1.c b/src/misc/zlib/1.c
deleted file mode 100644
index 8a06a346..00000000
--- a/src/misc/zlib/1.c
+++ /dev/null
@@ -1,35 +0,0 @@
- Volume in drive C is IBM_PRELOAD
- Volume Serial Number is 20EA-F780
-
- Directory of C:\_projects\abc\src\misc\zlib
-
-07/02/2008  03:51 PM    <DIR>          .
-07/02/2008  03:51 PM    <DIR>          ..
-07/02/2008  03:51 PM                 0 1.c
-12/21/2004  04:52 PM             4,708 adler32.c
-06/02/2003  06:16 AM             9,545 algorithm.txt
-07/07/2003  07:37 AM             2,568 compress_.c
-06/13/2005  01:56 AM            13,616 crc32.c
-01/05/2003  04:53 PM            31,009 crc32.h
-07/18/2005  04:27 AM            65,899 deflate.c
-05/29/2005  05:55 PM            12,445 deflate.h
-07/11/2005  10:31 PM            32,129 gzio.c
-05/31/2005  12:58 AM            22,787 infback.c
-11/13/2004  06:05 AM            12,886 inffast.c
-01/01/2003  05:46 PM               418 inffast.h
-11/24/2002  11:44 PM             6,437 inffixed.h
-06/14/2005  11:50 PM            50,345 inflate.c
-11/13/2004  05:38 AM             6,031 inflate.h
-07/18/2005  04:27 AM            14,085 inftrees.c
-07/11/2005  08:50 AM             2,428 inftrees.h
-07/02/2008  02:52 PM                34 link.txt
-07/18/2005  04:25 AM             5,821 README
-06/13/2005  02:34 AM            45,246 trees.c
-02/24/1998  12:14 PM             8,572 trees.h
-07/07/2003  07:36 AM             2,148 uncompr.c
-05/28/2005  08:40 AM             9,876 zconf.h
-07/18/2005  04:26 AM            67,545 zlib.h
-06/13/2005  02:37 AM             7,454 zutil.c
-07/11/2005  10:35 PM             7,128 zutil.h
-              26 File(s)        441,160 bytes
-               2 Dir(s)   1,641,279,488 bytes free
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index cc780580..5837e68f 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -941,7 +941,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     // stop the proof
     if ( p->fProofWrite )
-    {
+    { 
         fclose( p->pFile );
         p->pFile = NULL;    
     }
diff --git a/src/sat/psat/m114p.h b/src/sat/psat/m114p.h
new file mode 100644
index 00000000..5050cb4b
--- /dev/null
+++ b/src/sat/psat/m114p.h
@@ -0,0 +1,39 @@
+// C-language header for MiniSat 1.14p
+
+#ifndef m114p_h
+#define m114p_h
+
+#include "m114p_types.h"
+
+// SAT solver APIs
+extern M114p_Solver_t M114p_SolverNew( int fRecordProof );
+extern void           M114p_SolverDelete( M114p_Solver_t s );
+extern void           M114p_SolverPrintStats( M114p_Solver_t s, double Time );
+extern void           M114p_SolverSetVarNum( M114p_Solver_t s, int nVars );
+extern int            M114p_SolverAddClause( M114p_Solver_t s, lit* begin, lit* end );
+extern int            M114p_SolverSimplify( M114p_Solver_t s );
+extern int            M114p_SolverSolve( M114p_Solver_t s, lit* begin, lit* end, int nConfLimit );
+extern int            M114p_SolverGetConflictNum( M114p_Solver_t s );
+
+// proof status APIs
+extern int            M114p_SolverProofIsReady( M114p_Solver_t s );
+extern void           M114p_SolverProofSave( M114p_Solver_t s, char * pFileName );
+extern int            M114p_SolverProofClauseNum( M114p_Solver_t s );
+
+// proof traversal APIs
+extern int            M114p_SolverGetFirstRoot( M114p_Solver_t s, int ** ppLits );
+extern int            M114p_SolverGetNextRoot( M114p_Solver_t s, int ** ppLits );
+extern int            M114p_SolverGetFirstChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars );
+extern int            M114p_SolverGetNextChain( M114p_Solver_t s, int ** ppClauses, int ** ppVars );
+
+// iterator over the root clauses (should be called first)
+#define M114p_SolverForEachRoot( s, ppLits, nLits, i )                           \
+    for ( i = 0, nLits = M114p_SolverGetFirstRoot(s, ppLits); nLits;             \
+          i++, nLits = M114p_SolverGetNextRoot(s, ppLits) )
+
+// iterator over the learned clauses (should be called after iterating over roots)
+#define M114p_SolverForEachChain( s, ppClauses, ppVars, nVars, i )               \
+    for ( i = 0, nVars = M114p_SolverGetFirstChain(s, ppClauses, ppVars); nVars; \
+          i++, nVars = M114p_SolverGetNextChain(s, ppClauses, ppVars) )
+
+#endif
\ No newline at end of file
diff --git a/src/sat/psat/m114p_types.h b/src/sat/psat/m114p_types.h
new file mode 100644
index 00000000..54a20c5c
--- /dev/null
+++ b/src/sat/psat/m114p_types.h
@@ -0,0 +1,9 @@
+// C-language header for MiniSat 1.14p
+
+#ifndef m114p_types_h
+#define m114p_types_h
+
+typedef int   M114p_Solver_t;
+typedef int   lit;
+
+#endif
\ No newline at end of file
diff --git a/src/sat/psat/module.make b/src/sat/psat/module.make
new file mode 100644
index 00000000..d6d908e7
--- /dev/null
+++ b/src/sat/psat/module.make
@@ -0,0 +1 @@
+SRC +=