From 4d71c114a3405f0a2c59a8467c82a8da3f785262 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 21 Sep 2008 08:01:00 -0700
Subject: Version abc80921
---
src/aig/aig/aig.h | 1 +
src/aig/aig/aigDfs.c | 27 ++++++
src/aig/dch/dchSat.c | 4 +-
src/aig/dch/dchSimSat.c | 11 ++-
src/aig/fra/fraSec.c | 19 +++--
src/aig/int/intCtrex.c | 5 +-
src/aig/ntl/ntlFraig.c | 8 +-
src/aig/ssw/ssw.h | 9 +-
src/aig/ssw/sswAig.c | 18 ++--
src/aig/ssw/sswClass.c | 42 ++-------
src/aig/ssw/sswCore.c | 86 ++++++++++++++++---
src/aig/ssw/sswInt.h | 50 ++++++-----
src/aig/ssw/sswLcorr.c | 172 ++++++++++++++++++++++++++-----------
src/aig/ssw/sswMan.c | 23 ++---
src/aig/ssw/sswPairs.c | 2 +-
src/aig/ssw/sswSim.c | 215 ++++++++++++++++++++++-------------------------
src/aig/ssw/sswSimSat.c | 210 ++-------------------------------------------
src/aig/ssw/sswSweep.c | 60 +++++++++----
src/base/abci/abc.c | 6 +-
src/base/abci/abcDar.c | 1 -
src/map/pcm/module.make | 0
src/map/ply/module.make | 0
src/sat/bsat/satInterA.c | 68 +++++++--------
23 files changed, 510 insertions(+), 527 deletions(-)
delete mode 100644 src/map/pcm/module.make
delete mode 100644 src/map/ply/module.make
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 093912c3..fcaf41fa 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -471,6 +471,7 @@ extern int Aig_ManChoiceLevel( Aig_Man_t * p );
extern int Aig_DagSize( Aig_Obj_t * pObj );
extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
extern Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp );
extern void Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
extern Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
extern Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 3c6658d9..568d6a68 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -732,6 +732,33 @@ Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
return vSupp;
}
+/**Function*************************************************************
+
+ Synopsis [Counts the support size of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_SupportNodes( Aig_Man_t * p, Aig_Obj_t ** ppObjs, int nObjs, Vec_Ptr_t * vSupp )
+{
+ int i;
+ Vec_PtrClear( vSupp );
+ Aig_ManIncrementTravId( p );
+ Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+ for ( i = 0; i < nObjs; i++ )
+ {
+ assert( !Aig_IsComplement(ppObjs[i]) );
+ if ( Aig_ObjIsPo(ppObjs[i]) )
+ Aig_Support_rec( p, Aig_ObjFanin0(ppObjs[i]), vSupp );
+ else
+ Aig_Support_rec( p, ppObjs[i], vSupp );
+ }
+}
+
/**Function*************************************************************
Synopsis [Transfers the AIG from one manager into another.]
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index 66c7f7b9..07196259 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -50,13 +50,13 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
assert( !Aig_IsComplement(pOld) );
assert( pNew != pOld );
-// p->nCallsSince++; // experiment with this!!!
+ p->nCallsSince++; // experiment with this!!!
// check if SAT solver needs recycling
if ( p->pSat == NULL ||
(p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax &&
- ++p->nCallsSince > p->pPars->nCallsRecycle) )
+ p->nCallsSince > p->pPars->nCallsRecycle) )
Dch_ManSatSolverRecycle( p );
// if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 7a6865bd..61d2ab93 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -60,10 +60,10 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vSimRoots, pObj );
return;
}
- // pRepr is the representative of the equivalence class
- if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pRepr) )
+ // pRepr is the representative of an equivalence class
+ if ( pRepr->fMarkA )
return;
- Aig_ObjSetTravIdCurrent(p->pAigTotal, pRepr);
+ pRepr->fMarkA = 1;
Vec_PtrPush( p->vSimClasses, pRepr );
}
@@ -80,6 +80,8 @@ void Dch_ManCollectTfoCands_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
***********************************************************************/
void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
{
+ Aig_Obj_t * pObj;
+ int i;
Vec_PtrClear( p->vSimRoots );
Vec_PtrClear( p->vSimClasses );
Aig_ManIncrementTravId( p->pAigTotal );
@@ -88,6 +90,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
Dch_ManCollectTfoCands_rec( p, pObj2 );
Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
+ Vec_PtrForEachEntry( p->vSimClasses, pObj, i )
+ pObj->fMarkA = 0;
}
/**Function*************************************************************
@@ -116,6 +120,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
// get the value from the SAT solver
// (account for the fact that some vars may be minimized away)
pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+// pObj->fMarkB = !nVarNum? Aig_ManRandom(0) & 1 : sat_solver_var_value( p->pSat, nVarNum );
return;
}
Dch_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj) );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 677123d8..232a789e 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -92,8 +92,6 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
if ( RetValue >= 0 )
goto finish;
- // prepare parameters
- Ssw_ManSetDefaultParams( pPars2 );
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
@@ -142,7 +140,8 @@ PRT( "Time", clock() - clk );
if ( pParSec->fRetimeFirst && pNew->nRegs )
{
clk = clock();
- pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+// pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+ pNew = Saig_ManRetimeForward( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( pParSec->fVerbose )
{
@@ -172,11 +171,21 @@ clk = clock();
goto finish;
}
}
- pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+
+
+// pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+//Aig_ManDumpBlif( pNew, "ex.blif", NULL, NULL );
+ Ssw_ManSetDefaultParamsLcorr( pPars2 );
+ pNew = Ssw_LatchCorrespondence( pTemp = pNew, pPars2 );
+ nIter = pPars2->nIters;
+
+ // prepare parameters for scorr
+ Ssw_ManSetDefaultParams( pPars2 );
+
if ( pTemp->pSeqModel )
{
if ( !Ssw_SmlRunCounterExample( pTemp, pTemp->pSeqModel ) )
- printf( "Fra_FraigLatchCorrespondence(): Counter-example verification has FAILED.\n" );
+ printf( "Fra_FraigSec(): Counter-example verification has FAILED.\n" );
if ( Saig_ManPiNum(p) != Saig_ManPiNum(pTemp) )
printf( "The counter-example is invalid because of phase abstraction.\n" );
else
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index 5e417ce0..4cbe2007 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -66,7 +66,10 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
break;
// transfer to register outputs
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
- pObjLo->pData = pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
+ pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
}
// create POs for the output of the last frame
pObj = Aig_ManPo( pAig, 0 );
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index b1239e47..27d863af 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -435,6 +435,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
***********************************************************************/
Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
{
+ Ssw_Pars_t Pars, * pPars = &Pars;
Ntl_Man_t * pNew, * pAux;
Aig_Man_t * pAig, * pAigCol, * pTemp;
@@ -444,7 +445,12 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
pAigCol = Ntl_ManCollapseSeq( pNew, 0 );
// perform SCL for the given design
- pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
+// pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL, 0 );
+ Ssw_ManSetDefaultParamsLcorr( pPars );
+ pPars->nBTLimit = nConfMax;
+ pPars->fVerbose = fVerbose;
+ pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
+
Aig_ManStop( pTemp );
if ( p->vRegClasses && Vec_IntSize(p->vRegClasses) && pAigCol->pReprs )
Ntl_ManFilterRegisterClasses( pAigCol, p->vRegClasses, fVerbose );
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 2917f6d4..8d74f16b 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -50,11 +50,12 @@ struct Ssw_Pars_t_
int nBTLimit; // conflict limit at a node
int nMinDomSize; // min clock domain considered for optimization
int fPolarFlip; // uses polarity adjustment
+ int fSkipCheck; // do not run equivalence check for unaffected cones
int fLatchCorr; // perform register correspondence
+ // optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
- int nCallsRecycle; // calls to perform before recycling SAT solver (optimized latch corr only)
- int fSkipCheck; // does not run equivalence check for unaffected cones
+ int nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
int fVerbose; // verbose stats
// internal parameters
int nIters; // the number of iterations performed
@@ -82,7 +83,9 @@ struct Ssw_Cex_t_
/*=== sswCore.c ==========================================================*/
extern void Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
-extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+extern void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p );
+extern Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+extern Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPart.c ==========================================================*/
extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
/*=== sswPairs.c ===================================================*/
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 854a0e12..5a47ba5f 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -49,9 +49,9 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
// get the new node
- pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
+ pObjNew = Ssw_ObjFrame( p, pObj, iFrame );
// get the new node of the representative
- pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
+ pObjReprNew = Ssw_ObjFrame( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( pObj->fPhase == pObjRepr->fPhase )
{
@@ -69,7 +69,7 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
- Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
+ Ssw_ObjSetFrame( p, pObj, iFrame, pObjNew2 );
// add the constraint
Aig_ObjCreatePo( pFrames, pObjNew2 );
Aig_ObjCreatePo( pFrames, pObjNew );
@@ -99,15 +99,15 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
p->nConstrTotal = p->nConstrReduced = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
- Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
Aig_ManForEachPiSeq( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
@@ -115,16 +115,16 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
Aig_ManForEachNode( p->pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
}
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
- Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
+ Ssw_ObjSetFrame( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
}
// add the POs for the latch outputs of the last frame
Saig_ManForEachLo( p->pAig, pObj, i )
- Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
+ Aig_ObjCreatePo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
// remove dangling nodes
Aig_ManCleanup( pFrames );
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 81e8de8b..db593311 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -286,6 +286,8 @@ int Ssw_ClassesLitNum( Ssw_Cla_t * p )
***********************************************************************/
Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
{
+ if ( p->pId2Class[pRepr->Id] == NULL )
+ return NULL;
assert( p->pId2Class[pRepr->Id] != NULL );
assert( p->pClassSizes[pRepr->Id] > 1 );
*pnSize = p->pClassSizes[pRepr->Id];
@@ -333,6 +335,7 @@ void Ssw_ClassesCheck( Ssw_Cla_t * p )
Ssw_ManForEachClass( p, ppClass, k )
{
pPrev = NULL;
+ assert( p->pClassSizes[ppClass[0]->Id] >= 2 );
Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
{
if ( i == 0 )
@@ -423,12 +426,15 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pRepr, * pTemp;
+ assert( p->pClassSizes[pObj->Id] == 0 );
assert( p->pId2Class[pObj->Id] == NULL );
pRepr = Aig_ObjRepr( p->pAig, pObj );
assert( pRepr != NULL );
Vec_PtrPush( p->vRefined, pObj );
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
{
+ assert( p->pClassSizes[pRepr->Id] == 0 );
+ assert( p->pId2Class[pRepr->Id] == NULL );
Aig_ObjSetRepr( p->pAig, pObj, NULL );
p->nCands1--;
return;
@@ -439,7 +445,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
assert( p->pClassSizes[pRepr->Id] >= 2 );
if ( p->pClassSizes[pRepr->Id] == 2 )
{
- p->pId2Class[pObj->Id] = NULL;
+ p->pId2Class[pRepr->Id] = NULL;
p->nClasses--;
p->pClassSizes[pRepr->Id] = 0;
p->nLits--;
@@ -491,7 +497,7 @@ PRT( "Simulation of 32 frames with 4 words", clock() - clk );
// set comparison procedures
clk = clock();
- Ssw_ClassesSetData( p, pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+ Ssw_ClassesSetData( p, pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// allocate the hash table hashing simulation info into nodes
nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
@@ -591,38 +597,6 @@ PRT( "Collecting candidate equival classes", clock() - clk );
return p;
}
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
-{
- return pObj->fPhase == pObj->fMarkB;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the nodes appear equal.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
- return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
-}
-
/**Function*************************************************************
Synopsis [Creates initial simulation classes.]
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 6a3e9264..fc9f5672 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -50,16 +50,35 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->nBTLimit = 1000; // conflict limit at a node
p->nMinDomSize = 100; // min clock domain considered for optimization
p->fPolarFlip = 0; // uses polarity adjustment
+ p->fSkipCheck = 0; // do not run equivalence check for unaffected cones
p->fLatchCorr = 0; // performs register correspondence
p->fVerbose = 0; // verbose stats
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
- p->nSatVarMax = 5000; // the max number of SAT variables
- p->nCallsRecycle = 100; // calls to perform before recycling SAT solver
+ p->nSatVarMax = 1000; // the max number of SAT variables
+ p->nRecycleCalls = 50; // calls to perform before recycling SAT solver
// return values
p->nIters = 0; // the number of iterations performed
}
+/**Function*************************************************************
+
+ Synopsis [This procedure sets default parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
+{
+ Ssw_ManSetDefaultParams( p );
+ p->fLatchCorrOpt = 1;
+ p->nBTLimit = 10000;
+}
+
/**Function*************************************************************
Synopsis [Performs computation of signal correspondence with constraints.]
@@ -73,6 +92,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
{
+ int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal;
Aig_Man_t * pAigNew;
int RetValue, nIter;
int clk, clkTotal = clock();
@@ -97,23 +117,40 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using induction
+ nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
for ( nIter = 0; ; nIter++ )
{
clk = clock();
if ( p->pPars->fLatchCorrOpt )
+ {
RetValue = Ssw_ManSweepLatch( p );
+ if ( p->pPars->fVerbose )
+ {
+ printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat,
+ p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
+ PRT( "T", clock() - clk );
+ nSatProof = p->nSatProof;
+ nSatCallsSat = p->nSatCallsSat;
+ nRecycles = p->nRecycles;
+ nSatFailsReal = p->nSatFailsReal;
+ }
+ }
else
- RetValue = Ssw_ManSweep( p );
- if ( p->pPars->fVerbose )
{
- printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
- nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
- p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
- if ( p->pPars->fSkipCheck )
- printf( "Use = %5d. Skip = %5d. ",
- p->nRefUse, p->nRefSkip );
- PRT( "T", clock() - clk );
- }
+ RetValue = Ssw_ManSweep( p );
+ if ( p->pPars->fVerbose )
+ {
+ printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ",
+ nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses),
+ p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+ if ( p->pPars->fSkipCheck )
+ printf( "Use = %5d. Skip = %5d. ",
+ p->nRefUse, p->nRefSkip );
+ PRT( "T", clock() - clk );
+ }
+ }
Ssw_ManCleanup( p );
if ( !RetValue )
break;
@@ -161,7 +198,10 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
}
// check and update parameters
if ( pPars->fLatchCorrOpt )
+ {
pPars->fLatchCorr = 1;
+ pPars->nFramesAddSim = 0;
+ }
else
{
assert( pPars->nFramesK > 0 );
@@ -181,13 +221,13 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// perform one round of seq simulation and generate candidate equivalence classes
p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
- Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
}
else
{
// create trivial equivalence classes with all nodes being candidates for constant 1
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
- Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
+ Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_SmlObjIsConstBit, Ssw_SmlObjsAreEqualBit );
}
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
@@ -196,6 +236,24 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
return pAigNew;
}
+/**Function*************************************************************
+
+ Synopsis [Performs computation of latch correspondence.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ssw_LatchCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+ Ssw_Pars_t Pars;
+ if ( pPars == NULL )
+ Ssw_ManSetDefaultParamsLcorr( pPars = &Pars );
+ return Ssw_SignalCorrespondence( pAig, pPars );
+}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 5b4377c7..faa3a87d 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -53,25 +53,31 @@ struct Ssw_Man_t_
// AIGs used in the package
Aig_Man_t * pAig; // user-given AIG
Aig_Man_t * pFrames; // final AIG
- Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes
+ Aig_Obj_t ** pNodeToFrames; // mapping of AIG nodes into FRAIG nodes
// equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes of nodes
int fRefined; // is set to 1 when refinement happens
- int nRefUse;
- int nRefSkip;
+ int nRefUse; // the number of equivalences used
+ int nRefSkip; // the number of equivalences skipped
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
int * pSatVars; // mapping of each node into its SAT var
int nSatVarsTotal; // the total number of SAT vars created
Vec_Ptr_t * vFanins; // fanins of the CNF node
- Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate
- Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate
// SAT solving (latch corr only)
- int nCallsSince; // the number of calls since last recycling
- int nRecycles; // the number of time SAT solver was recycled
Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables
Vec_Ptr_t * vUsedPis; // the PIs with SAT variables
+ Vec_Ptr_t * vSimInfo; // simulation information for the framed PIs
+ int nPatterns; // the number of patterns saved
+ int nSimRounds; // the number of simulation rounds performed
+ int nCallsCount; // the number of calls in this round
+ int nCallsDelta; // the number of calls to skip
+ int nCallsSat; // the number of SAT calls in this round
+ int nCallsUnsat; // the number of UNSAT calls in this round
+ int nRecycleCalls; // the number of calls since last recycling
+ int nRecycles; // the number of time SAT solver was recycled
+ int nConeMax; // the maximum cone size
// sequential simulator
Ssw_Sml_t * pSml;
// counter example storage
@@ -125,11 +131,11 @@ static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
}
-static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFraig[p->nFrames*pObj->Id + i]; }
-static inline void Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
+static inline Aig_Obj_t * Ssw_ObjFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { return p->pNodeToFrames[p->nFrames*pObj->Id + i]; }
+static inline void Ssw_ObjSetFrame( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFrames[p->nFrames*pObj->Id + i] = pNode; }
-static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
-static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
+static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL; }
+static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
@@ -161,8 +167,6 @@ extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
-extern int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj );
-extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
/*=== sswCnf.c ===================================================*/
extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
/*=== sswCore.c ===================================================*/
@@ -178,19 +182,23 @@ extern void Ssw_ManStartSolver( Ssw_Man_t * p );
extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== sswSim.c ===================================================*/
+extern unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
+extern int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
+extern int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
+extern void Ssw_SmlClean( Ssw_Sml_t * p );
extern void Ssw_SmlStop( Ssw_Sml_t * p );
-extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
-extern unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj );
-extern int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj );
-extern int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
+extern void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
extern void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
extern void Ssw_SmlSimulateOne( Ssw_Sml_t * p );
+extern void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
+extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
/*=== sswSimSat.c ===================================================*/
-extern int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
-extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
-extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
-extern void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
+extern void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
+extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index dcc4f245..cde9b0c9 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "sswInt.h"
-#include "bar.h"
+//#include "bar.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -67,12 +67,13 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pFrames), p->nSatVars++ );
p->nRecycles++;
- p->nCallsSince = 0;
+ p->nRecycleCalls = 0;
}
+
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
+ Synopsis [Tranfers simulation information from FRAIG to AIG.]
Description []
@@ -81,19 +82,30 @@ void Ssw_ManSatSolverRecycle( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
+void Ssw_ManSweepTransfer( Ssw_Man_t * p )
{
- Aig_Obj_t * pObj;
+ Aig_Obj_t * pObj, * pObjFraig;
+ unsigned * pInfo;
int i;
- memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+ // transfer simulation information
Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Ssw_ManOriginalPiValue( p, pObj, 0 ) )
- Aig_InfoSetBit( p->pPatWords, i );
+ {
+ pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
+ if ( pObjFraig == Aig_ManConst0(p->pFrames) )
+ {
+ Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
+ continue;
+ }
+ assert( !Aig_IsComplement(pObjFraig) );
+ assert( Aig_ObjIsPi(pObjFraig) );
+ pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
+ }
}
/**Function*************************************************************
- Synopsis [Copy pattern from the solver into the internal storage.]
+ Synopsis [Performs one round of simulation with counter-examples.]
Description []
@@ -102,14 +114,50 @@ void Ssw_SmlSavePatternLatch( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-void Ssw_SmlSavePatternLatchPhase( Ssw_Man_t * p, int f )
+int Ssw_ManSweepResimulate( Ssw_Man_t * p )
+{
+ int RetValue1, RetValue2, clk = clock();
+ // transfer PI simulation information from storage
+ Ssw_ManSweepTransfer( p );
+ // simulate internal nodes
+ Ssw_SmlSimulateOneFrame( p->pSml );
+ // check equivalence classes
+ RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+ RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+ // prepare simulation info for the next round
+ Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+ p->nPatterns = 0;
+ p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+ return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Saves one counter-example into internal storage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
{
Aig_Obj_t * pObj;
- int i;
- memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
- Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
- Aig_InfoSetBit( p->pPatWords, i );
+ unsigned * pInfo;
+ int i, nVarNum, Value;
+ Vec_PtrForEachEntry( p->vUsedPis, pObj, i )
+ {
+ nVarNum = Ssw_ObjSatNum( p, pObj );
+ assert( nVarNum > 0 );
+ Value = sat_solver_var_value( p->pSat, nVarNum );
+ if ( Value == 0 )
+ continue;
+ pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+ Aig_InfoSetBit( pInfo, p->nPatterns );
+ }
}
/**Function*************************************************************
@@ -127,13 +175,13 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjNew;
assert( !Aig_IsComplement(pObj) );
- if ( Ssw_ObjFraig( p, pObj, 0 ) )
+ if ( Ssw_ObjFrame( p, pObj, 0 ) )
return;
assert( Aig_ObjIsNode(pObj) );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObj) );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin1(pObj) );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, 0), Ssw_ObjChild1Fra(p, pObj, 0) );
- Ssw_ObjSetFraig( p, pObj, 0, pObjNew );
+ Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
}
/**Function*************************************************************
@@ -149,10 +197,18 @@ void Ssw_ManBuildCone_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
***********************************************************************/
void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj )
{
- Aig_Obj_t * pObjFraig, * pObjFraig2, * pObjReprFraig, * pObjLi;
- int RetValue;
+ Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi;
+ int RetValue, clk;
assert( Aig_ObjIsPi(pObj) );
assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) );
+ // check if it makes sense to skip some calls
+ if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat )
+ {
+ if ( ++p->nCallsDelta < 0 )
+ return;
+ }
+ p->nCallsDelta = 0;
+clk = clock();
// get the fraiged node
pObjLi = Saig_ObjLoToLi( p->pAig, pObj );
Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) );
@@ -165,43 +221,44 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
pObjReprFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 );
}
else
- pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, 0 );
+ pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, 0 );
+p->timeReduce += clock() - clk;
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
return;
- p->nCallsSince++;
+ p->nRecycleCalls++;
+ p->nCallsCount++;
+
// check equivalence of the two nodes
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
{
+ p->nPatterns++;
p->nStrangers++;
- Ssw_SmlSavePatternLatchPhase( p, 0 );
+ p->fRefined = 1;
}
else
{
RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
- if ( RetValue == 1 ) // proved equivalent
+ if ( RetValue == 1 ) // proved equivalence
{
- pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
- Ssw_ObjSetFraig( p, pObj, 0, pObjFraig2 );
+ p->nCallsUnsat++;
return;
}
- else if ( RetValue == -1 ) // timed out
+ if ( RetValue == -1 ) // timed out
{
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+ p->nCallsUnsat++;
p->fRefined = 1;
return;
}
- else // disproved the equivalence
+ else // disproved equivalence
{
- Ssw_SmlSavePatternLatch( p );
+ Ssw_SmlAddPattern( p, pObjRepr, pObj );
+ p->nPatterns++;
+ p->nCallsSat++;
+ p->fRefined = 1;
}
}
- if ( p->pPars->nConstrs == 0 )
- Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, 0 );
- else
- Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, 0 );
- assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
- p->fRefined = 1;
}
/**Function*************************************************************
@@ -217,7 +274,7 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj
***********************************************************************/
int Ssw_ManSweepLatch( Ssw_Man_t * p )
{
- Bar_Progress_t * pProgress = NULL;
+// Bar_Progress_t * pProgress = NULL;
Vec_Ptr_t * vClass;
Aig_Obj_t * pObj, * pRepr, * pTemp;
int i, k;
@@ -225,30 +282,40 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
// start the timeframe
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) );
// map constants and PIs
- Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), 0, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreatePi(p->pFrames) );
// implement equivalence classes
Saig_ManForEachLo( p->pAig, pObj, i )
{
pRepr = Aig_ObjRepr( p->pAig, pObj );
if ( pRepr == NULL )
+ {
pTemp = Aig_ObjCreatePi(p->pFrames);
+ pTemp->pData = pObj;
+ }
else
- pTemp = Aig_NotCond( Ssw_ObjFraig(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
- Ssw_ObjSetFraig( p, pObj, 0, pTemp );
+ pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
+ Ssw_ObjSetFrame( p, pObj, 0, pTemp );
}
+ Aig_ManSetPioNumbers( p->pFrames );
+
+ // prepare simulation info
+ assert( p->vSimInfo == NULL );
+ p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+ Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
// go through the registers
- if ( p->pPars->fVerbose )
- pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
+// if ( p->pPars->fVerbose )
+// pProgress = Bar_ProgressStart( stdout, Aig_ManRegNum(p->pAig) );
vClass = Vec_PtrAlloc( 100 );
p->fRefined = 0;
+ p->nCallsCount = p->nCallsSat = p->nCallsUnsat = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
{
- if ( p->pPars->fVerbose )
- Bar_ProgressUpdate( pProgress, i, NULL );
+// if ( p->pPars->fVerbose )
+// Bar_ProgressUpdate( pProgress, i, NULL );
// consider the case of constant candidate
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
Ssw_ManSweepLatchOne( p, Aig_ManConst1(p->pAig), pObj );
@@ -261,21 +328,32 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
// try to prove equivalences in this class
Vec_PtrForEachEntry( vClass, pTemp, k )
if ( Aig_ObjRepr(p->pAig, pTemp) == pObj )
+ {
Ssw_ManSweepLatchOne( p, pObj, pTemp );
+ if ( p->nPatterns == 32 )
+ break;
+ }
}
+ // resimulate
+ if ( p->nPatterns == 32 )
+ Ssw_ManSweepResimulate( p );
// attempt recycling the SAT solver
if ( p->pPars->nSatVarMax &&
p->nSatVars > p->pPars->nSatVarMax &&
- p->nCallsSince > p->pPars->nCallsRecycle )
+ p->nRecycleCalls > p->pPars->nRecycleCalls )
Ssw_ManSatSolverRecycle( p );
}
+ // resimulate
+ if ( p->nPatterns > 0 )
+ Ssw_ManSweepResimulate( p );
+ // cleanup
Vec_PtrFree( vClass );
p->nSatFailsTotal += p->nSatFailsReal;
- if ( p->pPars->fVerbose )
- Bar_ProgressStop( pProgress );
+// if ( p->pPars->fVerbose )
+// Bar_ProgressStop( pProgress );
// cleanup
- Ssw_ClassesCheck( p->ppClasses );
+// Ssw_ClassesCheck( p->ppClasses );
return p->fRefined;
}
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 33c716ce..8d2c8c24 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -52,12 +52,10 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
p->pPars = pPars;
p->pAig = pAig;
p->nFrames = pPars->nFramesK + 1;
- p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
+ p->pNodeToFrames = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
// SAT solving
p->pSatVars = CALLOC( int, Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
p->vFanins = Vec_PtrAlloc( 100 );
- p->vSimRoots = Vec_PtrAlloc( 1000 );
- p->vSimClasses = Vec_PtrAlloc( 1000 );
// SAT solving (latch corr only)
p->vUsedNodes = Vec_PtrAlloc( 1000 );
p->vUsedPis = Vec_PtrAlloc( 1000 );
@@ -102,13 +100,15 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
{
double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
- printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
- p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
+ printf( "Parameters: F = %d. AddF = %d. C-lim = %d. Constr = %d. MaxLev = %d. Mem = %0.2f Mb.\n",
+ p->pPars->nFramesK, p->pPars->nFramesAddSim, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
printf( "AIG : PI = %d. PO = %d. Latch = %d. Node = %d. Ave SAT vars = %d.\n",
Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig),
p->nSatVarsTotal/p->pPars->nIters );
printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n",
p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
+ printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n",
+ p->nSatVars, p->nConeMax, p->nRecycles, p->nSimRounds );
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->nNodesBeg:1),
p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
@@ -139,12 +139,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
***********************************************************************/
void Ssw_ManCleanup( Ssw_Man_t * p )
{
- Aig_ManCleanMarkB( p->pAig );
if ( p->pFrames )
{
Aig_ManStop( p->pFrames );
p->pFrames = NULL;
- memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
+ memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
}
if ( p->pSat )
{
@@ -154,6 +153,11 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
p->pSat = NULL;
memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * (p->nFrames+1) );
}
+ if ( p->vSimInfo )
+ {
+ Vec_PtrFree( p->vSimInfo );
+ p->vSimInfo = NULL;
+ }
p->nConstrTotal = 0;
p->nConstrReduced = 0;
}
@@ -172,6 +176,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
void Ssw_ManStop( Ssw_Man_t * p )
{
Aig_ManCleanMarkA( p->pAig );
+ Aig_ManCleanMarkB( p->pAig );
if ( p->pPars->fVerbose )
Ssw_ManPrintStats( p );
if ( p->ppClasses )
@@ -179,11 +184,9 @@ void Ssw_ManStop( Ssw_Man_t * p )
if ( p->pSml )
Ssw_SmlStop( p->pSml );
Vec_PtrFree( p->vFanins );
- Vec_PtrFree( p->vSimRoots );
- Vec_PtrFree( p->vSimClasses );
Vec_PtrFree( p->vUsedNodes );
Vec_PtrFree( p->vUsedPis );
- FREE( p->pNodeToFraig );
+ FREE( p->pNodeToFrames );
FREE( p->pSatVars );
FREE( p->pPatWords );
free( p );
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index a11bdf98..c77ad30d 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -289,7 +289,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
// create equivalence classes using these IDs
p->ppClasses = Ssw_ClassesPreparePairs( pMiter, pvClasses );
p->pSml = Ssw_SmlStart( pMiter, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
- Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+ Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
// perform refinement of classes
pAigNew = Ssw_SignalCorrespondenceRefine( p );
// cleanup
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 769e923c..ba8ad247 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -57,7 +57,7 @@ static inline unsigned Ssw_ObjRandomSim() { return Aig_ManRa
SeeAlso []
***********************************************************************/
-unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+unsigned Ssw_SmlObjHashWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
@@ -96,7 +96,7 @@ unsigned Ssw_SmlNodeHash( Ssw_Sml_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj )
+int Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj )
{
unsigned * pSims;
int i;
@@ -118,7 +118,7 @@ int Ssw_SmlNodeIsConst( Ssw_Sml_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+int Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
unsigned * pSims0, * pSims1;
int i;
@@ -130,6 +130,39 @@ int Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the node appears to be constant 1 candidate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj )
+{
+ return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the nodes appear equal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+ return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+
/**Function*************************************************************
Synopsis [Counts the number of 1s in the XOR of simulation data.]
@@ -340,7 +373,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
Aig_ManForEachPo( p->pAig, pObj, i )
{
- if ( !Ssw_SmlNodeIsConst( p, Aig_ObjFanin0(pObj) ) )
+ if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
return Ssw_SmlCheckOutputSavePattern( p, pObj );
@@ -404,7 +437,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
SeeAlso []
***********************************************************************/
-void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
+void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
{
unsigned * pSims;
int i;
@@ -414,6 +447,25 @@ void Ssw_SmlAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram
pSims[i] = fConst1? ~(unsigned)0 : 0;
}
+/**Function*************************************************************
+
+ Synopsis [Assigns constant patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
+{
+ unsigned * pSims;
+ assert( Aig_ObjIsPi(pObj) );
+ pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+ pSims[iWord] = Word;
+}
+
/**Function*************************************************************
Synopsis [Assings random simulation info for the PIs.]
@@ -438,7 +490,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
Ssw_SmlAssignRandom( p, pObj );
// assign the initial state for the latches
Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_SmlAssignConst( p, pObj, 0, 0 );
+ Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
}
else
{
@@ -467,7 +519,7 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
{
// copy the PI info
Aig_ManForEachPi( p->pAig, pObj, i )
- Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+ Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// flip one bit
Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
for ( i = 0; i < Limit; i++ )
@@ -481,11 +533,11 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat )
nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
for ( f = 0; f < p->nFrames; f++ )
Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+ Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
// copy the latch info
k = 0;
Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
+ Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
// assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) );
// flip one bit of the last frame
@@ -517,7 +569,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
// copy the pattern into the primary inputs
Aig_ManForEachPi( p->pAig, pObj, i )
- Ssw_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+ Ssw_SmlObjAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
// set distance one PIs for the first frame
Limit = AIG_MIN( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
@@ -530,7 +582,6 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat )
Ssw_SmlAssignRandomFrame( p, pObj, f );
}
-
/**Function*************************************************************
Synopsis [Simulates one node.]
@@ -746,46 +797,39 @@ p->timeSim += clock() - clk;
p->nSimRounds++;
}
-
-#if 0
-
/**Function*************************************************************
- Synopsis [Resimulates fraiging manager after finding a counter-example.]
+ Synopsis [Simulates AIG manager.]
- Description []
+ Description [Assumes that the PI simulation info is attached.]
SideEffects []
SeeAlso []
***********************************************************************/
-void Ssw_SmlResimulate( Ssw_Man_t * p )
+void Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p )
{
- int nChanges, clk;
- Ssw_SmlAssignDist1( p, p->pPatWords );
- Ssw_SmlSimulateOne( p );
-// if ( p->pPars->fPatScores )
-// Ssw_CleanPatScores( p );
- if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
- return;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, clk;
clk = clock();
- nChanges = Ssw_ClassesRefine( p->pCla, 1 );
- nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
- if ( p->pCla->vImps )
- nChanges += Ssw_ImpRefineUsingCex( p, p->pCla->vImps );
- if ( p->vOneHots )
- nChanges += Ssw_OneHotRefineUsingCex( p, p->vOneHots );
-p->timeRef += clock() - clk;
- if ( !p->pPars->nFramesK && nChanges < 1 )
- printf( "Error: A counter-example did not refine classes!\n" );
-// assert( nChanges >= 1 );
-//printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
+ // simulate the nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ Ssw_SmlNodeSimulate( p, pObj, 0 );
+ // copy simulation info into outputs
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ Ssw_SmlNodeCopyFanin( p, pObj, 0 );
+ // copy simulation info into the inputs
+ Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+ Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
+p->timeSim += clock() - clk;
+p->nSimRounds++;
}
+
/**Function*************************************************************
- Synopsis [Performs simulation of the manager.]
+ Synopsis [Allocates simulation manager.]
Description []
@@ -794,69 +838,19 @@ p->timeRef += clock() - clk;
SeeAlso []
***********************************************************************/
-void Ssw_SmlSimulate( Ssw_Man_t * p, int fInit )
+Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
{
- int fVerbose = 0;
- int nChanges, nClasses, clk;
- assert( !fInit || Aig_ManRegNum(p->pAig) );
- // start the classes
- Ssw_SmlInitialize( p, fInit );
- Ssw_SmlSimulateOne( p );
- if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
- return;
- Ssw_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
-// Ssw_ClassesPrint( p->pCla, 0 );
-if ( fVerbose )
-printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) );
-
-//return;
-
- // refine classes by walking 0/1 patterns
- Ssw_SmlSavePattern0( p, fInit );
- Ssw_SmlAssignDist1( p, p->pPatWords );
- Ssw_SmlSimulateOne( p );
- if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
- return;
-clk = clock();
- nChanges = Ssw_ClassesRefine( p->pCla, 1 );
- nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
- Ssw_SmlSavePattern1( p, fInit );
- Ssw_SmlAssignDist1( p, p->pPatWords );
- Ssw_SmlSimulateOne( p );
- if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
- return;
-clk = clock();
- nChanges = Ssw_ClassesRefine( p->pCla, 1 );
- nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-
-if ( fVerbose )
-printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
- // refine classes by random simulation
- do {
- Ssw_SmlInitialize( p, fInit );
- Ssw_SmlSimulateOne( p );
- nClasses = Vec_PtrSize(p->pCla->vClasses);
- if ( p->pPars->fProve && Ssw_SmlCheckOutput(p) )
- return;
-clk = clock();
- nChanges = Ssw_ClassesRefine( p->pCla, 1 );
- nChanges += Ssw_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Ssw_ClassesCountLits(p->pCla) );
- } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
-
-// if ( p->pPars->fVerbose )
-// printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n",
-// Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Ssw_ClassesCountLits(p->pCla) );
-// Ssw_ClassesPrint( p->pCla, 0 );
+ Ssw_Sml_t * p;
+ p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
+ memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
+ p->pAig = pAig;
+ p->nPref = nPref;
+ p->nFrames = nPref + nFrames;
+ p->nWordsFrame = nWordsFrame;
+ p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
+ p->nWordsPref = nPref * nWordsFrame;
+ return p;
}
-
-#endif
/**Function*************************************************************
@@ -869,18 +863,9 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(
SeeAlso []
***********************************************************************/
-Ssw_Sml_t * Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
+void Ssw_SmlClean( Ssw_Sml_t * p )
{
- Ssw_Sml_t * p;
- p = (Ssw_Sml_t *)malloc( sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
- memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
- p->pAig = pAig;
- p->nPref = nPref;
- p->nFrames = nPref + nFrames;
- p->nWordsFrame = nWordsFrame;
- p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
- p->nWordsPref = nPref * nWordsFrame;
- return p;
+ memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
}
/**Function*************************************************************
@@ -1005,11 +990,11 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
- Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+ Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
- Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+ Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
@@ -1042,11 +1027,11 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
- Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+ Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
- Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+ Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
@@ -1271,13 +1256,13 @@ int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Ssw_Cex_t * p )
// assign simulation info for the registers
iBit = 0;
Saig_ManForEachLo( pAig, pObj, i )
-// Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
- Ssw_SmlAssignConst( pSml, pObj, 0, 0 );
+// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+ Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 );
// assign simulation info for the primary inputs
iBit = p->nRegs;
for ( i = 0; i <= p->iFrame; i++ )
Saig_ManForEachPi( pAig, pObj, k )
- Ssw_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+ Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Ssw_SmlSimulateOne( pSml );
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 715750ca..c85b8bcf 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -28,157 +28,6 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-/**Function*************************************************************
-
- Synopsis [Collects internal nodes in the reverse DFS order.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pFanout, * pRepr;
- int iFanout = -1, i;
- assert( !Aig_IsComplement(pObj) );
- if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAig, pObj);
- // traverse the fanouts
- Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i )
- Ssw_ManCollectTfoCands_rec( p, pFanout );
- // check if the given node has a representative
- pRepr = Aig_ObjRepr( p->pAig, pObj );
- if ( pRepr == NULL )
- return;
- // pRepr is the constant 1 node
- if ( pRepr == Aig_ManConst1(p->pAig) )
- {
- Vec_PtrPush( p->vSimRoots, pObj );
- return;
- }
- // pRepr is the representative of the equivalence class
- if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
- Vec_PtrPush( p->vSimClasses, pRepr );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collect equivalence classes and const1 cands in the TFO.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
-{
- Vec_PtrClear( p->vSimRoots );
- Vec_PtrClear( p->vSimClasses );
- Aig_ManIncrementTravId( p->pAig );
- Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
- Ssw_ManCollectTfoCands_rec( p, pObj1 );
- Ssw_ManCollectTfoCands_rec( p, pObj2 );
- Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
- Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
-}
-
-/**Function*************************************************************
-
- Synopsis [Retrives value of the PI in the original AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
-{
- Aig_Obj_t * pObjFraig;
- int nVarNum, Value;
- assert( Aig_ObjIsPi(pObj) );
- pObjFraig = Ssw_ObjFraig( p, pObj, f );
- nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
- Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
- if ( p->pPars->fPolarFlip )
- {
- if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1;
- }
-/*
- if ( nVarNum==0 )
- printf( "x" );
- else if ( Value == 0 )
- printf( "0" );
- else
- printf( "1" );
-*/
- return Value;
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the solved nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAig, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
- return;
- }
- Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
- Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
-/**Function*************************************************************
-
- Synopsis [Resimulates the cone of influence of the other nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
-{
- if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
- return;
- Aig_ObjSetTravIdCurrent(p->pAig, pObj);
- if ( Aig_ObjIsPi(pObj) )
- {
- // set random value
- pObj->fMarkB = Aig_ManRandom(0) & 1;
- return;
- }
- Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
- Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
- pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
- & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-}
-
/**Function*************************************************************
Synopsis [Handle the counter-example.]
@@ -190,52 +39,7 @@ void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f )
-{
- Aig_Obj_t * pRoot, ** ppClass;
- int i, k, nSize, RetValue1, RetValue2, clk = clock();
- // get the equivalence classes
- Ssw_ManCollectTfoCands( p, pObj, pRepr );
- // resimulate the cone of influence of the solved nodes
- Aig_ManIncrementTravId( p->pAig );
- Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
- Ssw_ManResimulateSolved_rec( p, pObj, f );
- Ssw_ManResimulateSolved_rec( p, pRepr, f );
- // resimulate the cone of influence of the other nodes
- Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
- Ssw_ManResimulateOther_rec( p, pRoot );
- // refine these nodes
- RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
- // resimulate the cone of influence of the cand classes
- RetValue2 = 0;
- Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
- {
- ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize );
- for ( k = 0; k < nSize; k++ )
- Ssw_ManResimulateOther_rec( p, ppClass[k] );
- // refine this class
- RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
- }
- // make sure refinement happened
- if ( Aig_ObjIsConst1(pRepr) )
- assert( RetValue1 );
- else
- assert( RetValue2 );
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
- Synopsis [Handle the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
{
Aig_Obj_t * pObj;
int i, RetValue1, RetValue2, clk = clock();
@@ -255,18 +59,17 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
{
assert( RetValue1 );
if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateCexTotal() Error: RetValue1 does not hold.\n" );
+ printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateCexTotal() Error: RetValue2 does not hold.\n" );
+ printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
-
/**Function*************************************************************
Synopsis [Handle the counter-example.]
@@ -278,7 +81,7 @@ p->timeSimSat += clock() - clk;
SeeAlso []
***********************************************************************/
-void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
{
int RetValue1, RetValue2, clk = clock();
// set the PI simulation information
@@ -293,18 +96,17 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
{
assert( RetValue1 );
if ( RetValue1 == 0 )
- printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue1 does not hold.\n" );
+ printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
}
else
{
assert( RetValue2 );
if ( RetValue2 == 0 )
- printf( "\nSsw_ManResimulateCexTotalSim() Error: RetValue2 does not hold.\n" );
+ printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
}
p->timeSimSat += clock() - clk;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 1cf4b81b..9330dafa 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -76,6 +76,33 @@ void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
pObjLo->fMarkA |= pObjLi->fMarkA;
}
+/**Function*************************************************************
+
+ Synopsis [Retrives value of the PI in the original AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+ Aig_Obj_t * pObjFraig;
+ int nVarNum, Value;
+ assert( Aig_ObjIsPi(pObj) );
+ pObjFraig = Ssw_ObjFrame( p, pObj, f );
+ nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
+ Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+// Value = (!nVarNum)? Aig_ManRandom(0) & 1 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+ if ( p->pPars->fPolarFlip )
+ {
+ if ( Aig_Regular(pObjFraig)->fPhase ) Value ^= 1;
+ }
+ return Value;
+}
+
/**Function*************************************************************
Synopsis [Copy pattern from the solver into the internal storage.]
@@ -114,7 +141,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
int i;
memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+ if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
Aig_InfoSetBit( p->pPatWords, i );
}
@@ -138,9 +165,9 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( pObjRepr == NULL )
return;
// get the fraiged node
- pObjFraig = Ssw_ObjFraig( p, pObj, f );
+ pObjFraig = Ssw_ObjFrame( p, pObj, f );
// get the fraiged representative
- pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
+ pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
// check if constant 0 pattern distinquishes these nodes
assert( pObjFraig != NULL && pObjReprFraig != NULL );
if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
@@ -168,7 +195,7 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( RetValue == 1 ) // proved equivalent
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
- Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
+ Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return;
}
if ( RetValue == -1 ) // timed out
@@ -181,16 +208,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
{
assert( 0 );
- printf( "\nMistake!!!\n" );
+ printf( "\nSsw_ManSweepNode(): Error!\n" );
}
// disproved the equivalence
Ssw_SmlSavePatternAig( p, f );
}
-// Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
if ( p->pPars->nConstrs == 0 )
- Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+ Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
else
- Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
+ Ssw_ManResimulateBit( p, pObj, pObjRepr );
assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
p->fRefined = 1;
}
@@ -216,7 +242,7 @@ clk = clock();
// start initialized timeframes
p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
Saig_ManForEachLo( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) );
+ Ssw_ObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrames) );
// sweep internal nodes
p->fRefined = 0;
@@ -226,16 +252,16 @@ clk = clock();
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// map constants and PIs
- Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
// sweep internal nodes
Aig_ManForEachNode( p->pAig, pObj, i )
{
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f, 1 );
}
// quit if this is the last timeframe
@@ -246,7 +272,7 @@ clk = clock();
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
- Ssw_ObjSetFraig( p, pObjLo, f+1, pObjNew );
+ Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
Ssw_CnfNodeAddToSolver( p, Aig_Regular(pObjNew) );
}
}
@@ -307,12 +333,12 @@ p->timeMarkCones += clock() - clk;
// map constants and PIs of the last frame
f = p->pPars->nFramesK;
- Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+ Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+ Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
// make sure LOs are assigned
Saig_ManForEachLo( p->pAig, pObj, i )
- assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
+ assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
// sweep internal nodes
p->fRefined = 0;
p->nSatFailsReal = 0;
@@ -330,7 +356,7 @@ p->timeMarkCones += clock() - clk;
{
pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+ Ssw_ObjSetFrame( p, pObj, f, pObjNew );
Ssw_ManSweepNode( p, pObj, f, 0 );
}
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7247f8ed..09fd26ab 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -13888,10 +13888,10 @@ int Abc_CommandLcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFramesP = 0;
- nConfMax = 10000;
- nVarsMax = 5000;
+ nConfMax = 1000;
+ nVarsMax = 1000;
fNewAlgor = 0;
- fVerbose = 1;
+ fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PCSnvh" ) ) != EOF )
{
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ac5ee882..71443265 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1335,7 +1335,6 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
return NULL;
Ssw_ManSetDefaultParams( pPars );
pPars->fLatchCorrOpt = 1;
-// pPars->nFramesAddSim = 0;
pPars->nBTLimit = nConfMax;
pPars->nSatVarMax = nVarsMax;
pPars->fVerbose = fVerbose;
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 967639ae..57628989 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -544,13 +544,7 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int i, v, Var, PrevId;
int fPrint = 0;
int clk = clock();
-/*
- if ( pFinal->Id == 5187 )
- {
- int x = 0;
- Inta_ManPrintClause( p, pConflict );
- }
-*/
+
// collect resolvent literals
if ( p->fProofVerif )
{
@@ -579,28 +573,17 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
if ( !p->pSeens[Var] )
continue;
p->pSeens[Var] = 0;
-/*
- if ( pFinal->Id == 5187 )
- {
- printf( "pivot = %d ", p->pTrail[i] );
- }
-*/
+
// skip literals of the resulting clause
pReason = p->pReasons[Var];
if ( pReason == NULL )
continue;
assert( p->pTrail[i] == pReason->pLits[0] );
-/*
- if ( pFinal->Id == 5187 )
- {
- Inta_ManPrintClause( p, pReason );
- }
-*/
+
// add the variables to seen
for ( v = 1; v < (int)pReason->nLits; v++ )
p->pSeens[lit_var(pReason->pLits[v])] = 1;
-
// record the reason clause
assert( Inta_ManProofGet(p, pReason) > 0 );
p->Counter++;
@@ -656,7 +639,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
printf( "Recording clause %d: Trying to resolve the clause with more than one opposite literal.\n", pFinal->Id );
}
}
-
// Vec_PtrPush( pFinal->pAntis, pReason );
}
@@ -673,20 +655,6 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
int v1, v2;
if ( fPrint )
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
-/*
- if ( pFinal->Id == 5187 )
- {
- Inta_ManPrintResolvent( p->pResLits, p->nResLits );
- Inta_ManPrintClause( p, pFinal );
- }
-*/
-/*
- if ( p->nResLits != pFinal->nLits )
- {
- printf( "Recording clause %d: The resolvent is wrong (nRetLits = %d, pFinal->nLits = %d).\n",
- pFinal->Id, p->nResLits, pFinal->nLits );
- }
-*/
for ( v1 = 0; v1 < p->nResLits; v1++ )
{
for ( v2 = 0; v2 < (int)pFinal->nLits; v2++ )
@@ -703,6 +671,27 @@ int Inta_ManProofTraceOne( Inta_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pF
Inta_ManPrintResolvent( p->pResLits, p->nResLits );
Inta_ManPrintClause( p, pFinal );
}
+
+ // if there are literals in the clause that are not in the resolvent
+ // it means that the derived resolvent is stronger than the clause
+ // we can replace the clause with the resolvent by removing these literals
+ if ( p->nResLits != (int)pFinal->nLits )
+ {
+ for ( v1 = 0; v1 < (int)pFinal->nLits; v1++ )
+ {
+ for ( v2 = 0; v2 < p->nResLits; v2++ )
+ if ( pFinal->pLits[v1] == p->pResLits[v2] )
+ break;
+ if ( v2 < p->nResLits )
+ continue;
+ // remove literal v1 from the final clause
+ pFinal->nLits--;
+ for ( v2 = v1; v2 < (int)pFinal->nLits; v2++ )
+ pFinal->pLits[v2] = pFinal->pLits[v2+1];
+ v1--;
+ }
+ assert( p->nResLits == (int)pFinal->nLits );
+ }
}
p->timeTrace += clock() - clk;
@@ -736,9 +725,16 @@ int Inta_ManProofRecordOne( Inta_Man_t * p, Sto_Cls_t * pClause )
if ( pClause->nLits == 0 )
printf( "Error: Empty clause is attempted.\n" );
- // add assumptions to the trail
assert( !pClause->fRoot );
assert( p->nTrailSize == p->nRootSize );
+
+ // if any of the clause literals are already assumed
+ // it means that the clause is redundant and can be skipped
+ for ( i = 0; i < (int)pClause->nLits; i++ )
+ if ( p->pAssigns[lit_var(pClause->pLits[i])] == pClause->pLits[i] )
+ return 1;
+
+ // add assumptions to the trail
for ( i = 0; i < (int)pClause->nLits; i++ )
if ( !Inta_ManEnqueue( p, lit_neg(pClause->pLits[i]), NULL ) )
{
--
cgit v1.2.3