absGla.c File Reference

#include "base/main/main.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
#include "bool/kit/kit.h"
#include "abs.h"
#include "absRef.h"

Include dependency graph for absGla.c:

Go to the source code of this file.

Classes
struct	Ga2_Man_t_

Macros
#define	GA2_BIG_NUM   0x3FFFFFF0
	DECLARATIONS ///.

Typedefs
typedef struct Ga2_Man_t_	Ga2_Man_t

Functions
unsigned	Ga2_ObjComputeTruth_rec (Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst)
	FUNCTION DEFINITIONS ///.
unsigned	Ga2_ManComputeTruth (Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves)
int	Ga2_ManBreakTree_rec (Gia_Man_t *p, Gia_Obj_t *pObj, int fFirst, int N)
int	Ga2_ManCheckNodesAnd (Gia_Man_t *p, Vec_Int_t *vNodes)
void	Ga2_ManCollectNodes_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vNodes, int fFirst)
void	Ga2_ManCollectLeaves_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vLeaves, int fFirst)
int	Ga2_ManMarkup (Gia_Man_t *p, int N, int fSimple)
void	Ga2_ManComputeTest (Gia_Man_t *p)
Ga2_Man_t *	Ga2_ManStart (Gia_Man_t *pGia, Abs_Par_t *pPars)
void	Ga2_ManDumpStats (Gia_Man_t *pGia, Abs_Par_t *pPars, sat_solver2 *pSat, int iFrame, int fUseN)
void	Ga2_ManReportMemory (Ga2_Man_t *p)
void	Ga2_ManStop (Ga2_Man_t *p)
unsigned	Ga2_ObjComputeTruthSpecial (Gia_Man_t *p, Gia_Obj_t *pRoot, Vec_Int_t *vLeaves, Vec_Int_t *vLits)
Vec_Int_t *	Ga2_ManCnfCompute (unsigned uTruth, int nVars, Vec_Int_t *vCover)
void	Ga2_ManCnfAddStatic (sat_solver2 *pSat, Vec_Int_t *vCnf0, Vec_Int_t *vCnf1, int Lits[], int iLitOut, int ProofId)
void	Ga2_ManAddAbsClauses (Ga2_Man_t *p, int f)
void	Ga2_ManAddToAbs (Ga2_Man_t *p, Vec_Int_t *vToAdd)
void	Ga2_ManShrinkAbs (Ga2_Man_t *p, int nAbs, int nValues, int nSatVars)
void	Ga2_ManAbsTranslate_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vClasses, int fFirst)
Vec_Int_t *	Ga2_ManAbsTranslate (Ga2_Man_t *p)
Vec_Int_t *	Ga2_ManAbsDerive (Gia_Man_t *p)
void	Ga2_ManRestart (Ga2_Man_t *p)
Abc_Cex_t *	Ga2_ManDeriveCex (Ga2_Man_t *p, Vec_Int_t *vPis)
void	Ga2_ManRefinePrint (Ga2_Man_t *p, Vec_Int_t *vVec)
void	Ga2_ManRefinePrintPPis (Ga2_Man_t *p)
void	Ga2_GlaPrepareCexAndMap (Ga2_Man_t *p, Abc_Cex_t **ppCex, Vec_Int_t **pvMaps)
Vec_Int_t *	Ga2_ManRefine (Ga2_Man_t *p)
int	Ga2_GlaAbsCount (Ga2_Man_t *p, int fRo, int fAnd)
void	Ga2_ManAbsPrintFrame (Ga2_Man_t *p, int nFrames, int nConfls, int nCexes, abctime Time, int fFinal)
char *	Ga2_GlaGetFileName (Ga2_Man_t *p, int fAbs)
void	Ga2_GlaDumpAbsracted (Ga2_Man_t *p, int fVerbose)
void	Gia_Ga2SendAbsracted (Ga2_Man_t *p, int fVerbose)
void	Gia_Ga2SendCancel (Ga2_Man_t *p, int fVerbose)
int	Gia_ManPerformGla (Gia_Man_t *pAig, Abs_Par_t *pPars)

Macro Definition Documentation

GA2_BIG_NUM

#define GA2_BIG_NUM   0x3FFFFFF0

DECLARATIONS ///.

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

FileName [absGla2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Scalable gate-level abstraction.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

absGla2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 35 of file absGla.c.

Typedef Documentation

Ga2_Man_t

typedef struct Ga2_Man_t_ Ga2_Man_t

Definition at line 37 of file absGla.c.

Function Documentation

Ga2_GlaAbsCount()

int Ga2_GlaAbsCount	(	Ga2_Man_t *	p,
		int	fRo,
		int	fAnd )

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1344 of file absGla.c.

{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    if ( fRo )
        Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
            Counter += Gia_ObjIsRo(p->pGia, pObj);
    else if ( fAnd )
        Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
            Counter += Gia_ObjIsAnd(pObj);
    else assert( 0 );
    return Counter;
}

Here is the caller graph for this function:

Ga2_GlaDumpAbsracted()

void Ga2_GlaDumpAbsracted	(	Ga2_Man_t *	p,
		int	fVerbose )

Definition at line 1421 of file absGla.c.

{
    char * pFileName;
    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs );
    if ( p->pPars->fDumpMabs )
    {
        pFileName = Ga2_GlaGetFileName(p, 0);
        if ( fVerbose )
            Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
        // dump abstraction map
        Vec_IntFreeP( &p->pGia->vGateClasses );
        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
        Gia_AigerWrite( p->pGia, pFileName, 0, 0, 0 );
    }
    else if ( p->pPars->fDumpVabs )
    {
        Vec_Int_t * vGateClasses;
        Gia_Man_t * pAbs;
        pFileName = Ga2_GlaGetFileName(p, 1);
        if ( fVerbose )
            Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
        // dump absracted model
        vGateClasses = Ga2_ManAbsTranslate( p );
        pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
        Gia_ManCleanValue( p->pGia );
        Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
        Gia_ManStop( pAbs );
        Vec_IntFreeP( &vGateClasses );
    }
    else assert( 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_GlaGetFileName()

char * Ga2_GlaGetFileName	(	Ga2_Man_t *	p,
		int	fAbs )

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1406 of file absGla.c.

{
    static char * pFileNameDef = "glabs.aig";
    if ( p->pPars->pFileVabs )
        return p->pPars->pFileVabs;
    if ( p->pGia->pSpec )
    {
        if ( fAbs )
            return Extra_FileNameGenericAppend( p->pGia->pSpec, "_abs.aig");
        else
            return Extra_FileNameGenericAppend( p->pGia->pSpec, "_gla.aig");
    }
    return pFileNameDef;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_GlaPrepareCexAndMap()

void Ga2_GlaPrepareCexAndMap	(	Ga2_Man_t *	p,
		Abc_Cex_t **	ppCex,
		Vec_Int_t **	pvMaps )

Definition at line 1247 of file absGla.c.

{
    Abc_Cex_t * pCex;
    Vec_Int_t * vMap;
    Gia_Obj_t * pObj;
    int f, i, k;
/*
    Gia_ManForEachObj( p->pGia, pObj, i )
        if ( Ga2_ObjId(p, pObj) >= 0 )
            assert( Vec_IntEntry(p->vValues, Ga2_ObjId(p, pObj)) == i );
*/
    // find PIs and PPIs
    vMap = Vec_IntAlloc( 1000 );
    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
    {
        if ( !i ) continue;
        if ( Ga2_ObjIsAbs(p, pObj) )
            continue;
        assert( pObj->fPhase );
        assert( Ga2_ObjIsLeaf(p, pObj) );
        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
        Vec_IntPush( vMap, Gia_ObjId(p->pGia, pObj) );
    }
    // derive counter-example
    pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
    pCex->iFrame = p->pPars->iFrame;
    for ( f = 0; f <= p->pPars->iFrame; f++ )
        Gia_ManForEachObjVec( vMap, p->pGia, pObj, k )
            if ( Ga2_ObjSatValue( p, pObj, f ) )
                Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
    *pvMaps = vMap;
    *ppCex = pCex;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManAbsDerive()

Vec_Int_t * Ga2_ManAbsDerive

(

Gia_Man_t *

p

)

Definition at line 1097 of file absGla.c.

{
    Vec_Int_t * vToAdd;
    Gia_Obj_t * pObj;
    int i;
    vToAdd = Vec_IntAlloc( 1000 );
    Gia_ManForEachRo( p, pObj, i )
        if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
            Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
    Gia_ManForEachAnd( p, pObj, i )
        if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, i) )
            Vec_IntPush( vToAdd, i );
    return vToAdd;
}

Here is the caller graph for this function:

Ga2_ManAbsPrintFrame()

void Ga2_ManAbsPrintFrame	(	Ga2_Man_t *	p,
		int	nFrames,
		int	nConfls,
		int	nCexes,
		abctime	Time,
		int	fFinal )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1369 of file absGla.c.

{
    int fUseNewLine = ((fFinal && nCexes) || p->pPars->fVeryVerbose);
    if ( Abc_FrameIsBatchMode() && !fUseNewLine )
        return;
    p->fUseNewLine = fUseNewLine;
    Abc_Print( 1, "%4d :", nFrames );
    Abc_Print( 1, "%4d", Abc_MinInt(100, 100 * Vec_IntSize(p->vAbs) / p->nMarked) ); 
    Abc_Print( 1, "%6d", Vec_IntSize(p->vAbs) );
    Abc_Print( 1, "%5d", Vec_IntSize(p->vValues)-Vec_IntSize(p->vAbs)-1 );
    Abc_Print( 1, "%5d", Ga2_GlaAbsCount(p, 1, 0) );
    Abc_Print( 1, "%6d", Ga2_GlaAbsCount(p, 0, 1) );
    Abc_Print( 1, "%8d", nConfls );
    if ( nCexes == 0 )
        Abc_Print( 1, "%5c", '-' ); 
    else
        Abc_Print( 1, "%5d", nCexes ); 
    Abc_PrintInt( sat_solver2_nvars(p->pSat) );
    Abc_PrintInt( sat_solver2_nclauses(p->pSat) );
    Abc_PrintInt( sat_solver2_nlearnts(p->pSat) );
    Abc_Print( 1, "%9.2f sec", 1.0*Time/CLOCKS_PER_SEC );
    Abc_Print( 1, "%5.0f MB", (sat_solver2_memory_proof(p->pSat) + sat_solver2_memory(p->pSat, 0)) / (1<<20) );
    Abc_Print( 1, "%s", fUseNewLine ? "\n" : "\r" );
    fflush( stdout );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManAbsTranslate()

Vec_Int_t * Ga2_ManAbsTranslate

(

Ga2_Man_t *

p

)

Definition at line 1077 of file absGla.c.

{
    Vec_Int_t * vGateClasses;
    Gia_Obj_t * pObj;
    int i;
    vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) );
    Vec_IntWriteEntry( vGateClasses, 0, 1 );
    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
        else if ( Gia_ObjIsRo(p->pGia, pObj) )
            Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
        else if ( !Gia_ObjIsConst0(pObj) )
            assert( 0 );
//        Gia_ObjPrint( p->pGia, pObj );
    }
    return vGateClasses;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManAbsTranslate_rec()

void Ga2_ManAbsTranslate_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vClasses,
		int	fFirst )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1067 of file absGla.c.

{
    if ( pObj->fPhase && !fFirst )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 );
    Ga2_ManAbsTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 );
    Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManAddAbsClauses()

void Ga2_ManAddAbsClauses	(	Ga2_Man_t *	p,
		int	f )

Definition at line 959 of file absGla.c.

{
    int fSimple = 0;
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
    {
        if ( i == p->LimAbs )
            break;
        if ( fSimple )
            Ga2_ManAddToAbsOneStatic( p, pObj, f, 0 );
        else
            Ga2_ManAddToAbsOneDynamic( p, pObj, f );
    }
    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
        if ( i >= p->LimAbs )
            Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
//    sat_solver2_simplify( p->pSat );
}

Here is the caller graph for this function:

Ga2_ManAddToAbs()

void Ga2_ManAddToAbs	(	Ga2_Man_t *	p,
		Vec_Int_t *	vToAdd )

Definition at line 979 of file absGla.c.

{
    Vec_Int_t * vLeaves;
    Gia_Obj_t * pObj, * pFanin;
    int f, i, k;
    // add abstraction objects
    Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
    {
        Ga2_ManSetupNode( p, pObj, 1 );
        if ( p->pSat->pPrf2 )
            Vec_IntWriteEntry( p->vProofIds, Gia_ObjId(p->pGia, pObj), p->nProofIds++ );
    }
    // add PPI objects
    Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
    {
        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
            if ( Ga2_ObjId( p, pFanin ) == -1 )
                Ga2_ManSetupNode( p, pFanin, 0 );
    }
    // add new clauses to the timeframes
    for ( f = 0; f <= p->pPars->iFrame; f++ )
    {
        Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
        Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
            Ga2_ManAddToAbsOneStatic( p, pObj, f, 1 );
    }
//    sat_solver2_simplify( p->pSat );
}

Here is the caller graph for this function:

Ga2_ManBreakTree_rec()

int Ga2_ManBreakTree_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int	fFirst,
		int	N )

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

Synopsis [Returns AIG marked for CNF generation.]

Description [The marking satisfies the following requirements: Each marked node has the number of marked fanins no more than N.]

SideEffects [Uses pObj->fPhase to store the markings.]

SeeAlso []

Definition at line 176 of file absGla.c.

{   // breaks a tree rooted at the node into N-feasible subtrees
    int Val0, Val1;
    if ( pObj->fPhase && !fFirst )
        return 1;
    Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N );
    Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N );
    if ( Val0 + Val1 < N )
        return Val0 + Val1;
    if ( Val0 + Val1 == N )
    {
        pObj->fPhase = 1;
        return 1;
    }
    assert( Val0 + Val1 > N );
    assert( Val0 < N && Val1 < N );
    if ( Val0 >= Val1 )
    {
        Gia_ObjFanin0(pObj)->fPhase = 1;
        Val0 = 1;
    }
    else 
    {
        Gia_ObjFanin1(pObj)->fPhase = 1;
        Val1 = 1;
    }
    if ( Val0 + Val1 < N )
        return Val0 + Val1;
    if ( Val0 + Val1 == N )
    {
        pObj->fPhase = 1;
        return 1;
    }
    assert( 0 );
    return -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManCheckNodesAnd()

int Ga2_ManCheckNodesAnd	(	Gia_Man_t *	p,
		Vec_Int_t *	vNodes )

Definition at line 212 of file absGla.c.

{
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) || 
             (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) )
            return 0;
    return 1;
}

Ga2_ManCnfAddStatic()

void Ga2_ManCnfAddStatic	(	sat_solver2 *	pSat,
		Vec_Int_t *	vCnf0,
		Vec_Int_t *	vCnf1,
		int	Lits[],
		int	iLitOut,
		int	ProofId )

Definition at line 684 of file absGla.c.

{
    Vec_Int_t * vCnf;
    int i, k, b, Cube, Literal, nClaLits, ClaLits[6];
    for ( i = 0; i < 2; i++ )
    {
        vCnf = i ? vCnf1 : vCnf0;
        Vec_IntForEachEntry( vCnf, Cube, k )
        {
            nClaLits = 0;
            ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
            for ( b = 0; b < 5; b++ )
            {
                Literal = 3 & (Cube >> (b << 1));
                if ( Literal == 1 ) // value 0 --> add positive literal
                {
//                    assert( Lits[b] > 1 );
                    ClaLits[nClaLits++] = Lits[b];
                }
                else if ( Literal == 2 ) // value 1 --> add negative literal
                {
//                    assert( Lits[b] > 1 );
                    ClaLits[nClaLits++] = lit_neg(Lits[b]);
                }
                else if ( Literal != 0 )
                    assert( 0 );
            }
            sat_solver2_addclause( pSat, ClaLits, ClaLits+nClaLits, ProofId );
        }
    }
}

Here is the call graph for this function:

Ga2_ManCnfCompute()

Vec_Int_t * Ga2_ManCnfCompute	(	unsigned	uTruth,
		int	nVars,
		Vec_Int_t *	vCover )

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

Synopsis [Returns CNF of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 630 of file absGla.c.

{
    int RetValue;
    assert( nVars <= 5 );
    // transform truth table into the SOP
    RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 0 );
    assert( RetValue == 0 );
    // check the case of constant cover
    return Vec_IntDup( vCover );
}

Here is the call graph for this function:

Ga2_ManCollectLeaves_rec()

void Ga2_ManCollectLeaves_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vLeaves,
		int	fFirst )

Definition at line 232 of file absGla.c.

{
    if ( pObj->fPhase && !fFirst )
    {
        Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) );
        return;
    }
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 );
    Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManCollectNodes_rec()

void Ga2_ManCollectNodes_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vNodes,
		int	fFirst )

Definition at line 222 of file absGla.c.

{
    if ( pObj->fPhase && !fFirst )
        return;
    assert( Gia_ObjIsAnd(pObj) );
    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 );
    Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 );
    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
 
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManComputeTest()

void Ga2_ManComputeTest

(

Gia_Man_t *

p

)

Definition at line 338 of file absGla.c.

{
    abctime clk;
//    unsigned uTruth;
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    clk = Abc_Clock();
    Ga2_ManMarkup( p, 5, 0 );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !pObj->fPhase )
            continue;
//        uTruth = Ga2_ObjTruth( p, pObj );
//        printf( "%6d : ", Counter );
//        Kit_DsdPrintFromTruth( &uTruth, Ga2_ObjLeaveNum(p, pObj) ); 
//        printf( "\n" );
        Counter++;
    }
    Abc_Print( 1, "Marked AND nodes = %6d.  ", Counter );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

Here is the call graph for this function:

Ga2_ManComputeTruth()

unsigned Ga2_ManComputeTruth	(	Gia_Man_t *	p,
		Gia_Obj_t *	pRoot,
		Vec_Int_t *	vLeaves )

Definition at line 150 of file absGla.c.

{
    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    Gia_Obj_t * pObj;
    unsigned Res;
    int i;
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        pObj->Value = uTruth5[i];
    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        pObj->Value = 0;
    return Res;
}

Here is the call graph for this function:

Ga2_ManDeriveCex()

Abc_Cex_t * Ga2_ManDeriveCex	(	Ga2_Man_t *	p,
		Vec_Int_t *	vPis )

Definition at line 1166 of file absGla.c.

{
    Abc_Cex_t * pCex;
    Gia_Obj_t * pObj;
    int i, f;
    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pGia), Gia_ManPiNum(p->pGia), p->pPars->iFrame+1 );
    pCex->iPo = 0;
    pCex->iFrame = p->pPars->iFrame;
    Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
    {
        if ( !Gia_ObjIsPi(p->pGia, pObj) )
            continue;
        assert( Gia_ObjIsPi(p->pGia, pObj) );
        for ( f = 0; f <= pCex->iFrame; f++ )
            if ( Ga2_ObjSatValue( p, pObj, f ) )
                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Gia_ObjCioId(pObj) );
    }
    return pCex;
} 

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManDumpStats()

void Ga2_ManDumpStats	(	Gia_Man_t *	pGia,
		Abs_Par_t *	pPars,
		sat_solver2 *	pSat,
		int	iFrame,
		int	fUseN )

Definition at line 410 of file absGla.c.

{
    FILE * pFile;
    char pFileName[32];
    sprintf( pFileName, "stats_gla%s%s.txt", fUseN ? "n":"", pPars->fUseFullProof ? "p":"" ); 
 
    pFile = fopen( pFileName, "a+" );
 
    fprintf( pFile, "%s pi=%d ff=%d and=%d mem=%d bmc=%d", 
        pGia->pName, 
        Gia_ManPiNum(pGia), Gia_ManRegNum(pGia), Gia_ManAndNum(pGia), 
        (int)(1 + sat_solver2_memory_proof(pSat)/(1<<20)),
        iFrame );
 
    if ( pGia->vGateClasses )
    fprintf( pFile, " ff=%d and=%d",                 
        Gia_GlaCountFlops( pGia, pGia->vGateClasses ),
        Gia_GlaCountNodes( pGia, pGia->vGateClasses )  );
 
    fprintf( pFile, "\n" );
    fclose( pFile );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManMarkup()

int Ga2_ManMarkup	(	Gia_Man_t *	p,
		int	N,
		int	fSimple )

Definition at line 243 of file absGla.c.

{
    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
//    abctime clk = Abc_Clock();
    Vec_Int_t * vLeaves;
    Gia_Obj_t * pObj;
    int i, k, Leaf, CountMarks;
 
    vLeaves = Vec_IntAlloc( 100 );
 
    if ( fSimple )
    {
        Gia_ManForEachObj( p, pObj, i )
            pObj->fPhase = !Gia_ObjIsCo(pObj);
    }
    else
    {
        // label nodes with multiple fanouts and inputs MUXes
        Gia_ManForEachObj( p, pObj, i )
        {
            pObj->Value = 0;
            if ( !Gia_ObjIsAnd(pObj) )
                continue;
            Gia_ObjFanin0(pObj)->Value++;
            Gia_ObjFanin1(pObj)->Value++;
            if ( !Gia_ObjIsMuxType(pObj) )
                continue;
            Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++;
            Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++;
            Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++;
            Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++;
        }
        Gia_ManForEachObj( p, pObj, i )
        {
            pObj->fPhase = 0;
            if ( Gia_ObjIsAnd(pObj) )
                pObj->fPhase = (pObj->Value > 1);
            else if ( Gia_ObjIsCo(pObj) )
                Gia_ObjFanin0(pObj)->fPhase = 1;
            else 
                pObj->fPhase = 1;
        } 
        // add marks when needed
        Gia_ManForEachAnd( p, pObj, i )
        {
            if ( !pObj->fPhase )
                continue;
            Vec_IntClear( vLeaves );
            Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
            if ( Vec_IntSize(vLeaves) > N )
                Ga2_ManBreakTree_rec( p, pObj, 1, N );
        }
    }
 
    // verify that the tree is split correctly
    Vec_IntFreeP( &p->vMapping );
    p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_ManForEachRo( p, pObj, i )
    {
        Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
        assert( pObj->fPhase );
        assert( Gia_ObjFanin0(pObjRi)->fPhase );
        // create map
        Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
        Vec_IntPush( p->vMapping, 1 );
        Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
        Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
        Vec_IntPush( p->vMapping, -1 );  // placeholder for ref counter
    }
    CountMarks = Gia_ManRegNum(p);
    Gia_ManForEachAnd( p, pObj, i )
    {
        if ( !pObj->fPhase )
            continue;
        Vec_IntClear( vLeaves );
        Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 );
        assert( Vec_IntSize(vLeaves) <= N );
        // create map
        Vec_IntWriteEntry( p->vMapping, i, Vec_IntSize(p->vMapping) );
        Vec_IntPush( p->vMapping, Vec_IntSize(vLeaves) );
        Vec_IntForEachEntry( vLeaves, Leaf, k )
        {            
            Vec_IntPush( p->vMapping, Leaf );
            Gia_ManObj(p, Leaf)->Value = uTruth5[k];
            assert( Gia_ManObj(p, Leaf)->fPhase );
        }
        Vec_IntPush( p->vMapping,  (int)Ga2_ObjComputeTruth_rec( p, pObj, 1 ) );
        Vec_IntPush( p->vMapping, -1 );  // placeholder for ref counter
        CountMarks++;
    }
//    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    Vec_IntFree( vLeaves );
    Gia_ManCleanValue( p );
    return CountMarks;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManRefine()

Vec_Int_t * Ga2_ManRefine

(

Ga2_Man_t *

p

)

Definition at line 1280 of file absGla.c.

{
    Abc_Cex_t * pCex;
    Vec_Int_t * vMap, * vVec;
    Gia_Obj_t * pObj;
    int i, k;
    if ( p->pPars->fAddLayer )
    {
        // use simplified refinement strategy, which adds logic near at PPI without finding important ones
        vVec = Vec_IntAlloc( 100 );
        Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
        {
            if ( !i ) continue;
            if ( Ga2_ObjIsAbs(p, pObj) )
                continue;
            assert( pObj->fPhase );
            assert( Ga2_ObjIsLeaf(p, pObj) );
            assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
            if ( Gia_ObjIsPi(p->pGia, pObj) )
                continue;
            Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
        }
        p->nObjAdded += Vec_IntSize(vVec);
        return vVec;
    }
    Ga2_GlaPrepareCexAndMap( p, &pCex, &vMap );
 //    Rf2_ManRefine( p->pRf2, pCex, vMap, p->pPars->fPropFanout, 1 );
    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, p->pPars->fNewRefine, 1 );
//    printf( "Refinement %d\n", Vec_IntSize(vVec) );
    Abc_CexFree( pCex );
    if ( Vec_IntSize(vVec) == 0 )
    {
        Vec_IntFree( vVec );
        Abc_CexFreeP( &p->pGia->pCexSeq );
        p->pGia->pCexSeq = Ga2_ManDeriveCex( p, vMap );
        Vec_IntFree( vMap );
        return NULL;
    }
    Vec_IntFree( vMap );
    // remove those already added
    k = 0;
    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
        if ( !Ga2_ObjIsAbs(p, pObj) )
            Vec_IntWriteEntry( vVec, k++, Gia_ObjId(p->pGia, pObj) );
    Vec_IntShrink( vVec, k );
 
    // these objects should be PPIs that are not abstracted yet
    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
        assert( pObj->fPhase );//&& Ga2_ObjIsLeaf(p, pObj) );
    p->nObjAdded += Vec_IntSize(vVec);
    return vVec;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManRefinePrint()

void Ga2_ManRefinePrint	(	Ga2_Man_t *	p,
		Vec_Int_t *	vVec )

Definition at line 1185 of file absGla.c.

{
    Gia_Obj_t * pObj, * pFanin;
    int i, k;
    printf( "\n         Unsat core: \n" );
    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
    {
        Vec_Int_t * vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
        printf( "%12d : ", i );
        printf( "Obj =%6d ", Gia_ObjId(p->pGia, pObj) );
        if ( Gia_ObjIsRo(p->pGia, pObj) )
            printf( "ff " );
        else
            printf( "   " );
        if ( Ga2_ObjIsAbs0(p, pObj) )
            printf( "a " );
        else if ( Ga2_ObjIsLeaf0(p, pObj) )
            printf( "l " );
        else 
            printf( "  " );
        printf( "Fanins: " );
        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
        {
            printf( "%6d ", Gia_ObjId(p->pGia, pFanin) );
            if ( Gia_ObjIsRo(p->pGia, pFanin) )
                printf( "ff " );
            else
                printf( "   " );
            if ( Ga2_ObjIsAbs0(p, pFanin) )
                printf( "a " );
            else if ( Ga2_ObjIsLeaf0(p, pFanin) )
                printf( "l " );
            else
                printf( "  " );
        }
        printf( "\n" );
    }
}

Ga2_ManRefinePrintPPis()

void Ga2_ManRefinePrintPPis

(

Ga2_Man_t *

p

)

Definition at line 1223 of file absGla.c.

{
    Vec_Int_t * vVec = Vec_IntAlloc( 100 );
    Gia_Obj_t * pObj;
    int i;
    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
    {
        if ( !i ) continue;
        if ( Ga2_ObjIsAbs(p, pObj) )
            continue;
        assert( pObj->fPhase );
        assert( Ga2_ObjIsLeaf(p, pObj) );
        assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );
        Vec_IntPush( vVec, Gia_ObjId(p->pGia, pObj) );
    }
    printf( "        Current PPIs (%d): ", Vec_IntSize(vVec) );
    Vec_IntSort( vVec, 1 );
    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
        printf( "%d ", Gia_ObjId(p->pGia, pObj) );
    printf( "\n" );
    Vec_IntFree( vVec );
}

Ga2_ManReportMemory()

void Ga2_ManReportMemory

(

Ga2_Man_t *

p

)

Definition at line 432 of file absGla.c.

{
    double memTot = 0;
    double memAig = 1.0 * p->pGia->nObjsAlloc * sizeof(Gia_Obj_t) + Vec_IntMemory(p->pGia->vMapping);
    double memSat = sat_solver2_memory( p->pSat, 1 );
    double memPro = sat_solver2_memory_proof( p->pSat );
    double memMap = Vec_VecMemoryInt( (Vec_Vec_t *)p->vId2Lit );
    double memRef = Rnm_ManMemoryUsage( p->pRnm );
    double memHash= sizeof(int) * 6 * p->nTable;
    double memOth = sizeof(Ga2_Man_t);
    memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
    memOth += Vec_IntMemory( p->vIds );
    memOth += Vec_IntMemory( p->vProofIds );
    memOth += Vec_IntMemory( p->vAbs );
    memOth += Vec_IntMemory( p->vValues );
    memOth += Vec_IntMemory( p->vLits );
    memOth += Vec_IntMemory( p->vIsopMem );
    memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
    memTot = memAig + memSat + memPro + memMap + memRef + memHash + memOth;
    ABC_PRMP( "Memory: AIG      ", memAig, memTot );
    ABC_PRMP( "Memory: SAT      ", memSat, memTot );
    ABC_PRMP( "Memory: Proof    ", memPro, memTot );
    ABC_PRMP( "Memory: Map      ", memMap, memTot );
    ABC_PRMP( "Memory: Refine   ", memRef, memTot );
    ABC_PRMP( "Memory: Hash     ", memHash,memTot );
    ABC_PRMP( "Memory: Other    ", memOth, memTot );
    ABC_PRMP( "Memory: TOTAL    ", memTot, memTot );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManRestart()

void Ga2_ManRestart

(

Ga2_Man_t *

p

)

Definition at line 1112 of file absGla.c.

{
    Vec_Int_t * vToAdd;
    int Lit = 1;
    assert( p->pGia != NULL && p->pGia->vGateClasses != NULL );
    assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set
    // clear SAT variable numbers (begin with 1)
    if ( p->pSat ) sat_solver2_delete( p->pSat );
    p->pSat      = sat_solver2_new();
    p->pSat->nLearntStart = p->pPars->nLearnedStart;
    p->pSat->nLearntDelta = p->pPars->nLearnedDelta;
    p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
    p->pSat->nLearntMax   = p->pSat->nLearntStart;
    // add clause x0 = 0  (lit0 = 1; lit1 = 0)
    sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, -1 );
    // remove previous abstraction
    Ga2_ManShrinkAbs( p, 1, 1, 1 );
    // start new abstraction
    vToAdd = Ga2_ManAbsDerive( p->pGia );
    assert( p->pSat->pPrf2 == NULL );
    assert( p->pPars->iFrame < 0 );
    Ga2_ManAddToAbs( p, vToAdd );
    Vec_IntFree( vToAdd );
    p->LimAbs = Vec_IntSize(p->vAbs);
    p->LimPpi = Vec_IntSize(p->vValues);
    // set runtime limit
    if ( p->pPars->nTimeOut )
        sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart );
    // clean the hash table
    memset( p->pTable, 0, 6 * sizeof(int) * p->nTable );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManShrinkAbs()

void Ga2_ManShrinkAbs	(	Ga2_Man_t *	p,
		int	nAbs,
		int	nValues,
		int	nSatVars )

Definition at line 1009 of file absGla.c.

{
    Vec_Int_t * vMap;
    Gia_Obj_t * pObj;
    int i, k, Entry;
    assert( nAbs > 0 );
    assert( nValues > 0 );
    assert( nSatVars > 0 );
    // shrink abstraction
    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
    {
        if ( !i ) continue;
        assert( Ga2_ObjCnf0(p, pObj) != NULL );
        assert( Ga2_ObjCnf1(p, pObj) != NULL );
        if ( i < nAbs )
            continue;
        Vec_IntFree( Ga2_ObjCnf0(p, pObj) );
        Vec_IntFree( Ga2_ObjCnf1(p, pObj) );
        Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj),     NULL );    
        Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, NULL );
    }
    Vec_IntShrink( p->vAbs, nAbs );
    // shrink values
    Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
    {
        assert( Ga2_ObjId(p,pObj) >= 0 );
        if ( i < nValues )
            continue;
        Ga2_ObjSetId( p, pObj, -1 );
    }
    Vec_IntShrink( p->vValues, nValues );
    Vec_PtrShrink( p->vCnfs, 2 * nValues );
    // hack to clear constant
    if ( nValues == 1 )
        nValues = 0;
    // clean mapping for each timeframe
    Vec_PtrForEachEntry( Vec_Int_t *, p->vId2Lit, vMap, i )
    {
        Vec_IntShrink( vMap, nValues );
        Vec_IntForEachEntryStart( vMap, Entry, k, p->LimAbs )
            if ( Entry >= 2*nSatVars )
                Vec_IntWriteEntry( vMap, k, -1 );
    }
    // shrink SAT variables
    p->nSatVars = nSatVars;
}

Here is the caller graph for this function:

Ga2_ManStart()

Ga2_Man_t * Ga2_ManStart	(	Gia_Man_t *	pGia,
		Abs_Par_t *	pPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 372 of file absGla.c.

{
    Ga2_Man_t * p;
    p = ABC_CALLOC( Ga2_Man_t, 1 );
    p->timeStart = Abc_Clock();
    p->fUseNewLine = 1;
    // user data
    p->pGia      = pGia;
    p->pPars     = pPars;
    // markings 
    p->nMarked   = Ga2_ManMarkup( pGia, 5, pPars->fUseSimple );
    p->vCnfs     = Vec_PtrAlloc( 1000 );
    Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
    Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
    // abstraction
    p->vIds      = Vec_IntStartFull( Gia_ManObjNum(pGia) );
    p->vProofIds = Vec_IntAlloc( 0 );
    p->vAbs      = Vec_IntAlloc( 1000 );
    p->vValues   = Vec_IntAlloc( 1000 );
    // add constant node to abstraction
    Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
    Vec_IntPush( p->vValues, 0 );
    Vec_IntPush( p->vAbs, 0 );
    // refinement
    p->pRnm      = Rnm_ManStart( pGia );
//    p->pRf2      = Rf2_ManStart( pGia );
    // SAT solver and variables
    p->vId2Lit   = Vec_PtrAlloc( 1000 );
    // temporaries
    p->vLits     = Vec_IntAlloc( 100 );
    p->vIsopMem  = Vec_IntAlloc( 100 );
    Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
    // hash table
    p->nTable = Abc_PrimeCudd(1<<18);
    p->pTable = ABC_CALLOC( int, 6 * p->nTable ); 
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ManStop()

void Ga2_ManStop

(

Ga2_Man_t *

p

)

Definition at line 460 of file absGla.c.

{
    Vec_IntFreeP( &p->pGia->vMapping );
    Gia_ManSetPhase( p->pGia );
    if ( p->pPars->fVerbose )
        Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  ObjsAdded = %d\n", 
            sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), 
            sat_solver2_nconflicts(p->pSat), sat_solver2_nlearnts(p->pSat), 
            p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
    if ( p->pPars->fVerbose )
    Abc_Print( 1, "Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  Concurrent calls = %d.\n", 
        p->nHashHit, p->nHashMiss, p->nHashOver, p->nPdrCalls );
 
    if( p->pSat ) sat_solver2_delete( p->pSat );
    Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
    Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
    Vec_IntFree( p->vIds );
    Vec_IntFree( p->vProofIds );
    Vec_IntFree( p->vAbs );
    Vec_IntFree( p->vValues );
    Vec_IntFree( p->vLits );
    Vec_IntFree( p->vIsopMem );
    Rnm_ManStop( p->pRnm, 0 );
//    Rf2_ManStop( p->pRf2, p->pPars->fVerbose );
    ABC_FREE( p->pTable );
    ABC_FREE( p->pSopSizes );
    ABC_FREE( p->pSops[1] );
    ABC_FREE( p->pSops );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ObjComputeTruth_rec()

unsigned Ga2_ObjComputeTruth_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		int	fFirst )

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes truth table for the marked node.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file absGla.c.

{
    unsigned Val0, Val1;
    if ( pObj->fPhase && !fFirst )
        return pObj->Value;
    assert( Gia_ObjIsAnd(pObj) );
    Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 );
    Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 );
    return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ga2_ObjComputeTruthSpecial()

unsigned Ga2_ObjComputeTruthSpecial	(	Gia_Man_t *	p,
		Gia_Obj_t *	pRoot,
		Vec_Int_t *	vLeaves,
		Vec_Int_t *	vLits )

Definition at line 512 of file absGla.c.

{
    int fVerbose = 0;
    static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    unsigned Res;
    Gia_Obj_t * pObj;
    int i, Entry;
//    int Id = Gia_ObjId(p, pRoot);
    assert( Gia_ObjIsAnd(pRoot) );
 
    if ( fVerbose )
    printf( "Object %d.\n", Gia_ObjId(p, pRoot) );
 
    // assign elementary truth tables
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
    {
        Entry = Vec_IntEntry( vLits, i );
        assert( Entry >= 0 );
        if ( Entry == 0 )
            pObj->Value = 0;
        else if ( Entry == 1 )
            pObj->Value = ~0;
        else // non-trivial literal
            pObj->Value = uTruth5[i];
        if ( fVerbose )
        printf( "%d ", Entry );
    }
 
    if ( fVerbose )
    {
    Res = Ga2_ObjTruth( p, pRoot );
//    Kit_DsdPrintFromTruth( &Res, Vec_IntSize(vLeaves) );
    printf( "\n" );
    }
 
    // compute truth table
    Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
    if ( Res != 0 && Res != ~0 )
    {
        // find essential variables
        int nUsed = 0, pUsed[5];
        for ( i = 0; i < Vec_IntSize(vLeaves); i++ )
            if ( Ga2_ObjTruthDepends( Res, i ) )
                pUsed[nUsed++] = i;
        assert( nUsed > 0 );
        // order positions by literal value
        Vec_IntSelectSortCost( pUsed, nUsed, vLits );
        assert( Vec_IntEntry(vLits, pUsed[0]) <= Vec_IntEntry(vLits, pUsed[nUsed-1]) );
        // assign elementary truth tables to the leaves
        Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        {
            Entry = Vec_IntEntry( vLits, i );
            assert( Entry >= 0 );
            if ( Entry == 0 )
                pObj->Value = 0;
            else if ( Entry == 1 )
                pObj->Value = ~0;
            else // non-trivial literal
                pObj->Value = 0xDEADCAFE; // not important
        }
        for ( i = 0; i < nUsed; i++ )
        {
            Entry = Vec_IntEntry( vLits, pUsed[i] );
            assert( Entry > 1 );
            pObj = Gia_ManObj( p, Vec_IntEntry(vLeaves, pUsed[i]) );
            pObj->Value = Abc_LitIsCompl(Entry) ? ~uTruth5[i] : uTruth5[i];
//            pObj->Value = uTruth5[i];
            // remember this literal
            pUsed[i] = Abc_LitRegular(Entry);
//            pUsed[i] = Entry;
        }
        // compute truth table
        Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 );
        // reload the literals
        Vec_IntClear( vLits );
        for ( i = 0; i < nUsed; i++ )
        {
            Vec_IntPush( vLits, pUsed[i] );
            assert( Ga2_ObjTruthDepends(Res, i) );
            if ( fVerbose )
            printf( "%d ", pUsed[i] );
        }
        for ( ; i < 5; i++ )
            assert( !Ga2_ObjTruthDepends(Res, i) );
 
if ( fVerbose )
{
//    Kit_DsdPrintFromTruth( &Res, nUsed );
    printf( "\n" );
}
 
    }
    else
    {
 
if ( fVerbose )
{
    Vec_IntClear( vLits );
    printf( "Const %d\n", Res > 0 );
}
 
    }
    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
        pObj->Value = 0;
    return Res;
}

Here is the call graph for this function:

Gia_Ga2SendAbsracted()

void Gia_Ga2SendAbsracted	(	Ga2_Man_t *	p,
		int	fVerbose )

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

Synopsis [Send abstracted model or send cancel.]

Description [Counter-example will be sent automatically when &vta terminates.]

SideEffects []

SeeAlso []

Definition at line 1464 of file absGla.c.

