Adding new Python API 'is_func_iso'.

5 files changed, 129 insertions, 0 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e4136810..ae7c02a5 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -626,6 +626,7 @@ extern ABC_DLL Vec_Ptr_t *        Abc_NtkDfsWithBoxes( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern ABC_DLL Vec_Int_t *        Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo );
+extern ABC_DLL int                Abc_NtkFunctionalIso( Abc_Ntk_t * pNtk, int iCo1, int iCo2 );
 extern ABC_DLL Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern ABC_DLL Vec_Ptr_t *        Abc_AigDfsMap( Abc_Ntk_t * pNtk );
 extern ABC_DLL Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, int  fTfi );
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 8017ce95..9bca1e64 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "proof/cec/cec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -957,6 +958,97 @@ Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives GIA comparing two outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkFunctionalIsoGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
+{
+    int iLit0, iLit1;
+    if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
+        return pNode->iTemp;
+    assert( Abc_ObjIsNode( pNode ) );
+    Abc_NodeSetTravIdCurrent( pNode );
+    iLit0 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pNode) );
+    iLit1 = Abc_NtkFunctionalIsoGia_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_NtkFunctionalIsoGia( Abc_Ntk_t * pNtk, int iCo1, int iCo2 )
+{
+    Gia_Man_t * pNew = NULL, * pTemp;
+    Vec_Int_t * vSupp1 = Abc_NtkNodeSupportInt( pNtk, iCo1 );
+    Vec_Int_t * vSupp2 = Abc_NtkNodeSupportInt( pNtk, iCo2 );
+    if ( Vec_IntSize(vSupp1) == Vec_IntSize(vSupp2) )
+    {
+        Abc_Obj_t * pObj;
+        int i, iCi, iLit1, iLit2;
+        pNew = Gia_ManStart( 1000 );
+        pNew->pName = Abc_UtilStrsav( pNtk->pName );
+        pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
+        Gia_ManHashStart( pNew );
+        // primary inputs
+        Abc_AigConst1(pNtk)->iTemp = 1;
+        Vec_IntForEachEntry( vSupp1, iCi, i )
+            Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManAppendCi(pNew);
+        // create the first cone
+        Abc_NtkIncrementTravId( pNtk );
+        pObj = Abc_NtkCo( pNtk, iCo1 );
+        iLit1 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pObj) );
+        iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC0(pObj) );
+        // primary inputs
+        Vec_IntForEachEntry( vSupp2, iCi, i )
+            Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManCiLit(pNew, i);
+        // create the second cone
+        Abc_NtkIncrementTravId( pNtk );
+        pObj = Abc_NtkCo( pNtk, iCo2 );
+        iLit2 = Abc_NtkFunctionalIsoGia_rec( pNew, Abc_ObjFanin0(pObj) );
+        iLit2 = Abc_LitNotCond( iLit2, Abc_ObjFaninC0(pObj) );
+        Gia_ManAppendCo( pNew, iLit1 );
+        Gia_ManAppendCo( pNew, iLit2 );
+        // perform cleanup
+        pNew = Gia_ManCleanup( pTemp = pNew );
+        Gia_ManStop( pTemp );
+    }
+    Vec_IntFree( vSupp1 );
+    Vec_IntFree( vSupp2 );
+    return pNew;
+}
+int Abc_NtkFunctionalIsoInt( Abc_Ntk_t * pNtk, int iCo1, int iCo2 )
+{
+    Gia_Man_t * pGia; int Value;
+    assert( Abc_NtkIsStrash(pNtk) );
+    if ( iCo1 < 0 || iCo1 >= Abc_NtkCoNum(pNtk) )
+        return 0;
+    if ( iCo2 < 0 || iCo2 >= Abc_NtkCoNum(pNtk) )
+        return 0;
+    pGia = Abc_NtkFunctionalIsoGia( pNtk, iCo1, iCo2 );
+    if ( pGia == NULL )
+        return 0;
+    Value = Cec_ManVerifySimple( pGia );
+    Gia_ManStop( pGia );
+    return (int)(Value == 1);
+}
+int Abc_NtkFunctionalIso( Abc_Ntk_t * pNtk, int iCo1, int iCo2 )
+{
+    Abc_Ntk_t * pNtkNew; int Result;
+    if ( Abc_NtkIsStrash(pNtk) )
+        return Abc_NtkFunctionalIsoInt( pNtk, iCo1, iCo2 );
+    pNtkNew = Abc_NtkStrash( pNtk, 0, 0, 0 );
+    Result = Abc_NtkFunctionalIsoInt( pNtkNew, iCo1, iCo2 );
+    Abc_NtkDelete( pNtkNew );
+    return Result;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Computes support size of the node.]
 
   Description []
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 805a5d73..a0b92b52 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -197,6 +197,7 @@ struct Cec_ParSeq_t_
 /*=== cecCec.c ==========================================================*/
 extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
 extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
+extern int           Cec_ManVerifySimple( Gia_Man_t * p );
 /*=== cecChoice.c ==========================================================*/
 extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
 /*=== cecCorr.c ==========================================================*/
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 1465a721..77a6ed4a 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -415,6 +415,27 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
 
 /**Function*************************************************************
 
+  Synopsis    [Simple SAT run to check equivalence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerifySimple( Gia_Man_t * p )
+{
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Cec_ManCecSetDefaultParams( pPars );
+    pPars->fSilent = 1;
+    assert( Gia_ManCoNum(p) == 2 );
+    assert( Gia_ManRegNum(p) == 0 );
+    return Cec_ManVerify( p, pPars );
+}
+
+/**Function*************************************************************
+
   Synopsis    [New CEC engine applied to two circuits.]
 
   Description []
diff --git a/src/python/pyabc.i b/src/python/pyabc.i
index 208235a4..e3bad4bc 100644
--- a/src/python/pyabc.i
+++ b/src/python/pyabc.i
@@ -384,6 +384,19 @@ PyObject* co_supp( int iCo )
     return co_supp;    
 }
 
+int is_func_iso( int iCo1, int iCo2 )
+{
+    Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+
+    if ( !pNtk )
+    {
+        return 0;
+    }
+
+    return Abc_NtkFunctionalIso( pNtk, iCo1, iCo2 );
+}
+
 void _pyabc_array_clear()
 {
     Abc_Frame_t* pAbc = Abc_FrameGetGlobalFrame();
@@ -741,6 +754,7 @@ int _cex_get_frame(Abc_Cex_t* pCex);
 
 PyObject* eq_classes();
 PyObject* co_supp(int iCo);
+int is_func_iso(int iCo1, int iCo2);
 
 void _pyabc_array_clear();
 void _pyabc_array_push(int i);