summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h8
-rw-r--r--src/aig/fra/fraBmc.c7
-rw-r--r--src/aig/fra/fraClass.c19
-rw-r--r--src/aig/fra/fraCore.c44
-rw-r--r--src/aig/fra/fraImp.c6
-rw-r--r--src/aig/fra/fraInd.c18
-rw-r--r--src/aig/fra/fraLcr.c4
-rw-r--r--src/aig/fra/fraMan.c112
-rw-r--r--src/aig/fra/fraPart.c8
-rw-r--r--src/aig/fra/fraSat.c1
-rw-r--r--src/aig/fra/fraSec.c30
-rw-r--r--src/aig/fra/fraSim.c2
12 files changed, 143 insertions, 116 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 931e0930..cd6bdfd4 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -39,6 +39,7 @@ extern "C" {
#include "aig.h"
#include "dar.h"
#include "satSolver.h"
+#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -126,6 +127,7 @@ struct Fra_Man_t_
// mapping AIG into FRAIG
int nFramesAll; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
+ int nSizeAlloc; // allocated size of the arrays for timeframe nodes
// equivalence classes
Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes
// simulation info
@@ -144,7 +146,7 @@ struct Fra_Man_t_
sint64 nInsLimitGlobal; // resource limit
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
+ int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins
Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out
// statistics
int nSimRounds;
@@ -240,7 +242,7 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
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 Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
@@ -259,7 +261,7 @@ extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int n
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_ManClean( Fra_Man_t * p );
+extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax );
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 );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 648d08c4..1df25c0a 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -187,8 +187,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
p->nPref = nPref;
p->nDepth = nDepth;
p->nFramesAll = nPref + nDepth;
- p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
- memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+ p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
+ memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
return p;
}
@@ -231,7 +231,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
int i, k, f;
// start the fraig package
- pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll );
+ pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
+ pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 3e3392c7..a03fa6e5 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -60,8 +60,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
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->pMemRepr = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+ memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
p->vClasses = Vec_PtrAlloc( 100 );
p->vClasses1 = Vec_PtrAlloc( 100 );
p->vClassesTemp = Vec_PtrAlloc( 100 );
@@ -112,8 +112,8 @@ 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) );
+ Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
+ memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
{
Aig_ManForEachObj( p->pAig, pObj, i )
@@ -277,7 +277,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
int i, k, nTableSize, nEntries, nNodes, iEntry;
// allocate the hash table hashing simulation info into nodes
- nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 );
+ nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
ppTable = ALLOC( Aig_Obj_t *, nTableSize );
ppNexts = ALLOC( Aig_Obj_t *, nTableSize );
memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
@@ -643,8 +643,8 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
// perform combinational simulation
pComb = Fra_SmlSimulateComb( p->pAig, 32 );
// compute the weight of each node in the classes
- pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
- memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+ pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
{
pRepr = Fra_ClassObjRepr( pObj );
@@ -798,9 +798,10 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
assert( nFramesK > 0 );
// start the fraig package
- pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+ pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
+ pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
// allocate place for the node mapping
- ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+ ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
// create latches for the first frame
Aig_ManForEachLoSeq( p->pAig, pObj, i )
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 94beb61a..b390edbe 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -267,7 +267,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
***********************************************************************/
void Fra_FraigSweep( Fra_Man_t * p )
{
- ProgressBar * pProgress;
+ Bar_Progress_t * pProgress;
Aig_Obj_t * pObj, * pObjNew;
int i, k = 0, Pos = 0;
// fraig latch outputs
@@ -280,10 +280,10 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pPars->fLatchCorr )
return;
// fraig internal nodes
- pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+ pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
Aig_ManForEachNode( p->pManAig, pObj, i )
{
- Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Bar_ProgressUpdate( pProgress, i, NULL );
// derive and remember the new fraig node
pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
@@ -296,7 +296,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
if ( p->pPars->fUseImps )
Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
}
- Extra_ProgressBarStop( pProgress );
+ Bar_ProgressStop( pProgress );
// try to prove the outputs of the miter
p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
@@ -331,8 +331,8 @@ clk = clock();
p->pManFraig = Fra_ManPrepareComb( p );
p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
Fra_SmlSimulate( p, 0 );
- if ( p->pPars->fChoicing )
- Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
+// if ( p->pPars->fChoicing )
+// Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
// collect initial states
p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
@@ -346,10 +346,12 @@ clk = clock();
Fra_ManFinalizeComb( p );
if ( p->pPars->fChoicing )
{
- int clk2 = clock();
+int clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
- pManAigNew = Aig_ManDupRepr( p->pManAig );
- Aig_ManCreateChoices( pManAigNew );
+ pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
+ Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
+ Aig_ManTransferRepr( pManAigNew, p->pManAig );
+ Aig_ManMarkValidChoices( pManAigNew );
Aig_ManStop( p->pManFraig );
p->pManFraig = NULL;
p->timeTrav += clock() - clk2;
@@ -359,14 +361,6 @@ p->timeTrav += clock() - clk2;
Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
-/*
- Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
- pManAigNew = Aig_ManDupRepr( p->pManAig );
-// Aig_ManCreateChoices( pManAigNew );
- Aig_ManCleanup( pManAigNew );
- Aig_ManStop( p->pManFraig );
- p->pManFraig = NULL;
-*/
}
p->timeTotal = clock() - clk;
// collect final stats
@@ -388,16 +382,16 @@ p->timeTotal = clock() - clk;
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
{
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
- pPars->nBTLimitNode = 1000;
- pPars->fVerbose = 0;
- pPars->fProve = 0;
+ pPars->nBTLimitNode = nConfMax;
+ pPars->fChoicing = 1;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
- pPars->fChoicing = 1;
+ pPars->fProve = 0;
+ pPars->fVerbose = 0;
return Fra_FraigPerform( pManAig, pPars );
}
@@ -418,11 +412,11 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
Fra_Par_t Pars, * pPars = &Pars;
Fra_ParamsDefault( pPars );
pPars->nBTLimitNode = nConfMax;
- pPars->fVerbose = 0;
- pPars->fProve = 0;
+ pPars->fChoicing = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
- pPars->fChoicing = 0;
+ pPars->fProve = 0;
+ pPars->fVerbose = 0;
pFraig = Fra_FraigPerform( pManAig, pPars );
return pFraig;
}
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 5e4b8c28..d8bf4e48 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -64,8 +64,8 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
{
Aig_Obj_t * pObj;
int i, * pnBits;
- pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
- memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+ pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+ memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
Aig_ManForEachObj( p->pAig, pObj, i )
pnBits[i] = Fra_SmlCountOnesOne( p, i );
return pnBits;
@@ -325,7 +325,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
int CostMin = AIG_INFINITY, CostMax = 0;
int i, k, Imp, CostRange, clk = clock();
- assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
+ assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
// normalize both managers
pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 53dbdbb6..14fba9ba 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -133,7 +133,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
// start the fraig package
- pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
+ pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
+ pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
pManFraig->nRegs = p->pManAig->nRegs;
// create PI nodes for the frames
for ( f = 0; f < p->nFramesAll; f++ )
@@ -194,7 +195,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
Aig_ManForEachObj( p, pObj, i )
pObj->pData = pObj;
// iterate and add objects
- nNodesOld = Aig_ManObjIdMax(p);
+ nNodesOld = Aig_ManObjNumMax(p);
pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
for ( f = 0; f < nFrames; f++ )
{
@@ -372,11 +373,14 @@ PRT( "Time", clock() - clk );
if ( p->pSat == NULL )
printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
}
-
+
// set the pointers to the manager
Aig_ManForEachObj( p->pManFraig, pObj, i )
pObj->pData = p;
+ // prepare solver for fraiging the last timeframe
+ Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
+
// transfer PI/LO variable numbers
Aig_ManForEachObj( p->pManFraig, pObj, i )
{
@@ -402,12 +406,14 @@ PRT( "Time", clock() - clk );
p->nSatCallsRecent = 0;
p->nSatCallsSkipped = 0;
Fra_FraigSweep( p );
+ // remove FRAIG and SAT solver
+ Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
+ sat_solver_delete( p->pSat ); p->pSat = NULL;
+ memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
// printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
assert( p->vTimeouts == NULL );
if ( p->vTimeouts )
printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
- // cleanup
- Fra_ManClean( p );
// check if refinement has happened
// p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
if ( p->pCla->fRefinement &&
@@ -435,7 +441,7 @@ clk2 = clock();
// Fra_ClassesPrint( p->pCla, 1 );
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
- pManAigNew = Aig_ManDupRepr( pManAig );
+ pManAigNew = Aig_ManDupRepr( pManAig, 0 );
// add implications to the manager
if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
Fra_ImpRecordInManager( p, pManAigNew );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index c3b5504e..e73d610f 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -509,7 +509,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Vec_Int_t * vPart;
- Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
+// Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
int i, nIter, clk = clock(), clk2, clk3;
if ( Aig_ManNodeNum(pAig) == 0 )
{
@@ -622,7 +622,7 @@ clk2 = clock();
if ( fReprSelect )
Fra_ClassesSelectRepr( p->pCla );
Fra_ClassesCopyReprs( p->pCla, NULL );
- pAigNew = Aig_ManDupRepr( p->pAig );
+ pAigNew = Aig_ManDupRepr( p->pAig, 0 );
Aig_ManSeqCleanup( pAigNew );
// Aig_ManCountMergeRegs( pAigNew );
p->timeUpdate += clock() - clk2;
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 97282e98..f505b0c2 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -42,20 +42,20 @@
void Fra_ParamsDefault( 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 = 100; // conflict limit at a node
- pPars->nBTLimitMiter = 500000; // conflict limit at an output
- pPars->nFramesK = 0; // the number of timeframes to unroll
- pPars->fConeBias = 1;
- pPars->fRewrite = 0;
+ 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 = 100; // conflict limit at a node
+ pPars->nBTLimitMiter = 500000; // conflict limit at an output
+ pPars->nFramesK = 0; // the number of timeframes to unroll
+ pPars->fConeBias = 1;
+ pPars->fRewrite = 0;
}
/**Function*************************************************************
@@ -72,20 +72,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
{
memset( pPars, 0, sizeof(Fra_Par_t) );
- pPars->nSimWords = 1; // 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.3; // the ratio of cone to be bumped
- pPars->dActConeBumpMax = 10.0; // the largest bump of activity
- pPars->nBTLimitNode =10000000; // conflict limit at a node
- pPars->nBTLimitMiter = 500000; // conflict limit at an output
- pPars->nFramesK = 1; // the number of timeframes to unroll
- pPars->fConeBias = 0;
- pPars->fRewrite = 0;
- pPars->fLatchCorr = 0;
-}
+ pPars->nSimWords = 1; // 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.3; // the ratio of cone to be bumped
+ pPars->dActConeBumpMax = 10.0; // the largest bump of activity
+ pPars->nBTLimitNode = 10000000; // conflict limit at a node
+ pPars->nBTLimitMiter = 500000; // conflict limit at an output
+ pPars->nFramesK = 1; // the number of timeframes to unroll
+ pPars->fConeBias = 0;
+ pPars->fRewrite = 0;
+ pPars->fLatchCorr = 0;
+}
/**Function*************************************************************
@@ -108,7 +108,7 @@ 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->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
+ p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
p->nFramesAll = pPars->nFramesK + 1;
// allocate storage for sim pattern
p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
@@ -119,10 +119,6 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
// allocate other members
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
- p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 );
- memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 );
- p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 );
- memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 );
// set random number generator
srand( 0xABCABC );
// set the pointer to the manager
@@ -142,24 +138,24 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
SeeAlso []
***********************************************************************/
-void Fra_ManClean( Fra_Man_t * p )
+void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
{
- int i, Limit;
-
- Limit = Aig_ManObjIdMax(p->pManFraig) + 1;
- for ( i = 0; i < Limit; i++ )
+ int i;
+ // remove old arrays
+ for ( i = 0; i < p->nMemAlloc; i++ )
if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
Vec_PtrFree( p->pMemFanins[i] );
-
- memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
- memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit );
- memset( p->pMemSatNums, 0, sizeof(int) * Limit );
-
- Aig_ManStop( p->pManFraig );
- p->pManFraig = NULL;
-
- sat_solver_delete( p->pSat );
- p->pSat = NULL;
+ // realloc for the new size
+ if ( p->nMemAlloc < nNodesMax )
+ {
+ int nMemAllocNew = nNodesMax + 5000;
+ p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
+ p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
+ p->nMemAlloc = nMemAllocNew;
+ }
+ // prepare for the new run
+ memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
+ memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
}
/**Function*************************************************************
@@ -180,7 +176,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
int i;
assert( p->pManFraig == NULL );
// start the fraig package
- pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
+ pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
+ pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
pManFraig->nRegs = p->pManAig->nRegs;
pManFraig->nAsserts = p->pManAig->nAsserts;
// set the pointers to the available fraig nodes
@@ -190,6 +187,12 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
// set the pointers to the manager
Aig_ManForEachObj( pManFraig, pObj, i )
pObj->pData = p;
+ // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
+ p->nMemAlloc = p->nSizeAlloc;
+ p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
+ memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
+ p->pMemSatNums = ALLOC( int, p->nMemAlloc );
+ memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
// make sure the satisfying assignment is node assigned
assert( pManFraig->pData == NULL );
return pManFraig;
@@ -231,7 +234,6 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
***********************************************************************/
void Fra_ManStop( Fra_Man_t * p )
{
- int i;
if ( p->pPars->fVerbose )
Fra_ManPrint( p );
// save mapping from original nodes into FRAIG nodes
@@ -242,9 +244,7 @@ void Fra_ManStop( Fra_Man_t * p )
p->pManAig->pObjCopies = p->pMemFraig;
p->pMemFraig = NULL;
}
- for ( i = 0; i < p->nSizeAlloc; i++ )
- if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
- Vec_PtrFree( p->pMemFanins[i] );
+ Fra_ManClean( p, 0 );
if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
if ( p->pSat ) sat_solver_delete( p->pSat );
@@ -271,14 +271,14 @@ void Fra_ManStop( Fra_Man_t * p )
***********************************************************************/
void Fra_ManPrint( Fra_Man_t * p )
{
- double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+ double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n",
p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
- p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg,
- p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
+ p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
+ p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
PRT( "AIG simulation ", p->pSml->timeSim );
PRT( "AIG traversal ", p->timeTrav );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index 23b6dd1d..691b2b3d 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -41,7 +41,7 @@
***********************************************************************/
void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
{
- ProgressBar * pProgress;
+ Bar_Progress_t * pProgress;
Vec_Vec_t * vSupps, * vSuppsIn;
Vec_Ptr_t * vSuppsNew;
Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
@@ -86,10 +86,10 @@ clk = clock();
vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) );
vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
- pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
+ pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
{
- Extra_ProgressBarUpdate( pProgress, i, NULL );
+ Bar_ProgressUpdate( pProgress, i, NULL );
// get old supports
vSup = Vec_VecEntry( vSupps, i );
if ( Vec_IntSize(vSup) < 2 )
@@ -152,7 +152,7 @@ clk = clock();
printf( "\n" );
*/
}
- Extra_ProgressBarStop( pProgress );
+ Bar_ProgressStop( pProgress );
PRT( "Scanning", clock() - clk );
// print cumulative statistics
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index bc8ef08a..e1cc4c32 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -18,6 +18,7 @@
***********************************************************************/
+#include <math.h>
#include "fra.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 88c552dc..0146ac5a 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "fra.h"
+#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -100,7 +101,7 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
@@ -116,7 +117,9 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose,
// perform sequential cleanup
clk = clock();
+ if ( pNew->nRegs )
pNew = Aig_ManReduceLaches( pNew, 0 );
+ if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
if ( fVerbose )
{
@@ -126,7 +129,7 @@ PRT( "Time", clock() - clk );
}
// perform forward retiming
- if ( fRetimeFirst )
+ if ( fRetimeFirst && pNew->nRegs )
{
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -141,6 +144,8 @@ PRT( "Time", clock() - clk );
// run latch correspondence
clk = clock();
+ if ( pNew->nRegs )
+ {
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
@@ -151,6 +156,7 @@ clk = clock();
nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
+ }
// perform fraiging
clk = clock();
@@ -166,7 +172,7 @@ PRT( "Time", clock() - clk );
// perform seq sweeping while increasing the number of frames
RetValue = Fra_FraigMiterStatus( pNew );
if ( RetValue == -1 )
- for ( nFrames = 1; ; nFrames *= 2 )
+ for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
{
clk = clock();
pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
@@ -203,19 +209,35 @@ clk = clock();
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
+ if ( pNew->nRegs )
+ pNew = Aig_ManConstReduce( pNew, 0 );
}
+
// get the miter status
RetValue = Fra_FraigMiterStatus( pNew );
- Aig_ManStop( pNew );
// report the miter
if ( RetValue == 1 )
+ {
printf( "Networks are equivalent. " );
+PRT( "Time", clock() - clkTotal );
+ }
else if ( RetValue == 0 )
+ {
printf( "Networks are NOT EQUIVALENT. " );
+PRT( "Time", clock() - clkTotal );
+ }
else
+ {
+ static int Counter = 1;
+ char pFileName[1000];
printf( "Networks are UNDECIDED. " );
PRT( "Time", clock() - clkTotal );
+ sprintf( pFileName, "sm%03d.aig", Counter++ );
+ Ioa_WriteAiger( pNew, pFileName, 0 );
+ printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+ }
+ Aig_ManStop( pNew );
return RetValue;
}
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 0b93fb73..d6f6d74a 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -703,7 +703,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
Fra_Sml_t * p;
- p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
+ p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
p->pAig = pAig;
p->nPref = nPref;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:37:14 +0000