fraig.h File Reference

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

Go to the source code of this file.

Classes
struct	Fraig_ParamsStruct_t_
struct	Prove_ParamsStruct_t_

Macros
#define	Fraig_IsComplement(p)
	GLOBAL VARIABLES ///.
#define	Fraig_Regular(p)
#define	Fraig_Not(p)
#define	Fraig_NotCond(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 ///.
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

Functions
Fraig_NodeVec_t *	Fraig_ManReadVecInputs (Fraig_Man_t *p)
	FUNCTION DEFINITIONS ///.
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 ///.
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 ///.
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 ///.
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 ///.
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

Fraig_Deref

#define Fraig_Deref

(

p

)

Definition at line 114 of file fraig.h.

Fraig_IsComplement

#define Fraig_IsComplement

(

p

)

Value:

(((int)((ABC_PTRUINT_T) (p) & 01)))

GLOBAL VARIABLES ///.

MACRO DEFINITIONS ///

Definition at line 107 of file fraig.h.

Fraig_Not

#define Fraig_Not

(

p

)

Value:

((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ 01))

Definition at line 109 of file fraig.h.

Fraig_NotCond

#define Fraig_NotCond	(		p,
			c )

Value:

((Fraig_Node_t *)((ABC_PTRUINT_T)(p) ^ (c)))

Definition at line 110 of file fraig.h.

Fraig_RecursiveDeref

#define Fraig_RecursiveDeref	(		p,
			c )

Definition at line 115 of file fraig.h.

Fraig_Ref

#define Fraig_Ref

(

p

)

Definition at line 113 of file fraig.h.

Fraig_Regular

#define Fraig_Regular

(

p

)

Value:

((Fraig_Node_t *)((ABC_PTRUINT_T)(p) & ~01))

Definition at line 108 of file fraig.h.

Typedef Documentation

Fraig_HashTable_t

typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t

Definition at line 43 of file fraig.h.

Fraig_Man_t

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.

Fraig_Node_t

typedef struct Fraig_NodeStruct_t_ Fraig_Node_t

Definition at line 41 of file fraig.h.

Fraig_NodeVec_t

typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t

Definition at line 42 of file fraig.h.

Fraig_Params_t

typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t

Definition at line 44 of file fraig.h.

Fraig_Patterns_t

typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t

Definition at line 45 of file fraig.h.

Function Documentation

Fraig_CheckTfi()

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

extern

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 );
}

Here is the caller graph for this function:

Fraig_CollectSupergate()

Fraig_NodeVec_t * Fraig_CollectSupergate ( Fraig_Node_t * pNode, int fStopAtMux )

extern

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;
}

Here is the call graph for this function:

Fraig_CountLevels()

int Fraig_CountLevels ( Fraig_Man_t * pMan )

extern

Fraig_CountNodes()

int Fraig_CountNodes ( Fraig_Man_t * pMan, int fEquiv )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_Dfs()

Fraig_NodeVec_t * Fraig_Dfs ( Fraig_Man_t * pMan, int fEquiv )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_DfsNodes()

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

extern

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;
}

Here is the call graph for this function:

Fraig_DfsOne()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_DfsReverse()

Fraig_NodeVec_t * Fraig_DfsReverse ( Fraig_Man_t * pMan )

extern

Fraig_GetMaxLevel()

int Fraig_GetMaxLevel ( Fraig_Man_t * pMan )

extern

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;
}

Here is the caller graph for this function:

Fraig_ManAddClause()

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

extern

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 );
}

Here is the call graph for this function:

Fraig_ManCheckClauseUsingSat()

int Fraig_ManCheckClauseUsingSat ( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit )

extern

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;
    }
}

Here is the call graph for this function:

Fraig_ManCheckClauseUsingSimInfo()

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

extern

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;
    }
}

Fraig_ManCheckConsistency()

int Fraig_ManCheckConsistency ( Fraig_Man_t * p )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManCheckMiter()

int Fraig_ManCheckMiter ( Fraig_Man_t * p )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManCreate()

Fraig_Man_t * Fraig_ManCreate ( Fraig_Params_t * pParams )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManFree()

void Fraig_ManFree ( Fraig_Man_t * p )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManGetSimInfo()

Fraig_NodeVec_t * Fraig_ManGetSimInfo ( Fraig_Man_t * p )

extern

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;
}

Here is the call graph for this function:

Fraig_ManMarkRealFanouts()

void Fraig_ManMarkRealFanouts ( Fraig_Man_t * p )

extern

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 );
}

Here is the call graph for this function:

Fraig_ManPrintStats()

void Fraig_ManPrintStats ( Fraig_Man_t * p )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManProveMiter()

void Fraig_ManProveMiter ( Fraig_Man_t * p )

extern

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 );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManReadChoicing()

int Fraig_ManReadChoicing ( Fraig_Man_t * p )

extern

Definition at line 61 of file fraigApi.c.

{ return p->fChoicing;  }

Fraig_ManReadConflicts()

int Fraig_ManReadConflicts ( Fraig_Man_t * p )

extern

Definition at line 73 of file fraigApi.c.

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

Here is the call graph for this function:

Fraig_ManReadConst1()

Fraig_Node_t * Fraig_ManReadConst1 ( Fraig_Man_t * p )

extern

Definition at line 52 of file fraigApi.c.

{ return p->pConst1;            }

Here is the caller graph for this function:

Fraig_ManReadDoSparse()

int Fraig_ManReadDoSparse ( Fraig_Man_t * p )

extern

Definition at line 60 of file fraigApi.c.

{ return p->fDoSparse;  }

Fraig_ManReadFeedBack()

int Fraig_ManReadFeedBack ( Fraig_Man_t * p )

extern

Definition at line 59 of file fraigApi.c.

{ return p->fFeedBack;  }

Fraig_ManReadFuncRed()

int Fraig_ManReadFuncRed ( Fraig_Man_t * p )

extern

Definition at line 58 of file fraigApi.c.

{ return p->fFuncRed;   }

Fraig_ManReadInputNames()

char ** Fraig_ManReadInputNames ( Fraig_Man_t * p )

extern

Definition at line 54 of file fraigApi.c.

{ return p->ppInputNames;       }

Fraig_ManReadInputNum()

int Fraig_ManReadInputNum ( Fraig_Man_t * p )

extern

Definition at line 49 of file fraigApi.c.

{ return p->vInputs->nSize;     }

Here is the caller graph for this function:

Fraig_ManReadInputs()

Fraig_Node_t ** Fraig_ManReadInputs ( Fraig_Man_t * p )

extern

Definition at line 46 of file fraigApi.c.

{ return p->vInputs->pArray;    }

Fraig_ManReadInspects()

int Fraig_ManReadInspects ( Fraig_Man_t * p )

extern

Definition at line 75 of file fraigApi.c.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManReadIthNode()

Fraig_Node_t * Fraig_ManReadIthNode ( Fraig_Man_t * p, int i )

extern

Definition at line 53 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_ManReadIthVar()

Fraig_Node_t * Fraig_ManReadIthVar ( Fraig_Man_t * p, int i )

extern

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];
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManReadModel()

int * Fraig_ManReadModel ( Fraig_Man_t * p )

extern

Definition at line 63 of file fraigApi.c.

{ return p->pModel;     }

Fraig_ManReadNodeNum()

int Fraig_ManReadNodeNum ( Fraig_Man_t * p )

extern

Definition at line 51 of file fraigApi.c.

{ return p->vNodes->nSize;      }

Here is the caller graph for this function:

Fraig_ManReadNodes()

Fraig_Node_t ** Fraig_ManReadNodes ( Fraig_Man_t * p )

extern

Definition at line 48 of file fraigApi.c.

{ return p->vNodes->pArray;     }

Fraig_ManReadOutputNames()

char ** Fraig_ManReadOutputNames ( Fraig_Man_t * p )

extern

Definition at line 55 of file fraigApi.c.

{ return p->ppOutputNames;      }

Fraig_ManReadOutputNum()

int Fraig_ManReadOutputNum ( Fraig_Man_t * p )

extern

Definition at line 50 of file fraigApi.c.

{ return p->vOutputs->nSize;    }

Fraig_ManReadOutputs()

Fraig_Node_t ** Fraig_ManReadOutputs ( Fraig_Man_t * p )

extern

Definition at line 47 of file fraigApi.c.

{ return p->vOutputs->pArray;   }

Here is the caller graph for this function:

Fraig_ManReadPatternNumDynamic()

int Fraig_ManReadPatternNumDynamic ( Fraig_Man_t * p )

extern

Definition at line 67 of file fraigApi.c.

{ return p->iWordStart * 32;  }

Here is the caller graph for this function:

Fraig_ManReadPatternNumDynamicFiltered()

int Fraig_ManReadPatternNumDynamicFiltered ( Fraig_Man_t * p )

extern

Definition at line 69 of file fraigApi.c.

{ return p->iPatsPerm;        }

Fraig_ManReadPatternNumRandom()

int Fraig_ManReadPatternNumRandom ( Fraig_Man_t * p )

extern

Definition at line 65 of file fraigApi.c.

{ return p->nWordsRand * 32;  }

Here is the caller graph for this function:

Fraig_ManReadSat()

char * Fraig_ManReadSat ( Fraig_Man_t * p )

extern

Definition at line 57 of file fraigApi.c.

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

Fraig_ManReadSatFails()

int Fraig_ManReadSatFails ( Fraig_Man_t * p )

extern

Definition at line 71 of file fraigApi.c.

{ return p->nSatFailsReal;    }      

Fraig_ManReadVarsInt()

char * Fraig_ManReadVarsInt ( Fraig_Man_t * p )

extern

Definition at line 56 of file fraigApi.c.

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

Fraig_ManReadVecInputs()

Fraig_NodeVec_t * Fraig_ManReadVecInputs ( Fraig_Man_t * p )

extern

FUNCTION DEFINITIONS ///.

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.

{ return p->vInputs;            }

Fraig_ManReadVecNodes()

Fraig_NodeVec_t * Fraig_ManReadVecNodes ( Fraig_Man_t * p )

extern

Definition at line 45 of file fraigApi.c.

{ return p->vNodes;             }

Fraig_ManReadVecOutputs()

Fraig_NodeVec_t * Fraig_ManReadVecOutputs ( Fraig_Man_t * p )

extern

Definition at line 44 of file fraigApi.c.

{ return p->vOutputs;           }

Fraig_ManReadVerbose()

int Fraig_ManReadVerbose ( Fraig_Man_t * p )

extern

Definition at line 62 of file fraigApi.c.

{ return p->fVerbose;   }

Fraig_ManReportChoices()

void Fraig_ManReportChoices ( Fraig_Man_t * pMan )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManSetChoicing()

void Fraig_ManSetChoicing ( Fraig_Man_t * p, int fChoicing )

extern

Definition at line 91 of file fraigApi.c.

{ p->fChoicing = fChoicing; }

Fraig_ManSetDoSparse()

void Fraig_ManSetDoSparse ( Fraig_Man_t * p, int fDoSparse )

extern

Definition at line 90 of file fraigApi.c.

{ p->fDoSparse = fDoSparse; }

Fraig_ManSetFeedBack()

void Fraig_ManSetFeedBack ( Fraig_Man_t * p, int fFeedBack )

extern

Definition at line 89 of file fraigApi.c.

{ p->fFeedBack = fFeedBack; }

Fraig_ManSetFuncRed()

void Fraig_ManSetFuncRed ( Fraig_Man_t * p, int fFuncRed )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 88 of file fraigApi.c.

{ p->fFuncRed  = fFuncRed;  }

Here is the caller graph for this function:

Fraig_ManSetInputNames()

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

extern

Definition at line 95 of file fraigApi.c.

{ p->ppInputNames  = ppNames; }

Fraig_ManSetOutputNames()

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

extern

Definition at line 94 of file fraigApi.c.

{ p->ppOutputNames = ppNames; }

Fraig_ManSetPo()

void Fraig_ManSetPo ( Fraig_Man_t * p, Fraig_Node_t * pNode )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ManSetTryProve()

void Fraig_ManSetTryProve ( Fraig_Man_t * p, int fTryProve )

extern

Definition at line 92 of file fraigApi.c.

{ p->fTryProve = fTryProve; }

Fraig_ManSetVerbose()

void Fraig_ManSetVerbose ( Fraig_Man_t * p, int fVerbose )

extern

Definition at line 93 of file fraigApi.c.

{ p->fVerbose  = fVerbose;  }

Fraig_MappingSetChoiceLevels()

void Fraig_MappingSetChoiceLevels ( Fraig_Man_t * pMan, int fMaximum )

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeAnd()

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

extern

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 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeComparePhase()

