abc/src/proof/fraig/fraigUtil.c
/**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     []

***********************************************************************/
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.]




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 . ]
Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE )
{
    Fraig_Node_t * pNode1, * pNode2;
    assert( !Fraig_IsComplement(pNode) );
    assert( Fraig_NodeIsMuxType(pNode) );
    pNode1 = Fraig_Regular(pNode->p1);
    pNode2 = Fraig_Regular(pNode->p2);
    if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { 
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p1;
        }
        else
        { 
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p1) )
        { 
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p2);
            return pNode2->p2;
        }
        else
        { 
            *ppNodeT = Fraig_Not(pNode1->p2);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p1;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { 
            *ppNodeT = Fraig_Not(pNode2->p2);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p1;
        }
        else
        { 
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p2);
            return pNode1->p2;
        }
    }
    else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
    {
        if ( Fraig_IsComplement(pNode1->p2) )
        { 
            *ppNodeT = Fraig_Not(pNode2->p1);
            *ppNodeE = Fraig_Not(pNode1->p1);
            return pNode2->p2;
        }
        else
        { 
            *ppNodeT = Fraig_Not(pNode1->p1);
            *ppNodeE = Fraig_Not(pNode2->p1);
            return pNode1->p2;
        }
    }
    assert( 0 ); 
    return NULL;
}
Fraig_Node_t * Fraig_NodeRecognizeMux ( Fraig_Node_t * pNode , Fraig_Node_t * * ppNodeT , Fraig_Node_t * * ppNodeE ) { Fraig_Node_t * pNode1 , * pNode2 ; assert ( ! Fraig_IsComplement ( pNode ) ) ; assert ( Fraig_NodeIsMuxType ( pNode ) ) ; pNode1 = Fraig_Regular ( pNode -> p1 ) ; pNode2 = Fraig_Regular ( pNode -> p2 ) ; if ( pNode1 -> p1 == Fraig_Not ( pNode2 -> p1 ) ) { if ( Fraig_IsComplement ( pNode1 -> p1 ) ) { * ppNodeT = Fraig_Not ( pNode2 -> p2 ) ; * ppNodeE = Fraig_Not ( pNode1 -> p2 ) ; return pNode2 -> p1 ; } else { * ppNodeT = Fraig_Not ( pNode1 -> p2 ) ; * ppNodeE = Fraig_Not ( pNode2 -> p2 ) ; return pNode1 -> p1 ; } } else if ( pNode1 -> p1 == Fraig_Not ( pNode2 -> p2 ) ) { if ( Fraig_IsComplement ( pNode1 -> p1 ) ) { * ppNodeT = Fraig_Not ( pNode2 -> p1 ) ; * ppNodeE = Fraig_Not ( pNode1 -> p2 ) ; return pNode2 -> p2 ; } else { * ppNodeT = Fraig_Not ( pNode1 -> p2 ) ; * ppNodeE = Fraig_Not ( pNode2 -> p1 ) ; return pNode1 -> p1 ; } } else if ( pNode1 -> p2 == Fraig_Not ( pNode2 -> p1 ) ) { if ( Fraig_IsComplement ( pNode1 -> p2 ) ) { * ppNodeT = Fraig_Not ( pNode2 -> p2 ) ; * ppNodeE = Fraig_Not ( pNode1 -> p1 ) ; return pNode2 -> p1 ; } else { * ppNodeT = Fraig_Not ( pNode1 -> p1 ) ; * ppNodeE = Fraig_Not ( pNode2 -> p2 ) ; return pNode1 -> p2 ; } } else if ( pNode1 -> p2 == Fraig_Not ( pNode2 -> p2 ) ) { if ( Fraig_IsComplement ( pNode1 -> p2 ) ) { * ppNodeT = Fraig_Not ( pNode2 -> p1 ) ; * ppNodeE = Fraig_Not ( pNode1 -> p1 ) ; return pNode2 -> p2 ; } else { * ppNodeT = Fraig_Not ( pNode1 -> p1 ) ; * ppNodeE = Fraig_Not ( pNode2 -> p1 ) ; return pNode1 -> p2 ; } } assert ( 0 ) ; return NULL ; }
Function
Synopsis    [Recognizes what nodes are control and data inputs of a MUX.]
Function Synopsis [ Recognizes what nodes are control and data inputs of a MUX . ]
// get children // find the control variable // pNode2->p1 is positive phase of C // pNode1->p1 is positive phase of C // pNode2->p2 is positive phase of C // pNode1->p1 is positive phase of C // pNode2->p1 is positive phase of C // pNode1->p2 is positive phase of C // pNode2->p2 is positive phase of C // pNode1->p2 is positive phase of C // this is not MUX