Several changes to various packages.

7 files changed, 148 insertions, 6 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b05c8636..477c44dc 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -764,6 +764,27 @@ Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p )
         pNew->pCellStr = Abc_UtilStrsav( p->pCellStr );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupRemovePis( Gia_Man_t * p, int nRemPis )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else if ( Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManCiNum(p)-nRemPis )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 8defc9d4..51ed350e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -602,6 +602,7 @@ extern ABC_DLL int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk )
 /*=== abcCollapse.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose );
+extern ABC_DLL Gia_Man_t *        Abc_NtkClpGia( Abc_Ntk_t * pNtk );
 /*=== abcCut.c ==========================================================*/
 extern ABC_DLL void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
 extern ABC_DLL void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
@@ -787,6 +788,7 @@ extern ABC_DLL void               Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemove
 extern ABC_DLL void               Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pFlopPermFile );
 extern ABC_DLL void               Abc_NtkUnpermute( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias );
 /*=== abcObj.c ==========================================================*/
 extern ABC_DLL Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern ABC_DLL void               Abc_ObjRecycle( Abc_Obj_t * pObj );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ff1a2822..a62542b9 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -2239,6 +2239,55 @@ Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops )
     return pNtk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias )
+{
+    Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry(vGias, 0);
+    Abc_Ntk_t * pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    Abc_Obj_t * pAbcObj, * pAbcObjPo;
+    Gia_Obj_t * pObj; int i, k;
+    pNtk->pName = Extra_UtilStrsav( pName );
+    for ( k = 0; k < Gia_ManCiNum(pGia); k++ )
+        Abc_NtkCreatePi( pNtk );
+    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
+    {
+        assert( Gia_ManCoNum(pGia) == 1 );
+        Gia_ManCleanValue(pGia);
+        Gia_ManForEachCi( pGia, pObj, k )
+            pObj->Value = Abc_ObjId( Abc_NtkCi(pNtk, k) );
+        Gia_ManForEachAnd( pGia, pObj, k )
+        {
+            Abc_Obj_t * pAbcObj0 = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value );
+            Abc_Obj_t * pAbcObj1 = Abc_NtkObj( pNtk, Gia_ObjFanin1(pObj)->Value );
+            pAbcObj0 = Abc_ObjNotCond( pAbcObj0, Gia_ObjFaninC0(pObj) );
+            pAbcObj1 = Abc_ObjNotCond( pAbcObj1, Gia_ObjFaninC1(pObj) );
+            pAbcObj  = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, pAbcObj0, pAbcObj1 );
+            pObj->Value = Abc_ObjId( pAbcObj ); 
+        }
+        pObj = Gia_ManCo(pGia, 0);
+        if ( Gia_ObjFaninId0p(pGia, pObj) == 0 )
+            pAbcObj = Abc_ObjNot( Abc_AigConst1(pNtk) );
+        else
+            pAbcObj = Abc_NtkObj( pNtk, Gia_ObjFanin0(pObj)->Value );
+        pAbcObj = Abc_ObjNotCond( pAbcObj, Gia_ObjFaninC0(pObj) );
+        pAbcObjPo = Abc_NtkCreatePo( pNtk );
+        Abc_ObjAddFanin( pAbcObjPo, pAbcObj );
+    }
+    Abc_NtkAddDummyPiNames( pNtk );
+    Abc_NtkAddDummyPoNames( pNtk );
+    return pNtk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 6b67d82a..8cac0a42 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -3142,6 +3142,45 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops )
     assert( Vec_WecSize(vRes) == iNode );
     return vRes;
 }