int Fraig_NodeComparePhase ( Fraig_Node_t * p1, Fraig_Node_t * p2 )

extern

Definition at line 154 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodeExor()

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

extern

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 );
}

Here is the call graph for this function:

Fraig_NodeIsAnd()

int Fraig_NodeIsAnd ( Fraig_Node_t * p )

extern

Definition at line 153 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodeIsConst()

int Fraig_NodeIsConst ( Fraig_Node_t * p )

extern

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

Synopsis [Checks the type of the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodeIsEquivalent()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeIsVar()

int Fraig_NodeIsVar ( Fraig_Node_t * p )

extern

Definition at line 152 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodeMux()

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

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeOr()

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

extern

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) ) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeReadData0()

Fraig_Node_t * Fraig_NodeReadData0 ( Fraig_Node_t * p )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file fraigApi.c.

{ return p->pData0;    }

Fraig_NodeReadData1()

Fraig_Node_t * Fraig_NodeReadData1 ( Fraig_Node_t * p )

extern

Definition at line 109 of file fraigApi.c.

{ return p->pData1;    }

Fraig_NodeReadNextE()

Fraig_Node_t * Fraig_NodeReadNextE ( Fraig_Node_t * p )

extern

Definition at line 113 of file fraigApi.c.

{ return p->pNextE;    }

Fraig_NodeReadNum()

int Fraig_NodeReadNum ( Fraig_Node_t * p )

extern

Definition at line 110 of file fraigApi.c.

{ return p->Num;       }

Fraig_NodeReadNumFanouts()

int Fraig_NodeReadNumFanouts ( Fraig_Node_t * p )

extern

Definition at line 116 of file fraigApi.c.

{ return p->nFanouts;  }

Fraig_NodeReadNumOnes()

int Fraig_NodeReadNumOnes ( Fraig_Node_t * p )

extern

Definition at line 118 of file fraigApi.c.

{ return p->nOnes;     }

Fraig_NodeReadNumRefs()

int Fraig_NodeReadNumRefs ( Fraig_Node_t * p )

extern

Definition at line 115 of file fraigApi.c.

{ return p->nRefs;     }

Fraig_NodeReadOne()

Fraig_Node_t * Fraig_NodeReadOne ( Fraig_Node_t * p )

extern

Definition at line 111 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodeReadPatternsDynamic()

unsigned * Fraig_NodeReadPatternsDynamic ( Fraig_Node_t * p )

extern

Definition at line 124 of file fraigApi.c.

{ return p->puSimD;    }

Fraig_NodeReadPatternsRandom()

unsigned * Fraig_NodeReadPatternsRandom ( Fraig_Node_t * p )

extern

Definition at line 121 of file fraigApi.c.

{ return p->puSimR;    }

Fraig_NodeReadRepr()

Fraig_Node_t * Fraig_NodeReadRepr ( Fraig_Node_t * p )

extern

Definition at line 114 of file fraigApi.c.

{ return p->pRepr;     }

Fraig_NodeReadSimInv()

int Fraig_NodeReadSimInv ( Fraig_Node_t * p )

extern

Definition at line 117 of file fraigApi.c.

{ return p->fInv;      }

Fraig_NodeReadTwo()

Fraig_Node_t * Fraig_NodeReadTwo ( Fraig_Node_t * p )

extern

Definition at line 112 of file fraigApi.c.

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

Here is the caller graph for this function:

Fraig_NodesAreEqual()

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

extern

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 );
}

Here is the call graph for this function:

Fraig_NodeSetChoice()

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

extern

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;
}

Fraig_NodeSetData0()

void Fraig_NodeSetData0 ( Fraig_Node_t * p, Fraig_Node_t * pData )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file fraigApi.c.

{ p->pData0  = pData;  }

Fraig_NodeSetData1()

void Fraig_NodeSetData1 ( Fraig_Node_t * p, Fraig_Node_t * pData )

extern

Definition at line 138 of file fraigApi.c.

{ p->pData1  = pData;  }

Here is the caller graph for this function:

Fraig_NodeVecAlloc()

Fraig_NodeVec_t * Fraig_NodeVecAlloc ( int nCap )

extern

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;
}

Here is the caller graph for this function:

Fraig_NodeVecClear()

void Fraig_NodeVecClear ( Fraig_NodeVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file fraigVec.c.

{
    p->nSize = 0;
}

Fraig_NodeVecDup()

Fraig_NodeVec_t * Fraig_NodeVecDup ( Fraig_NodeVec_t * pVec )

extern

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;
}

Here is the call graph for this function:

Fraig_NodeVecFree()

void Fraig_NodeVecFree ( Fraig_NodeVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 66 of file fraigVec.c.

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

Here is the caller graph for this function:

Fraig_NodeVecGrow()

void Fraig_NodeVecGrow ( Fraig_NodeVec_t * p, int nCapMin )

extern

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;
}

Here is the caller graph for this function:

Fraig_NodeVecPop()

Fraig_Node_t * Fraig_NodeVecPop ( Fraig_NodeVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 331 of file fraigVec.c.

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

Fraig_NodeVecPush()

void Fraig_NodeVecPush ( Fraig_NodeVec_t * p, Fraig_Node_t * Entry )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeVecPushOrder()

void Fraig_NodeVecPushOrder ( Fraig_NodeVec_t * p, Fraig_Node_t * pNode )

extern

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;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeVecPushOrderByLevel()

void Fraig_NodeVecPushOrderByLevel ( Fraig_NodeVec_t * p, Fraig_Node_t * pNode )

extern

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;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeVecPushUnique()

int Fraig_NodeVecPushUnique ( Fraig_NodeVec_t * p, Fraig_Node_t * Entry )

extern

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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_NodeVecPushUniqueOrder()

int Fraig_NodeVecPushUniqueOrder ( Fraig_NodeVec_t * p, Fraig_Node_t * pNode )

extern

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;
}

Here is the call graph for this function:

Fraig_NodeVecPushUniqueOrderByLevel()

int Fraig_NodeVecPushUniqueOrderByLevel ( Fraig_NodeVec_t * p, Fraig_Node_t * pNode )

extern

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;
}

Here is the call graph for this function:

Fraig_NodeVecReadArray()

Fraig_Node_t ** Fraig_NodeVecReadArray ( Fraig_NodeVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file fraigVec.c.

{
    return p->pArray;
}

Fraig_NodeVecReadEntry()

Fraig_Node_t * Fraig_NodeVecReadEntry ( Fraig_NodeVec_t * p, int i )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 387 of file fraigVec.c.

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

Fraig_NodeVecReadSize()

int Fraig_NodeVecReadSize ( Fraig_NodeVec_t * p )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file fraigVec.c.

{
    return p->nSize;
}

Fraig_NodeVecRemove()

void Fraig_NodeVecRemove ( Fraig_NodeVec_t * p, Fraig_Node_t * Entry )

extern

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--;
}

Fraig_NodeVecShrink()

void Fraig_NodeVecShrink ( Fraig_NodeVec_t * p, int nSizeNew )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 156 of file fraigVec.c.

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

Fraig_NodeVecSortByLevel()

void Fraig_NodeVecSortByLevel ( Fraig_NodeVec_t * p, int fIncreasing )

extern

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, (size_t)p->nSize, sizeof(Fraig_Node_t *), 
                (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsIncreasing );
    else 
        qsort( (void *)p->pArray, (size_t)p->nSize, sizeof(Fraig_Node_t *), 
                (int (*)(const void *, const void *)) Fraig_NodeVecCompareLevelsDecreasing );
}

Here is the call graph for this function:

Fraig_NodeVecSortByNumber()

void Fraig_NodeVecSortByNumber ( Fraig_NodeVec_t * p )

extern

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

Synopsis [Sorting the entries by their integer value.]

Description []

SideEffects []

SeeAlso []

Definition at line 522 of file fraigVec.c.

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

Here is the call graph for this function:

Fraig_NodeVecWriteEntry()

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

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file fraigVec.c.

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

Fraig_ParamsSetDefault()

void Fraig_ParamsSetDefault ( Fraig_Params_t * pParams )

extern

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
}

Here is the call graph for this function:

Here is the caller graph for this function:

Fraig_ParamsSetDefaultFull()

void Fraig_ParamsSetDefaultFull ( Fraig_Params_t * pParams )

extern

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
}

Here is the call graph for this function:

Prove_ParamsSetDefault()

void Prove_ParamsSetDefault ( Prove_Params_t * pParams )

extern

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
}

Here is the call graph for this function:

Here is the caller graph for this function: