src/sat/fraig/fraig.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  Fraig_ParamsStruct_t_
struct  Prove_ParamsStruct_t_

Defines

#define Fraig_IsComplement(p)   (((int)((unsigned long) (p) & 01)))
#define Fraig_Regular(p)   ((Fraig_Node_t *)((unsigned long)(p) & ~01))
#define Fraig_Not(p)   ((Fraig_Node_t *)((unsigned long)(p) ^ 01))
#define Fraig_NotCond(p, c)   ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))
#define Fraig_Ref(p)
#define Fraig_Deref(p)
#define Fraig_RecursiveDeref(p, c)

Typedefs

typedef long long sint64
typedef struct Fraig_ManStruct_t_ Fraig_Man_t
typedef struct Fraig_NodeStruct_t_ Fraig_Node_t
typedef struct
Fraig_NodeVecStruct_t_ 		Fraig_NodeVec_t
typedef struct
Fraig_HashTableStruct_t_ 		Fraig_HashTable_t
typedef struct
Fraig_ParamsStruct_t_ 		Fraig_Params_t
typedef struct
Fraig_PatternsStruct_t_ 		Fraig_Patterns_t
typedef struct
Prove_ParamsStruct_t_ 		Prove_Params_t

Functions

Fraig_NodeVec_t * Fraig_ManReadVecInputs (Fraig_Man_t *p)
Fraig_NodeVec_t * Fraig_ManReadVecOutputs (Fraig_Man_t *p)
Fraig_NodeVec_t * Fraig_ManReadVecNodes (Fraig_Man_t *p)
Fraig_Node_t ** Fraig_ManReadInputs (Fraig_Man_t *p)
Fraig_Node_t ** Fraig_ManReadOutputs (Fraig_Man_t *p)
Fraig_Node_t ** Fraig_ManReadNodes (Fraig_Man_t *p)
int Fraig_ManReadInputNum (Fraig_Man_t *p)
int Fraig_ManReadOutputNum (Fraig_Man_t *p)
int Fraig_ManReadNodeNum (Fraig_Man_t *p)
Fraig_Node_t * Fraig_ManReadConst1 (Fraig_Man_t *p)
Fraig_Node_t * Fraig_ManReadIthVar (Fraig_Man_t *p, int i)
Fraig_Node_t * Fraig_ManReadIthNode (Fraig_Man_t *p, int i)
char ** Fraig_ManReadInputNames (Fraig_Man_t *p)
char ** Fraig_ManReadOutputNames (Fraig_Man_t *p)
char * Fraig_ManReadVarsInt (Fraig_Man_t *p)
char * Fraig_ManReadSat (Fraig_Man_t *p)
int Fraig_ManReadFuncRed (Fraig_Man_t *p)
int Fraig_ManReadFeedBack (Fraig_Man_t *p)
int Fraig_ManReadDoSparse (Fraig_Man_t *p)
int Fraig_ManReadChoicing (Fraig_Man_t *p)
int Fraig_ManReadVerbose (Fraig_Man_t *p)
int * Fraig_ManReadModel (Fraig_Man_t *p)
int Fraig_ManReadPatternNumRandom (Fraig_Man_t *p)
int Fraig_ManReadPatternNumDynamic (Fraig_Man_t *p)
int Fraig_ManReadPatternNumDynamicFiltered (Fraig_Man_t *p)
int Fraig_ManReadSatFails (Fraig_Man_t *p)
int Fraig_ManReadConflicts (Fraig_Man_t *p)
int Fraig_ManReadInspects (Fraig_Man_t *p)
void Fraig_ManSetFuncRed (Fraig_Man_t *p, int fFuncRed)
void Fraig_ManSetFeedBack (Fraig_Man_t *p, int fFeedBack)
void Fraig_ManSetDoSparse (Fraig_Man_t *p, int fDoSparse)
void Fraig_ManSetChoicing (Fraig_Man_t *p, int fChoicing)
void Fraig_ManSetTryProve (Fraig_Man_t *p, int fTryProve)
void Fraig_ManSetVerbose (Fraig_Man_t *p, int fVerbose)
void Fraig_ManSetTimeToGraph (Fraig_Man_t *p, int Time)
void Fraig_ManSetTimeToNet (Fraig_Man_t *p, int Time)
void Fraig_ManSetTimeTotal (Fraig_Man_t *p, int Time)
void Fraig_ManSetOutputNames (Fraig_Man_t *p, char **ppNames)
void Fraig_ManSetInputNames (Fraig_Man_t *p, char **ppNames)
void Fraig_ManSetPo (Fraig_Man_t *p, Fraig_Node_t *pNode)
Fraig_Node_t * Fraig_NodeReadData0 (Fraig_Node_t *p)
Fraig_Node_t * Fraig_NodeReadData1 (Fraig_Node_t *p)
int Fraig_NodeReadNum (Fraig_Node_t *p)
Fraig_Node_t * Fraig_NodeReadOne (Fraig_Node_t *p)
Fraig_Node_t * Fraig_NodeReadTwo (Fraig_Node_t *p)
Fraig_Node_t * Fraig_NodeReadNextE (Fraig_Node_t *p)
Fraig_Node_t * Fraig_NodeReadRepr (Fraig_Node_t *p)
int Fraig_NodeReadNumRefs (Fraig_Node_t *p)
int Fraig_NodeReadNumFanouts (Fraig_Node_t *p)
int Fraig_NodeReadSimInv (Fraig_Node_t *p)
int Fraig_NodeReadNumOnes (Fraig_Node_t *p)
unsigned * Fraig_NodeReadPatternsRandom (Fraig_Node_t *p)
unsigned * Fraig_NodeReadPatternsDynamic (Fraig_Node_t *p)
void Fraig_NodeSetData0 (Fraig_Node_t *p, Fraig_Node_t *pData)
void Fraig_NodeSetData1 (Fraig_Node_t *p, Fraig_Node_t *pData)
int Fraig_NodeIsConst (Fraig_Node_t *p)
int Fraig_NodeIsVar (Fraig_Node_t *p)
int Fraig_NodeIsAnd (Fraig_Node_t *p)
int Fraig_NodeComparePhase (Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t * Fraig_NodeOr (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t * Fraig_NodeAnd (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t * Fraig_NodeExor (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Fraig_Node_t * Fraig_NodeMux (Fraig_Man_t *p, Fraig_Node_t *pNode, Fraig_Node_t *pNodeT, Fraig_Node_t *pNodeE)
void Fraig_NodeSetChoice (Fraig_Man_t *pMan, Fraig_Node_t *pNodeOld, Fraig_Node_t *pNodeNew)
void Prove_ParamsSetDefault (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 *pMan)
void Fraig_ManPrintStats (Fraig_Man_t *p)
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)
Fraig_NodeVec_t * Fraig_Dfs (Fraig_Man_t *pMan, int fEquiv)
Fraig_NodeVec_t * Fraig_DfsOne (Fraig_Man_t *pMan, Fraig_Node_t *pNode, int fEquiv)
Fraig_NodeVec_t * Fraig_DfsNodes (Fraig_Man_t *pMan, Fraig_Node_t **ppNodes, int nNodes, int fEquiv)
Fraig_NodeVec_t * Fraig_DfsReverse (Fraig_Man_t *pMan)
int Fraig_CountNodes (Fraig_Man_t *pMan, int fEquiv)
int Fraig_CheckTfi (Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
int Fraig_CountLevels (Fraig_Man_t *pMan)
int Fraig_NodesAreEqual (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit, int nTimeLimit)
int Fraig_NodeIsEquivalent (Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit, int nTimeLimit)
void Fraig_ManProveMiter (Fraig_Man_t *p)
int Fraig_ManCheckMiter (Fraig_Man_t *p)
int Fraig_ManCheckClauseUsingSat (Fraig_Man_t *p, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2, int nBTLimit)
Fraig_NodeVec_t * Fraig_NodeVecAlloc (int nCap)
void Fraig_NodeVecFree (Fraig_NodeVec_t *p)
Fraig_NodeVec_t * Fraig_NodeVecDup (Fraig_NodeVec_t *p)
Fraig_Node_t ** Fraig_NodeVecReadArray (Fraig_NodeVec_t *p)
int Fraig_NodeVecReadSize (Fraig_NodeVec_t *p)
void Fraig_NodeVecGrow (Fraig_NodeVec_t *p, int nCapMin)
void Fraig_NodeVecShrink (Fraig_NodeVec_t *p, int nSizeNew)
void Fraig_NodeVecClear (Fraig_NodeVec_t *p)
void Fraig_NodeVecPush (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
int Fraig_NodeVecPushUnique (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
void Fraig_NodeVecPushOrder (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
int Fraig_NodeVecPushUniqueOrder (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
void Fraig_NodeVecPushOrderByLevel (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
int Fraig_NodeVecPushUniqueOrderByLevel (Fraig_NodeVec_t *p, Fraig_Node_t *pNode)
Fraig_Node_t * Fraig_NodeVecPop (Fraig_NodeVec_t *p)
void Fraig_NodeVecRemove (Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
void Fraig_NodeVecWriteEntry (Fraig_NodeVec_t *p, int i, Fraig_Node_t *Entry)
Fraig_Node_t * Fraig_NodeVecReadEntry (Fraig_NodeVec_t *p, int i)
void Fraig_NodeVecSortByLevel (Fraig_NodeVec_t *p, int fIncreasing)
void Fraig_NodeVecSortByNumber (Fraig_NodeVec_t *p)
void Fraig_ManMarkRealFanouts (Fraig_Man_t *p)
int Fraig_ManCheckConsistency (Fraig_Man_t *p)
int Fraig_GetMaxLevel (Fraig_Man_t *pMan)
void Fraig_ManReportChoices (Fraig_Man_t *pMan)
void Fraig_MappingSetChoiceLevels (Fraig_Man_t *pMan, int fMaximum)
Fraig_NodeVec_t * Fraig_CollectSupergate (Fraig_Node_t *pNode, int fStopAtMux)

Define Documentation

#define Fraig_Deref ( p   ) 

Definition at line 123 of file fraig.h.

#define Fraig_IsComplement ( p   )     (((int)((unsigned long) (p) & 01)))

GLOBAL VARIABLES /// MACRO DEFINITIONS ///

Definition at line 116 of file fraig.h.

#define Fraig_Not ( p   )     ((Fraig_Node_t *)((unsigned long)(p) ^ 01))

Definition at line 118 of file fraig.h.

#define Fraig_NotCond ( p,
c   )     ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))

Definition at line 119 of file fraig.h.

#define Fraig_RecursiveDeref ( p,
c   ) 

Definition at line 124 of file fraig.h.

#define Fraig_Ref ( p   ) 

Definition at line 122 of file fraig.h.

#define Fraig_Regular ( p   )     ((Fraig_Node_t *)((unsigned long)(p) & ~01))

Definition at line 117 of file fraig.h.

Typedef Documentation

typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t

Definition at line 52 of file fraig.h.

typedef struct Fraig_ManStruct_t_ Fraig_Man_t

PARAMETERS /// STRUCTURE DEFINITIONS ///

Definition at line 49 of file fraig.h.

typedef struct Fraig_NodeStruct_t_ Fraig_Node_t

Definition at line 50 of file fraig.h.

typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t

Definition at line 51 of file fraig.h.

typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t

Definition at line 53 of file fraig.h.

typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t

Definition at line 54 of file fraig.h.

typedef struct Prove_ParamsStruct_t_ Prove_Params_t

Definition at line 55 of file fraig.h.

typedef long long sint64

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

FileName [fraig.h]

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

Synopsis [External declarations of the FRAIG package.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraig.h,v 1.18 2005/07/08 01:01:30 alanmi Exp

] INCLUDES ///

Definition at line 36 of file fraig.h.

Function Documentation

int Fraig_CheckTfi ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew 
)

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

Synopsis [Returns 1 if pOld is in the TFI of pNew.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file fraigUtil.c.

00171 {
00172     assert( !Fraig_IsComplement(pOld) );
00173     assert( !Fraig_IsComplement(pNew) );
00174     pMan->nTravIds++;
00175     return Fraig_CheckTfi_rec( pMan, pNew, pOld );
00176 }

Fraig_NodeVec_t* Fraig_CollectSupergate ( Fraig_Node_t *  pNode,
int  fStopAtMux 
)

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

Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 957 of file fraigUtil.c.

00958 {
00959     Fraig_NodeVec_t * vSuper;
00960     vSuper = Fraig_NodeVecAlloc( 8 );
00961     Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
00962     return vSuper;
00963 }

int Fraig_CountLevels ( Fraig_Man_t *  pMan  ) 
int Fraig_CountNodes ( Fraig_Man_t *  pMan,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 149 of file fraigUtil.c.

00150 {
00151     Fraig_NodeVec_t * vNodes;
00152     int RetValue;
00153     vNodes = Fraig_Dfs( pMan, fEquiv );
00154     RetValue = vNodes->nSize;
00155     Fraig_NodeVecFree( vNodes );
00156     return RetValue;
00157 }

Fraig_NodeVec_t* Fraig_Dfs ( Fraig_Man_t *  pMan,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 55 of file fraigUtil.c.

00056 {
00057     Fraig_NodeVec_t * vNodes;
00058     int i;
00059     pMan->nTravIds++;
00060     vNodes = Fraig_NodeVecAlloc( 100 );
00061     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00062         Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv );
00063     return vNodes;
00064 }

Fraig_NodeVec_t* Fraig_DfsNodes ( Fraig_Man_t *  pMan,
Fraig_Node_t **  ppNodes,
int  nNodes,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file fraigUtil.c.

00098 {
00099     Fraig_NodeVec_t * vNodes;
00100     int i;
00101     pMan->nTravIds++;
00102     vNodes = Fraig_NodeVecAlloc( 100 );
00103     for ( i = 0; i < nNodes; i++ )
00104         Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv );
00105     return vNodes;
00106 }

Fraig_NodeVec_t* Fraig_DfsOne ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNode,
int  fEquiv 
)

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

Synopsis [Computes the DFS ordering of the nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file fraigUtil.c.

00078 {
00079     Fraig_NodeVec_t * vNodes;
00080     pMan->nTravIds++;
00081     vNodes = Fraig_NodeVecAlloc( 100 );
00082     Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv );
00083     return vNodes;
00084 }

Fraig_NodeVec_t* Fraig_DfsReverse ( Fraig_Man_t *  pMan  ) 
int Fraig_GetMaxLevel ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Sets up the mask.]

Description []

SideEffects []

SeeAlso []

Definition at line 425 of file fraigUtil.c.

00426 {
00427     int nLevelMax, i;
00428     nLevelMax = 0;
00429     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00430         nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? 
00431                 nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level;
00432     return nLevelMax;
00433 }

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_ManCheckClauseUsingSat ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  nBTLimit 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 648 of file fraigSat.c.

00649 {
00650     Fraig_Node_t * pNode1R, * pNode2R;
00651     int RetValue, RetValue1, i, clk;
00652     int fVerbose = 0;
00653 
00654     pNode1R = Fraig_Regular(pNode1);
00655     pNode2R = Fraig_Regular(pNode2);
00656     assert( pNode1R != pNode2R );
00657 
00658     // make sure the solver is allocated and has enough variables
00659     if ( p->pSat == NULL )
00660         Fraig_ManCreateSolver( p );
00661     // make sure the SAT solver has enough variables
00662     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00663         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00664 
00665    // get the logic cone
00666 clk = clock();
00667     Fraig_OrderVariables( p, pNode1R, pNode2R );
00668 //    Fraig_PrepareCones( p, pNode1R, pNode2R );
00669 p->timeTrav += clock() - clk;
00670 
00672     // prepare the solver to run incrementally on these variables
00673 //clk = clock();
00674     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00675 //p->time3 += clock() - clk;
00676 
00677     // solve under assumptions
00678     // A = 1; B = 0     OR     A = 1; B = 1 
00679     Msat_IntVecClear( p->vProj );
00680     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
00681     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
00682     // run the solver
00683 clk = clock();
00684     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
00685 p->timeSat += clock() - clk;
00686 
00687     if ( RetValue1 == MSAT_FALSE )
00688     {
00689 //p->time1 += clock() - clk;
00690 
00691 if ( fVerbose )
00692 {
00693     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00694 PRT( "time", clock() - clk );
00695 }
00696 
00697         // add the clause
00698         Msat_IntVecClear( p->vProj );
00699         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
00700         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
00701         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00702         assert( RetValue );
00703 //        p->nSatProofImp++;
00704         return 1;
00705     }
00706     else if ( RetValue1 == MSAT_TRUE )
00707     {
00708 //p->time2 += clock() - clk;
00709 
00710 if ( fVerbose )
00711 {
00712     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00713 PRT( "time", clock() - clk );
00714 }
00715         // record the counter example
00716 //        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
00717         p->nSatCounterImp++;
00718         return 0;
00719     }
00720     else // if ( RetValue1 == MSAT_UNKNOWN )
00721     {
00722 p->time3 += clock() - clk;
00723         p->nSatFailsImp++;
00724         return 0;
00725     }
00726 }

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 }

int Fraig_ManCheckConsistency ( Fraig_Man_t *  p  ) 

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

Synopsis [Verify one useful property.]

Description [This procedure verifies one useful property. After the FRAIG construction with choice nodes is over, each primary node should have fanins that are primary nodes. The primary nodes is the one that does not have pNode->pRepr set to point to another node.]

SideEffects []

SeeAlso []

Definition at line 309 of file fraigUtil.c.

00310 {
00311     Fraig_Node_t * pNode;
00312     Fraig_NodeVec_t * pVec;
00313     int i;
00314     pVec = Fraig_Dfs( p, 0 );
00315     for ( i = 0; i < pVec->nSize; i++ )
00316     {
00317         pNode = pVec->pArray[i];
00318         if ( Fraig_NodeIsVar(pNode) )
00319         {
00320             if ( pNode->pRepr )
00321                 printf( "Primary input %d is a secondary node.\n", pNode->Num );
00322         }
00323         else if ( Fraig_NodeIsConst(pNode) )
00324         {
00325             if ( pNode->pRepr )
00326                 printf( "Constant 1 %d is a secondary node.\n", pNode->Num );
00327         }
00328         else
00329         {
00330             if ( pNode->pRepr )
00331                 printf( "Internal node %d is a secondary node.\n", pNode->Num );
00332             if ( Fraig_Regular(pNode->p1)->pRepr )
00333                 printf( "Internal node %d has first fanin %d that is a secondary node.\n", 
00334                     pNode->Num, Fraig_Regular(pNode->p1)->Num );
00335             if ( Fraig_Regular(pNode->p2)->pRepr )
00336                 printf( "Internal node %d has second fanin %d that is a secondary node.\n", 
00337                     pNode->Num, Fraig_Regular(pNode->p2)->Num );
00338         }
00339     }
00340     Fraig_NodeVecFree( pVec );
00341     return 1;
00342 }

int Fraig_ManCheckMiter ( Fraig_Man_t *  p  ) 

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

Synopsis [Returns 1 if the miter is unsat; 0 if sat; -1 if undecided.]

Description []

SideEffects []

SeeAlso []

Definition at line 127 of file fraigSat.c.

00128 {
00129     Fraig_Node_t * pNode;
00130     int i;
00131     FREE( p->pModel );
00132     for ( i = 0; i < p->vOutputs->nSize; i++ )
00133     {
00134         // get the output node (it can be complemented!)
00135         pNode = p->vOutputs->pArray[i];
00136         // if the miter is constant 0, the problem is UNSAT
00137         if ( pNode == Fraig_Not(p->pConst1) )
00138             continue;
00139         // consider the special case when the miter is constant 1
00140         if ( pNode == p->pConst1 )
00141         {
00142             // in this case, any counter example will do to distinquish it from constant 0
00143             // here we pick the counter example composed of all zeros
00144             p->pModel = Fraig_ManAllocCounterExample( p );
00145             return 0;
00146         }
00147         // save the counter example
00148         p->pModel = Fraig_ManSaveCounterExample( p, pNode );
00149         // if the model is not found, return undecided
00150         if ( p->pModel == NULL )
00151             return -1;
00152         else
00153             return 0;
00154     }
00155     return 1;
00156 }

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_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_ManMarkRealFanouts ( Fraig_Man_t *  p  ) 

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

Synopsis [Sets the number of fanouts (none, one, or many).]

Description [This procedure collects the nodes reachable from the POs of the AIG and sets the type of fanout counter (none, one, or many) for each node. This procedure is useful to determine fanout-free cones of AND-nodes, which is helpful for rebalancing the AIG (see procedure Fraig_ManRebalance, or something like that).]

SideEffects []

SeeAlso []

Definition at line 248 of file fraigUtil.c.

00249 {
00250     Fraig_NodeVec_t * vNodes;
00251     Fraig_Node_t * pNodeR;
00252     int i;
00253     // collect the nodes reachable
00254     vNodes = Fraig_Dfs( p, 0 );
00255     // clean the fanouts field
00256     for ( i = 0; i < vNodes->nSize; i++ )
00257     {
00258         vNodes->pArray[i]->nFanouts = 0;
00259         vNodes->pArray[i]->pData0 = NULL;
00260     }
00261     // mark reachable nodes by setting the two-bit counter pNode->nFans
00262     for ( i = 0; i < vNodes->nSize; i++ )
00263     {
00264         pNodeR = Fraig_Regular(vNodes->pArray[i]->p1);
00265         if ( pNodeR && ++pNodeR->nFanouts == 3 )
00266             pNodeR->nFanouts = 2;
00267         pNodeR = Fraig_Regular(vNodes->pArray[i]->p2);
00268         if ( pNodeR && ++pNodeR->nFanouts == 3 )
00269             pNodeR->nFanouts = 2;
00270     }
00271     Fraig_NodeVecFree( vNodes );
00272 }

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_ManProveMiter ( Fraig_Man_t *  p  ) 

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

Synopsis [Tries to prove the final miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file fraigSat.c.

00084 {
00085     Fraig_Node_t * pNode;
00086     int i, clk;
00087 
00088     if ( !p->fTryProve )
00089         return;
00090  
00091     clk = clock();
00092     // consider all outputs of the multi-output miter
00093     for ( i = 0; i < p->vOutputs->nSize; i++ )
00094     {
00095         pNode = Fraig_Regular(p->vOutputs->pArray[i]);
00096         // skip already constant nodes
00097         if ( pNode == p->pConst1 )
00098             continue;
00099         // skip nodes that are different according to simulation
00100         if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
00101             continue;
00102         if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
00103         {
00104             if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
00105                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
00106             else
00107                 p->vOutputs->pArray[i] = p->pConst1;
00108         }
00109     }
00110     if ( p->fVerboseP ) 
00111     {
00112 //        PRT( "Final miter proof time", clock() - clk );
00113     }
00114 }

int Fraig_ManReadChoicing ( Fraig_Man_t *  p  ) 

Definition at line 58 of file fraigApi.c.

00058 { return p->fChoicing;  }

int Fraig_ManReadConflicts ( Fraig_Man_t *  p  ) 

Definition at line 70 of file fraigApi.c.

00070 { return p->pSat? Msat_SolverReadBackTracks(p->pSat) : 0; }

Fraig_Node_t* Fraig_ManReadConst1 ( Fraig_Man_t *  p  ) 

Definition at line 49 of file fraigApi.c.

00049 { return p->pConst1;            }

int Fraig_ManReadDoSparse ( Fraig_Man_t *  p  ) 

Definition at line 57 of file fraigApi.c.

00057 { return p->fDoSparse;  }

int Fraig_ManReadFeedBack ( Fraig_Man_t *  p  ) 

Definition at line 56 of file fraigApi.c.

00056 { return p->fFeedBack;  }

int Fraig_ManReadFuncRed ( Fraig_Man_t *  p  ) 

Definition at line 55 of file fraigApi.c.

00055 { return p->fFuncRed;   }

char** Fraig_ManReadInputNames ( Fraig_Man_t *  p  ) 

Definition at line 51 of file fraigApi.c.

00051 { return p->ppInputNames;       }

int Fraig_ManReadInputNum ( Fraig_Man_t *  p  ) 

Definition at line 46 of file fraigApi.c.

00046 { return p->vInputs->nSize;     }

Fraig_Node_t** Fraig_ManReadInputs ( Fraig_Man_t *  p  ) 

Definition at line 43 of file fraigApi.c.

00043 { return p->vInputs->pArray;    }

int Fraig_ManReadInspects ( Fraig_Man_t *  p  ) 

Definition at line 72 of file fraigApi.c.

00072 { return p->pSat? Msat_SolverReadInspects(p->pSat) : 0;   }

Fraig_Node_t* Fraig_ManReadIthNode ( Fraig_Man_t *  p,
int  i 
)

Definition at line 50 of file fraigApi.c.

00050 { assert ( i < p->vNodes->nSize  ); return p->vNodes->pArray[i];  }

Fraig_Node_t* Fraig_ManReadIthVar ( Fraig_Man_t *  p,
int  i 
)

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

Synopsis [Returns a new primary input node.]

Description [If the node with this number does not exist, create a new PI node with this number.]

SideEffects []

SeeAlso []

Definition at line 168 of file fraigApi.c.

00169 {
00170     int k;
00171     if ( i < 0 )
00172     {
00173         printf( "Requesting a PI with a negative number\n" );
00174         return NULL;
00175     }
00176     // create the PIs to fill in the interval
00177     if ( i >= p->vInputs->nSize )
00178         for ( k = p->vInputs->nSize; k <= i; k++ )
00179             Fraig_NodeCreatePi( p ); 
00180     return p->vInputs->pArray[i];
00181 }

int* Fraig_ManReadModel ( Fraig_Man_t *  p  ) 

Definition at line 60 of file fraigApi.c.

00060 { return p->pModel;     }

int Fraig_ManReadNodeNum ( Fraig_Man_t *  p  ) 

Definition at line 48 of file fraigApi.c.

00048 { return p->vNodes->nSize;      }

Fraig_Node_t** Fraig_ManReadNodes ( Fraig_Man_t *  p  ) 

Definition at line 45 of file fraigApi.c.

00045 { return p->vNodes->pArray;     }

char** Fraig_ManReadOutputNames ( Fraig_Man_t *  p  ) 

Definition at line 52 of file fraigApi.c.

00052 { return p->ppOutputNames;      }

int Fraig_ManReadOutputNum ( Fraig_Man_t *  p  ) 

Definition at line 47 of file fraigApi.c.

00047 { return p->vOutputs->nSize;    }

Fraig_Node_t** Fraig_ManReadOutputs ( Fraig_Man_t *  p  ) 

Definition at line 44 of file fraigApi.c.

00044 { return p->vOutputs->pArray;   }

int Fraig_ManReadPatternNumDynamic ( Fraig_Man_t *  p  ) 

Definition at line 64 of file fraigApi.c.

00064 { return p->iWordStart * 32;  }

int Fraig_ManReadPatternNumDynamicFiltered ( Fraig_Man_t *  p  ) 

Definition at line 66 of file fraigApi.c.

00066 { return p->iPatsPerm;        }

int Fraig_ManReadPatternNumRandom ( Fraig_Man_t *  p  ) 

Definition at line 62 of file fraigApi.c.

00062 { return p->nWordsRand * 32;  }

char* Fraig_ManReadSat ( Fraig_Man_t *  p  ) 

Definition at line 54 of file fraigApi.c.

00054 { return (char *)p->pSat;       }

int Fraig_ManReadSatFails ( Fraig_Man_t *  p  ) 

Definition at line 68 of file fraigApi.c.

00068 { return p->nSatFailsReal;    }

char* Fraig_ManReadVarsInt ( Fraig_Man_t *  p  ) 

Definition at line 53 of file fraigApi.c.

00053 { return (char *)p->vVarsInt;   }

Fraig_NodeVec_t* Fraig_ManReadVecInputs ( Fraig_Man_t *  p  ) 

FUNCTION DEFINITIONS ///

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

FileName [fraigApi.c]

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

Synopsis [Access APIs for the FRAIG manager and node.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigApi.c,v 1.2 2005/07/08 01:01:30 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Access functions to read the data members of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 40 of file fraigApi.c.

00040 { return p->vInputs;            }

Fraig_NodeVec_t* Fraig_ManReadVecNodes ( Fraig_Man_t *  p  ) 

Definition at line 42 of file fraigApi.c.

00042 { return p->vNodes;             }

Fraig_NodeVec_t* Fraig_ManReadVecOutputs ( Fraig_Man_t *  p  ) 

Definition at line 41 of file fraigApi.c.

00041 { return p->vOutputs;           }

int Fraig_ManReadVerbose ( Fraig_Man_t *  p  ) 

Definition at line 59 of file fraigApi.c.

00059 { return p->fVerbose;   }

void Fraig_ManReportChoices ( Fraig_Man_t *  pMan  ) 

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

Synopsis [Reports statistics on choice nodes.]

Description [The number of choice nodes is the number of primary nodes, which has pNextE set to a pointer. The number of choices is the number of entries in the equivalent-node lists of the primary nodes.]

SideEffects []

SeeAlso []

Definition at line 517 of file fraigUtil.c.

00518 {
00519     Fraig_Node_t * pNode, * pTemp;
00520     int nChoiceNodes, nChoices;
00521     int i, LevelMax1, LevelMax2;
00522 
00523     // report the number of levels
00524     LevelMax1 = Fraig_GetMaxLevel( pMan );
00525     Fraig_MappingSetChoiceLevels( pMan, 0 );
00526     LevelMax2 = Fraig_GetMaxLevel( pMan );
00527 
00528     // report statistics about choices
00529     nChoiceNodes = nChoices = 0;
00530     for ( i = 0; i < pMan->vNodes->nSize; i++ )
00531     {
00532         pNode = pMan->vNodes->pArray[i];
00533         if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
00534         { // this is a choice node = the primary node that has equivalent nodes
00535             nChoiceNodes++;
00536             for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
00537                 nChoices++;
00538         }
00539     }
00540     printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
00541     printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
00542 }

void Fraig_ManSetChoicing ( Fraig_Man_t *  p,
int  fChoicing 
)

Definition at line 88 of file fraigApi.c.

00088 { p->fChoicing = fChoicing; }

void Fraig_ManSetDoSparse ( Fraig_Man_t *  p,
int  fDoSparse 
)

Definition at line 87 of file fraigApi.c.

00087 { p->fDoSparse = fDoSparse; }

void Fraig_ManSetFeedBack ( Fraig_Man_t *  p,
int  fFeedBack 
)

Definition at line 86 of file fraigApi.c.

00086 { p->fFeedBack = fFeedBack; }

void Fraig_ManSetFuncRed ( Fraig_Man_t *  p,
int  fFuncRed 
)

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

Synopsis [Access functions to set the data members of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file fraigApi.c.

00085 { p->fFuncRed  = fFuncRed;  }

void Fraig_ManSetInputNames ( Fraig_Man_t *  p,
char **  ppNames 
)

Definition at line 95 of file fraigApi.c.

00095 { p->ppInputNames  = ppNames; }

void Fraig_ManSetOutputNames ( Fraig_Man_t *  p,
char **  ppNames 
)

Definition at line 94 of file fraigApi.c.

00094 { p->ppOutputNames = ppNames; }

void Fraig_ManSetPo ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Creates a new PO node.]

Description [This procedure may take a complemented node.]

SideEffects []

SeeAlso []

Definition at line 194 of file fraigApi.c.

00195 {
00196     // internal node may be a PO two times
00197     Fraig_Regular(pNode)->fNodePo = 1;
00198     Fraig_NodeVecPush( p->vOutputs, pNode );
00199 }

void Fraig_ManSetTimeToGraph ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 91 of file fraigApi.c.

00091 { p->timeToAig = Time;      }

void Fraig_ManSetTimeToNet ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 92 of file fraigApi.c.

00092 { p->timeToNet = Time;      }

void Fraig_ManSetTimeTotal ( Fraig_Man_t *  p,
int  Time 
)

Definition at line 93 of file fraigApi.c.

00093 { p->timeTotal = Time;      }

void Fraig_ManSetTryProve ( Fraig_Man_t *  p,
int  fTryProve 
)

Definition at line 89 of file fraigApi.c.

00089 { p->fTryProve = fTryProve; }

void Fraig_ManSetVerbose ( Fraig_Man_t *  p,
int  fVerbose 
)

Definition at line 90 of file fraigApi.c.

00090 { p->fVerbose  = fVerbose;  }

void Fraig_MappingSetChoiceLevels ( Fraig_Man_t *  pMan,
int  fMaximum 
)

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

Synopsis [Resets the levels of the nodes in the choice graph.]

Description [Makes the level of the choice nodes to be equal to the maximum of the level of the nodes in the equivalence class. This way sorting by level leads to the reverse topological order, which is needed for the required time computation.]

SideEffects []

SeeAlso []

Definition at line 496 of file fraigUtil.c.

00497 {
00498     int i;
00499     pMan->nTravIds++;
00500     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
00501         Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum );
00502 }

Fraig_Node_t* Fraig_NodeAnd ( Fraig_Man_t *  p,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

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

Synopsis [Perfoms the AND operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file fraigApi.c.

00213 {
00214     return Fraig_NodeAndCanon( p, p1, p2 );
00215 }

int Fraig_NodeComparePhase ( Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

Definition at line 154 of file fraigApi.c.

00154 { assert( !Fraig_IsComplement(p1) ); assert( !Fraig_IsComplement(p2) ); return p1->fInv ^ p2->fInv; }

Fraig_Node_t* Fraig_NodeExor ( Fraig_Man_t *  p,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

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

Synopsis [Perfoms the EXOR operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file fraigApi.c.

00245 {
00246     return Fraig_NodeMux( p, p1, Fraig_Not(p2), p2 );
00247 }

int Fraig_NodeIsAnd ( Fraig_Node_t *  p  ) 

Definition at line 153 of file fraigApi.c.

00153 {  return (Fraig_Regular(p))->NumPi <  0 && (Fraig_Regular(p))->Num > 0;  }

int Fraig_NodeIsConst ( Fraig_Node_t *  p  ) 

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

Synopsis [Checks the type of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file fraigApi.c.

00151 {  return (Fraig_Regular(p))->Num   == 0;  }

int Fraig_NodeIsEquivalent ( Fraig_Man_t *  p,
Fraig_Node_t *  pOld,
Fraig_Node_t *  pNew,
int  nBTLimit,
int  nTimeLimit 
)

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

Synopsis [Checks whether two nodes are functinally equivalent.]

Description [The flag (fComp) tells whether the nodes to be checked are in the opposite polarity. The second flag (fSkipZeros) tells whether the checking should be performed if the simulation vectors are zeros. Returns 1 if the nodes are equivalent; 0 othewise.]

SideEffects []

SeeAlso []

Definition at line 299 of file fraigSat.c.

00300 {
00301     int RetValue, RetValue1, i, fComp, clk;
00302     int fVerbose = 0;
00303     int fSwitch = 0;
00304 
00305     // make sure the nodes are not complemented
00306     assert( !Fraig_IsComplement(pNew) );
00307     assert( !Fraig_IsComplement(pOld) );
00308     assert( pNew != pOld );
00309 
00310     // if at least one of the nodes is a failed node, perform adjustments:
00311     // if the backtrack limit is small, simply skip this node
00312     // if the backtrack limit is > 10, take the quare root of the limit
00313     if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
00314     {
00315         p->nSatFails++;
00316 //            return 0;
00317 //        if ( nBTLimit > 10 )
00318 //            nBTLimit /= 10;
00319         if ( nBTLimit <= 10 )
00320             return 0;
00321         nBTLimit = (int)sqrt(nBTLimit);
00322 //        fSwitch = 1;
00323     }
00324 
00325     p->nSatCalls++;
00326 
00327     // make sure the solver is allocated and has enough variables
00328     if ( p->pSat == NULL )
00329         Fraig_ManCreateSolver( p );
00330     // make sure the SAT solver has enough variables
00331     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
00332         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
00333 
00334 
00335  
00336 /*
00337     {
00338         Fraig_Node_t * ppNodes[2] = { pOld, pNew };
00339         extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
00340         Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
00341     }
00342 */
00343 
00344     nMuxes = 0;
00345 
00346 
00347     // get the logic cone
00348 clk = clock();
00349 //    Fraig_VarsStudy( p, pOld, pNew );
00350     Fraig_OrderVariables( p, pOld, pNew );
00351 //    Fraig_PrepareCones( p, pOld, pNew );
00352 p->timeTrav += clock() - clk;
00353 
00354 //    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
00355 //    PRT( "Time", clock() - clk );
00356 
00357 if ( fVerbose )
00358     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
00359 
00360 
00361     // prepare variable activity
00362     Fraig_SetActivity( p, pOld, pNew );
00363 
00364     // get the complemented attribute
00365     fComp = Fraig_NodeComparePhase( pOld, pNew );
00366 //Msat_SolverPrintClauses( p->pSat );
00367 
00369     // prepare the solver to run incrementally on these variables
00370 //clk = clock();
00371     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00372 //p->time3 += clock() - clk;
00373 
00374 
00375     // solve under assumptions
00376     // A = 1; B = 0     OR     A = 1; B = 1 
00377     Msat_IntVecClear( p->vProj );
00378     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00379     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00380 
00381 //Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
00382 
00383     // run the solver
00384 clk = clock();
00385     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
00386 p->timeSat += clock() - clk;
00387 
00388     if ( RetValue1 == MSAT_FALSE )
00389     {
00390 //p->time1 += clock() - clk;
00391 
00392 if ( fVerbose )
00393 {
00394     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00395 PRT( "time", clock() - clk );
00396 }
00397 
00398         // add the clause
00399         Msat_IntVecClear( p->vProj );
00400         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00401         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00402         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00403         assert( RetValue );
00404         // continue solving the other implication
00405     }
00406     else if ( RetValue1 == MSAT_TRUE )
00407     {
00408 //p->time2 += clock() - clk;
00409 
00410 if ( fVerbose )
00411 {
00412     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00413 PRT( "time", clock() - clk );
00414 }
00415 
00416         // record the counter example
00417         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00418 
00419 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00420 //            printf( "*" );
00421 //        printf( "s(%d)", pNew->Level );
00422         if ( fSwitch )
00423              printf( "s(%d)", pNew->Level );
00424         p->nSatCounter++;
00425         return 0;
00426     }
00427     else // if ( RetValue1 == MSAT_UNKNOWN )
00428     {
00429 p->time3 += clock() - clk;
00430 
00431 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00432 //            printf( "*" );
00433 //        printf( "T(%d)", pNew->Level );
00434 
00435         // mark the node as the failed node
00436         if ( pOld != p->pConst1 ) 
00437             pOld->fFailTfo = 1;
00438         pNew->fFailTfo = 1;
00439 //        p->nSatFails++;
00440         if ( fSwitch )
00441              printf( "T(%d)", pNew->Level );
00442         p->nSatFailsReal++;
00443         return 0;
00444     }
00445 
00446     // if the old node was constant 0, we already know the answer
00447     if ( pOld == p->pConst1 )
00448         return 1;
00449 
00451     // prepare the solver to run incrementally 
00452 //clk = clock();
00453     Msat_SolverPrepare( p->pSat, p->vVarsInt );
00454 //p->time3 += clock() - clk;
00455     // solve under assumptions
00456     // A = 0; B = 1     OR     A = 0; B = 0 
00457     Msat_IntVecClear( p->vProj );
00458     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
00459     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
00460     // run the solver
00461 clk = clock();
00462     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
00463 p->timeSat += clock() - clk;
00464 
00465     if ( RetValue1 == MSAT_FALSE )
00466     {
00467 //p->time1 += clock() - clk;
00468 
00469 if ( fVerbose )
00470 {
00471     printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00472 PRT( "time", clock() - clk );
00473 }
00474 
00475         // add the clause
00476         Msat_IntVecClear( p->vProj );
00477         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
00478         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
00479         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
00480         assert( RetValue );
00481         // continue solving the other implication
00482     }
00483     else if ( RetValue1 == MSAT_TRUE )
00484     {
00485 //p->time2 += clock() - clk;
00486 
00487 if ( fVerbose )
00488 {
00489     printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
00490 PRT( "time", clock() - clk );
00491 }
00492 
00493         // record the counter example
00494         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
00495         p->nSatCounter++;
00496 
00497 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00498 //            printf( "*" );
00499 //        printf( "s(%d)", pNew->Level );
00500         if ( fSwitch )
00501              printf( "s(%d)", pNew->Level );
00502         return 0;
00503     }
00504     else // if ( RetValue1 == MSAT_UNKNOWN )
00505     {
00506 p->time3 += clock() - clk;
00507 
00508 //        if ( pOld->fFailTfo || pNew->fFailTfo )
00509 //            printf( "*" );
00510 //        printf( "T(%d)", pNew->Level );
00511         if ( fSwitch )
00512              printf( "T(%d)", pNew->Level );
00513 
00514         // mark the node as the failed node
00515         pOld->fFailTfo = 1;
00516         pNew->fFailTfo = 1;
00517 //        p->nSatFails++;
00518         p->nSatFailsReal++;
00519         return 0;
00520     }
00521 
00522     // return SAT proof
00523     p->nSatProof++;
00524 
00525 //    if ( pOld->fFailTfo || pNew->fFailTfo )
00526 //        printf( "*" );
00527 //    printf( "u(%d)", pNew->Level );
00528 
00529     if ( fSwitch )
00530          printf( "u(%d)", pNew->Level );
00531 
00532     return 1;
00533 }

int Fraig_NodeIsVar ( Fraig_Node_t *  p  ) 

Definition at line 152 of file fraigApi.c.

00152 {  return (Fraig_Regular(p))->NumPi >= 0;  }

Fraig_Node_t* Fraig_NodeMux ( Fraig_Man_t *  p,
Fraig_Node_t *  pC,
Fraig_Node_t *  pT,
Fraig_Node_t *  pE 
)

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

Synopsis [Perfoms the MUX operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file fraigApi.c.

00261 {
00262     Fraig_Node_t * pAnd1, * pAnd2, * pRes;
00263     pAnd1 = Fraig_NodeAndCanon( p, pC,          pT );     Fraig_Ref( pAnd1 );
00264     pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE );   Fraig_Ref( pAnd2 );
00265     pRes  = Fraig_NodeOr( p, pAnd1, pAnd2 ); 
00266     Fraig_RecursiveDeref( p, pAnd1 );
00267     Fraig_RecursiveDeref( p, pAnd2 );
00268     Fraig_Deref( pRes );
00269     return pRes;
00270 }

Fraig_Node_t * Fraig_NodeOr ( Fraig_Man_t *  p,
Fraig_Node_t *  p1,
Fraig_Node_t *  p2 
)

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

Synopsis [Perfoms the OR operation with functional hashing.]

Description []

SideEffects []

SeeAlso []

Definition at line 228 of file fraigApi.c.

00229 {
00230     return Fraig_Not( Fraig_NodeAndCanon( p, Fraig_Not(p1), Fraig_Not(p2) ) );
00231 }

Fraig_Node_t* Fraig_NodeReadData0 ( Fraig_Node_t *  p  ) 

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

Synopsis [Access functions to read the data members of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file fraigApi.c.

00108 { return p->pData0;    }

Fraig_Node_t* Fraig_NodeReadData1 ( Fraig_Node_t *  p  ) 

Definition at line 109 of file fraigApi.c.

00109 { return p->pData1;    }

Fraig_Node_t* Fraig_NodeReadNextE ( Fraig_Node_t *  p  ) 

Definition at line 113 of file fraigApi.c.

00113 { return p->pNextE;    }

int Fraig_NodeReadNum ( Fraig_Node_t *  p  ) 

Definition at line 110 of file fraigApi.c.

00110 { return p->Num;       }

int Fraig_NodeReadNumFanouts ( Fraig_Node_t *  p  ) 

Definition at line 116 of file fraigApi.c.

00116 { return p->nFanouts;  }

int Fraig_NodeReadNumOnes ( Fraig_Node_t *  p  ) 

Definition at line 118 of file fraigApi.c.

00118 { return p->nOnes;     }

int Fraig_NodeReadNumRefs ( Fraig_Node_t *  p  ) 

Definition at line 115 of file fraigApi.c.

00115 { return p->nRefs;     }

Fraig_Node_t* Fraig_NodeReadOne ( Fraig_Node_t *  p  ) 

Definition at line 111 of file fraigApi.c.

00111 { assert (!Fraig_IsComplement(p)); return p->p1; }

unsigned* Fraig_NodeReadPatternsDynamic ( Fraig_Node_t *  p  ) 

Definition at line 124 of file fraigApi.c.

00124 { return p->puSimD;    }

unsigned* Fraig_NodeReadPatternsRandom ( Fraig_Node_t *  p  ) 

Definition at line 121 of file fraigApi.c.

00121 { return p->puSimR;    }

Fraig_Node_t* Fraig_NodeReadRepr ( Fraig_Node_t *  p  ) 

Definition at line 114 of file fraigApi.c.

00114 { return p->pRepr;     }

int Fraig_NodeReadSimInv ( Fraig_Node_t *  p  ) 

Definition at line 117 of file fraigApi.c.

00117 { return p->fInv;      }

Fraig_Node_t* Fraig_NodeReadTwo ( Fraig_Node_t *  p  ) 

Definition at line 112 of file fraigApi.c.

00112 { assert (!Fraig_IsComplement(p)); return p->p2; }

int Fraig_NodesAreEqual ( Fraig_Man_t *  p,
Fraig_Node_t *  pNode1,
Fraig_Node_t *  pNode2,
int  nBTLimit,
int  nTimeLimit 
)

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

Synopsis [Checks equivalence of two nodes.]

Description [Returns 1 iff the nodes are equivalent.]

SideEffects []

SeeAlso []

Definition at line 63 of file fraigSat.c.

00064 {
00065     if ( pNode1 == pNode2 )
00066         return 1;
00067     if ( pNode1 == Fraig_Not(pNode2) )
00068         return 0;
00069     return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
00070 }

void Fraig_NodeSetChoice ( Fraig_Man_t *  pMan,
Fraig_Node_t *  pNodeOld,
Fraig_Node_t *  pNodeNew 
)

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

Synopsis [Sets the node to be equivalent to the given one.]

Description [This procedure is a work-around for the equivalence check. Does not verify the equivalence. Use at the user's risk.]

SideEffects []

SeeAlso []

Definition at line 285 of file fraigApi.c.

00286 {
00287 //    assert( pMan->fChoicing );
00288     pNodeNew->pNextE = pNodeOld->pNextE;
00289     pNodeOld->pNextE = pNodeNew;
00290     pNodeNew->pRepr  = pNodeOld;
00291 }

void Fraig_NodeSetData0 ( Fraig_Node_t *  p,
Fraig_Node_t *  pData 
)

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

Synopsis [Access functions to set the data members of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fraigApi.c.

00137 { p->pData0  = pData;  }

void Fraig_NodeSetData1 ( Fraig_Node_t *  p,
Fraig_Node_t *  pData 
)

Definition at line 138 of file fraigApi.c.

00138 { p->pData1  = pData;  }

Fraig_NodeVec_t* Fraig_NodeVecAlloc ( int  nCap  ) 

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

FileName [fraigVec.c]

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

Synopsis [Vector of FRAIG nodes.]

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

Affiliation [UC Berkeley]

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

Revision [

Id
fraigVec.c,v 1.7 2005/07/08 01:01:34 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 40 of file fraigVec.c.

00041 {
00042     Fraig_NodeVec_t * p;
00043     p = ALLOC( Fraig_NodeVec_t, 1 );
00044     if ( nCap > 0 && nCap < 8 )
00045         nCap = 8;
00046     p->nSize  = 0;
00047     p->nCap   = nCap;
00048     p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
00049     return p;
00050 }

void Fraig_NodeVecClear ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file fraigVec.c.

00171 {
00172     p->nSize = 0;
00173 }

Fraig_NodeVec_t* Fraig_NodeVecDup ( Fraig_NodeVec_t *  pVec  ) 

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

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file fraigVec.c.

00081 {
00082     Fraig_NodeVec_t * p;
00083     p = ALLOC( Fraig_NodeVec_t, 1 );
00084     p->nSize  = pVec->nSize;
00085     p->nCap   = pVec->nCap;
00086     p->pArray = p->nCap? ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
00087     memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize );
00088     return p;
00089 }

void Fraig_NodeVecFree ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file fraigVec.c.

00064 {
00065     FREE( p->pArray );
00066     FREE( p );
00067 }

void Fraig_NodeVecGrow ( Fraig_NodeVec_t *  p,
int  nCapMin 
)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file fraigVec.c.

00135 {
00136     if ( p->nCap >= nCapMin )
00137         return;
00138     p->pArray = REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); 
00139     p->nCap   = nCapMin;
00140 }

Fraig_Node_t* Fraig_NodeVecPop ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file fraigVec.c.

00329 {
00330     return p->pArray[--p->nSize];
00331 }

void Fraig_NodeVecPush ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file fraigVec.c.

00187 {
00188     if ( p->nSize == p->nCap )
00189     {
00190         if ( p->nCap < 16 )
00191             Fraig_NodeVecGrow( p, 16 );
00192         else
00193             Fraig_NodeVecGrow( p, 2 * p->nCap );
00194     }
00195     p->pArray[p->nSize++] = Entry;
00196 }

void Fraig_NodeVecPushOrder ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Inserts a new node in the order by arrival times.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file fraigVec.c.

00231 {
00232     Fraig_Node_t * pNode1, * pNode2;
00233     int i;
00234     Fraig_NodeVecPush( p, pNode );
00235     // find the p of the node
00236     for ( i = p->nSize-1; i > 0; i-- )
00237     {
00238         pNode1 = p->pArray[i  ];
00239         pNode2 = p->pArray[i-1];
00240         if ( pNode1 >= pNode2 )
00241             break;
00242         p->pArray[i  ] = pNode2;
00243         p->pArray[i-1] = pNode1;
00244     }
00245 }

void Fraig_NodeVecPushOrderByLevel ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Inserts a new node in the order by arrival times.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file fraigVec.c.

00280 {
00281     Fraig_Node_t * pNode1, * pNode2;
00282     int i;
00283     Fraig_NodeVecPush( p, pNode );
00284     // find the p of the node
00285     for ( i = p->nSize-1; i > 0; i-- )
00286     {
00287         pNode1 = p->pArray[i  ];
00288         pNode2 = p->pArray[i-1];
00289         if ( Fraig_Regular(pNode1)->Level <= Fraig_Regular(pNode2)->Level )
00290             break;
00291         p->pArray[i  ] = pNode2;
00292         p->pArray[i-1] = pNode1;
00293     }
00294 }

int Fraig_NodeVecPushUnique ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis [Add the element while ensuring uniqueness.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 209 of file fraigVec.c.

00210 {
00211     int i;
00212     for ( i = 0; i < p->nSize; i++ )
00213         if ( p->pArray[i] == Entry )
00214             return 1;
00215     Fraig_NodeVecPush( p, Entry );
00216     return 0;
00217 }

int Fraig_NodeVecPushUniqueOrder ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Add the element while ensuring uniqueness in the order.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 258 of file fraigVec.c.

00259 {
00260     int i;
00261     for ( i = 0; i < p->nSize; i++ )
00262         if ( p->pArray[i] == pNode )
00263             return 1;
00264     Fraig_NodeVecPushOrder( p, pNode );
00265     return 0;
00266 }

int Fraig_NodeVecPushUniqueOrderByLevel ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  pNode 
)

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

Synopsis [Add the element while ensuring uniqueness in the order.]

Description [Returns 1 if the element was found, and 0 if it was new. ]

SideEffects []

SeeAlso []

Definition at line 307 of file fraigVec.c.

00308 {
00309     int i;
00310     for ( i = 0; i < p->nSize; i++ )
00311         if ( p->pArray[i] == pNode )
00312             return 1;
00313     Fraig_NodeVecPushOrderByLevel( p, pNode );
00314     return 0;
00315 }

Fraig_Node_t** Fraig_NodeVecReadArray ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file fraigVec.c.

00103 {
00104     return p->pArray;
00105 }

Fraig_Node_t* Fraig_NodeVecReadEntry ( Fraig_NodeVec_t *  p,
int  i 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file fraigVec.c.

00385 {
00386     assert( i >= 0 && i < p->nSize );
00387     return p->pArray[i];
00388 }

int Fraig_NodeVecReadSize ( Fraig_NodeVec_t *  p  ) 

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file fraigVec.c.

00119 {
00120     return p->nSize;
00121 }

void Fraig_NodeVecRemove ( Fraig_NodeVec_t *  p,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 344 of file fraigVec.c.

00345 {
00346     int i;
00347     for ( i = 0; i < p->nSize; i++ )
00348         if ( p->pArray[i] == Entry )
00349             break;
00350     assert( i < p->nSize );
00351     for ( i++; i < p->nSize; i++ )
00352         p->pArray[i-1] = p->pArray[i];
00353     p->nSize--;
00354 }

void Fraig_NodeVecShrink ( Fraig_NodeVec_t *  p,
int  nSizeNew 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file fraigVec.c.

00154 {
00155     assert( p->nSize >= nSizeNew );
00156     p->nSize = nSizeNew;
00157 }

void Fraig_NodeVecSortByLevel ( Fraig_NodeVec_t *  p,
int  fIncreasing 
)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file fraigVec.c.

00499 {
00500     if ( fIncreasing )
00501         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00502                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsIncreasing );
00503     else 
00504         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00505                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsDecreasing );
00506 }

void Fraig_NodeVecSortByNumber ( Fraig_NodeVec_t *  p  ) 

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 519 of file fraigVec.c.

00520 {
00521     qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
00522             (int (*)(const void *, const void *)) Fraig_NodeVecCompareNumbers );
00523 }

void Fraig_NodeVecWriteEntry ( Fraig_NodeVec_t *  p,
int  i,
Fraig_Node_t *  Entry 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file fraigVec.c.

00368 {
00369     assert( i >= 0 && i < p->nSize );
00370     p->pArray[i] = Entry;
00371 }

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 }

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 }

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