summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-09-23 23:53:12 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-09-23 23:53:12 -0700
commit255f171f632610eead441e62c7fe4cd4148bb207 (patch)
tree321863ebb934ee8a72587a7d863919e949fb2228 /src
parent40d9b5853b2849c3bf7e2157a4b4c6b798b043d5 (diff)
downloadabc-255f171f632610eead441e62c7fe4cd4148bb207.tar.gz
abc-255f171f632610eead441e62c7fe4cd4148bb207.tar.bz2
abc-255f171f632610eead441e62c7fe4cd4148bb207.zip
Improving computation of choices from equivalence classes.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h12
-rw-r--r--src/aig/gia/giaAig.c35
-rw-r--r--src/aig/gia/giaAig.h1
-rw-r--r--src/aig/gia/giaChoice.c498
-rw-r--r--src/aig/gia/giaEquiv.c83
-rw-r--r--src/aig/gia/giaUtil.c49
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/proof/dch/dchCore.c6
8 files changed, 535 insertions, 150 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index ef87c5d5..e9e714ad 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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 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_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; }
@@ -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_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 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_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
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_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_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; }
@@ -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_ManCounterExampleValueStop( Gia_Man_t * pGia );
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 ============================================================*/
extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
/*=== giaCsat.c ============================================================*/
@@ -760,7 +764,6 @@ extern int Gia_ManEquivCountLitsAll( 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_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_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
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 **
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_ManHasChoices( Gia_Man_t * p );
-extern void Gia_ManVerifyChoices( Gia_Man_t * p );
extern int Gia_ManHasDangling( Gia_Man_t * p );
extern int Gia_ManMarkDangling( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index d9a1693c..224d3bda 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -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) );
}
}
-
-/**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 )
{
Gia_Obj_t * pGiaObj, * pGiaRepr;
@@ -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) );
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 )
{
-// Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 );
if ( Gia_ObjIsCo(pObjGia) )
continue;
assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
@@ -490,6 +478,27 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * 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*************************************************************
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index adcf9097..b72f6415 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -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_ManReprToAigRepr2( 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_ManPerformDch( Gia_Man_t * p, void * pPars );
extern Gia_Man_t * Gia_ManAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops );
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c
new file mode 100644
index 00000000..373f9104
--- /dev/null
+++ b/src/aig/gia/giaChoice.c
@@ -0,0 +1,498 @@
+/**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
+
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index b9557600..2cbdb75f 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -347,89 +347,6 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
/**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.]
Description []
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 499f9293..5f443dc8 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -981,55 +981,6 @@ int Gia_ManHasChoices( Gia_Man_t * p )
/**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.]
Description []
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 89af261a..d35dcde2 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -5,6 +5,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaCCof.c \
src/aig/gia/giaCex.c \
src/aig/gia/giaCexMin.c \
+ src/aig/gia/giaChoice.c \
src/aig/gia/giaCof.c \
src/aig/gia/giaCSatOld.c \
src/aig/gia/giaCSat.c \
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 0d2e8c0d..654ed359 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -106,6 +106,12 @@ p->timeSimInit = clock() - clk;
// free memory ahead of time
p->timeTotal = clock() - clkTotal;
Dch_ManStop( p );
+ // try something different
+ {
+// extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig );
+// Gia_ManNormalizeChoicesTest( pAig );
+ }
+
// create choices
ABC_FREE( pAig->pTable );
pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );