1 files changed, 208 insertions, 243 deletions

diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c
index 3d1ac335..3b77bf41 100644
--- a/src/temp/ivy/ivyUtil.c
+++ b/src/temp/ivy/ivyUtil.c
@@ -68,136 +68,6 @@ void Ivy_ManCleanTravId( Ivy_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    // check that the node is regular
-    assert( !Ivy_IsComplement(pNode) );
-    // if the node is not AND, this is not MUX
-    if ( !Ivy_ObjIsAnd(pNode) )
-        return 0;
-    // if the children are not complemented, this is not MUX
-    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
-        return 0;
-    // get children
-    pNode0 = Ivy_ObjFanin0(pNode);
-    pNode1 = Ivy_ObjFanin1(pNode);
-    // if the children are not ANDs, this is not MUX
-    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
-        return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
-    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
-           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
-           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
-           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
-
-  Description [If the node is a MUX, returns the control variable C.
-  Assigns nodes T and E to be the then and else variables of the MUX. 
-  Node C is never complemented. Nodes T and E can be complemented.
-  This function also recognizes EXOR/NEXOR gates as MUXes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
-{
-    Ivy_Obj_t * pNode0, * pNode1;
-    assert( !Ivy_IsComplement(pNode) );
-    assert( Ivy_ObjIsMuxType(pNode) );
-    // get children
-    pNode0 = Ivy_ObjFanin0(pNode);
-    pNode1 = Ivy_ObjFanin1(pNode);
-    // find the control variable
-//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
-    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Ivy_ObjFaninC0(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            return Ivy_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            return Ivy_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
-    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p1) )
-        if ( Ivy_ObjFaninC0(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            return Ivy_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            return Ivy_ObjChild0(pNode0);//pNode1->p1;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
-    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Ivy_ObjFaninC1(pNode0) )
-        { // pNode2->p1 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            return Ivy_ObjChild0(pNode1);//pNode2->p1;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
-            return Ivy_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
-    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
-    {
-//        if ( Fraig_IsComplement(pNode1->p2) )
-        if ( Ivy_ObjFaninC1(pNode0) )
-        { // pNode2->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            return Ivy_ObjChild1(pNode1);//pNode2->p2;
-        }
-        else
-        { // pNode1->p2 is positive phase of C
-            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
-            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
-            return Ivy_ObjChild1(pNode0);//pNode1->p2;
-        }
-    }
-    assert( 0 ); // this is not MUX
-    return NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Computes truth table of the cut.]
 
   Description []
@@ -207,14 +77,14 @@ Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Ob
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
+void Ivy_ManCollectCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
 {
     if ( pNode->fMarkA )
         return;
     pNode->fMarkA = 1;
     assert( Ivy_ObjIsAnd(pNode) || Ivy_ObjIsExor(pNode) );
-    Ivy_ManCollectCut_rec( Ivy_ObjFanin0(pNode), vNodes );
-    Ivy_ManCollectCut_rec( Ivy_ObjFanin1(pNode), vNodes );
+    Ivy_ManCollectCut_rec( p, Ivy_ObjFanin0(pNode), vNodes );
+    Ivy_ManCollectCut_rec( p, Ivy_ObjFanin1(pNode), vNodes );
     Vec_IntPush( vNodes, pNode->Id );
 }
 
@@ -230,7 +100,7 @@ void Ivy_ManCollectCut_rec( Ivy_Obj_t * pNode, Vec_Int_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+void Ivy_ManCollectCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
 {
     int i, Leaf;
     // collect and mark the leaves
@@ -238,13 +108,13 @@ void Ivy_ManCollectCut( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNod
     Vec_IntForEachEntry( vLeaves, Leaf, i )
     {
         Vec_IntPush( vNodes, Leaf );
-        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 1;
+        Ivy_ManObj(p, Leaf)->fMarkA = 1;
     }
     // collect and mark the nodes
-    Ivy_ManCollectCut_rec( pRoot, vNodes );
+    Ivy_ManCollectCut_rec( p, pRoot, vNodes );
     // clean the nodes
     Vec_IntForEachEntry( vNodes, Leaf, i )
-        Ivy_ObjObj(pRoot, Leaf)->fMarkA = 0;
+        Ivy_ManObj(p, Leaf)->fMarkA = 0;
 }
 
 /**Function*************************************************************
@@ -274,7 +144,7 @@ unsigned * Ivy_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
+void Ivy_ManCutTruthOne( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
 {
     unsigned * pTruth, * pTruth0, * pTruth1;
     int i;
@@ -310,7 +180,7 @@ void Ivy_ManCutTruthOne( Ivy_Obj_t * pNode, Vec_Int_t * vTruth, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
+unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth )
 {
     static unsigned uTruths[8][8] = { // elementary truth tables
         { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
@@ -324,10 +194,10 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t *
     };
     int i, Leaf;
     // collect the cut
-    Ivy_ManCollectCut( pRoot, vLeaves, vNodes );
+    Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes );
     // set the node numbers
     Vec_IntForEachEntry( vNodes, Leaf, i )
-        Ivy_ObjObj(pRoot, Leaf)->TravId = i;
+        Ivy_ManObj(p, Leaf)->TravId = i;
     // alloc enough memory
     Vec_IntClear( vTruth );
     Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) );
@@ -336,7 +206,7 @@ unsigned * Ivy_ManCutTruth( Ivy_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t *
         memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) );
     // compute truths for other nodes
     Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) )
-        Ivy_ManCutTruthOne( Ivy_ObjObj(pRoot, Leaf), vTruth, 8 );
+        Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 );
     return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth );
 }
 
@@ -373,21 +243,18 @@ Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManReadLevels( Ivy_Man_t * p )
+int Ivy_ManLevels( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj;
     int i, LevelMax = 0;
     Ivy_ManForEachPo( p, pObj, i )
-    {
-        pObj = Ivy_ObjFanin0(pObj);
-        LevelMax = IVY_MAX( LevelMax, (int)pObj->Level );
-    }
+        LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level );
     return LevelMax;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the real fanin.]
+  Synopsis    [Collect the latches.]
 
   Description []
                
@@ -396,20 +263,42 @@ int Ivy_ManReadLevels( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
+int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj )
 {
-    Ivy_Obj_t * pFanin;
-    if ( !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
-        return pObj;
-    pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
-    return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
+    if ( pObj->Level || Ivy_ObjIsCi(pObj) )
+        return pObj->Level;
+    if ( Ivy_ObjIsBuf(pObj) )
+        return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+    assert( Ivy_ObjIsNode(pObj) );
+    Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+    Ivy_ManResetLevels_rec( Ivy_ObjFanin1(pObj) );
+    return pObj->Level = Ivy_ObjLevelNew( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collect the latches.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManResetLevels( Ivy_Man_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    Ivy_ManForEachObj( p, pObj, i )
+        pObj->Level = 0;
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) );
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the cube has exactly one 1.]
+  Synopsis    [Recursively updates fanout levels.]
 
   Description []
                
@@ -418,14 +307,33 @@ Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthHasOneOne( unsigned uCube )
+void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    return (uCube & (uCube - 1)) == 0;
+    Ivy_Obj_t * pFanout;
+    Vec_Ptr_t * vFanouts;
+    int i, LevelNew;
+    assert( p->vFanouts );
+    assert( Ivy_ObjIsNode(pObj) );
+    vFanouts = Vec_PtrAlloc( 10 );
+    Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
+    {
+        if ( Ivy_ObjIsCo(pFanout) )
+        {
+//            assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax );
+            continue;
+        }
+        LevelNew = Ivy_ObjLevelNew( pFanout );
+        if ( (int)pFanout->Level == LevelNew )
+            continue;
+        pFanout->Level = LevelNew;
+        Ivy_ObjUpdateLevel_rec( p, pFanout );
+    }
+    Vec_PtrFree( vFanouts );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if two cubes are distance-1.]
+  Synopsis    [Compute the new required level.]
 
   Description []
                
@@ -434,15 +342,25 @@ static inline int Ivy_TruthHasOneOne( unsigned uCube )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
+int Ivy_ObjLevelRNew( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    unsigned uTemp = uCube1 | uCube2;
-    return Ivy_TruthHasOneOne( (uTemp >> 1) & uTemp & 0x55555555 );
+    Ivy_Obj_t * pFanout;
+    Vec_Ptr_t * vFanouts;
+    int i, Required, LevelNew = 1000000;
+    assert( p->vFanouts && p->vRequired );
+    vFanouts = Vec_PtrAlloc( 10 );
+    Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i )
+    {
+        Required = Vec_IntEntry(p->vRequired, pFanout->Id);
+        LevelNew = IVY_MIN( LevelNew, Required );
+    }
+    Vec_PtrFree( vFanouts );
+    return LevelNew - 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if two cubes differ in only one literal.]
+  Synopsis    [Recursively updates fanout levels.]
 
   Description []
                
@@ -451,15 +369,33 @@ static inline int Ivy_TruthCubesDist1( unsigned uCube1, unsigned uCube2 )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
+void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew )
 {
-    unsigned uTemp = uCube1 ^ uCube2;
-    return Ivy_TruthHasOneOne( ((uTemp >> 1) | uTemp) & 0x55555555 );
+    Ivy_Obj_t * pFanin;
+    if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) )
+        return;
+    assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) );
+    // process the first fanin
+    pFanin = Ivy_ObjFanin0(pObj);
+    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
+    {
+        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
+        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
+    }
+    if ( Ivy_ObjIsBuf(pObj) )
+        return;
+    // process the second fanin
+    pFanin = Ivy_ObjFanin1(pObj);
+    if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 )
+    {
+        Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 );
+        Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 );
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Combines two distance 1 cubes.]
+  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
 
   Description []
                
@@ -468,95 +404,128 @@ static inline int Ivy_TruthCubesDiff1( unsigned uCube1, unsigned uCube2 )
   SeeAlso     []
 
 ***********************************************************************/
-static inline unsigned Ivy_TruthCubesMerge( unsigned uCube1, unsigned uCube2 )
+int Ivy_ObjIsMuxType( Ivy_Obj_t * pNode )
 {
-    unsigned uTemp;
-    uTemp = uCube1 | uCube2;
-    uTemp &= (uTemp >> 1) & 0x55555555;
-    assert( Ivy_TruthHasOneOne(uTemp) );
-    uTemp |= (uTemp << 1);
-    return (uCube1 | uCube2) ^ uTemp;
+    Ivy_Obj_t * pNode0, * pNode1;
+    // check that the node is regular
+    assert( !Ivy_IsComplement(pNode) );
+    // if the node is not AND, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode) )
+        return 0;
+    // if the children are not complemented, this is not MUX
+    if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) )
+        return 0;
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // if the children are not ANDs, this is not MUX
+    if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) )
+        return 0;
+    // otherwise the node is MUX iff it has a pair of equal grandchildren
+    return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 
+           (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) ||
+           (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)));
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Estimates the number of AIG nodes in the truth table.]
+  Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
 
