ivyFraig.c File Reference

#include <math.h>
#include "sat/bsat/satSolver.h"
#include "misc/extra/extra.h"
#include "ivy.h"
#include "aig/aig/aig.h"

Include dependency graph for ivyFraig.c:

Go to the source code of this file.

Classes
struct	Ivy_FraigList_t_
struct	Ivy_FraigSim_t_
struct	Ivy_FraigMan_t_
struct	Prove_ParamsStruct_t_

Macros
#define	Ivy_FraigForEachEquivClass(pList, pEnt)
#define	Ivy_FraigForEachEquivClassSafe(pList, pEnt, pEnt2)
#define	Ivy_FraigForEachClassNode(pClass, pEnt)
#define	Ivy_FraigForEachBinNode(pBin, pEnt)

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Ivy_FraigMan_t_	Ivy_FraigMan_t
	DECLARATIONS ///.
typedef struct Ivy_FraigSim_t_	Ivy_FraigSim_t
typedef struct Ivy_FraigList_t_	Ivy_FraigList_t
typedef struct Prove_ParamsStruct_t_	Prove_Params_t

Functions
void	Ivy_FraigParamsDefault (Ivy_FraigParams_t *pParams)
	FUNCTION DEFINITIONS ///.
int	Ivy_FraigProve (Ivy_Man_t **ppManAig, void *pPars)
Ivy_Man_t *	Ivy_FraigPerform (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
Ivy_Man_t *	Ivy_FraigMiter (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
void	Ivy_NodeAssignRandom (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
void	Ivy_NodeAssignConst (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, int fConst1)
void	Ivy_FraigAssignRandom (Ivy_FraigMan_t *p)
void	Ivy_FraigAssignDist1 (Ivy_FraigMan_t *p, unsigned *pPat)
int	Ivy_NodeHasZeroSim (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
void	Ivy_NodeComplementSim (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
int	Ivy_NodeCompareSims (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
void	Ivy_NodeSimulateSim (Ivy_FraigMan_t *p, Ivy_FraigSim_t *pSims)
void	Ivy_NodeSimulate (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
unsigned	Ivy_NodeHash (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
void	Ivy_FraigSimulateOne (Ivy_FraigMan_t *p)
void	Ivy_FraigSimulateOneSim (Ivy_FraigMan_t *p)
void	Ivy_NodeAddToClass (Ivy_Obj_t *pClass, Ivy_Obj_t *pObj)
void	Ivy_FraigAddClass (Ivy_FraigList_t *pList, Ivy_Obj_t *pClass)
void	Ivy_FraigInsertClass (Ivy_FraigList_t *pList, Ivy_Obj_t *pBase, Ivy_Obj_t *pClass)
void	Ivy_FraigRemoveClass (Ivy_FraigList_t *pList, Ivy_Obj_t *pClass)
int	Ivy_FraigCountPairsClasses (Ivy_FraigMan_t *p)
void	Ivy_FraigCreateClasses (Ivy_FraigMan_t *p)
int	Ivy_FraigRefineClass_rec (Ivy_FraigMan_t *p, Ivy_Obj_t *pClass)
void	Ivy_FraigCheckOutputSimsSavePattern (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
int	Ivy_FraigCheckOutputSims (Ivy_FraigMan_t *p)
int	Ivy_FraigRefineClasses (Ivy_FraigMan_t *p)
void	Ivy_FraigPrintClass (Ivy_Obj_t *pClass)
int	Ivy_FraigCountClassNodes (Ivy_Obj_t *pClass)
void	Ivy_FraigPrintSimClasses (Ivy_FraigMan_t *p)
void	Ivy_FraigSavePattern0 (Ivy_FraigMan_t *p)
void	Ivy_FraigSavePattern1 (Ivy_FraigMan_t *p)
void	Ivy_FraigSavePattern (Ivy_FraigMan_t *p)
void	Ivy_FraigSavePattern2 (Ivy_FraigMan_t *p)
void	Ivy_FraigSavePattern3 (Ivy_FraigMan_t *p)
void	Ivy_FraigCleanPatScores (Ivy_FraigMan_t *p)
int	Ivy_FraigSelectBestPat (Ivy_FraigMan_t *p)
void	Ivy_FraigResimulate (Ivy_FraigMan_t *p)
void	Ivy_FraigPrintActivity (Ivy_FraigMan_t *p)
void	Ivy_FraigAddClausesMux (Ivy_FraigMan_t *p, Ivy_Obj_t *pNode)
void	Ivy_FraigAddClausesSuper (Ivy_FraigMan_t *p, Ivy_Obj_t *pNode, Vec_Ptr_t *vSuper)
void	Ivy_FraigCollectSuper_rec (Ivy_Obj_t *pObj, Vec_Ptr_t *vSuper, int fFirst, int fUseMuxes)
Vec_Ptr_t *	Ivy_FraigCollectSuper (Ivy_Obj_t *pObj, int fUseMuxes)
void	Ivy_FraigObjAddToFrontier (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, Vec_Ptr_t *vFrontier)
int	Ivy_FraigSetActivityFactors_rec (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj, int LevelMin, int LevelMax)
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void	Ivy_FraigExtractCone_rec (Ivy_Man_t *p, Ivy_Obj_t *pNode, Vec_Int_t *vLeaves, Vec_Int_t *vNodes)
Aig_Man_t *	Ivy_FraigExtractCone (Ivy_Man_t *p, Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2, Vec_Int_t *vLeaves)

Macro Definition Documentation

Ivy_FraigForEachBinNode

#define Ivy_FraigForEachBinNode	(		pBin,
			pEnt )

Value:

    for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = Ivy_ObjNodeHashNext(pEnt) )

Definition at line 181 of file ivyFraig.c.

#define Ivy_FraigForEachBinNode( pBin, pEnt )                     \
    for ( pEnt = pBin;                                            \
          pEnt;                                                   \
          pEnt = Ivy_ObjNodeHashNext(pEnt) )

Ivy_FraigForEachClassNode

#define Ivy_FraigForEachClassNode	(		pClass,
			pEnt )

Value:

    for ( pEnt = pClass;                                          \
          pEnt;                                                   \
          pEnt = Ivy_ObjClassNodeNext(pEnt) )

Definition at line 176 of file ivyFraig.c.

#define Ivy_FraigForEachClassNode( pClass, pEnt )                 \
    for ( pEnt = pClass;                                          \
          pEnt;                                                   \
          pEnt = Ivy_ObjClassNodeNext(pEnt) )

Ivy_FraigForEachEquivClass

#define Ivy_FraigForEachEquivClass	(		pList,
			pEnt )

Value:

    for ( pEnt = pList;                                           \
          pEnt;                                                   \
          pEnt = Ivy_ObjEquivListNext(pEnt) )

Definition at line 165 of file ivyFraig.c.

#define Ivy_FraigForEachEquivClass( pList, pEnt )                 \
    for ( pEnt = pList;                                           \
          pEnt;                                                   \
          pEnt = Ivy_ObjEquivListNext(pEnt) )

Ivy_FraigForEachEquivClassSafe

#define Ivy_FraigForEachEquivClassSafe	(		pList,
			pEnt,
			pEnt2 )

Value:

    for ( pEnt = pList,                                           \
          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL;         \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )

Definition at line 169 of file ivyFraig.c.

#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 )      \
    for ( pEnt = pList,                                           \
          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL;         \
          pEnt;                                                   \
          pEnt = pEnt2,                                           \
          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )

Typedef Documentation

Ivy_FraigList_t

typedef struct Ivy_FraigList_t_ Ivy_FraigList_t

Definition at line 35 of file ivyFraig.c.

Ivy_FraigMan_t

typedef typedefABC_NAMESPACE_IMPL_START struct Ivy_FraigMan_t_ Ivy_FraigMan_t

DECLARATIONS ///.

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

FileName [ivyFraig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Functional reduction of AIGs]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id

ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Definition at line 33 of file ivyFraig.c.

Ivy_FraigSim_t

typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t

Definition at line 34 of file ivyFraig.c.

Prove_Params_t

typedef struct Prove_ParamsStruct_t_ Prove_Params_t

Definition at line 108 of file ivyFraig.c.

Function Documentation

Ivy_FraigAddClass()

void Ivy_FraigAddClass	(	Ivy_FraigList_t *	pList,
		Ivy_Obj_t *	pClass )

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

Synopsis [Adds equivalence class to the list of classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1067 of file ivyFraig.c.

{
    if ( pList->pHead == NULL )
    {
        pList->pHead = pClass;
        pList->pTail = pClass;
        Ivy_ObjSetEquivListPrev( pClass, NULL );
        Ivy_ObjSetEquivListNext( pClass, NULL ); 
    }
    else
    {
        Ivy_ObjSetEquivListNext( pList->pTail, pClass ); 
        Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
        Ivy_ObjSetEquivListNext( pClass, NULL ); 
        pList->pTail = pClass;
    }
    pList->nItems++;
}

Here is the caller graph for this function:

Ivy_FraigAddClausesMux()

void Ivy_FraigAddClausesMux	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pNode )

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 2352 of file ivyFraig.c.

{
    Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
 
    assert( !Ivy_IsComplement( pNode ) );
    assert( Ivy_ObjIsMuxType( pNode ) );
    // get nodes (I = if, T = then, E = else)
    pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
    // get the variable numbers
    VarF = Ivy_ObjSatNum(pNode);
    VarI = Ivy_ObjSatNum(pNodeI);
    VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
    VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
    // get the complementation flags
    fCompT = Ivy_IsComplement(pNodeT);
    fCompE = Ivy_IsComplement(pNodeE);
 
    // f = ITE(i, t, e)
 
    // i' + t' + f
    // i' + t  + f'
    // i  + e' + f
    // i  + e  + f'
 
    // create four clauses
    pLits[0] = toLitCond(VarI, 1);
    pLits[1] = toLitCond(VarT, 1^fCompT);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 1);
    pLits[1] = toLitCond(VarT, 0^fCompT);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 0);
    pLits[1] = toLitCond(VarE, 1^fCompE);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarI, 0);
    pLits[1] = toLitCond(VarE, 0^fCompE);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
 
    // two additional clauses
    // t' & e' -> f'
    // t  & e  -> f 
 
    // t  + e   + f'
    // t' + e'  + f 
 
    if ( VarT == VarE )
    {
//        assert( fCompT == !fCompE );
        return;
    }
 
    pLits[0] = toLitCond(VarT, 0^fCompT);
    pLits[1] = toLitCond(VarE, 0^fCompE);
    pLits[2] = toLitCond(VarF, 1);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
    pLits[0] = toLitCond(VarT, 1^fCompT);
    pLits[1] = toLitCond(VarE, 1^fCompE);
    pLits[2] = toLitCond(VarF, 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
    assert( RetValue );
}

Here is the call graph for this function:

Ivy_FraigAddClausesSuper()

void Ivy_FraigAddClausesSuper	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pNode,
		Vec_Ptr_t *	vSuper )

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

Synopsis [Addes clauses to the solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 2435 of file ivyFraig.c.

{
    Ivy_Obj_t * pFanin;
    int * pLits, nLits, RetValue, i;
    assert( !Ivy_IsComplement(pNode) );
    assert( Ivy_ObjIsNode( pNode ) );
    // create storage for literals
    nLits = Vec_PtrSize(vSuper) + 1;
    pLits = ABC_ALLOC( int, nLits );
    // suppose AND-gate is A & B = C
    // add !A => !C   or   A + !C
    Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i )
    {
        pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
        pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
    }
    // add A & B => C   or   !A + !B + C
    Vec_PtrForEachEntry( Ivy_Obj_t *, vSuper, pFanin, i )
        pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
    pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
    assert( RetValue );
    ABC_FREE( pLits );
}

Ivy_FraigAssignDist1()

void Ivy_FraigAssignDist1	(	Ivy_FraigMan_t *	p,
		unsigned *	pPat )

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

Synopsis [Assings distance-1 simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 741 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i, Limit;
    Ivy_ManForEachPi( p->pManAig, pObj, i )
    {
        Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
//        printf( "%d", Ivy_InfoHasBit(pPat, i) );
    }
//    printf( "\n" );
 
    Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
    for ( i = 0; i < Limit; i++ )
        Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigAssignRandom()

void Ivy_FraigAssignRandom

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 722 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    Ivy_ManForEachPi( p->pManAig, pObj, i )
        Ivy_NodeAssignRandom( p, pObj );
}

Here is the call graph for this function:

Ivy_FraigCheckOutputSims()

int Ivy_FraigCheckOutputSims

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Returns 1 if the one of the output is already non-constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 1349 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    // make sure the reference simulation pattern does not detect the bug
//    pObj = Ivy_ManPo( p->pManAig, 0 );
    Ivy_ManForEachPo( p->pManAig, pObj, i )
    {
        //assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
        // complement simulation info
//        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
//            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
        // check 
        if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
        {
            // create the counter-example from this pattern
            Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
            return 1;
        }
        // complement simulation info
//        if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
//            Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
    }
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigCheckOutputSimsSavePattern()

void Ivy_FraigCheckOutputSimsSavePattern	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Creates the counter-example from the successful pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 1307 of file ivyFraig.c.

{ 
    Ivy_FraigSim_t * pSims;
    int i, k, BestPat, * pModel;
    // find the word of the pattern
    pSims = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        if ( pSims->pData[i] )
            break;
    assert( i < p->nSimWords );
    // find the bit of the pattern
    for ( k = 0; k < 32; k++ )
        if ( pSims->pData[i] & (1 << k) )
            break;
    assert( k < 32 );
    // determine the best pattern
    BestPat = i * 32 + k;
    // fill in the counter-example data
    pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
    Ivy_ManForEachPi( p->pManAig, pObj, i )
    {
        pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
//        printf( "%d", pModel[i] );
    }
//    printf( "\n" );
    // set the model
    assert( p->pManFraig->pData == NULL );
    p->pManFraig->pData = pModel;
    return;
}

Here is the caller graph for this function:

Ivy_FraigCleanPatScores()

void Ivy_FraigCleanPatScores

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Cleans pattern scores.]

Description []

SideEffects []

SeeAlso []

Definition at line 1664 of file ivyFraig.c.

{
    int i, nLimit = p->nSimWords * 32;
    for ( i = 0; i < nLimit; i++ )
        p->pPatScores[i] = 0;
}

Here is the caller graph for this function:

Ivy_FraigCollectSuper()

Vec_Ptr_t * Ivy_FraigCollectSuper	(	Ivy_Obj_t *	pObj,
		int	fUseMuxes )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 2498 of file ivyFraig.c.

{
    Vec_Ptr_t * vSuper;
    assert( !Ivy_IsComplement(pObj) );
    assert( !Ivy_ObjIsPi(pObj) );
    vSuper = Vec_PtrAlloc( 4 );
    Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
    return vSuper;
}

Here is the call graph for this function:

Ivy_FraigCollectSuper_rec()

void Ivy_FraigCollectSuper_rec	(	Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vSuper,
		int	fFirst,
		int	fUseMuxes )

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

Synopsis [Collects the supergate.]

Description []

SideEffects []

SeeAlso []

Definition at line 2473 of file ivyFraig.c.

{
    // if the new node is complemented or a PI, another gate begins
    if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || 
         (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
    {
        Vec_PtrPushUnique( vSuper, pObj );
        return;
    }
    // go through the branches
    Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
    Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigCountClassNodes()

int Ivy_FraigCountClassNodes

(

Ivy_Obj_t *

pClass

)

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

Synopsis [Count the number of elements in the class.]

Description []

SideEffects []

SeeAlso []

Definition at line 1446 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int Counter = 0;
    Ivy_FraigForEachClassNode( pClass, pObj )
        Counter++;
    return Counter;
}

Here is the caller graph for this function:

Ivy_FraigCountPairsClasses()

int Ivy_FraigCountPairsClasses

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Count the number of pairs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1147 of file ivyFraig.c.

{
    Ivy_Obj_t * pClass, * pNode;
    int nPairs = 0, nNodes;
    return nPairs;
 
    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
    {
        nNodes = 0;
        Ivy_FraigForEachClassNode( pClass, pNode )
            nNodes++;
        nPairs += nNodes * (nNodes - 1) / 2;
    }
    return nPairs;
}

Ivy_FraigCreateClasses()

void Ivy_FraigCreateClasses

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Creates initial simulation classes.]

Description [Assumes that simulation info is assigned.]

SideEffects []

SeeAlso []

Definition at line 1174 of file ivyFraig.c.

{
    Ivy_Obj_t ** pTable;
    Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
    int i, nTableSize;
    unsigned Hash;
    pConst1 = Ivy_ManConst1(p->pManAig);
    // allocate the table
    nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
    pTable = ABC_ALLOC( Ivy_Obj_t *, nTableSize ); 
    memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
    // collect nodes into the table
    Ivy_ManForEachObj( p->pManAig, pObj, i )
    {
        if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
            continue;
        Hash = Ivy_NodeHash( p, pObj );
        if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
        {
            Ivy_NodeAddToClass( pConst1, pObj );
            continue;
        }
        // add the node to the table
        pBin = pTable[Hash % nTableSize];
        Ivy_FraigForEachBinNode( pBin, pEntry )
            if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
            {
                Ivy_NodeAddToClass( pEntry, pObj );
                break;
            }
        // check if the entry was added
        if ( pEntry )
            continue;
        Ivy_ObjSetNodeHashNext( pObj, pBin );
        pTable[Hash % nTableSize] = pObj;
    }
    // collect non-trivial classes
    assert( p->lClasses.pHead == NULL );
    Ivy_ManForEachObj( p->pManAig, pObj, i )
    {
        if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
            continue;
        Ivy_ObjSetNodeHashNext( pObj, NULL );
        if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
        {
            assert( Ivy_ObjClassNodeNext(pObj) == NULL );
            continue;
        }
        // recognize the head of the class
        if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
            continue;
        // clean the class representative and add it to the list
        Ivy_ObjSetClassNodeRepr( pObj, NULL );
        Ivy_FraigAddClass( &p->lClasses, pObj );
    }
    // free the table
    ABC_FREE( pTable );
}

Here is the call graph for this function:

Ivy_FraigExtractCone()

Aig_Man_t * Ivy_FraigExtractCone	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pObj1,
		Ivy_Obj_t *	pObj2,
		Vec_Int_t *	vLeaves )

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

Synopsis [Checks equivalence using BDDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 2867 of file ivyFraig.c.

{
    Aig_Man_t * pMan;
    Aig_Obj_t * pMiter;
    Vec_Int_t * vNodes;
    Ivy_Obj_t * pObjIvy;
    int i;
    // collect nodes
    vNodes  = Vec_IntAlloc( 100 );
    Ivy_ManConst1(p)->fMarkB = 1;
    Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes );
    Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes );
    Ivy_ManConst1(p)->fMarkB = 0;
    // create new manager
    pMan = Aig_ManStart( 1000 );
    Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan);
    Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i )
    {
        pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreateCi( pMan );
        pObjIvy->fMarkB = 0;
    }
    // duplicate internal nodes
    Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i )
    {
 
        pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) );
        pObjIvy->fMarkB = 0;
 
        pMiter = (Aig_Obj_t *)pObjIvy->pEquiv;
        assert( pMiter->fPhase == pObjIvy->fPhase );
    }
    // create the PO
    pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv );
    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
 
/*
printf( "Polarity = %d\n", pMiter->fPhase );
    if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) )
    {
        pMiter = Aig_NotCond( pMiter, 1 );
printf( "***************\n" );
    }
*/
    pMiter = Aig_ObjCreateCo( pMan, pMiter );
//printf( "Polarity = %d\n", pMiter->fPhase );
    Aig_ManCleanup( pMan );
    Vec_IntFree( vNodes );
    return pMan;
}

Here is the call graph for this function:

Ivy_FraigExtractCone_rec()

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START void Ivy_FraigExtractCone_rec	(	Ivy_Man_t *	p,
		Ivy_Obj_t *	pNode,
		Vec_Int_t *	vLeaves,
		Vec_Int_t *	vNodes )

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

Synopsis [Computes truth table of the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 2840 of file ivyFraig.c.

{
    if ( pNode->fMarkB )
        return;
    pNode->fMarkB = 1;
    if ( Ivy_ObjIsPi(pNode) )
    {
        Vec_IntPush( vLeaves, pNode->Id );
        return;
    }
    assert( Ivy_ObjIsAnd(pNode) );
    Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes );
    Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes );
    Vec_IntPush( vNodes, pNode->Id );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigInsertClass()

void Ivy_FraigInsertClass	(	Ivy_FraigList_t *	pList,
		Ivy_Obj_t *	pBase,
		Ivy_Obj_t *	pClass )

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

Synopsis [Updates the list of classes after base class has split.]

Description []

SideEffects []

SeeAlso []

Definition at line 1097 of file ivyFraig.c.

{
    Ivy_ObjSetEquivListPrev( pClass, pBase );
    Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); 
    if ( Ivy_ObjEquivListNext(pBase) )
        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
    Ivy_ObjSetEquivListNext( pBase, pClass ); 
    if ( pList->pTail == pBase )
        pList->pTail = pClass;
    pList->nItems++;
}

Here is the caller graph for this function:

Ivy_FraigMiter()

Ivy_Man_t * Ivy_FraigMiter	(	Ivy_Man_t *	pManAig,
		Ivy_FraigParams_t *	pParams )

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

Synopsis [Applies brute-force SAT to the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    Ivy_Man_t * pManAigNew;
    Ivy_Obj_t * pObj;
    int i;
    abctime clk;
clk = Abc_Clock();
    assert( Ivy_ManLatchNum(pManAig) == 0 );
    p = Ivy_FraigStartSimple( pManAig, pParams );
    // set global limits
    p->nBTLimitGlobal  = s_nBTLimitGlobal;
    p->nInsLimitGlobal = s_nInsLimitGlobal; 
    // duplicate internal nodes
    Ivy_ManForEachNode( p->pManAig, pObj, i )
        pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
    // try to prove each output of the miter
    Ivy_FraigMiterProve( p );
    // add the POs
    Ivy_ManForEachPo( p->pManAig, pObj, i )
        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
    // clean the new manager
    Ivy_ManForEachObj( p->pManFraig, pObj, i )
    {
        if ( Ivy_ObjFaninVec(pObj) )
            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
    }
    // remove dangling nodes 
    Ivy_ManCleanup( p->pManFraig );
    pManAigNew = p->pManFraig;
p->timeTotal = Abc_Clock() - clk;
 
//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
//ABC_PRT( "Time", p->timeTotal );
    Ivy_FraigStop( p );
    return pManAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigObjAddToFrontier()

void Ivy_FraigObjAddToFrontier	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj,
		Vec_Ptr_t *	vFrontier )

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 2519 of file ivyFraig.c.

{
    assert( !Ivy_IsComplement(pObj) );
    if ( Ivy_ObjSatNum(pObj) )
        return;
    assert( Ivy_ObjSatNum(pObj) == 0 );
    assert( Ivy_ObjFaninVec(pObj) == NULL );
    if ( Ivy_ObjIsConst1(pObj) )
        return;
//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
    Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
    if ( Ivy_ObjIsNode(pObj) )
        Vec_PtrPush( vFrontier, pObj );
}

Ivy_FraigParamsDefault()

void Ivy_FraigParamsDefault

(

Ivy_FraigParams_t *

pParams

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Sets the default solving parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 225 of file ivyFraig.c.

{
    memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
    pParams->nSimWords        =      32;  // the number of words in the simulation info
    pParams->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
    pParams->fPatScores       =       0;  // enables simulation pattern scoring
    pParams->MaxScore         =      25;  // max score after which resimulation is used
    pParams->fDoSparse        =       1;  // skips sparse functions
//    pParams->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
//    pParams->dActConeBumpMax  =     5.0;  // the largest bump of activity
    pParams->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
    pParams->dActConeBumpMax  =    10.0;  // the largest bump of activity
 
    pParams->nBTLimitNode     =     100;  // conflict limit at a node
    pParams->nBTLimitMiter    =  500000;  // conflict limit at an output
//    pParams->nBTLimitGlobal   =       0;  // conflict limit global
//    pParams->nInsLimitGlobal  =       0;  // inspection limit global
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigPerform()

Ivy_Man_t * Ivy_FraigPerform	(	Ivy_Man_t *	pManAig,
		Ivy_FraigParams_t *	pParams )

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

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 451 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    Ivy_Man_t * pManAigNew;
    abctime clk;
    if ( Ivy_ManNodeNum(pManAig) == 0 )
        return Ivy_ManDup(pManAig);
clk = Abc_Clock();
    assert( Ivy_ManLatchNum(pManAig) == 0 );
    p = Ivy_FraigStart( pManAig, pParams );
    Ivy_FraigSimulate( p );
    Ivy_FraigSweep( p );
    pManAigNew = p->pManFraig;
p->timeTotal = Abc_Clock() - clk;
    Ivy_FraigStop( p );
    return pManAigNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigPrintActivity()

void Ivy_FraigPrintActivity

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Prints variable activity.]

Description []

SideEffects []

SeeAlso []

Definition at line 2080 of file ivyFraig.c.

{
    int i;
    for ( i = 0; i < p->nSatVars; i++ )
        printf( "%d %d  ", i, (int)p->pSat->activity[i] );
    printf( "\n" );
}

Ivy_FraigPrintClass()

void Ivy_FraigPrintClass

(

Ivy_Obj_t *

pClass

)

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

Synopsis [Print the class.]

Description []

SideEffects []

SeeAlso []

Definition at line 1426 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    printf( "Class {" );
    Ivy_FraigForEachClassNode( pClass, pObj )
        printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
    printf( " }\n" );
}

Ivy_FraigPrintSimClasses()

void Ivy_FraigPrintSimClasses

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Prints simulation classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1466 of file ivyFraig.c.

{
    Ivy_Obj_t * pClass;
    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
    {
//        Ivy_FraigPrintClass( pClass );
        printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
    }
//    printf( "\n" );
}

Here is the call graph for this function:

Ivy_FraigProve()

int Ivy_FraigProve	(	Ivy_Man_t **	ppManAig,
		void *	pPars )

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

Synopsis [Performs combinational equivalence checking for the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file ivyFraig.c.

{
    Prove_Params_t * pParams = (Prove_Params_t *)pPars;
    Ivy_FraigParams_t Params, * pIvyParams = &Params; 
    Ivy_Man_t * pManAig, * pManTemp;
    int RetValue, nIter;
    abctime clk;//, Counter;
    ABC_INT64_T nSatConfs = 0, nSatInspects = 0;
 
    // start the network and parameters
    pManAig = *ppManAig;
    Ivy_FraigParamsDefault( pIvyParams );
    pIvyParams->fVerbose = pParams->fVerbose;
    pIvyParams->fProve = 1;
 
    if ( pParams->fVerbose )
    {
        printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
            pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
        printf( "Miter = %d (%3.1f).  Rwr = %d (%3.1f).  Fraig = %d (%3.1f).  Last = %d.\n", 
            pParams->nMiteringLimitStart,  pParams->nMiteringLimitMulti, 
            pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
            pParams->nFraigingLimitStart,  pParams->nFraigingLimitMulti, pParams->nMiteringLimitLast );
    }
 
    // if SAT only, solve without iteration
    if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
    {
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        *ppManAig = pManAig;
        return RetValue;
    }
 
    if ( Ivy_ManNodeNum(pManAig) < 500 )
    {
        // run the first mitering
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        if ( RetValue >= 0 )
        {
            *ppManAig = pManAig;
            return RetValue;
        }
    }
 
    // check the current resource limits
    RetValue = -1;
    for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
    {
        if ( pParams->fVerbose )
        {
            printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 
                 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 
                 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
            fflush( stdout );
        }
 
        // try rewriting
        if ( pParams->fUseRewriting )
        { // bug in Ivy_NodeFindCutsAll() when leaves are identical!
/*
            clk = Abc_Clock();
            Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
            pManAig = Ivy_ManRwsat( pManAig, 0 );  
            RetValue = Ivy_FraigMiterStatus( pManAig );
            Ivy_FraigMiterPrint( pManAig, "Rewriting  ", clk, pParams->fVerbose );
*/
        }
        if ( RetValue >= 0 )
            break;
 
        // catch the situation when ref pattern detects the bug
        RetValue = Ivy_FraigMiterStatus( pManAig );
        if ( RetValue >= 0 )
            break;
 
        // try fraiging followed by mitering
        if ( pParams->fUseFraiging )
        {
            clk = Abc_Clock();
            pIvyParams->nBTLimitNode  = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
            pIvyParams->nBTLimitMiter = 1 + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
            pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects );  Ivy_ManStop( pManTemp );
            RetValue = Ivy_FraigMiterStatus( pManAig );
            Ivy_FraigMiterPrint( pManAig, "Fraiging   ", clk, pParams->fVerbose );
        }
        if ( RetValue >= 0 )
            break;
 
        // add to the number of backtracks and inspects
        pParams->nTotalBacktracksMade += nSatConfs;
        pParams->nTotalInspectsMade   += nSatInspects;
        // check if global resource limit is reached
        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
        {
            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
            *ppManAig = pManAig;
            return -1;
        }
    }    
/*
    if ( RetValue < 0 )
    {
        if ( pParams->fVerbose )
        {
            printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
            fflush( stdout );
        }
        clk = Abc_Clock();
        pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
        if ( pParams->nTotalBacktrackLimit )
            s_nBTLimitGlobal  = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
        if ( pParams->nTotalInspectLimit )
            s_nInsLimitGlobal = pParams->nTotalInspectLimit -   pParams->nTotalInspectsMade;        
        pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams );  Ivy_ManStop( pManTemp );
        s_nBTLimitGlobal  = 0;
        s_nInsLimitGlobal = 0;        
        RetValue = Ivy_FraigMiterStatus( pManAig );
        Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
        // make sure that the sover never returns "undecided" when infinite resource limits are set
        if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
            pParams->nTotalBacktrackLimit == 0 )
        {
            extern void Prove_ParamsPrint( Prove_Params_t * pParams );
            Prove_ParamsPrint( pParams );
            printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
            exit(1);
        }
    }
*/
    // assign the model if it was proved by rewriting (const 1 miter)
    if ( RetValue == 0 && pManAig->pData == NULL )
    {
        pManAig->pData = ABC_ALLOC( int, Ivy_ManPiNum(pManAig) );
        memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
    }
    *ppManAig = pManAig;
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigRefineClass_rec()

int Ivy_FraigRefineClass_rec	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pClass )

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

Synopsis [Recursively refines the class after simulation.]

Description [Returns 1 if the class has changed.]

SideEffects []

SeeAlso []

Definition at line 1244 of file ivyFraig.c.

{
    Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
    int RetValue = 0;
    // check if there is refinement
    pListOld = pClass;
    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
    {
        if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
        {
            if ( p->pParams->fPatScores )
                Ivy_FraigAddToPatScores( p, pClass, pClassNew );
            break;
        }
        pListOld = pClassNew;
    }
    if ( pClassNew == NULL )
        return 0;
    // set representative of the new class
    Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
    // start the new list
    pListNew = pClassNew;
    // go through the remaining nodes and sort them into two groups:
    // (1) matches of the old node; (2) non-matches of the old node
    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
        if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
        {
            Ivy_ObjSetClassNodeNext( pListOld, pNode );
            pListOld = pNode;
        }
        else
        {
            Ivy_ObjSetClassNodeNext( pListNew, pNode );
            Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
            pListNew = pNode;
        }
    // finish both lists
    Ivy_ObjSetClassNodeNext( pListNew, NULL );
    Ivy_ObjSetClassNodeNext( pListOld, NULL );
    // update the list of classes
    Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
    // if the old class is trivial, remove it
    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
        Ivy_FraigRemoveClass( &p->lClasses, pClass );
    // if the new class is trivial, remove it; otherwise, try to refine it
    if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
        Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
    else
        RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
    return RetValue + 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigRefineClasses()

int Ivy_FraigRefineClasses

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Refines the classes after simulation.]

Description [Assumes that simulation info is assigned. Returns the number of classes refined.]

SideEffects [Large equivalence class of constant 0 may cause problems.]

SeeAlso []

Definition at line 1387 of file ivyFraig.c.

{
    Ivy_Obj_t * pClass, * pClass2;
    int RetValue, Counter = 0;
    abctime clk;
    // check if some outputs already became non-constant
    // this is a special case when computation can be stopped!!!
    if ( p->pParams->fProve )
        Ivy_FraigCheckOutputSims( p );
    if ( p->pManFraig->pData )
        return 0;
    // refine the classed
clk = Abc_Clock();
    Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
    {
        if ( pClass->fMarkA )
            continue;
        RetValue = Ivy_FraigRefineClass_rec( p, pClass );
        Counter += ( RetValue > 0 );
//if ( Ivy_ObjIsConst1(pClass) )
//printf( "%d ", RetValue );
//if ( Ivy_ObjIsConst1(pClass) )
//    p->time1 += Abc_Clock() - clk;
    }
p->timeRef += Abc_Clock() - clk;
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigRemoveClass()

void Ivy_FraigRemoveClass	(	Ivy_FraigList_t *	pList,
		Ivy_Obj_t *	pClass )

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

Synopsis [Removes equivalence class from the list of classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1120 of file ivyFraig.c.

{
    if ( pList->pHead == pClass )
        pList->pHead = Ivy_ObjEquivListNext(pClass);
    if ( pList->pTail == pClass )
        pList->pTail = Ivy_ObjEquivListPrev(pClass);
    if ( Ivy_ObjEquivListPrev(pClass) )
        Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); 
    if ( Ivy_ObjEquivListNext(pClass) )
        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
    Ivy_ObjSetEquivListNext( pClass, NULL ); 
    Ivy_ObjSetEquivListPrev( pClass, NULL );
    pClass->fMarkA = 0;
    pList->nItems--;
}

Here is the caller graph for this function:

Ivy_FraigResimulate()

void Ivy_FraigResimulate

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Resimulates fraiging manager after finding a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 1752 of file ivyFraig.c.

{
    int nChanges;
    Ivy_FraigAssignDist1( p, p->pPatWords );
    Ivy_FraigSimulateOne( p );
    if ( p->pParams->fPatScores )
        Ivy_FraigCleanPatScores( p );
    nChanges = Ivy_FraigRefineClasses( p );
    if ( p->pManFraig->pData )
        return;
    if ( nChanges < 1 )
        printf( "Error: A counter-example did not refine classes!\n" );
    assert( nChanges >= 1 );
//printf( "Refined classes! = %5d.   Changes = %4d.\n", p->lClasses.nItems, nChanges );
    if ( !p->pParams->fPatScores )
        return;
 
    // perform additional simulation using dist1 patterns derived from successful patterns
    while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
    {
        Ivy_FraigAssignDist1( p, p->pPatWords );
        Ivy_FraigSimulateOne( p );
        Ivy_FraigCleanPatScores( p );
        nChanges = Ivy_FraigRefineClasses( p );
        if ( p->pManFraig->pData )
            return;
//printf( "Refined class!!! = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
        if ( nChanges == 0 )
            break;
    }
}

Here is the call graph for this function:

Ivy_FraigSavePattern()

void Ivy_FraigSavePattern

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 1543 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Ivy_ManForEachPi( p->pManFraig, pObj, i )
//    Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
//        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
        if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
            Ivy_InfoSetBit( p->pPatWords, i );
//            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}

Here is the call graph for this function:

Ivy_FraigSavePattern0()

void Ivy_FraigSavePattern0

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Generated const 0 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 1488 of file ivyFraig.c.

{
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
}

Here is the call graph for this function:

Ivy_FraigSavePattern1()

void Ivy_FraigSavePattern1

(

Ivy_FraigMan_t *

p

)

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

Synopsis [[Generated const 1 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 1504 of file ivyFraig.c.

{
    memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
}

Here is the call graph for this function:

Ivy_FraigSavePattern2()

void Ivy_FraigSavePattern2

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 1567 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
//    Ivy_ManForEachPi( p->pManFraig, pObj, i )
    Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
//        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
        if ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True )
//            Ivy_InfoSetBit( p->pPatWords, i );
            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}

Here is the call graph for this function:

Ivy_FraigSavePattern3()

void Ivy_FraigSavePattern3

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 1591 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    for ( i = 0; i < p->nPatWords; i++ )
        p->pPatWords[i] = Ivy_ObjRandomSim();
    Vec_PtrForEachEntry( Ivy_Obj_t *, p->vPiVars, pObj, i )
//        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
        if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ sat_solver_var_value(p->pSat, Ivy_ObjSatNum(pObj)) )
            Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
}

Ivy_FraigSelectBestPat()

int Ivy_FraigSelectBestPat

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Selects the best pattern.]

Description [Returns 1 if such pattern is found.]

SideEffects []

SeeAlso []

Definition at line 1713 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    Ivy_Obj_t * pObj;
    int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
    for ( i = 1; i < nLimit; i++ )
    {
        if ( MaxScore < p->pPatScores[i] )
        {
            MaxScore = p->pPatScores[i];
            BestPat = i;
        }
    }
    if ( MaxScore == 0 )
        return 0;
//    if ( MaxScore > p->pParams->MaxScore )
//    printf( "Max score is %3d.  ", MaxScore );
    // copy the best pattern into the selected pattern
    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
    Ivy_ManForEachPi( p->pManAig, pObj, i )
    {
        pSims = Ivy_ObjSim(pObj);
        if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
            Ivy_InfoSetBit(p->pPatWords, i);
    }
    return MaxScore;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigSetActivityFactors_rec()

int Ivy_FraigSetActivityFactors_rec	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj,
		int	LevelMin,
		int	LevelMax )

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

Synopsis [Sets variable activities in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 2600 of file ivyFraig.c.

{
    Vec_Ptr_t * vFanins;
    Ivy_Obj_t * pFanin;
    int i, Counter = 0;
    assert( !Ivy_IsComplement(pObj) );
    assert( Ivy_ObjSatNum(pObj) );
    // skip visited variables
    if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
        return 0;
    Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
    // add the PI to the list
    if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
        return 0;
    // set the factor of this variable
    // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
    p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
    veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
    // explore the fanins
    vFanins = Ivy_ObjFaninVec( pObj );
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, i )
        Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
    return 1 + Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigSimulateOne()

void Ivy_FraigSimulateOne

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 990 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;
    int i;
    abctime clk;
clk = Abc_Clock();
    Ivy_ManForEachNode( p->pManAig, pObj, i )
    {
        Ivy_NodeSimulate( p, pObj );
/*
        if ( Ivy_ObjFraig(pObj) == NULL )
            printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
        else
            printf( "%3d %3d %2d %d  :  ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
        Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
        printf( "\n" );
*/
    }
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_FraigSimulateOneSim()

void Ivy_FraigSimulateOneSim

(

Ivy_FraigMan_t *

p

)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1023 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    abctime clk;
clk = Abc_Clock();
    for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
        Ivy_NodeSimulateSim( p, pSims );
p->timeSim += Abc_Clock() - clk;
p->nSimRounds++;
}

Here is the call graph for this function:

Ivy_NodeAddToClass()

void Ivy_NodeAddToClass	(	Ivy_Obj_t *	pClass,
		Ivy_Obj_t *	pObj )

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

Synopsis [Adds one node to the equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 1045 of file ivyFraig.c.

{
    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
        Ivy_ObjSetClassNodeNext( pClass, pObj );
    else
        Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
    Ivy_ObjSetClassNodeLast( pClass, pObj );
    Ivy_ObjSetClassNodeRepr( pObj, pClass );
    Ivy_ObjSetClassNodeNext( pObj, NULL );
}

Here is the caller graph for this function:

Ivy_NodeAssignConst()

void Ivy_NodeAssignConst	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj,
		int	fConst1 )

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 701 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    int i;
    assert( Ivy_ObjIsPi(pObj) );
    pSims = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
}

Here is the caller graph for this function:

Ivy_NodeAssignRandom()

void Ivy_NodeAssignRandom	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 680 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    int i;
    assert( Ivy_ObjIsPi(pObj) );
    pSims = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        pSims->pData[i] = Ivy_ObjRandomSim();
}

Here is the caller graph for this function:

Ivy_NodeCompareSims()

int Ivy_NodeCompareSims	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj0,
		Ivy_Obj_t *	pObj1 )

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 810 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims0, * pSims1;
    int i;
    pSims0 = Ivy_ObjSim(pObj0);
    pSims1 = Ivy_ObjSim(pObj1);
    for ( i = 0; i < p->nSimWords; i++ )
        if ( pSims0->pData[i] != pSims1->pData[i] )
            return 0;
    return 1;
}

Here is the caller graph for this function:

Ivy_NodeComplementSim()

void Ivy_NodeComplementSim	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 790 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    int i;
    pSims = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        pSims->pData[i] = ~pSims->pData[i];
}

Ivy_NodeHash()

unsigned Ivy_NodeHash	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Computes hash value using simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 951 of file ivyFraig.c.

{
    static int s_FPrimes[128] = { 
        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
    };
    Ivy_FraigSim_t * pSims;
    unsigned uHash;
    int i;
    assert( p->nSimWords <= 128 );
    uHash = 0;
    pSims  = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        uHash ^= pSims->pData[i] * s_FPrimes[i];
    return uHash;
}

Here is the caller graph for this function:

Ivy_NodeHasZeroSim()

int Ivy_NodeHasZeroSim	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 768 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims;
    int i;
    pSims = Ivy_ObjSim(pObj);
    for ( i = 0; i < p->nSimWords; i++ )
        if ( pSims->pData[i] )
            return 0;
    return 1;
}

Here is the caller graph for this function:

Ivy_NodeSimulate()

void Ivy_NodeSimulate	(	Ivy_FraigMan_t *	p,
		Ivy_Obj_t *	pObj )

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 888 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
    int fCompl, fCompl0, fCompl1, i;
    assert( !Ivy_IsComplement(pObj) );
    // get hold of the simulation information
    pSims  = Ivy_ObjSim(pObj);
    pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
    pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
    // get complemented attributes of the children using their random info
    fCompl  = pObj->fPhase;
    fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
    fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
    // simulate
    if ( fCompl0 && fCompl1 )
    {
        if ( fCompl )
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
        else
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
    }
    else if ( fCompl0 && !fCompl1 )
    {
        if ( fCompl )
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
        else
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
    }
    else if ( !fCompl0 && fCompl1 )
    {
        if ( fCompl )
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
        else
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
    }
    else // if ( !fCompl0 && !fCompl1 )
    {
        if ( fCompl )
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
        else
            for ( i = 0; i < p->nSimWords; i++ )
                pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
    }
}

Here is the caller graph for this function:

Ivy_NodeSimulateSim()

void Ivy_NodeSimulateSim	(	Ivy_FraigMan_t *	p,
		Ivy_FraigSim_t *	pSims )

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 833 of file ivyFraig.c.

{
    unsigned * pData, * pData0, * pData1;
    int i;
    pData  = pSims->pData;
    pData0 = pSims->pFanin0->pData;
    pData1 = pSims->pFanin1->pData;
    switch( pSims->Type )
    {
    case 0:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (pData0[i] & pData1[i]);
        break;
    case 1:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = ~(pData0[i] & pData1[i]);
        break;
    case 2:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (pData0[i] & ~pData1[i]);
        break;
    case 3:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (~pData0[i] | pData1[i]);
        break;
    case 4:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (~pData0[i] & pData1[i]);
        break;
    case 5:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (pData0[i] | ~pData1[i]);
        break;
    case 6:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = ~(pData0[i] | pData1[i]);
        break;
    case 7:
        for ( i = 0; i < p->nSimWords; i++ )
            pData[i] = (pData0[i] | pData1[i]);
        break;
    }
}

Here is the caller graph for this function: