Making &gla iterate over property outputs.

3 files changed, 61 insertions, 13 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 18544a73..0efc263b 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1293,6 +1293,7 @@ extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
+extern Gia_Man_t *         Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo );
 extern Gia_Man_t *         Gia_ManDupCofactorVar( Gia_Man_t * p, int iVar, int Value );  
 extern Gia_Man_t *         Gia_ManDupCofactorObj( Gia_Man_t * p, int iObj, int Value );  
 extern Gia_Man_t *         Gia_ManDupMux( int iVar, Gia_Man_t * pCof1, Gia_Man_t * pCof0 );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 988d50a2..e05380d5 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1556,6 +1556,30 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
         pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
+Gia_Man_t * Gia_ManDupDfsOnePo( Gia_Man_t * p, int iPo )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( iPo >= 0 && iPo < Gia_ManPoNum(p) );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachCo( p, pObj, i )
+        if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
+            Gia_ManDupDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( !Gia_ObjIsPo(p, pObj) || i == iPo )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 17e255b8..96432812 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -45764,11 +45764,6 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 */
-    if ( Gia_ManPoNum(pAbc->pGia) > 1 )
-    {
-        Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );
-        return 0;
-    }
     if ( pPars->nFramesMax < 0 )
     {
         Abc_Print( 1, "The number of starting frames should be a positive integer.\n" );
@@ -45779,14 +45774,42 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "The starting frame is larger than the max number of frames.\n" );
         return 0;
     }
-    if ( fNewAlgo )
-        pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
-    else
-        pAbc->Status  = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 );
-    pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
-    if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" );
+    if ( Gia_ManPoNum(pAbc->pGia) == 1 )
+    {
+        if ( fNewAlgo )
+            pAbc->Status = Gia_ManPerformGla( pAbc->pGia, pPars );
+        else
+            pAbc->Status  = Gia_ManPerformGlaOld( pAbc->pGia, pPars, 0 );
+        pAbc->nFrames = pPars->iFrame;
+        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+        if ( pLogFileName )
+            Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&gla" );
+    }
+    else // iterate over outputs
+    {
+        Gia_Obj_t * pObj; int o, Status;
+        Vec_Ptr_t * vSeqModelVec = Vec_PtrStart( Gia_ManPoNum(pAbc->pGia) );
+        Vec_Int_t * vStatuses = Vec_IntAlloc( Gia_ManPoNum(pAbc->pGia) );
+        Gia_ManForEachPo( pAbc->pGia, pObj, o )
+        {
+            Gia_Man_t * pOne = Gia_ManDupDfsOnePo( pAbc->pGia, o );
+            if ( fNewAlgo )
+                Status = Gia_ManPerformGla( pOne, pPars );
+            else
+                Status = Gia_ManPerformGlaOld( pOne, pPars, 0 );
+            Vec_IntPush( vStatuses, Status );
+            if ( pLogFileName )
+                Abc_NtkWriteLogFile( pLogFileName, pOne->pCexSeq, Status, pPars->iFrame, "&gla" );
+            if ( pOne->pCexSeq )
+                Vec_PtrWriteEntry( vSeqModelVec, o, pOne->pCexSeq );
+            pOne->pCexSeq = NULL;
+            Gia_ManStop( pOne );
+        }
+        assert( Vec_IntSize(vStatuses) == Gia_ManPoNum(pAbc->pGia) );
+        Abc_FrameReplaceCexVec( pAbc, &vSeqModelVec );
+        Abc_FrameReplacePoStatuses( pAbc, &vStatuses );
+        pAbc->nFrames = -1;
+    }
     return 0;
 
 usage: