diff options
Diffstat (limited to 'src/aig/llb')
-rw-r--r-- | src/aig/llb/llb2Bad.c | 2 | ||||
-rw-r--r-- | src/aig/llb/llb2Core.c | 3 | ||||
-rw-r--r-- | src/aig/llb/llb2Dump.c | 2 | ||||
-rw-r--r-- | src/aig/llb/llb2Flow.c | 14 | ||||
-rw-r--r-- | src/aig/llb/llb3Nonlin.c | 3 | ||||
-rw-r--r-- | src/aig/llb/llbInt.h | 2 |
6 files changed, 13 insertions, 13 deletions
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c index 88ff4c75..8e2a37ff 100644 --- a/src/aig/llb/llb2Bad.c +++ b/src/aig/llb/llb2Bad.c @@ -87,7 +87,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) { if ( !Aig_ObjIsNode(pObj) ) continue; - Cudd_RecursiveDeref( dd, pObj->pData ); + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); } Vec_PtrFree( vNodes ); Cudd_Deref( bResult ); diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c index 7fa361b9..596a34af 100644 --- a/src/aig/llb/llb2Core.c +++ b/src/aig/llb/llb2Core.c @@ -95,7 +95,6 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) { extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); - extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Ptr_t * vSupps, * vQuant0, * vQuant1; @@ -118,7 +117,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p ) pCex->iPo = -1; // get the last cube - bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube ); + 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 ); diff --git a/src/aig/llb/llb2Dump.c b/src/aig/llb/llb2Dump.c index 55f94907..3e1dd8c5 100644 --- a/src/aig/llb/llb2Dump.c +++ b/src/aig/llb/llb2Dump.c @@ -83,7 +83,7 @@ void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char // write the file pFile = fopen( pFileName, "wb" ); - Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile ); + Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 ); fclose( pFile ); // cleanup diff --git a/src/aig/llb/llb2Flow.c b/src/aig/llb/llb2Flow.c index 36b3ff1b..1b177807 100644 --- a/src/aig/llb/llb2Flow.c +++ b/src/aig/llb/llb2Flow.c @@ -144,7 +144,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp continue; if ( piFirst[i] == piLast[i] ) { - vMap = Vec_PtrEntry( vMaps, piFirst[i] ); + vMap = (Vec_Int_t *)Vec_PtrEntry( vMaps, piFirst[i] ); Vec_IntWriteEntry( vMap, pObj->Id, 2 ); continue; } @@ -152,7 +152,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp // set support for all in between for ( k = piFirst[i]; k <= piLast[i]; k++ ) { - vMap = Vec_PtrEntry( vMaps, k ); + vMap = (Vec_Int_t *)Vec_PtrEntry( vMaps, k ); Vec_IntWriteEntry( vMap, pObj->Id, 1 ); } } @@ -165,8 +165,8 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp printf( "%d ", Counter ); Vec_PtrForEachEntryStart( Vec_Int_t *, vMaps, vMap, i, 1 ) { - vPrev = Vec_PtrEntry( vMaps, i-1 ); - vNext = (i == Vec_PtrSize(vMaps)-1)? NULL: Vec_PtrEntry( vMaps, i+1 ); + vPrev = (Vec_Int_t *)Vec_PtrEntry( vMaps, i-1 ); + vNext = (i == Vec_PtrSize(vMaps)-1)? NULL: (Vec_Int_t *)Vec_PtrEntry( vMaps, i+1 ); CounterPlus = CounterMinus = 0; Aig_ManForEachObj( p, pObj, k ) @@ -1134,7 +1134,7 @@ void Llb_ManFlowGetObjSet( Aig_Man_t * p, Vec_Ptr_t * vLower, int iStart, int nS Vec_PtrClear( vSet ); for ( i = 0; i < nSize; i++ ) { - pObj = Vec_PtrEntry( vLower, (iStart + i) % Vec_PtrSize(vLower) ); + pObj = (Aig_Obj_t *)Vec_PtrEntry( vLower, (iStart + i) % Vec_PtrSize(vLower) ); Vec_PtrPush( vSet, pObj ); } } @@ -1334,7 +1334,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num ) { extern void Llb_BddConstructTest( Aig_Man_t * p, Vec_Ptr_t * vResult ); extern void Llb_BddExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, Vec_Ptr_t * vMaps ); - extern void Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult ); + int fVerbose = 1; Gia_ParLlb_t Pars, * pPars = &Pars; @@ -1354,7 +1354,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num ) // vMaps = Llb_ManCutMap( p, vResult, vSupps ); // Llb_BddExperiment( pAig, p, pPars, vResult, vMaps ); - Llb_CoreExperiment( pAig, p, pPars, vResult ); + Llb_CoreExperiment( pAig, p, pPars, vResult, 0 ); // Vec_VecFree( (Vec_Vec_t *)vMaps ); // Vec_VecFree( (Vec_Vec_t *)vSupps ); diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c index adab5b0b..e52e28ca 100644 --- a/src/aig/llb/llb3Nonlin.c +++ b/src/aig/llb/llb3Nonlin.c @@ -238,7 +238,6 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ) Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) { extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames ); - extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p ); Abc_Cex_t * pCex; Aig_Obj_t * pObj; Vec_Int_t * vVarsNs; @@ -269,7 +268,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p ) pCex->iPo = -1; // get the last cube - bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube ); + 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 ); diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 3ee1f5c2..70578c47 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -29,6 +29,7 @@ #include <stdio.h> #include "aig.h" #include "saig.h" +#include "ssw.h" #include "cuddInt.h" #include "extra.h" #include "llb.h" @@ -150,6 +151,7 @@ extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ); /*=== llb2Core.c ======================================================*/ extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues ); +extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ); /*=== llb2Driver.c ======================================================*/ extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p ); extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs ); |