Version abc80718

6 files changed, 372 insertions, 28 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                                ///
 ////////////////////////////////////////////////////////////////////////