Version abc80510

abc.dsp

@@ -3254,6 +3254,10 @@ SOURCE=.\src\aig\saig\saig.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\saig\saigInter.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\saig\saigPhase.c
 # End Source File
 # Begin Source File

abc.rc

@@ -133,4 +133,6 @@ alias pjsolve   "scl; dc2; fr; dc2; ic; ic -t; if -a; cs tacas/005_care.aig; mfs
 alias t0        "r test/mc1.blif; st; test"
 alias t1        "r s27mc2.blif; st; test"
 alias t2        "r i/intel_001.aig; ps; indcut -v"
+alias t         "r c\s\0\000.aig; int"
+#alias t         "r test/interpol.blif; st; int"
 

src/aig/aig/aig.h

@@ -64,7 +64,7 @@ typedef enum {
 } Aig_Type_t;
 
 // the AIG node
-struct Aig_Obj_t_  // 8 words
+struct Aig_Obj_t_  // 9 words
 {
     union {                         
         Aig_Obj_t *  pNext;          // strashing table
@@ -477,6 +477,7 @@ extern Aig_Man_t *     Aig_ManDupLevelized( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepresDfs( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
@@ -524,6 +525,7 @@ extern Aig_Obj_t *     Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
 extern Aig_Obj_t *     Aig_Exor( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 );
 extern Aig_Obj_t *     Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 );
 extern Aig_Obj_t *     Aig_Maj( Aig_Man_t * p, Aig_Obj_t * pA, Aig_Obj_t * pB, Aig_Obj_t * pC );
+extern Aig_Obj_t *     Aig_Multi( Aig_Man_t * p, Aig_Obj_t ** pArgs, int nArgs, Aig_Type_t Type );
 extern Aig_Obj_t *     Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs );
 extern Aig_Obj_t *     Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes2 );
 extern Aig_Obj_t *     Aig_CreateAnd( Aig_Man_t * p, int nVars );

src/aig/aig/aigDup.c

@@ -732,6 +732,61 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the miter of the two AIG managers.]
+
+  Description [Oper is the operation to perform on the outputs of the miter.
+  Oper == 0 is XOR
+  Oper == 1 is complemented implication (p1 => p2)
+  Oper == 2 is OR
+  Oper == 3 is AND
+  ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManRegNum(p1) == 0 );
+    assert( Aig_ManRegNum(p2) == 0 );
+    assert( Aig_ManPoNum(p1) == 1 );
+    assert( Aig_ManPoNum(p2) == 1 );
+    assert( Aig_ManPiNum(p1) == Aig_ManPiNum(p2) );
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
+    // add first AIG
+    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p1, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachNode( p1, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add second AIG
+    Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p2, pObj, i )
+        pObj->pData = Aig_ManPi( pNew, i );
+    Aig_ManForEachNode( p2, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the output
+    if ( Oper == 0 ) // XOR
+        pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
+    else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2)  ...  complement is PO(p1) & !PO(p2) 
+        pObj = Aig_And( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) );
+    else if ( Oper == 2 ) // OR
+        pObj = Aig_Or( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
+    else if ( Oper == 3 ) // AND
+        pObj = Aig_And( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1,0)), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
+    else
+        assert( 0 );
+    Aig_ObjCreatePo( pNew, pObj );
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/aig/aigMan.c

@@ -216,7 +216,7 @@ void Aig_ManStop( Aig_Man_t * p )
     FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
-//    free( p->pTable );
+    free( p->pTable );
     free( p );
 }
 

src/aig/aig/aigObj.c

@@ -370,6 +370,11 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     // make sure object is not pointing to itself
     assert( pObjOld != Aig_ObjFanin0(pObjNewR) );
     assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
+    if ( pObjOld == Aig_ObjFanin0(pObjNewR) || pObjOld == Aig_ObjFanin1(pObjNewR) )
+    {
+        printf( "Aig_ObjReplace(): Internal error!\n" );
+        exit(1);
+    }
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
     if ( !Aig_ObjIsPi(pObjOld) )

src/aig/cnf/cnf.h

@@ -136,8 +136,9 @@ extern Cnf_Dat_t *     Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses,
 extern Cnf_Dat_t *     Cnf_DataDup( Cnf_Dat_t * p );
 extern void            Cnf_DataFree( Cnf_Dat_t * p );
 extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
+extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
-void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
 extern void            Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );

src/aig/cnf/cnfMan.c

@@ -212,6 +212,31 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
   SeeAlso     []
 
 ***********************************************************************/
+void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable )
+{
+    FILE * pFile = stdout;
+    int * pLit, * pStop, i;
+    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
+    for ( i = 0; i < p->nClauses; i++ )
+    {
+        for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
+            fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
+        fprintf( pFile, "\n" );
+    }
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes CNF into a file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
 {
     FILE * pFile;

src/aig/ntl/ntl.h

@@ -98,6 +98,7 @@ struct Ntl_Mod_t_
     float *            pDelayTable;   
     // other data members
     void *             pCopy;
+    int                nUsed, nRems;
 }; 
 
 struct Ntl_Obj_t_
@@ -186,12 +187,12 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#define Ntl_ManForEachModel( p, pNtl, i )                                       \
-    Vec_PtrForEachEntry( p->vModels, pNtl, i )
-#define Ntl_ManForEachCiNet( p, pNtl, i )                                       \
-    Vec_PtrForEachEntry( p->vCis, pNtl, i )
-#define Ntl_ManForEachCoNet( p, pNtl, i )                                       \
-    Vec_PtrForEachEntry( p->vCos, pNtl, i )
+#define Ntl_ManForEachModel( p, pMod, i )                                       \
+    Vec_PtrForEachEntry( p->vModels, pMod, i )
+#define Ntl_ManForEachCiNet( p, pNet, i )                                       \
+    Vec_PtrForEachEntry( p->vCis, pNet, i )
+#define Ntl_ManForEachCoNet( p, pNet, i )                                       \
+    Vec_PtrForEachEntry( p->vCos, pNet, i )
 #define Ntl_ManForEachNode( p, pObj, i )                                   \
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else

src/aig/ntl/ntlSweep.c

@@ -97,11 +97,11 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
 int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
 {
     int nObjsOld[NTL_OBJ_VOID];
-    Ntl_Mod_t * pRoot;
+    Ntl_Mod_t * pRoot, * pMod;
     Ntl_Net_t * pNet;
     Ntl_Obj_t * pObj;
     int i, k, nNetsOld;
-    int Counter = 0;
+    int ModelCounter = 0, Counter = 0;
 
     // remember the number of objects
     pRoot = Ntl_ManRootModel( p );
@@ -112,6 +112,23 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
     // mark the nets that do not fanout into POs
     Ntl_ManSweepMark( p );
 
+    // count how many boxes of each type are swept away
+    if ( fVerbose )
+    {
+    Ntl_ManForEachModel( p, pMod, i )
+        pMod->nUsed = pMod->nRems = 0;
+    Ntl_ModelForEachObj( pRoot, pObj, i )
+        if ( Ntl_ObjIsBox(pObj) && pObj->pImplem )
+        {
+            pObj->pImplem->nUsed++;
+            if ( !pObj->fMark )
+            {
+                if ( pObj->pImplem->nRems++ == 0 )
+                    ModelCounter++;
+            }
+        }
+    }
+
     // remove the useless objects and their nets
     Ntl_ModelForEachObj( pRoot, pObj, i )
     {
@@ -134,6 +151,8 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
         Counter++;
     }
 
+
+
     // print detailed statistics of sweeping
     if ( fVerbose )
     {
@@ -151,6 +170,14 @@ int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose )
             nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX],
             !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] );
         printf( "\n" );
+        if ( ModelCounter )
+        {
+            printf( "Sweep removed %d boxed of %d types (out of %d types):\n", 
+                nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX], ModelCounter, Vec_PtrSize(p->vModels)-1 );
+            Ntl_ManForEachModel( p, pMod, i )
+              if ( i )
+                printf( "Model %3d : %-40s  Swept = %5d. Left = %5d.\n", i, pMod->pName, pMod->nRems, pMod->nUsed-pMod->nRems );
+        }
     }
     if ( !Ntl_ManCheck( p ) )
         printf( "Ntl_ManSweep: The check has failed for design %s.\n", p->pName );

src/aig/saig/module.make

 SRC +=    src/aig/saig/saig_.c \
+    src/aig/saig/saigInter.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
     src/aig/saig/saigRetMin.c \

src/aig/saig/saig.h

@@ -75,6 +75,8 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== saigInter.c ==========================================================*/
+extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDepth );
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/

src/aig/saig/saigInter.c

+/**CFile****************************************************************
+
+  FileName    [saigInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Interplation for unbounded model checking.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "fra.h"
+#include "cnf.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+/* 
+    The interpolation algorithm implemented here was introduced in the paper:
+    K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
+*/
+
+
+// simulation manager
+typedef struct Saig_IntMan_t_ Saig_IntMan_t;
+struct Saig_IntMan_t_
+{
+    // AIG manager
+    Aig_Man_t *      pAig;         // the original AIG manager
+    Aig_Man_t *      pAigTrans;    // the transformed original AIG manager
+    Cnf_Dat_t *      pCnfAig;      // CNF for the original manager
+    // interpolant
+    Aig_Man_t *      pInter;       // the current interpolant
+    Cnf_Dat_t *      pCnfInter;    // CNF for the current interplant
+    // timeframes
+    Aig_Man_t *      pFrames;      // the timeframes      
+    Cnf_Dat_t *      pCnfFrames;   // CNF for the timeframes 
+    // other data
+    Vec_Int_t *      vVarsAB;      // the variables participating in 
+    // temporary place for the new interpolant
+    Aig_Man_t *      pInterNew;
+    // parameters
+    int              nFrames;      // the number of timeframes
+    int              nConfCur;     // the current number of conflicts
+    int              nConfLimit;   // the limit on the number of conflicts
+    int              fVerbose;     // the verbosiness flag
+    // runtime
+    int              timeRwr;
+    int              timeCnf;
+    int              timeSat;
+    int              timeInt;
+    int              timeEqu;
+    int              timeOther;
+    int              timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create trivial AIG manager for the init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManInit( int nRegs )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pRes;
+    Aig_Obj_t ** ppInputs;
+    int i;
+    assert( nRegs > 0 );
+    ppInputs = ALLOC( Aig_Obj_t *, nRegs );
+    p = Aig_ManStart( nRegs );
+    for ( i = 0; i < nRegs; i++ )
+        ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
+    pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
+    Aig_ObjCreatePo( p, pRes );
+    free( ppInputs );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the AIG w/o POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDuplicated( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // set registers
+    pNew->nRegs    = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = 0;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create register inputs with MUXes
+    Saig_ManForEachLi( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the AIG w/o POs and transforms to transit into init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pCtrl;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( i == Saig_ManPiNum(p) )
+            pCtrl = Aig_ObjCreatePi( pNew );
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    }
+    // set registers
+    pNew->nRegs    = p->nRegs;
+    pNew->nTruePis = p->nTruePis + 1;
+    pNew->nTruePos = 0;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create register inputs with MUXes
+    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+    {
+        pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+        Aig_ObjCreatePo( pNew, pObj );
+    }
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for interpolation.]
+
+  Description [The resulting manager is combinational. The primary inputs
+  corresponding to register outputs are ordered first. The only POs of the 
+  manager is the property output of the last timeframe.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesInter( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManPoNum(pAig) == 1 );
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    // create the only PO of the manager
+    pObj = Aig_ManPo( pAig, 0 );
+    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**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     []
+
+***********************************************************************/
+sat_solver * Saig_DeriveSatSolver( 
+    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 * vVarsAB )
+{
+    sat_solver * 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 );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat );
+    sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+    // add clauses of A
+    // interpolant
+    for ( i = 0; i < pCnfInter->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( 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 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfAig->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Vec_IntClear( vVarsAB );
+    Aig_ManForEachPi( pFrames, pObj, i )
+    {
+        if ( i == Aig_ManRegNum(pAig) )
+            break;
+        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+
+        pObj2 = Saig_ManLi( pAig, i );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // add clauses of B
+    sat_solver_store_mark_clauses_a( pSat );
+    for ( i = 0; i < pCnfFrames->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    sat_solver_store_mark_roots( pSat );
+    // return clauses to the original state
+    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_PerformOneStep( Saig_IntMan_t * p )
+{
+    sat_solver * pSat;
+    void * pSatCnf = NULL;
+    Inta_Man_t * pManInter; 
+    int clk, status, RetValue;
+    assert( p->pInterNew == NULL );
+
+    // derive the SAT solver
+    pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB );
+Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 );
+    // solve the problem
+clk = clock();
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    p->nConfCur = pSat->stats.conflicts;
+p->timeSat += clock() - clk;
+    if ( status == l_False )
+    {
+        pSatCnf = sat_solver_store_release( pSat );
+        RetValue = 1;
+    }
+    else if ( status == l_True )
+    {
+        RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+    }
+    sat_solver_delete( pSat );
+    if ( pSatCnf == NULL )
+        return RetValue;
+
+    // create the resulting manager
+clk = clock();
+    pManInter = Inta_ManAlloc();
+    p->pInterNew = Inta_ManInterpolate( pManInter, pSatCnf, p->vVarsAB, 0 );
+    Inta_ManFree( pManInter );
+p->timeInt += clock() - clk;
+    Sto_ManFree( pSatCnf );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks constainment of two interpolants.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
+{
+    Aig_Man_t * pMiter, * pAigTemp;
+    int RetValue;
+    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
+    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
+    Aig_ManStop( pAigTemp );
+    RetValue = Fra_FraigMiterStatus( pMiter );
+    if ( RetValue == -1 )
+    {
+        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
+        RetValue = Fra_FraigMiterStatus( pAigTemp );
+        Aig_ManStop( pAigTemp );
+    }
+    assert( RetValue != -1 );
+    Aig_ManStop( pMiter );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManagerClean( Saig_IntMan_t * p )
+{
+    if ( p->pCnfInter )
+        Cnf_DataFree( p->pCnfInter );
+    if ( p->pCnfFrames )
+        Cnf_DataFree( p->pCnfFrames );
+    if ( p->pInter )
+        Aig_ManStop( p->pInter );
+    if ( p->pFrames )
+        Aig_ManStop( p->pFrames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManagerFree( Saig_IntMan_t * p )
+{
+    if ( p->fVerbose )
+    {
+        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
+        printf( "Runtime statistics:\n" );
+        PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
+        PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
+        PRTP( "SAT solving", p->timeSat,   p->timeTotal );
+        PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
+        PRTP( "Containment", p->timeEqu,   p->timeTotal );
+        PRTP( "Other      ", p->timeOther, p->timeTotal );
+        PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
+    }
+
+    if ( p->pCnfAig )
+        Cnf_DataFree( p->pCnfAig );
+    if ( p->pCnfFrames )
+        Cnf_DataFree( p->pCnfFrames );
+    if ( p->pCnfInter )
+        Cnf_DataFree( p->pCnfInter );
+    Vec_IntFree( p->vVarsAB );
+    if ( p->pAigTrans )
+        Aig_ManStop( p->pAigTrans );
+    if ( p->pFrames )
+        Aig_ManStop( p->pFrames );
+    if ( p->pInter )
+        Aig_ManStop( p->pInter );
+    if ( p->pInterNew )
+        Aig_ManStop( p->pInterNew );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interplates while the number of conflicts is not exceeded.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects [Does not check the property in 0-th frame.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fVerbose, int * pDepth )
+{
+    int fUseTransRel = 0;
+    Saig_IntMan_t * p;
+    Aig_Man_t * pAigTemp;
+    int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
+
+    // sanity checks
+    assert( Saig_ManRegNum(pAig) > 0 );
+    assert( Saig_ManPiNum(pAig) > 0 );
+    assert( Saig_ManPoNum(pAig) == 1 );
+
+    // create interpolation manager
+    p = ALLOC( Saig_IntMan_t, 1 );
+    memset( p, 0, sizeof(Saig_IntMan_t) );
+    p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    p->nFrames = 1;
+    p->nConfLimit = nConfLimit;
+    p->fVerbose = fVerbose;
+    // can perform SAT sweeping and/or rewriting of this AIG...
+    p->pAig = pAig;      
+    if ( fUseTransRel )
+        p->pAigTrans = Saig_ManTransformed( pAig );
+    else
+        p->pAigTrans = Saig_ManDuplicated( pAig );
+    // derive CNF for the transformed AIG
+clk = clock();
+    p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); 
+p->timeCnf += clock() - clk;    
+    if ( fVerbose )
+    {
+        printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d.  CNF: Var/Cla = %d/%d.\n",
+            Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), Aig_ManRegNum(pAig), 
+            Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
+            p->pCnfAig->nVars, p->pCnfAig->nClauses );
+    }
+
+    // derive interpolant
+    *pDepth = -1;
+    for ( s = 0; ; s++ )
+    {
+clk2 = clock();
+        // initial state
+        p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) );
+clk = clock();
+        p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
+p->timeCnf += clock() - clk;    
+        // timeframes
+        p->pFrames = Saig_ManFramesInter( pAig, p->nFrames );
+clk = clock();
+//        p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
+//        Aig_ManStop( pAigTemp );
+//        p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
+//        Aig_ManStop( pAigTemp );
+p->timeRwr += clock() - clk;
+        // can also do SAT sweeping on the timeframes...
+clk = clock();
+        p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
+p->timeCnf += clock() - clk;    
+        // report statistics
+        if ( fVerbose )
+        {
+            printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d.  ", 
+                s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
+            PRT( "Time", clock() - clk2 );
+        }
+        // iterate the interpolation procedure
+        for ( i = 0; ; i++ )
+        {
+            // perform interplation
+            clk = clock();
+            RetValue = Saig_PerformOneStep( p );
+            if ( fVerbose )
+            {
+                printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%4d. Conf =%6d.  ", 
+                    i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
+                PRT( "Time", clock() - clk );
+                if ( Aig_ManNodeNum(p->pInter) == 0 )
+                {
+                    Aig_Obj_t * pObj = Aig_ManPo(p->pInter, 0);
+                    Aig_Obj_t * pObjR = Aig_Regular(pObj);
+                    int x = 0;
+                }
+            }
+            if ( RetValue == 0 ) // found a (spurious?) counter-example
+            {
+                if ( i == 0 ) // real counterexample
+                {
+                    if ( fVerbose )
+                        printf( "Found a real counterexample in the first frame.\n" );
+                    p->timeTotal = clock() - clkTotal;
+                    *pDepth = p->nFrames + 1;
+                    Saig_ManagerFree( p );
+                    return 0;
+                }
+                // likely spurious counter-example
+                p->nFrames += i;
+                Saig_ManagerClean( p );
+                break;
+            }
+            else if ( RetValue == -1 ) // timed out
+            {
+                if ( fVerbose )
+                    printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
+                assert( p->nConfCur >= p->nConfLimit );
+                p->timeTotal = clock() - clkTotal;
+                Saig_ManagerFree( p );
+                return -1;
+            }
+            assert( RetValue == 1 ); // found new interpolant
+            // compress the interpolant
+clk = clock();
+            p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
+            Aig_ManStop( pAigTemp );
+p->timeRwr += clock() - clk;
+            // check containment of interpolants
+clk = clock();
+            Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
+p->timeEqu += clock() - clk;
+            if ( Status ) // contained
+            {
+                if ( fVerbose )
+                    printf( "Proved containment of interpolants.\n" );
+                p->timeTotal = clock() - clkTotal;
+                Saig_ManagerFree( p );
+                return 1;
+            }
+            // save interpolant and convert it into CNF
+            if ( fUseTransRel )
+            {
+                Aig_ManStop( p->pInter );
+                p->pInter = p->pInterNew; 
+            }
+            else
+            {
+                p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
+                Aig_ManStop( pAigTemp );
+                Aig_ManStop( p->pInterNew );
+                // compress the interpolant
+clk = clock();
+                p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
+                Aig_ManStop( pAigTemp );
+p->timeRwr += clock() - clk;
+            }
+            p->pInterNew = NULL;
+            Cnf_DataFree( p->pCnfInter );
+clk = clock();
+            p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
+p->timeCnf += clock() - clk;
+        }
+    }
+    assert( 0 );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abc.h

@@ -703,7 +703,7 @@ extern Abc_Ntk_t *        Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * p
 extern Abc_Ntk_t *        Abc_NtkCreateWithNode( char * pSop );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
-extern void               Abc_NtkMakeComb( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches );
 /*=== abcObj.c ==========================================================*/
 extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );

src/base/abc/abcNtk.c

@@ -1104,7 +1104,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
+void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches )
 {
     Abc_Obj_t * pObj;
     int i;
@@ -1136,17 +1136,48 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
     }
     assert( Abc_NtkBoNum(pNtk) == 0 );
 
-    // move COs to become POs
-    Vec_PtrClear( pNtk->vPos );
-    Abc_NtkForEachCo( pNtk, pObj, i )
+    if ( fRemoveLatches )
+    {
+        // remove registers
+        Vec_Ptr_t * vBos;
+        vBos = Vec_PtrAlloc( 100 );
+        Vec_PtrClear( pNtk->vPos );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            if ( Abc_ObjIsBi(pObj) )
+                Vec_PtrPush( vBos, pObj );
+            else
+                Vec_PtrPush( pNtk->vPos, pObj );
+        // remove COs
+        Vec_PtrFree( pNtk->vCos );
+        pNtk->vCos = NULL;
+        // remove the BOs
+        Vec_PtrForEachEntry( vBos, pObj, i )
+            Abc_NtkDeleteObj( pObj );
+        Vec_PtrFree( vBos );
+        // create COs
+        pNtk->vCos = Vec_PtrDup( pNtk->vPos );
+        // cleanup
+        if ( Abc_NtkIsLogic(pNtk) )
+            Abc_NtkCleanup( pNtk, 0 );
+        else if ( Abc_NtkIsStrash(pNtk) )
+            Abc_AigCleanup( pNtk->pManFunc );
+        else
+            assert( 0 );
+    }
+    else
     {
-        if ( Abc_ObjIsBi(pObj) )
+        // move COs to become POs
+        Vec_PtrClear( pNtk->vPos );
+        Abc_NtkForEachCo( pNtk, pObj, i )
         {
-            pObj->Type = ABC_OBJ_PO;
-            pNtk->nObjCounts[ABC_OBJ_PO]++;
-            pNtk->nObjCounts[ABC_OBJ_BI]--;
+            if ( Abc_ObjIsBi(pObj) )
+            {
+                pObj->Type = ABC_OBJ_PO;
+                pNtk->nObjCounts[ABC_OBJ_PO]++;
+                pNtk->nObjCounts[ABC_OBJ_BI]--;
+            }
+            Vec_PtrPush( pNtk->vPos, pObj );
         }
-        Vec_PtrPush( pNtk->vPos, pObj );
     }
     assert( Abc_NtkBiNum(pNtk) == 0 );
 
@@ -1157,6 +1188,60 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes all POs, except one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo )
+{
+    Vec_Ptr_t * vPosToRemove;
+    Abc_Obj_t * pObj;
+    int i;
+
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    assert( Abc_NtkHasOnlyLatchBoxes(pNtk) );
+
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+        return;
+
+    // make sure the node exists
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( pObj == pNodePo )
+            break;
+    assert( i < Abc_NtkPoNum(pNtk) );
+
+    // collect POs to remove
+    vPosToRemove = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( pObj != pNodePo )
+            Vec_PtrPush( vPosToRemove, pObj );
+
+    // remove the POs
+    Vec_PtrForEachEntry( vPosToRemove, pObj, i )
+        Abc_NtkDeleteObj( pObj );
+    Vec_PtrFree( vPosToRemove );
+
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_AigCleanup( pNtk->pManFunc );
+        printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" );
+    }
+    else
+    {
+        printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" );
+    }
+
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Removes POs with suppsize less than 2 and PIs without fanout.]
 
   Description []