+Vec_Wec_t * Abc_GiaSynthesize( Vec_Ptr_t * vGias )
+{
+    Vec_Wec_t * vRes = NULL;
+    Abc_Ntk_t * pNtk = Abc_NtkCreateFromGias( "top", vGias );
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, iNode = 0;
+    Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "dc2; map -a" );
+    pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
+    vRes = Vec_WecStart( Abc_NtkPiNum(pNtkNew) + Abc_NtkNodeNum(pNtkNew) + Abc_NtkPoNum(pNtkNew) );
+    Abc_NtkForEachPi( pNtkNew, pObj, i )
+        pObj->iTemp = iNode++;
+    Abc_NtkForEachNode( pNtkNew, pObj, i )
+    {
+        Vec_Int_t * vNode = Vec_WecEntry(vRes, iNode);
+        Vec_IntPush( vNode, Abc_GateToType(pObj) );
+        Vec_IntPush( vNode, iNode );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vNode, pFanin->iTemp );
+        pObj->iTemp = iNode++;
+    }
+    Abc_NtkForEachPo( pNtkNew, pObj, i )
+        Vec_IntPushTwo( Vec_WecEntry(vRes, iNode++), ABC_OPER_BIT_BUF, Abc_ObjFanin0(pObj)->iTemp );
+    assert( Vec_WecSize(vRes) == iNode );
+    return vRes;
+}
+Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p )
+{
+    Abc_Ntk_t * pNtkNew, * pNtk;
+    Vec_Ptr_t * vGias = Vec_PtrAlloc( 1 );
+    Vec_PtrPush( vGias, p );
+    pNtk = Abc_NtkCreateFromGias( "top", vGias );
+    Vec_PtrFree( vGias );
+    Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "ps; balance; collapse; ps; muxes; strash; ps; dc2; ps" );
+    pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
+    return Abc_NtkClpGia( pNtkNew );
+}
 
 /**Function*************************************************************
 
@@ -3197,11 +3236,10 @@ Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk )
     Gia_ManStop( pTemp );
     return pNew;
 }
-Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops )
+Gia_Man_t * Abc_SopSynthesizeOne( char * pSop )
 {
     Abc_Ntk_t * pNtkNew, * pNtk;
-    char * pSop = (char *)Vec_PtrEntry(vSops, 0);
-    assert( Vec_PtrSize(vSops) == 1 );
+    Vec_Ptr_t * vSops;
     if ( strlen(pSop) == 3 )
     {
         Gia_Man_t * pNew = Gia_ManStart( 1 );
@@ -3211,9 +3249,12 @@ Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops )
         Gia_ManAppendCo( pNew, pSop[1] == '1' );
         return pNew;
     }
+    vSops = Vec_PtrAlloc( 1 );
+    Vec_PtrPush( vSops, pSop );
     pNtk = Abc_NtkCreateFromSops( "top", vSops );
+    Vec_PtrFree( vSops );
     Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
-    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; dc2" );
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; balance; dc2" );
     pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
     return Abc_NtkStrashToGia( pNtkNew );
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a6a77571..45198165 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9883,7 +9883,6 @@ usage:
 ***********************************************************************/
 int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk );
     extern void Abc_NtkExpandCubes( Abc_Ntk_t * pNtk, Gia_Man_t * pGia, int fVerbose );
     Abc_Ntk_t * pStrash, * pNtk2, * pNtk = Abc_FrameReadNtk(pAbc);
     Gia_Man_t * pGia; int c, fVerbose = 0;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 996ae6a2..8ec810f5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3773,6 +3773,35 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelat
     Aig_ManStop( pManAig );
     return pNtkAig;
 }
+Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose )
+{
+    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
+    Gia_Man_t * pNtkAig;
+    Aig_Man_t * pManOn, * pManOff, * pManAig;
+    assert( Gia_ManCiNum(pNtkOn)  == Gia_ManCiNum(pNtkOff) );
+    assert( Gia_ManCoNum(pNtkOn)  == 1 );
+    assert( Gia_ManCoNum(pNtkOff) == 1 );
+    // create internal AIGs
+    pManOn = Gia_ManToAigSimple( pNtkOn );
+    if ( pManOn == NULL )
+        return NULL;
+    pManOff = Gia_ManToAigSimple( pNtkOff );
+    if ( pManOff == NULL )
+        return NULL;
+    // derive the interpolant
+    pManAig = Aig_ManInter( pManOn, pManOff, 0, fVerbose );
+    if ( pManAig == NULL )
+    {
+        Abc_Print( 1, "Interpolant computation failed.\n" );
+        return NULL;
+    }
+    Aig_ManStop( pManOn );
+    Aig_ManStop( pManOff );
+    // create logic network
+    pNtkAig = Gia_ManFromAigSimple( pManAig );
+    Aig_ManStop( pManAig );
+    return pNtkAig;
+}
 
 /**Function*************************************************************
 
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index c769352f..df127d1d 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -1019,10 +1019,11 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop
     if ( fVerbose )
     {
 //        ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
-    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
+    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB  ", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
         1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
 p->timeTotal += Abc_Clock() - clkTotal;
     }