summaryrefslogtreecommitdiffstats
path: root/src/aig/llb
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/llb')
-rw-r--r--src/aig/llb/llb1Core.c1
-rw-r--r--src/aig/llb/llb1Man.c45
-rw-r--r--src/aig/llb/llb1Reach.c271
-rw-r--r--src/aig/llb/llbInt.h4
4 files changed, 262 insertions, 59 deletions
diff --git a/src/aig/llb/llb1Core.c b/src/aig/llb/llb1Core.c
index ff7eadbb..ad2c5934 100644
--- a/src/aig/llb/llb1Core.c
+++ b/src/aig/llb/llb1Core.c
@@ -208,6 +208,7 @@ int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars )
RetValue = Llb_ManModelCheckAig( pAig, pPars, NULL, NULL );
else
RetValue = Llb_ManModelCheckAigWithHints( pAig, pPars );
+ pGia->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
return RetValue;
}
diff --git a/src/aig/llb/llb1Man.c b/src/aig/llb/llb1Man.c
index d9c13a76..f5de25e0 100644
--- a/src/aig/llb/llb1Man.c
+++ b/src/aig/llb/llb1Man.c
@@ -47,9 +47,13 @@ void Llb_ManPrepareVarMap( Llb_Man_t * p )
Aig_Obj_t * pObjLi, * pObjLo;
int i, iVarLi, iVarLo;
assert( p->vNs2Glo == NULL );
+ assert( p->vCs2Glo == NULL );
assert( p->vGlo2Cs == NULL );
+ assert( p->vGlo2Ns == NULL );
p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
+ p->vCs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
+ p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
{
iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
@@ -57,7 +61,16 @@ void Llb_ManPrepareVarMap( Llb_Man_t * p )
assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
+ Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
+ Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
+ }
+ // add mapping of the PIs
+ Saig_ManForEachPi( p->pAig, pObjLo, i )
+ {
+ iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
+ Vec_IntWriteEntry( p->vCs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
+ Vec_IntWriteEntry( p->vNs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
}
}
@@ -117,6 +130,7 @@ void Llb_ManPrepareVarLimits( Llb_Man_t * p )
void Llb_ManStop( Llb_Man_t * p )
{
Llb_Grp_t * pGrp;
+ DdNode * bTemp;
int i;
// Vec_IntFreeP( &p->vMem );
@@ -128,25 +142,39 @@ void Llb_ManStop( Llb_Man_t * p )
Llb_MtrFree( p->pMatrix );
Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
Llb_ManGroupStop( pGrp );
- Vec_PtrFreeP( &p->vGroups );
- Vec_IntFreeP( &p->vVar2Obj );
- Vec_IntFreeP( &p->vObj2Var );
- Vec_IntFreeP( &p->vVarBegs );
- Vec_IntFreeP( &p->vVarEnds );
- Vec_IntFreeP( &p->vNs2Glo );
- Vec_IntFreeP( &p->vGlo2Cs );
-// Vec_IntFreeP( &p->vHints );
if ( p->dd )
{
+// printf( "Manager dd\n" );
Extra_StopManager( p->dd );
}
if ( p->ddG )
{
+// printf( "Manager ddG\n" );
if ( p->ddG->bFunc )
Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
Extra_StopManager( p->ddG );
}
+ if ( p->ddR )
+ {
+// printf( "Manager ddR\n" );
+ if ( p->ddR->bFunc )
+ Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
+ Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
+ Cudd_RecursiveDeref( p->ddR, bTemp );
+ Extra_StopManager( p->ddR );
+ }
Aig_ManStop( p->pAig );
+ Vec_PtrFreeP( &p->vGroups );
+ Vec_IntFreeP( &p->vVar2Obj );
+ Vec_IntFreeP( &p->vObj2Var );
+ Vec_IntFreeP( &p->vVarBegs );
+ Vec_IntFreeP( &p->vVarEnds );
+ Vec_PtrFreeP( &p->vRings );
+ Vec_IntFreeP( &p->vNs2Glo );
+ Vec_IntFreeP( &p->vCs2Glo );
+ Vec_IntFreeP( &p->vGlo2Cs );
+ Vec_IntFreeP( &p->vGlo2Ns );
+// Vec_IntFreeP( &p->vHints );
ABC_FREE( p );
}
@@ -172,6 +200,7 @@ Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t *
p->pAig = pAig;
p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
+ p->vRings = Vec_PtrAlloc( 100 );
Llb_ManPrepareVarMap( p );
Llb_ManPrepareGroups( p );
Aig_ManCleanMarkA( pAig );
diff --git a/src/aig/llb/llb1Reach.c b/src/aig/llb/llb1Reach.c
index 32944bef..341ebd95 100644
--- a/src/aig/llb/llb1Reach.c
+++ b/src/aig/llb/llb1Reach.c
@@ -152,7 +152,7 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
SeeAlso []
***********************************************************************/
-DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
+DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace, int fBackward )
{
Aig_Obj_t * pObj;
DdNode * bRes, * bTemp, * bVar;
@@ -162,6 +162,8 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
{
+ if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
+ continue;
iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
assert( iGroupFirst <= iGroupLast );
@@ -173,6 +175,8 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
}
Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
{
+ if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
+ continue;
iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
assert( iGroupFirst <= iGroupLast );
@@ -198,7 +202,7 @@ DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int
SeeAlso []
***********************************************************************/
-DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
+DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
{
Aig_Obj_t * pObj;
DdNode * bRes, * bTemp, * bVar;
@@ -232,6 +236,53 @@ DdNode * Llb_ManConstructQuantCube( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpP
/**Function*************************************************************
+ Synopsis [Derives quantification cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
+{
+ Aig_Obj_t * pObj;
+ DdNode * bRes, * bTemp, * bVar;
+ int i, iGroupFirst, TimeStop;
+ TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
+ bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
+ Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
+ {
+ if ( Saig_ObjIsPi(p->pAig, pObj) )
+ continue;
+ iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
+ assert( iGroupFirst <= iGrpPlace );
+ if ( iGroupFirst < iGrpPlace )
+ continue;
+ bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+ bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
+ Cudd_RecursiveDeref( p->dd, bTemp );
+ }
+ Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
+ {
+ if ( Saig_ObjIsPi(p->pAig, pObj) )
+ continue;
+ iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
+ assert( iGroupFirst <= iGrpPlace );
+ if ( iGroupFirst < iGrpPlace )
+ continue;
+ bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
+ bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
+ Cudd_RecursiveDeref( p->dd, bTemp );
+ }
+ Cudd_Deref( bRes );
+ p->dd->TimeStop = TimeStop;
+ return bRes;
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -271,17 +322,22 @@ DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
SeeAlso []
***********************************************************************/
-DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit )
+DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit, int fBackward )
{
int fCheckSupport = 0;
Llb_Grp_t * pGroup;
DdNode * bImage, * bGroup, * bCube, * bTemp;
- int i;
+ int k, Index;
bImage = bInit; Cudd_Ref( bImage );
- for ( i = 1; i < p->pMatrix->nCols-1; i++ )
+ for ( k = 1; k < p->pMatrix->nCols-1; k++ )
{
+ if ( fBackward )
+ Index = p->pMatrix->nCols - 1 - k;
+ else
+ Index = k;
+
// compute group BDD
- pGroup = p->pMatrix->pColGrps[i];
+ pGroup = p->pMatrix->pColGrps[Index];
bGroup = Llb_ManConstructGroupBdd( p, pGroup );
if ( bGroup == NULL )
{
@@ -290,7 +346,7 @@ DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit )
}
Cudd_Ref( bGroup );
// quantify variables appearing only in this group
- bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, i ); Cudd_Ref( bCube );
+ bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, Index, fBackward ); Cudd_Ref( bCube );
bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );
if ( bGroup == NULL )
{
@@ -302,7 +358,11 @@ DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit )
Cudd_RecursiveDeref( p->dd, bTemp );
Cudd_RecursiveDeref( p->dd, bCube );
// perform partial product
- bCube = Llb_ManConstructQuantCube( p, pGroup, i ); Cudd_Ref( bCube );
+ if ( fBackward )
+ bCube = Llb_ManConstructQuantCubeBwd( p, pGroup, Index );
+ else
+ bCube = Llb_ManConstructQuantCubeFwd( p, pGroup, Index );
+ Cudd_Ref( bCube );
// bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );
bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );
if ( bImage == NULL )
@@ -393,7 +453,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
/**Function*************************************************************
- Synopsis []
+ Synopsis [Perform reachability with hints and returns reached states in ppGlo.]
Description []
@@ -402,9 +462,106 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs
SeeAlso []
***********************************************************************/
-Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int iIter )
+Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p )
{
- return NULL;
+ Abc_Cex_t * pCex;
+ Aig_Obj_t * pObj;
+ DdNode * bState, * bImage, * bOneCube, * bTemp, * bRing;
+ int i, v, RetValue, nPiOffset;
+ char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
+ assert( Vec_PtrSize(p->vRings) > 0 );
+
+ p->dd->TimeStop = 0;
+ p->ddR->TimeStop = 0;
+
+/*
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ printf( "%d ", pObj->Id );
+ printf( "\n" );
+ Saig_ManForEachLi( p->pAig, pObj, i )
+ printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
+ printf( "\n" );
+*/
+ // allocate room for the counter-example
+ pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
+ pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
+ pCex->iPo = -1;
+
+ // get the last cube
+ bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
+ RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
+ Cudd_RecursiveDeref( p->ddR, bOneCube );
+ assert( RetValue );
+
+ // write PIs of counter-example
+ nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
+ Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+
+ // write state in terms of NS variables
+ if ( Vec_PtrSize(p->vRings) > 1 )
+ {
+ bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
+ }
+ // perform backward analysis
+ Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
+ {
+ if ( v == Vec_PtrSize(p->vRings) - 1 )
+ continue;
+//Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
+//Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
+ // compute the next states
+ bImage = Llb_ManComputeImage( p, bState, 1 );
+ assert( bImage != NULL );
+ Cudd_Ref( bImage );
+ Cudd_RecursiveDeref( p->dd, bState );
+//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
+
+ // move reached states into ring manager
+ bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
+ Cudd_RecursiveDeref( p->dd, bTemp );
+//Extra_bddPrintSupport( p->ddR, bImage ); printf( "\n" );
+
+ // intersect with the previous set
+ bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
+ Cudd_RecursiveDeref( p->ddR, bImage );
+
+ // find any assignment of the BDD
+ RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
+ Cudd_RecursiveDeref( p->ddR, bOneCube );
+ assert( RetValue );
+/*
+ for ( i = 0; i < p->ddR->size; i++ )
+ printf( "%d ", pValues[i] );
+ printf( "\n" );
+*/
+ // write PIs of counter-example
+ nPiOffset -= Saig_ManPiNum(p->pAig);
+ Saig_ManForEachPi( p->pAig, pObj, i )
+ if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
+ Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+
+ // check that we get the init state
+ if ( v == 0 )
+ {
+ Saig_ManForEachLo( p->pAig, pObj, i )
+ assert( pValues[i] == 0 );
+ break;
+ }
+
+ // write state in terms of NS variables
+ bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
+ }
+ assert( nPiOffset == Saig_ManRegNum(p->pAig) );
+ // update the output number
+//Abc_CexPrint( pCex );
+ RetValue = Saig_ManFindFailedPoCex( p->pAigGlo, pCex );
+ assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAigGlo) ); // invalid CEX!!!
+ pCex->iPo = RetValue;
+ // cleanup
+ ABC_FREE( pValues );
+ return pCex;
}
/**Function*************************************************************
@@ -420,12 +577,12 @@ Abc_Cex_t * Llb_ManDeriveCex( Llb_Man_t * p, DdNode * bInter, int iOutFail, int
***********************************************************************/
int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
{
- int fCheckOutputs = !p->pPars->fSkipOutCheck;
int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
+ int * pCs2Glo = Vec_IntArray( p->vCs2Glo );
int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
DdNode * bConstrCs, * bConstrNs;
- int clk2, clk = clock(), nIters, nBddSize = 0, iOutFail = -1;
+ int clk2, clk = clock(), nIters, nBddSize = 0;
int nThreshold = 10000;
// compute time to stop
@@ -440,7 +597,9 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
// start the managers
assert( p->dd == NULL );
assert( p->ddG == NULL );
+ assert( p->ddR == NULL );
p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+ p->ddR = Cudd_Init( Aig_ManPiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
if ( pddGlo && *pddGlo )
p->ddG = *pddGlo, *pddGlo = NULL;
else
@@ -450,16 +609,29 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
{
Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
+ Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
}
else
{
Cudd_AutodynDisable( p->dd );
Cudd_AutodynDisable( p->ddG );
+ Cudd_AutodynDisable( p->ddR );
}
// set the stop time parameter
p->dd->TimeStop = p->pPars->TimeTarget;
p->ddG->TimeStop = p->pPars->TimeTarget;
+ p->ddR->TimeStop = p->pPars->TimeTarget;
+
+ // create bad state in the ring manager
+ p->ddR->bFunc = Llb_BddComputeBad( p->pAigGlo, p->ddR, p->pPars->TimeTarget );
+ if ( p->ddR->bFunc == NULL )
+ {
+ if ( !p->pPars->fSilent )
+ printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+ return -1;
+ }
+ Cudd_Ref( p->ddR->bFunc );
// derive constraints
bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 ); Cudd_Ref( bConstrCs );
@@ -499,61 +671,58 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo
return -1;
}
- // check outputs
- if ( fCheckOutputs )
+ // save the onion ring
+ bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo );
+ if ( bTemp == NULL )
{
- Aig_Obj_t * pObj;
- int i;
- Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
- Aig_ManForEachPi( p->pAig, pObj, i )
- pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
- Aig_ManForEachPi( p->pAigGlo, pObj, i )
- pObj->pData = Aig_ManPi(p->pAig, i)->pData;
+ if ( !p->pPars->fSilent )
+ printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
+ p->pPars->iFrame = nIters - 1;
+ Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
+ Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
+ Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
+ Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
+ return -1;
+ }
+ Cudd_Ref( bTemp );
+ Vec_PtrPush( p->vRings, bTemp );
-//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
- for ( iOutFail = 0; iOutFail < Saig_ManPoNum(p->pAig); iOutFail++ )
- {
- DdNode * bFunc, * bInter;
- bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManPo(p->pAigGlo, iOutFail), p->dd ); Cudd_Ref( bFunc );
-//Extra_bddPrint( p->dd, bFunc ); printf( "\n" );
- if ( Cudd_bddLeq( p->dd, bCurrent, Cudd_Not(bFunc) ) ) // no cex
- {
- Cudd_RecursiveDeref( p->dd, bFunc );
- continue;
- }
- bInter = Cudd_bddIntersect( p->dd, bCurrent, bFunc ); Cudd_Ref( bInter );
- assert( p->pAig->pSeqModel == NULL );
- p->pAig->pSeqModel = Llb_ManDeriveCex( p, bInter, iOutFail, nIters );
- Cudd_RecursiveDeref( p->dd, bInter );
- Cudd_RecursiveDeref( p->dd, bFunc );
- break;
- }
- if ( iOutFail < Saig_ManPoNum(p->pAig) )
+ // check it for bad states
+ if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
+ {
+ assert( p->pAigGlo->pSeqModel == NULL );
+ if ( !p->pPars->fBackward )
+ p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p );
+ if ( !p->pPars->fSilent )
{
- if ( !p->pPars->fSilent )
- printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", iOutFail, nIters );
- Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
- Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
- p->pPars->iFrame = nIters;
- break;
+ if ( !p->pPars->fBackward )
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAigGlo->pSeqModel->iPo, nIters );
+ else
+ printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
+ Abc_PrintTime( 1, "Time", clock() - clk );
}
+ Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
+ Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
+ Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
+ Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
+ return 0;
}
// restrict reachable states using constraints
if ( vHints )
{
- bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent );
+ bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
}
// quantify variables appearing only in the init state
- bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0 ); Cudd_Ref( bCube );
- bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent );
+ bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 ); Cudd_Ref( bCube );
+ bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent );
Cudd_RecursiveDeref( p->dd, bTemp );
Cudd_RecursiveDeref( p->dd, bCube );
// compute the next states
- bNext = Llb_ManComputeImage( p, bCurrent );
+ bNext = Llb_ManComputeImage( p, bCurrent, 0 );
if ( bNext == NULL )
{
if ( !p->pPars->fSilent )
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 70578c47..6bca2adb 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -55,16 +55,20 @@ struct Llb_Man_t_
Aig_Man_t * pAig; // derived AIG manager (created in this package)
DdManager * dd; // BDD manager
DdManager * ddG; // BDD manager
+ DdManager * ddR; // BDD manager
Vec_Int_t * vObj2Var; // mapping AIG ObjId into BDD var index
Vec_Int_t * vVar2Obj; // mapping BDD var index into AIG ObjId
Vec_Ptr_t * vGroups; // group Id into group pointer
Llb_Mtr_t * pMatrix; // dependency matrix
// image computation
+ Vec_Ptr_t * vRings; // onion rings
Vec_Int_t * vVarBegs; // the first group where the var appears
Vec_Int_t * vVarEnds; // the last group where the var appears
// variable mapping
Vec_Int_t * vNs2Glo; // next state variables into global variables
+ Vec_Int_t * vCs2Glo; // next state variables into global variables
Vec_Int_t * vGlo2Cs; // global variables into current state variables
+ Vec_Int_t * vGlo2Ns; // global variables into current state variables
// flow computation
// Vec_Int_t * vMem;
// Vec_Ptr_t * vTops;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 14:46:41 +0000