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
23879f92
Commit
23879f92
authored
Sep 05, 2013
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Unifying parameters for the &ps command.
parent
9d14b0c0
Hide whitespace changes
Inline
Side-by-side
Showing
21 changed files
with
68 additions
and
55 deletions
+68
-55
src/aig/gia/gia.h
+10
-1
src/aig/gia/giaCof.c
+2
-2
src/aig/gia/giaEquiv.c
+1
-1
src/aig/gia/giaFrames.c
+1
-1
src/aig/gia/giaIso.c
+1
-1
src/aig/gia/giaMan.c
+7
-6
src/aig/gia/giaMuxes.c
+3
-3
src/aig/gia/giaSweeper.c
+1
-1
src/base/abc/abcHieCec.c
+3
-3
src/base/abci/abc.c
+15
-12
src/misc/util/utilBridge.c
+1
-1
src/proof/abs/absRpmOld.c
+5
-5
src/proof/cec/cecCore.c
+1
-1
src/proof/ssc/sscCore.c
+2
-2
src/proof/ssc/sscUtil.c
+3
-3
src/sat/bmc/bmcBmcAnd.c
+1
-1
src/sat/bmc/bmcCexDepth.c
+4
-4
src/sat/bmc/bmcCexMin2.c
+2
-2
src/sat/bmc/bmcCexTools.c
+2
-2
src/sat/bmc/bmcUnroll.c
+2
-2
src/sat/bsat/satSolver2i.c
+1
-1
No files found.
src/aig/gia/gia.h
View file @
23879f92
...
...
@@ -181,6 +181,15 @@ struct Gia_Man_t_
typedef
struct
Gps_Par_t_
Gps_Par_t
;
struct
Gps_Par_t_
{
int
fTents
;
int
fSwitch
;
int
fCut
;
int
fNpn
;
};
typedef
struct
Emb_Par_t_
Emb_Par_t
;
struct
Emb_Par_t_
{
...
...
@@ -1019,7 +1028,7 @@ extern Gia_Man_t * Gia_ManStart( int nObjsMax );
extern
void
Gia_ManStop
(
Gia_Man_t
*
p
);
extern
void
Gia_ManStopP
(
Gia_Man_t
**
p
);
extern
float
Gia_ManMemory
(
Gia_Man_t
*
p
);
extern
void
Gia_ManPrintStats
(
Gia_Man_t
*
p
,
int
fTents
,
int
fSwitch
,
int
fCut
);
extern
void
Gia_ManPrintStats
(
Gia_Man_t
*
p
,
Gps_Par_t
*
pPars
);
extern
void
Gia_ManPrintStatsShort
(
Gia_Man_t
*
p
);
extern
void
Gia_ManPrintMiterStatus
(
Gia_Man_t
*
p
);
extern
void
Gia_ManSetRegNum
(
Gia_Man_t
*
p
,
int
nRegs
);
...
...
src/aig/gia/giaCof.c
View file @
23879f92
...
...
@@ -863,7 +863,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
if
(
fVerbose
)
{
printf
(
"Cofactoring %d signals.
\n
"
,
Vec_IntSize
(
vSigs
)
);
Gia_ManPrintStats
(
p
,
0
,
0
,
0
);
Gia_ManPrintStats
(
p
,
NULL
);
}
if
(
Vec_IntSize
(
vSigs
)
>
200
)
{
...
...
@@ -889,7 +889,7 @@ Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs, int fVerbose
if
(
fVerbose
)
printf
(
"Cofactored variable %d.
\n
"
,
iVar
);
if
(
fVerbose
)
Gia_ManPrintStats
(
pAig
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pAig
,
NULL
);
}
Vec_IntFree
(
vSigsNew
);
return
pAig
;
...
...
src/aig/gia/giaEquiv.c
View file @
23879f92
...
...
@@ -1773,7 +1773,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
}
// (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
Gia_ManCleanMark0
(
pGia
);
Gia_ManPrintStats
(
pGia
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pGia
,
NULL
);
for
(
nIter
=
0
;
;
nIter
++
)
{
if
(
Gia_ManHasNoEquivs
(
pGia
)
)
...
...
src/aig/gia/giaFrames.c
View file @
23879f92
...
...
@@ -956,7 +956,7 @@ Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbos
if
(
fVerbose
&&
(
f
%
100
==
0
)
)
{
printf
(
"%6d : "
,
f
);
Gia_ManPrintStats
(
pFrames
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pFrames
,
NULL
);
}
Gia_ManForEachRo
(
pAig
,
pObj
,
i
)
pObj
->
Value
=
f
?
Gia_ObjRoToRi
(
pAig
,
pObj
)
->
Value
:
0
;
...
...
src/aig/gia/giaIso.c
View file @
23879f92
...
...
@@ -1139,7 +1139,7 @@ Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_P
iPo
=
Vec_IntEntry
(
vLevel
,
0
);
printf
(
"%6d %6d %6d : "
,
i
,
Vec_IntSize
(
vLevel
),
iPo
);
pPart
=
Gia_ManDupCones
(
p
,
&
iPo
,
1
,
1
);
Gia_ManPrintStats
(
pPart
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pPart
,
NULL
);
Gia_ManStop
(
pPart
);
}
...
...
src/aig/gia/giaMan.c
View file @
23879f92
...
...
@@ -326,7 +326,7 @@ void Gia_ManPrintChoiceStats( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void
Gia_ManPrintStats
(
Gia_Man_t
*
p
,
int
fTents
,
int
fSwitch
,
int
fCut
)
void
Gia_ManPrintStats
(
Gia_Man_t
*
p
,
Gps_Par_t
*
pPars
)
{
if
(
p
->
pName
)
printf
(
"%-8s : "
,
p
->
pName
);
...
...
@@ -337,13 +337,12 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut )
printf
(
" ff =%7d"
,
Gia_ManRegNum
(
p
)
);
printf
(
" and =%8d"
,
Gia_ManAndNum
(
p
)
);
printf
(
" lev =%5d"
,
Gia_ManLevelNum
(
p
)
);
Vec_IntFreeP
(
&
p
->
vLevels
);
if
(
fCut
)
if
(
pPars
&&
pPars
->
fCut
)
printf
(
" cut = %d(%d)"
,
Gia_ManCrossCut
(
p
,
0
),
Gia_ManCrossCut
(
p
,
1
)
);
// printf( " mem =%5.2f MB", 1.0*(sizeof(Gia_Obj_t)*p->nObjs + sizeof(int)*(Vec_IntSize(p->vCis) + Vec_IntSize(p->vCos)))/(1<<20) );
printf
(
" mem =%5.2f MB"
,
1
.
0
*
(
sizeof
(
Gia_Obj_t
)
*
p
->
nObjsAlloc
+
sizeof
(
int
)
*
(
Vec_IntCap
(
p
->
vCis
)
+
Vec_IntCap
(
p
->
vCos
)))
/
(
1
<<
20
)
);
printf
(
" mem =%5.2f MB"
,
Gia_ManMemory
(
p
)
);
if
(
Gia_ManHasDangling
(
p
)
)
printf
(
" ch =%5d"
,
Gia_ManEquivCountClasses
(
p
)
);
if
(
fSwitch
)
if
(
pPars
&&
pPars
->
fSwitch
)
{
if
(
p
->
pSwitching
)
printf
(
" power =%7.2f"
,
Gia_ManEvaluateSwitching
(
p
)
);
...
...
@@ -360,6 +359,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut )
Gia_ManPrintChoiceStats
(
p
);
if
(
Gia_ManHasMapping
(
p
)
)
Gia_ManPrintMappingStats
(
p
);
if
(
pPars
&&
pPars
->
fNpn
&&
Gia_ManHasMapping
(
p
)
&&
Gia_ManLutSizeMax
(
p
)
<=
4
)
Gia_ManPrintNpnClasses
(
p
);
if
(
p
->
vPacking
)
Gia_ManPrintPackingStats
(
p
);
if
(
p
->
pPlacement
)
...
...
@@ -370,7 +371,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut )
Gia_ManPrintFlopClasses
(
p
);
Gia_ManPrintGateClasses
(
p
);
Gia_ManPrintObjClasses
(
p
);
if
(
fTents
)
if
(
pPars
&&
pPars
->
fTents
)
{
/*
int k, Entry, Prev = 1;
...
...
src/aig/gia/giaMuxes.c
View file @
23879f92
...
...
@@ -147,9 +147,9 @@ Gia_Man_t * Gia_ManDupMuxesTest( Gia_Man_t * p )
Gia_Man_t
*
pNew
,
*
pNew2
;
pNew
=
Gia_ManDupMuxes
(
p
);
pNew2
=
Gia_ManDupNoMuxes
(
pNew
);
Gia_ManPrintStats
(
p
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew2
,
0
,
0
,
0
);
Gia_ManPrintStats
(
p
,
NULL
);
Gia_ManPrintStats
(
pNew
,
NULL
);
Gia_ManPrintStats
(
pNew2
,
NULL
);
Gia_ManStop
(
pNew
);
// Gia_ManStop( pNew2 );
return
pNew2
;
...
...
src/aig/gia/giaSweeper.c
View file @
23879f92
...
...
@@ -213,7 +213,7 @@ void Gia_SweeperPrintStats( Gia_Man_t * pGia )
ABC_PRTP
(
" Undecided "
,
p
->
timeSatUndec
,
p
->
timeTotal
);
ABC_PRTP
(
"TOTAL RUNTIME "
,
p
->
timeTotal
,
p
->
timeTotal
);
printf
(
"GIA: "
);
Gia_ManPrintStats
(
pGia
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pGia
,
NULL
);
printf
(
"SAT calls = %d. Sat = %d. Unsat = %d. Undecided = %d. Proofs = %d.
\n
"
,
p
->
nSatCalls
,
p
->
nSatCallsSat
,
p
->
nSatCallsUnsat
,
p
->
nSatCallsUndec
,
p
->
nSatProofs
);
Sat_SolverPrintStats
(
stdout
,
p
->
pSat
);
...
...
src/base/abc/abcHieCec.c
View file @
23879f92
...
...
@@ -404,7 +404,7 @@ Gia_Man_t * Abc_NtkDeriveFlatGia2Derive( Abc_Ntk_t * pNtk, Vec_Ptr_t * vOrder )
Gia_ManStop
(
pGiaBox
);
printf
(
"%8d -> "
,
Abc_NtkCountAndNodes
(
vOrder
)
);
Gia_ManPrintStats
(
pGia
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pGia
,
NULL
);
return
pGia
;
}
/*
...
...
@@ -724,7 +724,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
clk
=
Abc_Clock
();
pGia
=
Abc_NtkDeriveFlatGia2
(
pNtk
,
vOrder
);
Abc_PrintTime
(
1
,
"Deriving GIA"
,
Abc_Clock
()
-
clk
);
Gia_ManPrintStats
(
pGia
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pGia
,
NULL
);
// Gia_ManStop( pGia );
Vec_PtrFree
(
vOrder
);
...
...
@@ -740,7 +740,7 @@ Gia_Man_t * Abc_NtkHieCecTest( char * pFileName, int fVerbose )
clk
=
Abc_Clock
();
pGia
=
Abc_NtkDeriveFlatGia
(
pNtk
);
Abc_PrintTime
(
1
,
"Deriving GIA"
,
Abc_Clock
()
-
clk
);
Gia_ManPrintStats
(
pGia
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pGia
,
NULL
);
// clean nodes/boxes of all nodes
Vec_PtrForEachEntry
(
Abc_Ntk_t
*
,
vMods
,
pModel
,
i
)
...
...
src/base/abci/abc.c
View file @
23879f92
...
...
@@ -25260,23 +25260,25 @@ usage:
***********************************************************************/
int
Abc_CommandAbc9Ps
(
Abc_Frame_t
*
pAbc
,
int
argc
,
char
**
argv
)
{
Gps_Par_t
Pars
,
*
pPars
=
&
Pars
;
int
c
;
int
fTents
=
0
;
int
fSwitch
=
0
;
int
fCut
=
0
;
memset
(
pPars
,
0
,
sizeof
(
Gps_Par_t
)
);
Extra_UtilGetoptReset
();
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"tpch"
)
)
!=
EOF
)
while
(
(
c
=
Extra_UtilGetopt
(
argc
,
argv
,
"tpc
n
h"
)
)
!=
EOF
)
{
switch
(
c
)
{
case
't'
:
fTents
^=
1
;
pPars
->
fTents
^=
1
;
break
;
case
'p'
:
fSwitch
^=
1
;
pPars
->
fSwitch
^=
1
;
break
;
case
'c'
:
fCut
^=
1
;
pPars
->
fCut
^=
1
;
break
;
case
'n'
:
pPars
->
fNpn
^=
1
;
break
;
case
'h'
:
goto
usage
;
...
...
@@ -25289,15 +25291,16 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print
(
-
1
,
"Abc_CommandAbc9Ps(): There is no AIG.
\n
"
);
return
1
;
}
Gia_ManPrintStats
(
pAbc
->
pGia
,
fTents
,
fSwitch
,
fCut
);
Gia_ManPrintStats
(
pAbc
->
pGia
,
pPars
);
return
0
;
usage:
Abc_Print
(
-
2
,
"usage: &ps [-tpch]
\n
"
);
Abc_Print
(
-
2
,
"usage: &ps [-tpc
n
h]
\n
"
);
Abc_Print
(
-
2
,
"
\t
prints stats of the current AIG
\n
"
);
Abc_Print
(
-
2
,
"
\t
-t : toggle printing BMC tents [default = %s]
\n
"
,
fTents
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-p : toggle printing switching activity [default = %s]
\n
"
,
fSwitch
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-c : toggle printing the size of frontier cut [default = %s]
\n
"
,
fCut
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-t : toggle printing BMC tents [default = %s]
\n
"
,
pPars
->
fTents
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-p : toggle printing switching activity [default = %s]
\n
"
,
pPars
->
fSwitch
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-c : toggle printing the size of frontier cut [default = %s]
\n
"
,
pPars
->
fCut
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-n : toggle printing NPN classes of functions [default = %s]
\n
"
,
pPars
->
fNpn
?
"yes"
:
"no"
);
Abc_Print
(
-
2
,
"
\t
-h : print the command usage
\n
"
);
return
1
;
}
src/misc/util/utilBridge.c
View file @
23879f92
...
...
@@ -501,7 +501,7 @@ void Gia_ManFromBridgeTest( char * pFileName )
p
=
Gia_ManFromBridge
(
pFile
,
NULL
);
fclose
(
pFile
);
Gia_ManPrintStats
(
p
,
0
,
0
,
0
);
Gia_ManPrintStats
(
p
,
NULL
);
Gia_AigerWrite
(
p
,
"temp.aig"
,
0
,
0
);
Gia_ManToBridgeAbsNetlistTest
(
"par_.dump"
,
p
,
BRIDGE_ABS_NETLIST
);
...
...
src/proof/abs/absRpmOld.c
View file @
23879f92
...
...
@@ -147,7 +147,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
if
(
fVerbose
)
{
printf
(
"Original AIG:
\n
"
);
Gia_ManPrintStats
(
p
,
0
,
0
,
0
);
Gia_ManPrintStats
(
p
,
NULL
);
}
// perform input trimming
...
...
@@ -155,7 +155,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
if
(
fVerbose
)
{
printf
(
"After PI trimming:
\n
"
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
}
// transform GIA
pNew
=
Gia_ManDupIn2Ff
(
pTmp
=
pNew
);
...
...
@@ -163,7 +163,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
if
(
fVerbose
)
{
printf
(
"After PI-2-FF transformation:
\n
"
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
}
// derive AIG
...
...
@@ -178,7 +178,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
if
(
fVerbose
)
{
printf
(
"After min-area retiming:
\n
"
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
}
// transform back
...
...
@@ -187,7 +187,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
if
(
fVerbose
)
{
printf
(
"After FF-2-PI tranformation:
\n
"
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
}
return
pNew
;
}
...
...
src/proof/cec/cecCore.c
View file @
23879f92
...
...
@@ -401,7 +401,7 @@ p->timeSim += Abc_Clock() - clk;
// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
if
(
pPars
->
fVeryVerbose
)
Gia_ManPrintStats
(
pSrm
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pSrm
,
NULL
);
if
(
Gia_ManCoNum
(
pSrm
)
==
0
)
{
Gia_ManStop
(
pSrm
);
...
...
src/proof/ssc/sscCore.c
View file @
23879f92
...
...
@@ -385,9 +385,9 @@ Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
if
(
pPars
->
fVerbose
)
{
printf
(
"User AIG: "
);
Gia_ManPrintStats
(
pAig
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pAig
,
NULL
);
printf
(
"Care AIG: "
);
Gia_ManPrintStats
(
pCare
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pCare
,
NULL
);
}
pAig
=
Gia_ManDupLevelized
(
pResult
=
pAig
);
...
...
src/proof/ssc/sscUtil.c
View file @
23879f92
...
...
@@ -130,10 +130,10 @@ Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
int
i
;
assert
(
p
->
nConstrs
==
0
);
printf
(
"User AIG: "
);
Gia_ManPrintStats
(
p
,
0
,
0
,
0
);
Gia_ManPrintStats
(
p
,
NULL
);
pTemp
=
Gia_ManDropContained
(
p
);
printf
(
"Drop AIG: "
);
Gia_ManPrintStats
(
pTemp
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pTemp
,
NULL
);
// return pTemp;
if
(
Gia_ManPoNum
(
pTemp
)
==
1
)
return
pTemp
;
...
...
@@ -158,7 +158,7 @@ Gia_Man_t * Gia_ManOptimizeRing( Gia_Man_t * p )
Gia_ManStop
(
pAux
);
// report results
printf
(
"AIG%3d : "
,
i
);
Gia_ManPrintStats
(
pTemp
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pTemp
,
NULL
);
}
pTemp
->
nConstrs
=
0
;
return
pTemp
;
...
...
src/sat/bmc/bmcBmcAnd.c
View file @
23879f92
...
...
@@ -345,7 +345,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// report statistics
if
(
pPars
->
fVerbose
)
{
printf
(
"%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f M
b
"
,
printf
(
"%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f M
B
"
,
f
,
Gia_ManPiNum
(
p
->
pFrames
),
Gia_ManAndNum
(
p
->
pFrames
),
p
->
nSatVars
-
1
,
Vec_IntSize
(
p
->
vInputs
),
Vec_IntSize
(
p
->
vNodes
),
sat_solver_nclauses
(
p
->
pSat
),
sat_solver_nconflicts
(
p
->
pSat
),
Gia_ManMemory
(
p
->
pFrames
)
);
...
...
src/sat/bmc/bmcCexDepth.c
View file @
23879f92
...
...
@@ -148,14 +148,14 @@ Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
{
printf
(
"%3d : "
,
i
);
if
(
i
%
Gia_ManPiNum
(
p
)
==
0
)
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
pNew
=
Gia_ManDupExist
(
pTemp
=
pNew
,
i
);
Gia_ManStop
(
pTemp
);
}
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
pNew
=
Gia_ManDupLastPis
(
pTemp
=
pNew
,
Gia_ManRegNum
(
p
)
);
Gia_ManStop
(
pTemp
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
pTemp
=
Gia_ManDupAppendCones
(
p
,
&
pNew
,
1
,
1
);
Gia_ManStop
(
pNew
);
Gia_AigerWrite
(
pTemp
,
"miter3.aig"
,
0
,
0
);
...
...
@@ -352,7 +352,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
{
printf
(
"Frame %5d : "
,
i
);
pNew
=
Bmc_CexBuildNetwork2_
(
p
,
pCex
,
i
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
Vec_PtrPush
(
vCones
,
pNew
);
}
pNew
=
Gia_ManDupAppendCones
(
p
,
(
Gia_Man_t
**
)
Vec_PtrArray
(
vCones
),
Vec_PtrSize
(
vCones
),
1
);
...
...
src/sat/bmc/bmcCexMin2.c
View file @
23879f92
...
...
@@ -332,7 +332,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
{
pNew
=
Gia_ManCreateUnate
(
p
,
pCex
,
iFrameStart
,
nRealPis
,
fUseAll
);
printf
(
"%3d : "
,
iFrameStart
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
if
(
fVerbose
)
Gia_AigerWrite
(
pNew
,
"temp.aig"
,
0
,
0
);
Gia_ManStop
(
pNew
);
...
...
@@ -343,7 +343,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
{
pNew
=
Gia_ManCreateUnate
(
p
,
pCex
,
f
,
-
1
,
fUseAll
);
printf
(
"%3d : "
,
f
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
if
(
fVerbose
)
Gia_AigerWrite
(
pNew
,
"temp.aig"
,
0
,
0
);
Gia_ManStop
(
pNew
);
...
...
src/sat/bmc/bmcCexTools.c
View file @
23879f92
...
...
@@ -172,7 +172,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
Gia_Man_t
*
pNew
;
abctime
clk
=
Abc_Clock
();
pNew
=
Bmc_CexPerformUnrolling
(
p
,
pCex
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
Gia_AigerWrite
(
pNew
,
"unroll.aig"
,
0
,
0
);
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop
(
pNew
);
...
...
@@ -284,7 +284,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
Gia_Man_t
*
pNew
;
abctime
clk
=
Abc_Clock
();
pNew
=
Bmc_CexBuildNetwork
(
p
,
pCex
);
Gia_ManPrintStats
(
pNew
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pNew
,
NULL
);
Gia_AigerWrite
(
pNew
,
"unate.aig"
,
0
,
0
);
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop
(
pNew
);
...
...
src/sat/bmc/bmcUnroll.c
View file @
23879f92
...
...
@@ -487,8 +487,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
pFrames1
=
Unr_ManUnrollSimple
(
pGia
,
nFrames
);
Abc_PrintTime
(
1
,
"UnrollS"
,
Abc_Clock
()
-
clk
);
Gia_ManPrintStats
(
pFrames0
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pFrames1
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pFrames0
,
NULL
);
Gia_ManPrintStats
(
pFrames1
,
NULL
);
Gia_AigerWrite
(
pFrames0
,
"frames0.aig"
,
0
,
0
);
Gia_AigerWrite
(
pFrames1
,
"frames1.aig"
,
0
,
0
);
...
...
src/sat/bsat/satSolver2i.c
View file @
23879f92
...
...
@@ -220,7 +220,7 @@ Gia_Man_t * Gia_ManInterTest( Gia_Man_t * p )
// derive interpolant
pInter
=
(
Gia_Man_t
*
)
Int2_ManReadInterpolant
(
pSat
);
Gia_ManPrintStats
(
pInter
,
0
,
0
,
0
);
Gia_ManPrintStats
(
pInter
,
NULL
);
Abc_PrintTime
(
1
,
"Total interpolation time"
,
Abc_Clock
()
-
clk
);
// clean up
...
...
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