src/sat/fraig/fraigMan.c File Reference

#include "fraigInt.h"
Include dependency graph for fraigMan.c:

Go to the source code of this file.

Functions

void Prove_ParamsSetDefault (Prove_Params_t *pParams)
void Prove_ParamsPrint (Prove_Params_t *pParams)
void Fraig_ParamsSetDefault (Fraig_Params_t *pParams)
void Fraig_ParamsSetDefaultFull (Fraig_Params_t *pParams)
Fraig_Man_t * Fraig_ManCreate (Fraig_Params_t *pParams)
void Fraig_ManFree (Fraig_Man_t *p)
void Fraig_ManCreateSolver (Fraig_Man_t *p)
void Fraig_ManPrintStats (Fraig_Man_t *p)
Fraig_NodeVec_t * Fraig_UtilInfoAlloc (int nSize, int nWords, bool fClean)
Fraig_NodeVec_t * Fraig_ManGetSimInfo (Fraig_Man_t *p)
int Fraig_ManCheckClauseUsingSimInfo (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2)
void Fraig_ManAddClause (Fraig_Man_t *p, Fraig_Node_t **ppNodes, int nNodes)

Variables

int timeSelect
int timeAssign

Function Documentation

void Fraig_ManAddClause ( Fraig_Man_t *  p,
Fraig_Node_t **  ppNodes,
int  nNodes 
)

Function*************************************************************

Synopsis [Adds clauses to the solver.]

Description [This procedure is used to add external clauses to the solver. The clauses are given by sets of nodes. Each node stands for one literal. If the node is complemented, the literal is negated.]

SideEffects []

SeeAlso []

Definition at line 517 of file fraigMan.c.

00518 {
00519     Fraig_Node_t * pNode;
00520     int i, fComp, RetValue;
00521     if ( p->pSat == NULL )
00522         Fraig_ManCreateSolver( p );
00523     // create four clauses
00524     Msat_IntVecClear( p->vProj );
00525     for ( i = 0; i < nNodes; i++ )
00526     {
00527         pNode = Fraig_Regular(ppNodes[i]);
00528         fComp = Fraig_IsComplement(ppNodes[i]);
00529         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
00530 //        printf( "%d(%d) ", pNode->Num, fComp );
00531     }
00532 //    printf( "\n" );
00533     RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00534     assert( RetValue );
00535 }

int Fraig_ManCheckClauseUsingSimInfo ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2 
)

Function*************************************************************

Synopsis [Returns 1 if A v B is always true based on the siminfo.]

Description [A v B is always true iff A' * B' is always false.]

SideEffects []

SeeAlso []

Definition at line 450 of file fraigMan.c.

00451 {
00452     int fCompl1, fCompl2, i;
00453 
00454     fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
00455     fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
00456 
00457     pNode1 = Fraig_Regular(pNode1);
00458     pNode2 = Fraig_Regular(pNode2);
00459     assert( pNode1 != pNode2 );
00460     
00461     // check the simulation info
00462     if ( fCompl1 && fCompl2 )
00463     {
00464         for ( i = 0; i < p->nWordsRand; i++ )
00465             if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
00466                 return 0;
00467         for ( i = 0; i < p->iWordStart; i++ )
00468             if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
00469                 return 0;
00470         return 1;
00471     }
00472     if ( !fCompl1 && fCompl2 )
00473     {
00474         for ( i = 0; i < p->nWordsRand; i++ )
00475             if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
00476                 return 0;
00477         for ( i = 0; i < p->iWordStart; i++ )
00478             if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
00479                 return 0;
00480         return 1;
00481     }
00482     if ( fCompl1 && !fCompl2 )
00483     {
00484         for ( i = 0; i < p->nWordsRand; i++ )
00485             if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
00486                 return 0;
00487         for ( i = 0; i < p->iWordStart; i++ )
00488             if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
00489                 return 0;
00490         return 1;
00491     }
00492 //    if ( fCompl1 && fCompl2 )
00493     {
00494         for ( i = 0; i < p->nWordsRand; i++ )
00495             if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
00496                 return 0;
00497         for ( i = 0; i < p->iWordStart; i++ )
00498             if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
00499                 return 0;
00500         return 1;
00501     }
00502 }

Fraig_Man_t* Fraig_ManCreate ( Fraig_Params_t *  pParams  ) 

Function*************************************************************

Synopsis [Creates the new FRAIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file fraigMan.c.

00182 {
00183     Fraig_Params_t Params;
00184     Fraig_Man_t * p;
00185 
00186     // set the random seed for simulation
00187 //    srand( 0xFEEDDEAF );
00188     srand( 0xDEADCAFE );
00189 
00190     // set parameters for equivalence checking
00191     if ( pParams == NULL )
00192         Fraig_ParamsSetDefault( pParams = &Params );
00193     // adjust the amount of simulation info
00194     if ( pParams->nPatsRand < 128 )
00195         pParams->nPatsRand = 128;
00196     if ( pParams->nPatsRand > 32768 )
00197         pParams->nPatsRand = 32768;
00198     if ( pParams->nPatsDyna < 128 )
00199         pParams->nPatsDyna = 128;
00200     if ( pParams->nPatsDyna > 32768 )
00201         pParams->nPatsDyna = 32768;
00202     // if reduction is not performed, allocate minimum simulation info
00203     if ( !pParams->fFuncRed )
00204         pParams->nPatsRand = pParams->nPatsDyna = 128;
00205 
00206     // start the manager
00207     p = ALLOC( Fraig_Man_t, 1 );
00208     memset( p, 0, sizeof(Fraig_Man_t) );
00209 
00210     // set the default parameters
00211     p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand );  // the number of words of random simulation info
00212     p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna );  // the number of patterns for dynamic simulation info
00213     p->nBTLimit   = pParams->nBTLimit;    // -1 means infinite backtrack limit
00214     p->nSeconds   = pParams->nSeconds;    // the timeout for the final miter
00215     p->fFuncRed   = pParams->fFuncRed;    // enables functional reduction (otherwise, only one-level hashing is performed)
00216     p->fFeedBack  = pParams->fFeedBack;   // enables solver feedback (the use of counter-examples in simulation)
00217     p->fDist1Pats = pParams->fDist1Pats;  // enables solver feedback (the use of counter-examples in simulation)
00218     p->fDoSparse  = pParams->fDoSparse;   // performs equivalence checking for sparse functions (whose sim-info is 0)
00219     p->fChoicing  = pParams->fChoicing;   // disable accumulation of structural choices (keeps only the first choice)
00220     p->fTryProve  = pParams->fTryProve;   // disable accumulation of structural choices (keeps only the first choice)
00221     p->fVerbose   = pParams->fVerbose;    // disable verbose output
00222     p->fVerboseP  = pParams->fVerboseP;   // disable verbose output
00223     p->nInspLimit = pParams->nInspLimit;  // the limit on the number of inspections
00224 
00225     // start memory managers
00226     p->mmNodes    = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
00227     p->mmSims     = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) );
00228     // allocate node arrays
00229     p->vInputs    = Fraig_NodeVecAlloc( 1000 );    // the array of primary inputs
00230     p->vOutputs   = Fraig_NodeVecAlloc( 1000 );    // the array of primary outputs
00231     p->vNodes     = Fraig_NodeVecAlloc( 1000 );    // the array of internal nodes
00232     // start the tables
00233     p->pTableS    = Fraig_HashTableCreate( 1000 ); // hashing by structure
00234     p->pTableF    = Fraig_HashTableCreate( 1000 ); // hashing by function
00235     p->pTableF0   = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions)
00236     // create the constant node
00237     p->pConst1    = Fraig_NodeCreateConst( p );
00238     // initialize SAT solver feedback data structures
00239     Fraig_FeedBackInit( p );
00240     // initialize other variables
00241     p->vProj      = Msat_IntVecAlloc( 10 ); 
00242     p->nTravIds   = 1;
00243     p->nTravIds2  = 1;
00244     return p;
00245 }

void Fraig_ManCreateSolver ( Fraig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Prepares the SAT solver to run on the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file fraigMan.c.

00322 {
00323     extern int timeSelect;
00324     extern int timeAssign;
00325     assert( p->pSat == NULL );
00326     // allocate data for SAT solving
00327     p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
00328     p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
00329     p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
00330     p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
00331     timeSelect = 0;
00332     timeAssign = 0;
00333 }

void Fraig_ManFree ( Fraig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Deallocates the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file fraigMan.c.

00259 {
00260     int i;
00261     if ( p->fVerbose )   
00262     {
00263         if ( p->fChoicing ) Fraig_ManReportChoices( p );
00264         Fraig_ManPrintStats( p );
00265 //        Fraig_TablePrintStatsS( p );
00266 //        Fraig_TablePrintStatsF( p );
00267 //        Fraig_TablePrintStatsF0( p );
00268     }
00269  
00270     for ( i = 0; i < p->vNodes->nSize; i++ )
00271         if ( p->vNodes->pArray[i]->vFanins )
00272         {
00273             Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins );
00274             p->vNodes->pArray[i]->vFanins = NULL;
00275         }
00276 
00277     if ( p->vInputs )    Fraig_NodeVecFree( p->vInputs );
00278     if ( p->vNodes )     Fraig_NodeVecFree( p->vNodes );
00279     if ( p->vOutputs )   Fraig_NodeVecFree( p->vOutputs );
00280 
00281     if ( p->pTableS )    Fraig_HashTableFree( p->pTableS );
00282     if ( p->pTableF )    Fraig_HashTableFree( p->pTableF );
00283     if ( p->pTableF0 )   Fraig_HashTableFree( p->pTableF0 );
00284 
00285     if ( p->pSat )       Msat_SolverFree( p->pSat );
00286     if ( p->vProj )      Msat_IntVecFree( p->vProj );
00287     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
00288     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
00289     if ( p->pModel )     free( p->pModel );
00290 
00291     Fraig_MemFixedStop( p->mmNodes, 0 );
00292     Fraig_MemFixedStop( p->mmSims, 0 );
00293 
00294     if ( p->pSuppS )
00295     {
00296         FREE( p->pSuppS[0] );
00297         FREE( p->pSuppS );
00298     }
00299     if ( p->pSuppF )
00300     {
00301         FREE( p->pSuppF[0] );
00302         FREE( p->pSuppF );
00303     }
00304 
00305     FREE( p->ppOutputNames );
00306     FREE( p->ppInputNames );
00307     FREE( p );
00308 }

Fraig_NodeVec_t* Fraig_ManGetSimInfo ( Fraig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Returns simulation info of all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 413 of file fraigMan.c.

00414 {
00415     Fraig_NodeVec_t * vInfo;
00416     Fraig_Node_t * pNode;
00417     unsigned * pUnsigned;
00418     int nRandom, nDynamic;
00419     int i, k, nWords;
00420 
00421     nRandom  = Fraig_ManReadPatternNumRandom( p );
00422     nDynamic = Fraig_ManReadPatternNumDynamic( p );
00423     nWords = nRandom / 32 + nDynamic / 32;
00424 
00425     vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
00426     for ( i = 0; i < p->vNodes->nSize; i++ )
00427     {
00428         pNode = p->vNodes->pArray[i];
00429         assert( i == pNode->Num );
00430         pUnsigned = (unsigned *)vInfo->pArray[i];
00431         for ( k = 0; k < nRandom / 32; k++ )
00432             pUnsigned[k] = pNode->puSimR[k];
00433         for ( k = 0; k < nDynamic / 32; k++ )
00434             pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
00435     }
00436     return vInfo;
00437 }

void Fraig_ManPrintStats ( Fraig_Man_t *  p  ) 

Function*************************************************************

Synopsis [Deallocates the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file fraigMan.c.

00348 {
00349     double nMemory;
00350     int clk = clock();
00351     nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * 
00352         (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
00353     printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", 
00354         p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
00355     printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
00356         p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
00357     printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", 
00358         Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
00359     if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
00360     Fraig_PrintTime( "AIG simulation  ", p->timeSims  );
00361     Fraig_PrintTime( "AIG traversal   ", p->timeTrav  );
00362     Fraig_PrintTime( "Solver feedback ", p->timeFeed  );
00363     Fraig_PrintTime( "SAT solving     ", p->timeSat   );
00364     Fraig_PrintTime( "Network update  ", p->timeToNet );
00365     Fraig_PrintTime( "TOTAL RUNTIME   ", p->timeTotal );
00366     if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); }
00367     if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); }
00368     if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); }
00369     if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
00370 //    PRT( "Selection ", timeSelect );
00371 //    PRT( "Assignment", timeAssign );
00372 }

void Fraig_ParamsSetDefault ( Fraig_Params_t *  pParams  ) 

Function*************************************************************

Synopsis [Sets the default parameters of the package.]

Description [This set of parameters is tuned for equivalence checking.]

SideEffects []

SeeAlso []

Definition at line 119 of file fraigMan.c.

00120 {
00121     memset( pParams, 0, sizeof(Fraig_Params_t) );
00122     pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
00123     pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
00124     pParams->nBTLimit   = 99;                     // the max number of backtracks to perform
00125     pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
00126     pParams->fFuncRed   =  1;                     // performs only one level hashing
00127     pParams->fFeedBack  =  1;                     // enables solver feedback
00128     pParams->fDist1Pats =  1;                     // enables distance-1 patterns
00129     pParams->fDoSparse  =  0;                     // performs equiv tests for sparse functions 
00130     pParams->fChoicing  =  0;                     // enables recording structural choices
00131     pParams->fTryProve  =  1;                     // tries to solve the final miter
00132     pParams->fVerbose   =  0;                     // the verbosiness flag
00133     pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
00134     pParams->fInternal  =  0;                     // the flag indicates the internal run 
00135     pParams->nConfLimit =  0;                     // the limit on the number of conflicts
00136     pParams->nInspLimit =  0;                     // the limit on the number of inspections
00137 }

