Experiments with mini AIG manager.

3 files changed, 41 insertions, 12 deletions

diff --git a/src/base/abc/miniaig.h b/src/base/abc/miniaig.h
index ab7ab9a5..0d6aa62f 100644
--- a/src/base/abc/miniaig.h
+++ b/src/base/abc/miniaig.h
@@ -139,14 +139,14 @@ static void Mini_AigStop( Mini_Aig_t * p )
 // (constant node is created when AIG manager is created)
 static int Mini_AigCreatePi( Mini_Aig_t * p )
 {
-    int Lit = Mini_AigNodeNum(p);
+    int Lit = p->nSize;
     Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
     return Lit;
 }
 static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 )
 {
-    int Lit = Mini_AigNodeNum(p);
-    assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNodeNum(p) );
+    int Lit = p->nSize;
+    assert( Lit0 >= 0 && Lit0 < Lit );
     Mini_AigPush( p, Lit0, MINI_AIG_NULL );
     return Lit;
 }
@@ -154,9 +154,9 @@ static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 )
 // boolean operations
 static int Mini_AigAnd( Mini_Aig_t * p, int Lit0, int Lit1 )
 {
-    int Lit = Mini_AigNodeNum(p);
-    assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNodeNum(p) );
-    assert( Lit1 >= 0 && Lit1 < 2 * Mini_AigNodeNum(p) );
+    int Lit = p->nSize;
+    assert( Lit0 >= 0 && Lit0 < Lit );
+    assert( Lit1 >= 0 && Lit1 < Lit );
     Mini_AigPush( p, Lit0, Lit1 );
     return Lit;
 }
diff --git a/src/base/abci/abcMini.c b/src/base/abci/abcMini.c
index bcfed643..a43b7d7b 100644
--- a/src/base/abci/abcMini.c
+++ b/src/base/abci/abcMini.c
@@ -66,6 +66,7 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
     nNodes = Mini_AigNodeNum(p);
     // create ABC network
     pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtk->pName = Abc_UtilStrsav( "MiniAig" );
     // create mapping from MiniAIG objects into ABC objects
     vCopies = Vec_IntAlloc( nNodes );
     Vec_IntPush( vCopies, Abc_LitNot(Abc_ObjToLit(Abc_AigConst1(pNtk))) );
@@ -81,6 +82,7 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
         else assert( 0 );
         Vec_IntPush( vCopies, Abc_ObjToLit(pObj) );
     }
+    assert( Vec_IntSize(vCopies) == nNodes );
     Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
     Vec_IntFree( vCopies );
     Abc_NtkAddDummyPiNames( pNtk );
@@ -92,7 +94,7 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Converts the network from the AIG manager into ABC.]
+  Synopsis    [Converts the network from ABC into the AIG manager.]
 
   Description []
                
@@ -134,7 +136,7 @@ Mini_Aig_t * Abc_NtkToMiniAig( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Procedures to update internal ABC network using AIG node array.]
 
   Description []
                
@@ -164,6 +166,37 @@ void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Testing the above code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMiniAigTest( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkNew;
+    Mini_Aig_t * p;
+    p = Abc_NtkToMiniAig( pNtk );
+    pNtkNew = Abc_NtkFromMiniAig( p );
+    Mini_AigStop( p );
+    Abc_NtkPrintStats( pNtkNew, 0, 0, 0, 0, 0, 0, 0 );
+    Abc_NtkDelete( pNtkNew );
+}
+
+/*
+    if ( pNtk )
+    {
+        extern void Abc_NtkMiniAigTest( Abc_Ntk_t * pNtk );
+        Abc_NtkMiniAigTest( pNtk );
+
+    }
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/main.h b/src/base/main/main.h
index f2d7cbf4..849e1956 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -131,10 +131,6 @@ extern ABC_DLL void            Abc_FrameSetCex( Abc_Cex_t * pCex );
 extern ABC_DLL void            Abc_FrameSetNFrames( int nFrames );
 extern ABC_DLL void            Abc_FrameSetStatus( int Status );
 
-/*=== mainFrame.c ===========================================================*/
-extern ABC_DLL void            Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * p );
-extern ABC_DLL void *          Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
-
 
 ABC_NAMESPACE_HEADER_END