summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/aig/aigDoms.c8
-rw-r--r--src/aig/llb/llb2Bad.c2
-rw-r--r--src/aig/llb/llb2Core.c3
-rw-r--r--src/aig/llb/llb2Dump.c2
-rw-r--r--src/aig/llb/llb2Flow.c14
-rw-r--r--src/aig/llb/llb3Nonlin.c3
-rw-r--r--src/aig/llb/llbInt.h2
-rw-r--r--src/aig/saig/saigDup.c2
-rw-r--r--src/aig/saig/saigTempor.c4
-rw-r--r--src/aig/ssw/sswInt.h1
-rw-r--r--src/aig/ssw/sswSweep.c1
11 files changed, 21 insertions, 21 deletions
diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c
index c12c0caa..7097a34a 100644
--- a/src/aig/aig/aigDoms.c
+++ b/src/aig/aig/aigDoms.c
@@ -547,11 +547,11 @@ void Aig_ObjDomCompute( Aig_Sto_t * pSto, Aig_Obj_t * pObj )
Vec_IntPush( pSto->vFans, iFanout>>1 );
if ( Vec_IntSize(pSto->vFans) == 0 )
return;
- vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(pSto->vFans, 0) );
+ vDoms0 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(pSto->vFans, 0) );
vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 0 );
Vec_IntForEachEntryStart( pSto->vFans, iFanout, i, 1 )
{
- vDoms1 = Vec_PtrEntry( pSto->vDoms, iFanout );
+ vDoms1 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, iFanout );
vDoms2 = Aig_ObjDomMerge( pSto, vDomsT = vDoms2, vDoms1 );
Aig_ObjDomVecRecycle( pSto, vDomsT );
}
@@ -662,11 +662,11 @@ Vec_Ptr_t * Aig_ObjDomCollect( Aig_Sto_t * pSto, Vec_Int_t * vCut )
{
Vec_Ptr_t * vDoms0, * vDoms1, * vDoms2;
int i, ObjId;
- vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(vCut, 0) );
+ vDoms0 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(vCut, 0) );
vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 1 );
Vec_IntForEachEntryStart( vCut, ObjId, i, 1 )
{
- vDoms1 = Vec_PtrEntry( pSto->vDoms, ObjId );
+ vDoms1 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, ObjId );
if ( vDoms1 == NULL )
continue;
Aig_ObjDomUnion( pSto, vDoms2, vDoms1 );
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 );
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 4d34224e..f4e557f8 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -115,7 +115,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
{
pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
- pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData );
+ pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
Aig_ObjCreatePo( pAigNew, pMiter );
}
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 74f4a9d3..962a81de 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -69,7 +69,7 @@ Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
}
// create POs for the flop inputs
Saig_ManForEachLi( pAig, pObj, i )
- Aig_ObjCreatePo( pFrames, pObj->pData );
+ Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObj->pData );
Aig_ManCleanup( pFrames );
return pFrames;
}
@@ -123,7 +123,7 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
// create flop output values
Saig_ManForEachLo( pAig, pObj, i )
- pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), Aig_ManPo(pFrames, i)->pData );
+ pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), (Aig_Obj_t *)Aig_ManPo(pFrames, i)->pData );
Aig_ManStop( pFrames );
// add internal nodes of this frame
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index ad868c6e..189494bc 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -29,6 +29,7 @@
#include "saig.h"
#include "satSolver.h"
#include "ssw.h"
+#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 40121e42..edae0846 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -331,7 +331,6 @@ p->timeBmc += clock() - clk;
***********************************************************************/
void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
{
- extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
FILE * pFile;
char pBuffer[16];
Aig_Man_t * pNew;
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-15 06:32:09 +0000