src/base/abci/abc.c

@@ -197,6 +197,7 @@ static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmcInter       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIndcut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEnlarge        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -447,6 +448,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "int",           Abc_CommandBmcInter,         0 );
     Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
 
@@ -4531,17 +4533,22 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fRemoveLatches;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fRemoveLatches = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'l':
+            fRemoveLatches ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -4562,14 +4569,15 @@ int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     pNtkRes = Abc_NtkDup( pNtk );
-    Abc_NtkMakeComb( pNtkRes );
+    Abc_NtkMakeComb( pNtkRes, fRemoveLatches );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: comb [-h]\n" );
+    fprintf( pErr, "usage: comb [-lh]\n" );
     fprintf( pErr, "\t        makes the current network combinational by replacing latches by PI/PO pairs\n" );
+    fprintf( pErr, "\t-l    : toggle removing latches [default = %s]\n", fRemoveLatches? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -5741,8 +5749,11 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fUseAllCis;
     int fUseMffc;
+    int fSeq;
     int Output;
 
+    extern void Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodePo );
+
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
@@ -5750,9 +5761,10 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fUseAllCis = 0;
     fUseMffc = 0;
+    fSeq = 0;
     Output = -1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Omah" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Omash" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5769,9 +5781,13 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
             break;
         case 'm':
             fUseMffc ^= 1;
