Data Structures
struct	Fraig_ParamsStruct_t_

struct	Prove_ParamsStruct_t_

Macros
#define	Fraig_IsComplement(p) (((int)((ABC_PTRUINT_T) (p) & 01)))
	GLOBAL VARIABLES ///. More...

#define	Fraig_Regular(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01))

#define	Fraig_Not(p) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01))

#define	Fraig_NotCond(p, c) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))

#define	Fraig_Ref(p)

#define	Fraig_Deref(p)

#define	Fraig_RecursiveDeref(p, c)

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_	Fraig_Man_t
	INCLUDES ///. More...

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)
	FUNCTION DEFINITIONS ///. More...

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_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)
	FUNCTION DEFINITIONS ///. More...

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)
	FUNCTION DEFINITIONS ///. More...

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)
	FUNCTION DEFINITIONS ///. More...

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)
	DECLARATIONS ///. More...

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)

Macro Definition Documentation

#define Fraig_Deref ( p )

Definition at line 114 of file fraig.h.

#define Fraig_IsComplement ( p ) (((int)((ABC_PTRUINT_T) (p) & 01)))

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///

Definition at line 107 of file fraig.h.

#define Fraig_Not ( p ) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01))

Definition at line 109 of file fraig.h.

#define Fraig_NotCond	(	p,
		c
	)	((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))

Definition at line 110 of file fraig.h.

#define Fraig_RecursiveDeref	(	p,
		c
	)

Definition at line 115 of file fraig.h.

#define Fraig_Ref ( p )

Definition at line 113 of file fraig.h.

#define Fraig_Regular ( p ) ((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01))

Definition at line 108 of file fraig.h.

Typedef Documentation

typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t

Definition at line 43 of file fraig.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t

INCLUDES ///.

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

FileName [fraig.h]

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

Synopsis [External declarations of the FRAIG package.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

]PARAMETERS ///STRUCTURE DEFINITIONS ///

Definition at line 40 of file fraig.h.

typedef struct Fraig_NodeStruct_t_ Fraig_Node_t

Definition at line 41 of file fraig.h.

typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t

Definition at line 42 of file fraig.h.

typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t

Definition at line 44 of file fraig.h.

typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t

Definition at line 45 of file fraig.h.

typedef struct Prove_ParamsStruct_t_ Prove_Params_t

Definition at line 46 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 173 of file fraigUtil.c.

 {
     assert( !Fraig_IsComplement(pOld) );
     assert( !Fraig_IsComplement(pNew) );
     pMan->nTravIds++;
     return Fraig_CheckTfi_rec( pMan, pNew, pOld );
 }

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 960 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vSuper;
     vSuper = Fraig_NodeVecAlloc( 8 );
     Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
     return vSuper;
 }

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 152 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vNodes;
     int RetValue;
     vNodes = Fraig_Dfs( pMan, fEquiv );
     RetValue = vNodes->nSize;
     Fraig_NodeVecFree( vNodes );
     return RetValue;
 }

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 58 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vNodes;
     int i;
     pMan->nTravIds++;
     vNodes = Fraig_NodeVecAlloc( 100 );
     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
         Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv );
     return vNodes;
 }

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 100 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vNodes;
     int i;
     pMan->nTravIds++;
     vNodes = Fraig_NodeVecAlloc( 100 );
     for ( i = 0; i < nNodes; i++ )
         Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv );
     return vNodes;
 }

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 80 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vNodes;
     pMan->nTravIds++;
     vNodes = Fraig_NodeVecAlloc( 100 );
     Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv );
     return vNodes;
 }

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 428 of file fraigUtil.c.

 {
     int nLevelMax, i;
     nLevelMax = 0;
     for ( i = 0; i < pMan->vOutputs->nSize; i++ )
         nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level? 
                 nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level;
     return nLevelMax;
 }

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 521 of file fraigMan.c.

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

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 653 of file fraigSat.c.

 {
     Fraig_Node_t * pNode1R, * pNode2R;
     int RetValue, RetValue1, i;
     abctime clk;
     int fVerbose = 0;
 
     pNode1R = Fraig_Regular(pNode1);
     pNode2R = Fraig_Regular(pNode2);
     assert( pNode1R != pNode2R );
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
         Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
    // get the logic cone
 clk = Abc_Clock();
     Fraig_OrderVariables( p, pNode1R, pNode2R );
 //    Fraig_PrepareCones( p, pNode1R, pNode2R );
 p->timeTrav += Abc_Clock() - clk;
 
     ////////////////////////////////////////////
     // prepare the solver to run incrementally on these variables
 //clk = Abc_Clock();
     Msat_SolverPrepare( p->pSat, p->vVarsInt );
 //p->time3 += Abc_Clock() - clk;
 
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
     Msat_IntVecClear( p->vProj );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, !Fraig_IsComplement(pNode1)) );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, !Fraig_IsComplement(pNode2)) );
     // run the solver
 clk = Abc_Clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 );
 p->timeSat += Abc_Clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
 
         // add the clause
         Msat_IntVecClear( p->vProj );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode1R->Num, Fraig_IsComplement(pNode1)) );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode2R->Num, Fraig_IsComplement(pNode2)) );
         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
         assert( RetValue );
 //        p->nSatProofImp++;
         return 1;
     }
     else if ( RetValue1 == MSAT_TRUE )
     {
 //p->time2 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
         // record the counter example
 //        Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pNode1R, pNode2R );
         p->nSatCounterImp++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += Abc_Clock() - clk;
         p->nSatFailsImp++;
         return 0;
     }
 }

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 454 of file fraigMan.c.

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

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 312 of file fraigUtil.c.

 {
     Fraig_Node_t * pNode;
     Fraig_NodeVec_t * pVec;
     int i;
     pVec = Fraig_Dfs( p, 0 );
     for ( i = 0; i < pVec->nSize; i++ )
     {
         pNode = pVec->pArray[i];
         if ( Fraig_NodeIsVar(pNode) )
         {
             if ( pNode->pRepr )
                 printf( "Primary input %d is a secondary node.\n", pNode->Num );
         }
         else if ( Fraig_NodeIsConst(pNode) )
         {
             if ( pNode->pRepr )
                 printf( "Constant 1 %d is a secondary node.\n", pNode->Num );
         }
         else
         {
             if ( pNode->pRepr )
                 printf( "Internal node %d is a secondary node.\n", pNode->Num );
             if ( Fraig_Regular(pNode->p1)->pRepr )
                 printf( "Internal node %d has first fanin %d that is a secondary node.\n", 
                     pNode->Num, Fraig_Regular(pNode->p1)->Num );
             if ( Fraig_Regular(pNode->p2)->pRepr )
                 printf( "Internal node %d has second fanin %d that is a secondary node.\n", 
                     pNode->Num, Fraig_Regular(pNode->p2)->Num );
         }
     }
     Fraig_NodeVecFree( pVec );
     return 1;
 }

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 130 of file fraigSat.c.

 {
     Fraig_Node_t * pNode;
     int i;
     ABC_FREE( p->pModel );
     for ( i = 0; i < p->vOutputs->nSize; i++ )
     {
         // get the output node (it can be complemented!)
         pNode = p->vOutputs->pArray[i];
         // if the miter is constant 0, the problem is UNSAT
         if ( pNode == Fraig_Not(p->pConst1) )
             continue;
         // consider the special case when the miter is constant 1
         if ( pNode == p->pConst1 )
         {
             // in this case, any counter example will do to distinquish it from constant 0
             // here we pick the counter example composed of all zeros
             p->pModel = Fraig_ManAllocCounterExample( p );
             return 0;
         }
         // save the counter example
         p->pModel = Fraig_ManSaveCounterExample( p, pNode );
         // if the model is not found, return undecided
         if ( p->pModel == NULL )
             return -1;
         else
             return 0;
     }
     return 1;
 }

Fraig_Man_t* Fraig_ManCreate ( Fraig_Params_t * pParams )

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

Synopsis [Creates the new FRAIG manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file fraigMan.c.

 {
     Fraig_Params_t Params;
     Fraig_Man_t * p;
 
     // set the random seed for simulation
 //    srand( 0xFEEDDEAF );
 //    srand( 0xDEADCAFE );
     Aig_ManRandom( 1 );
 
     // set parameters for equivalence checking
     if ( pParams == NULL )
         Fraig_ParamsSetDefault( pParams = &Params );
     // adjust the amount of simulation info
     if ( pParams->nPatsRand < 128 )
         pParams->nPatsRand = 128;
     if ( pParams->nPatsRand > 32768 )
         pParams->nPatsRand = 32768;
     if ( pParams->nPatsDyna < 128 )
         pParams->nPatsDyna = 128;
     if ( pParams->nPatsDyna > 32768 )
         pParams->nPatsDyna = 32768;
     // if reduction is not performed, allocate minimum simulation info
     if ( !pParams->fFuncRed )
         pParams->nPatsRand = pParams->nPatsDyna = 128;
 
     // start the manager
     p = ABC_ALLOC( Fraig_Man_t, 1 );
     memset( p, 0, sizeof(Fraig_Man_t) );
 
     // set the default parameters
     p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand );  // the number of words of random simulation info
     p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna );  // the number of patterns for dynamic simulation info
     p->nBTLimit   = pParams->nBTLimit;    // -1 means infinite backtrack limit
     p->nSeconds   = pParams->nSeconds;    // the timeout for the final miter
     p->fFuncRed   = pParams->fFuncRed;    // enables functional reduction (otherwise, only one-level hashing is performed)
     p->fFeedBack  = pParams->fFeedBack;   // enables solver feedback (the use of counter-examples in simulation)
     p->fDist1Pats = pParams->fDist1Pats;  // enables solver feedback (the use of counter-examples in simulation)
     p->fDoSparse  = pParams->fDoSparse;   // performs equivalence checking for sparse functions (whose sim-info is 0)
     p->fChoicing  = pParams->fChoicing;   // disable accumulation of structural choices (keeps only the first choice)
     p->fTryProve  = pParams->fTryProve;   // disable accumulation of structural choices (keeps only the first choice)
     p->fVerbose   = pParams->fVerbose;    // disable verbose output
     p->fVerboseP  = pParams->fVerboseP;   // disable verbose output
     p->nInspLimit = pParams->nInspLimit;  // the limit on the number of inspections
 
     // start memory managers
     p->mmNodes    = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
     p->mmSims     = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) );
     // allocate node arrays
     p->vInputs    = Fraig_NodeVecAlloc( 1000 );    // the array of primary inputs
     p->vOutputs   = Fraig_NodeVecAlloc( 1000 );    // the array of primary outputs
     p->vNodes     = Fraig_NodeVecAlloc( 1000 );    // the array of internal nodes
     // start the tables
     p->pTableS    = Fraig_HashTableCreate( 1000 ); // hashing by structure
     p->pTableF    = Fraig_HashTableCreate( 1000 ); // hashing by function
     p->pTableF0   = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions)
     // create the constant node
     p->pConst1    = Fraig_NodeCreateConst( p );
     // initialize SAT solver feedback data structures
     Fraig_FeedBackInit( p );
     // initialize other variables
     p->vProj      = Msat_IntVecAlloc( 10 ); 
     p->nTravIds   = 1;
     p->nTravIds2  = 1;
     return p;
 }

void Fraig_ManFree ( Fraig_Man_t * p )

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

Synopsis [Deallocates the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 262 of file fraigMan.c.

 {
     int i;
     if ( p->fVerbose )   
     {
         if ( p->fChoicing ) Fraig_ManReportChoices( p );
         Fraig_ManPrintStats( p );
 //        Fraig_TablePrintStatsS( p );
 //        Fraig_TablePrintStatsF( p );
 //        Fraig_TablePrintStatsF0( p );
     }
  
     for ( i = 0; i < p->vNodes->nSize; i++ )
         if ( p->vNodes->pArray[i]->vFanins )
         {
             Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins );
             p->vNodes->pArray[i]->vFanins = NULL;
         }
 
     if ( p->vInputs )    Fraig_NodeVecFree( p->vInputs );
     if ( p->vNodes )     Fraig_NodeVecFree( p->vNodes );
     if ( p->vOutputs )   Fraig_NodeVecFree( p->vOutputs );
 
     if ( p->pTableS )    Fraig_HashTableFree( p->pTableS );
     if ( p->pTableF )    Fraig_HashTableFree( p->pTableF );
     if ( p->pTableF0 )   Fraig_HashTableFree( p->pTableF0 );
 
     if ( p->pSat )       Msat_SolverFree( p->pSat );
     if ( p->vProj )      Msat_IntVecFree( p->vProj );
     if ( p->vCones )     Fraig_NodeVecFree( p->vCones );
     if ( p->vPatsReal )  Msat_IntVecFree( p->vPatsReal );
     if ( p->pModel )     ABC_FREE( p->pModel );
 
     Fraig_MemFixedStop( p->mmNodes, 0 );
     Fraig_MemFixedStop( p->mmSims, 0 );
 
     if ( p->pSuppS )
     {
         ABC_FREE( p->pSuppS[0] );
         ABC_FREE( p->pSuppS );
     }
     if ( p->pSuppF )
     {
         ABC_FREE( p->pSuppF[0] );
         ABC_FREE( p->pSuppF );
     }
 
     ABC_FREE( p->ppOutputNames );
     ABC_FREE( p->ppInputNames );
     ABC_FREE( p );
 }

Fraig_NodeVec_t* Fraig_ManGetSimInfo ( Fraig_Man_t * p )

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

Synopsis [Returns simulation info of all nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 417 of file fraigMan.c.

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

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 251 of file fraigUtil.c.

 {
     Fraig_NodeVec_t * vNodes;
     Fraig_Node_t * pNodeR;
     int i;
     // collect the nodes reachable
     vNodes = Fraig_Dfs( p, 0 );
     // clean the fanouts field
     for ( i = 0; i < vNodes->nSize; i++ )
     {
         vNodes->pArray[i]->nFanouts = 0;
         vNodes->pArray[i]->pData0 = NULL;
     }
     // mark reachable nodes by setting the two-bit counter pNode->nFans
     for ( i = 0; i < vNodes->nSize; i++ )
     {
         pNodeR = Fraig_Regular(vNodes->pArray[i]->p1);
         if ( pNodeR && ++pNodeR->nFanouts == 3 )
             pNodeR->nFanouts = 2;
         pNodeR = Fraig_Regular(vNodes->pArray[i]->p2);
         if ( pNodeR && ++pNodeR->nFanouts == 3 )
             pNodeR->nFanouts = 2;
     }
     Fraig_NodeVecFree( vNodes );
 }

void Fraig_ManPrintStats ( Fraig_Man_t * p )

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

Synopsis [Deallocates the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 351 of file fraigMan.c.

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

void Fraig_ManProveMiter ( Fraig_Man_t * p )

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

Synopsis [Tries to prove the final miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file fraigSat.c.

 {
     Fraig_Node_t * pNode;
     int i;
     abctime clk;
 
     if ( !p->fTryProve )
         return;
  
     clk = Abc_Clock();
     // consider all outputs of the multi-output miter
     for ( i = 0; i < p->vOutputs->nSize; i++ )
     {
         pNode = Fraig_Regular(p->vOutputs->pArray[i]);
         // skip already constant nodes
         if ( pNode == p->pConst1 )
             continue;
         // skip nodes that are different according to simulation
         if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) )
             continue;
         if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) )
         {
             if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ^ Fraig_NodeComparePhase(p->pConst1, pNode) )
                 p->vOutputs->pArray[i] = Fraig_Not(p->pConst1);
             else
                 p->vOutputs->pArray[i] = p->pConst1;
         }
     }
     if ( p->fVerboseP ) 
     {
 //        ABC_PRT( "Final miter proof time", Abc_Clock() - clk );
     }
 }

int Fraig_ManReadChoicing ( Fraig_Man_t * p )

Definition at line 61 of file fraigApi.c.

61 { return p->fChoicing; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadConflicts ( Fraig_Man_t * p )

Definition at line 73 of file fraigApi.c.

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

Msat_SolverReadBackTracks

int Msat_SolverReadBackTracks(Msat_Solver_t *p)

Definition: msatSolverApi.c:58

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_Node_t* Fraig_ManReadConst1 ( Fraig_Man_t * p )

Definition at line 52 of file fraigApi.c.

52 { return p->pConst1; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadDoSparse ( Fraig_Man_t * p )

Definition at line 60 of file fraigApi.c.

60 { return p->fDoSparse; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadFeedBack ( Fraig_Man_t * p )

Definition at line 59 of file fraigApi.c.

59 { return p->fFeedBack; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadFuncRed ( Fraig_Man_t * p )

Definition at line 58 of file fraigApi.c.

58 { return p->fFuncRed; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

char** Fraig_ManReadInputNames ( Fraig_Man_t * p )

Definition at line 54 of file fraigApi.c.

54 { return p->ppInputNames; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadInputNum ( Fraig_Man_t * p )

Definition at line 49 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_Node_t** Fraig_ManReadInputs ( Fraig_Man_t * p )

Definition at line 46 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadInspects ( Fraig_Man_t * p )

Definition at line 75 of file fraigApi.c.

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

Msat_SolverReadInspects

int Msat_SolverReadInspects(Msat_Solver_t *p)

Definition: msatSolverApi.c:59

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_Node_t* Fraig_ManReadIthNode	(	Fraig_Man_t *	p,
		int	i
	)

Definition at line 53 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

assert

#define assert(ex)

Definition: util_old.h:213

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.

 {
     int k;
     if ( i < 0 )
     {
         printf( "Requesting a PI with a negative number\n" );
         return NULL;
     }
     // create the PIs to fill in the interval
     if ( i >= p->vInputs->nSize )
         for ( k = p->vInputs->nSize; k <= i; k++ )
             Fraig_NodeCreatePi( p ); 
     return p->vInputs->pArray[i];
 }

int* Fraig_ManReadModel ( Fraig_Man_t * p )

Definition at line 63 of file fraigApi.c.

63 { return p->pModel; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadNodeNum ( Fraig_Man_t * p )

Definition at line 51 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_Node_t** Fraig_ManReadNodes ( Fraig_Man_t * p )

Definition at line 48 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

char** Fraig_ManReadOutputNames ( Fraig_Man_t * p )

Definition at line 55 of file fraigApi.c.

55 { return p->ppOutputNames; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadOutputNum ( Fraig_Man_t * p )

Definition at line 50 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_Node_t** Fraig_ManReadOutputs ( Fraig_Man_t * p )

Definition at line 47 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadPatternNumDynamic ( Fraig_Man_t * p )

Definition at line 67 of file fraigApi.c.

67 { return p->iWordStart * 32; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadPatternNumDynamicFiltered ( Fraig_Man_t * p )

Definition at line 69 of file fraigApi.c.

69 { return p->iPatsPerm; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadPatternNumRandom ( Fraig_Man_t * p )

Definition at line 65 of file fraigApi.c.

65 { return p->nWordsRand * 32; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

char* Fraig_ManReadSat ( Fraig_Man_t * p )

Definition at line 57 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadSatFails ( Fraig_Man_t * p )

Definition at line 71 of file fraigApi.c.

71 { return p->nSatFailsReal; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

char* Fraig_ManReadVarsInt ( Fraig_Man_t * p )

Definition at line 56 of file fraigApi.c.

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

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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 alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigApi.c.

43 { return p->vInputs; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_NodeVec_t* Fraig_ManReadVecNodes ( Fraig_Man_t * p )

Definition at line 45 of file fraigApi.c.

45 { return p->vNodes; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

Fraig_NodeVec_t* Fraig_ManReadVecOutputs ( Fraig_Man_t * p )

Definition at line 44 of file fraigApi.c.

44 { return p->vOutputs; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

int Fraig_ManReadVerbose ( Fraig_Man_t * p )

Definition at line 62 of file fraigApi.c.

62 { return p->fVerbose; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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 520 of file fraigUtil.c.

 {
     Fraig_Node_t * pNode, * pTemp;
     int nChoiceNodes, nChoices;
     int i, LevelMax1, LevelMax2;
 
     // report the number of levels
     LevelMax1 = Fraig_GetMaxLevel( pMan );
     Fraig_MappingSetChoiceLevels( pMan, 0 );
     LevelMax2 = Fraig_GetMaxLevel( pMan );
 
     // report statistics about choices
     nChoiceNodes = nChoices = 0;
     for ( i = 0; i < pMan->vNodes->nSize; i++ )
     {
         pNode = pMan->vNodes->pArray[i];
         if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
         { // this is a choice node = the primary node that has equivalent nodes
             nChoiceNodes++;
             for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
                 nChoices++;
         }
     }
     printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
     printf( "Choice stats:  Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
 }

void Fraig_ManSetChoicing	(	Fraig_Man_t *	p,
		int	fChoicing
	)

Definition at line 91 of file fraigApi.c.

91 { p->fChoicing = fChoicing; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

void Fraig_ManSetDoSparse	(	Fraig_Man_t *	p,
		int	fDoSparse
	)

Definition at line 90 of file fraigApi.c.

90 { p->fDoSparse = fDoSparse; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

void Fraig_ManSetFeedBack	(	Fraig_Man_t *	p,
		int	fFeedBack
	)

Definition at line 89 of file fraigApi.c.

89 { p->fFeedBack = fFeedBack; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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 88 of file fraigApi.c.

88 { p->fFuncRed = fFuncRed; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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

Definition at line 95 of file fraigApi.c.

95 { p->ppInputNames = ppNames; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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

Definition at line 94 of file fraigApi.c.

94 { p->ppOutputNames = ppNames; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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.

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

void Fraig_ManSetTryProve	(	Fraig_Man_t *	p,
		int	fTryProve
	)

Definition at line 92 of file fraigApi.c.

92 { p->fTryProve = fTryProve; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

void Fraig_ManSetVerbose	(	Fraig_Man_t *	p,
		int	fVerbose
	)

Definition at line 93 of file fraigApi.c.

93 { p->fVerbose = fVerbose; }

p

static Llb_Mgr_t * p

Definition: llb3Image.c:950

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 499 of file fraigUtil.c.

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

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.

 {
     return Fraig_NodeAndCanon( p, p1, p2 );
 }

int Fraig_NodeComparePhase	(	Fraig_Node_t *	p1,
		Fraig_Node_t *	p2
	)

Definition at line 154 of file fraigApi.c.

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

Fraig_IsComplement

#define Fraig_IsComplement(p)

GLOBAL VARIABLES ///.

Definition: fraig.h:107

assert

#define assert(ex)

Definition: util_old.h:213

Fraig_NodeStruct_t_::fInv

unsigned fInv

Definition: fraigInt.h:218

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.

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

int Fraig_NodeIsAnd ( Fraig_Node_t * p )

Definition at line 153 of file fraigApi.c.

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

Fraig_Regular

#define Fraig_Regular(p)

Definition: fraig.h:108

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.

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

Fraig_Regular

#define Fraig_Regular(p)

Definition: fraig.h:108

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 302 of file fraigSat.c.

 {
     int RetValue, RetValue1, i, fComp;
     abctime clk;
     int fVerbose = 0;
     int fSwitch = 0;
 
     // make sure the nodes are not complemented
     assert( !Fraig_IsComplement(pNew) );
     assert( !Fraig_IsComplement(pOld) );
     assert( pNew != pOld );
 
     // if at least one of the nodes is a failed node, perform adjustments:
     // if the backtrack limit is small, simply skip this node
     // if the backtrack limit is > 10, take the quare root of the limit
     if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
     {
         p->nSatFails++;
 //            return 0;
 //        if ( nBTLimit > 10 )
 //            nBTLimit /= 10;
         if ( nBTLimit <= 10 )
             return 0;
         nBTLimit = (int)sqrt((double)nBTLimit);
 //        fSwitch = 1;
     }
 
     p->nSatCalls++;
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
         Fraig_ManCreateSolver( p );
     // make sure the SAT solver has enough variables
     for ( i = Msat_SolverReadVarNum(p->pSat); i < p->vNodes->nSize; i++ )
         Msat_SolverAddVar( p->pSat, p->vNodes->pArray[i]->Level );
 
 
  
 /*
     {
         Fraig_Node_t * ppNodes[2] = { pOld, pNew };
         extern void Fraig_MappingShowNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppRoots, int nRoots, char * pFileName );
         Fraig_MappingShowNodes( p, ppNodes, 2, "temp_aig" );
     }
 */
 
     nMuxes = 0;
 
 
     // get the logic cone
 clk = Abc_Clock();
 //    Fraig_VarsStudy( p, pOld, pNew );
     Fraig_OrderVariables( p, pOld, pNew );
 //    Fraig_PrepareCones( p, pOld, pNew );
 p->timeTrav += Abc_Clock() - clk;
 
 //    printf( "The number of MUXes detected = %d (%5.2f %% of logic).  ", nMuxes, 300.0*nMuxes/(p->vNodes->nSize - p->vInputs->nSize) );
 //    ABC_PRT( "Time", Abc_Clock() - clk );
 
 if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
     // prepare variable activity
     Fraig_SetActivity( p, pOld, pNew );
 
     // get the complemented attribute
     fComp = Fraig_NodeComparePhase( pOld, pNew );
 //Msat_SolverPrintClauses( p->pSat );
 
     ////////////////////////////////////////////
     // prepare the solver to run incrementally on these variables
 //clk = Abc_Clock();
     Msat_SolverPrepare( p->pSat, p->vVarsInt );
 //p->time3 += Abc_Clock() - clk;
 
 
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
     Msat_IntVecClear( p->vProj );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
 
 //Msat_SolverWriteDimacs( p->pSat, "temp_fraig.cnf" );
 
     // run the solver
 clk = Abc_Clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += Abc_Clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
 
         // add the clause
         Msat_IntVecClear( p->vProj );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
         assert( RetValue );
         // continue solving the other implication
     }
     else if ( RetValue1 == MSAT_TRUE )
     {
 //p->time2 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
 
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
 
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "s(%d)", pNew->Level );
         if ( fSwitch )
              printf( "s(%d)", pNew->Level );
         p->nSatCounter++;
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += Abc_Clock() - clk;
 
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "T(%d)", pNew->Level );
 
         // mark the node as the failed node
         if ( pOld != p->pConst1 ) 
             pOld->fFailTfo = 1;
         pNew->fFailTfo = 1;
 //        p->nSatFails++;
         if ( fSwitch )
              printf( "T(%d)", pNew->Level );
         p->nSatFailsReal++;
         return 0;
     }
 
     // if the old node was constant 0, we already know the answer
     if ( pOld == p->pConst1 )
         return 1;
 
     ////////////////////////////////////////////
     // prepare the solver to run incrementally 
 //clk = Abc_Clock();
     Msat_SolverPrepare( p->pSat, p->vVarsInt );
 //p->time3 += Abc_Clock() - clk;
     // solve under assumptions
     // A = 0; B = 1     OR     A = 0; B = 0 
     Msat_IntVecClear( p->vProj );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 1) );
     Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) );
     // run the solver
 clk = Abc_Clock();
     RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit );
 p->timeSat += Abc_Clock() - clk;
 
     if ( RetValue1 == MSAT_FALSE )
     {
 //p->time1 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "unsat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
 
         // add the clause
         Msat_IntVecClear( p->vProj );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pOld->Num, 0) );
         Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) );
         RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
         assert( RetValue );
         // continue solving the other implication
     }
     else if ( RetValue1 == MSAT_TRUE )
     {
 //p->time2 += Abc_Clock() - clk;
 
 if ( fVerbose )
 {
 //    printf( "sat  %d  ", Msat_SolverReadBackTracks(p->pSat) );
 //ABC_PRT( "time", Abc_Clock() - clk );
 }
 
         // record the counter example
         Fraig_FeedBack( p, Msat_SolverReadModelArray(p->pSat), p->vVarsInt, pOld, pNew );
         p->nSatCounter++;
 
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "s(%d)", pNew->Level );
         if ( fSwitch )
              printf( "s(%d)", pNew->Level );
         return 0;
     }
     else // if ( RetValue1 == MSAT_UNKNOWN )
     {
 p->time3 += Abc_Clock() - clk;
 
 //        if ( pOld->fFailTfo || pNew->fFailTfo )
 //            printf( "*" );
 //        printf( "T(%d)", pNew->Level );
         if ( fSwitch )
              printf( "T(%d)", pNew->Level );
 
         // mark the node as the failed node
         pOld->fFailTfo = 1;
         pNew->fFailTfo = 1;
 //        p->nSatFails++;
         p->nSatFailsReal++;
         return 0;
     }
 
     // return SAT proof
     p->nSatProof++;
 
 //    if ( pOld->fFailTfo || pNew->fFailTfo )
 //        printf( "*" );
 //    printf( "u(%d)", pNew->Level );
 
     if ( fSwitch )
          printf( "u(%d)", pNew->Level );
 
     return 1;
 }

int Fraig_NodeIsVar ( Fraig_Node_t * p )

Definition at line 152 of file fraigApi.c.

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

Fraig_Regular

#define Fraig_Regular(p)

Definition: fraig.h:108

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.

 {
     Fraig_Node_t * pAnd1, * pAnd2, * pRes;
     pAnd1 = Fraig_NodeAndCanon( p, pC,          pT );     Fraig_Ref( pAnd1 );
     pAnd2 = Fraig_NodeAndCanon( p, Fraig_Not(pC), pE );   Fraig_Ref( pAnd2 );
     pRes  = Fraig_NodeOr( p, pAnd1, pAnd2 ); 
     Fraig_RecursiveDeref( p, pAnd1 );
     Fraig_RecursiveDeref( p, pAnd2 );
     Fraig_Deref( pRes );
     return pRes;
 }

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.

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

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.

108 { return p->pData0; }

Fraig_NodeStruct_t_::pData0

Fraig_Node_t * pData0

Definition: fraigInt.h:251

Fraig_Node_t* Fraig_NodeReadData1 ( Fraig_Node_t * p )

Definition at line 109 of file fraigApi.c.

109 { return p->pData1; }

Fraig_NodeStruct_t_::pData1

Fraig_Node_t * pData1

Definition: fraigInt.h:252

Fraig_Node_t* Fraig_NodeReadNextE ( Fraig_Node_t * p )

Definition at line 113 of file fraigApi.c.

113 { return p->pNextE; }

Fraig_NodeStruct_t_::pNextE

Fraig_Node_t * pNextE

Definition: fraigInt.h:241

int Fraig_NodeReadNum ( Fraig_Node_t * p )

Definition at line 110 of file fraigApi.c.

110 { return p->Num; }

Fraig_NodeStruct_t_::Num

int Num

Definition: fraigInt.h:210

int Fraig_NodeReadNumFanouts ( Fraig_Node_t * p )

Definition at line 116 of file fraigApi.c.

116 { return p->nFanouts; }

Fraig_NodeStruct_t_::nFanouts

unsigned nFanouts

Definition: fraigInt.h:228

int Fraig_NodeReadNumOnes ( Fraig_Node_t * p )

Definition at line 118 of file fraigApi.c.

118 { return p->nOnes; }

Fraig_NodeStruct_t_::nOnes

unsigned nOnes

Definition: fraigInt.h:229

int Fraig_NodeReadNumRefs ( Fraig_Node_t * p )

Definition at line 115 of file fraigApi.c.

115 { return p->nRefs; }

Fraig_NodeStruct_t_::nRefs

int nRefs

Definition: fraigInt.h:213

Fraig_Node_t* Fraig_NodeReadOne ( Fraig_Node_t * p )

Definition at line 111 of file fraigApi.c.

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

Fraig_NodeStruct_t_::p1

Fraig_Node_t * p1

Definition: fraigInt.h:232

Fraig_IsComplement

#define Fraig_IsComplement(p)

GLOBAL VARIABLES ///.

Definition: fraig.h:107

assert

#define assert(ex)

Definition: util_old.h:213

unsigned* Fraig_NodeReadPatternsDynamic ( Fraig_Node_t * p )

Definition at line 124 of file fraigApi.c.

124 { return p->puSimD; }

Fraig_NodeStruct_t_::puSimD

unsigned * puSimD

Definition: fraigInt.h:248

unsigned* Fraig_NodeReadPatternsRandom ( Fraig_Node_t * p )

Definition at line 121 of file fraigApi.c.

121 { return p->puSimR; }

Fraig_NodeStruct_t_::puSimR

unsigned * puSimR

Definition: fraigInt.h:247

Fraig_Node_t* Fraig_NodeReadRepr ( Fraig_Node_t * p )

Definition at line 114 of file fraigApi.c.

114 { return p->pRepr; }

Fraig_NodeStruct_t_::pRepr

Fraig_Node_t * pRepr

Definition: fraigInt.h:242

int Fraig_NodeReadSimInv ( Fraig_Node_t * p )

Definition at line 117 of file fraigApi.c.

117 { return p->fInv; }

Fraig_NodeStruct_t_::fInv

unsigned fInv

Definition: fraigInt.h:218

Fraig_Node_t* Fraig_NodeReadTwo ( Fraig_Node_t * p )

Definition at line 112 of file fraigApi.c.

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

Fraig_NodeStruct_t_::p2

Fraig_Node_t * p2

Definition: fraigInt.h:233

Fraig_IsComplement

#define Fraig_IsComplement(p)

GLOBAL VARIABLES ///.

Definition: fraig.h:107

assert

#define assert(ex)

Definition: util_old.h:213

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 65 of file fraigSat.c.

 {
     if ( pNode1 == pNode2 )
         return 1;
     if ( pNode1 == Fraig_Not(pNode2) )
         return 0;
     return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit );
 }

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.

 {
 //    assert( pMan->fChoicing );
     pNodeNew->pNextE = pNodeOld->pNextE;
     pNodeOld->pNextE = pNodeNew;
     pNodeNew->pRepr  = pNodeOld;
 }

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.

137 { p->pData0 = pData; }

Fraig_NodeStruct_t_::pData0

Fraig_Node_t * pData0

Definition: fraigInt.h:251

void Fraig_NodeSetData1	(	Fraig_Node_t *	p,
		Fraig_Node_t *	pData
	)

Definition at line 138 of file fraigApi.c.

138 { p->pData1 = pData; }

Fraig_NodeStruct_t_::pData1

Fraig_Node_t * pData1

Definition: fraigInt.h:252

Fraig_NodeVec_t* Fraig_NodeVecAlloc ( int nCap )

DECLARATIONS ///.

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

FileName [fraigVec.c]

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

Synopsis [Vector of FRAIG nodes.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

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

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

Synopsis [Allocates a vector with the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file fraigVec.c.

 {
     Fraig_NodeVec_t * p;
     p = ABC_ALLOC( Fraig_NodeVec_t, 1 );
     if ( nCap > 0 && nCap < 8 )
         nCap = 8;
     p->nSize  = 0;
     p->nCap   = nCap;
     p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
     return p;
 }

void Fraig_NodeVecClear ( Fraig_NodeVec_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file fraigVec.c.

 {
     p->nSize = 0;
 }

Fraig_NodeVec_t* Fraig_NodeVecDup ( Fraig_NodeVec_t * pVec )

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

Synopsis [Duplicates the integer array.]

Description []

SideEffects []

SeeAlso []

Definition at line 83 of file fraigVec.c.

 {
     Fraig_NodeVec_t * p;
     p = ABC_ALLOC( Fraig_NodeVec_t, 1 );
     p->nSize  = pVec->nSize;
     p->nCap   = pVec->nCap;
     p->pArray = p->nCap? ABC_ALLOC( Fraig_Node_t *, p->nCap ) : NULL;
     memcpy( p->pArray, pVec->pArray, sizeof(Fraig_Node_t *) * pVec->nSize );
     return p;
 }

void Fraig_NodeVecFree ( Fraig_NodeVec_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file fraigVec.c.

 {
     ABC_FREE( p->pArray );
     ABC_FREE( p );
 }

void Fraig_NodeVecGrow	(	Fraig_NodeVec_t *	p,
		int	nCapMin
	)

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

Synopsis [Resizes the vector to the given capacity.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fraigVec.c.

 {
     if ( p->nCap >= nCapMin )
         return;
     p->pArray = ABC_REALLOC( Fraig_Node_t *, p->pArray, nCapMin ); 
     p->nCap   = nCapMin;
 }

Fraig_Node_t* Fraig_NodeVecPop ( Fraig_NodeVec_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file fraigVec.c.

 {
     return p->pArray[--p->nSize];
 }

void Fraig_NodeVecPush	(	Fraig_NodeVec_t *	p,
		Fraig_Node_t *	Entry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 189 of file fraigVec.c.

 {
     if ( p->nSize == p->nCap )
     {
         if ( p->nCap < 16 )
             Fraig_NodeVecGrow( p, 16 );
         else
             Fraig_NodeVecGrow( p, 2 * p->nCap );
     }
     p->pArray[p->nSize++] = Entry;
 }

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 233 of file fraigVec.c.

 {
     Fraig_Node_t * pNode1, * pNode2;
     int i;
     Fraig_NodeVecPush( p, pNode );
     // find the p of the node
     for ( i = p->nSize-1; i > 0; i-- )
     {
         pNode1 = p->pArray[i  ];
         pNode2 = p->pArray[i-1];
         if ( pNode1 >= pNode2 )
             break;
         p->pArray[i  ] = pNode2;
         p->pArray[i-1] = pNode1;
     }
 }

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 282 of file fraigVec.c.

 {
     Fraig_Node_t * pNode1, * pNode2;
     int i;
     Fraig_NodeVecPush( p, pNode );
     // find the p of the node
     for ( i = p->nSize-1; i > 0; i-- )
     {
         pNode1 = p->pArray[i  ];
         pNode2 = p->pArray[i-1];
         if ( Fraig_Regular(pNode1)->Level <= Fraig_Regular(pNode2)->Level )
             break;
         p->pArray[i  ] = pNode2;
         p->pArray[i-1] = pNode1;
     }
 }

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 212 of file fraigVec.c.

 {
     int i;
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == Entry )
             return 1;
     Fraig_NodeVecPush( p, Entry );
     return 0;
 }

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 261 of file fraigVec.c.

 {
     int i;
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == pNode )
             return 1;
     Fraig_NodeVecPushOrder( p, pNode );
     return 0;
 }

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 310 of file fraigVec.c.

 {
     int i;
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == pNode )
             return 1;
     Fraig_NodeVecPushOrderByLevel( p, pNode );
     return 0;
 }

Fraig_Node_t** Fraig_NodeVecReadArray ( Fraig_NodeVec_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file fraigVec.c.

 {
     return p->pArray;
 }

Fraig_Node_t* Fraig_NodeVecReadEntry	(	Fraig_NodeVec_t *	p,
		int	i
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file fraigVec.c.

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

int Fraig_NodeVecReadSize ( Fraig_NodeVec_t * p )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file fraigVec.c.

 {
     return p->nSize;
 }

void Fraig_NodeVecRemove	(	Fraig_NodeVec_t *	p,
		Fraig_Node_t *	Entry
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file fraigVec.c.

 {
     int i;
     for ( i = 0; i < p->nSize; i++ )
         if ( p->pArray[i] == Entry )
             break;
     assert( i < p->nSize );
     for ( i++; i < p->nSize; i++ )
         p->pArray[i-1] = p->pArray[i];
     p->nSize--;
 }

void Fraig_NodeVecShrink	(	Fraig_NodeVec_t *	p,
		int	nSizeNew
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 156 of file fraigVec.c.

 {
     assert( p->nSize >= nSizeNew );
     p->nSize = nSizeNew;
 }

void Fraig_NodeVecSortByLevel	(	Fraig_NodeVec_t *	p,
		int	fIncreasing
	)

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 501 of file fraigVec.c.

 {
     if ( fIncreasing )
         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsIncreasing );
     else 
         qsort( (void *)p->pArray, p->nSize, sizeof(Fraig_Node_t *), 
                 (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsDecreasing );
 }

void Fraig_NodeVecSortByNumber ( Fraig_NodeVec_t * p )

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 522 of file fraigVec.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file fraigVec.c.

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

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 122 of file fraigMan.c.

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

void Fraig_ParamsSetDefaultFull ( Fraig_Params_t * pParams )

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

Synopsis [Sets the default parameters of the package.]

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

SideEffects []

SeeAlso []

Definition at line 153 of file fraigMan.c.

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

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 46 of file fraigMan.c.

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

Data Structures

Macros

Typedefs

Functions

Macro Definition Documentation

Typedef Documentation

Function Documentation