New command 'testnpn' to compare semi-canonical forms.

2 files changed, 32 insertions, 11 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index afcce09b..6910f334 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -396,7 +396,7 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     Vec_IntPush( p->vAbs, 0 );
     // refinement
     p->pRnm      = Rnm_ManStart( pGia );
-//    p->pRf2      = Rf2_ManStart( pGia );
+    p->pRf2      = Rf2_ManStart( pGia );
     // SAT solver and variables
     p->vId2Lit   = Vec_PtrAlloc( 1000 );
     // temporaries
@@ -459,7 +459,7 @@ void Ga2_ManStop( Ga2_Man_t * p )
     Vec_IntFree( p->vLits );
     Vec_IntFree( p->vIsopMem );
     Rnm_ManStop( p->pRnm, p->pPars->fVerbose );
-//    Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
+    Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
     ABC_FREE( p->pTable );
     ABC_FREE( p->pSopSizes );
     ABC_FREE( p->pSops[1] );
@@ -1216,7 +1216,7 @@ Abc_Cex_t * Ga2_ManDeriveCex( Ga2_Man_t * p, Vec_Int_t * vPis )
                 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
     }
     return pCex;
-}
+} 
 Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
 {
     Abc_Cex_t * pCex;
@@ -1224,8 +1224,11 @@ Vec_Int_t * Ga2_ManRefine( Ga2_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
-    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
+ 
 //    Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
+    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
+//    printf( "Refinement %d\n", Vec_IntSize(vVec) );
+
     Abc_CexFree( pCex );
     if ( Vec_IntSize(vVec) == 0 )
     {
diff --git a/src/aig/gia/giaAbsRef2.c b/src/aig/gia/giaAbsRef2.c
index fcd5eae1..ac47333d 100644
--- a/src/aig/gia/giaAbsRef2.c
+++ b/src/aig/gia/giaAbsRef2.c
@@ -385,8 +385,9 @@ void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFani
         return;
     if ( Gia_ObjIsRo(p->pGia, pObj) )
     {
+        assert( pObj->fPhase );
         pObj = Gia_ObjRoToRi(p->pGia, pObj);
-        Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth, RootId, 0 );
+        Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 );
     }
     else if ( Gia_ObjIsAnd(pObj) )
     {
@@ -397,9 +398,10 @@ void Rf2_ManGatherFanins_rec( Rf2_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFani
 }
 void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
 {
+    Vec_Int_t * vUsed;
     Vec_Int_t * vVec;
     Gia_Obj_t * pObj;
-    int i;
+    int i, k, Entry;
     // mark PPIs
     Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
     {
@@ -416,24 +418,40 @@ void Rf2_ManGatherFanins( Rf2_Man_t * p, int Depth )
         Gia_ManIncrementTravId( p->pGia );
         Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 );
     }
+
+    vUsed = Vec_IntStart( Vec_IntSize(p->vMap) );
+
     // evaluate collected
-    printf( "\nMap: " );
+    printf( "\nMap (%d): ", Vec_IntSize(p->vMap) );
     Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
     {
         vVec = Rf2_ObjVec( p, pObj );
-        printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
+        if ( Vec_IntSize(vVec) > 1 )
+            printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
+        Vec_IntForEachEntryStart( vVec, Entry, k, 1 )
+            Vec_IntAddToEntry( vUsed, Entry, 1 );
         Vec_IntClear( vVec );
     }
     printf( "\n" );
     // evaluate internal
-    printf( "Int: " );
+    printf( "Int (%d): ", Vec_IntSize(p->vFanins) );
     Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
     {
         vVec = Rf2_ObjVec( p, pObj );
-        printf( "%d=%d ", i, Vec_IntSize(vVec) );
+        if ( Vec_IntSize(vVec) > 1 )
+            printf( "%d=%d ", i, Vec_IntSize(vVec) );
+        if ( Vec_IntSize(vVec) > 1 )
+            Vec_IntForEachEntry( vVec, Entry, k )
+                Vec_IntAddToEntry( vUsed, Entry, 1 );
         Vec_IntClear( vVec );
     }
     printf( "\n" );
+    // evaluate PPIs    
+    Vec_IntForEachEntry( vUsed, Entry, k )
+        printf( "%d ", Entry );
+    printf( "\n" );
+
+    Vec_IntFree( vUsed );
 }
 
 
@@ -461,7 +479,7 @@ Vec_Int_t * Rf2_ManRefine( Rf2_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, in
     // collects used objects
     Rf2_ManCollect( p );
     // collect reconvergence points
-    Rf2_ManGatherFanins( p, 1 );
+    Rf2_ManGatherFanins( p, 2 );
     // propagate justification IDs
 
     // select the result