+            break;
         case 'a':
             fUseAllCis ^= 1;
             break;
+        case 's':
+            fSeq ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -5824,12 +5840,18 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         pNodeCo = Abc_NtkCo( pNtk, Output );
-        if ( fUseMffc )
+        if ( fSeq )
+        {
+            pNtkRes = Abc_NtkDup( pNtk );
+            pNodeCo = Abc_NtkPo( pNtkRes, Output );
+            Abc_NtkMakeOnePo( pNtkRes, pNodeCo );
+        }
+        else if ( fUseMffc )
             pNtkRes = Abc_NtkCreateMffc( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo) );
-        else
+        else 
             pNtkRes = Abc_NtkCreateCone( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo), fUseAllCis );
     }
-    if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) )
+    if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) && !fSeq )
         printf( "The extracted cone represents the complement function of the CO.\n" );
     if ( pNtkRes == NULL )
     {
@@ -5841,10 +5863,11 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cone [-O num] [-amh] <name>\n" );
+    fprintf( pErr, "usage: cone [-O num] [-amsh] <name>\n" );
     fprintf( pErr, "\t         replaces the current network by one logic cone\n" );
-    fprintf( pErr, "\t-a     : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
-    fprintf( pErr, "\t-m     : toggle writing only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" );
+    fprintf( pErr, "\t-a     : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
+    fprintf( pErr, "\t-m     : toggle keeping only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" );
+    fprintf( pErr, "\t-s     : toggle comb or sequential cone (works with \"-O num\") [default = %s]\n", fSeq? "seq": "comb" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\t-O num : (optional) the 0-based number of the CO to extract\n");
     fprintf( pErr, "\tname   : (optional) the name of the node to extract\n");
@@ -14601,6 +14624,11 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "Does not work for combinational networks.\n" );
+        return 0;
+    }
     Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fVerbose );
     return 0;
 
@@ -14614,7 +14642,98 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
- 
+  
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nBTLimit;
+    int fRewrite;
+    int fVerbose;
+
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nBTLimit = 20000;
+    fRewrite = 0;
+    fVerbose = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Crvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRewrite ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "Does not work for combinational networks.\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) != 1 )
+    {
+        fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
+        return 0;
+    }
+    Abc_NtkDarBmcInter( pNtk, nBTLimit, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: int [-C num] [-vh]\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-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "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;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/base/abci/abcDar.c

@@ -1240,6 +1240,45 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
+{
+    Aig_Man_t * pMan;
+    int RetValue, Depth, clk = clock();
+    // derive the AIG manager
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    assert( pMan->nRegs > 0 );
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+    RetValue = Saig_Interpolate( pMan, nConfLimit, fVerbose, &Depth );
+    if ( RetValue == 1 )
+        printf( "Property proved.  " );
+    else if ( RetValue == 0 )
+        printf( "Property DISPROVED with counter-example at depth %d.  ", Depth );
+    else if ( RetValue == -1 )
+        printf( "Property UNDECIDED.  " );
+    else
+        assert( 0 );
+PRT( "Time", clock() - clk );
+    Aig_ManStop( pMan );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pMan;

src/base/io/ioUtil.c

@@ -299,7 +299,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
         {
             fprintf( stdout, "Latches are writen into the PLA file at PI/PO pairs.\n" );
             pNtkCopy = Abc_NtkDup( pNtk );
-            Abc_NtkMakeComb( pNtkCopy );
+            Abc_NtkMakeComb( pNtkCopy, 0 );
             pNtkTemp = Abc_NtkToNetlist( pNtk );
             Abc_NtkDelete( pNtkCopy );
         }

src/sat/bsat/satInterA.c

@@ -892,6 +892,7 @@ void Inta_ManPrepareInter( Inta_Man_t * p )
 void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )
 {
     Aig_Man_t * pRes;
+    Aig_Obj_t * pObj;
     Sto_Cls_t * pClause;
     int RetValue = 1;
     int clkTotal = clock();
@@ -955,7 +956,8 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 p->timeTotal += clock() - clkTotal;
     }
 
-    Aig_ObjCreatePo( pRes, *Inta_ManAigRead( p, p->pCnf->pTail ) );
+    pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
+    Aig_ObjCreatePo( pRes, pObj );
     Aig_ManCleanup( pRes );
 
     p->pAig = NULL;