Skip to content
Projects
Groups
Snippets
Help
This project
Loading...
Sign in / Register
Toggle navigation
A
abc
Overview
Overview
Details
Activity
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Board
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
lvzhengyang
abc
Commits
686d38d6
Commit
686d38d6
authored
Feb 13, 2011
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Changes to enable C++ compilation after recent modifications.
parent
8acd4edd
Hide whitespace changes
Inline
Side-by-side
Showing
20 changed files
with
58 additions
and
96 deletions
+58
-96
src/aig/aig/aigDoms.c
+4
-4
src/aig/llb/llb2Bad.c
+1
-1
src/aig/llb/llb2Core.c
+1
-2
src/aig/llb/llb2Dump.c
+1
-1
src/aig/llb/llb2Flow.c
+7
-7
src/aig/llb/llb3Nonlin.c
+1
-2
src/aig/llb/llbInt.h
+2
-0
src/aig/saig/saigDup.c
+1
-1
src/aig/saig/saigTempor.c
+2
-2
src/aig/ssw/sswInt.h
+1
-0
src/aig/ssw/sswSweep.c
+0
-1
src/base/cmd/cmd.h
+2
-0
src/base/cmd/cmdLoad.c
+0
-2
src/misc/extra/extra.h
+1
-1
src/misc/hash/hashGen.h
+2
-2
src/misc/util/utilSignal.c
+6
-5
src/misc/util/utilSignal.h
+16
-22
src/misc/util/util_hack.h
+7
-40
src/sat/pdr/pdrInv.c
+1
-1
src/sat/pdr/pdrMan.c
+2
-2
No files found.
src/aig/aig/aigDoms.c
View file @
686d38d6
...
...
@@ -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
);
...
...
src/aig/llb/llb2Bad.c
View file @
686d38d6
...
...
@@ -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
);
...
...
src/aig/llb/llb2Core.c
View file @
686d38d6
...
...
@@ -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
);
...
...
src/aig/llb/llb2Dump.c
View file @
686d38d6
...
...
@@ -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
...
...
src/aig/llb/llb2Flow.c
View file @
686d38d6
...
...
@@ -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 );
...
...
src/aig/llb/llb3Nonlin.c
View file @
686d38d6
...
...
@@ -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
);
...
...
src/aig/llb/llbInt.h
View file @
686d38d6
...
...
@@ -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
);
...
...
src/aig/saig/saigDup.c
View file @
686d38d6
...
...
@@ -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
);
}
...
...
src/aig/saig/saigTempor.c
View file @
686d38d6
...
...
@@ -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
...
...
src/aig/ssw/sswInt.h
View file @
686d38d6
...
...
@@ -29,6 +29,7 @@
#include "saig.h"
#include "satSolver.h"
#include "ssw.h"
#include "ioa.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
...
...
src/aig/ssw/sswSweep.c
View file @
686d38d6
...
...
@@ -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
;
...
...
src/base/cmd/cmd.h
View file @
686d38d6
...
...
@@ -60,6 +60,8 @@ extern void Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, const char * key );
extern
void
Cmd_FlagUpdateValue
(
Abc_Frame_t
*
pAbc
,
const
char
*
key
,
char
*
value
);
/*=== cmdHist.c ========================================================*/
extern
void
Cmd_HistoryAddCommand
(
Abc_Frame_t
*
pAbc
,
const
char
*
command
);
/*=== cmdLoad.c ========================================================*/
extern
int
CmdCommandLoad
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
...
...
src/base/cmd/cmdLoad.c
View file @
686d38d6
...
...
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static
int
CmdCommandLoad
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
);
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
...
...
src/misc/extra/extra.h
View file @
686d38d6
...
...
@@ -611,7 +611,7 @@ extern char * Extra_UtilTildeExpand( char *fname );
extern
char
*
Extra_UtilFileSearch
(
char
*
file
,
char
*
path
,
char
*
mode
);
extern
void
(
*
Extra_UtilMMoutOfMemory
)(
long
size
);
extern
const
char
*
globalUtilOptarg
;
extern
const
char
*
globalUtilOptarg
;
extern
int
globalUtilOptind
;
/**AutomaticEnd***************************************************************/
...
...
src/misc/hash/hashGen.h
View file @
686d38d6
...
...
@@ -229,7 +229,7 @@ static inline void Hash_GenWriteEntry( Hash_Gen_t *p, void * key, void * data )
p
->
nSize
++
;
(
*
pLast
)
=
pEntry
=
ABC_ALLOC
(
Hash_Gen_Entry_t
,
1
);
pEntry
->
pNext
=
NULL
;
pEntry
->
key
=
key
;
pEntry
->
key
=
(
char
*
)
key
;
pEntry
->
data
=
data
;
return
;
...
...
@@ -271,7 +271,7 @@ static inline Hash_Gen_Entry_t * Hash_GenEntry( Hash_Gen_t *p, void * key, int f
p
->
nSize
++
;
(
*
pLast
)
=
pEntry
=
ABC_ALLOC
(
Hash_Gen_Entry_t
,
1
);
pEntry
->
pNext
=
NULL
;
pEntry
->
key
=
key
;
pEntry
->
key
=
(
char
*
)
key
;
pEntry
->
data
=
NULL
;
return
pEntry
;
}
...
...
src/misc/util/utilSignal.c
View file @
686d38d6
...
...
@@ -4,17 +4,17 @@
SystemName [ABC: Logic synthesis and verification system.]
PackageName []
PackageName [
Signal handling utilities.
]
Synopsis []
Synopsis [
Signal handling utilities.
]
Author []
Author [
Baruch Sterin
]
Affiliation [UC Berkeley]
Date []
Date [
Ver. 1.0. Started - February 1, 2011.
]
Revision []
Revision [
$Id: utilSignal.c,v 1.00 2011/02/01 00:00:00 alanmi Exp $
]
***********************************************************************/
...
...
@@ -23,6 +23,7 @@
#include <signal.h>
#include "abc_global.h"
#include "hashGen.h"
#include "utilSignal.h"
#ifndef _MSC_VER
...
...
src/misc/util/utilSignal.h
View file @
686d38d6
...
...
@@ -4,17 +4,17 @@
SystemName [ABC: Logic synthesis and verification system.]
PackageName []
PackageName [
Signal handling utilities.
]
Synopsis []
Synopsis [
Signal handling utilities.
]
Author []
Author [
Baruch Sterin
]
Affiliation [UC Berkeley]
Date []
Date [
Ver. 1.0. Started - February 1, 2011.
]
Revision []
Revision [
$Id: utilSignal.h,v 1.00 2011/02/01 00:00:00 alanmi Exp $
]
***********************************************************************/
...
...
@@ -44,23 +44,17 @@ ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/*=== utilSignal.c ==========================================================*/
void
Util_SignalCleanup
();
void
Util_SignalStartHandler
();
void
Util_SignalResetHandler
();
void
Util_SignalStopHandler
();
void
Util_SignalBlockSignals
();
void
Util_SignalUnblockSignals
();
void
Util_SignalAddChildPid
(
int
pid
);
void
Util_SignalRemoveChildPid
(
int
pid
);
int
Util_SignalTmpFile
(
const
char
*
prefix
,
const
char
*
suffix
,
char
**
out_name
);
void
Util_SignalTmpFileRemove
(
const
char
*
fname
,
int
fLeave
);
int
Util_SignalSystem
(
const
char
*
cmd
);
extern
void
Util_SignalCleanup
();
extern
void
Util_SignalStartHandler
();
extern
void
Util_SignalResetHandler
();
extern
void
Util_SignalStopHandler
();
extern
void
Util_SignalBlockSignals
();
extern
void
Util_SignalUnblockSignals
();
extern
void
Util_SignalAddChildPid
(
int
pid
);
extern
void
Util_SignalRemoveChildPid
(
int
pid
);
extern
int
Util_SignalTmpFile
(
const
char
*
prefix
,
const
char
*
suffix
,
char
**
out_name
);
extern
void
Util_SignalTmpFileRemove
(
const
char
*
fname
,
int
fLeave
);
extern
int
Util_SignalSystem
(
const
char
*
cmd
);
ABC_NAMESPACE_HEADER_END
...
...
src/misc/util/util_hack.h
View file @
686d38d6
...
...
@@ -21,7 +21,6 @@
#ifndef __UTIL_HACK_H__
#define __UTIL_HACK_H__
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
...
...
@@ -31,50 +30,18 @@
#include "abc_global.h"
ABC_NAMESPACE_HEADER_START
#define NIL(type) ((type *) 0)
#ifndef EXTERN
#define EXTERN extern
#endif
#define NIL(type) ((type *) 0)
#define random rand
#define srandom srand
#define util_cpu_time Extra_CpuTime
#define getSoftDataLimit Extra_GetSoftDataLimit
#define util_getopt_reset Extra_UtilGetoptReset
#define util_getopt Extra_UtilGetopt
#define util_print_time Extra_UtilPrintTime
#define util_strsav Extra_UtilStrsav
#define util_tilde_expand Extra_UtilTildeExpand
#define util_file_search Extra_UtilFileSearch
#define MMoutOfMemory Extra_UtilMMoutOfMemory
#define util_optarg globalUtilOptarg
#define util_optind globalUtilOptind
#ifndef ARGS
#define ARGS(protos) protos
#endif
extern
long
Extra_CpuTime
();
extern
int
Extra_GetSoftDataLimit
();
extern
void
Extra_UtilGetoptReset
();
extern
int
Extra_UtilGetopt
(
int
argc
,
char
*
argv
[],
const
char
*
optstring
);
extern
char
*
Extra_UtilPrintTime
(
long
t
);
extern
char
*
Extra_UtilStrsav
(
char
*
s
);
extern
char
*
Extra_UtilTildeExpand
(
char
*
fname
);
extern
char
*
Extra_UtilFileSearch
(
char
*
file
,
char
*
path
,
char
*
mode
);
extern
char
*
globalUtilOptarg
;
extern
int
globalUtilOptind
;
#define util_cpu_time Extra_CpuTime
#define getSoftDataLimit Extra_GetSoftDataLimit
#define MMoutOfMemory Extra_UtilMMoutOfMemory
extern
long
Extra_CpuTime
();
extern
int
Extra_GetSoftDataLimit
();
extern
void
(
*
Extra_UtilMMoutOfMemory
)(
long
size
);
ABC_NAMESPACE_HEADER_END
#endif
src/sat/pdr/pdrInv.c
View file @
686d38d6
...
...
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
#include "extra.h"
ABC_NAMESPACE_IMPL_START
...
...
@@ -44,7 +45,6 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void
Pdr_ManPrintProgress
(
Pdr_Man_t
*
p
,
int
fClose
,
int
Time
)
{
extern
int
Extra_Base10Log
(
unsigned
int
Num
);
static
int
PastSize
;
Vec_Ptr_t
*
vVec
;
int
i
,
ThisSize
,
Length
,
LengthStart
;
...
...
src/sat/pdr/pdrMan.c
View file @
686d38d6
...
...
@@ -19,6 +19,7 @@
***********************************************************************/
#include "pdrInt.h"
#include "ssw.h"
ABC_NAMESPACE_IMPL_START
...
...
@@ -157,7 +158,6 @@ void Pdr_ManStop( Pdr_Man_t * p )
***********************************************************************/
Abc_Cex_t
*
Pdr_ManDeriveCex
(
Pdr_Man_t
*
p
)
{
extern
Abc_Cex_t
*
Gia_ManAllocCounterExample
(
int
nRegs
,
int
nRealPis
,
int
nFrames
);
Abc_Cex_t
*
pCex
;
Pdr_Obl_t
*
pObl
;
int
i
,
f
,
Lit
,
nFrames
=
0
;
...
...
@@ -165,7 +165,7 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
for
(
pObl
=
p
->
pQueue
;
pObl
;
pObl
=
pObl
->
pNext
)
nFrames
++
;
// create the counter-example
pCex
=
Gia_Man
AllocCounterExample
(
Aig_ManRegNum
(
p
->
pAig
),
Saig_ManPiNum
(
p
->
pAig
),
nFrames
);
pCex
=
Ssw_Sml
AllocCounterExample
(
Aig_ManRegNum
(
p
->
pAig
),
Saig_ManPiNum
(
p
->
pAig
),
nFrames
);
pCex
->
iPo
=
(
p
->
pPars
->
iOutput
==-
1
)
?
0
:
p
->
pPars
->
iOutput
;
pCex
->
iFrame
=
nFrames
-
1
;
for
(
pObl
=
p
->
pQueue
,
f
=
0
;
pObl
;
pObl
=
pObl
->
pNext
,
f
++
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment