Skip to content

A
abc
Commit 255f171f by Alan Mishchenko
Options

Improving computation of choices from equivalence classes.

parent 40d9b585
Showing with 539 additions and 150 deletions
abclib.dsp
...@@ -3411,6 +3411,10 @@ SOURCE=.\src\aig\gia\giaCexMin.c ...@@ -3411,6 +3411,10 @@ SOURCE=.\src\aig\gia\giaCexMin.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\gia\giaChoice.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaCof.c SOURCE=.\src\aig\gia\giaCof.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/gia/gia.h
...@@ -271,6 +271,7 @@ static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj ...@@ -271,6 +271,7 @@ static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj
static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); } static inline int Gia_IsComplement( Gia_Obj_t * p ) { return (int)((ABC_PTRUINT_T)(p) & 01); }
static inline char * Gia_ManName( Gia_Man_t * p ) { return p->pName; }
static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); } static inline int Gia_ManCiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis); }
static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); } static inline int Gia_ManCoNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCos); }
static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; } static inline int Gia_ManPiNum( Gia_Man_t * p ) { return Vec_IntSize(p->vCis) - p->nRegs; }
...@@ -356,9 +357,10 @@ static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { ...@@ -356,9 +357,10 @@ static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) {
static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); }
static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj)); }
static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); }
static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjLevelId( p, Gia_ObjId(p,pObj) ); }
static inline void Gia_ObjSetLevelId( Gia_Man_t * p, int Id, int l ) { Vec_IntSetEntry(p->vLevels, Id, l); }
static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Gia_ObjSetLevelId( p, Gia_ObjId(p,pObj), l ); }
static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); } static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); }
static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); } static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
...@@ -596,7 +598,6 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r ...@@ -596,7 +598,6 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r
static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; }
static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; }
static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; }
static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; }
...@@ -699,6 +700,9 @@ extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * ...@@ -699,6 +700,9 @@ extern int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t *
extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex ); extern void Gia_ManCounterExampleValueStart( Gia_Man_t * pGia, Abc_Cex_t * pCex );
extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia ); extern void Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame ); extern int Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
/*=== giaChoice.c ============================================================*/
extern void Gia_ManVerifyChoices( Gia_Man_t * p );
extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
/*=== giaCsatOld.c ============================================================*/ /*=== giaCsatOld.c ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/ /*=== giaCsat.c ============================================================*/
...@@ -760,7 +764,6 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p ); ...@@ -760,7 +764,6 @@ extern int Gia_ManEquivCountLitsAll( Gia_Man_t * p );
extern int Gia_ManEquivCountClasses( Gia_Man_t * p ); extern int Gia_ManEquivCountClasses( Gia_Man_t * p );
extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter ); extern void Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ); extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
extern void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose ); extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs ); extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose ); extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
...@@ -912,7 +915,6 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ...@@ -912,7 +915,6 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasChoices( Gia_Man_t * p );
extern void Gia_ManVerifyChoices( Gia_Man_t * p );
extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManHasDangling( Gia_Man_t * p );
extern int Gia_ManMarkDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p ); extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
......
src/aig/gia/giaAig.c
...@@ -419,18 +419,6 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) ...@@ -419,18 +419,6 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) ); Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, pGiaRepr->Value), Aig_ManObj(pAig, pGiaObj->Value) );
} }
} }
/**Function*************************************************************
Synopsis [Transfers representatives from pGia to pAig.]
Description [Assumes that pAig was created from pGia.]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ) void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
{ {
Gia_Obj_t * pGiaObj, * pGiaRepr; Gia_Obj_t * pGiaObj, * pGiaRepr;
...@@ -470,9 +458,9 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) ...@@ -470,9 +458,9 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) ); pGia->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pGia) );
for ( i = 0; i < Gia_ManObjNum(pGia); i++ ) for ( i = 0; i < Gia_ManObjNum(pGia); i++ )
Gia_ObjSetRepr( pGia, i, GIA_VOID ); Gia_ObjSetRepr( pGia, i, GIA_VOID );
// move pointers from GIA to AIG
Gia_ManForEachObj( pGia, pObjGia, i ) Gia_ManForEachObj( pGia, pObjGia, i )
{ {
// Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 );
if ( Gia_ObjIsCo(pObjGia) ) if ( Gia_ObjIsCo(pObjGia) )
continue; continue;
assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) ); assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
...@@ -490,6 +478,27 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) ...@@ -490,6 +478,27 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
} }
pGia->pNexts = Gia_ManDeriveNexts( pGia ); pGia->pNexts = Gia_ManDeriveNexts( pGia );
} }
void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
{
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 );
}
/**Function************************************************************* /**Function*************************************************************
......
src/aig/gia/giaAig.h
...@@ -59,6 +59,7 @@ extern Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ); ...@@ -59,6 +59,7 @@ extern Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p );
extern void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia );
extern void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia );
extern void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ); extern void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia );
extern void Gia_ManReprFromAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia );
extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ); extern Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose );
extern Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ); extern Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars );
extern Gia_Man_t * Gia_ManAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops ); extern Gia_Man_t * Gia_ManAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops );
......
src/aig/gia/giaChoice.c 0 → 100644
/**CFile****************************************************************
FileName [giaChoice.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Normalization of structural choices.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Reverse the order of nodes in equiv classes.]
Description [If the flag is 1, assumed current increasing order ]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
{
Vec_Int_t * vCollected;
Vec_Int_t * vClass;
int i, k, iRepr, iNode, iPrev;
// collect classes
vCollected = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, iRepr )
{
Vec_IntPush( vCollected, iRepr );
/*
// check classes
if ( !fNowIncreasing )
{
iPrev = iRepr;
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( iPrev < iNode )
{
printf( "Class %d : ", iRepr );
Gia_ClassForEachObj( p, iRepr, iNode )
printf( " %d", iNode );
printf( "\n" );
break;
}
iPrev = iNode;
}
}
*/
}
// correct each class
vClass = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vCollected, iRepr, i )
{
Vec_IntClear( vClass );
Vec_IntPush( vClass, iRepr );
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( fNowIncreasing )
assert( iRepr < iNode );
// else
// assert( iRepr > iNode );
Vec_IntPush( vClass, iNode );
}
if ( !fNowIncreasing )
Vec_IntSort( vClass, 1 );
// if ( iRepr == 129720 || iRepr == 129737 )
// Vec_IntPrint( vClass );
// reverse the class
iPrev = 0;
iRepr = Vec_IntEntryLast( vClass );
Vec_IntForEachEntry( vClass, iNode, k )
{
if ( fNowIncreasing )
Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
else
Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
Gia_ObjSetNext( p, iNode, iPrev );
iPrev = iNode;
}
}
Vec_IntFree( vCollected );
Vec_IntFree( vClass );
// verify
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
if ( fNowIncreasing )
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
else
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManVerifyChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iRepr, iNode, fProb = 0;
assert( p->pReprs );
// mark nodes
Gia_ManCleanMark0(p);
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( Gia_ObjIsHead(p, iNode) )
printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
Gia_ManObj( p, iNode )->fMark0 = 1;
}
Gia_ManCleanMark0(p);
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
}
else if ( Gia_ObjIsCo(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
}
}
if ( !fProb )
printf( "GIA with choices is correct.\n" );
}
/**Function*************************************************************
Synopsis [Make sure reprsentative nodes do not have representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManCheckReprs( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, fProb = 0;
Gia_ManForEachObj( p, pObj, i )
{
if ( !Gia_ObjHasRepr(p, i) )
continue;
if ( !Gia_ObjIsAnd(pObj) )
printf( "Obj %d is not an AND but it has a repr %d.\n", i, Gia_ObjRepr(p, i) ), fProb = 1;
else if ( Gia_ObjHasRepr( p, Gia_ObjRepr(p, i) ) )
printf( "Obj %d has repr %d with a repr %d.\n", i, Gia_ObjRepr(p, i), Gia_ObjRepr(p, Gia_ObjRepr(p, i)) ), fProb = 1;
}
if ( !fProb )
printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) );
}
/**Function*************************************************************
Synopsis [Find minimum level of each node using representatives.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManMinLevelRepr_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
{
int levMin, levCur, objId, reprId;
// skip visited nodes
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return Gia_ObjLevel(p, pObj);
Gia_ObjSetTravIdCurrent(p, pObj);
// skip CI nodes
if ( Gia_ObjIsCi(pObj) )
return Gia_ObjLevel(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
objId = Gia_ObjId(p, pObj);
if ( Gia_ObjIsNone(p, objId) )
{
// not part of the equivalence class
Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManMinLevelRepr_rec( p, Gia_ObjFanin1(pObj) );
Gia_ObjSetAndLevel( p, pObj );
return Gia_ObjLevel(p, pObj);
}
// has equivalences defined
assert( Gia_ObjHasRepr(p, objId) || Gia_ObjIsHead(p, objId) );
reprId = Gia_ObjHasRepr(p, objId) ? Gia_ObjRepr(p, objId) : objId;
// iterate through objects
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
{
levCur = Gia_ManMinLevelRepr_rec( p, Gia_ManObj(p, objId) );
levMin = Abc_MinInt( levMin, levCur );
}
assert( levMin < ABC_INFINITY );
// assign minimum level to all
Gia_ClassForEachObj( p, reprId, objId )
Gia_ObjSetLevelId( p, objId, levMin );
return levMin;
}
int Gia_ManMinLevelRepr( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, LevelCur, LevelMax = 0;
assert( Gia_ManRegNum(p) == 0 );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
Gia_ManIncrementTravId( p );
Gia_ManForEachAnd( p, pObj, i )
{
assert( !Gia_ObjIsConst(p, i) );
LevelCur = Gia_ManMinLevelRepr_rec( p, pObj );
LevelMax = Abc_MaxInt( LevelMax, LevelCur );
}
printf( "Max level %d\n", LevelMax );
return LevelMax;
}
/**Function*************************************************************
Synopsis [Returns mapping of each old repr into new repr.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Gia_ManFindMinLevelMap( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int reprId, objId, levFan0, levFan1;
int levMin, levMinOld, levMax, reprBest;
int * pReprMap, * pMinLevels, iFanin;
int i, fChange = 1;
Gia_ManLevelNum( p );
pMinLevels = ABC_ALLOC( int, Gia_ManObjNum(p) );
while ( fChange )
{
fChange = 0;
// clean min-levels
memset( pMinLevels, 0xFF, sizeof(int) * Gia_ManObjNum(p) );
// for each class find min level
Gia_ManForEachClass( p, reprId )
{
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
levMin = Abc_MinInt( levMin, Gia_ObjLevelId(p, objId) );
assert( levMin >= 0 && levMin < ABC_INFINITY );
Gia_ClassForEachObj( p, reprId, objId )
{
assert( pMinLevels[objId] == -1 );
pMinLevels[objId] = levMin;
}
}
// recompute levels
levMax = 0;
Gia_ManForEachAnd( p, pObj, i )
{
iFanin = Gia_ObjFaninId0(pObj, i);
if ( Gia_ObjIsNone(p, iFanin) )
levFan0 = Gia_ObjLevelId(p, iFanin);
else if ( Gia_ObjIsConst(p, iFanin) )
levFan0 = 0;
else
{
assert( Gia_ObjIsClass( p, iFanin ) );
assert( pMinLevels[iFanin] >= 0 );
levFan0 = pMinLevels[iFanin];
}
iFanin = Gia_ObjFaninId1(pObj, i);
if ( Gia_ObjIsNone(p, iFanin) )
levFan1 = Gia_ObjLevelId(p, iFanin);
else if ( Gia_ObjIsConst(p, iFanin) )
levFan1 = 0;
else
{
assert( Gia_ObjIsClass( p, iFanin ) );
assert( pMinLevels[iFanin] >= 0 );
levFan1 = pMinLevels[iFanin];
}
levMinOld = Gia_ObjLevelId(p, i);
levMin = 1 + Abc_MaxInt( levFan0, levFan1 );
Gia_ObjSetLevelId( p, i, levMin );
assert( levMin <= levMinOld );
if ( levMin < levMinOld )
fChange = 1;
levMax = Abc_MaxInt( levMax, levMin );
}
printf( "%d ", levMax );
}
ABC_FREE( pMinLevels );
printf( "\n" );
// create repr map
pReprMap = ABC_FALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachAnd( p, pObj, i )
if ( Gia_ObjIsConst(p, i) )
pReprMap[i] = 0;
Gia_ManForEachClass( p, reprId )
{
// find min-level repr
reprBest = -1;
levMin = ABC_INFINITY;
Gia_ClassForEachObj( p, reprId, objId )
if ( levMin > Gia_ObjLevelId(p, objId) )
{
levMin = Gia_ObjLevelId(p, objId);
reprBest = objId;
}
assert( reprBest > 0 );
Gia_ClassForEachObj( p, reprId, objId )
pReprMap[objId] = reprBest;
}
return pReprMap;
}
/**Function*************************************************************
Synopsis [Find terminal AND nodes]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManDanglingAndNodes( Gia_Man_t * p )
{
Vec_Int_t * vTerms;
Gia_Obj_t * pObj;
int i;
Gia_ManCleanMark0( p );
Gia_ManForEachAnd( p, pObj, i )
{
Gia_ObjFanin0(pObj)->fMark0 = 1;
Gia_ObjFanin1(pObj)->fMark1 = 1;
}
vTerms = Vec_IntAlloc( 1000 );
Gia_ManForEachAnd( p, pObj, i )
if ( !pObj->fMark0 )
Vec_IntPush( vTerms, i );
Gia_ManCleanMark0( p );
return vTerms;
}
/**Function*************************************************************
Synopsis [Reconstruct AIG starting with terminals.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManRebuidRepr_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprMap )
{
int objId, reprLit = -1;
if ( ~pObj->Value )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
objId = Gia_ObjId( p, pObj );
if ( Gia_ObjIsClass(p, objId) )
{
assert( pReprMap[objId] > 0 );
reprLit = Gia_ManRebuidRepr_rec( pNew, p, Gia_ManObj(p, pReprMap[objId]), pReprMap );
assert( reprLit > 1 );
}
else
assert( Gia_ObjIsNone(p, objId) );
Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin0(pObj), pReprMap );
Gia_ManRebuidRepr_rec( pNew, p, Gia_ObjFanin1(pObj), pReprMap );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
assert( reprLit != (int)pObj->Value );
if ( reprLit > 1 )
pNew->pReprs[ Abc_Lit2Var(pObj->Value) ].iRepr = Abc_Lit2Var(reprLit);
return pObj->Value;
}
Gia_Man_t * Gia_ManRebuidRepr( Gia_Man_t * p, int * pReprMap )
{
Vec_Int_t * vTerms;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i;
Gia_ManFillValue( p );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
vTerms = Gia_ManDanglingAndNodes( p );
Gia_ManForEachObjVec( vTerms, p, pObj, i )
Gia_ManRebuidRepr_rec( pNew, p, pObj, pReprMap );
Vec_IntFree( vTerms );
Gia_ManForEachCo( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Gia_ManNormalizeChoices( Aig_Man_t * pAig )
{
int * pReprMap;
Aig_Man_t * pNew;
Gia_Man_t * pGia, * pTemp;
// create GIA with representatives
assert( Aig_ManRegNum(pAig) == 0 );
assert( pAig->pReprs != NULL );
pGia = Gia_ManFromAigSimple( pAig );
Gia_ManReprFromAigRepr2( pAig, pGia );
// verify that representatives are correct
Gia_ManCheckReprs( pGia );
// find min-level repr for each class
pReprMap = Gia_ManFindMinLevelMap( pGia );
// reconstruct using correct order
pGia = Gia_ManRebuidRepr( pTemp = pGia, pReprMap );
Gia_ManStop( pTemp );
ABC_FREE( pReprMap );
// create choices
// verify that choices are correct
// Gia_ManVerifyChoices( pGia );
// copy the result back into AIG
pNew = Gia_ManToAigSimple( pGia );
Gia_ManReprToAigRepr( pNew, pGia );
return pNew;
}
void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig )
{
Aig_Man_t * pNew = Gia_ManNormalizeChoices( pAig );
Aig_ManStop( pNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
src/aig/gia/giaEquiv.c
...@@ -347,89 +347,6 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) ...@@ -347,89 +347,6 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Reverse the order of nodes in equiv classes.]
Description [If the flag is 1, assumed current increasing order ]
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
{
Vec_Int_t * vCollected;
Vec_Int_t * vClass;
int i, k, iRepr, iNode, iPrev;
// collect classes
vCollected = Vec_IntAlloc( 100 );
Gia_ManForEachClass( p, iRepr )
{
Vec_IntPush( vCollected, iRepr );
/*
// check classes
if ( !fNowIncreasing )
{
iPrev = iRepr;
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( iPrev < iNode )
{
printf( "Class %d : ", iRepr );
Gia_ClassForEachObj( p, iRepr, iNode )
printf( " %d", iNode );
printf( "\n" );
break;
}
iPrev = iNode;
}
}
*/
}
// correct each class
vClass = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vCollected, iRepr, i )
{
Vec_IntClear( vClass );
Vec_IntPush( vClass, iRepr );
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( fNowIncreasing )
assert( iRepr < iNode );
// else
// assert( iRepr > iNode );
Vec_IntPush( vClass, iNode );
}
if ( !fNowIncreasing )
Vec_IntSort( vClass, 1 );
// if ( iRepr == 129720 || iRepr == 129737 )
// Vec_IntPrint( vClass );
// reverse the class
iPrev = 0;
iRepr = Vec_IntEntryLast( vClass );
Vec_IntForEachEntry( vClass, iNode, k )
{
if ( fNowIncreasing )
Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
else
Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
Gia_ObjSetNext( p, iNode, iPrev );
iPrev = iNode;
}
}
Vec_IntFree( vCollected );
Vec_IntFree( vClass );
// verify
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
if ( fNowIncreasing )
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
else
assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
}
/**Function*************************************************************
Synopsis [Returns representative node.] Synopsis [Returns representative node.]
Description [] Description []
......
src/aig/gia/giaUtil.c
...@@ -981,55 +981,6 @@ int Gia_ManHasChoices( Gia_Man_t * p ) ...@@ -981,55 +981,6 @@ int Gia_ManHasChoices( Gia_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManVerifyChoices( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iRepr, iNode, fProb = 0;
assert( p->pReprs );
// mark nodes
Gia_ManCleanMark0(p);
Gia_ManForEachClass( p, iRepr )
Gia_ClassForEachObj1( p, iRepr, iNode )
{
if ( Gia_ObjIsHead(p, iNode) )
printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
Gia_ManObj( p, iNode )->fMark0 = 1;
}
Gia_ManCleanMark0(p);
Gia_ManForEachObj( p, pObj, i )
{
if ( Gia_ObjIsAnd(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
}
else if ( Gia_ObjIsCo(pObj) )
{
if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
}
}
if ( !fProb )
printf( "GIA with choices is correct.\n" );
}
/**Function*************************************************************
Synopsis [Returns 1 if AIG has dangling nodes.] Synopsis [Returns 1 if AIG has dangling nodes.]
Description [] Description []
......
src/aig/gia/module.make
...@@ -5,6 +5,7 @@ SRC += src/aig/gia/gia.c \ ...@@ -5,6 +5,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaCCof.c \ src/aig/gia/giaCCof.c \
src/aig/gia/giaCex.c \ src/aig/gia/giaCex.c \
src/aig/gia/giaCexMin.c \ src/aig/gia/giaCexMin.c \
src/aig/gia/giaChoice.c \
src/aig/gia/giaCof.c \ src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \ src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \ src/aig/gia/giaCSat.c \
......
src/proof/dch/dchCore.c
...@@ -106,6 +106,12 @@ p->timeSimInit = clock() - clk; ...@@ -106,6 +106,12 @@ p->timeSimInit = clock() - clk;
// free memory ahead of time // free memory ahead of time
p->timeTotal = clock() - clkTotal; p->timeTotal = clock() - clkTotal;
Dch_ManStop( p ); Dch_ManStop( p );
// try something different
{
// extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig );
// Gia_ManNormalizeChoicesTest( pAig );
}
// create choices // create choices
ABC_FREE( pAig->pTable ); ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment