giaAig.c File Reference

#include "giaAig.h"
#include "aig/gia/gia.h"
#include "proof/fra/fra.h"
#include "proof/dch/dch.h"
#include "opt/dar/dar.h"
#include "opt/dau/dau.h"
#include <assert.h>

Include dependency graph for giaAig.c:

Go to the source code of this file.

Functions
void	Gia_ManFromAig_rec (Gia_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
	FUNCTION DEFINITIONS ///.
Gia_Man_t *	Gia_ManFromAig (Aig_Man_t *p)
	INCLUDES ///.
void	Gia_ManCheckChoices_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
void	Gia_ManCheckChoices (Gia_Man_t *p)
void	Gia_ManFromAigChoices_rec (Gia_Man_t *pNew, Aig_Man_t *p, Aig_Obj_t *pObj)
Gia_Man_t *	Gia_ManFromAigChoices (Aig_Man_t *p)
Gia_Man_t *	Gia_ManFromAigSimple (Aig_Man_t *p)
Gia_Man_t *	Gia_ManFromAigSwitch (Aig_Man_t *p)
void	Gia_ManToAig_rec (Aig_Man_t *pNew, Aig_Obj_t **ppNodes, Gia_Man_t *p, Gia_Obj_t *pObj)
Aig_Man_t *	Gia_ManToAig (Gia_Man_t *p, int fChoices)
Aig_Man_t *	Gia_ManToAigSkip (Gia_Man_t *p, int nOutDelta)
Aig_Man_t *	Gia_ManToAigSimple (Gia_Man_t *p)
Aig_Man_t *	Gia_ManCofactorAig (Aig_Man_t *p, int nFrames, int nCofFanLit)
void	Gia_ManReprToAigRepr (Aig_Man_t *pAig, Gia_Man_t *pGia)
void	Gia_ManReprToAigRepr2 (Aig_Man_t *pAig, Gia_Man_t *pGia)
void	Gia_ManReprFromAigRepr (Aig_Man_t *pAig, Gia_Man_t *pGia)
void	Gia_ManReprFromAigRepr2 (Aig_Man_t *pAig, Gia_Man_t *pGia)
Gia_Man_t *	Gia_ManCompress2 (Gia_Man_t *p, int fUpdateLevel, int fVerbose)
int	Gia_ManTestChoices (Gia_Man_t *p)
Gia_Man_t *	Gia_ManPerformDch (Gia_Man_t *p, void *pPars)
void	Gia_ManSeqCleanupClasses (Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
int	Gia_ManSolveSat (Gia_Man_t *p)

Function Documentation

Gia_ManCheckChoices()

void Gia_ManCheckChoices

(

Gia_Man_t *

p

)

Definition at line 125 of file giaAig.c.

{
    Gia_Obj_t * pObj;
    int i, fFound = 0;
    Gia_ManCleanPhase( p );
    Gia_ManForEachCo( p, pObj, i )
        Gia_ManCheckChoices_rec( p, Gia_ObjFanin0(pObj) );
    Gia_ManForEachAnd( p, pObj, i )
        if ( !pObj->fPhase )
            printf( "Object %d is dangling.\n", i ), fFound = 1;
    if ( !fFound )
        printf( "There are no dangling objects.\n" );
    Gia_ManCleanPhase( p );
}

Here is the call graph for this function:

Gia_ManCheckChoices_rec()

void Gia_ManCheckChoices_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj )

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

Synopsis [Checks integrity of choice nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 116 of file giaAig.c.

{
    if ( !pObj || !Gia_ObjIsAnd(pObj) || pObj->fPhase )
        return;
    pObj->fPhase = 1;
    Gia_ManCheckChoices_rec( p, Gia_ObjFanin0(pObj) );
    Gia_ManCheckChoices_rec( p, Gia_ObjFanin1(pObj) );
    Gia_ManCheckChoices_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManCofactorAig()

Aig_Man_t * Gia_ManCofactorAig	(	Aig_Man_t *	p,
		int	nFrames,
		int	nCofFanLit )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file giaAig.c.

{
    Aig_Man_t * pMan;
    Gia_Man_t * pGia, * pTemp;
    pGia = Gia_ManFromAig( p );
    pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
    Gia_ManStop( pTemp );
    pMan = Gia_ManToAig( pGia, 0 );
    Gia_ManStop( pGia );
    return pMan;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManCompress2()

Gia_Man_t * Gia_ManCompress2	(	Gia_Man_t *	p,
		int	fUpdateLevel,
		int	fVerbose )

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

Synopsis [Applies DC2 to the GIA manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 592 of file giaAig.c.

{
    Gia_Man_t * pGia;
    Aig_Man_t * pNew, * pTemp;
    if ( p->pManTime && p->vLevels == NULL )
        Gia_ManLevelWithBoxes( p );
    pNew = Gia_ManToAig( p, 0 );
    pNew = Dar_ManCompress2( pTemp = pNew, 1, fUpdateLevel, 1, 0, fVerbose );
    Aig_ManStop( pTemp );
    pGia = Gia_ManFromAig( pNew );
    Aig_ManStop( pNew );
    Gia_ManTransferTiming( pGia, p );
    return pGia;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAig()

Gia_Man_t * Gia_ManFromAig

(

Aig_Man_t *

p

)

INCLUDES ///.

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

FileName [giaAig.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

giaAig.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES /// MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

Definition at line 76 of file giaAig.c.

{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    pNew = Gia_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create room to store equivalences
    if ( p->pEquivs )
        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Gia_ManAppendCi( pNew );
    // add logic for the POs
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    if ( pNew->pNexts )
        Gia_ManDeriveReprs( pNew );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAig_rec()

void Gia_ManFromAig_rec	(	Gia_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj )

FUNCTION DEFINITIONS ///.

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 57 of file giaAig.c.

{
    Aig_Obj_t * pNext;
    if ( pObj->iData )
        return;
    assert( Aig_ObjIsNode(pObj) );
    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
    if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
    {
        int iObjNew, iNextNew;
        Gia_ManFromAig_rec( pNew, p, pNext );
        iObjNew  = Abc_Lit2Var(pObj->iData);
        iNextNew = Abc_Lit2Var(pNext->iData);
        if ( pNew->pNexts )
            pNew->pNexts[iObjNew] = iNextNew;        
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAigChoices()

Gia_Man_t * Gia_ManFromAigChoices

(

Aig_Man_t *

p

)

Definition at line 170 of file giaAig.c.

{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( p->pEquivs != NULL );
    // create the new manager
    pNew = Gia_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create room to store equivalences
    pNew->pSibls = ABC_CALLOC( int, Aig_ManObjNum(p) );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Gia_ManAppendCi( pNew );
    // add logic for the POs
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );        
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
    //Gia_ManCheckChoices( pNew );
    if ( pNew->pSibls )
        Gia_ManDeriveReprsFromSibls( pNew );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAigChoices_rec()

void Gia_ManFromAigChoices_rec	(	Gia_Man_t *	pNew,
		Aig_Man_t *	p,
		Aig_Obj_t *	pObj )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 151 of file giaAig.c.

{
    if ( pObj == NULL || pObj->iData )
        return;
    assert( Aig_ObjIsNode(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin0(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjFanin1(pObj) );
    Gia_ManFromAigChoices_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
    pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
    if ( Aig_ObjEquiv(p, pObj) )
    {
        int iObjNew, iNextNew;
        iObjNew  = Abc_Lit2Var(pObj->iData);
        iNextNew = Abc_Lit2Var(Aig_ObjEquiv(p, pObj)->iData);
        assert( iObjNew > iNextNew );
        assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) );
        pNew->pSibls[iObjNew] = iNextNew;        
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAigSimple()

Gia_Man_t * Gia_ManFromAigSimple

(

Aig_Man_t *

p

)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 212 of file giaAig.c.

{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    pNew = Gia_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManForEachObj( p, pObj, i )
    {
        if ( Aig_ObjIsAnd(pObj) )
            pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
        else if ( Aig_ObjIsCi(pObj) )
            pObj->iData = Gia_ManAppendCi( pNew );
        else if ( Aig_ObjIsCo(pObj) )
            pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
        else if ( Aig_ObjIsConst1(pObj) )
            pObj->iData = 1;
        else
            assert( 0 );
    }
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManFromAigSwitch()

Gia_Man_t * Gia_ManFromAigSwitch

(

Aig_Man_t *

p

)

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

Synopsis [Handles choices as additional combinational outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file giaAig.c.

{
    Gia_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    // create the new manager
    pNew = Gia_ManStart( Aig_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->iData = 1;
    Aig_ManForEachCi( p, pObj, i )
        pObj->iData = Gia_ManAppendCi( pNew );
    // add POs corresponding to the nodes with choices
    Aig_ManForEachNode( p, pObj, i )
        if ( Aig_ObjRefs(pObj) == 0 )
        {
            Gia_ManFromAig_rec( pNew, p, pObj );        
            Gia_ManAppendCo( pNew, pObj->iData );
        }
    // add logic for the POs
    Aig_ManForEachCo( p, pObj, i )
        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
    Aig_ManForEachCo( p, pObj, i )
        pObj->iData = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
    Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManPerformDch()

Gia_Man_t * Gia_ManPerformDch	(	Gia_Man_t *	p,
		void *	pPars )

Definition at line 639 of file giaAig.c.

{
    int fUseMapping = 0;
    Gia_Man_t * pGia, * pGia1;
    Aig_Man_t * pNew;
    if ( p->pManTime && p->vLevels == NULL )
        Gia_ManLevelWithBoxes( p );
    if ( fUseMapping && Gia_ManHasMapping(p) )
        pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( p, 0 );
    else
        pGia1 = Gia_ManDup( p );
    pNew = Gia_ManToAig( pGia1, 0 );
    Gia_ManStop( pGia1 );
    pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars );
//    pGia = Gia_ManFromAig( pNew );
    pGia = Gia_ManFromAigChoices( pNew );
    Aig_ManStop( pNew );
    if ( !p->pManTime && !Gia_ManTestChoices(pGia) )
    {
        Gia_ManStop( pGia );
        pGia = Gia_ManDup( p );
    }
    Gia_ManTransferTiming( pGia, p );
    return pGia;
}

Here is the call graph for this function:

Gia_ManReprFromAigRepr()

void Gia_ManReprFromAigRepr	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia )

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

Synopsis [Transfers representatives from pAig to pGia.]

Description []

SideEffects []

SeeAlso []

Definition at line 528 of file giaAig.c.

{
    Gia_Obj_t * pObjGia; 
    Aig_Obj_t * pObjAig, * pReprAig;
    int i;
    assert( pAig->pReprs != NULL );
    assert( pGia->pReprs == NULL );
    assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
    pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
        Gia_ObjSetRepr( pGia, i, GIA_VOID );
    // move pointers from GIA to AIG
    Gia_ManForEachObj( pGia, pObjGia, i )
    {
        if ( Gia_ObjIsCo(pObjGia) )
            continue;
        assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
        pObjAig  = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
        pObjAig->iData = i;
    }
    Aig_ManForEachObj( pAig, pObjAig, i )
    {
        if ( Aig_ObjIsCo(pObjAig) )
            continue;
        if ( pAig->pReprs[i] == NULL )
            continue;
        pReprAig = pAig->pReprs[i];
        Gia_ObjSetRepr( pGia, pObjAig->iData, pReprAig->iData );
    }
    pGia->pNexts = Gia_ManDeriveNexts( pGia );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManReprFromAigRepr2()

void Gia_ManReprFromAigRepr2	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia )

Definition at line 559 of file giaAig.c.

{
    Aig_Obj_t * pObjAig, * pReprAig;
    int i;
    assert( pAig->pReprs != NULL );
    assert( pGia->pReprs == NULL );
    assert( Gia_ManObjNum(pGia) - Gia_ManCoNum(pGia) == Aig_ManObjNum(pAig) - Aig_ManCoNum(pAig) );
    pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
    for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
        Gia_ObjSetRepr( pGia, i, GIA_VOID );
    Aig_ManForEachObj( pAig, pObjAig, i )
    {
        if ( Aig_ObjIsCo(pObjAig) )
            continue;
        if ( pAig->pReprs[i] == NULL )
            continue;
        pReprAig = pAig->pReprs[i];
        Gia_ObjSetRepr( pGia, Abc_Lit2Var(pObjAig->iData), Abc_Lit2Var(pReprAig->iData) );
    }
    pGia->pNexts = Gia_ManDeriveNexts( pGia );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManReprToAigRepr()

void Gia_ManReprToAigRepr	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia )

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

Synopsis [Transfers representatives from pGia to pAig.]

Description [Assumes that pGia was created from pAig.]

SideEffects []

SeeAlso []

Definition at line 476 of file giaAig.c.

{
    Aig_Obj_t * pObj;
    Gia_Obj_t * pGiaObj, * pGiaRepr;
    int i;
    assert( pAig->pReprs == NULL );
    assert( pGia->pReprs != NULL );
    // move pointers from AIG to GIA
    Aig_ManForEachObj( pAig, pObj, i )
    {
        assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
        pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
        pGiaObj->Value = i;
    }
    // set the pointers to the nodes in AIG
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    Gia_ManForEachObj( pGia, pGiaObj, i )
    {
        pGiaRepr = Gia_ObjReprObj( pGia, i );
        if ( pGiaRepr == NULL )
            continue;
        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManReprToAigRepr2()

void Gia_ManReprToAigRepr2	(	Aig_Man_t *	pAig,
		Gia_Man_t *	pGia )

Definition at line 500 of file giaAig.c.

{
    Gia_Obj_t * pGiaObj, * pGiaRepr;
    int i;
    assert( pAig->pReprs == NULL );
    assert( pGia->pReprs != NULL );
    // set the pointers to the nodes in AIG
    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
    Gia_ManForEachObj( pGia, pGiaObj, i )
    {
        pGiaRepr = Gia_ObjReprObj( pGia, i );
        if ( pGiaRepr == NULL )
            continue;
        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManSeqCleanupClasses()

void Gia_ManSeqCleanupClasses	(	Gia_Man_t *	p,
		int	fConst,
		int	fEquiv,
		int	fVerbose )

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

Synopsis [Computes equivalences after structural sequential cleanup.]

Description []

SideEffects []

SeeAlso []

Definition at line 676 of file giaAig.c.

{
    Aig_Man_t * pNew, * pTemp;
    pNew  = Gia_ManToAigSimple( p );
    pTemp = Aig_ManScl( pNew, fConst, fEquiv, 0, -1, -1, fVerbose, 0 );
    Gia_ManReprFromAigRepr( pNew, p );
    Aig_ManStop( pTemp );
    Aig_ManStop( pNew );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManSolveSat()

int Gia_ManSolveSat

(

Gia_Man_t *

p

)

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

Synopsis [Solves SAT problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 697 of file giaAig.c.

{
//    extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
    Aig_Man_t * pNew;
    int RetValue;//, clk = Abc_Clock();
    pNew = Gia_ManToAig( p, 0 );
    RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
    if ( RetValue == 0 )
    {
        Gia_Obj_t * pObj;
        int i, * pInit = (int *)pNew->pData;
        Gia_ManConst0(p)->fMark0 = 0;
        Gia_ManForEachPi( p, pObj, i )
            pObj->fMark0 = pInit[i];
        Gia_ManForEachAnd( p, pObj, i )
            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
        Gia_ManForEachPo( p, pObj, i )
            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
        Gia_ManForEachPo( p, pObj, i )
            if ( pObj->fMark0 != 1 )
                break;
        if ( i != Gia_ManPoNum(p) )
            Abc_Print( 1, "Counter-example verification has failed.  " );
//        else
//            Abc_Print( 1, "Counter-example verification succeeded.  " );
    }
/*
    else if ( RetValue == 1 )
        Abc_Print( 1, "The SAT problem is unsatisfiable.  " );
    else if ( RetValue == -1 )
        Abc_Print( 1, "The SAT problem is undecided.  " );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
*/
    Aig_ManStop( pNew );
    return RetValue;
}

Here is the call graph for this function:

Gia_ManTestChoices()

int Gia_ManTestChoices

(

Gia_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 618 of file giaAig.c.

{
    Gia_Obj_t * pObj; int i;
    Vec_Int_t * vPointed = Vec_IntStart( Gia_ManObjNum(p) );
    Gia_ManForEachAnd( p, pObj, i )
        if ( Gia_ObjSibl(p, i) )
            Vec_IntWriteEntry( vPointed, Gia_ObjSibl(p, i), 1 );
    Gia_ManCreateRefs( p );
    Gia_ManForEachAnd( p, pObj, i )
        if ( Vec_IntEntry(vPointed, i) && Gia_ObjRefNumId(p, i) > 0 )
        {
            printf( "Gia_ManCheckChoices: Member %d", i );
            printf( " of a choice node has %d fanouts.\n", Gia_ObjRefNumId(p, i) );
            ABC_FREE( p->pRefs );
            Vec_IntFree( vPointed );
            return 0;
        }
    ABC_FREE( p->pRefs );
    Vec_IntFree( vPointed );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManToAig()

Aig_Man_t * Gia_ManToAig	(	Gia_Man_t *	p,
		int	fChoices )

Definition at line 318 of file giaAig.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
    assert( !fChoices || (p->pNexts && p->pReprs) );
    // create the new manager
    pNew = Aig_ManStart( Gia_ManAndNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
//    pNew->pSpec = Abc_UtilStrsav( p->pName );
    // duplicate representation of choice nodes
    if ( fChoices )
        pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
    // create the PIs
    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
    ppNodes[0] = Aig_ManConst0(pNew);
    Gia_ManForEachCi( p, pObj, i )
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
    // transfer level
    if ( p->vLevels )
    Gia_ManForEachCi( p, pObj, i )
        Aig_ObjSetLevel( ppNodes[Gia_ObjId(p, pObj)], Gia_ObjLevel(p, pObj) );
    // add logic for the POs
    Gia_ManForEachCo( p, pObj, i )
    {
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManToAig_rec()

void Gia_ManToAig_rec	(	Aig_Man_t *	pNew,
		Aig_Obj_t **	ppNodes,
		Gia_Man_t *	p,
		Gia_Obj_t *	pObj )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 294 of file giaAig.c.

{
    Gia_Obj_t * pNext;
    if ( ppNodes[Gia_ObjId(p, pObj)] )
        return;
    if ( Gia_ObjIsCi(pObj) )
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
    else
    {
        assert( Gia_ObjIsAnd(pObj) );
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
        ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
    }
    if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
    {
        Aig_Obj_t * pObjNew, * pNextNew;
        Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
        pObjNew  = ppNodes[Gia_ObjId(p, pObj)];
        pNextNew = ppNodes[Gia_ObjId(p, pNext)];
        if ( pNew->pEquivs )
            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManToAigSimple()

Aig_Man_t * Gia_ManToAigSimple

(

Gia_Man_t *

p

)

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 408 of file giaAig.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
    ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
    // create the new manager
    pNew = Aig_ManStart( Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
    // create the PIs
    Gia_ManForEachObj( p, pObj, i )
    {
        if ( Gia_ObjIsAnd(pObj) )
            ppNodes[i] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
        else if ( Gia_ObjIsCi(pObj) )
            ppNodes[i] = Aig_ObjCreateCi( pNew );
        else if ( Gia_ObjIsCo(pObj) )
            ppNodes[i] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
        else if ( Gia_ObjIsConst0(pObj) )
            ppNodes[i] = Aig_ManConst0(pNew);
        else
            assert( 0 );
        pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
        assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManToAigSkip()

Aig_Man_t * Gia_ManToAigSkip	(	Gia_Man_t *	p,
		int	nOutDelta )

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

Synopsis [Duplicates AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file giaAig.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t ** ppNodes;
    Gia_Obj_t * pObj;
    int i;
    assert( p->pNexts == NULL && p->pReprs == NULL );
    assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
    // create the new manager
    pNew = Aig_ManStart( Gia_ManAndNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    pNew->nConstrs = p->nConstrs;
//    pNew->pSpec = Abc_UtilStrsav( p->pName );
    // create the PIs
    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
    ppNodes[0] = Aig_ManConst0(pNew);
    Gia_ManForEachCi( p, pObj, i )
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCi( pNew );
    // add logic for the POs
    Gia_ManForEachCo( p, pObj, i )
    {
        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
        if ( i % nOutDelta != 0 )
            continue;
        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreateCo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
    }
    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    ABC_FREE( ppNodes );
    return pNew;
}

Here is the call graph for this function:

Here is the caller graph for this function: