darScript.c File Reference

#include "darInt.h"
#include "proof/dch/dch.h"
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Aig_Man_t *	Dar_ManRewriteDefault (Aig_Man_t *pAig)
	DECLARATIONS ///. More...
Aig_Man_t *	Dar_ManRwsat (Aig_Man_t *pAig, int fBalance, int fVerbose)
	DECLARATIONS ///. More...
Aig_Man_t *	Dar_ManCompress (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Aig_Man_t *	Dar_ManCompress2 (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Vec_Ptr_t *	Dar_ManChoiceSynthesis (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Aig_Man_t *	Dar_ManChoice (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Aig_Man_t *	Dar_NewCompress (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Aig_Man_t *	Dar_NewCompress2 (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose)
int	Dar_NewChoiceSynthesisGuard (Aig_Man_t *pAig)
Gia_Man_t *	Dar_NewChoiceSynthesis (Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
Aig_Man_t *	Dar_ManChoiceNewAig (Aig_Man_t *pAig, Dch_Pars_t *pPars)
Aig_Man_t *	Dar_ManChoiceNew (Aig_Man_t *pAig, Dch_Pars_t *pPars)

Function Documentation

Aig_Man_t* Dar_ManChoice	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fConstruct,
		int	nConfMax,
		int	nLevelMax,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file darScript.c.

{
    Aig_Man_t * pMan, * pTemp;
    Vec_Ptr_t * vAigs;
    int i;
    abctime clk;

clk = Abc_Clock();
//    vAigs = Dar_ManChoiceSynthesisExt();
    vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, 0, fVerbose );

    // swap the first and last network
    // this should lead to the primary choice being "better" because of synthesis
    // (it is also important when constructing choices)
    if ( !fConstruct )
    {
        pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
        Vec_PtrWriteEntry( vAigs, 0, pMan );
    }

if ( fVerbose )
{
ABC_PRT( "Synthesis time", Abc_Clock() - clk );
}
clk = Abc_Clock();
    if ( fConstruct )
        pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
    else
        pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
        Aig_ManStop( pTemp );
    Vec_PtrFree( vAigs );
if ( fVerbose )
{
ABC_PRT( "Choicing time ", Abc_Clock() - clk );
}
    return pMan;
//    return NULL;
}

Aig_Man_t* Dar_ManChoiceNew	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Reproduces script "compress2".]

Description [Consumes the input AIG to reduce memory usage.]

SideEffects []

SeeAlso []

Definition at line 849 of file darScript.c.

{
    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
//    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
    extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
//    int fVerbose = pPars->fVerbose;
    Aig_Man_t * pMan, * pTemp;
    Gia_Man_t * pGia;
    Vec_Ptr_t * vPios;
    void * pManTime;
    char * pName, * pSpec;
    abctime clk;

    // save useful things
    pManTime = pAig->pManTime; pAig->pManTime = NULL;
    pName = Abc_UtilStrsav( pAig->pName );
    pSpec = Abc_UtilStrsav( pAig->pSpec );

    // perform synthesis
clk = Abc_Clock();
    pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
pPars->timeSynth = Abc_Clock() - clk;

    // perform choice computation
    if ( pPars->fUseGia )
        pMan = Cec_ComputeChoices( pGia, pPars );
    else
    {
        pMan = Gia_ManToAigSkip( pGia, 3 );
        Gia_ManStop( pGia );
        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
        Aig_ManStop( pTemp );
    }

    // create guidence
    vPios = Aig_ManOrderPios( pMan, pAig ); 
    Aig_ManStop( pAig );

    // reconstruct the network
    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
    Aig_ManStop( pTemp );
    Vec_PtrFree( vPios );

    // reset levels
    pMan->pManTime = pManTime;
    Aig_ManChoiceLevel( pMan );

    // copy names
    ABC_FREE( pMan->pName );
    ABC_FREE( pMan->pSpec );
    pMan->pName = pName;
    pMan->pSpec = pSpec;
    return pMan;
}

Aig_Man_t* Dar_ManChoiceNewAig	(	Aig_Man_t *	pAig,
		Dch_Pars_t *	pPars
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso [] Function*************************************************************

Synopsis [Reproduces script "compress2".]

Description [Consumes the input AIG to reduce memory usage.]

SideEffects []

SeeAlso []

Definition at line 778 of file darScript.c.

{
//    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
    extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
    int fVerbose = pPars->fVerbose;
    Aig_Man_t * pMan, * pTemp;
    Vec_Ptr_t * vAigs;
    Vec_Ptr_t * vPios;
    void * pManTime;
    char * pName, * pSpec;
    int i;
    abctime clk;

clk = Abc_Clock();
    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
pPars->timeSynth = Abc_Clock() - clk;
    // swap the first and last network
    // this should lead to the primary choice being "better" because of synthesis
    // (it is also important when constructing choices)
    pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
    Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
    Vec_PtrWriteEntry( vAigs, 0, pMan );

    // derive the total AIG
    pMan = Dch_DeriveTotalAig( vAigs );
    // cleanup
    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
        Aig_ManStop( pTemp );
    Vec_PtrFree( vAigs );

    // compute choices
    pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
    Aig_ManStop( pTemp );

    // save useful things
    pManTime = pAig->pManTime; pAig->pManTime = NULL;
    pName = Abc_UtilStrsav( pAig->pName );
    pSpec = Abc_UtilStrsav( pAig->pSpec );

    // create guidence
    vPios = Aig_ManOrderPios( pMan, pAig ); 
    Aig_ManStop( pAig );

    // reconstruct the network
    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
    Aig_ManStop( pTemp );
    Vec_PtrFree( vPios );

    // reset levels
    pMan->pManTime = pManTime;
    Aig_ManChoiceLevel( pMan );

    // copy names
    ABC_FREE( pMan->pName );
    ABC_FREE( pMan->pSpec );
    pMan->pName = pName;
    pMan->pSpec = pSpec;
    return pMan;
}

Vec_Ptr_t* Dar_ManChoiceSynthesis	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 345 of file darScript.c.

{
    Vec_Ptr_t * vAigs;

    vAigs = Vec_PtrAlloc( 3 );
    pAig = Aig_ManDupDfs(pAig);
    Vec_PtrPush( vAigs, pAig );

    pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
    Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );

    pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
    Vec_PtrPush( vAigs, pAig );
//Aig_ManPrintStats( pAig );

    pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
    return vAigs;
}

Aig_Man_t* Dar_ManCompress	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress".]

Description []

SideEffects []

SeeAlso []

Definition at line 162 of file darScript.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;

    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );
/*
    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
*/    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );

    return pAig;
}

Aig_Man_t* Dar_ManCompress2	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fFanout,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file darScript.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;
    pParsRwr->fFanout = fFanout;
    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );
/*
    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
*/
    // rewrite
//    Dar_ManRewrite( pAig, pParsRwr );
    pParsRwr->fUpdateLevel = 0;  // disable level update
    Dar_ManRewrite( pAig, pParsRwr );
    pParsRwr->fUpdateLevel = fUpdateLevel;  // reenable level update if needed

    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );

    // balance
//    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
    return pAig;
}

ABC_NAMESPACE_IMPL_START Aig_Man_t* Dar_ManRewriteDefault

(

Aig_Man_t *

pAig

)

DECLARATIONS ///.

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

FileName [darScript.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [Rewriting scripts.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Performs one iteration of AIG rewriting.]

Description []

SideEffects []

SeeAlso []

Definition at line 48 of file darScript.c.

{
    Aig_Man_t * pTemp;
    Dar_RwrPar_t Pars, * pPars = &Pars;
    Dar_ManDefaultRwrParams( pPars );
    pAig = Aig_ManDupDfs( pAig ); 
    Dar_ManRewrite( pAig, pPars );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    return pAig;
}

Aig_Man_t* Dar_ManRwsat	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fVerbose
	)

DECLARATIONS ///.

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

Synopsis [Reproduces script "rwsat".]

Description []

SideEffects [This procedure does not tighten level during restructuring.]

SeeAlso []

Definition at line 71 of file darScript.c.

{
    Aig_Man_t * pTemp;
    abctime Time = pAig->Time2Quit;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = 0;
    pParsRef->fUpdateLevel = 0;

    pParsRwr->fVerbose = fVerbose;
    pParsRef->fVerbose = fVerbose;
//printf( "1" );
    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );

//printf( "2" );
    // balance
    if ( fBalance )
    {
    pAig->Time2Quit = Time;
    pAig = Dar_ManBalance( pTemp = pAig, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
    }
   
//Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
//printf( "3" );
    // rewrite
    pAig->Time2Quit = Time;
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "4" );
    // refactor
    pAig->Time2Quit = Time;
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "5" );
    // balance
    if ( fBalance )
    {
    pAig->Time2Quit = Time;
    pAig = Dar_ManBalance( pTemp = pAig, 0 );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
    }

//printf( "6" );
    // rewrite
    pAig->Time2Quit = Time;
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    if ( Time && Abc_Clock() > Time )
        { if ( pAig ) Aig_ManStop( pAig ); return NULL; }

//printf( "7" );
    return pAig;
}

Gia_Man_t* Dar_NewChoiceSynthesis	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fLightSynth,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description [Takes AIG manager, consumes it, and produces GIA manager.]

SideEffects []

SeeAlso []

Definition at line 632 of file darScript.c.

{
    Vec_Ptr_t * vGias;
    Gia_Man_t * pGia, * pTemp;
    int i;

    if ( fUpdateLevel && Dar_NewChoiceSynthesisGuard(pAig) )
    {
        if ( fVerbose )
            printf( "Warning: Due to high fanout count of some nodes, level updating is disabled.\n" );
        fUpdateLevel = 0;
    }

    vGias = Vec_PtrAlloc( 3 );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );

    pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );

    pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
    pGia = Gia_ManFromAig(pAig);
    Vec_PtrPush( vGias, pGia );
//Aig_ManPrintStats( pAig );

    Aig_ManStop( pAig );

    // swap around the first and the last
    pTemp = (Gia_Man_t *)Vec_PtrPop( vGias );
    Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
    Vec_PtrWriteEntry( vGias, 0, pTemp );

//    Aig_Man_t * pAig;
//    int i;
//    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
//    Vec_PtrForEachEntry( Aig_Man_t *, p->vAigs, pAig, i )
//        Aig_ManPrintStats( pAig );

    // derive the miter
    pGia = Gia_ManChoiceMiter( vGias );

    // cleanup
    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
        Gia_ManStop( pTemp );
    Vec_PtrFree( vGias );
    return pGia;
}

int Dar_NewChoiceSynthesisGuard

(

Aig_Man_t *

pAig

)

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

Synopsis [Count the number of nodes with very high fanout count.]

Description []

SideEffects []

SeeAlso []

Definition at line 611 of file darScript.c.

{
    Aig_Obj_t * pObj;
    int i, Count = 0;
    Aig_ManForEachNode( pAig, pObj, i )
        if ( Aig_ObjRefs(pObj) > 1000 )
            Count += Aig_ObjRefs(pObj) / 1000;
    return (int)(Count > 10);
}

Aig_Man_t* Dar_NewCompress	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fPower,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress".]

Description []

SideEffects []

SeeAlso []

Definition at line 431 of file darScript.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;

    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

//    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );

    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );

    return pAig;
}

Aig_Man_t* Dar_NewCompress2	(	Aig_Man_t *	pAig,
		int	fBalance,
		int	fUpdateLevel,
		int	fFanout,
		int	fPower,
		int	fLightSynth,
		int	fVerbose
	)

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

Synopsis [Reproduces script "compress2".]

Description []

SideEffects []

SeeAlso []

Definition at line 496 of file darScript.c.

{
    Aig_Man_t * pTemp;

    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;

    Dar_ManDefaultRwrParams( pParsRwr );
    Dar_ManDefaultRefParams( pParsRef );

    pParsRwr->fUpdateLevel = fUpdateLevel;
    pParsRef->fUpdateLevel = fUpdateLevel;
    pParsRwr->fFanout = fFanout;
    pParsRwr->fPower = fPower;

    pParsRwr->fVerbose = 0;//fVerbose;
    pParsRef->fVerbose = 0;//fVerbose;

//    pAig = Aig_ManDupDfs( pAig ); 
    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );

    // skip if lighter synthesis is requested
    if ( !fLightSynth )
    {
        // rewrite
        //Dar_ManRewrite( pAig, pParsRwr );
//        pParsRwr->fUpdateLevel = 0;  // disable level update  // this change was requested in July and later disabled
        Dar_ManRewrite( pAig, pParsRwr );
//        pParsRwr->fUpdateLevel = fUpdateLevel;  // reenable level update if needed

        pAig = Aig_ManDupDfs( pTemp = pAig ); 
        Aig_ManStop( pTemp );
        if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    
        // refactor
        Dar_ManRefactor( pAig, pParsRef );
        pAig = Aig_ManDupDfs( pTemp = pAig ); 
        Aig_ManStop( pTemp );
        if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
    }

    // balance
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    
    // skip if lighter synthesis is requested
    if ( !fLightSynth )
    {
        // rewrite
        Dar_ManRewrite( pAig, pParsRwr );
        pAig = Aig_ManDupDfs( pTemp = pAig ); 
        Aig_ManStop( pTemp );
        if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
    }

    pParsRwr->fUseZeros = 1;
    pParsRef->fUseZeros = 1;
    
    // rewrite
    Dar_ManRewrite( pAig, pParsRwr );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );

    // skip if lighter synthesis is requested
    if ( !fLightSynth )
    {
        // balance
        if ( fBalance )
        {
        pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
        Aig_ManStop( pTemp );
        if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
        }
    }
    
    // refactor
    Dar_ManRefactor( pAig, pParsRef );
    pAig = Aig_ManDupDfs( pTemp = pAig ); 
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
    
    // skip if lighter synthesis is requested
    if ( !fLightSynth )
    {
        // rewrite
        Dar_ManRewrite( pAig, pParsRwr );
        pAig = Aig_ManDupDfs( pTemp = pAig ); 
        Aig_ManStop( pTemp );
        if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );
    }

    // balance
    if ( fBalance )
    {
    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
    Aig_ManStop( pTemp );
    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
    }
    return pAig;
}