Skip to content

A
abc
Commit fefd8b90 by Alan Mishchenko
Options

Version abc70730

parent a8a80d9a
Showing with 535 additions and 209 deletions
abc.dsp
...@@ -2774,6 +2774,10 @@ SOURCE=.\src\aig\aig\aigSeq.c ...@@ -2774,6 +2774,10 @@ SOURCE=.\src\aig\aig\aigSeq.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\aig\aig\aigShow.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\aig\aigTable.c SOURCE=.\src\aig\aig\aigTable.c
# End Source File # End Source File
# Begin Source File # Begin Source File
......
src/aig/aig/aig.h
...@@ -92,7 +92,7 @@ struct Aig_Man_t_ ...@@ -92,7 +92,7 @@ struct Aig_Man_t_
Vec_Ptr_t * vBufs; // the array of buffers Vec_Ptr_t * vBufs; // the array of buffers
Aig_Obj_t * pConst1; // the constant 1 node Aig_Obj_t * pConst1; // the constant 1 node
Aig_Obj_t Ghost; // the ghost node Aig_Obj_t Ghost; // the ghost node
Vec_Int_t * vInits; // the initial values of the latches (latches are last PIs/POs) int nRegs; // the number of registers
int nAsserts; // the number of asserts among POs (asserts are first POs) int nAsserts; // the number of asserts among POs (asserts are first POs)
// AIG node counters // AIG node counters
int nObjs[AIG_OBJ_VOID];// the number of objects by type int nObjs[AIG_OBJ_VOID];// the number of objects by type
...@@ -156,13 +156,6 @@ static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_ ...@@ -156,13 +156,6 @@ static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_
static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); } static inline Aig_Obj_t * Aig_NotCond( Aig_Obj_t * p, int c ) { return (Aig_Obj_t *)((unsigned long)(p) ^ (c)); }
static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int )(((unsigned long)p) & 01); } static inline int Aig_IsComplement( Aig_Obj_t * p ) { return (int )(((unsigned long)p) & 01); }
static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; } static inline int Aig_ManPiNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PI]; }
static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; } static inline int Aig_ManPoNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_PO]; }
static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; } static inline int Aig_ManBufNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_BUF]; }
...@@ -173,7 +166,16 @@ static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nO ...@@ -173,7 +166,16 @@ static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nO
static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; }
static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; } static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; }
static inline int Aig_ManObjIdMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); } static inline int Aig_ManObjIdMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); }
static inline int Aig_ManInitNum( Aig_Man_t * p ) { return p->vInits? Vec_IntSize(p->vInits) : 0; } static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; }
static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); }
static inline Aig_Obj_t * Aig_ManConst1( Aig_Man_t * p ) { return p->pConst1; }
static inline Aig_Obj_t * Aig_ManGhost( Aig_Man_t * p ) { return &p->Ghost; }
static inline Aig_Obj_t * Aig_ManPi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i); }
static inline Aig_Obj_t * Aig_ManPo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i); }
static inline Aig_Obj_t * Aig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Aig_ManPiNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Aig_ManPoNum(p)-Aig_ManRegNum(p)+i); }
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; }
static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; }
...@@ -204,14 +206,16 @@ static inline int Aig_ObjRefs( Aig_Obj_t * pObj ) { return pObj- ...@@ -204,14 +206,16 @@ static inline int Aig_ObjRefs( Aig_Obj_t * pObj ) { return pObj-
static inline void Aig_ObjRef( Aig_Obj_t * pObj ) { pObj->nRefs++; } static inline void Aig_ObjRef( Aig_Obj_t * pObj ) { pObj->nRefs++; }
static inline void Aig_ObjDeref( Aig_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } static inline void Aig_ObjDeref( Aig_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; }
static inline void Aig_ObjClearRef( Aig_Obj_t * pObj ) { pObj->nRefs = 0; } static inline void Aig_ObjClearRef( Aig_Obj_t * pObj ) { pObj->nRefs = 0; }
static inline int Aig_ObjFaninId0( Aig_Obj_t * pObj ) { return pObj->pFanin0? Aig_Regular(pObj->pFanin0)->Id : -1; }
static inline int Aig_ObjFaninId1( Aig_Obj_t * pObj ) { return pObj->pFanin1? Aig_Regular(pObj->pFanin1)->Id : -1; }
static inline int Aig_ObjFaninC0( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin0); } static inline int Aig_ObjFaninC0( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin0); }
static inline int Aig_ObjFaninC1( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin1); } static inline int Aig_ObjFaninC1( Aig_Obj_t * pObj ) { return Aig_IsComplement(pObj->pFanin1); }
static inline Aig_Obj_t * Aig_ObjFanin0( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin0); } static inline Aig_Obj_t * Aig_ObjFanin0( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin0); }
static inline Aig_Obj_t * Aig_ObjFanin1( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin1); } static inline Aig_Obj_t * Aig_ObjFanin1( Aig_Obj_t * pObj ) { return Aig_Regular(pObj->pFanin1); }
static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj->pFanin0; } static inline Aig_Obj_t * Aig_ObjChild0( Aig_Obj_t * pObj ) { return pObj->pFanin0; }
static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; } static inline Aig_Obj_t * Aig_ObjChild1( Aig_Obj_t * pObj ) { return pObj->pFanin1; }
static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; }
static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; }
static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; } static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; }
...@@ -314,16 +318,16 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF ...@@ -314,16 +318,16 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF
// iterator over the primary inputs // iterator over the primary inputs
#define Aig_ManForEachPiSeq( p, pObj, i ) \ #define Aig_ManForEachPiSeq( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) ) Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
// iterator over the latch outputs // iterator over the latch outputs
#define Aig_ManForEachLoSeq( p, pObj, i ) \ #define Aig_ManForEachLoSeq( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) ) Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
// iterator over the primary outputs // iterator over the primary outputs
#define Aig_ManForEachPoSeq( p, pObj, i ) \ #define Aig_ManForEachPoSeq( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) ) Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
// iterator over the latch inputs // iterator over the latch inputs
#define Aig_ManForEachLiSeq( p, pObj, i ) \ #define Aig_ManForEachLiSeq( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) ) Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
...@@ -410,6 +414,8 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); ...@@ -410,6 +414,8 @@ extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p ); extern void Aig_ManCreateChoices( Aig_Man_t * p );
/*=== aigSeq.c ========================================================*/ /*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits ); extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigShow.c ========================================================*/
extern void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
/*=== aigTable.c ========================================================*/ /*=== aigTable.c ========================================================*/
extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost ); extern Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 ); extern Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 );
......
src/aig/aig/aigMan.c
...@@ -239,7 +239,6 @@ void Aig_ManStop( Aig_Man_t * p ) ...@@ -239,7 +239,6 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vBufs ) Vec_PtrFree( p->vBufs );
if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels ); if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vInits ) Vec_IntFree( p->vInits );
FREE( p->pReprs ); FREE( p->pReprs );
FREE( p->pEquivs ); FREE( p->pEquivs );
free( p->pTable ); free( p->pTable );
......
src/aig/aig/aigRepr.c
...@@ -238,11 +238,15 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) ...@@ -238,11 +238,15 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
Aig_ManForEachPi( p, pObj, i ) Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew); pObj->pData = Aig_ObjCreatePi(pNew);
// map the internal nodes // map the internal nodes
//printf( "\n" );
Aig_ManForEachNode( p, pObj, i ) Aig_ManForEachNode( p, pObj, i )
{ {
pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ); pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class if ( pRepr = Aig_ObjFindRepr(p, pObj) ) // member of the class
{
//printf( "Using node %d for node %d.\n", pRepr->Id, pObj->Id );
Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) );
}
} }
// transfer the POs // transfer the POs
Aig_ManForEachPo( p, pObj, i ) Aig_ManForEachPo( p, pObj, i )
...@@ -381,6 +385,7 @@ void Aig_ManCreateChoices( Aig_Man_t * p ) ...@@ -381,6 +385,7 @@ void Aig_ManCreateChoices( Aig_Man_t * p )
pRepr = Aig_ObjFindRepr( p, pObj ); pRepr = Aig_ObjFindRepr( p, pObj );
if ( pRepr == NULL ) if ( pRepr == NULL )
continue; continue;
assert( pObj->nRefs == 0 );
// skip constant and PI classes // skip constant and PI classes
if ( !Aig_ObjIsNode(pRepr) ) if ( !Aig_ObjIsNode(pRepr) )
{ {
......
src/aig/cnf/cnf.h
...@@ -133,7 +133,7 @@ extern Cnf_Man_t * Cnf_ManStart(); ...@@ -133,7 +133,7 @@ extern Cnf_Man_t * Cnf_ManStart();
extern void Cnf_ManStop( Cnf_Man_t * p ); extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p ); extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern void Cnf_DataFree( Cnf_Dat_t * p ); extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ); extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ); void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
/*=== cnfMap.c ========================================================*/ /*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p ); extern void Cnf_DeriveMapping( Cnf_Man_t * p );
...@@ -148,6 +148,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre ...@@ -148,6 +148,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
/*=== cnfWrite.c ========================================================*/ /*=== cnfWrite.c ========================================================*/
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
#ifdef __cplusplus #ifdef __cplusplus
} }
......
src/aig/cnf/cnfCore.c
...@@ -75,9 +75,9 @@ clk = clock(); ...@@ -75,9 +75,9 @@ clk = clock();
Aig_MmFixedStop( pMemCuts, 0 ); Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = clock() - clk; p->timeSave = clock() - clk;
PRT( "Cuts ", p->timeCuts ); //PRT( "Cuts ", p->timeCuts );
PRT( "Map ", p->timeMap ); //PRT( "Map ", p->timeMap );
PRT( "Saving ", p->timeSave ); //PRT( "Saving ", p->timeSave );
return pCnf; return pCnf;
} }
......
src/aig/cnf/cnfMan.c
...@@ -26,6 +26,7 @@ ...@@ -26,6 +26,7 @@
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; } static inline int Cnf_Lit2Var( int Lit ) { return (Lit & 1)? -(Lit >> 1)-1 : (Lit >> 1)+1; }
static inline int Cnf_Lit2Var2( int Lit ) { return (Lit & 1)? -(Lit >> 1) : (Lit >> 1); }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -138,7 +139,7 @@ void Cnf_DataFree( Cnf_Dat_t * p ) ...@@ -138,7 +139,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable )
{ {
FILE * pFile; FILE * pFile;
int * pLit, * pStop, i; int * pLit, * pStop, i;
...@@ -153,7 +154,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) ...@@ -153,7 +154,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
for ( i = 0; i < p->nClauses; i++ ) for ( i = 0; i < p->nClauses; i++ )
{ {
for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
fprintf( pFile, "%d ", Cnf_Lit2Var(*pLit) ); fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
fprintf( pFile, "0\n" ); fprintf( pFile, "0\n" );
} }
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
...@@ -174,7 +175,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName ) ...@@ -174,7 +175,7 @@ void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName )
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
{ {
sat_solver * pSat; sat_solver * pSat;
int i; int i, status;
pSat = sat_solver_new(); pSat = sat_solver_new();
sat_solver_setnvars( pSat, p->nVars ); sat_solver_setnvars( pSat, p->nVars );
for ( i = 0; i < p->nClauses; i++ ) for ( i = 0; i < p->nClauses; i++ )
...@@ -185,6 +186,12 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p ) ...@@ -185,6 +186,12 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p )
return NULL; return NULL;
} }
} }
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
sat_solver_delete( pSat );
return NULL;
}
return pSat; return pSat;
} }
......
src/aig/cnf/cnfUtil.c
...@@ -98,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect ) ...@@ -98,7 +98,7 @@ Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
p->aArea = 0; p->aArea = 0;
Aig_ManForEachPo( p->pManAig, pObj, i ) Aig_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped ); p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped; return vMapped;
} }
...@@ -177,7 +177,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder ) ...@@ -177,7 +177,7 @@ Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder )
p->aArea = 0; p->aArea = 0;
Aig_ManForEachPo( p->pManAig, pObj, i ) Aig_ManForEachPo( p->pManAig, pObj, i )
p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder ); p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 ); // printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManPiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
return vMapped; return vMapped;
} }
......
src/aig/cnf/cnfWrite.c
...@@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) ...@@ -217,11 +217,12 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) ); pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) ); memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
// assign variables to the last (nOutputs) POs // assign variables to the last (nOutputs) POs
Number = 0; Number = 1;
for ( i = 0; i < nOutputs; i++ ) if ( nOutputs )
{ {
pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i ); assert( nOutputs == Aig_ManRegNum(p->pManAig) );
pCnf->pVarNums[pObj->Id] = Number++; Aig_ManForEachLiSeq( p->pManAig, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
} }
// assign variables to the internal nodes // assign variables to the internal nodes
Vec_PtrForEachEntry( vMapped, pObj, i ) Vec_PtrForEachEntry( vMapped, pObj, i )
...@@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) ...@@ -291,16 +292,15 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
// write the output literals // write the output literals
Aig_ManForEachPo( p->pManAig, pObj, i ) Aig_ManForEachPo( p->pManAig, pObj, i )
{ {
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
if ( i < Aig_ManPoNum(p->pManAig) - nOutputs ) if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
{ {
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
*pClas++ = pLits; *pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
} }
else else
{ {
PoVar = pCnf->pVarNums[ pObj->Id ]; PoVar = pCnf->pVarNums[ pObj->Id ];
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
// first clause // first clause
*pClas++ = pLits; *pClas++ = pLits;
*pLits++ = 2 * PoVar; *pLits++ = 2 * PoVar;
...@@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) ...@@ -319,6 +319,123 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
} }
/**Function*************************************************************
Synopsis [Derives a simple CNF for the AIG.]
Description [The last argument shows the number of last outputs
of the manager, which will not be converted into clauses but the
new variables for which will be introduced.]
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
{
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
int i, nLiterals, nClauses, Number;
// count the number of literals and clauses
nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + 3 * nOutputs;
nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManPoNum( p ) + nOutputs;
// allocate CNF
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// create room for variable numbers
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) );
// assign variables to the last (nOutputs) POs
Number = 1;
if ( nOutputs )
{
assert( nOutputs == Aig_ManRegNum(p) );
Aig_ManForEachLiSeq( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
}
// assign variables to the internal nodes
Aig_ManForEachNode( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
// assign variables to the PIs and constant node
Aig_ManForEachPi( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
pCnf->nVars = Number;
/*
// print CNF numbers
printf( "SAT numbers of each node:\n" );
Aig_ManForEachObj( p, pObj, i )
printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
printf( "\n" );
*/
// assign the clauses
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Aig_ManForEachNode( p, pObj, i )
{
OutVar = pCnf->pVarNums[ pObj->Id ];
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
// positive phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
// negative phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
}
// write the constant literal
OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
assert( OutVar <= Aig_ManObjIdMax(p) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
// write the output literals
Aig_ManForEachPo( p, pObj, i )
{
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
if ( i < Aig_ManPoNum(p) - nOutputs )
{
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
else
{
PoVar = pCnf->pVarNums[ pObj->Id ];
// first clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar;
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
// second clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar + 1;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
}
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
return pCnf;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fra.h
...@@ -69,7 +69,7 @@ struct Fra_Par_t_ ...@@ -69,7 +69,7 @@ struct Fra_Par_t_
int fConeBias; // bias variables in the cone (good for unsat runs) int fConeBias; // bias variables in the cone (good for unsat runs)
int nBTLimitNode; // conflict limit at a node int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output int nBTLimitMiter; // conflict limit at an output
int nTimeFrames; // the number of timeframes to unroll int nFramesK; // the number of timeframes to unroll
}; };
// FRAIG equivalence classes // FRAIG equivalence classes
...@@ -97,7 +97,7 @@ struct Fra_Man_t_ ...@@ -97,7 +97,7 @@ struct Fra_Man_t_
Aig_Man_t * pManAig; // the starting AIG manager Aig_Man_t * pManAig; // the starting AIG manager
Aig_Man_t * pManFraig; // the final AIG manager Aig_Man_t * pManFraig; // the final AIG manager
// mapping AIG into FRAIG // mapping AIG into FRAIG
int nFrames; // the number of timeframes used int nFramesAll; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
// simulation info // simulation info
unsigned * pSimWords; // memory for simulation information unsigned * pSimWords; // memory for simulation information
...@@ -152,20 +152,20 @@ struct Fra_Man_t_ ...@@ -152,20 +152,20 @@ struct Fra_Man_t_
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); } static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i]; } static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; }
static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i] = pNode; } static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; } static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; }
static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; } static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
...@@ -187,6 +187,8 @@ extern void Fra_ClassesPrepare( Fra_Cla_t * p ); ...@@ -187,6 +187,8 @@ extern void Fra_ClassesPrepare( Fra_Cla_t * p );
extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p );
extern int Fra_ClassesCountLits( Fra_Cla_t * p ); extern int Fra_ClassesCountLits( Fra_Cla_t * p );
extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
/*=== fraCnf.c ========================================================*/ /*=== fraCnf.c ========================================================*/
extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/ /*=== fraCore.c ========================================================*/
...@@ -195,11 +197,12 @@ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); ...@@ -195,11 +197,12 @@ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern void Fra_FraigSweep( Fra_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig );
/*=== fraDfs.c ========================================================*/ /*=== fraDfs.c ========================================================*/
/*=== fraInd.c ========================================================*/ /*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose ); extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose );
/*=== fraMan.c ========================================================*/ /*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
extern void Fra_ManClean( Fra_Man_t * p );
extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ); extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p );
extern void Fra_ManFinalizeComb( Fra_Man_t * p ); extern void Fra_ManFinalizeComb( Fra_Man_t * p );
extern void Fra_ManStop( Fra_Man_t * p ); extern void Fra_ManStop( Fra_Man_t * p );
......
src/aig/fra/fraClass.c
...@@ -62,11 +62,11 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) ...@@ -62,11 +62,11 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
p->pAig = pAig; p->pAig = pAig;
p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) ); p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) );
memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) ); memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) );
p->vClasses = Vec_PtrAlloc( 100 ); p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 ); p->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 ); p->vClassesTemp = Vec_PtrAlloc( 100 );
p->vClassOld = Vec_PtrAlloc( 100 ); p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 ); p->vClassNew = Vec_PtrAlloc( 100 );
return p; return p;
} }
...@@ -83,8 +83,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) ...@@ -83,8 +83,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
***********************************************************************/ ***********************************************************************/
void Fra_ClassesStop( Fra_Cla_t * p ) void Fra_ClassesStop( Fra_Cla_t * p )
{ {
free( p->pMemClasses ); FREE( p->pMemClasses );
free( p->pMemRepr ); FREE( p->pMemRepr );
if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp ); if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew ); if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld ); if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
...@@ -110,11 +110,9 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) ...@@ -110,11 +110,9 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
int i; int i;
Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
if ( vFailed )
Vec_PtrForEachEntry( vFailed, pObj, i ) Vec_PtrForEachEntry( vFailed, pObj, i )
{
// assert( p->pAig->pReprs[pObj->Id] != NULL );
p->pAig->pReprs[pObj->Id] = NULL; p->pAig->pReprs[pObj->Id] = NULL;
}
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -159,7 +157,7 @@ int Fra_ClassCount( Aig_Obj_t ** pClass ) ...@@ -159,7 +157,7 @@ int Fra_ClassCount( Aig_Obj_t ** pClass )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Count the number of pairs.] Synopsis [Count the number of literals.]
Description [] Description []
...@@ -168,22 +166,23 @@ int Fra_ClassCount( Aig_Obj_t ** pClass ) ...@@ -168,22 +166,23 @@ int Fra_ClassCount( Aig_Obj_t ** pClass )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Fra_ClassesCountPairs( Fra_Cla_t * p ) int Fra_ClassesCountLits( Fra_Cla_t * p )
{ {
Aig_Obj_t ** pClass; Aig_Obj_t ** pClass;
int i, nNodes, nPairs = 0; int i, nNodes, nLits = 0;
nLits = Vec_PtrSize( p->vClasses1 );
Vec_PtrForEachEntry( p->vClasses, pClass, i ) Vec_PtrForEachEntry( p->vClasses, pClass, i )
{ {
nNodes = Fra_ClassCount( pClass ); nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 ); assert( nNodes > 1 );
nPairs += nNodes * (nNodes - 1) / 2; nLits += nNodes - 1;
} }
return nPairs; return nLits;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Count the number of literals.] Synopsis [Count the number of pairs.]
Description [] Description []
...@@ -192,18 +191,17 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) ...@@ -192,18 +191,17 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Fra_ClassesCountLits( Fra_Cla_t * p ) int Fra_ClassesCountPairs( Fra_Cla_t * p )
{ {
Aig_Obj_t ** pClass; Aig_Obj_t ** pClass;
int i, nNodes, nLits = 0; int i, nNodes, nPairs = 0;
nLits = Vec_PtrSize( p->vClasses1 );
Vec_PtrForEachEntry( p->vClasses, pClass, i ) Vec_PtrForEachEntry( p->vClasses, pClass, i )
{ {
nNodes = Fra_ClassCount( pClass ); nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 ); assert( nNodes > 1 );
nLits += nNodes - 1; nPairs += nNodes * (nNodes - 1) / 2;
} }
return nLits; return nPairs;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -220,14 +218,22 @@ int Fra_ClassesCountLits( Fra_Cla_t * p ) ...@@ -220,14 +218,22 @@ int Fra_ClassesCountLits( Fra_Cla_t * p )
void Fra_ClassesPrint( Fra_Cla_t * p ) void Fra_ClassesPrint( Fra_Cla_t * p )
{ {
Aig_Obj_t ** pClass; Aig_Obj_t ** pClass;
Aig_Obj_t * pObj;
int i; int i;
printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_ClassesCountPairs(p) ); printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n",
Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
/*
printf( "Constants { " );
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
printf( "%d ", pObj->Id );
printf( "}\n" );
Vec_PtrForEachEntry( p->vClasses, pClass, i ) Vec_PtrForEachEntry( p->vClasses, pClass, i )
{ {
printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
Fra_PrintClass( pClass ); Fra_PrintClass( pClass );
} }
printf( "\n" ); printf( "\n" );
*/
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -259,6 +265,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p ) ...@@ -259,6 +265,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
{ {
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue; continue;
//printf( "%3d : ", pObj->Id );
//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
//printf( "\n" );
// hash the node by its simulation info // hash the node by its simulation info
iEntry = Fra_NodeHashSims( pObj ) % nTableSize; iEntry = Fra_NodeHashSims( pObj ) % nTableSize;
// check if the node belongs to the class of constant 1 // check if the node belongs to the class of constant 1
...@@ -428,6 +437,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses ) ...@@ -428,6 +437,7 @@ int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
break; break;
} }
// othewise, add the class and continue // othewise, add the class and continue
assert( pClass2[0] != NULL );
Vec_PtrPush( vClasses, pClass2 ); Vec_PtrPush( vClasses, pClass2 );
pClass = pClass2; pClass = pClass2;
} }
...@@ -457,6 +467,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p ) ...@@ -457,6 +467,7 @@ int Fra_ClassesRefine( Fra_Cla_t * p )
Vec_PtrForEachEntry( p->vClasses, pClass, i ) Vec_PtrForEachEntry( p->vClasses, pClass, i )
{ {
// add the class to the new array // add the class to the new array
assert( pClass[0] != NULL );
Vec_PtrPush( p->vClassesTemp, pClass ); Vec_PtrPush( p->vClassesTemp, pClass );
// refine the class iteratively // refine the class iteratively
nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp ); nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
...@@ -517,12 +528,38 @@ int Fra_ClassesRefine1( Fra_Cla_t * p ) ...@@ -517,12 +528,38 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL; ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL ); Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
} }
assert( ppClass[0] != NULL );
Vec_PtrPush( p->vClasses, ppClass ); Vec_PtrPush( p->vClasses, ppClass );
// iteratively refine this class // iteratively refine this class
nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses ); nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
return nRefis; return nRefis;
} }
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes with one class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
{
Aig_Obj_t ** pClass;
p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
pClass = p->pMemClasses;
assert( Id1 < Id2 );
pClass[0] = Aig_ManObj( p->pAig, Id1 );
pClass[1] = Aig_ManObj( p->pAig, Id2 );
pClass[2] = NULL;
pClass[3] = NULL;
Fra_ClassObjSetRepr( pClass[1], pClass[0] );
Vec_PtrPush( p->vClasses, pClass );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fraCore.c
...@@ -30,6 +30,37 @@ ...@@ -30,6 +30,37 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Write speculative miter for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
{
static int Counter = 0;
char FileName[20];
Aig_Man_t * pTemp;
Aig_Obj_t * pNode;
int i;
// create manager with the logic for these two nodes
Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig };
pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
// dump the logic into a file
sprintf( FileName, "aig\\%03d.blif", ++Counter );
Aig_ManDumpBlif( pTemp, FileName );
printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
// clean up
Aig_ManStop( pTemp );
Aig_ManForEachObj( p->pManFraig, pNode, i )
pNode->pData = p;
}
/**Function*************************************************************
Synopsis [Performs fraiging for one node.] Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.] Description [Returns the fraiged node.]
...@@ -39,84 +70,59 @@ ...@@ -39,84 +70,59 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObj ) void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
{ {
Aig_Obj_t * pObjRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjReprFraig; Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue; int RetValue;
assert( !Aig_IsComplement(pObj) ); assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
// get the fraiged fanins
pFanin0Fraig = Fra_ObjChild0Fra(pObj,0);
pFanin1Fraig = Fra_ObjChild1Fra(pObj,0);
// get the fraiged node
pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
return pObjFraig;
Aig_Regular(pObjFraig)->pData = p;
// get representative of this class // get representative of this class
pObjRepr = Fra_ClassObjRepr(pObj); pObjRepr = Fra_ClassObjRepr( pObj );
if ( pObjRepr == NULL || // this is a unique node if ( pObjRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
{ return;
assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) ); // get the fraiged node
assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) ); pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK );
assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
return pObjFraig;
}
// get the fraiged representative // get the fraiged representative
pObjReprFraig = Fra_ObjFraig(pObjRepr,0); pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
// if the fraiged nodes are the same, return // if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return pObjFraig; return;
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
// printf( "Node = %d. Repr = %d.\n", pObj->Id, pObjRepr->Id );
// if they are proved different, the c-ex will be in p->pPatWords // if they are proved different, the c-ex will be in p->pPatWords
RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent if ( RetValue == 1 ) // proved equivalent
{ {
// pObj->fMarkA = 1;
// if ( p->pPars->fChoicing ) // if ( p->pPars->fChoicing )
// Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); // Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); // the nodes proved equal
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
return;
} }
if ( RetValue == -1 ) // failed if ( RetValue == -1 ) // failed
{ {
static int Counter = 0; if ( p->vTimeouts == NULL )
char FileName[20]; p->vTimeouts = Vec_PtrAlloc( 100 );
Aig_Man_t * pTemp;
Aig_Obj_t * pNode;
int i;
Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) };
// Vec_Ptr_t * vNodes;
Vec_PtrPush( p->vTimeouts, pObj ); Vec_PtrPush( p->vTimeouts, pObj );
if ( !p->pPars->fSpeculate ) if ( !p->pPars->fSpeculate )
return pObjFraig; return;
// substitute the node assert( 0 );
// pObj->fMarkB = 1; // speculate
p->nSpeculs++; p->nSpeculs++;
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
sprintf( FileName, "aig\\%03d.blif", ++Counter ); Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
Aig_ManDumpBlif( pTemp, FileName ); return;
printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
Aig_ManStop( pTemp );
Aig_ManForEachObj( p->pManFraig, pNode, i )
pNode->pData = p;
// vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
// printf( "Cone=%d ", Vec_PtrSize(vNodes) );
// Vec_PtrFree( vNodes );
return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
} }
//printf( "Disproved %d and %d.\n", pObj->Id, pObjRepr->Id );
// disprove the nodes
// if we do not include the node into those disproved, we may end up
// merging this node with another representative, for which proof has timed out
if ( p->vTimeouts )
Vec_PtrPush( p->vTimeouts, pObj );
// simulate the counter-example and return the Fraig node // simulate the counter-example and return the Fraig node
Fra_Resimulate( p ); Fra_Resimulate( p );
assert( Fra_ClassObjRepr(pObj) != pObjRepr ); assert( Fra_ClassObjRepr(pObj) != pObjRepr );
return pObjFraig;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -139,15 +145,22 @@ p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1); ...@@ -139,15 +145,22 @@ p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
// duplicate internal nodes // duplicate internal nodes
pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
// fraig latch outputs
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_FraigNode( p, pObj );
// fraig internal nodes
Aig_ManForEachNode( p->pManAig, pObj, i ) Aig_ManForEachNode( p->pManAig, pObj, i )
{ {
Extra_ProgressBarUpdate( pProgress, i, NULL ); Extra_ProgressBarUpdate( pProgress, i, NULL );
// default to simple strashing if simulation detected a counter-example for a PO // derive and remember the new fraig node
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
Aig_Regular(pObjNew)->pData = p;
// quit if simulation detected a counter-example for a PO
if ( p->pManFraig->pData ) if ( p->pManFraig->pData )
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,0), Fra_ObjChild1Fra(pObj,0) ); continue;
else // perform fraiging
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented Fra_FraigNode( p, pObj );
Fra_ObjSetFraig( pObj, 0, pObjNew );
} }
Extra_ProgressBarStop( pProgress ); Extra_ProgressBarStop( pProgress );
p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
...@@ -198,6 +211,14 @@ clk = clock(); ...@@ -198,6 +211,14 @@ clk = clock();
Aig_ManCleanup( p->pManFraig ); Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig; pManAigNew = p->pManFraig;
p->pManFraig = NULL; p->pManFraig = NULL;
/*
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig );
// Aig_ManCreateChoices( pManAigNew );
Aig_ManCleanup( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
*/
} }
p->timeTotal = clock() - clk; p->timeTotal = clock() - clk;
Fra_ManStop( p ); Fra_ManStop( p );
......
src/aig/fra/fraInd.c
...@@ -31,6 +31,42 @@ ...@@ -31,6 +31,42 @@
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
// skip nodes without representative
if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
return;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Fra_ObjFraig( pObj, iFrame );
// get the new node of the representative
pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
// add the constraint
pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
pMiter = Aig_Not( pMiter );
Aig_ObjCreatePo( pManFraig, pMiter );
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.] Synopsis [Prepares the inductive case with speculative reduction.]
Description [] Description []
...@@ -43,77 +79,58 @@ ...@@ -43,77 +79,58 @@
Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
{ {
Aig_Man_t * pManFraig; Aig_Man_t * pManFraig;
Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter; Aig_Obj_t * pObj, * pObjNew;
Aig_Obj_t ** pLatches; Aig_Obj_t ** pLatches;
int i, k, f; int i, k, f;
assert( p->pManFraig == NULL ); assert( p->pManFraig == NULL );
assert( Aig_ManInitNum(p->pManAig) > 0 ); assert( Aig_ManRegNum(p->pManAig) > 0 );
assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// start the fraig package // start the fraig package
pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames ); pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
pManFraig->vInits = Vec_IntDup(p->pManAig->vInits); pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames // create PI nodes for the frames
for ( f = 0; f < p->nFrames; f++ ) for ( f = 0; f < p->nFramesAll; f++ )
{
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) ); Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
for ( f = 0; f < p->nFramesAll; f++ )
Aig_ManForEachPiSeq( p->pManAig, pObj, i ) Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) ); Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
}
// create latches for the first frame // create latches for the first frame
Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// add timeframes // add timeframes
pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) ); pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pManAig) );
for ( f = 0; f < p->nFrames - 1; f++ ) for ( f = 0; f < p->nFramesAll - 1; f++ )
{ {
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_FramesConstrainNode( pManFraig, pObj, f );
// add internal nodes of this frame // add internal nodes of this frame
Aig_ManForEachNode( p->pManAig, pObj, i ) Aig_ManForEachNode( p->pManAig, pObj, i )
{ {
pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) ); pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
Fra_ObjSetFraig( pObj, f, pObjNew ); Fra_ObjSetFraig( pObj, f, pObjNew );
// skip nodes without representative Fra_FramesConstrainNode( pManFraig, pObj, f );
if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
continue;
assert( pObjRepr->Id < pObj->Id );
// get the new node of the representative
pObjReprNew = Fra_ObjFraig( pObjRepr, f );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
continue;
// these are different nodes
// perform speculative reduction
Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) );
// add the constraint
pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
Aig_ObjCreatePo( pManFraig, pMiter );
} }
// save the latch input values // save the latch input values
k = 0; k = 0;
Aig_ManForEachLiSeq( p->pManAig, pObj, i ) Aig_ManForEachLiSeq( p->pManAig, pObj, i )
pLatches[k++] = Fra_ObjChild0Fra(pObj,f); pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
assert( k == Aig_ManInitNum(p->pManAig) ); assert( k == Aig_ManRegNum(p->pManAig) );
// insert them to the latch output values // insert them to the latch output values
k = 0; k = 0;
Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f+1, pLatches[k++] ); Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
assert( k == Aig_ManInitNum(p->pManAig) ); assert( k == Aig_ManRegNum(p->pManAig) );
} }
free( pLatches ); free( pLatches );
// mark the asserts // mark the asserts
pManFraig->nAsserts = Aig_ManPoNum(pManFraig); pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
// add the POs for the latch inputs // add the POs for the latch inputs
Aig_ManForEachLiSeq( p->pManAig, pObj, i ) Aig_ManForEachLiSeq( p->pManAig, pObj, i )
Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) ); Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
// set the pointer to the manager
Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
// set the pointers to the manager
Aig_ManForEachObj( pManFraig, pObj, i )
pObj->pData = p;
// make sure the satisfying assignment is node assigned // make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL ); assert( pManFraig->pData == NULL );
return pManFraig; return pManFraig;
...@@ -130,7 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) ...@@ -130,7 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose )
{ {
Fra_Man_t * p; Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars; Fra_Par_t Pars, * pPars = &Pars;
...@@ -142,20 +159,23 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) ...@@ -142,20 +159,23 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
if ( Aig_ManNodeNum(pManAig) == 0 ) if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig, 1); return Aig_ManDup(pManAig, 1);
assert( Aig_ManLatchNum(pManAig) == 0 ); assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManInitNum(pManAig) > 0 ); assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
// get parameters // get parameters
Fra_ParamsDefaultSeq( pPars ); Fra_ParamsDefaultSeq( pPars );
pPars->nTimeFrames = nFrames; pPars->nFramesK = nFramesK;
pPars->fVerbose = fVerbose; pPars->fVerbose = fVerbose;
// start the fraig manager for this run // start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars ); p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using the 1st init frame // derive and refine e-classes using the 1st init frame
Fra_Simulate( p, 1 ); Fra_Simulate( p, 1 );
// Fra_ClassesTest( p->pCla, 2, 3 );
//Aig_ManShow( pManAig, 0, NULL );
// refine e-classes using sequential simulation // refine e-classes using sequential simulation
// iterate the inductive case // iterate the inductive case
p->pCla->fRefinement = 1; p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ ) for ( nIter = 0; p->pCla->fRefinement; nIter++ )
...@@ -165,18 +185,32 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) ...@@ -165,18 +185,32 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
// derive non-init K-timeframes while implementing e-classes // derive non-init K-timeframes while implementing e-classes
p->pManFraig = Fra_FramesWithClasses( p ); p->pManFraig = Fra_FramesWithClasses( p );
if ( fVerbose ) if ( fVerbose )
printf( "Iter = %3d. Original = %6d. Reduced = %6d.\n", {
nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n",
nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
}
// perform AIG rewriting on the speculated frames // perform AIG rewriting on the speculated frames
// convert the manager to SAT solver (the last nLatches outputs are inputs) // convert the manager to SAT solver (the last nLatches outputs are inputs)
pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) ); // pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = Cnf_DataWriteIntoSolver( pCnf ); p->pSat = Cnf_DataWriteIntoSolver( pCnf );
// transfer variable numbers p->nSatVars = pCnf->nVars;
Aig_ManForEachPi( p->pManAig, pObj, i )
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
// transfer PI/LO variable numbers
pObj = Aig_ManConst1( p->pManFraig );
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Aig_ManForEachPi( p->pManFraig, pObj, i )
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Aig_ManForEachLiSeq( p->pManAig, pObj, i ) // transfer LI variable numbers
Aig_ManForEachLiSeq( p->pManFraig, pObj, i )
{ {
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Fra_ObjSetFaninVec( pObj, (void *)1 ); Fra_ObjSetFaninVec( pObj, (void *)1 );
...@@ -185,9 +219,10 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) ...@@ -185,9 +219,10 @@ Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
// perform sweeping // perform sweeping
Fra_FraigSweep( p ); Fra_FraigSweep( p );
assert( Vec_PtrSize(p->vTimeouts) == 0 ); assert( p->vTimeouts == NULL );
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
sat_solver_delete( p->pSat ); p->pSat = NULL; // cleanup
Fra_ManClean( p );
} }
// move the classes into representatives // move the classes into representatives
......
src/aig/fra/fraMan.c
...@@ -53,7 +53,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) ...@@ -53,7 +53,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
pPars->dActConeBumpMax = 10.0; // the largest bump of activity pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 100; // conflict limit at a node pPars->nBTLimitNode = 100; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nTimeFrames = 0; // the number of timeframes to unroll pPars->nFramesK = 0; // the number of timeframes to unroll
pPars->fConeBias = 1; pPars->fConeBias = 1;
} }
...@@ -71,7 +71,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) ...@@ -71,7 +71,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
{ {
memset( pPars, 0, sizeof(Fra_Par_t) ); memset( pPars, 0, sizeof(Fra_Par_t) );
pPars->nSimWords = 32; // the number of words in the simulation info pPars->nSimWords = 4; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used pPars->MaxScore = 25; // max score after which resimulation is used
...@@ -82,7 +82,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) ...@@ -82,7 +82,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
pPars->dActConeBumpMax = 10.0; // the largest bump of activity pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 1000000; // conflict limit at a node pPars->nBTLimitNode = 1000000; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nTimeFrames = 1; // the number of timeframes to unroll pPars->nFramesK = 1; // the number of timeframes to unroll
pPars->fConeBias = 0; pPars->fConeBias = 0;
} }
...@@ -100,40 +100,76 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) ...@@ -100,40 +100,76 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{ {
Fra_Man_t * p; Fra_Man_t * p;
Aig_Obj_t * pObj;
int i;
// allocate the fraiging manager // allocate the fraiging manager
p = ALLOC( Fra_Man_t, 1 ); p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) ); memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars; p->pPars = pPars;
p->pManAig = pManAig; p->pManAig = pManAig;
p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1; p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
p->nFrames = pPars->nTimeFrames + 1; p->nFramesAll = pPars->nFramesK + 1;
// allocate simulation info // allocate simulation info
p->nSimWords = pPars->nSimWords * p->nFrames; p->nSimWords = pPars->nSimWords * p->nFramesAll;
p->pSimWords = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords * p->nFrames ); p->pSimWords = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords );
// clean simulation info of the constant node // clean simulation info of the constant node
memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords * p->nFrames ); memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords );
// allocate storage for sim pattern // allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) ); p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
p->pPatWords = ALLOC( unsigned, p->nPatWords ); p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords ); p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 ); p->vPiVars = Vec_PtrAlloc( 100 );
p->vTimeouts = Vec_PtrAlloc( 100 );
// equivalence classes // equivalence classes
p->pCla = Fra_ClassesStart( pManAig ); p->pCla = Fra_ClassesStart( pManAig );
// allocate other members // allocate other members
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFrames ); p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFrames ); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFrames ); p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFrames ); memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFrames ); p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 );
memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFrames ); memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 );
// set random number generator // set random number generator
srand( 0xABCABC ); srand( 0xABCABC );
// set the pointer to the manager
Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
return p; return p;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManClean( Fra_Man_t * p )
{
int i, Limit;
Limit = Aig_ManObjIdMax(p->pManFraig) + 1;
for ( i = 0; i < Limit; i++ )
if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
Vec_PtrFree( p->pMemFanins[i] );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit );
memset( p->pMemSatNums, 0, sizeof(int) * Limit );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
sat_solver_delete( p->pSat );
p->pSat = NULL;
p->nSatVars = 0;
}
/**Function*************************************************************
Synopsis [Prepares the new manager to begin fraiging.] Synopsis [Prepares the new manager to begin fraiging.]
Description [] Description []
...@@ -149,9 +185,6 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) ...@@ -149,9 +185,6 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
int i; int i;
assert( p->pManFraig == NULL ); assert( p->pManFraig == NULL );
// set the pointer to the manager
Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
// start the fraig package // start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 ); pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
// set the pointers to the available fraig nodes // set the pointers to the available fraig nodes
...@@ -204,7 +237,7 @@ void Fra_ManStop( Fra_Man_t * p ) ...@@ -204,7 +237,7 @@ void Fra_ManStop( Fra_Man_t * p )
{ {
int i; int i;
for ( i = 0; i < p->nSizeAlloc; i++ ) for ( i = 0; i < p->nSizeAlloc; i++ )
if ( p->pMemFanins[i] ) if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
Vec_PtrFree( p->pMemFanins[i] ); Vec_PtrFree( p->pMemFanins[i] );
if ( p->pPars->fVerbose ) if ( p->pPars->fVerbose )
Fra_ManPrint( p ); Fra_ManPrint( p );
......
src/aig/fra/fraSat.c
...@@ -44,6 +44,7 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * ...@@ -44,6 +44,7 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t *
int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
{ {
int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock(); int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
int status;
// make sure the nodes are not complemented // make sure the nodes are not complemented
assert( !Aig_IsComplement(pNew) ); assert( !Aig_IsComplement(pNew) );
...@@ -54,7 +55,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -54,7 +55,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// if the backtrack limit is small, simply skip this node // if the backtrack limit is small, simply skip this node
// if the backtrack limit is > 10, take the quare root of the limit // if the backtrack limit is > 10, take the quare root of the limit
nBTLimit = p->pPars->nBTLimitNode; nBTLimit = p->pPars->nBTLimitNode;
if ( !p->pPars->fSpeculate && p->pPars->nTimeFrames == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) ) if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
{ {
p->nSatFails++; p->nSatFails++;
// fail immediately // fail immediately
...@@ -77,6 +78,13 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -77,6 +78,13 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
// if the nodes do not have SAT variables, allocate them // if the nodes do not have SAT variables, allocate them
Fra_NodeAddToSolver( p, pOld, pNew ); Fra_NodeAddToSolver( p, pOld, pNew );
if ( p->pSat->qtail != p->pSat->qhead )
{
status = sat_solver_simplify(p->pSat);
assert( status != 0 );
assert( p->pSat->qtail == p->pSat->qhead );
}
// prepare variable activity // prepare variable activity
if ( p->pPars->fConeBias ) if ( p->pPars->fConeBias )
Fra_SetActivityFactors( p, pOld, pNew ); Fra_SetActivityFactors( p, pOld, pNew );
......
src/base/abci/abc.c
...@@ -6187,7 +6187,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6187,7 +6187,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_Ntk4VarTable( pNtk ); // Abc_Ntk4VarTable( pNtk );
// Dar_NtkGenerateArrays( pNtk ); // Dar_NtkGenerateArrays( pNtk );
// Dar_ManDeriveCnfTest2(); // Dar_ManDeriveCnfTest2();
/*
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
{ {
fprintf( pErr, "Network should be strashed. Command has failed.\n" ); fprintf( pErr, "Network should be strashed. Command has failed.\n" );
...@@ -6195,7 +6195,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -6195,7 +6195,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// pNtkRes = Abc_NtkDar( pNtk ); // pNtkRes = Abc_NtkDar( pNtk );
pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
// pNtkRes = NULL; */
pNtkRes = NULL;
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
fprintf( pErr, "Command has failed.\n" ); fprintf( pErr, "Command has failed.\n" );
...@@ -10732,7 +10733,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -10732,7 +10733,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes; Abc_Ntk_t * pNtk, * pNtkRes;
int c; int c;
int nFrames; int nFramesK;
int fExdc; int fExdc;
int fImp; int fImp;
int fVerbose; int fVerbose;
...@@ -10742,13 +10743,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -10742,13 +10743,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
printf( "This command is not implemented\n" );
// set defaults // set defaults
nFrames = 1; nFramesK = 1;
fExdc = 1; fExdc = 1;
fImp = 0; fImp = 0;
fVerbose = 1; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF )
{ {
...@@ -10760,9 +10759,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -10760,9 +10759,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nFrames = atoi(argv[globalUtilOptind]); nFramesK = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nFrames <= 0 ) if ( nFramesK <= 0 )
goto usage; goto usage;
break; break;
case 'e': case 'e':
...@@ -10800,7 +10799,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -10800,7 +10799,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// get the new network // get the new network
pNtkRes = Abc_NtkSeqSweep( pNtk, nFrames, fVerbose ); pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose );
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
fprintf( pErr, "Sequential sweeping has failed.\n" ); fprintf( pErr, "Sequential sweeping has failed.\n" );
...@@ -10813,7 +10812,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -10813,7 +10812,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" ); fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" );
fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
// fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
// fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); // fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
......
src/base/abci/abcDar.c
...@@ -268,7 +268,10 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) ...@@ -268,7 +268,10 @@ Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
int i; int i;
vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i ) Abc_NtkForEachLatch( pNtk, pLatch, i )
{
assert( Abc_LatchIsInit1(pLatch) == 0 );
Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) ); Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
}
return vInits; return vInits;
} }
...@@ -715,7 +718,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) ...@@ -715,7 +718,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
Vec_PtrFree( vMapped ); Vec_PtrFree( vMapped );
// write CNF into a file // write CNF into a file
Cnf_DataWriteIntoFile( pCnf, pFileName ); Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
Cnf_DataFree( pCnf ); Cnf_DataFree( pCnf );
Cnf_ClearMemory(); Cnf_ClearMemory();
...@@ -750,7 +753,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer ...@@ -750,7 +753,8 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
// conver to the manager // conver to the manager
pMan = Abc_NtkToDar( pNtk ); pMan = Abc_NtkToDar( pNtk );
// derive CNF // derive CNF
pCnf = Cnf_Derive( pMan, 0 ); // pCnf = Cnf_Derive( pMan, 0 );
pCnf = Cnf_DeriveSimple( pMan, 0 );
// convert into the SAT solver // convert into the SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf ); pSat = Cnf_DataWriteIntoSolver( pCnf );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan ); vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
...@@ -832,16 +836,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer ...@@ -832,16 +836,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fVerbose )
{ {
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp; Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk ); pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL ) if ( pMan == NULL )
return NULL; return NULL;
pMan->vInits = Abc_NtkGetLatchValues( pNtk ); pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan = Fra_Induction( pTemp = pMan, nFrames, fVerbose ); pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fVerbose );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDar( pNtk, pMan ); pNtkAig = Abc_NtkFromDar( pNtk, pMan );
......
src/opt/ret/retFlow.c
...@@ -75,6 +75,8 @@ static int Abc_NtkMaxFlowBwdPath_rec( Abc_Obj_t * pObj ); ...@@ -75,6 +75,8 @@ static int Abc_NtkMaxFlowBwdPath_rec( Abc_Obj_t * pObj );
static int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj );
static int Abc_NtkMaxFlowBwdPath2_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowBwdPath2_rec( Abc_Obj_t * pObj );
static int Abc_NtkMaxFlowFwdPath2_rec( Abc_Obj_t * pObj ); static int Abc_NtkMaxFlowFwdPath2_rec( Abc_Obj_t * pObj );
//static int Abc_NtkMaxFlowBwdPath3_rec( Abc_Obj_t * pObj );
static int Abc_NtkMaxFlowFwdPath3_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPrev, int fFanin );
static Vec_Ptr_t * Abc_NtkMaxFlowMinCut( Abc_Ntk_t * pNtk, int fForward ); static Vec_Ptr_t * Abc_NtkMaxFlowMinCut( Abc_Ntk_t * pNtk, int fForward );
static void Abc_NtkMaxFlowMinCutUpdate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ); static void Abc_NtkMaxFlowMinCutUpdate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward );
static int Abc_NtkMaxFlowVerifyCut( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ); static int Abc_NtkMaxFlowVerifyCut( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward );
...@@ -107,6 +109,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ) ...@@ -107,6 +109,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk )
pObj->fMarkA = 1; pObj->fMarkA = 1;
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
pObj->fMarkA = Abc_ObjFanin0(pObj)->fMarkA = 1; pObj->fMarkA = Abc_ObjFanin0(pObj)->fMarkA = 1;
// Abc_ObjFanin0(pObj)->fMarkA = 1;
vMinCut = Abc_NtkMaxFlow( pNtk, 1, 1 ); vMinCut = Abc_NtkMaxFlow( pNtk, 1, 1 );
Vec_PtrFree( vMinCut ); Vec_PtrFree( vMinCut );
Abc_NtkCleanMarkA( pNtk ); Abc_NtkCleanMarkA( pNtk );
...@@ -116,6 +119,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ) ...@@ -116,6 +119,7 @@ void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk )
pObj->fMarkA = 1; pObj->fMarkA = 1;
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
pObj->fMarkA = Abc_ObjFanout0(pObj)->fMarkA = 1; pObj->fMarkA = Abc_ObjFanout0(pObj)->fMarkA = 1;
// Abc_ObjFanout0(pObj)->fMarkA = 1;
vMinCut = Abc_NtkMaxFlow( pNtk, 0, 1 ); vMinCut = Abc_NtkMaxFlow( pNtk, 0, 1 );
Vec_PtrFree( vMinCut ); Vec_PtrFree( vMinCut );
Abc_NtkCleanMarkA( pNtk ); Abc_NtkCleanMarkA( pNtk );
...@@ -151,6 +155,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) ...@@ -151,6 +155,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
{ {
// assert( !Abc_ObjFanout0(pLatch)->fMarkA ); // assert( !Abc_ObjFanout0(pLatch)->fMarkA );
FlowCur = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) ); FlowCur = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) );
// FlowCur = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 );
Flow += FlowCur; Flow += FlowCur;
} }
else else
...@@ -195,6 +200,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) ...@@ -195,6 +200,7 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose )
// assert( !Abc_ObjFanout0(pLatch)->fMarkA ); // assert( !Abc_ObjFanout0(pLatch)->fMarkA );
if ( fUseDirectedFlow ) if ( fUseDirectedFlow )
RetValue = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) ); RetValue = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) );
// RetValue = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 );
else else
RetValue = Abc_NtkMaxFlowFwdPath_rec( Abc_ObjFanout0(pLatch) ); RetValue = Abc_NtkMaxFlowFwdPath_rec( Abc_ObjFanout0(pLatch) );
} }
...@@ -333,6 +339,47 @@ int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj ) ...@@ -333,6 +339,47 @@ int Abc_NtkMaxFlowFwdPath_rec( Abc_Obj_t * pObj )
return 0; return 0;
} }
/**Function*************************************************************
Synopsis [Tries to find an augmenting path originating in this edge.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMaxFlowFwdPath3_rec( Abc_Obj_t * pObj, Abc_Obj_t * pPrev, int fFanin )
{
Abc_Obj_t * pFanin, * pFanout;
int i;
// skip visited nodes
if ( Abc_NodeIsTravIdCurrent(pObj) )
return 0;
Abc_NodeSetTravIdCurrent(pObj);
// skip the fanin which already has flow
if ( fFanin && Abc_ObjGetPath(pPrev) )
return 0;
// if the node has no flow, try to push through the fanouts
if ( !Abc_ObjGetPath(pObj) )
{
// start the path if we reached a terminal node
if ( pObj->fMarkA )
return Abc_ObjSetPath( pObj, (void *)1 );
// try to push flow through the fanouts
Abc_ObjForEachFanout( pObj, pFanout, i )
if ( Abc_NtkMaxFlowFwdPath3_rec(pFanout, pObj, 1) )
return fFanin? Abc_ObjSetPath(pPrev, pObj) : 1;
}
// try to push through the fanins
Abc_ObjForEachFanin( pObj, pFanin, i )
if ( !Abc_ObjIsLatch(pFanin) && Abc_NtkMaxFlowFwdPath3_rec(pFanin, pObj, 0) )
return Abc_ObjSetPath( pFanin, NULL );
return 0;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Tries to find an augmenting path originating in this node.] Synopsis [Tries to find an augmenting path originating in this node.]
......
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