void Fraig_ParamsSetDefaultFull ( Fraig_Params_t *  pParams  ) 

Function*************************************************************

Synopsis [Sets the default parameters of the package.]

Description [This set of parameters is tuned for complete FRAIGing.]

SideEffects []

SeeAlso []

Definition at line 150 of file fraigMan.c.

00151 {
00152     memset( pParams, 0, sizeof(Fraig_Params_t) );
00153     pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
00154     pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
00155     pParams->nBTLimit   = -1;                     // the max number of backtracks to perform
00156     pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
00157     pParams->fFuncRed   =  1;                     // performs only one level hashing
00158     pParams->fFeedBack  =  1;                     // enables solver feedback
00159     pParams->fDist1Pats =  1;                     // enables distance-1 patterns
00160     pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
00161     pParams->fChoicing  =  0;                     // enables recording structural choices
00162     pParams->fTryProve  =  0;                     // tries to solve the final miter
00163     pParams->fVerbose   =  0;                     // the verbosiness flag
00164     pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
00165     pParams->fInternal  =  0;                     // the flag indicates the internal run 
00166     pParams->nConfLimit =  0;                     // the limit on the number of conflicts
00167     pParams->nInspLimit =  0;                     // the limit on the number of inspections
00168 }

Fraig_NodeVec_t* Fraig_UtilInfoAlloc ( int  nSize,
int  nWords,
bool  fClean 
)

Function*************************************************************

Synopsis [Allocates simulation information for all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 385 of file fraigMan.c.

00386 {
00387     Fraig_NodeVec_t * vInfo;
00388     unsigned * pUnsigned;
00389     int i;
00390     assert( nSize > 0 && nWords > 0 );
00391     vInfo = Fraig_NodeVecAlloc( nSize );
00392     pUnsigned = ALLOC( unsigned, nSize * nWords );
00393     vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
00394     if ( fClean )
00395         memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
00396     for ( i = 1; i < nSize; i++ )
00397         vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
00398     vInfo->nSize = nSize;
00399     return vInfo;
00400 }

void Prove_ParamsPrint ( Prove_Params_t *  pParams  ) 

Function*************************************************************

Synopsis [Prints out the current values of CEC engine parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file fraigMan.c.

00087 {
00088     printf( "CEC enging parameters:\n" );
00089     printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
00090     printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
00091     printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
00092     printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
00093     printf( "Solver iterations: %d\n", pParams->nItersMax );
00094     printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
00095     printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
00096     printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
00097     printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
00098     printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
00099     printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
00100     printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
00101     printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
00102     printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
00103     printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
00104     printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
00105     printf( "Parameter dump complete.\n" );
00106 }

void Prove_ParamsSetDefault ( Prove_Params_t *  pParams  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Sets the default parameters of the package.]

Description [This set of parameters is tuned for equivalence checking.]

SideEffects []

SeeAlso []

Definition at line 43 of file fraigMan.c.

00044 {
00045     // clean the parameter structure
00046     memset( pParams, 0, sizeof(Prove_Params_t) );
00047     // general parameters
00048     pParams->fUseFraiging         = 1;       // enables fraiging
00049     pParams->fUseRewriting        = 1;       // enables rewriting
00050     pParams->fUseBdds             = 0;       // enables BDD construction when other methods fail
00051     pParams->fVerbose             = 0;       // prints verbose stats
00052     // iterations
00053     pParams->nItersMax            = 6;       // the number of iterations
00054     // mitering 
00055     pParams->nMiteringLimitStart  = 300;    // starting mitering limit
00056     pParams->nMiteringLimitMulti  = 2.0;     // multiplicative coefficient to increase the limit in each iteration
00057     // rewriting (currently not used)
00058     pParams->nRewritingLimitStart = 3;       // the number of rewriting iterations
00059     pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
00060     // fraiging 
00061     pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
00062     pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
00063     // last-gasp BDD construction
00064     pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
00065     pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
00066     // last-gasp mitering
00067 //    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
00068     pParams->nMiteringLimitLast   = 0;       // final mitering limit
00069     // global SAT solver limits
00070     pParams->nTotalBacktrackLimit = 0;       // global limit on the number of backtracks
00071     pParams->nTotalInspectLimit   = 0;       // global limit on the number of clause inspects
00072 //    pParams->nTotalInspectLimit   = 100000000;  // global limit on the number of clause inspects
00073 }

Variable Documentation

int timeAssign

Definition at line 26 of file fraigMan.c.

int timeSelect

CFile****************************************************************

FileName [fraigMan.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Implementation of the FRAIG manager.]

Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id
fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp

] DECLARATIONS ///

Definition at line 25 of file fraigMan.c.

Generated on Tue Jan 5 12:19:38 2010 for abc70930 by  doxygen 1.6.1