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
d4f073ba
Commit
d4f073ba
authored
Oct 22, 2021
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Various changes.
parent
abc54a2d
Show whitespace changes
Inline
Side-by-side
Showing
9 changed files
with
224 additions
and
78 deletions
+224
-78
src/aig/gia/gia.h
+7
-0
src/aig/gia/giaMan.c
+1
-0
src/aig/gia/giaPat2.c
+97
-43
src/aig/gia/giaSimBase.c
+78
-0
src/aig/gia/giaStoch.c
+0
-20
src/base/acb/acbFunc.c
+2
-0
src/misc/util/utilTruth.h
+15
-15
src/misc/vec/vecPtr.h
+20
-0
src/misc/vec/vecWrd.h
+4
-0
No files found.
src/aig/gia/gia.h
View file @
d4f073ba
...
...
@@ -217,6 +217,7 @@ struct Gia_Man_t_
Vec_Int_t
*
vClassOld
;
Vec_Int_t
*
vClassNew
;
Vec_Int_t
*
vPats
;
Vec_Bit_t
*
vPolars
;
// incremental simulation
int
fIncrSim
;
int
iNextPi
;
...
...
@@ -1592,6 +1593,12 @@ extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, i
/*=== giaSimBase.c ============================================================*/
extern
Vec_Wrd_t
*
Gia_ManSimPatSim
(
Gia_Man_t
*
p
);
extern
Vec_Wrd_t
*
Gia_ManSimPatSimOut
(
Gia_Man_t
*
pGia
,
Vec_Wrd_t
*
vSimsPi
,
int
fOuts
);
extern
void
Gia_ManSim2ArrayOne
(
Vec_Wrd_t
*
vSimsPi
,
Vec_Int_t
*
vRes
);
extern
Vec_Wec_t
*
Gia_ManSim2Array
(
Vec_Ptr_t
*
vSims
);
extern
Vec_Wrd_t
*
Gia_ManArray2SimOne
(
Vec_Int_t
*
vRes
);
extern
Vec_Ptr_t
*
Gia_ManArray2Sim
(
Vec_Wec_t
*
vRes
);
extern
void
Gia_ManPtrWrdDumpBin
(
char
*
pFileName
,
Vec_Ptr_t
*
p
,
int
fVerbose
);
extern
Vec_Ptr_t
*
Gia_ManPtrWrdReadBin
(
char
*
pFileName
,
int
fVerbose
);
/*=== giaSpeedup.c ============================================================*/
extern
float
Gia_ManDelayTraceLut
(
Gia_Man_t
*
p
);
extern
float
Gia_ManDelayTraceLutPrint
(
Gia_Man_t
*
p
,
int
fVerbose
);
...
...
src/aig/gia/giaMan.c
View file @
d4f073ba
...
...
@@ -95,6 +95,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP
(
&
p
->
vClassNew
);
Vec_IntFreeP
(
&
p
->
vClassOld
);
Vec_IntFreeP
(
&
p
->
vPats
);
Vec_BitFreeP
(
&
p
->
vPolars
);
Vec_WrdFreeP
(
&
p
->
vSims
);
Vec_WrdFreeP
(
&
p
->
vSimsT
);
Vec_WrdFreeP
(
&
p
->
vSimsPi
);
...
...
src/aig/gia/giaPat2.c
View file @
d4f073ba
...
...
@@ -78,6 +78,8 @@ static inline char Min_LitValL( Min_Man_t * p, int i ) { return Vec_
static
inline
void
Min_LitSetValL
(
Min_Man_t
*
p
,
int
i
,
char
v
){
assert
(
v
==
0
||
v
==
1
);
Vec_StrWriteEntry
(
&
p
->
vValsL
,
i
,
v
);
Vec_StrWriteEntry
(
&
p
->
vValsL
,
i
^
1
,
(
char
)
!
v
);
Vec_IntPush
(
&
p
->
vVis
,
Abc_Lit2Var
(
i
));
}
static
inline
void
Min_ObjCleanValL
(
Min_Man_t
*
p
,
int
i
)
{
((
short
*
)
Vec_StrArray
(
&
p
->
vValsL
))[
i
]
=
0x0202
;
}
static
inline
void
Min_ObjMarkValL
(
Min_Man_t
*
p
,
int
i
)
{
((
short
*
)
Vec_StrArray
(
&
p
->
vValsL
))[
i
]
|=
0x0404
;
}
static
inline
void
Min_ObjMark2ValL
(
Min_Man_t
*
p
,
int
i
)
{
((
short
*
)
Vec_StrArray
(
&
p
->
vValsL
))[
i
]
|=
0x0808
;
}
static
inline
void
Min_ObjUnmark2ValL
(
Min_Man_t
*
p
,
int
i
)
{
((
short
*
)
Vec_StrArray
(
&
p
->
vValsL
))[
i
]
&=
0xF7F7
;
}
static
inline
int
Min_LitIsCi
(
Min_Man_t
*
p
,
int
v
)
{
return
v
>
1
&&
v
<
p
->
FirstAndLit
;
}
static
inline
int
Min_LitIsNode
(
Min_Man_t
*
p
,
int
v
)
{
return
v
>=
p
->
FirstAndLit
&&
v
<
p
->
FirstCoLit
;
}
...
...
@@ -270,7 +272,7 @@ char Min_LitVerify_rec( Min_Man_t * p, int iLit )
int
iLit1
=
Min_LitFan
(
p
,
iLit
^
1
);
char
Val0
=
Min_LitVerify_rec
(
p
,
iLit0
);
char
Val1
=
Min_LitVerify_rec
(
p
,
iLit1
);
assert
(
Min_LitIsNode
(
p
,
iLit
)
);
// internal node
assert
(
Val0
<
3
&&
Val1
<
3
);
if
(
Min_LitIsXor
(
iLit
,
iLit0
,
iLit1
)
)
Val
=
Min_XsimXor
(
Val0
,
Val1
);
else
...
...
@@ -280,8 +282,11 @@ char Min_LitVerify_rec( Min_Man_t * p, int iLit )
Val
^=
Abc_LitIsCompl
(
iLit
);
Min_LitSetValL
(
p
,
iLit
,
Val
);
}
else
Vec_IntPush
(
&
p
->
vVis
,
Abc_Lit2Var
(
iLit
)
);
Min_ObjMark2ValL
(
p
,
Abc_Lit2Var
(
iLit
)
);
}
return
Val
;
return
Val
&
3
;
}
char
Min_LitVerify
(
Min_Man_t
*
p
,
int
iLit
,
Vec_Int_t
*
vLits
)
{
...
...
@@ -313,7 +318,7 @@ void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
Vec_IntForEachEntryReverse
(
&
p
->
vVis
,
iObj
,
i
)
{
int
iLit
=
Abc_Var2Lit
(
iObj
,
0
);
int
Value
=
Min_LitValL
(
p
,
iLit
);
int
Value
=
7
&
Min_LitValL
(
p
,
iLit
);
if
(
Value
>=
4
)
{
if
(
Min_LitIsCi
(
p
,
iLit
)
)
...
...
@@ -324,7 +329,7 @@ void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits )
int
iLit1
=
Min_LitFan
(
p
,
iLit
^
1
);
char
Val0
=
Min_LitValL
(
p
,
iLit0
);
char
Val1
=
Min_LitValL
(
p
,
iLit1
);
if
(
Value
==
5
)
// value == 1
if
(
Value
&
1
)
// value == 1
{
assert
(
(
Val0
&
1
)
&&
(
Val1
&
1
)
);
Min_ObjMarkValL
(
p
,
Abc_Lit2Var
(
iLit0
)
);
...
...
@@ -610,7 +615,7 @@ int Min_LitJustify_rec( Min_Man_t * p, int iLit )
}
int
Min_LitJustify
(
Min_Man_t
*
p
,
int
iLit
)
{
int
Res
,
fCheck
=
1
;
int
Res
,
fCheck
=
0
;
Vec_IntClear
(
&
p
->
vPat
);
if
(
iLit
<
2
)
return
1
;
assert
(
!
Min_LitIsCo
(
p
,
iLit
)
);
...
...
@@ -621,7 +626,6 @@ int Min_LitJustify( Min_Man_t * p, int iLit )
Min_ManCleanVisitedValL
(
p
);
if
(
Res
)
{
Vec_IntSort
(
&
p
->
vPat
,
0
);
if
(
fCheck
&&
Min_LitVerify
(
p
,
iLit
,
&
p
->
vPat
)
!=
1
)
printf
(
"Verification FAILED for literal %d.
\n
"
,
iLit
);
//else
...
...
@@ -912,7 +916,7 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
if
(
1
)
// minimization
{
//printf( "%d -> ", Vec_IntSize(vPatBest) );
for
(
i
=
0
;
i
<
1
0
;
i
++
)
for
(
i
=
0
;
i
<
2
0
;
i
++
)
{
Min_LitMinimize
(
pNew
,
Min_ObjLit0
(
pNew
,
iObj
),
vLits
);
if
(
Vec_IntSize
(
vPatBest
)
>
Vec_IntSize
(
&
pNew
->
vPat
)
)
...
...
@@ -921,6 +925,7 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie
//printf( "%d ", Vec_IntSize(vPatBest) );
}
assert
(
Vec_IntSize
(
vPatBest
)
>
0
);
Vec_IntSort
(
vPatBest
,
0
);
nCurrCexes
+=
Min_ManAccumulate
(
vCexes
,
nOuts
*
nMinCexes
,
(
nOuts
+
1
)
*
nMinCexes
,
vPatBest
);
nGoodCalls
++
;
}
...
...
@@ -1054,46 +1059,69 @@ int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * v
break
;
return
iPat
;
}
Vec_Wrd_t
*
Min_ManBitPack
(
Gia_Man_t
*
p
,
Vec_Wec_t
*
vCexes
,
int
fRandom
,
int
nMinCexes
,
Vec_Int_t
*
vScores
,
int
fVerbose
)
Vec_Ptr_t
*
Min_ReloadCexes
(
Vec_Wec_t
*
vCexes
,
int
nMinCexes
)
{
Vec_Ptr_t
*
vRes
=
Vec_PtrAlloc
(
Vec_WecSize
(
vCexes
)
);
int
i
,
c
,
nOuts
=
Vec_WecSize
(
vCexes
)
/
nMinCexes
;
for
(
i
=
0
;
i
<
nMinCexes
;
i
++
)
for
(
c
=
0
;
c
<
nOuts
;
c
++
)
{
Vec_Int_t
*
vLevel
=
Vec_WecEntry
(
vCexes
,
c
*
nMinCexes
+
i
);
if
(
Vec_IntSize
(
vLevel
)
)
Vec_PtrPush
(
vRes
,
vLevel
);
}
return
vRes
;
}
Vec_Wrd_t
*
Min_ManBitPack
(
Gia_Man_t
*
p
,
int
nWords0
,
Vec_Wec_t
*
vCexes
,
int
fRandom
,
int
nMinCexes
,
Vec_Int_t
*
vScores
,
int
fVerbose
)
{
abctime
clk
=
Abc_Clock
();
int
fVeryVerbose
=
0
;
Vec_Wrd_t
*
vSimsPi
=
NULL
;
Vec_Int_t
*
vLevel
;
int
w
,
nBits
,
nTotal
=
0
,
fFailed
=
ABC_INFINITY
;
Vec_Int_t
*
vOrder
=
Vec_IntStartNatural
(
Vec_WecSize
(
vCexes
)
/
nMinCexes
);
Vec_Int_t
*
vOrder
=
NULL
;
Vec_Ptr_t
*
vReload
=
NULL
;
if
(
0
)
{
vOrder
=
Vec_IntStartNatural
(
Vec_WecSize
(
vCexes
)
/
nMinCexes
);
assert
(
Vec_IntSize
(
vOrder
)
==
Vec_IntSize
(
vScores
)
);
assert
(
Vec_WecSize
(
vCexes
)
%
nMinCexes
==
0
);
Abc_MergeSortCost2Reverse
(
Vec_IntArray
(
vOrder
),
Vec_IntSize
(
vOrder
),
Vec_IntArray
(
vScores
)
);
}
else
vReload
=
Min_ReloadCexes
(
vCexes
,
nMinCexes
);
if
(
fVerbose
)
printf
(
"Packing: "
);
//for ( w = 1; fFailed > 100; w++ )
for
(
w
=
1
;
fFailed
>
0
;
w
++
)
for
(
w
=
nWords0
?
nWords0
:
1
;
nWords0
?
w
<=
nWords0
:
fFailed
>
0
;
w
++
)
{
int
i
,
k
,
iOut
,
iPatUsed
,
iPat
=
0
;
int
i
,
iPatUsed
,
iPat
=
0
;
//int k, iOut;
Vec_WrdFreeP
(
&
vSimsPi
);
vSimsPi
=
fRandom
?
Vec_WrdStartRandom
(
2
*
Gia_ManCiNum
(
p
)
*
w
)
:
Vec_WrdStart
(
2
*
Gia_ManCiNum
(
p
)
*
w
);
Vec_WrdShrink
(
vSimsPi
,
Vec_WrdSize
(
vSimsPi
)
/
2
);
Abc_TtClear
(
Vec_WrdLimit
(
vSimsPi
),
Vec_WrdSize
(
vSimsPi
)
);
fFailed
=
nTotal
=
0
;
Vec_IntForEachEntry
(
vOrder
,
iOut
,
k
)
Vec_WecForEachLevelStartStop
(
vCexes
,
vLevel
,
i
,
iOut
*
nMinCexes
,
(
iOut
+
1
)
*
nMinCexes
)
//Vec_IntForEachEntry( vOrder, iOut, k )
//Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes )
Vec_PtrForEachEntry
(
Vec_Int_t
*
,
vReload
,
vLevel
,
i
)
{
if
(
fVeryVerbose
&&
i
%
nMinCexes
==
0
)
printf
(
"
\n
"
);
//
if ( fVeryVerbose && i%nMinCexes == 0 )
//
printf( "\n" );
if
(
Vec_IntSize
(
vLevel
)
==
0
)
continue
;
iPatUsed
=
Min_ManBitPackOne
(
vSimsPi
,
iPat
,
w
,
vLevel
);
fFailed
+=
iPatUsed
==
iPat
;
iPat
=
(
iPatUsed
+
1
)
%
(
64
*
w
-
1
);
if
(
fVeryVerbose
)
printf
(
"Adding output %3d cex %3d to pattern %3d "
,
i
/
nMinCexes
,
i
%
nMinCexes
,
iPatUsed
);
if
(
fVeryVerbose
)
Vec_IntPrint
(
vLevel
);
iPat
=
(
iPatUsed
+
1
)
%
(
64
*
(
w
-
1
)
-
1
);
//
if ( fVeryVerbose )
//
printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed );
//
if ( fVeryVerbose )
//
Vec_IntPrint( vLevel );
nTotal
++
;
}
if
(
fVerbose
)
printf
(
"W = %d (F = %d) "
,
w
,
fFailed
);
// printf( "Failed patterns = %d\n", fFailed );
}
if
(
fVerbose
)
printf
(
"Total = %d
\n
"
,
nTotal
);
...
...
@@ -1104,7 +1132,8 @@ Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, Vec_Wec_t * vCexes, int fRandom, int
Vec_WrdSize
(
vSimsPi
)
/
Gia_ManCiNum
(
p
),
nBits
,
100
.
0
*
nBits
/
64
/
Vec_WrdSize
(
vSimsPi
)
);
Abc_PrintTime
(
1
,
"Time"
,
Abc_Clock
()
-
clk
);
}
Vec_IntFree
(
vOrder
);
Vec_IntFreeP
(
&
vOrder
);
Vec_PtrFreeP
(
&
vReload
);
return
vSimsPi
;
}
...
...
@@ -1205,37 +1234,42 @@ Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p )
Gia_ManForEachCoDriverId
(
p
,
Driver
,
i
)
if
(
Driver
>
0
)
Vec_IntPush
(
vRes
,
i
);
if
(
Vec_IntSize
(
vRes
)
==
0
)
Vec_IntFreeP
(
&
vRes
);
return
vRes
;
}
Vec_Wrd_t
*
Min_ManCollect
(
Gia_Man_t
*
p
,
int
nConf
,
int
nConf2
,
int
nMaxTries
,
int
nMinCexes
,
int
fUseSim
,
int
fUseSat
,
int
fVerbose
)
Vec_Wrd_t
*
Min_ManRemapSims
(
int
nInputs
,
Vec_Int_t
*
vMap
,
Vec_Wrd_t
*
vSimsPi
)
{
int
i
,
iObj
,
nWords
=
Vec_WrdSize
(
vSimsPi
)
/
Vec_IntSize
(
vMap
);
Vec_Wrd_t
*
vSimsNew
=
Vec_WrdStart
(
2
*
nInputs
*
nWords
);
assert
(
Vec_WrdSize
(
vSimsPi
)
%
Vec_IntSize
(
vMap
)
==
0
);
Vec_WrdShrink
(
vSimsNew
,
Vec_WrdSize
(
vSimsNew
)
/
2
);
Vec_IntForEachEntry
(
vMap
,
iObj
,
i
)
{
Abc_TtCopy
(
Vec_WrdArray
(
vSimsNew
)
+
(
iObj
-
1
)
*
nWords
,
Vec_WrdArray
(
vSimsPi
)
+
i
*
nWords
,
nWords
,
0
);
Abc_TtCopy
(
Vec_WrdLimit
(
vSimsNew
)
+
(
iObj
-
1
)
*
nWords
,
Vec_WrdLimit
(
vSimsPi
)
+
i
*
nWords
,
nWords
,
0
);
}
return
vSimsNew
;
}
Vec_Wrd_t
*
Gia_ManCollectSims
(
Gia_Man_t
*
pSwp
,
int
nWords
,
Vec_Int_t
*
vOuts
,
int
nMaxTries
,
int
nMinCexes
,
int
fUseSim
,
int
fUseSat
,
int
fVerbose
,
int
fVeryVerbose
)
{
abctime
clk
=
Abc_Clock
();
Vec_Int_t
*
vStats
[
3
]
=
{
0
};
int
i
,
iObj
;
extern
Gia_Man_t
*
Cec4_ManSimulateTest4
(
Gia_Man_t
*
p
,
int
nBTLimit
,
int
nBTLimitPo
,
int
fVerbose
);
Gia_Man_t
*
pSwp
=
Cec4_ManSimulateTest4
(
p
,
nConf
,
nConf2
,
0
);
abctime
clkSweep
=
Abc_Clock
()
-
clk
;
int
nArgs
=
fVerbose
?
printf
(
"Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.
\n
"
,
nConf
,
nConf2
,
nMaxTries
,
nMinCexes
,
fUseSim
,
fUseSat
)
:
0
;
Vec_Int_t
*
vOuts
=
Min_ManGetUnsolved
(
pSwp
);
Gia_Man_t
*
pSwp2
=
Gia_ManDupSelectedOutputs
(
pSwp
,
vOuts
);
Vec_Int_t
*
vMap
=
Vec_IntAlloc
(
100
);
Gia_Man_t
*
pSwp2
=
Gia_ManDupCones2
(
pSwp
,
Vec_IntArray
(
vOuts
),
Vec_IntSize
(
vOuts
),
vMap
);
Vec_Wec_t
*
vCexes
=
Min_ManComputeCexes
(
pSwp2
,
NULL
,
nMaxTries
,
nMinCexes
,
vStats
,
fUseSim
,
fUseSat
,
fVerbose
);
Vec_Wrd_t
*
vSimsPi
=
Min_ManBitPack
(
p
,
vCexes
,
1
,
nMinCexes
,
vStats
[
0
],
fVerbose
);
Vec_Wrd_t
*
vSimsPi
=
Min_ManBitPack
(
p
Swp2
,
nWords
,
vCexes
,
1
,
nMinCexes
,
vStats
[
0
],
fVerbose
);
Vec_Wrd_t
*
vSimsPo
=
Gia_ManSimPatSimOut
(
pSwp2
,
vSimsPi
,
1
);
Vec_Int_t
*
vCounts
=
Patt_ManOutputErrorCoverage
(
vSimsPo
,
Vec_IntSize
(
vOuts
)
);
if
(
fVerbose
)
{
Patt_ManProfileErrorsOne
(
vSimsPo
,
Vec_IntSize
(
vOuts
)
);
Abc_PrintTime
(
1
,
"Sweep time"
,
clkSweep
);
Abc_PrintTime
(
1
,
"Total time"
,
Abc_Clock
()
-
clk
);
}
if
(
0
)
if
(
fVeryVerbose
)
{
printf
(
"Unsolved = %4d "
,
Vec_IntSize
(
vOuts
)
);
Gia_ManPrintStats
(
pSwp2
,
NULL
);
Vec_IntForEachEntry
(
vOuts
,
iObj
,
i
)
{
printf
(
"%4d : "
,
i
);
printf
(
"Out = %5d "
,
iObj
);
printf
(
"Out = %5d "
,
Vec_IntEntry
(
vMap
,
i
)
);
printf
(
"SimAll =%8d "
,
Vec_IntEntry
(
vStats
[
0
],
i
)
);
printf
(
"SimGood =%8d "
,
Vec_IntEntry
(
vStats
[
1
],
i
)
);
printf
(
"PatsAll =%8d "
,
Vec_IntEntry
(
vStats
[
2
],
i
)
);
...
...
@@ -1250,20 +1284,40 @@ Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries,
Vec_IntFree
(
vCounts
);
Vec_WrdFree
(
vSimsPo
);
Vec_WecFree
(
vCexes
);
Vec_IntFree
(
vOuts
);
Gia_ManStop
(
pSwp
);
Gia_ManStop
(
pSwp2
);
//printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) );
vSimsPi
=
Min_ManRemapSims
(
Gia_ManCiNum
(
pSwp
),
vMap
,
vSimsPo
=
vSimsPi
);
Vec_WrdFree
(
vSimsPo
);
Vec_IntFree
(
vMap
);
return
vSimsPi
;
}
Vec_Wrd_t
*
Min_ManCollect
(
Gia_Man_t
*
p
,
int
nConf
,
int
nConf2
,
int
nMaxTries
,
int
nMinCexes
,
int
fUseSim
,
int
fUseSat
,
int
fVerbose
,
int
fVeryVerbose
)
{
abctime
clk
=
Abc_Clock
();
extern
Gia_Man_t
*
Cec4_ManSimulateTest4
(
Gia_Man_t
*
p
,
int
nBTLimit
,
int
nBTLimitPo
,
int
fVerbose
);
Gia_Man_t
*
pSwp
=
Cec4_ManSimulateTest4
(
p
,
nConf
,
nConf2
,
0
);
abctime
clkSweep
=
Abc_Clock
()
-
clk
;
int
nArgs
=
fVerbose
?
printf
(
"Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.
\n
"
,
nConf
,
nConf2
,
nMaxTries
,
nMinCexes
,
fUseSim
,
fUseSat
)
:
0
;
Vec_Int_t
*
vOuts
=
Min_ManGetUnsolved
(
pSwp
);
Vec_Wrd_t
*
vSimsPi
=
vOuts
?
Gia_ManCollectSims
(
pSwp
,
0
,
vOuts
,
nMaxTries
,
nMinCexes
,
fUseSim
,
fUseSat
,
fVerbose
,
fVeryVerbose
)
:
NULL
;
if
(
vOuts
==
NULL
)
printf
(
"There is no satisfiable outputs.
\n
"
);
if
(
fVerbose
)
Abc_PrintTime
(
1
,
"Sweep time"
,
clkSweep
);
if
(
fVerbose
)
Abc_PrintTime
(
1
,
"Total time"
,
Abc_Clock
()
-
clk
);
Vec_IntFreeP
(
&
vOuts
);
Gia_ManStop
(
pSwp
);
nArgs
=
0
;
return
vSimsPi
;
}
void
Min_ManTest2
(
Gia_Man_t
*
p
)
{
Vec_Wrd_t
*
vSimsPi
=
Min_ManCollect
(
p
,
100000
,
100000
,
10000
,
20
,
1
,
1
,
0
);
Vec_Wrd_t
*
vSimsPi
=
Min_ManCollect
(
p
,
100000
,
100000
,
10000
,
20
,
1
,
0
,
1
,
1
);
Vec_WrdFreeP
(
&
vSimsPi
);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
...
...
src/aig/gia/giaSimBase.c
View file @
d4f073ba
...
...
@@ -2622,6 +2622,84 @@ void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi )
}
Vec_PtrFree
(
vTemp
);
}
/**Function*************************************************************
Synopsis [Serialization.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Gia_ManPtrWrdDumpBin
(
char
*
pFileName
,
Vec_Ptr_t
*
p
,
int
fVerbose
)
{
Vec_Wrd_t
*
vLevel
;
int
i
,
nSize
,
RetValue
;
FILE
*
pFile
=
fopen
(
pFileName
,
"wb"
);
if
(
pFile
==
NULL
)
{
printf
(
"Cannot open file
\"
%s
\"
for writing.
\n
"
,
pFileName
);
return
;
}
nSize
=
Vec_PtrSize
(
p
);
RetValue
=
fwrite
(
&
nSize
,
1
,
sizeof
(
int
),
pFile
);
Vec_PtrForEachEntry
(
Vec_Wrd_t
*
,
p
,
vLevel
,
i
)
{
nSize
=
Vec_WrdSize
(
vLevel
);
RetValue
+=
fwrite
(
&
nSize
,
1
,
sizeof
(
int
),
pFile
);
RetValue
+=
fwrite
(
Vec_WrdArray
(
vLevel
),
1
,
sizeof
(
word
)
*
nSize
,
pFile
);
}
fclose
(
pFile
);
if
(
fVerbose
)
printf
(
"Written %d arrays into file
\"
%s
\"
.
\n
"
,
Vec_PtrSize
(
p
),
pFileName
);
}
Vec_Ptr_t
*
Gia_ManPtrWrdReadBin
(
char
*
pFileName
,
int
fVerbose
)
{
Vec_Ptr_t
*
p
=
NULL
;
Vec_Wrd_t
*
vLevel
;
int
i
,
nSize
,
RetValue
;
FILE
*
pFile
=
fopen
(
pFileName
,
"rb"
);
if
(
pFile
==
NULL
)
{
printf
(
"Cannot open file
\"
%s
\"
for reading.
\n
"
,
pFileName
);
return
NULL
;
}
fseek
(
pFile
,
0
,
SEEK_END
);
nSize
=
ftell
(
pFile
);
if
(
nSize
==
0
)
{
printf
(
"The input file is empty.
\n
"
);
fclose
(
pFile
);
return
NULL
;
}
if
(
nSize
%
(
int
)
sizeof
(
int
)
>
0
)
{
printf
(
"Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).
\n
"
,
nSize
%
(
int
)
sizeof
(
int
)
);
fclose
(
pFile
);
return
NULL
;
}
rewind
(
pFile
);
RetValue
=
fread
(
&
nSize
,
1
,
sizeof
(
int
),
pFile
);
assert
(
RetValue
==
4
);
p
=
Vec_PtrAlloc
(
nSize
);
for
(
i
=
0
;
i
<
nSize
;
i
++
)
Vec_PtrPush
(
p
,
Vec_WrdAlloc
(
100
)
);
Vec_PtrForEachEntry
(
Vec_Wrd_t
*
,
p
,
vLevel
,
i
)
{
RetValue
=
fread
(
&
nSize
,
1
,
sizeof
(
int
),
pFile
);
assert
(
RetValue
==
4
);
Vec_WrdFill
(
vLevel
,
nSize
,
0
);
RetValue
=
fread
(
Vec_WrdArray
(
vLevel
),
1
,
sizeof
(
word
)
*
nSize
,
pFile
);
assert
(
RetValue
==
8
*
nSize
);
}
fclose
(
pFile
);
if
(
fVerbose
)
printf
(
"Read %d arrays from file
\"
%s
\"
.
\n
"
,
Vec_PtrSize
(
p
),
pFileName
);
return
p
;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
...
...
src/aig/gia/giaStoch.c
View file @
d4f073ba
...
...
@@ -43,26 +43,6 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
static
void
Vec_PtrFreeFunc
(
Vec_Ptr_t
*
p
,
void
(
*
pFuncItemFree
)(
void
*
)
)
___unused
;
static
void
Vec_PtrFreeFunc
(
Vec_Ptr_t
*
p
,
void
(
*
pFuncItemFree
)(
void
*
)
)
{
void
*
pItem
;
int
i
;
Vec_PtrForEachEntry
(
void
*
,
p
,
pItem
,
i
)
pFuncItemFree
(
pItem
);
Vec_PtrFree
(
p
);
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void
Gia_ManDupMapping
(
Gia_Man_t
*
pNew
,
Gia_Man_t
*
p
)
{
Gia_Obj_t
*
pObj
,
*
pFanin
;
int
i
,
k
;
...
...
src/base/acb/acbFunc.c
View file @
d4f073ba
...
...
@@ -506,6 +506,7 @@ Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fN
// create names
if
(
fNames
)
{
pNew
->
vPolars
=
Vec_BitStart
(
Gia_ManObjNum
(
pNew
)
);
pNew
->
vNamesNode
=
Vec_PtrStart
(
Gia_ManObjNum
(
pNew
)
);
Vec_IntForEachEntry
(
vMap
,
iLit
,
Token
)
{
...
...
@@ -514,6 +515,7 @@ Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fN
sprintf
(
Buffer
,
"%c_%s"
,
Abc_LitIsCompl
(
iLit
)
?
'c'
:
'd'
,
Abc_NamStr
(
pNames
,
Token
)
);
assert
(
Vec_PtrEntry
(
pNew
->
vNamesNode
,
Abc_Lit2Var
(
iLit
))
==
NULL
);
Vec_PtrWriteEntry
(
pNew
->
vNamesNode
,
Abc_Lit2Var
(
iLit
),
Abc_UtilStrsav
(
Buffer
)
);
Vec_BitWriteEntry
(
pNew
->
vPolars
,
Abc_Lit2Var
(
iLit
),
Abc_LitIsCompl
(
iLit
)
);
}
}
else
...
...
src/misc/util/utilTruth.h
View file @
d4f073ba
...
...
@@ -2106,12 +2106,15 @@ static inline int Abc_TtCountOnes( word x )
x
=
x
+
(
x
>>
32
);
return
(
int
)(
x
&
0xFF
);
}
static
inline
int
Abc_TtCountOnes2
(
word
x
)
{
return
x
?
Abc_TtCountOnes
(
x
)
:
0
;
}
static
inline
int
Abc_TtCountOnesVec
(
word
*
x
,
int
nWords
)
{
int
w
,
Count
=
0
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
x
[
w
]
)
Count
+=
Abc_TtCountOnes
(
x
[
w
]
);
Count
+=
Abc_TtCountOnes2
(
x
[
w
]
);
return
Count
;
}
static
inline
int
Abc_TtCountOnesVecMask
(
word
*
x
,
word
*
pMask
,
int
nWords
,
int
fCompl
)
...
...
@@ -2120,14 +2123,12 @@ static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, in
if
(
fCompl
)
{
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
pMask
[
w
]
&
~
x
[
w
]
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
~
x
[
w
]
);
Count
+=
Abc_TtCountOnes2
(
pMask
[
w
]
&
~
x
[
w
]
);
}
else
{
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
pMask
[
w
]
&
x
[
w
]
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
x
[
w
]
);
Count
+=
Abc_TtCountOnes2
(
pMask
[
w
]
&
x
[
w
]
);
}
return
Count
;
}
...
...
@@ -2136,24 +2137,23 @@ static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int
int
w
,
Count
=
0
;
if
(
!
fComp0
&&
!
fComp1
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
x0
[
w
]
&
x1
[
w
]
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
x0
[
w
]
&
x1
[
w
]
);
else
if
(
fComp0
&&
!
fComp1
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
~
x0
[
w
]
&
x1
[
w
]
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
~
x0
[
w
]
&
x1
[
w
]
);
else
if
(
!
fComp0
&&
fComp1
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
x0
[
w
]
&
~
x1
[
w
]
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
x0
[
w
]
&
~
x1
[
w
]
);
else
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
~
x0
[
w
]
&
~
x1
[
w
]
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
~
x0
[
w
]
&
~
x1
[
w
]
);
return
Count
;
}
static
inline
int
Abc_TtCountOnesVecXor
(
word
*
x
,
word
*
y
,
int
nWords
)
{
int
w
,
Count
=
0
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
if
(
x
[
w
]
^
y
[
w
]
)
Count
+=
Abc_TtCountOnes
(
x
[
w
]
^
y
[
w
]
);
Count
+=
Abc_TtCountOnes2
(
x
[
w
]
^
y
[
w
]
);
return
Count
;
}
static
inline
int
Abc_TtCountOnesVecXorMask
(
word
*
x
,
word
*
y
,
int
fCompl
,
word
*
pMask
,
int
nWords
)
...
...
@@ -2161,10 +2161,10 @@ static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, wor
int
w
,
Count
=
0
;
if
(
fCompl
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
(
x
[
w
]
^
~
y
[
w
])
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
(
x
[
w
]
^
~
y
[
w
])
);
else
for
(
w
=
0
;
w
<
nWords
;
w
++
)
Count
+=
Abc_TtCountOnes
(
pMask
[
w
]
&
(
x
[
w
]
^
y
[
w
])
);
Count
+=
Abc_TtCountOnes
2
(
pMask
[
w
]
&
(
x
[
w
]
^
y
[
w
])
);
return
Count
;
}
static
inline
int
Abc_TtAndXorSum
(
word
*
pOut
,
word
*
pIn1
,
word
*
pIn2
,
int
nWords
)
...
...
@@ -2173,7 +2173,7 @@ static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nW
for
(
w
=
0
;
w
<
nWords
;
w
++
)
{
pOut
[
w
]
&=
pIn1
[
w
]
^
pIn2
[
w
];
Count
+=
Abc_TtCountOnes
(
pOut
[
w
]
);
Count
+=
Abc_TtCountOnes
2
(
pOut
[
w
]
);
}
return
Count
;
}
...
...
src/misc/vec/vecPtr.h
View file @
d4f073ba
...
...
@@ -607,6 +607,26 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static
void
Vec_PtrFreeFunc
(
Vec_Ptr_t
*
p
,
void
(
*
pFuncItemFree
)(
void
*
)
)
___unused
;
static
void
Vec_PtrFreeFunc
(
Vec_Ptr_t
*
p
,
void
(
*
pFuncItemFree
)(
void
*
)
)
{
void
*
pItem
;
int
i
;
Vec_PtrForEachEntry
(
void
*
,
p
,
pItem
,
i
)
if
(
pItem
)
pFuncItemFree
(
pItem
);
Vec_PtrFree
(
p
);
}
/**Function*************************************************************
Synopsis [Copies the interger array.]
Description []
...
...
src/misc/vec/vecWrd.h
View file @
d4f073ba
...
...
@@ -382,6 +382,10 @@ static inline int Vec_WrdSize( Vec_Wrd_t * p )
{
return
p
->
nSize
;
}
static
inline
int
Vec_WrdChangeSize
(
Vec_Wrd_t
*
p
,
int
Shift
)
{
return
p
->
nSize
+=
Shift
;
}
/**Function*************************************************************
...
...
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