Skip to content

A
abc
Commit a8a80d9a by Alan Mishchenko
Options

Version abc70727

parent 054e2cd3
Showing with 860 additions and 3228 deletions
abc.dsp
......@@ -2570,7 +2570,7 @@ SOURCE=.\src\aig\fra\fraCore.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\fra\fraDfs.c
SOURCE=.\src\aig\fra\fraInd.c
# End Source File
# Begin Source File
......
src/aig/aig/aig.h
......@@ -92,6 +92,8 @@ struct Aig_Man_t_
Vec_Ptr_t * vBufs; // the array of buffers
Aig_Obj_t * pConst1; // the constant 1 node
Aig_Obj_t Ghost; // the ghost node
Vec_Int_t * vInits; // the initial values of the latches (latches are last PIs/POs)
int nAsserts; // the number of asserts among POs (asserts are first POs)
// AIG node counters
int nObjs[AIG_OBJ_VOID];// the number of objects by type
int nCreated; // the number of created objects
......@@ -114,8 +116,9 @@ struct Aig_Man_t_
int nAndTotal;
int nAndPrev;
// representatives
Aig_Obj_t ** pRepr;
int nReprAlloc;
Aig_Obj_t ** pEquivs; // linked list of equivalent nodes (when choices are used)
Aig_Obj_t ** pReprs; // representatives of each node
int nReprsAlloc; // the number of allocated representatives
// various data members
Aig_MmFixed_t * pMemObjs; // memory manager for objects
Vec_Int_t * vLevelR; // the reverse level of the nodes
......@@ -123,7 +126,6 @@ struct Aig_Man_t_
void * pData; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
Aig_Obj_t ** pReprs; // linked list of equivalent nodes (when choices are used)
// timing statistics
int time1;
int time2;
......@@ -171,6 +173,7 @@ 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_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_ManInitNum( Aig_Man_t * p ) { return p->vInits? Vec_IntSize(p->vInits) : 0; }
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; }
......@@ -304,6 +307,24 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF
(((iFan) = i? Aig_ObjFanoutNext(p, iFan) : Aig_ObjFanout0Int(p, pObj->Id)), 1) && \
(((pFanout) = Aig_ManObj(p, iFan>>1)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// SEQUENTIAL ITERATORS ///
////////////////////////////////////////////////////////////////////////
// iterator over the primary inputs
#define Aig_ManForEachPiSeq( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) )
// iterator over the latch outputs
#define Aig_ManForEachLoSeq( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManInitNum(p) )
// iterator over the primary outputs
#define Aig_ManForEachPoSeq( p, pObj, i ) \
Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) )
// iterator over the latch inputs
#define Aig_ManForEachLiSeq( p, pObj, i ) \
Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManInitNum(p) )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -382,8 +403,11 @@ extern Vec_Vec_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
/*=== aigRepr.c =========================================================*/
extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
extern void Aig_ManReprStop( Aig_Man_t * p );
extern void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p );
extern Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p );
extern void Aig_ManCreateChoices( Aig_Man_t * p );
/*=== aigSeq.c ========================================================*/
extern int Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
/*=== aigTable.c ========================================================*/
......
src/aig/aig/aigDfs.c
......@@ -138,7 +138,7 @@ void Aig_ManDfsChoices_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes
assert( Aig_ObjIsNode(pObj) );
Aig_ManDfsChoices_rec( p, Aig_ObjFanin0(pObj), vNodes );
Aig_ManDfsChoices_rec( p, Aig_ObjFanin1(pObj), vNodes );
Aig_ManDfsChoices_rec( p, p->pReprs[pObj->Id], vNodes );
Aig_ManDfsChoices_rec( p, p->pEquivs[pObj->Id], vNodes );
assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection
Aig_ObjSetTravIdCurrent(p, pObj);
Vec_PtrPush( vNodes, pObj );
......@@ -160,7 +160,7 @@ Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p )
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj;
int i;
assert( p->pReprs != NULL );
assert( p->pEquivs != NULL );
Aig_ManIncrementTravId( p );
// mark constant and PIs
Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
......
src/aig/aig/aigMan.c
......@@ -239,7 +239,9 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vBufs ) Vec_PtrFree( p->vBufs );
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vInits ) Vec_IntFree( p->vInits );
FREE( p->pReprs );
FREE( p->pEquivs );
free( p->pTable );
free( p );
}
......
src/aig/aig/aigPart.c
......@@ -873,8 +873,8 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
// perform choicing for each derived AIG
Vec_PtrForEachEntry( vMiters, pNew, i )
{
extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig );
pNew = Fra_Choice( p = pNew );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
pNew = Fra_FraigChoice( p = pNew );
Vec_PtrWriteEntry( vMiters, i, pNew );
Aig_ManStop( p );
}
......@@ -914,7 +914,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize )
Vec_PtrFree( vMiters );
// derive the result of choicing
pChoice = Aig_ManCreateChoices( pNew );
pChoice = Aig_ManRehash( pNew );
if ( pChoice != pNew )
Aig_ManStop( pNew );
return pChoice;
......
src/aig/aig/aigRepr.c
......@@ -42,10 +42,10 @@
void Aig_ManReprStart( Aig_Man_t * p, int nIdMax )
{
assert( Aig_ManBufNum(p) == 0 );
assert( p->pRepr == NULL );
p->nReprAlloc = nIdMax;
p->pRepr = ALLOC( Aig_Obj_t *, p->nReprAlloc );
memset( p->pRepr, 0, sizeof(Aig_Obj_t *) * p->nReprAlloc );
assert( p->pReprs == NULL );
p->nReprsAlloc = nIdMax;
p->pReprs = ALLOC( Aig_Obj_t *, p->nReprsAlloc );
memset( p->pReprs, 0, sizeof(Aig_Obj_t *) * p->nReprsAlloc );
}
/**Function*************************************************************
......@@ -61,9 +61,31 @@ void Aig_ManReprStart( Aig_Man_t * p, int nIdMax )
***********************************************************************/
void Aig_ManReprStop( Aig_Man_t * p )
{
assert( p->pRepr != NULL );
FREE( p->pRepr );
p->nReprAlloc = 0;
assert( p->pReprs != NULL );
FREE( p->pReprs );
p->nReprsAlloc = 0;
}
/**Function*************************************************************
Synopsis [Set the representative.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
{
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode1) );
assert( !Aig_IsComplement(pNode2) );
assert( pNode1->Id < p->nReprsAlloc );
assert( pNode2->Id < p->nReprsAlloc );
assert( pNode1->Id < pNode2->Id );
p->pReprs[pNode2->Id] = pNode1;
}
/**Function*************************************************************
......@@ -79,17 +101,17 @@ void Aig_ManReprStop( Aig_Man_t * p )
***********************************************************************/
static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
{
assert( p->pRepr != NULL );
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode1) );
assert( !Aig_IsComplement(pNode2) );
assert( pNode1->Id < p->nReprAlloc );
assert( pNode2->Id < p->nReprAlloc );
assert( pNode1->Id < p->nReprsAlloc );
assert( pNode2->Id < p->nReprsAlloc );
if ( pNode1 == pNode2 )
return;
if ( pNode1->Id < pNode2->Id )
p->pRepr[pNode2->Id] = pNode1;
p->pReprs[pNode2->Id] = pNode1;
else
p->pRepr[pNode1->Id] = pNode2;
p->pReprs[pNode1->Id] = pNode2;
}
/**Function*************************************************************
......@@ -105,11 +127,30 @@ static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t
***********************************************************************/
static inline Aig_Obj_t * Aig_ObjFindRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
{
assert( p->pRepr != NULL );
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode) );
assert( pNode->Id < p->nReprAlloc );
assert( !p->pRepr[pNode->Id] || p->pRepr[pNode->Id]->Id < pNode->Id );
return p->pRepr[pNode->Id];
assert( pNode->Id < p->nReprsAlloc );
assert( !p->pReprs[pNode->Id] || p->pReprs[pNode->Id]->Id < pNode->Id );
return p->pReprs[pNode->Id];
}
/**Function*************************************************************
Synopsis [Clears the representative.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Aig_ObjClearRepr( Aig_Man_t * p, Aig_Obj_t * pNode )
{
assert( p->pReprs != NULL );
assert( !Aig_IsComplement(pNode) );
assert( pNode->Id < p->nReprsAlloc );
p->pReprs[pNode->Id] = NULL;
}
/**Function*************************************************************
......@@ -166,7 +207,7 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pRepr;
int k;
assert( pNew->pRepr != NULL );
assert( pNew->pReprs != NULL );
// go through the nodes which have representatives
Aig_ManForEachObj( p, pObj, k )
if ( pRepr = Aig_ObjFindRepr(p, pObj) )
......@@ -269,7 +310,7 @@ int Aig_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
if ( Aig_ObjCheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
return 1;
// check equivalent nodes
return Aig_ObjCheckTfi_rec( p, pNode->pData, pOld );
return Aig_ObjCheckTfi_rec( p, p->pEquivs[pNode->Id], pOld );
}
/**Function*************************************************************
......@@ -293,7 +334,7 @@ int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
/**Function*************************************************************
Synopsis [Creates choices.]
Synopsis [Iteratively rehashes the AIG.]
Description [The input AIG is assumed to have representatives assigned.]
......@@ -302,20 +343,38 @@ int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p )
Aig_Man_t * Aig_ManRehash( Aig_Man_t * p )
{
Aig_Man_t * pTemp;
Aig_Obj_t * pObj, * pRepr;
int i;
assert( p->pRepr != NULL );
// iteratively reconstruct the HOP manager while transfering the fanouts
assert( p->pReprs != NULL );
while ( Aig_ManRemapRepr( p ) )
{
p = Aig_ManDupRepr( pTemp = p );
Aig_ManStop( pTemp );
}
// create choices in this manager
Aig_ManCleanData( p );
return p;
}
/**Function*************************************************************
Synopsis [Creates choices.]
Description [The input AIG is assumed to have representatives assigned.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManCreateChoices( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pRepr;
int i;
assert( p->pReprs != NULL );
// create equivalent nodes in the manager
assert( p->pEquivs == NULL );
p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p) + 1 );
memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p) + 1) );
// make the choice nodes
Aig_ManForEachNode( p, pObj, i )
{
......@@ -324,15 +383,21 @@ Aig_Man_t * Aig_ManCreateChoices( Aig_Man_t * p )
continue;
// skip constant and PI classes
if ( !Aig_ObjIsNode(pRepr) )
{
Aig_ObjClearRepr( p, pObj );
continue;
}
// skip choices with combinatinal loops
if ( Aig_ObjCheckTfi( p, pRepr, pObj ) )
if ( Aig_ObjCheckTfi( p, pObj, pRepr ) )
{
Aig_ObjClearRepr( p, pObj );
continue;
}
//printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
// add choice to the choice node
pObj->pData = pRepr->pData;
pRepr->pData = pObj;
p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
p->pEquivs[pRepr->Id] = pObj;
}
return p;
}
......
src/aig/cnf/cnf.h
......@@ -117,7 +117,7 @@ static inline void Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut
////////////////////////////////////////////////////////////////////////
/*=== cnfCore.c ========================================================*/
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig );
extern Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
extern Cnf_Man_t * Cnf_ManRead();
extern void Cnf_ClearMemory();
/*=== cnfCut.c ========================================================*/
......@@ -147,7 +147,7 @@ extern Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
/*=== cnfWrite.c ========================================================*/
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 );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
#ifdef __cplusplus
}
......
src/aig/cnf/cnfCore.c
......@@ -41,7 +41,7 @@ static Cnf_Man_t * s_pManCnf = NULL;
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig )
Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
{
Cnf_Man_t * p;
Cnf_Dat_t * pCnf;
......@@ -70,7 +70,7 @@ p->timeMap = clock() - clk;
clk = clock();
Cnf_ManTransferCuts( p );
vMapped = Cnf_ManScanMapping( p, 1, 1 );
pCnf = Cnf_ManWriteCnf( p, vMapped );
pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
Vec_PtrFree( vMapped );
Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = clock() - clk;
......
src/aig/cnf/cnfWrite.c
......@@ -145,28 +145,30 @@ int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
/**Function*************************************************************
Synopsis []
Synopsis [Derives CNF for the mapping.]
Description []
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_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
{
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Cnf_Cut_t * pCut;
Vec_Int_t * vCover, * vSopTemp;
int OutVar, pVars[32], * pLits, ** pClas;
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
unsigned uTruth;
int i, k, nLiterals, nClauses, Cube, Number;
// count the number of literals and clauses
nLiterals = 1 + Aig_ManPoNum( p->pManAig );
nClauses = 1 + Aig_ManPoNum( p->pManAig );
nLiterals = 1 + Aig_ManPoNum( p->pManAig ) + 3 * nOutputs;
nClauses = 1 + Aig_ManPoNum( p->pManAig ) + nOutputs;
Vec_PtrForEachEntry( vMapped, pObj, i )
{
assert( Aig_ObjIsNode(pObj) );
......@@ -211,12 +213,20 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// set variable numbers
Number = 0;
// create room for variable numbers
pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
// assign variables to the last (nOutputs) POs
Number = 0;
for ( i = 0; i < nOutputs; i++ )
{
pObj = Aig_ManPo( p->pManAig, Aig_ManPoNum(p->pManAig) - nOutputs + i );
pCnf->pVarNums[pObj->Id] = Number++;
}
// assign variables to the internal nodes
Vec_PtrForEachEntry( vMapped, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
// assign variables to the PIs and constant node
Aig_ManForEachPi( p->pManAig, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
......@@ -281,10 +291,26 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
// write the output literals
Aig_ManForEachPo( p->pManAig, pObj, i )
{
if ( i < Aig_ManPoNum(p->pManAig) - nOutputs )
{
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
*pClas++ = pLits;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
}
else
{
PoVar = pCnf->pVarNums[ pObj->Id ];
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(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 );
......
src/aig/fra/fra.h
......@@ -49,6 +49,7 @@ extern "C" {
////////////////////////////////////////////////////////////////////////
typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Man_t_ Fra_Man_t;
// FRAIG parameters
......@@ -65,8 +66,26 @@ struct Fra_Par_t_
int fProve; // prove the miter outputs
int fVerbose; // verbose output
int fDoSparse; // skip sparse functions
int fConeBias; // bias variables in the cone (good for unsat runs)
int nBTLimitNode; // conflict limit at a node
int nBTLimitMiter; // conflict limit at an output
int nTimeFrames; // the number of timeframes to unroll
};
// FRAIG equivalence classes
struct Fra_Cla_t_
{
Aig_Man_t * pAig; // the original AIG manager
Aig_Obj_t ** pMemRepr; // pointers to representatives of each node
Vec_Ptr_t * vClasses; // equivalence classes
Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
int nPairs; // the number of pairs of nodes
int fRefinement; // set to 1 when refinement has happened
};
// FRAIG manager
......@@ -77,6 +96,9 @@ struct Fra_Man_t_
// AIG managers
Aig_Man_t * pManAig; // the starting AIG manager
Aig_Man_t * pManFraig; // the final AIG manager
// mapping AIG into FRAIG
int nFrames; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
// simulation info
unsigned * pSimWords; // memory for simulation information
int nSimWords; // the number of simulation words
......@@ -85,27 +107,17 @@ struct Fra_Man_t_
unsigned * pPatWords; // the counter example
int * pPatScores; // the scores of each pattern
// equivalence classes
Vec_Ptr_t * vClasses; // equivalence classes
Vec_Ptr_t * vClasses1; // equivalence class of Const1 node
Vec_Ptr_t * vClassesTemp; // temporary storage for new classes
Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes
Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used
Vec_Ptr_t * vClassOld; // old equivalence class after splitting
Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting
int nPairs; // the number of pairs of nodes
Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes
// equivalence checking
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
Vec_Ptr_t * vPiVars; // the PIs of the cone used
sint64 nBTLimitGlobal; // resource limit
sint64 nInsLimitGlobal; // resource limit
// various data members
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
Aig_Obj_t ** pMemRepr; // memory allocated for points to the node representatives
Aig_Obj_t ** pMemReprFra; // memory allocated for points to the node representatives in the FRAIG
Vec_Ptr_t ** pMemFanins; // the arrays of fanins
int * pMemSatNums; // the array of SAT numbers
Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes
int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes
int nSizeAlloc; // allocated size of the arrays
Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out
// statistics
int nSimRounds;
int nNodesMiter;
......@@ -143,20 +155,20 @@ struct Fra_Man_t_
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 Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; }
static inline Aig_Obj_t * Fra_ObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; }
static inline Aig_Obj_t * Fra_ObjReprFra( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id]; }
static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; }
static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; }
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 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, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; }
static inline void Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; }
static inline void Fra_ObjSetReprFra( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id] = pNode; }
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 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 Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
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 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; }
////////////////////////////////////////////////////////////////////////
/// ITERATORS ///
......@@ -167,31 +179,40 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I
////////////////////////////////////////////////////////////////////////
/*=== fraClass.c ========================================================*/
extern void Fra_PrintClasses( Fra_Man_t * p );
extern void Fra_CreateClasses( Fra_Man_t * p );
extern int Fra_RefineClasses( Fra_Man_t * p );
extern int Fra_RefineClasses1( Fra_Man_t * p );
extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void Fra_ClassesPrint( Fra_Cla_t * p );
extern void Fra_ClassesPrepare( Fra_Cla_t * p );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
/*=== fraCnf.c ========================================================*/
extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
/*=== fraDfs.c ========================================================*/
extern int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( 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 void Fra_ManPrepare( 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_ManStop( Fra_Man_t * p );
extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
/*=== fraSim.c ========================================================*/
extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj );
extern int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern unsigned Fra_NodeHashSims( Aig_Obj_t * pObj );
extern void Fra_SavePattern( Fra_Man_t * p );
extern void Fra_Simulate( Fra_Man_t * p );
extern void Fra_Simulate( Fra_Man_t * p, int fInit );
extern void Fra_Resimulate( Fra_Man_t * p );
extern int Fra_CheckOutputSims( Fra_Man_t * p );
......
src/aig/fra/fraClass.c
......@@ -45,6 +45,80 @@ static inline void Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pOb
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
{
Fra_Cla_t * p;
p = ALLOC( Fra_Cla_t, 1 );
memset( p, 0, sizeof(Fra_Cla_t) );
p->pAig = pAig;
p->pMemRepr = ALLOC( 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->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis [Stop representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesStop( Fra_Cla_t * p )
{
free( p->pMemClasses );
free( p->pMemRepr );
if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
if ( p->vClasses ) Vec_PtrFree( p->vClasses );
free( p );
}
/**Function*************************************************************
Synopsis [Starts representation of equivalence classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
{
Aig_Obj_t * pObj;
int i;
Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
Vec_PtrForEachEntry( vFailed, pObj, i )
{
// assert( p->pAig->pReprs[pObj->Id] != NULL );
p->pAig->pReprs[pObj->Id] = NULL;
}
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
......@@ -75,7 +149,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
SeeAlso []
***********************************************************************/
int Fra_CountClass( Aig_Obj_t ** pClass )
int Fra_ClassCount( Aig_Obj_t ** pClass )
{
Aig_Obj_t * pTemp;
int i;
......@@ -94,13 +168,13 @@ int Fra_CountClass( Aig_Obj_t ** pClass )
SeeAlso []
***********************************************************************/
int Fra_CountPairsClasses( Fra_Man_t * p )
int Fra_ClassesCountPairs( Fra_Cla_t * p )
{
Aig_Obj_t ** pClass;
int i, nNodes, nPairs = 0;
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
nNodes = Fra_CountClass( pClass );
nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 );
nPairs += nNodes * (nNodes - 1) / 2;
}
......@@ -109,7 +183,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Synopsis [Count the number of literals.]
Description []
......@@ -118,22 +192,23 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
void Fra_PrintClasses( Fra_Man_t * p )
int Fra_ClassesCountLits( Fra_Cla_t * p )
{
Aig_Obj_t ** pClass;
int i;
printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
int i, nNodes, nLits = 0;
nLits = Vec_PtrSize( p->vClasses1 );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
// printf( "%3d (%3d) : ", Fra_CountClass(pClass) );
// Fra_PrintClass( pClass );
nNodes = Fra_ClassCount( pClass );
assert( nNodes > 1 );
nLits += nNodes - 1;
}
printf( "\n" );
return nLits;
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Synopsis [Prints simulation classes.]
Description []
......@@ -142,70 +217,18 @@ void Fra_PrintClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj )
void Fra_ClassesPrint( Fra_Cla_t * p )
{
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
unsigned uHash;
Aig_Obj_t ** pClass;
int i;
assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
uHash ^= pSims[i] * s_FPrimes[i];
return uHash;
}
/**Function********************************************************************
Synopsis [Returns the next prime >= p.]
Description [Copied from CUDD, for stand-aloneness.]
SideEffects [None]
SeeAlso []
******************************************************************************/
unsigned int Cudd_PrimeFra( unsigned int p )
{
int i,pn;
p--;
do {
p++;
if (p&1) {
pn = 1;
i = 3;
while ((unsigned) (i * i) <= p) {
if (p % i == 0) {
pn = 0;
break;
}
i += 2;
}
} else {
pn = 0;
printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_ClassesCountPairs(p) );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
{
printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
Fra_PrintClass( pClass );
}
} while (!pn);
return(p);
} /* end of Cudd_Prime */
printf( "\n" );
}
/**Function*************************************************************
......@@ -218,31 +241,31 @@ unsigned int Cudd_PrimeFra( unsigned int p )
SeeAlso []
***********************************************************************/
void Fra_CreateClasses( Fra_Man_t * p )
void Fra_ClassesPrepare( Fra_Cla_t * p )
{
Aig_Obj_t ** ppTable, ** ppNexts;
Aig_Obj_t * pObj, * pTemp;
int i, k, nTableSize, nEntries, nNodes, iEntry;
// allocate the hash table hashing simulation info into nodes
nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 );
nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 );
ppTable = ALLOC( Aig_Obj_t *, nTableSize );
ppNexts = ALLOC( Aig_Obj_t *, nTableSize );
memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
// add all the nodes to the hash table
Vec_PtrClear( p->vClasses1 );
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
// hash the node by its simulation info
iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
iEntry = Fra_NodeHashSims( pObj ) % nTableSize;
// check if the node belongs to the class of constant 1
if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
if ( iEntry == 0 && Fra_NodeHasZeroSim( pObj ) )
{
Vec_PtrPush( p->vClasses1, pObj );
Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
continue;
}
// add the node to the class
......@@ -281,7 +304,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
// copy the entries into storage in the topological order
Vec_PtrClear( p->vClasses );
nEntries = 0;
Aig_ManForEachObj( p->pManAig, pObj, i )
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
continue;
......@@ -304,7 +327,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
{
p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
Fra_ObjSetRepr( pTemp, pObj );
Fra_ClassObjSetRepr( pTemp, pObj );
}
// add as many empty entries
// memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
......@@ -315,7 +338,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
free( ppTable );
free( ppNexts );
// now it is time to refine the classes
Fra_RefineClasses( p );
Fra_ClassesRefine( p );
}
/**Function*************************************************************
......@@ -329,7 +352,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
{
Aig_Obj_t * pObj, ** ppThis;
int i;
......@@ -337,7 +360,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
// check if the class is going to be refined
for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )
if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
if ( !Fra_NodeCompareSims(ppClass[0], pObj) )
break;
if ( pObj == NULL )
return NULL;
......@@ -346,7 +369,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
Vec_PtrClear( p->vClassNew );
Vec_PtrPush( p->vClassOld, ppClass[0] );
for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )
if ( Fra_NodeCompareSims(p, ppClass[0], pObj) )
if ( Fra_NodeCompareSims(ppClass[0], pObj) )
Vec_PtrPush( p->vClassOld, pObj );
else
Vec_PtrPush( p->vClassNew, pObj );
......@@ -364,7 +387,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
{
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
}
ppClass += 2*Vec_PtrSize(p->vClassOld);
// put the new nodes into the class memory
......@@ -372,7 +395,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
{
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
}
return ppClass;
}
......@@ -388,7 +411,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
SeeAlso []
***********************************************************************/
int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
{
Aig_Obj_t ** pClass, ** pClass2;
int nRefis;
......@@ -423,19 +446,12 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
SeeAlso []
***********************************************************************/
int Fra_RefineClasses( Fra_Man_t * p )
int Fra_ClassesRefine( Fra_Cla_t * p )
{
Vec_Ptr_t * vTemp;
Aig_Obj_t ** pClass;
int clk, i, nRefis;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
if ( p->pPars->fProve )
Fra_CheckOutputSims( p );
if ( p->pManFraig->pData )
return 0;
int i, nRefis;
// refine the classes
clk = clock();
nRefis = 0;
Vec_PtrClear( p->vClassesTemp );
Vec_PtrForEachEntry( p->vClasses, pClass, i )
......@@ -449,7 +465,7 @@ clk = clock();
vTemp = p->vClassesTemp;
p->vClassesTemp = p->vClasses;
p->vClasses = vTemp;
p->timeRef += clock() - clk;
p->fRefinement = (nRefis > 0);
return nRefis;
}
......@@ -464,22 +480,21 @@ p->timeRef += clock() - clk;
SeeAlso []
***********************************************************************/
int Fra_RefineClasses1( Fra_Man_t * p )
int Fra_ClassesRefine1( Fra_Cla_t * p )
{
Aig_Obj_t * pObj, ** ppClass;
int i, k, nRefis, clk;
int i, k, nRefis;
// check if there is anything to refine
if ( Vec_PtrSize(p->vClasses1) == 0 )
return 0;
clk = clock();
// make sure constant 1 class contains only non-constant nodes
assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) );
assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
// collect all the nodes to be refined
k = 0;
Vec_PtrClear( p->vClassNew );
Vec_PtrForEachEntry( p->vClasses1, pObj, i )
{
if ( Fra_NodeHasZeroSim( p, pObj ) )
if ( Fra_NodeHasZeroSim( pObj ) )
Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
else
Vec_PtrPush( p->vClassNew, pObj );
......@@ -487,9 +502,10 @@ clk = clock();
Vec_PtrShrink( p->vClasses1, k );
if ( Vec_PtrSize(p->vClassNew) == 0 )
return 0;
p->fRefinement = 1;
if ( Vec_PtrSize(p->vClassNew) == 1 )
{
Fra_ObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
return 1;
}
// create a new class composed of these nodes
......@@ -499,12 +515,11 @@ clk = clock();
{
ppClass[i] = pObj;
ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
}
Vec_PtrPush( p->vClasses, ppClass );
// iteratively refine this class
nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
p->timeRef += clock() - clk;
return nRefis;
}
......
src/aig/fra/fraCore.c
......@@ -39,24 +39,24 @@
SeeAlso []
***********************************************************************/
Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
Aig_Obj_t * pObjRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjReprFraig;
int RetValue;
assert( !Aig_IsComplement(pObjOld) );
assert( Aig_ObjIsNode(pObjOld) );
assert( !Aig_IsComplement(pObj) );
assert( Aig_ObjIsNode(pObj) );
// get the fraiged fanins
pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
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
pObjOldRepr = Fra_ObjRepr(pObjOld);
if ( pObjOldRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
pObjRepr = Fra_ClassObjRepr(pObj);
if ( pObjRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
{
assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
......@@ -64,58 +64,38 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
return pObjFraig;
}
// get the fraiged representative
pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
pObjReprFraig = Fra_ObjFraig(pObjRepr,0);
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return pObjFraig;
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
// printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
// printf( "Node = %d. Repr = %d.\n", pObj->Id, pObjRepr->Id );
// if they are proved different, the c-ex will be in p->pPatWords
RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
// pObjOld->fMarkA = 1;
if ( p->pPars->fChoicing && !Fra_CheckTfi( p, Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) ) )
{
// Fra_ObjSetReprFra( Aig_Regular(pObjFraig), Aig_Regular(pObjOldReprFraig) );
Aig_Obj_t * pObjNew = Aig_Regular(pObjFraig);
Aig_Obj_t * pObjOld = Aig_Regular(pObjOldReprFraig);
Aig_Obj_t * pTemp;
assert( pObjNew != pObjOld );
for ( pTemp = Fra_ObjReprFra(pObjOld); pTemp; pTemp = Fra_ObjReprFra(pTemp) )
if ( pTemp == pObjNew )
break;
if ( pTemp == NULL )
{
Fra_ObjSetReprFra( pObjNew, Fra_ObjReprFra(pObjOld) );
Fra_ObjSetReprFra( pObjOld, pObjNew );
assert( pObjOld != Fra_ObjReprFra(pObjOld) );
assert( pObjNew != Fra_ObjReprFra(pObjNew) );
p->nChoices++;
assert( pObjOld->Id < pObjNew->Id );
}
else
p->nChoicesFake++;
}
return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
// pObj->fMarkA = 1;
// if ( p->pPars->fChoicing )
// Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
}
if ( RetValue == -1 ) // failed
{
static int Counter = 0;
char FileName[20];
Aig_Man_t * pTemp;
Aig_Obj_t * pObj;
Aig_Obj_t * pNode;
int i;
Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) };
// Vec_Ptr_t * vNodes;
Vec_PtrPush( p->vTimeouts, pObj );
if ( !p->pPars->fSpeculate )
return pObjFraig;
// substitute the node
// pObjOld->fMarkB = 1;
// pObj->fMarkB = 1;
p->nSpeculs++;
pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
......@@ -124,21 +104,18 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
Aig_ManStop( pTemp );
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
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( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
return Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
}
// printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
// simulate the counter-example and return the Fraig node
// printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
Fra_Resimulate( p );
// printf( "Representaive after = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
assert( Fra_ClassObjRepr(pObj) != pObjRepr );
return pObjFraig;
}
......@@ -153,13 +130,13 @@ Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
SeeAlso []
***********************************************************************/
void Fra_Sweep( Fra_Man_t * p )
void Fra_FraigSweep( Fra_Man_t * p )
{
ProgressBar * pProgress;
Aig_Obj_t * pObj, * pObjNew;
int i, k = 0;
p->nClassesZero = Vec_PtrSize(p->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
// duplicate internal nodes
pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
Aig_ManForEachNode( p->pManAig, pObj, i )
......@@ -167,36 +144,18 @@ p->nClassesBeg = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0
Extra_ProgressBarUpdate( pProgress, i, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,0), Fra_ObjChild1Fra(pObj,0) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
Fra_ObjSetFraig( pObj, pObjNew );
assert( Fra_ObjFraig(pObj) != NULL );
Fra_ObjSetFraig( pObj, 0, pObjNew );
}
Extra_ProgressBarStop( pProgress );
p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
// try to prove the outputs of the miter
p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
// Fra_MiterProve( p );
// add the POs
Aig_ManForEachPo( p->pManAig, pObj, i )
Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
// postprocess
Aig_ManCleanMarkB( p->pManFraig );
if ( p->pPars->fChoicing )
{
// transfer the representative info
p->pManFraig->pReprs = p->pMemReprFra;
p->pMemReprFra = NULL;
// printf( "The number of choices = %d. Fake choices = %d.\n", p->nChoices, p->nChoicesFake );
}
else
{
// remove dangling nodes
Aig_ManCleanup( p->pManFraig );
}
}
/**Function*************************************************************
......@@ -210,7 +169,7 @@ p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0)
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
{
Fra_Man_t * p;
Aig_Man_t * pManAigNew;
......@@ -220,9 +179,26 @@ Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
clk = clock();
assert( Aig_ManLatchNum(pManAig) == 0 );
p = Fra_ManStart( pManAig, pPars );
Fra_Simulate( p );
Fra_Sweep( p );
p->pManFraig = Fra_ManPrepareComb( p );
Fra_Simulate( p, 0 );
if ( p->pPars->fChoicing )
Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
Fra_FraigSweep( p );
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( p->pManAig );
Aig_ManCreateChoices( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
}
else
{
Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
}
p->timeTotal = clock() - clk;
Fra_ManStop( p );
return pManAigNew;
......@@ -239,7 +215,7 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig )
Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
......@@ -249,7 +225,7 @@ Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig )
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fChoicing = 1;
return Fra_Perform( pManAig, pPars );
return Fra_FraigPerform( pManAig, pPars );
}
////////////////////////////////////////////////////////////////////////
......
src/aig/fra/fraDfs.c deleted 100644 → 0
/**CFile****************************************************************
FileName [fraDfs.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fraig FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraDfs.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNew.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_CheckTfi_rec( Fra_Man_t * p, Aig_Obj_t * pNode, Aig_Obj_t * pOld )
{
// check the trivial cases
if ( pNode == NULL )
return 0;
// if ( pNode->Id < pOld->Id ) // cannot use because of choicesof pNode
// return 0;
if ( pNode == pOld )
return 1;
// skip the visited node
if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pNode) )
return 0;
Aig_ObjSetTravIdCurrent(p->pManFraig, pNode);
// check the children
if ( Fra_CheckTfi_rec( p, Aig_ObjFanin0(pNode), pOld ) )
return 1;
if ( Fra_CheckTfi_rec( p, Aig_ObjFanin1(pNode), pOld ) )
return 1;
// check equivalent nodes
return Fra_CheckTfi_rec( p, Fra_ObjReprFra(pNode), pOld );
}
/**Function*************************************************************
Synopsis [Returns 1 if pOld is in the TFI of pNew.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld )
{
assert( !Aig_IsComplement(pNew) );
assert( !Aig_IsComplement(pOld) );
Aig_ManIncrementTravId( p->pManFraig );
return Fra_CheckTfi_rec( p, pNew, pOld );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/fra/fraInd.c 0 → 100644
/**CFile****************************************************************
FileName [fraInd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [New FRAIG package.]
Synopsis [Inductive prover.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
#include "cnf.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
{
Aig_Man_t * pManFraig;
Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter;
Aig_Obj_t ** pLatches;
int i, k, f;
assert( p->pManFraig == NULL );
assert( Aig_ManInitNum(p->pManAig) > 0 );
assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// start the fraig package
pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames );
pManFraig->vInits = Vec_IntDup(p->pManAig->vInits);
// create PI nodes for the frames
for ( f = 0; f < p->nFrames; f++ )
{
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
}
// create latches for the first frame
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// add timeframes
pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) );
for ( f = 0; f < p->nFrames - 1; f++ )
{
// add internal nodes of this frame
Aig_ManForEachNode( p->pManAig, pObj, i )
{
pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
Fra_ObjSetFraig( pObj, f, pObjNew );
// skip nodes without representative
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
k = 0;
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
assert( k == Aig_ManInitNum(p->pManAig) );
// insert them to the latch output values
k = 0;
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
assert( k == Aig_ManInitNum(p->pManAig) );
}
free( pLatches );
// mark the asserts
pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
// add the POs for the latch inputs
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) );
// 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
assert( pManFraig->pData == NULL );
return pManFraig;
}
/**Function*************************************************************
Synopsis [Performs choicing of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
{
Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars;
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew;
int nIter, i;
if ( Aig_ManNodeNum(pManAig) == 0 )
return Aig_ManDup(pManAig, 1);
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManInitNum(pManAig) > 0 );
// get parameters
Fra_ParamsDefaultSeq( pPars );
pPars->nTimeFrames = nFrames;
pPars->fVerbose = fVerbose;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using the 1st init frame
Fra_Simulate( p, 1 );
// refine e-classes using sequential simulation
// iterate the inductive case
p->pCla->fRefinement = 1;
for ( nIter = 0; p->pCla->fRefinement; nIter++ )
{
// mark the classes as non-refined
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
p->pManFraig = Fra_FramesWithClasses( p );
if ( fVerbose )
printf( "Iter = %3d. Original = %6d. Reduced = %6d.\n",
nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
// perform AIG rewriting on the speculated frames
// convert the manager to SAT solver (the last nLatches outputs are inputs)
pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) );
p->pSat = Cnf_DataWriteIntoSolver( pCnf );
// transfer variable numbers
Aig_ManForEachPi( p->pManAig, pObj, i )
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
{
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
Fra_ObjSetFaninVec( pObj, (void *)1 );
}
Cnf_DataFree( pCnf );
// perform sweeping
Fra_FraigSweep( p );
assert( Vec_PtrSize(p->vTimeouts) == 0 );
Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
sat_solver_delete( p->pSat ); p->pSat = NULL;
}
// move the classes into representatives
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
// implement the classes
pManAigNew = Aig_ManDupRepr( pManAig );
Fra_ManStop( p );
return pManAigNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/fra/fraMan.c
......@@ -53,6 +53,37 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 100; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nTimeFrames = 0; // the number of timeframes to unroll
pPars->fConeBias = 1;
}
/**Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
{
memset( pPars, 0, sizeof(Fra_Par_t) );
pPars->nSimWords = 32; // the number of words in the simulation info
pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pPars->fPatScores = 0; // enables simulation pattern scoring
pPars->MaxScore = 25; // max score after which resimulation is used
pPars->fDoSparse = 1; // skips sparse functions
// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pPars->dActConeBumpMax = 5.0; // the largest bump of activity
pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
pPars->dActConeBumpMax = 10.0; // the largest bump of activity
pPars->nBTLimitNode = 1000000; // conflict limit at a node
pPars->nBTLimitMiter = 500000; // conflict limit at an output
pPars->nTimeFrames = 1; // the number of timeframes to unroll
pPars->fConeBias = 0;
}
/**Function*************************************************************
......@@ -74,47 +105,36 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
memset( p, 0, sizeof(Fra_Man_t) );
p->pPars = pPars;
p->pManAig = pManAig;
p->pManFraig = Aig_ManStartFrom( pManAig );
assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) );
p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
p->nFrames = pPars->nTimeFrames + 1;
// allocate simulation info
p->nSimWords = pPars->nSimWords;
p->pSimWords = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords );
p->nSimWords = pPars->nSimWords * p->nFrames;
p->pSimWords = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords * p->nFrames );
// clean simulation info of the constant node
memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) );
memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords * p->nFrames );
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassOld = Vec_PtrAlloc( 100 );
p->vClassNew = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
p->vTimeouts = Vec_PtrAlloc( 100 );
// equivalence classes
p->pCla = Fra_ClassesStart( pManAig );
// allocate other members
p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1;
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
p->pMemRepr = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
p->pMemReprFra = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
memset( p->pMemReprFra, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc );
memset( p->pMemSatNums, 0, p->nSizeAlloc * sizeof(int) );
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFrames );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFrames );
p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFrames );
memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFrames );
p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFrames );
memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFrames );
// set random number generator
srand( 0xABCABC );
// make sure the satisfying assignment is node assigned
assert( p->pManFraig->pData == NULL );
// connect AIG managers to the FRAIG manager
Fra_ManPrepare( p );
return p;
}
/**Function*************************************************************
Synopsis [Prepares managers by transfering pointers to the objects.]
Synopsis [Prepares the new manager to begin fraiging.]
Description []
......@@ -123,24 +143,54 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
SeeAlso []
***********************************************************************/
void Fra_ManPrepare( Fra_Man_t * p )
Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
{
Aig_Man_t * pManFraig;
Aig_Obj_t * pObj;
int i;
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
assert( p->pManFraig == NULL );
// set the pointer to the manager
Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
// start the fraig package
pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
// set the pointers to the available fraig nodes
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) );
Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
Aig_ManForEachPi( p->pManAig, pObj, i )
Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) );
Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
// set the pointers to the manager
Aig_ManForEachObj( pManFraig, pObj, i )
pObj->pData = p;
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
return pManFraig;
}
/**Function*************************************************************
Synopsis [Finalizes the combinational miter after fraiging.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ManFinalizeComb( Fra_Man_t * p )
{
Aig_Obj_t * pObj;
int i;
// add the POs
Aig_ManForEachPo( p->pManAig, pObj, i )
Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
// postprocess
Aig_ManCleanMarkB( p->pManFraig );
}
/**Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
......@@ -158,19 +208,13 @@ void Fra_ManStop( Fra_Man_t * p )
Vec_PtrFree( p->pMemFanins[i] );
if ( p->pPars->fVerbose )
Fra_ManPrint( p );
if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
if ( p->vClassNew ) Vec_PtrFree( p->vClassNew );
if ( p->vClassOld ) Vec_PtrFree( p->vClassOld );
if ( p->vClasses1 ) Vec_PtrFree( p->vClasses1 );
if ( p->vClasses ) Vec_PtrFree( p->vClasses );
if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
FREE( p->pMemSatNums );
FREE( p->pMemFanins );
FREE( p->pMemRepr );
FREE( p->pMemReprFra );
if ( p->pCla ) Fra_ClassesStop( p->pCla );
FREE( p->pMemFraig );
FREE( p->pMemClasses );
FREE( p->pMemFanins );
FREE( p->pMemSatNums );
FREE( p->pPatScores );
FREE( p->pPatWords );
FREE( p->pSimWords );
......@@ -197,7 +241,7 @@ void Fra_ManPrint( Fra_Man_t * p )
printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG traversal ", p->timeTrav );
......
src/aig/fra/fraSat.c
......@@ -54,7 +54,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 > 10, take the quare root of the limit
nBTLimit = p->pPars->nBTLimitNode;
if ( !p->pPars->fSpeculate && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
if ( !p->pPars->fSpeculate && p->pPars->nTimeFrames == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
{
p->nSatFails++;
// fail immediately
......@@ -78,6 +78,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
Fra_NodeAddToSolver( p, pOld, pNew );
// prepare variable activity
if ( p->pPars->fConeBias )
Fra_SetActivityFactors( p, pOld, pNew );
// solve under assumptions
......@@ -209,6 +210,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
Fra_NodeAddToSolver( p, NULL, pNew );
// prepare variable activity
if ( p->pPars->fConeBias )
Fra_SetActivityFactors( p, NULL, pNew );
// solve under assumptions
......
src/aig/fra/fraSim.c
......@@ -81,12 +81,27 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 )
SeeAlso []
***********************************************************************/
void Fra_AssignRandom( Fra_Man_t * p )
void Fra_AssignRandom( Fra_Man_t * p, int fInit )
{
Aig_Obj_t * pObj;
int i;
int i, k;
if ( fInit )
{
assert( Aig_ManInitNum(p->pManAig) > 0 );
assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// assign random info for primary inputs
Aig_ManForEachPiSeq( p->pManAig, pObj, i )
Fra_NodeAssignRandom( p, pObj );
// assign the initial state for the latches
k = 0;
Aig_ManForEachLoSeq( p->pManAig, pObj, i )
Fra_NodeAssignConst( p, pObj, Vec_IntEntry(p->pManAig->vInits,k++) );
}
else
{
Aig_ManForEachPi( p->pManAig, pObj, i )
Fra_NodeAssignRandom( p, pObj );
}
}
/**Function*************************************************************
......@@ -105,12 +120,8 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
Aig_Obj_t * pObj;
int i, Limit;
Aig_ManForEachPi( p->pManAig, pObj, i )
{
Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) );
// printf( "%d", Aig_InfoHasBit(pPat, i) );
}
// printf( "\n" );
Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
Limit = AIG_MIN( Aig_ManPiNum(p->pManAig) - Aig_ManInitNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
}
......@@ -126,15 +137,14 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
SeeAlso []
***********************************************************************/
int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj )
void Fra_NodeComplementSim( Aig_Obj_t * pObj )
{
Fra_Man_t * p = pObj->pData;
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims[i] )
return 0;
return 1;
pSims[i] = ~pSims[i];
}
/**Function*************************************************************
......@@ -148,13 +158,16 @@ int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
void Fra_NodeComplementSim( Fra_Man_t * p, Aig_Obj_t * pObj )
int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
{
Fra_Man_t * p = pObj->pData;
unsigned * pSims;
int i;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims[i] = ~pSims[i];
if ( pSims[i] )
return 0;
return 1;
}
/**Function*************************************************************
......@@ -168,8 +181,9 @@ void Fra_NodeComplementSim( Fra_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
Fra_Man_t * p = pObj0->pData;
unsigned * pSims0, * pSims1;
int i;
pSims0 = Fra_ObjSim(pObj0);
......@@ -180,6 +194,45 @@ int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
return 1;
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
{
Fra_Man_t * p = pObj->pData;
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
unsigned uHash;
int i;
assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Fra_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
uHash ^= pSims[i] * s_FPrimes[i];
return uHash;
}
/**Function*************************************************************
......@@ -245,6 +298,7 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
}
}
/**Function*************************************************************
Synopsis [Generated const 0 pattern.]
......@@ -294,10 +348,8 @@ void Fra_SavePattern( Fra_Man_t * p )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pManFraig, pObj, i )
// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
Aig_InfoSetBit( p->pPatWords, i );
// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
......@@ -433,15 +485,17 @@ p->nSimRounds++;
***********************************************************************/
void Fra_Resimulate( Fra_Man_t * p )
{
int nChanges;
int nChanges, clk;
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
if ( p->pPars->fPatScores )
Fra_CleanPatScores( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
p->timeRef += clock() - clk;
if ( nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
......@@ -456,10 +510,12 @@ void Fra_Resimulate( Fra_Man_t * p )
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
Fra_CleanPatScores( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
p->timeRef += clock() - clk;
//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
if ( nChanges == 0 )
break;
......@@ -477,43 +533,50 @@ void Fra_Resimulate( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
void Fra_Simulate( Fra_Man_t * p )
void Fra_Simulate( Fra_Man_t * p, int fInit )
{
int nChanges, nClasses;
int nChanges, nClasses, clk;
assert( !fInit || Aig_ManInitNum(p->pManAig) );
// start the classes
Fra_AssignRandom( p );
Fra_AssignRandom( p, fInit );
Fra_SimulateOne( p );
Fra_CreateClasses( p );
Fra_ClassesPrepare( p->pCla );
//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
// refine classes by walking 0/1 patterns
Fra_SavePattern0( p );
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
p->timeRef += clock() - clk;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
Fra_SavePattern1( p );
Fra_AssignDist1( p, p->pPatWords );
Fra_SimulateOne( p );
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
p->timeRef += clock() - clk;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
// refine classes by random simulation
do {
Fra_AssignRandom( p );
Fra_AssignRandom( p, fInit );
Fra_SimulateOne( p );
nClasses = Vec_PtrSize(p->vClasses);
nChanges = Fra_RefineClasses( p );
nChanges += Fra_RefineClasses1( p );
if ( p->pManFraig->pData )
nClasses = Vec_PtrSize(p->pCla->vClasses);
if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
return;
clk = clock();
nChanges = Fra_ClassesRefine( p->pCla );
nChanges += Fra_ClassesRefine1( p->pCla );
p->timeRef += clock() - clk;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
// Fra_PrintClasses( p );
// Fra_ClassesPrint( p->pCla );
}
/**Function*************************************************************
......@@ -578,19 +641,12 @@ int Fra_CheckOutputSims( Fra_Man_t * p )
assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0
Aig_ManForEachPo( p->pManAig, pObj, i )
{
// complement simulation info
// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) // Aig_ObjFaninPhase(Aig_ObjChild0(pObj))
// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
// check
if ( !Fra_NodeHasZeroSim( p, Aig_ObjFanin0(pObj) ) )
if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
return 1;
}
// complement simulation info
// if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
// Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
}
return 0;
}
......
src/aig/fra/ivyFraig.c deleted 100644 → 0
/**CFile****************************************************************
FileName [ivyFraig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Functional reduction of AIGs]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
***********************************************************************/
#include "satSolver.h"
#include "extra.h"
#include "ivy.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Ivy_FraigMan_t_ Ivy_FraigMan_t;
typedef struct Ivy_FraigSim_t_ Ivy_FraigSim_t;
typedef struct Ivy_FraigList_t_ Ivy_FraigList_t;
struct Ivy_FraigList_t_
{
Ivy_Obj_t * pHead;
Ivy_Obj_t * pTail;
int nItems;
};
struct Ivy_FraigSim_t_
{
int Type;
Ivy_FraigSim_t * pNext;
Ivy_FraigSim_t * pFanin0;
Ivy_FraigSim_t * pFanin1;
unsigned pData[0];
};
struct Ivy_FraigMan_t_
{
// general info
Ivy_FraigParams_t * pParams; // various parameters
// temporary backtrack limits because "sint64" cannot be defined in Ivy_FraigParams_t ...
sint64 nBTLimitGlobal; // global limit on the number of backtracks
sint64 nInsLimitGlobal;// global limit on the number of clause inspects
// AIG manager
Ivy_Man_t * pManAig; // the starting AIG manager
Ivy_Man_t * pManFraig; // the final AIG manager
// simulation information
int nSimWords; // the number of words
char * pSimWords; // the simulation info
Ivy_FraigSim_t * pSimStart; // the list of simulation info for internal nodes
// counter example storage
int nPatWords; // the number of words in the counter example
unsigned * pPatWords; // the counter example
int * pPatScores; // the scores of each pattern
// equivalence classes
Ivy_FraigList_t lClasses; // equivalence classes
Ivy_FraigList_t lCand; // candidatates
int nPairs; // the number of pairs of nodes
// equivalence checking
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables currently used
Vec_Ptr_t * vPiVars; // the PIs of the cone used
// other
ProgressBar * pProgress;
// statistics
int nSimRounds;
int nNodesMiter;
int nClassesZero;
int nClassesBeg;
int nClassesEnd;
int nPairsBeg;
int nPairsEnd;
int nSatCalls;
int nSatCallsSat;
int nSatCallsUnsat;
int nSatProof;
int nSatFails;
int nSatFailsReal;
// runtime
int timeSim;
int timeTrav;
int timeSat;
int timeSatUnsat;
int timeSatSat;
int timeSatFail;
int timeRef;
int timeTotal;
int time1;
int time2;
};
typedef struct Prove_ParamsStruct_t_ Prove_Params_t;
struct Prove_ParamsStruct_t_
{
// general parameters
int fUseFraiging; // enables fraiging
int fUseRewriting; // enables rewriting
int fUseBdds; // enables BDD construction when other methods fail
int fVerbose; // prints verbose stats
// iterations
int nItersMax; // the number of iterations
// mitering
int nMiteringLimitStart; // starting mitering limit
float nMiteringLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// rewriting
int nRewritingLimitStart; // the number of rewriting iterations
float nRewritingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// fraiging
int nFraigingLimitStart; // starting backtrack(conflict) limit
float nFraigingLimitMulti; // multiplicative coefficient to increase the limit in each iteration
// last-gasp BDD construction
int nBddSizeLimit; // the number of BDD nodes when construction is aborted
int fBddReorder; // enables dynamic BDD variable reordering
// last-gasp mitering
int nMiteringLimitLast; // final mitering limit
// global SAT solver limits
sint64 nTotalBacktrackLimit; // global limit on the number of backtracks
sint64 nTotalInspectLimit; // global limit on the number of clause inspects
// global resources applied
sint64 nTotalBacktracksMade; // the total number of backtracks made
sint64 nTotalInspectsMade; // the total number of inspects made
};
static inline Ivy_FraigSim_t * Ivy_ObjSim( Ivy_Obj_t * pObj ) { return (Ivy_FraigSim_t *)pObj->pFanout; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj ) { return pObj->pNextFan0; }
static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj ) { return pObj->pNextFan1; }
static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj ) { return pObj->pPrevFan0; }
static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj ) { return pObj->pPrevFan1; }
static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj ) { return pObj->pEquiv; }
static inline int Ivy_ObjSatNum( Ivy_Obj_t * pObj ) { return (int)pObj->pNextFan0; }
static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj ) { return (Vec_Ptr_t *)pObj->pNextFan1; }
static inline void Ivy_ObjSetSim( Ivy_Obj_t * pObj, Ivy_FraigSim_t * pSim ) { pObj->pFanout = (Ivy_Obj_t *)pSim; }
static inline void Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
static inline void Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
static inline void Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
static inline void Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
static inline void Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
static inline void Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
static inline void Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode ) { pObj->pEquiv = pNode; }
static inline void Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num ) { pObj->pNextFan0 = (Ivy_Obj_t *)Num; }
static inline void Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins ) { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
static inline unsigned Ivy_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
// iterate through equivalence classes
#define Ivy_FraigForEachEquivClass( pList, pEnt ) \
for ( pEnt = pList; \
pEnt; \
pEnt = Ivy_ObjEquivListNext(pEnt) )
#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 ) \
for ( pEnt = pList, \
pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL; \
pEnt; \
pEnt = pEnt2, \
pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
// iterate through nodes in one class
#define Ivy_FraigForEachClassNode( pClass, pEnt ) \
for ( pEnt = pClass; \
pEnt; \
pEnt = Ivy_ObjClassNodeNext(pEnt) )
// iterate through nodes in the hash table
#define Ivy_FraigForEachBinNode( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = Ivy_ObjNodeHashNext(pEnt) )
static Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
static Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
static Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects );
static void Ivy_FraigPrint( Ivy_FraigMan_t * p );
static void Ivy_FraigStop( Ivy_FraigMan_t * p );
static void Ivy_FraigSimulate( Ivy_FraigMan_t * p );
static void Ivy_FraigSweep( Ivy_FraigMan_t * p );
static Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld );
static int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
static int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj );
static void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
static int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew );
static void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew );
static int Ivy_FraigMiterStatus( Ivy_Man_t * pMan );
static void Ivy_FraigMiterProve( Ivy_FraigMan_t * p );
static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose );
static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
static sint64 s_nBTLimitGlobal = 0;
static sint64 s_nInsLimitGlobal = 0;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
{
memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
pParams->nSimWords = 32; // the number of words in the simulation info
pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
pParams->fPatScores = 0; // enables simulation pattern scoring
pParams->MaxScore = 25; // max score after which resimulation is used
pParams->fDoSparse = 1; // skips sparse functions
// pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped
// pParams->dActConeBumpMax = 5.0; // the largest bump of activity
pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped
pParams->dActConeBumpMax = 10.0; // the largest bump of activity
pParams->nBTLimitNode = 100; // conflict limit at a node
pParams->nBTLimitMiter = 500000; // conflict limit at an output
// pParams->nBTLimitGlobal = 0; // conflict limit global
// pParams->nInsLimitGlobal = 0; // inspection limit global
}
/**Function*************************************************************
Synopsis [Performs combinational equivalence checking for the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars )
{
Prove_Params_t * pParams = pPars;
Ivy_FraigParams_t Params, * pIvyParams = &Params;
Ivy_Man_t * pManAig, * pManTemp;
int RetValue, nIter, clk, timeStart = clock();//, Counter;
sint64 nSatConfs, nSatInspects;
// start the network and parameters
pManAig = *ppManAig;
Ivy_FraigParamsDefault( pIvyParams );
pIvyParams->fVerbose = pParams->fVerbose;
pIvyParams->fProve = 1;
if ( pParams->fVerbose )
{
printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" );
printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n",
pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti,
pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti,
pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti );
printf( "Mitering last = %d.\n",
pParams->nMiteringLimitLast );
}
// if SAT only, solve without iteration
if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
{
clk = clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
RetValue = Ivy_FraigMiterStatus( pManAig );
Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
*ppManAig = pManAig;
return RetValue;
}
if ( Ivy_ManNodeNum(pManAig) < 500 )
{
// run the first mitering
clk = clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
RetValue = Ivy_FraigMiterStatus( pManAig );
Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
if ( RetValue >= 0 )
{
*ppManAig = pManAig;
return RetValue;
}
}
// check the current resource limits
RetValue = -1;
for ( nIter = 0; nIter < pParams->nItersMax; nIter++ )
{
if ( pParams->fVerbose )
{
printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1,
(int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)),
(int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) );
fflush( stdout );
}
// try rewriting
if ( pParams->fUseRewriting )
{ // bug in Ivy_NodeFindCutsAll() when leaves are identical!
/*
clk = clock();
Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
pManAig = Ivy_ManRwsat( pManAig, 0 );
RetValue = Ivy_FraigMiterStatus( pManAig );
Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose );
*/
}
if ( RetValue >= 0 )
break;
// try fraiging followed by mitering
if ( pParams->fUseFraiging )
{
clk = clock();
pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter));
pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig);
pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp );
RetValue = Ivy_FraigMiterStatus( pManAig );
Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose );
}
if ( RetValue >= 0 )
break;
// add to the number of backtracks and inspects
pParams->nTotalBacktracksMade += nSatConfs;
pParams->nTotalInspectsMade += nSatInspects;
// check if global resource limit is reached
if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
(pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) )
{
printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
*ppManAig = pManAig;
return -1;
}
}
if ( RetValue < 0 )
{
if ( pParams->fVerbose )
{
printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast );
fflush( stdout );
}
clk = clock();
pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig);
if ( pParams->nTotalBacktrackLimit )
s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade;
if ( pParams->nTotalInspectLimit )
s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade;
pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp );
s_nBTLimitGlobal = 0;
s_nInsLimitGlobal = 0;
RetValue = Ivy_FraigMiterStatus( pManAig );
Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose );
// make sure that the sover never returns "undecided" when infinite resource limits are set
if( RetValue == -1 && pParams->nTotalInspectLimit == 0 &&
pParams->nTotalBacktrackLimit == 0 )
{
extern void Prove_ParamsPrint( Prove_Params_t * pParams );
Prove_ParamsPrint( pParams );
printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n");
exit(1);
}
}
// assign the model if it was proved by rewriting (const 1 miter)
if ( RetValue == 0 && pManAig->pData == NULL )
{
pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) );
memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) );
}
*ppManAig = pManAig;
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Ivy_FraigPerform_int( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams, sint64 nBTLimitGlobal, sint64 nInsLimitGlobal, sint64 * pnSatConfs, sint64 * pnSatInspects )
{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
int clk;
if ( Ivy_ManNodeNum(pManAig) == 0 )
return Ivy_ManDup(pManAig);
clk = clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
// set global limits
p->nBTLimitGlobal = nBTLimitGlobal;
p->nInsLimitGlobal = nInsLimitGlobal;
Ivy_FraigSimulate( p );
Ivy_FraigSweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
if ( pnSatConfs )
*pnSatConfs = p->pSat? p->pSat->stats.conflicts : 0;
if ( pnSatInspects )
*pnSatInspects = p->pSat? p->pSat->stats.inspects : 0;
Ivy_FraigStop( p );
return pManAigNew;
}
/**Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
int clk;
if ( Ivy_ManNodeNum(pManAig) == 0 )
return Ivy_ManDup(pManAig);
clk = clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStart( pManAig, pParams );
Ivy_FraigSimulate( p );
Ivy_FraigSweep( p );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
Ivy_FraigStop( p );
return pManAigNew;
}
/**Function*************************************************************
Synopsis [Applies brute-force SAT to the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Man_t * Ivy_FraigMiter( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
Ivy_FraigMan_t * p;
Ivy_Man_t * pManAigNew;
Ivy_Obj_t * pObj;
int i, clk;
clk = clock();
assert( Ivy_ManLatchNum(pManAig) == 0 );
p = Ivy_FraigStartSimple( pManAig, pParams );
// set global limits
p->nBTLimitGlobal = s_nBTLimitGlobal;
p->nInsLimitGlobal = s_nInsLimitGlobal;
// duplicate internal nodes
Ivy_ManForEachNode( p->pManAig, pObj, i )
pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
// try to prove each output of the miter
Ivy_FraigMiterProve( p );
// add the POs
Ivy_ManForEachPo( p->pManAig, pObj, i )
Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
// clean the new manager
Ivy_ManForEachObj( p->pManFraig, pObj, i )
{
if ( Ivy_ObjFaninVec(pObj) )
Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
pObj->pNextFan0 = pObj->pNextFan1 = NULL;
}
// remove dangling nodes
Ivy_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->timeTotal = clock() - clk;
//printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) );
//PRT( "Time", p->timeTotal );
Ivy_FraigStop( p );
return pManAigNew;
}
/**Function*************************************************************
Synopsis [Starts the fraiging manager without simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_FraigMan_t * Ivy_FraigStartSimple( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
Ivy_FraigMan_t * p;
// allocat the fraiging manager
p = ALLOC( Ivy_FraigMan_t, 1 );
memset( p, 0, sizeof(Ivy_FraigMan_t) );
p->pParams = pParams;
p->pManAig = pManAig;
p->pManFraig = Ivy_ManStartFrom( pManAig );
p->vPiVars = Vec_PtrAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis [Starts the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
{
Ivy_FraigMan_t * p;
Ivy_FraigSim_t * pSims;
Ivy_Obj_t * pObj;
int i, k, EntrySize;
// clean the fanout representation
Ivy_ManForEachObj( pManAig, pObj, i )
// pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
assert( !pObj->pEquiv && !pObj->pFanout );
// allocat the fraiging manager
p = ALLOC( Ivy_FraigMan_t, 1 );
memset( p, 0, sizeof(Ivy_FraigMan_t) );
p->pParams = pParams;
p->pManAig = pManAig;
p->pManFraig = Ivy_ManStartFrom( pManAig );
// allocate simulation info
p->nSimWords = pParams->nSimWords;
// p->pSimWords = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nSimWords );
EntrySize = sizeof(Ivy_FraigSim_t) + sizeof(unsigned) * p->nSimWords;
p->pSimWords = (char *)malloc( Ivy_ManObjNum(pManAig) * EntrySize );
memset( p->pSimWords, 0, EntrySize );
k = 0;
Ivy_ManForEachObj( pManAig, pObj, i )
{
pSims = (Ivy_FraigSim_t *)(p->pSimWords + EntrySize * k++);
pSims->pNext = NULL;
if ( Ivy_ObjIsNode(pObj) )
{
if ( p->pSimStart == NULL )
p->pSimStart = pSims;
else
((Ivy_FraigSim_t *)(p->pSimWords + EntrySize * (k-2)))->pNext = pSims;
pSims->pFanin0 = Ivy_ObjSim( Ivy_ObjFanin0(pObj) );
pSims->pFanin1 = Ivy_ObjSim( Ivy_ObjFanin1(pObj) );
pSims->Type = (Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) << 2) | (Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)) << 1) | pObj->fPhase;
}
else
{
pSims->pFanin0 = NULL;
pSims->pFanin1 = NULL;
pSims->Type = 0;
}
Ivy_ObjSetSim( pObj, pSims );
}
assert( k == Ivy_ManObjNum(pManAig) );
// allocate storage for sim pattern
p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
p->pPatWords = ALLOC( unsigned, p->nPatWords );
p->pPatScores = ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
// set random number generator
srand( 0xABCABC );
return p;
}
/**Function*************************************************************
Synopsis [Stops the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigStop( Ivy_FraigMan_t * p )
{
if ( p->pParams->fVerbose )
Ivy_FraigPrint( p );
if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
FREE( p->pPatScores );
FREE( p->pPatWords );
FREE( p->pSimWords );
free( p );
}
/**Function*************************************************************
Synopsis [Prints stats for the fraiging manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigPrint( Ivy_FraigMan_t * p )
{
double nMemory;
nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nSimWords*sizeof(unsigned)/(1<<20);
printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory );
printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pParams->nBTLimitNode, p->pParams->nBTLimitMiter );
printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n",
Ivy_ManNodeNum(p->pManFraig), p->nNodesMiter, Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->timeSim );
PRT( "AIG traversal ", p->timeTrav );
PRT( "SAT solving ", p->timeSat );
PRT( " Unsat ", p->timeSatUnsat );
PRT( " Sat ", p->timeSatSat );
PRT( " Fail ", p->timeSatFail );
PRT( "Class refining ", p->timeRef );
PRT( "TOTAL RUNTIME ", p->timeTotal );
if ( p->time1 ) { PRT( "time1 ", p->time1 ); }
}
/**Function*************************************************************
Synopsis [Assigns random patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeAssignRandom( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
Ivy_FraigSim_t * pSims;
int i;
assert( Ivy_ObjIsPi(pObj) );
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = Ivy_ObjRandomSim();
}
/**Function*************************************************************
Synopsis [Assigns constant patterns to the PI node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeAssignConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int fConst1 )
{
Ivy_FraigSim_t * pSims;
int i;
assert( Ivy_ObjIsPi(pObj) );
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = fConst1? ~(unsigned)0 : 0;
}
/**Function*************************************************************
Synopsis [Assings random simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAssignRandom( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
Ivy_ManForEachPi( p->pManAig, pObj, i )
Ivy_NodeAssignRandom( p, pObj );
}
/**Function*************************************************************
Synopsis [Assings distance-1 simulation info for the PIs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
{
Ivy_Obj_t * pObj;
int i, Limit;
Ivy_ManForEachPi( p->pManAig, pObj, i )
Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
for ( i = 0; i < Limit; i++ )
Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
Ivy_FraigSim_t * pSims;
int i;
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims->pData[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
Ivy_FraigSim_t * pSims;
int i;
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = ~pSims->pData[i];
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_NodeCompareSims( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
{
Ivy_FraigSim_t * pSims0, * pSims1;
int i;
pSims0 = Ivy_ObjSim(pObj0);
pSims1 = Ivy_ObjSim(pObj1);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims0->pData[i] != pSims1->pData[i] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeSimulateSim( Ivy_FraigMan_t * p, Ivy_FraigSim_t * pSims )
{
unsigned * pData, * pData0, * pData1;
int i;
pData = pSims->pData;
pData0 = pSims->pFanin0->pData;
pData1 = pSims->pFanin1->pData;
switch( pSims->Type )
{
case 0:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (pData0[i] & pData1[i]);
break;
case 1:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = ~(pData0[i] & pData1[i]);
break;
case 2:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (pData0[i] & ~pData1[i]);
break;
case 3:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (~pData0[i] | pData1[i]);
break;
case 4:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (~pData0[i] & pData1[i]);
break;
case 5:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (pData0[i] | ~pData1[i]);
break;
case 6:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = ~(pData0[i] | pData1[i]);
break;
case 7:
for ( i = 0; i < p->nSimWords; i++ )
pData[i] = (pData0[i] | pData1[i]);
break;
}
}
/**Function*************************************************************
Synopsis [Simulates one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeSimulate( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
Ivy_FraigSim_t * pSims, * pSims0, * pSims1;
int fCompl, fCompl0, fCompl1, i;
assert( !Ivy_IsComplement(pObj) );
// get hold of the simulation information
pSims = Ivy_ObjSim(pObj);
pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
// get complemented attributes of the children using their random info
fCompl = pObj->fPhase;
fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
// simulate
if ( fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (pSims0->pData[i] | pSims1->pData[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = ~(pSims0->pData[i] | pSims1->pData[i]);
}
else if ( fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (pSims0->pData[i] | ~pSims1->pData[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (~pSims0->pData[i] & pSims1->pData[i]);
}
else if ( !fCompl0 && fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (~pSims0->pData[i] | pSims1->pData[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (pSims0->pData[i] & ~pSims1->pData[i]);
}
else // if ( !fCompl0 && !fCompl1 )
{
if ( fCompl )
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = ~(pSims0->pData[i] & pSims1->pData[i]);
else
for ( i = 0; i < p->nSimWords; i++ )
pSims->pData[i] = (pSims0->pData[i] & pSims1->pData[i]);
}
}
/**Function*************************************************************
Synopsis [Computes hash value using simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ivy_NodeHash( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
static int s_FPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
Ivy_FraigSim_t * pSims;
unsigned uHash;
int i;
assert( p->nSimWords <= 128 );
uHash = 0;
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
uHash ^= pSims->pData[i] * s_FPrimes[i];
return uHash;
}
/**Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSimulateOne( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i, clk;
clk = clock();
Ivy_ManForEachNode( p->pManAig, pObj, i )
{
Ivy_NodeSimulate( p, pObj );
/*
if ( Ivy_ObjFraig(pObj) == NULL )
printf( "%3d --- -- %d : ", pObj->Id, pObj->fPhase );
else
printf( "%3d %3d %2d %d : ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
printf( "\n" );
*/
}
p->timeSim += clock() - clk;
p->nSimRounds++;
}
/**Function*************************************************************
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSimulateOneSim( Ivy_FraigMan_t * p )
{
Ivy_FraigSim_t * pSims;
int clk;
clk = clock();
for ( pSims = p->pSimStart; pSims; pSims = pSims->pNext )
Ivy_NodeSimulateSim( p, pSims );
p->timeSim += clock() - clk;
p->nSimRounds++;
}
/**Function*************************************************************
Synopsis [Adds one node to the equivalence class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
{
if ( Ivy_ObjClassNodeNext(pClass) == NULL )
Ivy_ObjSetClassNodeNext( pClass, pObj );
else
Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
Ivy_ObjSetClassNodeLast( pClass, pObj );
Ivy_ObjSetClassNodeRepr( pObj, pClass );
Ivy_ObjSetClassNodeNext( pObj, NULL );
}
/**Function*************************************************************
Synopsis [Adds equivalence class to the list of classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAddClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
{
if ( pList->pHead == NULL )
{
pList->pHead = pClass;
pList->pTail = pClass;
Ivy_ObjSetEquivListPrev( pClass, NULL );
Ivy_ObjSetEquivListNext( pClass, NULL );
}
else
{
Ivy_ObjSetEquivListNext( pList->pTail, pClass );
Ivy_ObjSetEquivListPrev( pClass, pList->pTail );
Ivy_ObjSetEquivListNext( pClass, NULL );
pList->pTail = pClass;
}
pList->nItems++;
}
/**Function*************************************************************
Synopsis [Updates the list of classes after base class has split.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigInsertClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
{
Ivy_ObjSetEquivListPrev( pClass, pBase );
Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) );
if ( Ivy_ObjEquivListNext(pBase) )
Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
Ivy_ObjSetEquivListNext( pBase, pClass );
if ( pList->pTail == pBase )
pList->pTail = pClass;
pList->nItems++;
}
/**Function*************************************************************
Synopsis [Removes equivalence class from the list of classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigRemoveClass( Ivy_FraigList_t * pList, Ivy_Obj_t * pClass )
{
if ( pList->pHead == pClass )
pList->pHead = Ivy_ObjEquivListNext(pClass);
if ( pList->pTail == pClass )
pList->pTail = Ivy_ObjEquivListPrev(pClass);
if ( Ivy_ObjEquivListPrev(pClass) )
Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) );
if ( Ivy_ObjEquivListNext(pClass) )
Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
Ivy_ObjSetEquivListNext( pClass, NULL );
Ivy_ObjSetEquivListPrev( pClass, NULL );
pClass->fMarkA = 0;
pList->nItems--;
}
/**Function*************************************************************
Synopsis [Count the number of pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigCountPairsClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass, * pNode;
int nPairs = 0, nNodes;
return nPairs;
Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
{
nNodes = 0;
Ivy_FraigForEachClassNode( pClass, pNode )
nNodes++;
nPairs += nNodes * (nNodes - 1) / 2;
}
return nPairs;
}
/**Function*************************************************************
Synopsis [Creates initial simulation classes.]
Description [Assumes that simulation info is assigned.]
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigCreateClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t ** pTable;
Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry;
int i, nTableSize;
unsigned Hash;
pConst1 = Ivy_ManConst1(p->pManAig);
// allocate the table
nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
pTable = ALLOC( Ivy_Obj_t *, nTableSize );
memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
// collect nodes into the table
Ivy_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
continue;
Hash = Ivy_NodeHash( p, pObj );
if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
{
Ivy_NodeAddToClass( pConst1, pObj );
continue;
}
// add the node to the table
pBin = pTable[Hash % nTableSize];
Ivy_FraigForEachBinNode( pBin, pEntry )
if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
{
Ivy_NodeAddToClass( pEntry, pObj );
break;
}
// check if the entry was added
if ( pEntry )
continue;
Ivy_ObjSetNodeHashNext( pObj, pBin );
pTable[Hash % nTableSize] = pObj;
}
// collect non-trivial classes
assert( p->lClasses.pHead == NULL );
Ivy_ManForEachObj( p->pManAig, pObj, i )
{
if ( !Ivy_ObjIsConst1(pObj) && !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
continue;
Ivy_ObjSetNodeHashNext( pObj, NULL );
if ( Ivy_ObjClassNodeRepr(pObj) == NULL )
{
assert( Ivy_ObjClassNodeNext(pObj) == NULL );
continue;
}
// recognize the head of the class
if ( Ivy_ObjClassNodeNext( Ivy_ObjClassNodeRepr(pObj) ) != NULL )
continue;
// clean the class representative and add it to the list
Ivy_ObjSetClassNodeRepr( pObj, NULL );
Ivy_FraigAddClass( &p->lClasses, pObj );
}
// free the table
free( pTable );
}
/**Function*************************************************************
Synopsis [Recursively refines the class after simulation.]
Description [Returns 1 if the class has changed.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass )
{
Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
int RetValue = 0;
// check if there is refinement
pListOld = pClass;
Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
{
if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
{
if ( p->pParams->fPatScores )
Ivy_FraigAddToPatScores( p, pClass, pClassNew );
break;
}
pListOld = pClassNew;
}
if ( pClassNew == NULL )
return 0;
// set representative of the new class
Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
// start the new list
pListNew = pClassNew;
// go through the remaining nodes and sort them into two groups:
// (1) matches of the old node; (2) non-matches of the old node
Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
{
Ivy_ObjSetClassNodeNext( pListOld, pNode );
pListOld = pNode;
}
else
{
Ivy_ObjSetClassNodeNext( pListNew, pNode );
Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
pListNew = pNode;
}
// finish both lists
Ivy_ObjSetClassNodeNext( pListNew, NULL );
Ivy_ObjSetClassNodeNext( pListOld, NULL );
// update the list of classes
Ivy_FraigInsertClass( &p->lClasses, pClass, pClassNew );
// if the old class is trivial, remove it
if ( Ivy_ObjClassNodeNext(pClass) == NULL )
Ivy_FraigRemoveClass( &p->lClasses, pClass );
// if the new class is trivial, remove it; otherwise, try to refine it
if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
Ivy_FraigRemoveClass( &p->lClasses, pClassNew );
else
RetValue = Ivy_FraigRefineClass_rec( p, pClassNew );
return RetValue + 1;
}
/**Function*************************************************************
Synopsis [Creates the counter-example from the successful pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
{
Ivy_FraigSim_t * pSims;
int i, k, BestPat, * pModel;
// find the word of the pattern
pSims = Ivy_ObjSim(pObj);
for ( i = 0; i < p->nSimWords; i++ )
if ( pSims->pData[i] )
break;
assert( i < p->nSimWords );
// find the bit of the pattern
for ( k = 0; k < 32; k++ )
if ( pSims->pData[i] & (1 << k) )
break;
assert( k < 32 );
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
Ivy_ManForEachPi( p->pManAig, pObj, i )
{
pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
// printf( "%d", pModel[i] );
}
// printf( "\n" );
// set the model
assert( p->pManFraig->pData == NULL );
p->pManFraig->pData = pModel;
return;
}
/**Function*************************************************************
Synopsis [Returns 1 if the one of the output is already non-constant 0.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
// make sure the reference simulation pattern does not detect the bug
pObj = Ivy_ManPo( p->pManAig, 0 );
assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
Ivy_ManForEachPo( p->pManAig, pObj, i )
{
// complement simulation info
// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
// check
if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
return 1;
}
// complement simulation info
// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
}
return 0;
}
/**Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description [Assumes that simulation info is assigned. Returns the
number of classes refined.]
SideEffects [Large equivalence class of constant 0 may cause problems.]
SeeAlso []
***********************************************************************/
int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass, * pClass2;
int clk, RetValue, Counter = 0;
// check if some outputs already became non-constant
// this is a special case when computation can be stopped!!!
if ( p->pParams->fProve )
Ivy_FraigCheckOutputSims( p );
if ( p->pManFraig->pData )
return 0;
// refine the classed
clk = clock();
Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 )
{
if ( pClass->fMarkA )
continue;
RetValue = Ivy_FraigRefineClass_rec( p, pClass );
Counter += ( RetValue > 0 );
//if ( Ivy_ObjIsConst1(pClass) )
//printf( "%d ", RetValue );
//if ( Ivy_ObjIsConst1(pClass) )
// p->time1 += clock() - clk;
}
p->timeRef += clock() - clk;
return Counter;
}
/**Function*************************************************************
Synopsis [Print the class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
{
Ivy_Obj_t * pObj;
printf( "Class {" );
Ivy_FraigForEachClassNode( pClass, pObj )
printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
printf( " }\n" );
}
/**Function*************************************************************
Synopsis [Count the number of elements in the class.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
{
Ivy_Obj_t * pObj;
int Counter = 0;
Ivy_FraigForEachClassNode( pClass, pObj )
Counter++;
return Counter;
}
/**Function*************************************************************
Synopsis [Prints simulation classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigPrintSimClasses( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pClass;
Ivy_FraigForEachEquivClass( p->lClasses.pHead, pClass )
{
// Ivy_FraigPrintClass( pClass );
printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
}
// printf( "\n" );
}
/**Function*************************************************************
Synopsis [Generated const 0 pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSavePattern0( Ivy_FraigMan_t * p )
{
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
}
/**Function*************************************************************
Synopsis [[Generated const 1 pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSavePattern1( Ivy_FraigMan_t * p )
{
memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
}
/**Function*************************************************************
Synopsis [Generates the counter-example satisfying the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p )
{
int * pModel;
Ivy_Obj_t * pObj;
int i;
pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
Ivy_ManForEachPi( p->pManFraig, pObj, i )
pModel[i] = ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True );
return pModel;
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSavePattern( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Ivy_ManForEachPi( p->pManFraig, pObj, i )
// Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
Ivy_InfoSetBit( p->pPatWords, i );
// Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSavePattern2( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
// Ivy_ManForEachPi( p->pManFraig, pObj, i )
Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
// Ivy_InfoSetBit( p->pPatWords, i );
Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
for ( i = 0; i < p->nPatWords; i++ )
p->pPatWords[i] = Ivy_ObjRandomSim();
Vec_PtrForEachEntry( p->vPiVars, pObj, i )
if ( Ivy_InfoHasBit( p->pPatWords, pObj->Id - 1 ) ^ (p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True) )
Ivy_InfoXorBit( p->pPatWords, pObj->Id - 1 );
}
/**Function*************************************************************
Synopsis [Performs simulation of the manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSimulate( Ivy_FraigMan_t * p )
{
int nChanges, nClasses;
// start the classes
Ivy_FraigAssignRandom( p );
Ivy_FraigSimulateOne( p );
Ivy_FraigCreateClasses( p );
//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Ivy_FraigCountPairsClasses(p) );
// refine classes by walking 0/1 patterns
Ivy_FraigSavePattern0( p );
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
nChanges = Ivy_FraigRefineClasses( p );
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
Ivy_FraigSavePattern1( p );
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
nChanges = Ivy_FraigRefineClasses( p );
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
// refine classes by random simulation
do {
Ivy_FraigAssignRandom( p );
Ivy_FraigSimulateOne( p );
nClasses = p->lClasses.nItems;
nChanges = Ivy_FraigRefineClasses( p );
if ( p->pManFraig->pData )
return;
//printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
} while ( (double)nChanges / nClasses > p->pParams->dSimSatur );
// Ivy_FraigPrintSimClasses( p );
}
/**Function*************************************************************
Synopsis [Cleans pattern scores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigCleanPatScores( Ivy_FraigMan_t * p )
{
int i, nLimit = p->nSimWords * 32;
for ( i = 0; i < nLimit; i++ )
p->pPatScores[i] = 0;
}
/**Function*************************************************************
Synopsis [Adds to pattern scores.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAddToPatScores( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass, Ivy_Obj_t * pClassNew )
{
Ivy_FraigSim_t * pSims0, * pSims1;
unsigned uDiff;
int i, w;
// get hold of the simulation information
pSims0 = Ivy_ObjSim(pClass);
pSims1 = Ivy_ObjSim(pClassNew);
// iterate through the differences and record the score
for ( w = 0; w < p->nSimWords; w++ )
{
uDiff = pSims0->pData[w] ^ pSims1->pData[w];
if ( uDiff == 0 )
continue;
for ( i = 0; i < 32; i++ )
if ( uDiff & ( 1 << i ) )
p->pPatScores[w*32+i]++;
}
}
/**Function*************************************************************
Synopsis [Selects the best pattern.]
Description [Returns 1 if such pattern is found.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigSelectBestPat( Ivy_FraigMan_t * p )
{
Ivy_FraigSim_t * pSims;
Ivy_Obj_t * pObj;
int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
for ( i = 1; i < nLimit; i++ )
{
if ( MaxScore < p->pPatScores[i] )
{
MaxScore = p->pPatScores[i];
BestPat = i;
}
}
if ( MaxScore == 0 )
return 0;
// if ( MaxScore > p->pParams->MaxScore )
// printf( "Max score is %3d. ", MaxScore );
// copy the best pattern into the selected pattern
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Ivy_ManForEachPi( p->pManAig, pObj, i )
{
pSims = Ivy_ObjSim(pObj);
if ( Ivy_InfoHasBit(pSims->pData, BestPat) )
Ivy_InfoSetBit(p->pPatWords, i);
}
return MaxScore;
}
/**Function*************************************************************
Synopsis [Resimulates fraiging manager after finding a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
{
int nChanges;
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
if ( p->pParams->fPatScores )
Ivy_FraigCleanPatScores( p );
nChanges = Ivy_FraigRefineClasses( p );
if ( p->pManFraig->pData )
return;
if ( nChanges < 1 )
printf( "Error: A counter-example did not refine classes!\n" );
assert( nChanges >= 1 );
//printf( "Refined classes! = %5d. Changes = %4d.\n", p->lClasses.nItems, nChanges );
if ( !p->pParams->fPatScores )
return;
// perform additional simulation using dist1 patterns derived from successful patterns
while ( Ivy_FraigSelectBestPat(p) > p->pParams->MaxScore )
{
Ivy_FraigAssignDist1( p, p->pPatWords );
Ivy_FraigSimulateOne( p );
Ivy_FraigCleanPatScores( p );
nChanges = Ivy_FraigRefineClasses( p );
if ( p->pManFraig->pData )
return;
//printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) );
if ( nChanges == 0 )
break;
}
}
/**Function*************************************************************
Synopsis [Prints the status of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int clk, int fVerbose )
{
if ( !fVerbose )
return;
printf( "Nodes = %7d. Levels = %4d. ", Ivy_ManNodeNum(pNtk), Ivy_ManLevels(pNtk) );
PRT( pString, clock() - clk );
}
/**Function*************************************************************
Synopsis [Reports the status of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigMiterStatus( Ivy_Man_t * pMan )
{
Ivy_Obj_t * pObj, * pObjNew;
int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
if ( pMan->pData )
return 0;
Ivy_ManForEachPo( pMan, pObj, i )
{
pObjNew = Ivy_ObjChild0(pObj);
// check if the output is constant 1
if ( pObjNew == pMan->pConst1 )
{
CountNonConst0++;
continue;
}
// check if the output is constant 0
if ( pObjNew == Ivy_Not(pMan->pConst1) )
{
CountConst0++;
continue;
}
// check if the output can be constant 0
if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
{
CountNonConst0++;
continue;
}
CountUndecided++;
}
/*
if ( p->pParams->fVerbose )
{
printf( "Miter has %d outputs. ", Ivy_ManPoNum(p->pManAig) );
printf( "Const0 = %d. ", CountConst0 );
printf( "NonConst0 = %d. ", CountNonConst0 );
printf( "Undecided = %d. ", CountUndecided );
printf( "\n" );
}
*/
if ( CountNonConst0 )
return 0;
if ( CountUndecided )
return -1;
return 1;
}
/**Function*************************************************************
Synopsis [Tries to prove each output of the miter until encountering a sat output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj, * pObjNew;
int i, RetValue, clk = clock();
int fVerbose = 0;
Ivy_ManForEachPo( p->pManAig, pObj, i )
{
if ( i && fVerbose )
{
PRT( "Time", clock() -clk );
}
pObjNew = Ivy_ObjChild0Equiv(pObj);
// check if the output is constant 1
if ( pObjNew == p->pManFraig->pConst1 )
{
if ( fVerbose )
printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) );
// assing constant 0 model
p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
break;
}
// check if the output is constant 0
if ( pObjNew == Ivy_Not(p->pManFraig->pConst1) )
{
if ( fVerbose )
printf( "Output %2d (out of %2d) is already constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
continue;
}
// check if the output can be constant 0
if ( Ivy_Regular(pObjNew)->fPhase != (unsigned)Ivy_IsComplement(pObjNew) )
{
if ( fVerbose )
printf( "Output %2d (out of %2d) cannot be constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
// assing constant 0 model
p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
break;
}
/*
// check the representative of this node
pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj));
if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 )
printf( "Representative is not constant 1.\n" );
else
printf( "Representative is constant 1.\n" );
*/
// try to prove the output constant 0
RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) );
if ( RetValue == 1 ) // proved equivalent
{
if ( fVerbose )
printf( "Output %2d (out of %2d) was proved constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
// set the constant miter
Ivy_ObjFanin0(pObj)->pEquiv = Ivy_NotCond( p->pManFraig->pConst1, !Ivy_ObjFaninC0(pObj) );
continue;
}
if ( RetValue == -1 ) // failed
{
if ( fVerbose )
printf( "Output %2d (out of %2d) has timed out at %d backtracks. ", i, Ivy_ManPoNum(p->pManAig), p->pParams->nBTLimitMiter );
continue;
}
// proved satisfiable
if ( fVerbose )
printf( "Output %2d (out of %2d) was proved NOT a constant 0. ", i, Ivy_ManPoNum(p->pManAig) );
// create the model
p->pManFraig->pData = Ivy_FraigCreateModel(p);
break;
}
if ( fVerbose )
{
PRT( "Time", clock() -clk );
}
}
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigSweep( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;//, * pTemp;
int i, k = 0;
p->nClassesZero = p->lClasses.pHead? (Ivy_ObjIsConst1(p->lClasses.pHead) ? Ivy_FraigCountClassNodes(p->lClasses.pHead) : 0) : 0;
p->nClassesBeg = p->lClasses.nItems;
// duplicate internal nodes
p->pProgress = Extra_ProgressBarStart( stdout, Ivy_ManNodeNum(p->pManAig) );
Ivy_ManForEachNode( p->pManAig, pObj, i )
{
Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
else
pObj->pEquiv = Ivy_FraigAnd( p, pObj );
assert( pObj->pEquiv != NULL );
// pTemp = Ivy_Regular(pObj->pEquiv);
// assert( Ivy_Regular(pObj->pEquiv)->Type );
}
Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = p->lClasses.nItems;
// try to prove the outputs of the miter
p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig);
// Ivy_FraigMiterStatus( p->pManFraig );
if ( p->pParams->fProve && p->pManFraig->pData == NULL )
Ivy_FraigMiterProve( p );
// add the POs
Ivy_ManForEachPo( p->pManAig, pObj, i )
Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
// clean the old manager
Ivy_ManForEachObj( p->pManAig, pObj, i )
pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
// clean the new manager
Ivy_ManForEachObj( p->pManFraig, pObj, i )
{
if ( Ivy_ObjFaninVec(pObj) )
Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
pObj->pNextFan0 = pObj->pNextFan1 = NULL;
}
// remove dangling nodes
Ivy_ManCleanup( p->pManFraig );
// clean up the class marks
Ivy_FraigForEachEquivClass( p->lClasses.pHead, pObj )
pObj->fMarkA = 0;
}
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
{
Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
int RetValue;
// get the fraiged fanins
pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
// get the candidate fraig node
pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
// get representative of this class
if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
(!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
{
assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
assert( pObjNew != Ivy_Regular(pFanin0New) );
assert( pObjNew != Ivy_Regular(pFanin1New) );
return pObjNew;
}
// get the fraiged representative
pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
// if the fraiged nodes are the same return
if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
return pObjNew;
assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
// they are different (the counter-example is in p->pPatWords)
RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
if ( RetValue == 1 ) // proved equivalent
{
// mark the class as proved
if ( Ivy_ObjClassNodeNext(pObjOld) == NULL )
Ivy_ObjClassNodeRepr(pObjOld)->fMarkA = 1;
return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
}
if ( RetValue == -1 ) // failed
return pObjNew;
// simulate the counter-example and return the new node
Ivy_FraigResimulate( p );
return pObjNew;
}
/**Function*************************************************************
Synopsis [Prints variable activity.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigPrintActivity( Ivy_FraigMan_t * p )
{
int i;
for ( i = 0; i < p->nSatVars; i++ )
printf( "%d %.3f ", i, p->pSat->activity[i] );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Runs equivalence test for the two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
assert( !Ivy_IsComplement(pOld) );
assert( pNew != pOld );
// if at least one of the nodes is a failed node, perform adjustments:
// if the backtrack limit is small, simply skip this node
// if the backtrack limit is > 10, take the quare root of the limit
nBTLimit = p->pParams->nBTLimitNode;
if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
{
p->nSatFails++;
// fail immediately
// return -1;
if ( nBTLimit <= 10 )
return -1;
nBTLimit = (int)pow(nBTLimit, 0.7);
}
p->nSatCalls++;
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
}
// if the nodes do not have SAT variables, allocate them
Ivy_FraigNodeAddToSolver( p, pOld, pNew );
// prepare variable activity
Ivy_FraigSetActivityFactors( p, pOld, pNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
clk = clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fFailTfo = 1;
pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
// if the old node was constant 0, we already know the answer
if ( pOld == p->pManFraig->pConst1 )
{
p->nSatProof++;
return 1;
}
// solve under assumptions
// A = 0; B = 1 OR A = 0; B = 0
clk = clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2,
(sint64)nBTLimit, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
pLits[1] = lit_neg( pLits[1] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
pOld->fFailTfo = 1;
pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
/*
// check BDD proof
{
int RetVal;
PRT( "Sat", clock() - clk2 );
clk2 = clock();
RetVal = Ivy_FraigNodesAreEquivBdd( pOld, pNew );
// printf( "%d ", RetVal );
assert( RetVal );
PRT( "Bdd", clock() - clk2 );
printf( "\n" );
}
*/
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Runs equivalence test for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
{
int pLits[2], RetValue1, RetValue, clk;
// make sure the nodes are not complemented
assert( !Ivy_IsComplement(pNew) );
assert( pNew != p->pManFraig->pConst1 );
p->nSatCalls++;
// make sure the solver is allocated and has enough variables
if ( p->pSat == NULL )
{
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
}
// if the nodes do not have SAT variables, allocate them
Ivy_FraigNodeAddToSolver( p, NULL, pNew );
// prepare variable activity
Ivy_FraigSetActivityFactors( p, NULL, pNew );
// solve under assumptions
clk = clock();
pLits[0] = toLitCond( Ivy_ObjSatNum(pNew), pNew->fPhase );
RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1,
(sint64)p->pParams->nBTLimitMiter, (sint64)0,
p->nBTLimitGlobal, p->nInsLimitGlobal );
p->timeSat += clock() - clk;
if ( RetValue1 == l_False )
{
p->timeSatUnsat += clock() - clk;
pLits[0] = lit_neg( pLits[0] );
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
assert( RetValue );
// continue solving the other implication
p->nSatCallsUnsat++;
}
else if ( RetValue1 == l_True )
{
p->timeSatSat += clock() - clk;
if ( p->pPatWords )
Ivy_FraigSavePattern( p );
p->nSatCallsSat++;
return 0;
}
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
// mark the node as the failed node
pNew->fFailTfo = 1;
p->nSatFailsReal++;
return -1;
}
// return SAT proof
p->nSatProof++;
return 1;
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAddClausesMux( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode )
{
Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
assert( !Ivy_IsComplement( pNode ) );
assert( Ivy_ObjIsMuxType( pNode ) );
// get nodes (I = if, T = then, E = else)
pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
// get the variable numbers
VarF = Ivy_ObjSatNum(pNode);
VarI = Ivy_ObjSatNum(pNodeI);
VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
// get the complementation flags
fCompT = Ivy_IsComplement(pNodeT);
fCompE = Ivy_IsComplement(pNodeE);
// f = ITE(i, t, e)
// i' + t' + f
// i' + t + f'
// i + e' + f
// i + e + f'
// create four clauses
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 1^fCompT);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 1);
pLits[1] = toLitCond(VarT, 0^fCompT);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarI, 0);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
// two additional clauses
// t' & e' -> f'
// t & e -> f
// t + e + f'
// t' + e' + f
if ( VarT == VarE )
{
// assert( fCompT == !fCompE );
return;
}
pLits[0] = toLitCond(VarT, 0^fCompT);
pLits[1] = toLitCond(VarE, 0^fCompE);
pLits[2] = toLitCond(VarF, 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
pLits[0] = toLitCond(VarT, 1^fCompT);
pLits[1] = toLitCond(VarE, 1^fCompE);
pLits[2] = toLitCond(VarF, 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
assert( RetValue );
}
/**Function*************************************************************
Synopsis [Addes clauses to the solver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigAddClausesSuper( Ivy_FraigMan_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
{
Ivy_Obj_t * pFanin;
int * pLits, nLits, RetValue, i;
assert( !Ivy_IsComplement(pNode) );
assert( Ivy_ObjIsNode( pNode ) );
// create storage for literals
nLits = Vec_PtrSize(vSuper) + 1;
pLits = ALLOC( int, nLits );
// suppose AND-gate is A & B = C
// add !A => !C or A + !C
Vec_PtrForEachEntry( vSuper, pFanin, i )
{
pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
assert( RetValue );
}
// add A & B => C or !A + !B + C
Vec_PtrForEachEntry( vSuper, pFanin, i )
pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
assert( RetValue );
free( pLits );
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
{
// if the new node is complemented or a PI, another gate begins
if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) ||
(fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
{
Vec_PtrPushUnique( vSuper, pObj );
return;
}
// go through the branches
Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
}
/**Function*************************************************************
Synopsis [Collects the supergate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
{
Vec_Ptr_t * vSuper;
assert( !Ivy_IsComplement(pObj) );
assert( !Ivy_ObjIsPi(pObj) );
vSuper = Vec_PtrAlloc( 4 );
Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
return vSuper;
}
/**Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigObjAddToFrontier( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
{
assert( !Ivy_IsComplement(pObj) );
if ( Ivy_ObjSatNum(pObj) )
return;
assert( Ivy_ObjSatNum(pObj) == 0 );
assert( Ivy_ObjFaninVec(pObj) == NULL );
if ( Ivy_ObjIsConst1(pObj) )
return;
//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
if ( Ivy_ObjIsNode(pObj) )
Vec_PtrPush( vFrontier, pObj );
}
/**Function*************************************************************
Synopsis [Updates the solver clause database.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
Vec_Ptr_t * vFrontier, * vFanins;
Ivy_Obj_t * pNode, * pFanin;
int i, k, fUseMuxes = 1;
assert( pOld || pNew );
// quit if CNF is ready
if ( (!pOld || Ivy_ObjFaninVec(pOld)) && (!pNew || Ivy_ObjFaninVec(pNew)) )
return;
// start the frontier
vFrontier = Vec_PtrAlloc( 100 );
if ( pOld ) Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
if ( pNew ) Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
// explore nodes in the frontier
Vec_PtrForEachEntry( vFrontier, pNode, i )
{
// create the supergate
assert( Ivy_ObjSatNum(pNode) );
assert( Ivy_ObjFaninVec(pNode) == NULL );
if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
{
vFanins = Vec_PtrAlloc( 4 );
Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
Vec_PtrForEachEntry( vFanins, pFanin, k )
Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
Ivy_FraigAddClausesMux( p, pNode );
}
else
{
vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
Vec_PtrForEachEntry( vFanins, pFanin, k )
Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
Ivy_FraigAddClausesSuper( p, pNode, vFanins );
}
assert( Vec_PtrSize(vFanins) > 1 );
Ivy_ObjSetFaninVec( pNode, vFanins );
}
Vec_PtrFree( vFrontier );
}
/**Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigSetActivityFactors_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj, int LevelMin, int LevelMax )
{
Vec_Ptr_t * vFanins;
Ivy_Obj_t * pFanin;
int i, Counter = 0;
assert( !Ivy_IsComplement(pObj) );
assert( Ivy_ObjSatNum(pObj) );
// skip visited variables
if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
return 0;
Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
// add the PI to the list
if ( pObj->Level <= (unsigned)LevelMin || Ivy_ObjIsPi(pObj) )
return 0;
// set the factor of this variable
// (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pParams->dActConeBumpMax / ThisBump
p->pSat->factors[Ivy_ObjSatNum(pObj)] = p->pParams->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
veci_push(&p->pSat->act_vars, Ivy_ObjSatNum(pObj));
// explore the fanins
vFanins = Ivy_ObjFaninVec( pObj );
Vec_PtrForEachEntry( vFanins, pFanin, i )
Counter += Ivy_FraigSetActivityFactors_rec( p, Ivy_Regular(pFanin), LevelMin, LevelMax );
return 1 + Counter;
}
/**Function*************************************************************
Synopsis [Sets variable activities in the cone.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigSetActivityFactors( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
{
int clk, LevelMin, LevelMax;
assert( pOld || pNew );
clk = clock();
// reset the active variables
veci_resize(&p->pSat->act_vars, 0);
// prepare for traversal
Ivy_ManIncrementTravId( p->pManFraig );
// determine the min and max level to visit
assert( p->pParams->dActConeRatio > 0 && p->pParams->dActConeRatio < 1 );
LevelMax = IVY_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
LevelMin = (int)(LevelMax * (1.0 - p->pParams->dActConeRatio));
// traverse
if ( pOld && !Ivy_ObjIsConst1(pOld) )
Ivy_FraigSetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
if ( pNew && !Ivy_ObjIsConst1(pNew) )
Ivy_FraigSetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
//Ivy_FraigPrintActivity( p );
p->timeTrav += clock() - clk;
return 1;
}
#include "cuddInt.h"
/**Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
DdNode * Ivy_FraigNodesAreEquivBdd_int( DdManager * dd, DdNode * bFunc, Vec_Ptr_t * vFront, int Level )
{
DdNode ** pFuncs;
DdNode * bFuncNew;
Vec_Ptr_t * vTemp;
Ivy_Obj_t * pObj, * pFanin;
int i, NewSize;
// create new frontier
vTemp = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( vFront, pObj, i )
{
if ( (int)pObj->Level != Level )
{
pObj->fMarkB = 1;
pObj->TravId = Vec_PtrSize(vTemp);
Vec_PtrPush( vTemp, pObj );
continue;
}
pFanin = Ivy_ObjFanin0(pObj);
if ( pFanin->fMarkB == 0 )
{
pFanin->fMarkB = 1;
pFanin->TravId = Vec_PtrSize(vTemp);
Vec_PtrPush( vTemp, pFanin );
}
pFanin = Ivy_ObjFanin1(pObj);
if ( pFanin->fMarkB == 0 )
{
pFanin->fMarkB = 1;
pFanin->TravId = Vec_PtrSize(vTemp);
Vec_PtrPush( vTemp, pFanin );
}
}
// collect the permutation
NewSize = IVY_MAX(dd->size, Vec_PtrSize(vTemp));
pFuncs = ALLOC( DdNode *, NewSize );
Vec_PtrForEachEntry( vFront, pObj, i )
{
if ( (int)pObj->Level != Level )
pFuncs[i] = Cudd_bddIthVar( dd, pObj->TravId );
else
pFuncs[i] = Cudd_bddAnd( dd,
Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ),
Cudd_NotCond( Cudd_bddIthVar(dd, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ) );
Cudd_Ref( pFuncs[i] );
}
// add the remaining vars
assert( NewSize == dd->size );
for ( i = Vec_PtrSize(vFront); i < dd->size; i++ )
{
pFuncs[i] = Cudd_bddIthVar( dd, i );
Cudd_Ref( pFuncs[i] );
}
// create new
bFuncNew = Cudd_bddVectorCompose( dd, bFunc, pFuncs ); Cudd_Ref( bFuncNew );
// clean trav Id
Vec_PtrForEachEntry( vTemp, pObj, i )
{
pObj->fMarkB = 0;
pObj->TravId = 0;
}
// deref
for ( i = 0; i < dd->size; i++ )
Cudd_RecursiveDeref( dd, pFuncs[i] );
free( pFuncs );
free( vFront->pArray );
*vFront = *vTemp;
vTemp->nCap = vTemp->nSize = 0;
vTemp->pArray = NULL;
Vec_PtrFree( vTemp );
Cudd_Deref( bFuncNew );
return bFuncNew;
}
/**Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
{
static DdManager * dd = NULL;
DdNode * bFunc, * bTemp;
Vec_Ptr_t * vFront;
Ivy_Obj_t * pObj;
int i, RetValue, Iter, Level;
// start the manager
if ( dd == NULL )
dd = Cudd_Init( 50, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
// create front
vFront = Vec_PtrAlloc( 100 );
Vec_PtrPush( vFront, pObj1 );
Vec_PtrPush( vFront, pObj2 );
// get the function
bFunc = Cudd_bddXor( dd, Cudd_bddIthVar(dd,0), Cudd_bddIthVar(dd,1) ); Cudd_Ref( bFunc );
bFunc = Cudd_NotCond( bFunc, pObj1->fPhase != pObj2->fPhase );
// try running BDDs
for ( Iter = 0; ; Iter++ )
{
// find max level
Level = 0;
Vec_PtrForEachEntry( vFront, pObj, i )
if ( Level < (int)pObj->Level )
Level = (int)pObj->Level;
if ( Level == 0 )
break;
bFunc = Ivy_FraigNodesAreEquivBdd_int( dd, bTemp = bFunc, vFront, Level ); Cudd_Ref( bFunc );
Cudd_RecursiveDeref( dd, bTemp );
if ( bFunc == Cudd_ReadLogicZero(dd) ) // proved
{printf( "%d", Iter ); break;}
if ( Cudd_DagSize(bFunc) > 1000 )
{printf( "b" ); break;}
if ( dd->size > 120 )
{printf( "s" ); break;}
if ( Iter > 50 )
{printf( "i" ); break;}
}
if ( bFunc == Cudd_ReadLogicZero(dd) ) // unsat
RetValue = 1;
else if ( Level == 0 ) // sat
RetValue = 0;
else
RetValue = -1; // spaceout/timeout
Cudd_RecursiveDeref( dd, bFunc );
Vec_PtrFree( vFront );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/aig/fra/module.make
SRC += src/aig/fra/fraClass.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
src/aig/fra/fraDfs.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
src/aig/fra/fraSim.c
src/base/abci/abc.c
......@@ -326,7 +326,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
......@@ -10736,8 +10736,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int fExdc;
int fImp;
int fVerbose;
extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
extern Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -10801,14 +10800,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the new network
// if ( fImp )
// pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose );
// else
// pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
pNtkRes = NULL;
pNtkRes = Abc_NtkSeqSweep( pNtk, nFrames, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
fprintf( pErr, "Sequential sweeping has failed.\n" );
return 1;
}
// replace the current network
......@@ -10819,8 +10814,8 @@ usage:
fprintf( pErr, "usage: ssweep [-F num] [-eivh]\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-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-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-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/abcDar.c
......@@ -129,7 +129,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Ntk_t * pNtkNew;
Aig_Obj_t * pObj, * pTemp;
int i;
assert( pMan->pReprs != NULL );
assert( pMan->pEquivs != NULL );
assert( Aig_ManBufNum(pMan) == 0 );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
......@@ -142,7 +142,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Vec_PtrForEachEntry( vNodes, pObj, i )
{
pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
if ( pTemp = pMan->pReprs[pObj->Id] )
if ( pTemp = pMan->pEquivs[pObj->Id] )
{
Abc_Obj_t * pAbcRepr, * pAbcObj;
assert( pTemp->pData != NULL );
......@@ -261,14 +261,15 @@ Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
SeeAlso []
***********************************************************************/
int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
Vec_Int_t * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vInits;
Abc_Obj_t * pLatch;
int i, * pArray;
pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
int i;
vInits = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachLatch( pNtk, pLatch, i )
pArray[i] = Abc_LatchIsInit1(pLatch);
return pArray;
Vec_IntPush( vInits, Abc_LatchIsInit1(pLatch) );
return vInits;
}
/**Function*************************************************************
......@@ -298,11 +299,13 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
Aig_ManPrintStats( pMan1 );
Aig_ManPrintStats( pMan2 );
pArray = Abc_NtkGetLatchValues(pNtk1);
// pArray = Abc_NtkGetLatchValues(pNtk1);
pArray = NULL;
Aig_ManSeqStrash( pMan1, Abc_NtkLatchNum(pNtk1), pArray );
free( pArray );
pArray = Abc_NtkGetLatchValues(pNtk2);
// pArray = Abc_NtkGetLatchValues(pNtk2);
pArray = NULL;
Aig_ManSeqStrash( pMan2, Abc_NtkLatchNum(pNtk2), pArray );
free( pArray );
......@@ -414,7 +417,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
pPars->fDoSparse = fDoSparse;
pPars->fSpeculate = fSpeculate;
pPars->fChoicing = fChoicing;
pMan = Fra_Perform( pTemp = pMan, pPars );
pMan = Fra_FraigPerform( pTemp = pMan, pPars );
if ( fChoicing )
pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
else
......@@ -471,14 +474,14 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
if ( pMan == NULL )
return NULL;
// Aig_ManPrintStats( pMan );
/*
// Aig_ManSupports( pMan );
{
Vec_Vec_t * vParts;
vParts = Aig_ManPartitionSmart( pMan, 50, 1, NULL );
Vec_VecFree( vParts );
}
*/
Dar_ManRewrite( pMan, pPars );
// pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
// Aig_ManStop( pTemp );
......@@ -703,7 +706,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
Aig_ManPrintStats( pMan );
// derive CNF
pCnf = Cnf_Derive( pMan );
pCnf = Cnf_Derive( pMan, 0 );
pManCnf = Cnf_ManRead();
// write the network for verification
......@@ -747,7 +750,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
// conver to the manager
pMan = Abc_NtkToDar( pNtk );
// derive CNF
pCnf = Cnf_Derive( pMan );
pCnf = Cnf_Derive( pMan, 0 );
// convert into the SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
......@@ -763,7 +766,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
PRT( "Time", clock() - clk );
// PRT( "Time", clock() - clk );
// simplify the problem
clk = clock();
......@@ -818,6 +821,35 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
return RetValue;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk );
if ( pMan == NULL )
return NULL;
pMan->vInits = Abc_NtkGetLatchValues( pNtk );
pMan = Fra_Induction( pTemp = pMan, nFrames, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDar( pNtk, pMan );
Aig_ManStop( pMan );
return pNtkAig;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcRewrite.c
......@@ -69,13 +69,13 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerb
assert( Abc_NtkIsStrash(pNtk) );
// cleanup the AIG
Abc_AigCleanup(pNtk->pManFunc);
/*
{
Vec_Vec_t * vParts;
vParts = Abc_NtkPartitionSmart( pNtk, 50, 1 );
Vec_VecFree( vParts );
}
*/
// start placement package
if ( fPlaceEnable )
......
src/base/abci/abcSat.c
......@@ -70,7 +70,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
//return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
PRT( "Time", clock() - clk );
// PRT( "Time", clock() - clk );
// simplify the problem
clk = clock();
......
src/base/main/main.c
......@@ -237,7 +237,13 @@ usage:
Synopsis [Initialization procedure for the library project.]
Description []
Description [Note that when Abc_Start() is run in a static library
project, it does not load the resource file by default. As a result,
ABC is not set up the same way, as when it is run on a command line.
For example, some error messages while parsing files will not be
produced, and intermediate networks will not be checked for consistancy.
One possibility is to load the resource file after Abc_Start() as follows:
Abc_UtilsSource( Abc_FrameGetGlobalFrame() );]
SideEffects []
......
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