abc/src/base/abci/abcExact.c
/**Function*************************************************************

  Synopsis    [Setup variables to find network with nGates gates.]

***********************************************************************/
Function
Synopsis    [Setup variables to find network with nGates gates.]
Function Synopsis [ Setup variables to find network with nGates gates . ]
static void Ses_ManCreateVars( Ses_Man_t * pSes, int nGates )
{
    int i;
    if ( pSes->fSatVerbose )
    {
        printf( "create variables for network with %d functions over %d variables and %d/%d gates\n", pSes->nSpecFunc, pSes->nSpecVars, nGates, pSes->nMaxGates );
    }
    pSes->nGates      = nGates;
    pSes->nSimVars    = nGates * pSes->nRows;
    pSes->nOutputVars = pSes->nSpecFunc * nGates;
    pSes->nGateVars   = nGates * 3;
    pSes->nSelectVars = 0;
    for ( i = pSes->nSpecVars; i < pSes->nSpecVars + nGates; ++i )
        pSes->nSelectVars += ( i * ( i - 1 ) ) / 2;
    pSes->nDepthVars = pSes->nMaxDepth > 0 ? nGates * pSes->nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0;
    pSes->nDepthOffset  = 0;
    pSes->nSelectOffset = pSes->nDepthVars;
    pSes->nGateOffset   = pSes->nDepthVars + pSes->nSelectVars;
    pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars;
    pSes->nSimOffset    = pSes->nDepthVars + pSes->nSelectVars + pSes->nGateVars + pSes->nOutputVars;
    if ( pSes->pSat )
        sat_solver_restart( pSes->pSat );
    else
        pSes->pSat = sat_solver_new();
    sat_solver_setnvars( pSes->pSat, pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars + pSes->nDepthVars );
}
static void Ses_ManCreateVars ( Ses_Man_t * pSes , int nGates ) { int i ; if ( pSes -> fSatVerbose ) { printf ( " \n " , pSes -> nSpecFunc , pSes -> nSpecVars , nGates , pSes -> nMaxGates ) ; } pSes -> nGates = nGates ; pSes -> nSimVars = nGates * pSes -> nRows ; pSes -> nOutputVars = pSes -> nSpecFunc * nGates ; pSes -> nGateVars = nGates * 3 ; pSes -> nSelectVars = 0 ; for ( i = pSes -> nSpecVars ; i < pSes -> nSpecVars + nGates ; ++ i ) pSes -> nSelectVars += ( i * ( i - 1 ) ) / 2 ; pSes -> nDepthVars = pSes -> nMaxDepth > 0 ? nGates * pSes -> nArrTimeMax + ( nGates * ( nGates + 1 ) ) / 2 : 0 ; pSes -> nDepthOffset = 0 ; pSes -> nSelectOffset = pSes -> nDepthVars ; pSes -> nGateOffset = pSes -> nDepthVars + pSes -> nSelectVars ; pSes -> nOutputOffset = pSes -> nDepthVars + pSes -> nSelectVars + pSes -> nGateVars ; pSes -> nSimOffset = pSes -> nDepthVars + pSes -> nSelectVars + pSes -> nGateVars + pSes -> nOutputVars ; if ( pSes -> pSat ) sat_solver_restart ( pSes -> pSat ) ; else pSes -> pSat = sat_solver_new ( ) ; sat_solver_setnvars ( pSes -> pSat , pSes -> nSimVars + pSes -> nOutputVars + pSes -> nGateVars + pSes -> nSelectVars + pSes -> nDepthVars ) ; }
Function
Synopsis    [Setup variables to find network with nGates gates.]
Function Synopsis [ Setup variables to find network with nGates gates . ]
/* pSes->nSimOffset    = 0; */ /* pSes->nOutputOffset = pSes->nSimVars; */ /* pSes->nGateOffset   = pSes->nSimVars + pSes->nOutputVars; */ /* pSes->nSelectOffset = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars; */ /* pSes->nDepthOffset  = pSes->nSimVars + pSes->nOutputVars + pSes->nGateVars + pSes->nSelectVars; */ /* pSes->nDepthOffset  = 0; */ /* pSes->nSelectOffset = pSes->nDepthVars; */ /* pSes->nOutputOffset = pSes->nDepthVars + pSes->nSelectVars; */ /* pSes->nGateOffset   = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars; */ /* pSes->nSimOffset    = pSes->nDepthVars + pSes->nSelectVars + pSes->nOutputVars + pSes->nGateVars; */ /* if we already have a SAT solver, then restart it (this saves a lot of time) */