ivyFraig.c File Reference

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

Go to the source code of this file.

Data Structures
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 ///. More...
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
static Ivy_FraigSim_t *	Ivy_ObjSim (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjClassNodeLast (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjClassNodeRepr (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjClassNodeNext (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjNodeHashNext (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjEquivListNext (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjEquivListPrev (Ivy_Obj_t *pObj)
static Ivy_Obj_t *	Ivy_ObjFraig (Ivy_Obj_t *pObj)
static int	Ivy_ObjSatNum (Ivy_Obj_t *pObj)
static Vec_Ptr_t *	Ivy_ObjFaninVec (Ivy_Obj_t *pObj)
static void	Ivy_ObjSetSim (Ivy_Obj_t *pObj, Ivy_FraigSim_t *pSim)
static void	Ivy_ObjSetClassNodeLast (Ivy_Obj_t *pObj, Ivy_Obj_t *pLast)
static void	Ivy_ObjSetClassNodeRepr (Ivy_Obj_t *pObj, Ivy_Obj_t *pRepr)
static void	Ivy_ObjSetClassNodeNext (Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
static void	Ivy_ObjSetNodeHashNext (Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
static void	Ivy_ObjSetEquivListNext (Ivy_Obj_t *pObj, Ivy_Obj_t *pNext)
static void	Ivy_ObjSetEquivListPrev (Ivy_Obj_t *pObj, Ivy_Obj_t *pPrev)
static void	Ivy_ObjSetFraig (Ivy_Obj_t *pObj, Ivy_Obj_t *pNode)
static void	Ivy_ObjSetSatNum (Ivy_Obj_t *pObj, int Num)
static void	Ivy_ObjSetFaninVec (Ivy_Obj_t *pObj, Vec_Ptr_t *vFanins)
static unsigned	Ivy_ObjRandomSim ()
static Ivy_FraigMan_t *	Ivy_FraigStart (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
static Ivy_FraigMan_t *	Ivy_FraigStartSimple (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams)
static Ivy_Man_t *	Ivy_FraigPerform_int (Ivy_Man_t *pManAig, Ivy_FraigParams_t *pParams, ABC_INT64_T nBTLimitGlobal, ABC_INT64_T nInsLimitGlobal, ABC_INT64_T *pnSatConfs, ABC_INT64_T *pnSatInspects)
static void	Ivy_FraigPrint (Ivy_FraigMan_t *p)
static void	Ivy_FraigStop (Ivy_FraigMan_t *p)
static void	Ivy_FraigSimulate (Ivy_FraigMan_t *p)
static void	Ivy_FraigSweep (Ivy_FraigMan_t *p)
static Ivy_Obj_t *	Ivy_FraigAnd (Ivy_FraigMan_t *p, Ivy_Obj_t *pObjOld)
static int	Ivy_FraigNodesAreEquiv (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
static int	Ivy_FraigNodeIsConst (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj)
static void	Ivy_FraigNodeAddToSolver (Ivy_FraigMan_t *p, Ivy_Obj_t *pObj0, Ivy_Obj_t *pObj1)
static int	Ivy_FraigSetActivityFactors (Ivy_FraigMan_t *p, Ivy_Obj_t *pOld, Ivy_Obj_t *pNew)
static void	Ivy_FraigAddToPatScores (Ivy_FraigMan_t *p, Ivy_Obj_t *pClass, Ivy_Obj_t *pClassNew)
static int	Ivy_FraigMiterStatus (Ivy_Man_t *pMan)
static void	Ivy_FraigMiterProve (Ivy_FraigMan_t *p)
static void	Ivy_FraigMiterPrint (Ivy_Man_t *pNtk, char *pString, abctime clk, int fVerbose)
static int *	Ivy_FraigCreateModel (Ivy_FraigMan_t *p)
static int	Ivy_FraigNodesAreEquivBdd (Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2)
static int	Ivy_FraigCheckCone (Ivy_FraigMan_t *pGlo, Ivy_Man_t *p, Ivy_Obj_t *pObj1, Ivy_Obj_t *pObj2, int nConfLimit)
void	Ivy_FraigParamsDefault (Ivy_FraigParams_t *pParams)
	FUNCTION DEFINITIONS ///. More...
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 DdNode *	Ivy_FraigNodesAreEquivBdd_int (DdManager *dd, DdNode *bFunc, Vec_Ptr_t *vFront, int Level)
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)

Variables
static ABC_INT64_T	s_nBTLimitGlobal = 0
static ABC_INT64_T	s_nInsLimitGlobal = 0

Macro Definition Documentation

#define Ivy_FraigForEachBinNode	(		pBin,
			pEnt
	)

Value:

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

Definition at line 181 of file ivyFraig.c.

#define Ivy_FraigForEachClassNode	(		pClass,
			pEnt
	)

Value:

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

Definition at line 176 of file ivyFraig.c.

#define Ivy_FraigForEachEquivClass	(		pList,
			pEnt
	)

Value:

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

Definition at line 165 of file ivyFraig.c.

#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.

Typedef Documentation

typedef struct Ivy_FraigList_t_ Ivy_FraigList_t

Definition at line 35 of file ivyFraig.c.

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.

typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t

Definition at line 34 of file ivyFraig.c.

typedef struct Prove_ParamsStruct_t_ Prove_Params_t

Definition at line 108 of file ivyFraig.c.

Function Documentation

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

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

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

void Ivy_FraigAddToPatScores ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pClass, Ivy_Obj_t *  pClassNew  )

static

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

Synopsis [Adds to pattern scores.]

Description []

SideEffects []

SeeAlso []

Definition at line 1682 of file ivyFraig.c.

{
    Ivy_FraigSim_t * pSims0, * pSims1;
    unsigned uDiff;
    int i, w;
    // get hold of the simulation information
    pSims0 = Ivy_ObjSim(pClass);
    pSims1 = Ivy_ObjSim(pClassNew);
    // iterate through the differences and record the score
    for ( w = 0; w < p->nSimWords; w++ )
    {
        uDiff = pSims0->pData[w] ^ pSims1->pData[w];
        if ( uDiff == 0 )
            continue;
        for ( i = 0; i < 32; i++ )
            if ( uDiff & ( 1 << i ) )
                p->pPatScores[w*32+i]++;
    }
}

Ivy_Obj_t * Ivy_FraigAnd ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pObjOld  )

static

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 2027 of file ivyFraig.c.

{ 
    Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
    int RetValue;
    // get the fraiged fanins
    pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
    pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
    // get the candidate fraig node
    pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
    // get representative of this class
    if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
         (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
    {
//        assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
//        assert( pObjNew != Ivy_Regular(pFanin0New) );
//        assert( pObjNew != Ivy_Regular(pFanin1New) );
        return pObjNew;
    }
    // get the fraiged representative
    pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
    // if the fraiged nodes are the same return
    if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
        return pObjNew;
    assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
//    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id );

    // they are different (the counter-example is in p->pPatWords)
    RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
    if ( RetValue == 1 )  // proved equivalent
    {
        // mark the class as proved
        if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
            Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
        return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
    }
    if ( RetValue == -1 ) // failed
        return pObjNew;
    // simulate the counter-example and return the new node
    Ivy_FraigResimulate( p );
    return pObjNew;
}

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

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

int Ivy_FraigCheckCone ( Ivy_FraigMan_t *  pGlo, Ivy_Man_t *  p, Ivy_Obj_t *  pObj1, Ivy_Obj_t *  pObj2, int  nConfLimit  )

static

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

Synopsis [Checks equivalence using BDDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 2924 of file ivyFraig.c.

{
    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
    Vec_Int_t * vLeaves;
    Aig_Man_t * pMan;
    Aig_Obj_t * pObj;
    int i, RetValue;
    vLeaves  = Vec_IntAlloc( 100 );
    pMan     = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
    RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 0, 0, 0, 1 ); 
    if ( RetValue == 0 )
    {
        int Counter = 0;
        memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords );
        Aig_ManForEachCi( pMan, pObj, i )
            if ( ((int *)pMan->pData)[i] )
            {
                int iObjIvy = Vec_IntEntry( vLeaves, i );
                assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) );
                Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 );
//printf( "%d ", iObjIvy );
Counter++;
            }
        assert( Counter > 0 );
    }
    Vec_IntFree( vLeaves );
    if ( RetValue == 1 )
        printf( "UNSAT\n" );
    else if ( RetValue == 0 )
        printf( "SAT\n" );
    else if ( RetValue == -1 )
        printf( "UNDEC\n" );

//    p->pModel = (int *)pMan->pData, pMan2->pData = NULL;
    Aig_ManStop( pMan );
    return RetValue;
}

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

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

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

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

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

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

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

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

int * Ivy_FraigCreateModel ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Generates the counter-example satisfying the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 1520 of file ivyFraig.c.

{
    int * pModel;
    Ivy_Obj_t * pObj;
    int i;
    pModel = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
    Ivy_ManForEachPi( p->pManFraig, pObj, i )
//        pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
        pModel[i] = ( p->pSat->model[Ivy_ObjSatNum(pObj)] == l_True );
    return pModel;
}

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

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

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

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

void Ivy_FraigMiterPrint ( Ivy_Man_t *  pNtk, char *  pString, abctime  clk, int  fVerbose  )

static

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

Synopsis [Prints the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 1796 of file ivyFraig.c.

{
    if ( !fVerbose )
        return;
    printf( "Nodes = %7d.  Levels = %4d.  ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
    ABC_PRT( pString, Abc_Clock() - clk );
}

void Ivy_FraigMiterProve ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Tries to prove each output of the miter until encountering a sat output.]

Description []

SideEffects []

SeeAlso []

Definition at line 1880 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj, * pObjNew;
    int i, RetValue;
    abctime clk = Abc_Clock();
    int fVerbose = 0;
    Ivy_ManForEachPo( p->pManAig, pObj, i )
    {
        if ( i && fVerbose )
        {
            ABC_PRT( "Time", Abc_Clock() -clk );
        }
        pObjNew = Ivy_ObjChild0Equiv(pObj);
        // check if the output is constant 1
        if ( pObjNew == p->pManFraig->pConst1 )
        {
            if ( fVerbose )
                printf( "Output %2d (out of %2d) is constant 1.  ", i, Ivy_ManPoNum(p->pManAig) );
            // assing constant 0 model
            p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
            memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
            break;
        }
        // check if the output is constant 0
        if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
        {
            if ( fVerbose )
                printf( "Output %2d (out of %2d) is already constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
            continue;
        }
        // check if the output can be constant 0
        if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
        {
            if ( fVerbose )
                printf( "Output %2d (out of %2d) cannot be constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
            // assing constant 0 model
            p->pManFraig->pData = ABC_ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
            memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
            break;
        }
/*
        // check the representative of this node
        pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
        if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
            printf( "Representative is not constant 1.\n" );
        else
            printf( "Representative is constant 1.\n" );
*/
        // try to prove the output constant 0
        RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
        if ( RetValue == 1 )  // proved equivalent
        {
            if ( fVerbose )
                printf( "Output %2d (out of %2d) was proved constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
            // set the constant miter
            Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
            continue;
        }
        if ( RetValue == -1 ) // failed
        {
            if ( fVerbose )
                printf( "Output %2d (out of %2d) has timed out at %d backtracks.  ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
            continue;
        }
        // proved satisfiable
        if ( fVerbose )
            printf( "Output %2d (out of %2d) was proved NOT a constant 0.  ", i, Ivy_ManPoNum(p->pManAig) );
        // create the model
        p->pManFraig->pData = Ivy_FraigCreateModel(p);
        break;
    }
    if ( fVerbose )
    {
        ABC_PRT( "Time", Abc_Clock() -clk );
    }
}

int Ivy_FraigMiterStatus ( Ivy_Man_t *  pMan )

static

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

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 1815 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj, * pObjNew;
    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
    if ( pMan->pData )
        return 0;
    Ivy_ManForEachPo( pMan, pObj, i )
    {
        pObjNew = Ivy_ObjChild0(pObj);
        // check if the output is constant 1
        if ( pObjNew == pMan->pConst1 )
        {
            CountNonConst0++;
            continue;
        }
        // check if the output is constant 0
        if ( pObjNew == Ivy_Not(pMan->pConst1) )
        {
            CountConst0++;
            continue;
        }
/*
        // check if the output is a primary input
        if ( Ivy_ObjIsPi(Ivy_Regular(pObjNew)) )
        {
            CountNonConst0++;
            continue;
        }
*/
        // check if the output can be constant 0
        if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
        {
            CountNonConst0++;
            continue;
        }
        CountUndecided++;
    }
/*
    if ( p->pParams->fVerbose )
    {
        printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
        printf( "Const0 = %d.  ", CountConst0 );
        printf( "NonConst0 = %d.  ", CountNonConst0 );
        printf( "Undecided = %d.  ", CountUndecided );
        printf( "\n" );
    }
*/
    if ( CountNonConst0 )
        return 0;
    if ( CountUndecided )
        return -1;
    return 1;
}

void Ivy_FraigNodeAddToSolver ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pOld, Ivy_Obj_t *  pNew  )

static

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

Synopsis [Updates the solver clause database.]

Description []

SideEffects []

SeeAlso []

Definition at line 2545 of file ivyFraig.c.

{ 
    Vec_Ptr_t * vFrontier, * vFanins;
    Ivy_Obj_t * pNode, * pFanin;
    int i, k, fUseMuxes = 1;
    assert( pOld || pNew );
    // quit if CNF is ready
    if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
        return;
    // start the frontier
    vFrontier = Vec_PtrAlloc( 100 );
    if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
    if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
    // explore nodes in the frontier
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFrontier, pNode, i )
    {
        // create the supergate
        assert( Ivy_ObjSatNum(pNode) );
        assert( Ivy_ObjFaninVec(pNode) == NULL );
        if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
        {
            vFanins = Vec_PtrAlloc( 4 );
            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
            Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k )
                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
            Ivy_FraigAddClausesMux( p, pNode );
        }
        else
        {
            vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
            Vec_PtrForEachEntry( Ivy_Obj_t *, vFanins, pFanin, k )
                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
            Ivy_FraigAddClausesSuper( p, pNode, vFanins );
        }
        assert( Vec_PtrSize(vFanins) > 1 );
        Ivy_ObjSetFaninVec( pNode, vFanins );
    }
    Vec_PtrFree( vFrontier );
    sat_solver_simplify( p->pSat );
}

int Ivy_FraigNodeIsConst ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pNew  )

