Version abc70110

5 files changed, 89 insertions, 5 deletions

diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index a5d6e2e5..ce4cdfde 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -304,6 +304,7 @@ extern void            Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSupe
 extern int             Hop_ObjIsMuxType( Hop_Obj_t * pObj );
 extern int             Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
 extern Hop_Obj_t *     Hop_ObjRecognizeMux( Hop_Obj_t * pObj, Hop_Obj_t ** ppObjT, Hop_Obj_t ** ppObjE );
+extern void            Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig );
 extern void            Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig );
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
index 738caa4a..a49e8397 100644
--- a/src/aig/hop/hopUtil.c
+++ b/src/aig/hop/hopUtil.c
@@ -283,6 +283,53 @@ Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pNode, Hop_Obj_t ** ppNodeT, Hop_Ob
 
 /**Function*************************************************************
 
+  Synopsis    [Prints Eqn formula for the AIG rooted at this node.]
+
+  Description [The formula is in terms of PIs, which should have
+  their names assigned in pObj->pData fields.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
+{
+    Vec_Ptr_t * vSuper;
+    Hop_Obj_t * pFanin;
+    int fCompl, i;
+    // store the complemented attribute
+    fCompl = Hop_IsComplement(pObj);
+    pObj = Hop_Regular(pObj);
+    // constant case
+    if ( Hop_ObjIsConst1(pObj) )
+    {
+        fprintf( pFile, "%d", !fCompl );
+        return;
+    }
+    // PI case
+    if ( Hop_ObjIsPi(pObj) )
+    {
+        fprintf( pFile, "%s%s", fCompl? "!" : "", pObj->pData );
+        return;
+    }
+    // AND case
+    Vec_VecExpand( vLevels, Level );
+    vSuper = Vec_VecEntry(vLevels, Level);
+    Hop_ObjCollectMulti( pObj, vSuper );
+    fprintf( pFile, "%s", (Level==0? "" : "(") );
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        Hop_ObjPrintEqn( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
+        if ( i < Vec_PtrSize(vSuper) - 1 )
+            fprintf( pFile, " %s ", fCompl? "+" : "*" );
+    }
+    fprintf( pFile, "%s", (Level==0? "" : ")") );
+    return;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints Verilog formula for the AIG rooted at this node.]
 
   Description [The formula is in terms of PIs, which should have
diff --git a/src/aig/ivy/attr.h b/src/aig/ivy/attr.h
index 5a760239..16cf0b84 100644
--- a/src/aig/ivy/attr.h
+++ b/src/aig/ivy/attr.h
@@ -193,7 +193,7 @@ static inline void Attr_ManStop( Attr_Man_t * p )
         p->pFuncFreeMan( p->pManAttr );
     // free the memory manager
     if ( p->pManMem )  
-        Extra_MmFixedStop( p->pManMem, 0 );
+        Extra_MmFixedStop( p->pManMem);
     // free the attribute manager
     FREE( p->pAttrs );
     free( p );
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index f48466ef..9e944028 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -268,6 +268,7 @@ static inline Ivy_Obj_t *  Ivy_ObjChild0( Ivy_Obj_t * pObj )      { return pObj-
 static inline Ivy_Obj_t *  Ivy_ObjChild1( Ivy_Obj_t * pObj )      { return pObj->pFanin1;                          }
 static inline Ivy_Obj_t *  Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL;  }
 static inline Ivy_Obj_t *  Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }
+static inline Ivy_Obj_t *  Ivy_ObjEquiv( Ivy_Obj_t * pObj )       { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; }
 static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { return pObj->Level;                            }
 static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
 static inline int          Ivy_ObjFaninPhase( Ivy_Obj_t * pObj )  { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 269ca257..ce21c269 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -752,6 +752,26 @@ int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+    Ivy_FraigSim_t * pSims;
+    int i;
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nSimWords; i++ )
+        pSims->pData[i] = ~pSims->pData[i];
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if simulation infos are equal.]
 
   Description []
@@ -1277,7 +1297,11 @@ void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
     // fill in the counter-example data
     pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
     Ivy_ManForEachPi( p->pManAig, pObj, i )
+    {
         pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
+//        printf( "%d", pModel[i] );
+    }
+//    printf( "\n" );
     // set the model
     assert( p->pManFraig->pData == NULL );
     p->pManFraig->pData = pModel;
@@ -1299,13 +1323,25 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
 {
     Ivy_Obj_t * pObj;
     int i;
+    // make sure the reference simulation pattern does not detect the bug
+    pObj = Ivy_ManPo( p->pManAig, 0 );
+    assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
     Ivy_ManForEachPo( p->pManAig, pObj, i )
+    {
+        // complement simulation info
+//        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
+//            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+        // check 
         if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
         {
             // create the counter-example from this pattern
             Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
             return 1;
         }
+        // complement simulation info
+//        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
+//            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+    }
     return 0;
 }
 
@@ -1819,6 +1855,9 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
         {
             if ( fVerbose )
                 printf( "Output %2d (out of %2d) is constant 1.  ", i, Ivy_ManPoNum(p->pManAig) );
+            // assing constant 0 model
+            p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+            memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
             break;
         }
         // check if the output is constant 0
@@ -1957,10 +1996,6 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
     if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
          (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
     {
-//        if ( Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1 )
-//        {
-//            int x = 0;
-//        }
         assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
         assert( pObjNew != Ivy_Regular(pFanin0New) );
         assert( pObjNew != Ivy_Regular(pFanin1New) );