src/sat/fraig/fraigMan.c

Go to the documentation of this file.

#include "fraigInt.h"


int timeSelect;
int timeAssign;


void Prove_ParamsSetDefault( Prove_Params_t * pParams )
{
    // clean the parameter structure
    memset( pParams, 0, sizeof(Prove_Params_t) );
    // general parameters
    pParams->fUseFraiging         = 1;       // enables fraiging
    pParams->fUseRewriting        = 1;       // enables rewriting
    pParams->fUseBdds             = 0;       // enables BDD construction when other methods fail
    pParams->fVerbose             = 0;       // prints verbose stats
    // iterations
    pParams->nItersMax            = 6;       // the number of iterations
    // mitering 
    pParams->nMiteringLimitStart  = 300;    // starting mitering limit
    pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
    // rewriting (currently not used)
    pParams->nRewritingLimitStart = 3;       // the number of rewriting iterations
    pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
    // fraiging 
    pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
    pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
    // last-gasp BDD construction
    pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
    pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
    // last-gasp mitering
//    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
    pParams->nMiteringLimitLast   = 0;       // final mitering limit
    // global SAT solver limits
    pParams->nTotalBacktrackLimit = 0;       // global limit on the number of backtracks
    pParams->nTotalInspectLimit   = 0;       // global limit on the number of clause inspects
//    pParams->nTotalInspectLimit   = 100000000;  // global limit on the number of clause inspects
}

void Prove_ParamsPrint( Prove_Params_t * pParams )
{
    printf( "CEC enging parameters:\n" );
    printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
    printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
    printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
    printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
    printf( "Solver iterations: %d\n", pParams->nItersMax );
    printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
    printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
    printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
    printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
    printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
    printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
    printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
    printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
    printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
    printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
    printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
    printf( "Parameter dump complete.\n" );
}

void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
{
    memset( pParams, 0, sizeof(Fraig_Params_t) );
    pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
    pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
    pParams->nBTLimit   = 99;                     // the max number of backtracks to perform
    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
    pParams->fFuncRed   =  1;                     // performs only one level hashing
    pParams->fFeedBack  =  1;                     // enables solver feedback
    pParams->fDist1Pats =  1;                     // enables distance-1 patterns
    pParams->fDoSparse  =  0;                     // performs equiv tests for sparse functions 
    pParams->fChoicing  =  0;                     // enables recording structural choices
    pParams->fTryProve  =  1;                     // tries to solve the final miter
    pParams->fVerbose   =  0;                     // the verbosiness flag
    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
    pParams->fInternal  =  0;                     // the flag indicates the internal run 
    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
    pParams->nInspLimit =  0;                     // the limit on the number of inspections
}

void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
{
    memset( pParams, 0, sizeof(Fraig_Params_t) );
    pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
    pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
    pParams->nBTLimit   = -1;                     // the max number of backtracks to perform
    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
    pParams->fFuncRed   =  1;                     // performs only one level hashing
    pParams->fFeedBack  =  1;                     // enables solver feedback
    pParams->fDist1Pats =  1;                     // enables distance-1 patterns
    pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
    pParams->fChoicing  =  0;                     // enables recording structural choices
    pParams->fTryProve  =  0;                     // tries to solve the final miter
    pParams->fVerbose   =  0;                     // the verbosiness flag
    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
    pParams->fInternal  =  0;                     // the flag indicates the internal run 
    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
    pParams->nInspLimit =  0;                     // the limit on the number of inspections
}

Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
{
    Fraig_Params_t Params;
    Fraig_Man_t * p;

    // set the random seed for simulation
//    srand( 0xFEEDDEAF );
    srand( 0xDEADCAFE );

    // set parameters for equivalence checking
    if ( pParams == NULL )
        Fraig_ParamsSetDefault( pParams = &Params );
    // adjust the amount of simulation info
    if ( pParams->nPatsRand < 128 )
        pParams->nPatsRand = 128;
    if ( pParams->nPatsRand > 32768 )
        pParams->nPatsRand = 32768;
    if ( pParams->nPatsDyna < 128 )
        pParams->nPatsDyna = 128;
    if ( pParams->nPatsDyna > 32768 )
        pParams->nPatsDyna = 32768;
    // if reduction is not performed, allocate minimum simulation info
    if ( !pParams->fFuncRed )
        pParams->nPatsRand = pParams->nPatsDyna = 128;

    // start the manager
    p = ALLOC( Fraig_Man_t, 1 );
    memset( p, 0, sizeof(Fraig_Man_t) );

    // set the default parameters
    p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand );  // the number of words of random simulation info
    p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna );  // the number of patterns for dynamic simulation info
    p->nBTLimit   = pParams->nBTLimit;    // -1 means infinite backtrack limit
    p->nSeconds   = pParams->nSeconds;    // the timeout for the final miter
    p->fFuncRed   = pParams->fFuncRed;    // enables functional reduction (otherwise, only one-level hashing is performed)
    p->fFeedBack  = pParams->fFeedBack;   // enables solver feedback (the use of counter-examples in simulation)
    p->fDist1Pats = pParams->fDist1Pats;  // enables solver feedback (the use of counter-examples in simulation)
    p->fDoSparse  = pParams->fDoSparse;   // performs equivalence checking for sparse functions (whose sim-info is 0)
    p->fChoicing  = pParams->fChoicing;   // disable accumulation of structural choices (keeps only the first choice)
    p->fTryProve  = pParams->fTryProve;   // disable accumulation of structural choices (keeps only the first choice)
    p->fVerbose   = pParams->fVerbose;    // disable verbose output
    p->fVerboseP  = pParams->fVerboseP;   // disable verbose output
    p->nInspLimit = pParams->nInspLimit;  // the limit on the number of inspections

    // start memory managers
    p->mmNodes    = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
    p->mmSims     = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) );
    // allocate node arrays
    p->vInputs    = Fraig_NodeVecAlloc( 1000 );    // the array of primary inputs
    p->vOutputs   = Fraig_NodeVecAlloc( 1000 );    // the array of primary outputs
    p->vNodes     = Fraig_NodeVecAlloc( 1000 );    // the array of internal nodes
    // start the tables
    p->pTableS    = Fraig_HashTableCreate( 1000 ); // hashing by structure
    p->pTableF    = Fraig_HashTableCreate( 1000 ); // hashing by function
    p->pTableF0   = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions)
    // create the constant node
    p->pConst1    = Fraig_NodeCreateConst( p );
    // initialize SAT solver feedback data structures
    Fraig_FeedBackInit( p );
    // initialize other variables
    p->vProj      = Msat_IntVecAlloc( 10 ); 
    p->nTravIds   = 1;
    p->nTravIds2  = 1;
    return p;
}

void Fraig_ManFree( Fraig_Man_t * p )
{
    int i;
    if ( p->fVerbose )   
    {
        if ( p->fChoicing ) Fraig_ManReportChoices( p );
        Fraig_ManPrintStats( p );
//        Fraig_TablePrintStatsS( p );
//        Fraig_TablePrintStatsF( p );
//        Fraig_TablePrintStatsF0( p );
    }
 
    for ( i = 0; i < p->vNodes->nSize; i++ )
        if ( p->vNodes->pArray[i]->vFanins )
        {
            Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins );
            p->vNodes->pArray[i]->vFanins = NULL;
        }

    if ( p->vInputs )    Fraig_NodeVecFree( p->vInputs );
    if ( p->vNodes )     Fraig_NodeVecFree( p->vNodes );
    if ( p->vOutputs )   Fraig_NodeVecFree( p->vOutputs );

    if ( p->pTableS )    Fraig_HashTableFree( p->pTableS );
    if ( p->pTableF )    Fraig_HashTableFree( p->pTableF );
    if ( p->pTableF0 )   Fraig_HashTableFree( p->pTableF0 );

    if ( p->pSat )       Msat_SolverFree( p->pSat );
    if ( p->vProj )      Msat_IntVecFree( p->vProj );
    if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
    if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
    if ( p->pModel )     free( p->pModel );

    Fraig_MemFixedStop( p->mmNodes, 0 );
    Fraig_MemFixedStop( p->mmSims, 0 );

    if ( p->pSuppS )
    {
        FREE( p->pSuppS[0] );
        FREE( p->pSuppS );
    }
    if ( p->pSuppF )
    {
        FREE( p->pSuppF[0] );
        FREE( p->pSuppF );
    }

    FREE( p->ppOutputNames );
    FREE( p->ppInputNames );
    FREE( p );
}

void Fraig_ManCreateSolver( Fraig_Man_t * p )
{
    extern int timeSelect;
    extern int timeAssign;
    assert( p->pSat == NULL );
    // allocate data for SAT solving
    p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
    p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
    p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
    p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
    timeSelect = 0;
    timeAssign = 0;
}

 
void Fraig_ManPrintStats( Fraig_Man_t * p )
{
    double nMemory;
    int clk = clock();
    nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * 
        (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
    printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
        p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
    printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", 
        Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
    if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
    Fraig_PrintTime( "AIG simulation  ", p->timeSims  );
    Fraig_PrintTime( "AIG traversal   ", p->timeTrav  );
    Fraig_PrintTime( "Solver feedback ", p->timeFeed  );
    Fraig_PrintTime( "SAT solving     ", p->timeSat   );
    Fraig_PrintTime( "Network update  ", p->timeToNet );
    Fraig_PrintTime( "TOTAL RUNTIME   ", p->timeTotal );
    if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); }
    if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); }
    if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); }
    if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
//    PRT( "Selection ", timeSelect );
//    PRT( "Assignment", timeAssign );
}

Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
{
    Fraig_NodeVec_t * vInfo;
    unsigned * pUnsigned;
    int i;
    assert( nSize > 0 && nWords > 0 );
    vInfo = Fraig_NodeVecAlloc( nSize );
    pUnsigned = ALLOC( unsigned, nSize * nWords );
    vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
    if ( fClean )
        memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
    for ( i = 1; i < nSize; i++ )
        vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
    vInfo->nSize = nSize;
    return vInfo;
}

Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
{
    Fraig_NodeVec_t * vInfo;
    Fraig_Node_t * pNode;
    unsigned * pUnsigned;
    int nRandom, nDynamic;
    int i, k, nWords;

    nRandom  = Fraig_ManReadPatternNumRandom( p );
    nDynamic = Fraig_ManReadPatternNumDynamic( p );
    nWords = nRandom / 32 + nDynamic / 32;

    vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
    for ( i = 0; i < p->vNodes->nSize; i++ )
    {
        pNode = p->vNodes->pArray[i];
        assert( i == pNode->Num );
        pUnsigned = (unsigned *)vInfo->pArray[i];
        for ( k = 0; k < nRandom / 32; k++ )
            pUnsigned[k] = pNode->puSimR[k];
        for ( k = 0; k < nDynamic / 32; k++ )
            pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
    }
    return vInfo;
}

int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
{
    int fCompl1, fCompl2, i;

    fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
    fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;

    pNode1 = Fraig_Regular(pNode1);
    pNode2 = Fraig_Regular(pNode2);
    assert( pNode1 != pNode2 );
    
    // check the simulation info
    if ( fCompl1 && fCompl2 )
    {
        for ( i = 0; i < p->nWordsRand; i++ )
            if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
                return 0;
        for ( i = 0; i < p->iWordStart; i++ )
            if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
                return 0;
        return 1;
    }
    if ( !fCompl1 && fCompl2 )
    {
        for ( i = 0; i < p->nWordsRand; i++ )
            if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
                return 0;
        for ( i = 0; i < p->iWordStart; i++ )
            if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
                return 0;
        return 1;
    }
    if ( fCompl1 && !fCompl2 )
    {
        for ( i = 0; i < p->nWordsRand; i++ )
            if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
                return 0;
        for ( i = 0; i < p->iWordStart; i++ )
            if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
                return 0;
        return 1;
    }
//    if ( fCompl1 && fCompl2 )
    {
        for ( i = 0; i < p->nWordsRand; i++ )
            if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
                return 0;
        for ( i = 0; i < p->iWordStart; i++ )
            if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
                return 0;
        return 1;
    }
}

void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
{
    Fraig_Node_t * pNode;
    int i, fComp, RetValue;
    if ( p->pSat == NULL )
        Fraig_ManCreateSolver( p );
    // create four clauses
    Msat_IntVecClear( p->vProj );
    for ( i = 0; i < nNodes; i++ )
    {
        pNode = Fraig_Regular(ppNodes[i]);
        fComp = Fraig_IsComplement(ppNodes[i]);
        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
//        printf( "%d(%d) ", pNode->Num, fComp );
    }
//    printf( "\n" );
    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
    assert( RetValue );
}

---