-  Description []
+  Description [If the node is a MUX, returns the control variable C.
+  Assigns nodes T and E to be the then and else variables of the MUX. 
+  Node C is never complemented. Nodes T and E can be complemented.
+  This function also recognizes EXOR/NEXOR gates as MUXes.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
+Ivy_Obj_t * Ivy_ObjRecognizeMux( Ivy_Obj_t * pNode, Ivy_Obj_t ** ppNodeT, Ivy_Obj_t ** ppNodeE )
 {
-    static unsigned short uResult[256];
-    static unsigned short uCover[81*81];
-    static char pVarCount[81*81];
-    int nMints, uCube, uCubeNew, i, k, c, nCubes, nRes, Counter;
-    assert( nVars <= 8 );
-    // create the cover
-    nCubes = 0;
-    nMints = (1 << nVars);
-    for ( i = 0; i < nMints; i++ )
-        if ( pTruth[i/32] & (1 << (i & 31)) )
-        {
-            uCube = 0;
-            for ( k = 0; k < nVars; k++ )
-                if ( i & (1 << k) )
-                    uCube |= (1 << ((k<<1)+1));
-                else
-                    uCube |= (1 << ((k<<1)+0));
-            uCover[nCubes] = uCube;
-            pVarCount[nCubes] = nVars;
-            nCubes++;
-//            Extra_PrintBinary( stdout, &uCube, 8 ); printf( "\n" );
+    Ivy_Obj_t * pNode0, * pNode1;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( Ivy_ObjIsMuxType(pNode) );
+    // get children
+    pNode0 = Ivy_ObjFanin0(pNode);
+    pNode1 = Ivy_ObjFanin1(pNode);
+    // find the control variable
+//    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
+    if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
         }
-    assert( nCubes <= 256 );
-    // reduce the cover by building larger cubes
-    for ( i = 1; i < nCubes; i++ )
-        for ( k = 0; k < i; k++ )
-            if ( pVarCount[i] && pVarCount[i] == pVarCount[k] && Ivy_TruthCubesDist1(uCover[i], uCover[k]) )
-            {
-                uCubeNew = Ivy_TruthCubesMerge(uCover[i], uCover[k]);
-                for ( c = i; c < nCubes; c++ )
-                    if ( uCubeNew == uCover[c] )
-                        break;
-                if ( c != nCubes )
-                    continue;
-                uCover[nCubes] = uCubeNew;
-                pVarCount[nCubes] = pVarCount[i] - 1;
-                nCubes++;
-                assert( nCubes < 81*81 );
-//                Extra_PrintBinary( stdout, &uCubeNew, 8 ); printf( "\n" );
-//                c = c;
-            }
-    // compact the cover
-    nRes = 0;
-    for ( i = nCubes -1; i >= 0; i-- )
+    }
+//    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
     {
-        for ( k = 0; k < nRes; k++ )
-            if ( (uCover[i] & uResult[k]) == uResult[k] )
-                break;
-        if ( k != nRes )
-            continue;
-        uResult[nRes++] = uCover[i];
+//        if ( Fraig_IsComplement(pNode1->p1) )
+        if ( Ivy_ObjFaninC0(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild0(pNode0);//pNode1->p1;
+        }
+    }
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) )
+    {
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p1 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild0(pNode1);//pNode2->p1;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
     }
-    // count the number of literals
-    Counter = 0;
-    for ( i = 0; i < nRes; i++ )
+//    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
+    else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) )
     {
-        for ( k = 0; k < nVars; k++ )
-            if ( uResult[i] & (3 << (k<<1)) )
-                Counter++;
+//        if ( Fraig_IsComplement(pNode1->p2) )
+        if ( Ivy_ObjFaninC1(pNode0) )
+        { // pNode2->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            return Ivy_ObjChild1(pNode1);//pNode2->p2;
+        }
+        else
+        { // pNode1->p2 is positive phase of C
+            *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1);
+            *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1);
+            return Ivy_ObjChild1(pNode0);//pNode1->p2;
+        }
     }
-    return Counter;
+    assert( 0 ); // this is not MUX
+    return NULL;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Tests the cover procedure.]
+  Synopsis    [Returns the real fanin.]
 
   Description []
                
@@ -565,17 +534,13 @@ int Ivy_TruthEstimateNodes( unsigned * pTruth, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TruthEstimateNodesTest()
+Ivy_Obj_t * Ivy_ObjReal( Ivy_Obj_t * pObj )
 {
-    unsigned uTruth[8];
-    int i;
-    for ( i = 0; i < 8; i++ )
-        uTruth[i] = ~(unsigned)0;
-    uTruth[3] ^= (1 << 13);
-//    uTruth[4] = 0xFFFFF;
-//    uTruth[0] = 0xFF;
-//    uTruth[0] ^= (1 << 3);
-    printf( "Number = %d.\n", Ivy_TruthEstimateNodes(uTruth, 8) );
+    Ivy_Obj_t * pFanin;
+    if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) )
+        return pObj;
+    pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) );
+    return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) );
 }
 
 ////////////////////////////////////////////////////////////////////////