Several new procedures for GIA manipulation.

3 files changed, 129 insertions, 1 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index ee709df4..5e7dc639 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1638,6 +1638,57 @@ Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar )
 
 /**Function*************************************************************
 
+  Synopsis    [Existentially quantified given variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManFillValue( p );
+    // find the cofactoring variable
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    // compute negative cofactor
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ObjFanin0Copy(pObj);
+    // compute the positive cofactor
+    Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create OR gate
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        if ( i == 0 )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) );
+        else 
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManHashStop( pNew );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Existentially quantifies the given variable.]
 
   Description []
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index e72ac93d..6b67d82a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -3110,6 +3110,8 @@ int Abc_GateToType( Abc_Obj_t * pObj )
     if ( !strncmp(pGateName, "nor",  3) )  return ABC_OPER_BIT_NOR;
     if ( !strncmp(pGateName, "xor",  3) )  return ABC_OPER_BIT_XOR;
     if ( !strncmp(pGateName, "xnor", 4) )  return ABC_OPER_BIT_NXOR;
+    if ( !strncmp(pGateName, "zero", 4) )  return ABC_OPER_CONST_F;
+    if ( !strncmp(pGateName, "one",  3) )  return ABC_OPER_CONST_T;
     assert( 0 );
     return -1;
 }
@@ -3141,6 +3143,81 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops )
     return vRes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
+{
+    int iLit0, iLit1;
+    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) )
+        return pNode->iTemp;
+    assert( Abc_ObjIsNode( pNode ) );
+    Abc_NodeSetTravIdCurrent( pNode );
+    iLit0 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) );
+    iLit1 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin1(pNode) );
+    iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) );
+    iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) );
+    return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1));
+}
+Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk )
+{
+    int i, iLit;
+    Abc_Obj_t * pNode;
+    Gia_Man_t * pNew, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        pNode->iTemp = -1;
+    // start new manager
+    pNew = Gia_ManStart( Abc_NtkObjNum(pNtk) );
+    pNew->pName = Abc_UtilStrsav( pNtk->pName );
+    pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
+    Gia_ManHashStart( pNew );
+    // primary inputs
+    Abc_AigConst1(pNtk)->iTemp = 1;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->iTemp = Gia_ManAppendCi(pNew);
+    // create the first cone
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        iLit = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) );
+        iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) );
+        Gia_ManAppendCo( pNew, iLit );
+    }
+    // perform cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops )
+{
+    Abc_Ntk_t * pNtkNew, * pNtk;
+    char * pSop = (char *)Vec_PtrEntry(vSops, 0);
+    assert( Vec_PtrSize(vSops) == 1 );
+    if ( strlen(pSop) == 3 )
+    {
+        Gia_Man_t * pNew = Gia_ManStart( 1 );
+        pNew->pName = Abc_UtilStrsav( "top" );
+        //Gia_ManAppendCi( pNew );
+        assert( pSop[1] == '0' || pSop[1] == '1' );
+        Gia_ManAppendCo( pNew, pSop[1] == '1' );
+        return pNew;
+    }
+    pNtk = Abc_NtkCreateFromSops( "top", vSops );
+    Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk );
+    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; dc2" );
+    pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() );
+    return Abc_NtkStrashToGia( pNtkNew );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 56ac8c4a..7055bf59 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4153,7 +4153,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    if ( Abc_NtkNodeNum(pNtk) == 0 || Abc_NtkPiNum(pNtk) == 0 )
     {
         Abc_Print( -1, "The network does not have internal nodes.\n" );
         return 1;