abc/src/proof/fraig/fraigSat.c
/**Function*************************************************************

  Synopsis    [Collect variables using their proximity from the nodes.]

  Description [This procedure creates a variable order based on collecting
  first the nodes that are the closest to the given two target nodes.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Collect variables using their proximity from the nodes.]

Description [This procedure creates a variable order based on collecting
first the nodes that are the closest to the given two target nodes.]




Function Synopsis [ Collect variables using their proximity from the nodes . ] Description [ This procedure creates a variable order based on collecting first the nodes that are the closest to the given two target nodes . ]
void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
{
    Fraig_Node_t * pNode, * pFanin;
    int i, k, Number, fUseMuxes = 1;
    int nVarsAlloc;
    assert( pOld != pNew );
    assert( !Fraig_IsComplement(pOld) );
    assert( !Fraig_IsComplement(pNew) );
    pMan->nTravIds++;
    nVarsAlloc = Msat_IntVecReadSize(pMan->vVarsUsed);
    Msat_IntVecFill( pMan->vVarsUsed, nVarsAlloc, 0 );
    Msat_IntVecClear( pMan->vVarsInt );
    Msat_IntVecPush( pMan->vVarsInt, pOld->Num );
    Msat_IntVecWriteEntry( pMan->vVarsUsed, pOld->Num, 1 );
    pOld->TravId = pMan->nTravIds;
    Msat_IntVecPush( pMan->vVarsInt, pNew->Num );
    Msat_IntVecWriteEntry( pMan->vVarsUsed, pNew->Num, 1 );
    pNew->TravId = pMan->nTravIds;
    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
    {
        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
        pNode = pMan->vNodes->pArray[Number];
        if ( !Fraig_NodeIsAnd(pNode) )
            continue;
        if ( pNode->vFanins == NULL )
        {
            assert( pNode->fClauses == 0 );
            if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
            {
                pNode->vFanins = Fraig_NodeVecAlloc( 4 );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p1) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p1)->p2) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p1) );
                Fraig_NodeVecPushUnique( pNode->vFanins, Fraig_Regular(Fraig_Regular(pNode->p2)->p2) );
                Fraig_SupergateAddClausesMux( pMan, pNode );
                nMuxes++;
            }
            else
            {
                pNode->vFanins = Fraig_CollectSupergate( pNode, fUseMuxes );
                Fraig_SupergateAddClauses( pMan, pNode, pNode->vFanins );
            }
            assert( pNode->vFanins->nSize > 1 );
            pNode->fClauses = 1;
            pMan->nVarsClauses++;
            pNode->fMark2 = 1; 
        }
        for ( k = 0; k < pNode->vFanins->nSize; k++ )
        {
            pFanin = Fraig_Regular(pNode->vFanins->pArray[k]);
            if ( pFanin->TravId == pMan->nTravIds ) 
                continue;
            Msat_IntVecPush( pMan->vVarsInt, pFanin->Num );
            Msat_IntVecWriteEntry( pMan->vVarsUsed, pFanin->Num, 1 );
            pFanin->TravId = pMan->nTravIds;
        }
    }
    Fraig_SetupAdjacentMark( pMan, pMan->vVarsInt );
}
void Fraig_OrderVariables ( Fraig_Man_t * pMan , Fraig_Node_t * pOld , Fraig_Node_t * pNew ) { Fraig_Node_t * pNode , * pFanin ; int i , k , Number , fUseMuxes = 1 ; int nVarsAlloc ; assert ( pOld != pNew ) ; assert ( ! Fraig_IsComplement ( pOld ) ) ; assert ( ! Fraig_IsComplement ( pNew ) ) ; pMan -> nTravIds ++ ; nVarsAlloc = Msat_IntVecReadSize ( pMan -> vVarsUsed ) ; Msat_IntVecFill ( pMan -> vVarsUsed , nVarsAlloc , 0 ) ; Msat_IntVecClear ( pMan -> vVarsInt ) ; Msat_IntVecPush ( pMan -> vVarsInt , pOld -> Num ) ; Msat_IntVecWriteEntry ( pMan -> vVarsUsed , pOld -> Num , 1 ) ; pOld -> TravId = pMan -> nTravIds ; Msat_IntVecPush ( pMan -> vVarsInt , pNew -> Num ) ; Msat_IntVecWriteEntry ( pMan -> vVarsUsed , pNew -> Num , 1 ) ; pNew -> TravId = pMan -> nTravIds ; for ( i = 0 ; i < Msat_IntVecReadSize ( pMan -> vVarsInt ) ; i ++ ) { Number = Msat_IntVecReadEntry ( pMan -> vVarsInt , i ) ; pNode = pMan -> vNodes -> pArray [ Number ] ; if ( ! Fraig_NodeIsAnd ( pNode ) ) continue ; if ( pNode -> vFanins == NULL ) { assert ( pNode -> fClauses == 0 ) ; if ( fUseMuxes && Fraig_NodeIsMuxType ( pNode ) ) { pNode -> vFanins = Fraig_NodeVecAlloc ( 4 ) ; Fraig_NodeVecPushUnique ( pNode -> vFanins , Fraig_Regular ( Fraig_Regular ( pNode -> p1 ) -> p1 ) ) ; Fraig_NodeVecPushUnique ( pNode -> vFanins , Fraig_Regular ( Fraig_Regular ( pNode -> p1 ) -> p2 ) ) ; Fraig_NodeVecPushUnique ( pNode -> vFanins , Fraig_Regular ( Fraig_Regular ( pNode -> p2 ) -> p1 ) ) ; Fraig_NodeVecPushUnique ( pNode -> vFanins , Fraig_Regular ( Fraig_Regular ( pNode -> p2 ) -> p2 ) ) ; Fraig_SupergateAddClausesMux ( pMan , pNode ) ; nMuxes ++ ; } else { pNode -> vFanins = Fraig_CollectSupergate ( pNode , fUseMuxes ) ; Fraig_SupergateAddClauses ( pMan , pNode , pNode -> vFanins ) ; } assert ( pNode -> vFanins -> nSize > 1 ) ; pNode -> fClauses = 1 ; pMan -> nVarsClauses ++ ; pNode -> fMark2 = 1 ; } for ( k = 0 ; k < pNode -> vFanins -> nSize ; k ++ ) { pFanin = Fraig_Regular ( pNode -> vFanins -> pArray [ k ] ) ; if ( pFanin -> TravId == pMan -> nTravIds ) continue ; Msat_IntVecPush ( pMan -> vVarsInt , pFanin -> Num ) ; Msat_IntVecWriteEntry ( pMan -> vVarsUsed , pFanin -> Num , 1 ) ; pFanin -> TravId = pMan -> nTravIds ; } } Fraig_SetupAdjacentMark ( pMan , pMan -> vVarsInt ) ; }
Function
Synopsis    [Collect variables using their proximity from the nodes.]
Function Synopsis [ Collect variables using their proximity from the nodes . ]
// clean the variables // add the first node // add the second node // create the variable order // get the new node on the frontier // if the node does not have fanins, create them // create the fanins of the supergate // detecting a fanout-free cone (experiment only) //            Fraig_DetectFanoutFreeCone( pMan, pNode ); //                Fraig_DetectFanoutFreeConeMux( pMan, pNode ); // goes together with Fraig_SetupAdjacentMark() // explore the implication fanins of pNode // already collected // collect and mark // set up the adjacent variable information //    Fraig_SetupAdjacent( pMan, pMan->vVarsInt );