summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-07-27 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-07-27 08:01:00 -0700
commita8a80d9a1a84c2c5f605f6630dc804f3631e7a9f (patch)
treee48831dc8c36a01683f1d73324e8c48af1db5b5c
parent054e2cd3a8ab4ada55db4def2d6ce7d309341e07 (diff)
downloadabc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.tar.gz
abc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.tar.bz2
abc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.zip
Version abc70727
Diffstat
-rw-r--r--abc.dsp2
-rw-r--r--src/aig/aig/aig.h34
-rw-r--r--src/aig/aig/aigDfs.c4
-rw-r--r--src/aig/aig/aigMan.c6
-rw-r--r--src/aig/aig/aigPart.c6
-rw-r--r--src/aig/aig/aigRepr.c125
-rw-r--r--src/aig/cnf/cnf.h4
-rw-r--r--src/aig/cnf/cnfCore.c4
-rw-r--r--src/aig/cnf/cnfWrite.c48
-rw-r--r--src/aig/fra/fra.h97
-rw-r--r--src/aig/fra/fraClass.c225
-rw-r--r--src/aig/fra/fraCore.c132
-rw-r--r--src/aig/fra/fraDfs.c87
-rw-r--r--src/aig/fra/fraInd.c205
-rw-r--r--src/aig/fra/fraMan.c134
-rw-r--r--src/aig/fra/fraSat.c8
-rw-r--r--src/aig/fra/fraSim.c154
-rw-r--r--src/aig/fra/ivyFraig.c2750
-rw-r--r--src/aig/fra/module.make2
-rw-r--r--src/base/abci/abc.c17
-rw-r--r--src/base/abci/abcDar.c62
-rw-r--r--src/base/abci/abcRewrite.c4
-rw-r--r--src/base/abci/abcSat.c2
-rw-r--r--src/base/main/main.c8
24 files changed, 876 insertions, 3244 deletions
diff --git a/abc.dsp b/abc.dsp
index c175b513..b7ad7e13 100644
--- a/abc.dsp
+++ b/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
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 230c354f..1785c44b 100644
--- a/src/aig/aig/aig.h
+++ b/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,8 +173,9 @@ 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 Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; }
static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; }
static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsPi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI; }
@@ -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 ========================================================*/
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index a9d3d860..5a18c4ac 100644
--- a/src/aig/aig/aigDfs.c
+++ b/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) );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index b235119f..27622944 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -52,8 +52,8 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
p->nTravIds = 1;
p->fCatchExor = 0;
// allocate arrays for nodes
- p->vPis = Vec_PtrAlloc( 100 );
- p->vPos = Vec_PtrAlloc( 100 );
+ p->vPis = Vec_PtrAlloc( 100 );
+ p->vPos = Vec_PtrAlloc( 100 );
p->vObjs = Vec_PtrAlloc( 1000 );
p->vBufs = Vec_PtrAlloc( 100 );
// prepare the internal memory manager
@@ -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 );
}
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 371e8773..f616bc25 100644
--- a/src/aig/aig/aigPart.c
+++ b/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;
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index fa6bf60e..8dd980ab 100644
--- a/src/aig/aig/aigRepr.c
+++ b/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;
}
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index 2f121752..941ec816 100644
--- a/src/aig/cnf/cnf.h
+++ b/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
}
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 7480d45d..88a55c22 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/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;
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 41a00732..fa5be801 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/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,9 +291,25 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
// write the output literals
Aig_ManForEachPo( p->pManAig, pObj, i )
{
- OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
- *pClas++ = pLits;
- *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
+ 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
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 127882ea..13e79a0e 100644
--- a/src/aig/fra/fra.h
+++ b/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;
@@ -140,23 +152,23 @@ struct Fra_Man_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
+static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; }
static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
-static inline 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 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 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 void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; }
-static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; }
+static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; }
+static inline 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 ) { 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_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 );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 3de54453..170fcd27 100644
--- a/src/aig/fra/fraClass.c
+++ b/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;
}
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index ca2d0fb4..977396dd 100644
--- a/src/aig/fra/fraCore.c
+++ b/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 );
- pManAigNew = p->pManFraig;
+ 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 );
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraDfs.c b/src/aig/fra/fraDfs.c
deleted file mode 100644
index cd0985e0..00000000
--- a/src/aig/fra/fraDfs.c
+++ /dev/null
@@ -1,87 +0,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 ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
new file mode 100644
index 00000000..1bfe1cb4
--- /dev/null
+++ b/src/aig/fra/fraInd.c
@@ -0,0 +1,205 @@
+/**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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 0e583d6c..e109df56 100644
--- a/src/aig/fra/fraMan.c
+++ b/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->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->vTimeouts ) Vec_PtrFree( p->vTimeouts );
+ if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
+ if ( p->pSat ) sat_solver_delete( p->pSat );
+ 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 );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 8ab10c40..418e9fee 100644
--- a/src/aig/fra/fraSat.c
+++ b/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,7 +78,8 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
Fra_NodeAddToSolver( p, pOld, pNew );
// prepare variable activity
- Fra_SetActivityFactors( p, pOld, pNew );
+ if ( p->pPars->fConeBias )
+ Fra_SetActivityFactors( p, pOld, pNew );
// solve under assumptions
// A = 1; B = 0 OR A = 1; B = 1
@@ -209,7 +210,8 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
Fra_NodeAddToSolver( p, NULL, pNew );
// prepare variable activity
- Fra_SetActivityFactors( p, NULL, pNew );
+ if ( p->pPars->fConeBias )
+ Fra_SetActivityFactors( p, NULL, pNew );
// solve under assumptions
clk = clock();
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index beaa79fd..a01bc2e0 100644
--- a/src/aig/fra/fraSim.c
+++ b/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;
- Aig_ManForEachPi( p->pManAig, pObj, i )
- Fra_NodeAssignRandom( p, pObj );
+ 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;
}
diff --git a/src/aig/fra/ivyFraig.c b/src/aig/fra/ivyFraig.c
deleted file mode 100644
index e9a65881..00000000
--- a/src/aig/fra/ivyFraig.c
+++ /dev/null
@@ -1,2750 +0,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 ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index df690700..191427c9 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,7 +1,7 @@
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
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1dd9b65e..1df13db8 100644
--- a/src/base/abci/abc.c
+++ b/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;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index f04f3d97..64043717 100644
--- a/src/base/abci/abcDar.c
+++ b/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 ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 2376b72c..89b79e5a 100644
--- a/src/base/abci/abcRewrite.c
+++ b/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 )
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index aafa6530..58614584 100644
--- a/src/base/abci/abcSat.c
+++ b/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();
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 1c6cbcb0..8f43c605 100644
--- a/src/base/main/main.c
+++ b/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 []
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 10:56:42 +0000