{
    Gia_Man_t * pAbs;
    Vec_Int_t * vGateClasses;
    assert( Abc_FrameIsBridgeMode() );
//    if ( fVerbose )
//        Abc_Print( 1, "Sending abstracted model...\n" );
    // create abstraction (value of p->pGia is not used here)
    vGateClasses = Ga2_ManAbsTranslate( p );
    pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
    Vec_IntFreeP( &vGateClasses );
    Gia_ManCleanValue( p->pGia );
    // send it out
    Gia_ManToBridgeAbsNetlist( stdout, pAbs, BRIDGE_ABS_NETLIST );
    Gia_ManStop( pAbs );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_Ga2SendCancel()

void Gia_Ga2SendCancel	(	Ga2_Man_t *	p,
		int	fVerbose )

Definition at line 1480 of file absGla.c.

{
    extern int Gia_ManToBridgeBadAbs( FILE * pFile );
    assert( Abc_FrameIsBridgeMode() );
//    if ( fVerbose )
//        Abc_Print( 1, "Cancelling previously sent model...\n" );
    Gia_ManToBridgeBadAbs( stdout );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPerformGla()

int Gia_ManPerformGla	(	Gia_Man_t *	pAig,
		Abs_Par_t *	pPars )

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

Synopsis [Performs gate-level abstraction.]

Description []

SideEffects []

SeeAlso []

Definition at line 1500 of file absGla.c.

{
    int fUseSecondCore = 1;
    Ga2_Man_t * p;
    Vec_Int_t * vCore, * vPPis;
    abctime clk2, clk = Abc_Clock();
    int Status = l_Undef, RetValue = -1, iFrameTryToProve = -1, fOneIsSent = 0;
    int i, c, f, Lit;
    pPars->iFrame = -1;
    // check trivial case 
    assert( Gia_ManPoNum(pAig) == 1 ); 
    ABC_FREE( pAig->pCexSeq );
    if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) )
    {
        if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) )
        {
            Abc_Print( 1, "Sequential miter is trivially UNSAT.\n" );
            return 1;
        }
        pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 );
        Abc_Print( 1, "Sequential miter is trivially SAT.\n" );
        return 0;
    }
    // create gate classes if not given
    if ( pAig->vGateClasses == NULL )
    {
        pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
        Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
        Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 );
    }
    // start the manager
    p = Ga2_ManStart( pAig, pPars );
    p->timeInit = Abc_Clock() - clk;
    // perform initial abstraction
    if ( p->pPars->fVerbose )
    {
        Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" );
        Abc_Print( 1, "FrameMax = %d  ConfMax = %d  Timeout = %d  Limit = %d %%  Limit2 = %d %%  RatioMax = %d %%\n", 
            pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin, pPars->nRatioMin2, pPars->nRatioMax );
        Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
            pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
        if ( pPars->fDumpVabs || pPars->fDumpMabs )
            Abc_Print( 1, "%s will be continuously dumped into file \"%s\".\n", 
                pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
        if ( pPars->fDumpMabs )
        {
            {
                char Command[1000];
                Abc_FrameSetStatus( -1 );
                Abc_FrameSetCex( NULL );
                Abc_FrameSetNFrames( -1 );
                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
            }
            {
                // create trivial abstraction map
                Gia_Obj_t * pObj; 
                char * pFileName = Ga2_GlaGetFileName(p, 0);
                Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
                pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
                Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
                Gia_ManForEachAnd( pAig, pObj, i )
                    Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
                Gia_ManForEachRo( pAig, pObj, i )
                    Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
                Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
                Vec_IntFree( pAig->vGateClasses );
                pAig->vGateClasses = vMap;
                if ( p->pPars->fVerbose )
                    Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
            }
        }
        Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
    }
    // iterate unrolling
    for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
    {
        int nAbsOld;
        // remember the timeframe
        p->pPars->iFrame = -1;
        // create new SAT solver
        Ga2_ManRestart( p );
        // remember abstraction size after the last restart
        nAbsOld = Vec_IntSize(p->vAbs);
        // unroll the circuit
        for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
        {
            // remember current limits
            int nConflsBeg = sat_solver2_nconflicts(p->pSat);
            int nAbs       = Vec_IntSize(p->vAbs);
            int nValues    = Vec_IntSize(p->vValues);
            int nVarsOld;
            // remember the timeframe
            p->pPars->iFrame = f;
            // extend and clear storage
            if ( f == Vec_PtrSize(p->vId2Lit) )
                Vec_PtrPush( p->vId2Lit, Vec_IntAlloc(0) );
            Vec_IntFillExtra( Ga2_MapFrameMap(p, f), Vec_IntSize(p->vValues), -1 );
            // add static clauses to this timeframe
            Ga2_ManAddAbsClauses( p, f );
            // skip checking if skipcheck is enabled (&gla -s)
            if ( p->pPars->fUseSkip && f <= p->pPars->iFrameProved )
                continue;
            // skip checking if we need to skip several starting frames (&gla -S <num>)
            if ( p->pPars->nFramesStart && f <= p->pPars->nFramesStart )
                continue;
            // get the output literal
//            Lit = Ga2_ManUnroll_rec( p, Gia_ManPo(pAig,0), f );
            Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(Gia_ManPo(pAig,0)), f );
            assert( Lit >= 0 );
            Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(Gia_ManPo(pAig,0)) );
            if ( Lit == 0 )
                continue;
            assert( Lit > 1 );
            // check for counter-examples
            if ( p->nSatVars > sat_solver2_nvars(p->pSat) )
                sat_solver2_setnvars( p->pSat, p->nSatVars );
            nVarsOld = p->nSatVars;
            for ( c = 0; ; c++ )
            {
                // consider the special case when the target literal is implied false
                // by implications which happened as a result of previous refinements
                // note that incremental UNSAT core cannot be computed because there is no learned clauses
                // in this case, we will assume that UNSAT core cannot reduce the problem
                if ( var_is_assigned(p->pSat, Abc_Lit2Var(Lit)) )
                {
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    break;
                }
                // perform SAT solving
                clk2 = Abc_Clock();
                Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                if ( Status == l_True ) // perform refinement
                {
                    p->nCexes++;
                    p->timeSat += Abc_Clock() - clk2;
 
                    // cancel old one if it was sent
                    if ( Abc_FrameIsBridgeMode() && fOneIsSent )
                    {
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                        fOneIsSent = 0;
                    }
                    if ( iFrameTryToProve >= 0 )
                    {
                        Gia_GlaProveCancel( pPars->fVerbose );
                        iFrameTryToProve = -1;
                    }
 
                    // perform refinement
                    clk2 = Abc_Clock();
                    Rnm_ManSetRefId( p->pRnm, c );
                    vPPis = Ga2_ManRefine( p );
                    p->timeCex += Abc_Clock() - clk2;
                    if ( vPPis == NULL )
                    {
                        if ( pPars->fVerbose )
                            Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
                        goto finish;
                    }
 
                    if ( c == 0 )
                    {
//                        Ga2_ManRefinePrintPPis( p );
                        // create bookmark to be used for rollback
                        assert( nVarsOld == p->pSat->size );
                        sat_solver2_bookmark( p->pSat );
                        // start incremental proof manager
                        assert( p->pSat->pPrf2 == NULL );
                        p->pSat->pPrf2 = Prf_ManAlloc();
                        if ( p->pSat->pPrf2 )
                        {
                            p->nProofIds = 0;
                            Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                            Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vPPis) );
                        }
                    }
                    else
                    {
                        // resize the proof logger
                        if ( p->pSat->pPrf2 )
                            Prf_ManGrow( p->pSat->pPrf2, p->nProofIds + Vec_IntSize(vPPis) );
                    }
 
                    Ga2_ManAddToAbs( p, vPPis );
                    Vec_IntFree( vPPis );
                    if ( pPars->fVerbose )
                        Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c+1, Abc_Clock() - clk, 0 );
                    // check if the number of objects is below limit
                    if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
                    {
                        Status = l_Undef;
                        goto finish;
                    }
                    continue;
                }
                p->timeUnsat += Abc_Clock() - clk2;
                if ( Status == l_Undef ) // ran out of resources
                    goto finish;
                if ( p->pSat->nRuntimeLimit && Abc_Clock() > p->pSat->nRuntimeLimit ) // timeout
                    goto finish;
                if ( c == 0 )
                {
                    if ( f > p->pPars->iFrameProved )
                        p->pPars->nFramesNoChange++;
                    break;
                }
                if ( f > p->pPars->iFrameProved )
                    p->pPars->nFramesNoChange = 0;
 
                // derive the core
                assert( p->pSat->pPrf2 != NULL );
                vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                Prf_ManStopP( &p->pSat->pPrf2 );
                // update the SAT solver
                sat_solver2_rollback( p->pSat );
                // reduce abstraction
                Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
 
                // purify UNSAT core
                if ( fUseSecondCore )
                {
//                    int nOldCore = Vec_IntSize(vCore);
                    // reverse the order of objects in the core
//                    Vec_IntSort( vCore, 0 );
//                    Vec_IntPrint( vCore );
                    // create bookmark to be used for rollback
                    assert( nVarsOld == p->pSat->size );
                    sat_solver2_bookmark( p->pSat );
                    // start incremental proof manager
                    assert( p->pSat->pPrf2 == NULL );
                    p->pSat->pPrf2 = Prf_ManAlloc();
                    if ( p->pSat->pPrf2 )
                    {
                        p->nProofIds = 0;
                        Vec_IntFill( p->vProofIds, Gia_ManObjNum(p->pGia), -1 );
                        Prf_ManRestart( p->pSat->pPrf2, p->vProofIds, sat_solver2_nlearnts(p->pSat), Vec_IntSize(vCore) );
 
                        Ga2_ManAddToAbs( p, vCore );
                        Vec_IntFree( vCore );
                    }
                    // run SAT solver
                    clk2 = Abc_Clock();
                    Status = sat_solver2_solve( p->pSat, &Lit, &Lit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
                    if ( Status == l_Undef )
                        goto finish;
                    assert( Status == l_False );
                    p->timeUnsat += Abc_Clock() - clk2;
 
                    // derive the core
                    assert( p->pSat->pPrf2 != NULL );
                    vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat );
                    Prf_ManStopP( &p->pSat->pPrf2 );
                    // update the SAT solver
                    sat_solver2_rollback( p->pSat );
                    // reduce abstraction
                    Ga2_ManShrinkAbs( p, nAbs, nValues, nVarsOld );
//                    printf( "\n%4d -> %4d\n", nOldCore, Vec_IntSize(vCore) );
                }
 
                Ga2_ManAddToAbs( p, vCore );
//                Ga2_ManRefinePrint( p, vCore );
                Vec_IntFree( vCore );
                break;
            }
            // remember the last proved frame
            if ( p->pPars->iFrameProved < f )
                p->pPars->iFrameProved = f;
            // print statistics
            if ( pPars->fVerbose )
                Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, Abc_Clock() - clk, 1 );
            // check if abstraction was proved
            if ( Gia_GlaProveCheck( pPars->fVerbose ) )
            {
                RetValue = 1;
                goto finish;
            }
            if ( c > 0 ) 
            {
                if ( p->pPars->fVeryVerbose )
                    Abc_Print( 1, "\n" );
                // recompute the abstraction
                Vec_IntFreeP( &pAig->vGateClasses );
                pAig->vGateClasses = Ga2_ManAbsTranslate( p );
                // check if the number of objects is below limit
                if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
                {
                    Status = l_Undef;
                    goto finish;
                }
            }
            // check the number of stable frames
            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
            {
                // dump the model into file
                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
                {
                    char Command[1000];
                    Abc_FrameSetStatus( -1 );
                    Abc_FrameSetCex( NULL );
                    Abc_FrameSetNFrames( f );
                    sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
                    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                    Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                }
                // call the prover
                if ( p->pPars->fCallProver )
                {
                    // cancel old one if it is proving
                    if ( iFrameTryToProve >= 0 )
                        Gia_GlaProveCancel( pPars->fVerbose );
                    // prove new one
                    Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose );
                    iFrameTryToProve = f;
                    p->nPdrCalls++;
                }
                // speak to the bridge
                if ( Abc_FrameIsBridgeMode() )
                {
                    // cancel old one if it was sent
                    if ( fOneIsSent )
                        Gia_Ga2SendCancel( p, pPars->fVerbose );
                    // send new one 
                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
                    fOneIsSent = 1;
                }
            }
            // if abstraction grew more than a certain percentage, force a restart
            if ( pPars->nRatioMax == 0 )
                continue;
            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
            {
                if ( p->pPars->fVerbose )
                Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
                    nAbsOld, Vec_IntSize(p->vAbs), pPars->nRatioMax );
                break;
            }
        }
    }
finish:
    Prf_ManStopP( &p->pSat->pPrf2 );
    // cancel old one if it is proving
    if ( iFrameTryToProve >= 0 )
        Gia_GlaProveCancel( pPars->fVerbose );
    // analize the results
    if ( !p->fUseNewLine )
        Abc_Print( 1, "\n" );
    if ( RetValue == 1 )
        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d  ", p->pPars->iFrameProved+1, iFrameTryToProve );
    else if ( pAig->pCexSeq == NULL )
    {
        Vec_IntFreeP( &pAig->vGateClasses );
        pAig->vGateClasses = Ga2_ManAbsTranslate( p );
        if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit ) 
            Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction.    ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
            Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction.  ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement.  ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
        else if ( pPars->nRatioMin && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin / 100 )
            Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d.  ", pPars->nRatioMin, p->pPars->iFrameProved+1 );
        else
            Abc_Print( 1, "GLA finished %d frames and produced a %d-stable abstraction.  ", p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
        p->pPars->iFrame = p->pPars->iFrameProved;
    }
    else
    {
        if ( p->pPars->fVerbose )
            Abc_Print( 1, "\n" );
        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
            Abc_Print( 1, "    Gia_ManPerformGlaOld(): CEX verification has failed!\n" );
        Abc_Print( 1, "True counter-example detected in frame %d.  ", f );
        p->pPars->iFrame = f - 1;
        Vec_IntFreeP( &pAig->vGateClasses );
        RetValue = 0;
    }
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    if ( p->pPars->fVerbose )
    {
        p->timeOther = (Abc_Clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit;
        ABC_PRTP( "Runtime: Initializing", p->timeInit,   Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Solver SAT  ", p->timeSat,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Refinement  ", p->timeCex,    Abc_Clock() - clk );
        ABC_PRTP( "Runtime: Other       ", p->timeOther,  Abc_Clock() - clk );
        ABC_PRTP( "Runtime: TOTAL       ", Abc_Clock() - clk, Abc_Clock() - clk );
        Ga2_ManReportMemory( p );
    }
//    Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
    Ga2_ManStop( p );
    fflush( stdout );
    return RetValue;
}

Here is the call graph for this function:

Here is the caller graph for this function: