From 232fe09ee41afaacf6382d01ef9c6a046874b6da Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 19 May 2013 21:27:23 -0700
Subject: Bug fix in &frames.

---
 src/aig/gia/giaFrames.c | 31 ++++++-------------------------
 1 file changed, 6 insertions(+), 25 deletions(-)

(limited to 'src/aig')

diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index b19e223b..23caacc4 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -713,29 +713,6 @@ void Gia_ManFraSupports( Gia_ManFra_t * p )
     }
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Moves the first nRegs entries to the end.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManFraTransformCis( Gia_Man_t * pAig, Vec_Int_t * vCis )
-{
-    int i, k = 0, Entry;
-    Vec_IntForEachEntryStop( vCis, Entry, i, Gia_ManRegNum(pAig) )
-        assert( Entry == i+1 );
-    Vec_IntForEachEntryStart( vCis, Entry, i, Gia_ManRegNum(pAig) )
-        Vec_IntWriteEntry( vCis, k++, Entry );
-    for ( i = 0; i < Gia_ManRegNum(pAig); i++ )
-        Vec_IntWriteEntry( vCis, k++, i+1 );
-    assert( k == Vec_IntSize(vCis) );
-}
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -878,6 +855,11 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     if ( !pPars->fDisableSt )
         Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
+    // create primary inputs
+    for ( f = 0; f < pPars->nFrames; f++ )
+        Gia_ManForEachPi( pAig, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pFrames );
+    // add internal nodes for each timeframe
     for ( f = 0; f < pPars->nFrames; f++ )
     {
         if ( f == 0 )
@@ -891,7 +873,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
                 pObj->Value = Gia_ObjRoToRi( pAig, pObj )->Value;
         }
         Gia_ManForEachPi( pAig, pObj, i )
-            pObj->Value = Gia_ManAppendCi( pFrames );
+            pObj->Value = Gia_Obj2Lit( pFrames, Gia_ManPi(pFrames, f * Gia_ManPiNum(pAig) + i) );
         if ( !pPars->fDisableSt )
             Gia_ManForEachAnd( pAig, pObj, i )
                 pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -929,7 +911,6 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     Vec_IntFreeP( &vPoLits );
     if ( !pPars->fDisableSt )
         Gia_ManHashStop( pFrames );
-    Gia_ManFraTransformCis( pAig, pFrames->vCis );
     Gia_ManSetRegNum( pFrames, Gia_ManRegNum(pAig) );
     if ( Gia_ManCombMarkUsed(pFrames) < Gia_ManAndNum(pFrames) )
     {
-- 
cgit v1.2.3