static

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

Synopsis [Runs equivalence test for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 2266 of file ivyFraig.c.

{
    int pLits[2], RetValue1;
    abctime clk;
    int RetValue;

    // make sure the nodes are not complemented
    assert( !Ivy_IsComplement(pNew) );
    assert( pNew != p->pManFraig->pConst1 );
    p->nSatCalls++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        sat_solver_setnvars( p->pSat, 1000 );
        p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
        p->nSatVars = 1;
        // var 0 is reserved for const1 node - add the clause
//        pLits[0] = toLit( 0 );
//        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

    // if the nodes do not have SAT variables, allocate them
    Ivy_FraigNodeAddToSolver( p, NULL, pNew );

    // prepare variable activity
    Ivy_FraigSetActivityFactors( p, NULL, pNew ); 

    // solve under assumptions
clk = Abc_Clock();
    pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
        (ABC_INT64_T)p->pParams->nBTLimitMiter, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        if ( p->pPatWords )
            Ivy_FraigSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
/*
        if ( p->pParams->nBTLimitMiter > 1000 )
        {
            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter );
            if ( RetValue != -1 )
                return RetValue;
        }
*/
        // mark the node as the failed node
        pNew->fFailTfo = 1;
        p->nSatFailsReal++;
        return -1;
    }

    // return SAT proof
    p->nSatProof++;
    return 1;
}

int Ivy_FraigNodesAreEquiv ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pOld, Ivy_Obj_t *  pNew  )

static

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

Synopsis [Runs equivalence test for the two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 2099 of file ivyFraig.c.

{
    int pLits[4], RetValue, RetValue1, nBTLimit;
    abctime clk; //, clk2 = Abc_Clock();

    // make sure the nodes are not complemented
    assert( !Ivy_IsComplement(pNew) );
    assert( !Ivy_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
    nBTLimit = p->pParams->nBTLimitNode;
    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
    {
        p->nSatFails++;
        // fail immediately
//        return -1;
        if ( nBTLimit <= 10 )
            return -1;
        nBTLimit = (int)pow(nBTLimit, 0.7);
    }
    p->nSatCalls++;

    // make sure the solver is allocated and has enough variables
    if ( p->pSat == NULL )
    {
        p->pSat = sat_solver_new();
        sat_solver_setnvars( p->pSat, 1000 );
        p->pSat->factors = ABC_CALLOC( double, p->pSat->cap );
        p->nSatVars = 1;
        // var 0 is reserved for const1 node - add the clause
//        pLits[0] = toLit( 0 );
//        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
    }

    // if the nodes do not have SAT variables, allocate them
    Ivy_FraigNodeAddToSolver( p, pOld, pNew );

    // prepare variable activity
    Ivy_FraigSetActivityFactors( p, pOld, pNew ); 

    // solve under assumptions
    // A = 1; B = 0     OR     A = 1; B = 1 
clk = Abc_Clock();
    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        // continue solving the other implication
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Ivy_FraigSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
/*
        if ( nBTLimit > 1000 )
        {
            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
            if ( RetValue != -1 )
                return RetValue;
        }
*/
        // mark the node as the failed node
        if ( pOld != p->pManFraig->pConst1 ) 
            pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
        p->nSatFailsReal++;
        return -1;
    }

    // if the old node was constant 0, we already know the answer
    if ( pOld == p->pManFraig->pConst1 )
    {
        p->nSatProof++;
        return 1;
    }

    // solve under assumptions
    // A = 0; B = 1     OR     A = 0; B = 0 
clk = Abc_Clock();
    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, 
        p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += Abc_Clock() - clk;
    if ( RetValue1 == l_False )
    {
p->timeSatUnsat += Abc_Clock() - clk;
        pLits[0] = lit_neg( pLits[0] );
        pLits[1] = lit_neg( pLits[1] );
        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
        assert( RetValue );
        p->nSatCallsUnsat++;
    }
    else if ( RetValue1 == l_True )
    {
p->timeSatSat += Abc_Clock() - clk;
        Ivy_FraigSavePattern( p );
        p->nSatCallsSat++;
        return 0;
    }
    else // if ( RetValue1 == l_Undef )
    {
p->timeSatFail += Abc_Clock() - clk;
/*
        if ( nBTLimit > 1000 )
        {
            RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
            if ( RetValue != -1 )
                return RetValue;
        }
*/
        // mark the node as the failed node
        pOld->fFailTfo = 1;
        pNew->fFailTfo = 1;
        p->nSatFailsReal++;
        return -1;
    }
/*
    // check BDD proof
    {
        int RetVal;
        ABC_PRT( "Sat", Abc_Clock() - clk2 );
        clk2 = Abc_Clock();
        RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
//        printf( "%d ", RetVal );
        assert( RetVal );
        ABC_PRT( "Bdd", Abc_Clock() - clk2 );
        printf( "\n" );
    }
*/
    // return SAT proof
    p->nSatProof++;
    return 1;
}

int Ivy_FraigNodesAreEquivBdd ( Ivy_Obj_t *  pObj1, Ivy_Obj_t *  pObj2  )

static

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

Synopsis [Checks equivalence using BDDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 2769 of file ivyFraig.c.

{
    static DdManager * dd = NULL;
    DdNode * bFunc, * bTemp;
    Vec_Ptr_t * vFront;
    Ivy_Obj_t * pObj;
    int i, RetValue, Iter, Level;
    // start the manager
    if ( dd == NULL )
        dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    // create front
    vFront = Vec_PtrAlloc( 100 );
    Vec_PtrPush( vFront, pObj1 );
    Vec_PtrPush( vFront, pObj2 );
    // get the function
    bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) );  Cudd_Ref( bFunc );
    bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
    // try running BDDs
    for ( Iter = 0; ; Iter++ )
    {
        // find max level
        Level = 0;
        Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
            if ( Level < (int)pObj->Level )
                Level = (int)pObj->Level;
        if ( Level == 0 )
            break;            
        bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
        if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
            {printf( "%d", Iter ); break;}
        if ( Cudd_DagSize(bFunc) > 1000 )
            {printf( "b" ); break;}
        if ( dd->size > 120 )
            {printf( "s" ); break;}
        if ( Iter > 50 )
            {printf( "i" ); break;}
    }
    if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
        RetValue = 1;
    else if ( Level == 0 ) // sat
        RetValue = 0;
    else 
        RetValue = -1; // spaceout/timeout
    Cudd_RecursiveDeref( dd, bFunc );
    Vec_PtrFree( vFront );
    return RetValue;
}

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START DdNode* Ivy_FraigNodesAreEquivBdd_int	(	DdManager *	dd,
		DdNode *	bFunc,
		Vec_Ptr_t *	vFront,
		int	Level
	)

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

Synopsis [Checks equivalence using BDDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 2678 of file ivyFraig.c.

{
    DdNode ** pFuncs;
    DdNode * bFuncNew;
    Vec_Ptr_t * vTemp;
    Ivy_Obj_t * pObj, * pFanin;
    int i, NewSize;
    // create new frontier
    vTemp = Vec_PtrAlloc( 100 );
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
    {
        if ( (int)pObj->Level != Level )
        {
            pObj->fMarkB = 1;
            pObj->TravId = Vec_PtrSize(vTemp);
            Vec_PtrPush( vTemp, pObj );
            continue;
        }

        pFanin = Ivy_ObjFanin0(pObj);
        if ( pFanin->fMarkB == 0 )
        {
            pFanin->fMarkB = 1;
            pFanin->TravId = Vec_PtrSize(vTemp);
            Vec_PtrPush( vTemp, pFanin );
        }

        pFanin = Ivy_ObjFanin1(pObj);
        if ( pFanin->fMarkB == 0 )
        {
            pFanin->fMarkB = 1;
            pFanin->TravId = Vec_PtrSize(vTemp);
            Vec_PtrPush( vTemp, pFanin );
        }
    }
    // collect the permutation
    NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
    pFuncs = ABC_ALLOC( DdNode *, NewSize );
    Vec_PtrForEachEntry( Ivy_Obj_t *, vFront, pObj, i )
    {
        if ( (int)pObj->Level != Level )
            pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
        else
            pFuncs[i] = Cudd_bddAnd( dd, 
                Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
                Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
        Cudd_Ref( pFuncs[i] );
    }
    // add the remaining vars
    assert( NewSize == dd->size );
    for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
    {
        pFuncs[i] = Cudd_bddIthVar( dd, i );
        Cudd_Ref( pFuncs[i] );
    }

    // create new
    bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
    // clean trav Id
    Vec_PtrForEachEntry( Ivy_Obj_t *, vTemp, pObj, i )
    {
        pObj->fMarkB = 0;
        pObj->TravId = 0;
    }
    // deref
    for ( i = 0; i < dd->size; i++ )
        Cudd_RecursiveDeref( dd, pFuncs[i] );
    ABC_FREE( pFuncs );

    ABC_FREE( vFront->pArray );
    *vFront = *vTemp;

    vTemp->nCap = vTemp->nSize = 0;
    vTemp->pArray = NULL;
    Vec_PtrFree( vTemp );

    Cudd_Deref( bFuncNew );
    return bFuncNew;
}

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

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
}

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

Ivy_Man_t * Ivy_FraigPerform_int ( Ivy_Man_t *  pManAig, Ivy_FraigParams_t *  pParams, ABC_INT64_T  nBTLimitGlobal, ABC_INT64_T  nInsLimitGlobal, ABC_INT64_T *  pnSatConfs, ABC_INT64_T *  pnSatInspects  )

static

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

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 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 );
    // set global limits
    p->nBTLimitGlobal  = nBTLimitGlobal;
    p->nInsLimitGlobal = nInsLimitGlobal; 
    
    Ivy_FraigSimulate( p );
    Ivy_FraigSweep( p );
    pManAigNew = p->pManFraig;
p->timeTotal = Abc_Clock() - clk;
    if ( pnSatConfs )
        *pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
    if ( pnSatInspects )
        *pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
    Ivy_FraigStop( p );
    return pManAigNew;
}

void Ivy_FraigPrint ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Prints stats for the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 644 of file ivyFraig.c.

{
    double nMemory;
    nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
    printf( "SimWords = %d. Rounds = %d. Mem = %0.2f MB.  ", p->nSimWords, p->nSimRounds, nMemory );
    printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
//    printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
    printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
        Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
    if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
    ABC_PRT( "AIG simulation  ", p->timeSim  );
    ABC_PRT( "AIG traversal   ", p->timeTrav  );
    ABC_PRT( "SAT solving     ", p->timeSat   );
    ABC_PRT( "    Unsat       ", p->timeSatUnsat );
    ABC_PRT( "    Sat         ", p->timeSatSat   );
    ABC_PRT( "    Fail        ", p->timeSatFail  );
    ABC_PRT( "Class refining  ", p->timeRef   );
    ABC_PRT( "TOTAL RUNTIME   ", p->timeTotal );
    if ( p->time1 ) { ABC_PRT( "time1           ", p->time1 ); }
}

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, p->pSat->activity[i] );
    printf( "\n" );
}

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

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

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

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

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

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

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

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

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

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

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

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

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

int Ivy_FraigSetActivityFactors ( Ivy_FraigMan_t *  p, Ivy_Obj_t *  pOld, Ivy_Obj_t *  pNew  )

static

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

Synopsis [Sets variable activities in the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 2636 of file ivyFraig.c.

{
    int LevelMin, LevelMax;
    abctime clk;
    assert( pOld || pNew );
clk = Abc_Clock(); 
    // reset the active variables
    veci_resize(&p->pSat->act_vars, 0);
    // prepare for traversal
    Ivy_ManIncrementTravId( p->pManFraig );
    // determine the min and max level to visit
    assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
    LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
    LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
    // traverse
    if ( pOld && !Ivy_ObjIsConst1(pOld) )
        Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
    if ( pNew && !Ivy_ObjIsConst1(pNew) )
        Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Ivy_FraigPrintActivity( p );
p->timeTrav += Abc_Clock() - clk;
    return 1;
}

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

void Ivy_FraigSimulate ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Performs simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1615 of file ivyFraig.c.

{
    int nChanges, nClasses;
    // start the classes
    Ivy_FraigAssignRandom( p );
    Ivy_FraigSimulateOne( p );
    Ivy_FraigCreateClasses( p );
//printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
    // refine classes by walking 0/1 patterns
    Ivy_FraigSavePattern0( p );
    Ivy_FraigAssignDist1( p, p->pPatWords );
    Ivy_FraigSimulateOne( p );
    nChanges = Ivy_FraigRefineClasses( p );
    if ( p->pManFraig->pData )
        return;
//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
    Ivy_FraigSavePattern1( p );
    Ivy_FraigAssignDist1( p, p->pPatWords );
    Ivy_FraigSimulateOne( p );
    nChanges = Ivy_FraigRefineClasses( p );
    if ( p->pManFraig->pData )
        return;
//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
    // refine classes by random simulation
    do {
        Ivy_FraigAssignRandom( p );
        Ivy_FraigSimulateOne( p );
        nClasses = p->lClasses.nItems;
        nChanges = Ivy_FraigRefineClasses( p );
        if ( p->pManFraig->pData )
            return;
//printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
    } while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
//    Ivy_FraigPrintSimClasses( p );
}

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

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

Ivy_FraigMan_t * Ivy_FraigStart ( Ivy_Man_t *  pManAig, Ivy_FraigParams_t *  pParams  )

static

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 554 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    Ivy_FraigSim_t * pSims;
    Ivy_Obj_t * pObj;
    int i, k, EntrySize;
    // clean the fanout representation
    Ivy_ManForEachObj( pManAig, pObj, i )
//        pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
        assert( !pObj->pEquiv && !pObj->pFanout );
    // allocat the fraiging manager
    p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
    memset( p, 0, sizeof(Ivy_FraigMan_t) );
    p->pParams   = pParams;
    p->pManAig   = pManAig;
    p->pManFraig = Ivy_ManStartFrom( pManAig );
    // allocate simulation info
    p->nSimWords    = pParams->nSimWords;
//    p->pSimWords    = ABC_ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords ); 
    EntrySize    = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
    p->pSimWords = (char *)ABC_ALLOC( char, Ivy_ManObjNum(pManAig) * EntrySize ); 
    memset( p->pSimWords, 0, EntrySize );
    k = 0;
    Ivy_ManForEachObj( pManAig, pObj, i )
    {
        pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
        pSims->pNext = NULL;
        if ( Ivy_ObjIsNode(pObj) )
        {
            if ( p->pSimStart == NULL )
                p->pSimStart = pSims;
            else
                ((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
            pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
            pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
            pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
        }
        else
        {
            pSims->pFanin0 = NULL;
            pSims->pFanin1 = NULL;
            pSims->Type = 0;
        }
        Ivy_ObjSetSim( pObj, pSims );
    }
    assert( k == Ivy_ManObjNum(pManAig) );
    // allocate storage for sim pattern
    p->nPatWords  = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
    p->pPatWords  = ABC_ALLOC( unsigned, p->nPatWords ); 
    p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords ); 
    p->vPiVars    = Vec_PtrAlloc( 100 );
    // set random number generator
    srand( 0xABCABC );
    return p;
}

Ivy_FraigMan_t * Ivy_FraigStartSimple ( Ivy_Man_t *  pManAig, Ivy_FraigParams_t *  pParams  )

static

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

Synopsis [Starts the fraiging manager without simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 530 of file ivyFraig.c.

{
    Ivy_FraigMan_t * p;
    // allocat the fraiging manager
    p = ABC_ALLOC( Ivy_FraigMan_t, 1 );
    memset( p, 0, sizeof(Ivy_FraigMan_t) );
    p->pParams   = pParams;
    p->pManAig   = pManAig;
    p->pManFraig = Ivy_ManStartFrom( pManAig );
    p->vPiVars   = Vec_PtrAlloc( 100 );
    return p;
}

void Ivy_FraigStop ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 621 of file ivyFraig.c.

{
    if ( p->pParams->fVerbose )
        Ivy_FraigPrint( p );
    if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
    if ( p->pSat ) sat_solver_delete( p->pSat );
    ABC_FREE( p->pPatScores );
    ABC_FREE( p->pPatWords );
    ABC_FREE( p->pSimWords );
    ABC_FREE( p );
}

void Ivy_FraigSweep ( Ivy_FraigMan_t *  p )

static

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 1968 of file ivyFraig.c.

{
    Ivy_Obj_t * pObj;//, * pTemp;
    int i, k = 0;
p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
p->nClassesBeg  = p->lClasses.nItems;
    // duplicate internal nodes
    p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
    Ivy_ManForEachNode( p->pManAig, pObj, i )
    {
        Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
        // default to simple strashing if simulation detected a counter-example for a PO
        if ( p->pManFraig->pData )
            pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
        else
            pObj->pEquiv = Ivy_FraigAnd( p, pObj );
        assert( pObj->pEquiv != NULL );
//        pTemp = Ivy_Regular(pObj->pEquiv);
//        assert( Ivy_Regular(pObj->pEquiv)->Type );
    }
    Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = p->lClasses.nItems;
    // try to prove the outputs of the miter
    p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
//    Ivy_FraigMiterStatus( p->pManFraig );
    if ( p->pParams->fProve && p->pManFraig->pData == NULL )
        Ivy_FraigMiterProve( p );
    // add the POs
    Ivy_ManForEachPo( p->pManAig, pObj, i )
        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
    // clean the old manager
    Ivy_ManForEachObj( p->pManAig, pObj, i )
        pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
    // clean the new manager
    Ivy_ManForEachObj( p->pManFraig, pObj, i )
    {
        if ( Ivy_ObjFaninVec(pObj) )
            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
        pObj->pEquiv = NULL;
    }
    // remove dangling nodes 
    Ivy_ManCleanup( p->pManFraig );
    // clean up the class marks
    Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
        pObj->fMarkA = 0;
}

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

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

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

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

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

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

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

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

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

static Ivy_Obj_t* Ivy_ObjClassNodeLast ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 141 of file ivyFraig.c.

{ return pObj->pNextFan0;  }

static Ivy_Obj_t* Ivy_ObjClassNodeNext ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 143 of file ivyFraig.c.

{ return pObj->pNextFan1;  }

static Ivy_Obj_t* Ivy_ObjClassNodeRepr ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 142 of file ivyFraig.c.

{ return pObj->pNextFan0;  }

static Ivy_Obj_t* Ivy_ObjEquivListNext ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 145 of file ivyFraig.c.

{ return pObj->pPrevFan0;  }

static Ivy_Obj_t* Ivy_ObjEquivListPrev ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 146 of file ivyFraig.c.

{ return pObj->pPrevFan1;  }

static Vec_Ptr_t* Ivy_ObjFaninVec ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 149 of file ivyFraig.c.

{ return (Vec_Ptr_t *)pObj->pNextFan1; }

static Ivy_Obj_t* Ivy_ObjFraig ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 147 of file ivyFraig.c.

{ return pObj->pEquiv;     }

static Ivy_Obj_t* Ivy_ObjNodeHashNext ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 144 of file ivyFraig.c.

{ return pObj->pPrevFan0;  }

static unsigned Ivy_ObjRandomSim ( )

inlinestatic

Definition at line 162 of file ivyFraig.c.

{ return (rand() << 24) ^ (rand() << 12) ^ rand(); }

static int Ivy_ObjSatNum ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 148 of file ivyFraig.c.

{ return (int)(ABC_PTRUINT_T)pObj->pNextFan0;         }

static void Ivy_ObjSetClassNodeLast ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pLast  )

inlinestatic

Definition at line 152 of file ivyFraig.c.

{ pObj->pNextFan0 = pLast; }

static void Ivy_ObjSetClassNodeNext ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pNext  )

inlinestatic

Definition at line 154 of file ivyFraig.c.

{ pObj->pNextFan1 = pNext; }

static void Ivy_ObjSetClassNodeRepr ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pRepr  )

inlinestatic

Definition at line 153 of file ivyFraig.c.

{ pObj->pNextFan0 = pRepr; }

static void Ivy_ObjSetEquivListNext ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pNext  )

inlinestatic

Definition at line 156 of file ivyFraig.c.

{ pObj->pPrevFan0 = pNext; }

static void Ivy_ObjSetEquivListPrev ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pPrev  )

inlinestatic

Definition at line 157 of file ivyFraig.c.

{ pObj->pPrevFan1 = pPrev; }

static void Ivy_ObjSetFaninVec ( Ivy_Obj_t *  pObj, Vec_Ptr_t *  vFanins  )

inlinestatic

Definition at line 160 of file ivyFraig.c.

{ pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }

static void Ivy_ObjSetFraig ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pNode  )

inlinestatic

Definition at line 158 of file ivyFraig.c.

{ pObj->pEquiv    = pNode; }

static void Ivy_ObjSetNodeHashNext ( Ivy_Obj_t *  pObj, Ivy_Obj_t *  pNext  )

inlinestatic

Definition at line 155 of file ivyFraig.c.

{ pObj->pPrevFan0 = pNext; }

static void Ivy_ObjSetSatNum ( Ivy_Obj_t *  pObj, int  Num  )

inlinestatic

Definition at line 159 of file ivyFraig.c.

{ pObj->pNextFan0 = (Ivy_Obj_t *)(ABC_PTRUINT_T)Num;     }

static void Ivy_ObjSetSim ( Ivy_Obj_t *  pObj, Ivy_FraigSim_t *  pSim  )

inlinestatic

Definition at line 151 of file ivyFraig.c.

{ pObj->pFanout = (Ivy_Obj_t *)pSim; }

static Ivy_FraigSim_t* Ivy_ObjSim ( Ivy_Obj_t *  pObj )

inlinestatic

Definition at line 140 of file ivyFraig.c.

{ return (Ivy_FraigSim_t *)pObj->pFanout;  }

Variable Documentation

ABC_INT64_T s_nBTLimitGlobal = 0

static

Definition at line 207 of file ivyFraig.c.

ABC_INT64_T s_nInsLimitGlobal = 0

static

Definition at line 208 of file ivyFraig.c.