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
4ed89d00
Commit
4ed89d00
authored
Oct 09, 2012
by
Alan Mishchenko
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Making explicit cast to 64-bit unsigned in a few places.
parent
7b9f4a27
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
31 additions
and
31 deletions
+31
-31
src/aig/aig/aigPack.c
+1
-1
src/base/abc/abcSop.c
+2
-2
src/base/io/ioWriteBlif.c
+1
-1
src/map/if/ifDec07.c
+2
-2
src/map/if/ifDec08.c
+4
-4
src/map/if/ifDec10.c
+4
-4
src/map/if/ifDec16.c
+4
-4
src/opt/dau/dauDsd.c
+5
-5
src/proof/ssw/sswRarity.c
+6
-6
src/sat/cnf/cnfFast.c
+2
-2
No files found.
src/aig/aig/aigPack.c
View file @
4ed89d00
...
@@ -185,7 +185,7 @@ void Aig_ManPackSimulate( Aig_ManPack_t * p )
...
@@ -185,7 +185,7 @@ void Aig_ManPackSimulate( Aig_ManPack_t * p )
word
Sign
,
Sign0
,
Sign1
;
word
Sign
,
Sign0
,
Sign1
;
int
i
;
int
i
;
// set the constant
// set the constant
Vec_WrdWriteEntry
(
p
->
vSigns
,
0
,
(
word
)
~
0
);
Vec_WrdWriteEntry
(
p
->
vSigns
,
0
,
~
(
word
)
0
);
// transfer into the array
// transfer into the array
Aig_ManForEachCi
(
p
->
pAig
,
pObj
,
i
)
Aig_ManForEachCi
(
p
->
pAig
,
pObj
,
i
)
Vec_WrdWriteEntry
(
p
->
vSigns
,
Aig_ObjId
(
pObj
),
Vec_WrdEntry
(
p
->
vPiPats
,
i
)
);
Vec_WrdWriteEntry
(
p
->
vSigns
,
Aig_ObjId
(
pObj
),
Vec_WrdEntry
(
p
->
vPiPats
,
i
)
);
...
...
src/base/abc/abcSop.c
View file @
4ed89d00
...
@@ -1229,7 +1229,7 @@ void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] )
...
@@ -1229,7 +1229,7 @@ void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] )
assert
(
nVars
==
nInputs
);
assert
(
nVars
==
nInputs
);
r
[
0
]
=
r
[
1
]
=
0
;
r
[
0
]
=
r
[
1
]
=
0
;
do
{
do
{
Cube
[
0
]
=
Cube
[
1
]
=
~
0
;
Cube
[
0
]
=
Cube
[
1
]
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
nVars
;
v
++
,
lit
++
)
for
(
v
=
0
;
v
<
nVars
;
v
++
,
lit
++
)
{
{
if
(
pSop
[
lit
]
==
'1'
)
if
(
pSop
[
lit
]
==
'1'
)
...
@@ -1282,7 +1282,7 @@ void Abc_SopToTruthBig( char * pSop, int nInputs, word ** pVars, word * pCube, w
...
@@ -1282,7 +1282,7 @@ void Abc_SopToTruthBig( char * pSop, int nInputs, word ** pVars, word * pCube, w
pRes
[
i
]
=
0
;
pRes
[
i
]
=
0
;
do
{
do
{
for
(
i
=
0
;
i
<
nWords
;
i
++
)
for
(
i
=
0
;
i
<
nWords
;
i
++
)
pCube
[
i
]
=
~
0
;
pCube
[
i
]
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
nVars
;
v
++
,
lit
++
)
for
(
v
=
0
;
v
<
nVars
;
v
++
,
lit
++
)
{
{
if
(
pSop
[
lit
]
==
'1'
)
if
(
pSop
[
lit
]
==
'1'
)
...
...
src/base/io/ioWriteBlif.c
View file @
4ed89d00
...
@@ -940,7 +940,7 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov
...
@@ -940,7 +940,7 @@ void Io_NtkWriteNodeIntStruct( FILE * pFile, Abc_Obj_t * pNode, Vec_Int_t * vCov
pTruths
[
i
][
k
]
=
Truth6
[
i
];
pTruths
[
i
][
k
]
=
Truth6
[
i
];
for
(
i
=
6
;
i
<
nVarsMax
;
i
++
)
for
(
i
=
6
;
i
<
nVarsMax
;
i
++
)
for
(
k
=
0
;
k
<
nWordsMax
;
k
++
)
for
(
k
=
0
;
k
<
nWordsMax
;
k
++
)
pTruths
[
i
][
k
]
=
((
k
>>
(
i
-
6
))
&
1
)
?
~
0
:
0
;
pTruths
[
i
][
k
]
=
((
k
>>
(
i
-
6
))
&
1
)
?
~
(
word
)
0
:
0
;
}
}
// collect variables
// collect variables
...
...
src/map/if/ifDec07.c
View file @
4ed89d00
...
@@ -108,7 +108,7 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
...
@@ -108,7 +108,7 @@ static word If_Dec6ComposeLut4( int t, word f[4] )
{
{
if
(
!
((
t
>>
m
)
&
1
)
)
if
(
!
((
t
>>
m
)
&
1
)
)
continue
;
continue
;
c
=
~
0
;
c
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
v
=
0
;
v
<
4
;
v
++
)
c
&=
((
m
>>
v
)
&
1
)
?
f
[
v
]
:
~
f
[
v
];
c
&=
((
m
>>
v
)
&
1
)
?
f
[
v
]
:
~
f
[
v
];
r
|=
c
;
r
|=
c
;
...
@@ -152,7 +152,7 @@ static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
...
@@ -152,7 +152,7 @@ static void If_Dec7ComposeLut4( int t, word f[4][2], word r[2] )
{
{
if
(
!
((
t
>>
m
)
&
1
)
)
if
(
!
((
t
>>
m
)
&
1
)
)
continue
;
continue
;
c
[
0
]
=
c
[
1
]
=
~
0
;
c
[
0
]
=
c
[
1
]
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
v
=
0
;
v
<
4
;
v
++
)
{
{
c
[
0
]
&=
((
m
>>
v
)
&
1
)
?
f
[
v
][
0
]
:
~
f
[
v
][
0
];
c
[
0
]
&=
((
m
>>
v
)
&
1
)
?
f
[
v
][
0
]
:
~
f
[
v
][
0
];
...
...
src/map/if/ifDec08.c
View file @
4ed89d00
...
@@ -113,7 +113,7 @@ static inline void If_Dec08ComposeLut4( int t, word ** pF, word * pR, int nVars
...
@@ -113,7 +113,7 @@ static inline void If_Dec08ComposeLut4( int t, word ** pF, word * pR, int nVars
if
(
!
((
t
>>
m
)
&
1
)
)
if
(
!
((
t
>>
m
)
&
1
)
)
continue
;
continue
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pC
[
w
]
=
~
0
;
pC
[
w
]
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pC
[
w
]
&=
((
m
>>
v
)
&
1
)
?
pF
[
v
][
w
]
:
~
pF
[
v
][
w
];
pC
[
w
]
&=
((
m
>>
v
)
&
1
)
?
pF
[
v
][
w
]
:
~
pF
[
v
][
w
];
...
@@ -159,7 +159,7 @@ static inline int If_Dec08CofCount2( word * pF, int nVars )
...
@@ -159,7 +159,7 @@ static inline int If_Dec08CofCount2( word * pF, int nVars )
int
i
;
int
i
;
assert
(
nVars
>=
6
&&
nVars
<=
8
);
assert
(
nVars
>=
6
&&
nVars
<=
8
);
// if ( nVars == 10 )
// if ( nVars == 10 )
// Mask = ~0;
// Mask = ~
(word)
0;
for
(
i
=
1
;
i
<
8
;
i
++
)
for
(
i
=
1
;
i
<
8
;
i
++
)
{
{
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
...
@@ -179,7 +179,7 @@ static inline int If_Dec08CofCount( word * pF, int nVars )
...
@@ -179,7 +179,7 @@ static inline int If_Dec08CofCount( word * pF, int nVars )
word
iCofs
[
16
],
iCof
;
word
iCofs
[
16
],
iCof
;
int
i
,
c
,
nCofs
=
1
;
int
i
,
c
,
nCofs
=
1
;
// if ( nVars == 10 )
// if ( nVars == 10 )
// Mask = ~0;
// Mask = ~
(word)
0;
iCofs
[
0
]
=
pF
[
0
]
&
Mask
;
iCofs
[
0
]
=
pF
[
0
]
&
Mask
;
for
(
i
=
1
;
i
<
8
;
i
++
)
for
(
i
=
1
;
i
<
8
;
i
++
)
{
{
...
@@ -270,7 +270,7 @@ static inline int If_Dec08DeriveCount2( word * pF, word * pRes, int nVars )
...
@@ -270,7 +270,7 @@ static inline int If_Dec08DeriveCount2( word * pF, word * pRes, int nVars )
word
iCof1
=
pF
[
0
]
&
Mask
;
word
iCof1
=
pF
[
0
]
&
Mask
;
word
iCof
,
*
pCof0
,
*
pCof1
;
word
iCof
,
*
pCof0
,
*
pCof1
;
if
(
nVars
==
10
)
if
(
nVars
==
10
)
Mask
=
~
0
;
Mask
=
~
(
word
)
0
;
for
(
i
=
1
;
i
<
16
;
i
++
)
for
(
i
=
1
;
i
<
16
;
i
++
)
{
{
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
...
...
src/map/if/ifDec10.c
View file @
4ed89d00
...
@@ -110,7 +110,7 @@ static inline void If_Dec10ComposeLut4( int t, word ** pF, word * pR, int nVars
...
@@ -110,7 +110,7 @@ static inline void If_Dec10ComposeLut4( int t, word ** pF, word * pR, int nVars
if
(
!
((
t
>>
m
)
&
1
)
)
if
(
!
((
t
>>
m
)
&
1
)
)
continue
;
continue
;
for
(
w
=
0
;
w
<
nWords
;
w
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pC
[
w
]
=
~
0
;
pC
[
w
]
=
~
(
word
)
0
;
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
v
=
0
;
v
<
4
;
v
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pC
[
w
]
&=
((
m
>>
v
)
&
1
)
?
pF
[
v
][
w
]
:
~
pF
[
v
][
w
];
pC
[
w
]
&=
((
m
>>
v
)
&
1
)
?
pF
[
v
][
w
]
:
~
pF
[
v
][
w
];
...
@@ -156,7 +156,7 @@ static inline int If_Dec10CofCount2( word * pF, int nVars )
...
@@ -156,7 +156,7 @@ static inline int If_Dec10CofCount2( word * pF, int nVars )
int
i
;
int
i
;
assert
(
nVars
>
6
&&
nVars
<=
10
);
assert
(
nVars
>
6
&&
nVars
<=
10
);
if
(
nVars
==
10
)
if
(
nVars
==
10
)
Mask
=
~
0
;
Mask
=
~
(
word
)
0
;
for
(
i
=
1
;
i
<
16
;
i
++
)
for
(
i
=
1
;
i
<
16
;
i
++
)
{
{
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
...
@@ -176,7 +176,7 @@ static inline int If_Dec10CofCount( word * pF, int nVars )
...
@@ -176,7 +176,7 @@ static inline int If_Dec10CofCount( word * pF, int nVars )
word
iCofs
[
16
],
iCof
;
word
iCofs
[
16
],
iCof
;
int
i
,
c
,
nCofs
=
1
;
int
i
,
c
,
nCofs
=
1
;
if
(
nVars
==
10
)
if
(
nVars
==
10
)
Mask
=
~
0
;
Mask
=
~
(
word
)
0
;
iCofs
[
0
]
=
pF
[
0
]
&
Mask
;
iCofs
[
0
]
=
pF
[
0
]
&
Mask
;
for
(
i
=
1
;
i
<
16
;
i
++
)
for
(
i
=
1
;
i
<
16
;
i
++
)
{
{
...
@@ -267,7 +267,7 @@ static inline int If_Dec10DeriveCount2( word * pF, word * pRes, int nVars )
...
@@ -267,7 +267,7 @@ static inline int If_Dec10DeriveCount2( word * pF, word * pRes, int nVars )
word
iCof1
=
pF
[
0
]
&
Mask
;
word
iCof1
=
pF
[
0
]
&
Mask
;
word
iCof
,
*
pCof0
,
*
pCof1
;
word
iCof
,
*
pCof0
,
*
pCof1
;
if
(
nVars
==
10
)
if
(
nVars
==
10
)
Mask
=
~
0
;
Mask
=
~
(
word
)
0
;
for
(
i
=
1
;
i
<
16
;
i
++
)
for
(
i
=
1
;
i
<
16
;
i
++
)
{
{
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
iCof
=
(
pF
[(
i
*
nShift
)
/
64
]
>>
((
i
*
nShift
)
&
63
))
&
Mask
;
...
...
src/map/if/ifDec16.c
View file @
4ed89d00
...
@@ -331,7 +331,7 @@ static inline void If_CluFill( word * pIn, int nVars )
...
@@ -331,7 +331,7 @@ static inline void If_CluFill( word * pIn, int nVars )
{
{
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
int
w
,
nWords
=
If_CluWordNum
(
nVars
);
for
(
w
=
0
;
w
<
nWords
;
w
++
)
for
(
w
=
0
;
w
<
nWords
;
w
++
)
pIn
[
w
]
=
~
0
;
pIn
[
w
]
=
~
(
word
)
0
;
}
}
static
inline
void
If_CluCopy
(
word
*
pOut
,
word
*
pIn
,
int
nVars
)
static
inline
void
If_CluCopy
(
word
*
pOut
,
word
*
pIn
,
int
nVars
)
{
{
...
@@ -610,7 +610,7 @@ void If_CluInitTruthTables()
...
@@ -610,7 +610,7 @@ void If_CluInitTruthTables()
TruthAll
[
i
][
k
]
=
Truth6
[
i
];
TruthAll
[
i
][
k
]
=
Truth6
[
i
];
for
(
i
=
6
;
i
<
CLU_VAR_MAX
;
i
++
)
for
(
i
=
6
;
i
<
CLU_VAR_MAX
;
i
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
for
(
k
=
0
;
k
<
CLU_WRD_MAX
;
k
++
)
TruthAll
[
i
][
k
]
=
((
k
>>
(
i
-
6
))
&
1
)
?
~
0
:
0
;
TruthAll
[
i
][
k
]
=
((
k
>>
(
i
-
6
))
&
1
)
?
~
(
word
)
0
:
0
;
// Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" );
// Extra_PrintHex( stdout, TruthAll[6], 8 ); printf( "\n" );
// Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" );
// Extra_PrintHex( stdout, TruthAll[7], 8 ); printf( "\n" );
...
@@ -1081,11 +1081,11 @@ int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar )
...
@@ -1081,11 +1081,11 @@ int If_CluDetectSpecialCaseCofs( word * pF, int nVars, int iVar )
if
(
Cof0
==
0
)
if
(
Cof0
==
0
)
State
[
0
]
++
;
State
[
0
]
++
;
else
if
(
Cof0
==
~
0
)
else
if
(
Cof0
==
~
(
word
)
0
)
State
[
1
]
++
;
State
[
1
]
++
;
else
if
(
Cof1
==
0
)
else
if
(
Cof1
==
0
)
State
[
2
]
++
;
State
[
2
]
++
;
else
if
(
Cof1
==
~
0
)
else
if
(
Cof1
==
~
(
word
)
0
)
State
[
3
]
++
;
State
[
3
]
++
;
else
if
(
Cof0
==
~
Cof1
)
else
if
(
Cof0
==
~
Cof1
)
State
[
4
]
++
;
State
[
4
]
++
;
...
...
src/opt/dau/dauDsd.c
View file @
4ed89d00
...
@@ -95,7 +95,7 @@ word Dau_DsdToTruth_rec( char ** p )
...
@@ -95,7 +95,7 @@ word Dau_DsdToTruth_rec( char ** p )
assert
(
(
**
p
==
'<'
)
==
(
*
q
==
'>'
)
);
assert
(
(
**
p
==
'<'
)
==
(
*
q
==
'>'
)
);
if
(
**
p
==
'('
)
// and/or
if
(
**
p
==
'('
)
// and/or
{
{
Res
=
~
0
;
Res
=
~
(
word
)
0
;
for
(
(
*
p
)
++
;
*
p
<
q
;
(
*
p
)
++
)
for
(
(
*
p
)
++
;
*
p
<
q
;
(
*
p
)
++
)
Res
&=
Dau_DsdToTruth_rec
(
p
);
Res
&=
Dau_DsdToTruth_rec
(
p
);
}
}
...
@@ -126,7 +126,7 @@ word Dau_DsdToTruth( char * p )
...
@@ -126,7 +126,7 @@ word Dau_DsdToTruth( char * p )
if
(
*
p
==
'0'
)
if
(
*
p
==
'0'
)
Res
=
0
;
Res
=
0
;
else
if
(
*
p
==
'1'
)
else
if
(
*
p
==
'1'
)
Res
=
~
0
;
Res
=
~
(
word
)
0
;
else
else
Res
=
Dau_DsdToTruth_rec
(
&
p
);
Res
=
Dau_DsdToTruth_rec
(
&
p
);
assert
(
*++
p
==
0
);
assert
(
*++
p
==
0
);
...
@@ -239,7 +239,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
...
@@ -239,7 +239,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
pBuffer
[
Pos
++
]
=
')'
;
pBuffer
[
Pos
++
]
=
')'
;
return
Pos
;
return
Pos
;
}
}
if
(
Cof0
[
v
]
==
~
0
)
// !(ax)
if
(
Cof0
[
v
]
==
~
(
word
)
0
)
// !(ax)
{
{
pBuffer
[
Pos
++
]
=
'!'
;
pBuffer
[
Pos
++
]
=
'!'
;
pBuffer
[
Pos
++
]
=
'('
;
pBuffer
[
Pos
++
]
=
'('
;
...
@@ -257,7 +257,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
...
@@ -257,7 +257,7 @@ int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars
pBuffer
[
Pos
++
]
=
')'
;
pBuffer
[
Pos
++
]
=
')'
;
return
Pos
;
return
Pos
;
}
}
if
(
Cof1
[
v
]
==
~
0
)
// !(!ax)
if
(
Cof1
[
v
]
==
~
(
word
)
0
)
// !(!ax)
{
{
pBuffer
[
Pos
++
]
=
'!'
;
pBuffer
[
Pos
++
]
=
'!'
;
pBuffer
[
Pos
++
]
=
'('
;
pBuffer
[
Pos
++
]
=
'('
;
...
@@ -397,7 +397,7 @@ char * Dau_DsdPerform( word t )
...
@@ -397,7 +397,7 @@ char * Dau_DsdPerform( word t )
int
Pos
=
0
;
int
Pos
=
0
;
if
(
t
==
0
)
if
(
t
==
0
)
pBuffer
[
Pos
++
]
=
'0'
;
pBuffer
[
Pos
++
]
=
'0'
;
else
if
(
t
==
~
0
)
else
if
(
t
==
~
(
word
)
0
)
pBuffer
[
Pos
++
]
=
'1'
;
pBuffer
[
Pos
++
]
=
'1'
;
else
else
Pos
=
Dau_DsdPerform_rec
(
t
,
pBuffer
,
Pos
,
pVarsNew
,
6
);
Pos
=
Dau_DsdPerform_rec
(
t
,
pBuffer
,
Pos
,
pVarsNew
,
6
);
...
...
src/proof/ssw/sswRarity.c
View file @
4ed89d00
...
@@ -433,7 +433,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
...
@@ -433,7 +433,7 @@ int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
{
{
Ssw_RarMan_t
*
p
=
(
Ssw_RarMan_t
*
)
pMan
;
Ssw_RarMan_t
*
p
=
(
Ssw_RarMan_t
*
)
pMan
;
word
*
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
word
*
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
word
Flip
=
pObj
->
fPhase
?
~
0
:
0
;
word
Flip
=
pObj
->
fPhase
?
~
(
word
)
0
:
0
;
int
w
;
int
w
;
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
if
(
pSim
[
w
]
^
Flip
)
if
(
pSim
[
w
]
^
Flip
)
...
@@ -457,7 +457,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
...
@@ -457,7 +457,7 @@ int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
Ssw_RarMan_t
*
p
=
(
Ssw_RarMan_t
*
)
pMan
;
Ssw_RarMan_t
*
p
=
(
Ssw_RarMan_t
*
)
pMan
;
word
*
pSim0
=
Ssw_RarObjSim
(
p
,
pObj0
->
Id
);
word
*
pSim0
=
Ssw_RarObjSim
(
p
,
pObj0
->
Id
);
word
*
pSim1
=
Ssw_RarObjSim
(
p
,
pObj1
->
Id
);
word
*
pSim1
=
Ssw_RarObjSim
(
p
,
pObj1
->
Id
);
word
Flip
=
(
pObj0
->
fPhase
!=
pObj1
->
fPhase
)
?
~
0
:
0
;
word
Flip
=
(
pObj0
->
fPhase
!=
pObj1
->
fPhase
)
?
~
(
word
)
0
:
0
;
int
w
;
int
w
;
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
if
(
pSim0
[
w
]
^
pSim1
[
w
]
^
Flip
)
if
(
pSim0
[
w
]
^
pSim1
[
w
]
^
Flip
)
...
@@ -518,7 +518,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
...
@@ -518,7 +518,7 @@ unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
int
Ssw_RarManObjWhichOne
(
Ssw_RarMan_t
*
p
,
Aig_Obj_t
*
pObj
)
int
Ssw_RarManObjWhichOne
(
Ssw_RarMan_t
*
p
,
Aig_Obj_t
*
pObj
)
{
{
word
*
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
word
*
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
word
Flip
=
pObj
->
fPhase
?
~
0
:
0
;
word
Flip
=
pObj
->
fPhase
?
~
(
word
)
0
:
0
;
int
w
,
i
;
int
w
,
i
;
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
if
(
pSim
[
w
]
^
Flip
)
if
(
pSim
[
w
]
^
Flip
)
...
@@ -609,8 +609,8 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
...
@@ -609,8 +609,8 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
pSim0
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId0
(
pObj
)
);
pSim0
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId0
(
pObj
)
);
pSim1
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId1
(
pObj
)
);
pSim1
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId1
(
pObj
)
);
Flip0
=
Aig_ObjFaninC0
(
pObj
)
?
~
0
:
0
;
Flip0
=
Aig_ObjFaninC0
(
pObj
)
?
~
(
word
)
0
:
0
;
Flip1
=
Aig_ObjFaninC1
(
pObj
)
?
~
0
:
0
;
Flip1
=
Aig_ObjFaninC1
(
pObj
)
?
~
(
word
)
0
:
0
;
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
pSim
[
w
]
=
(
Flip0
^
pSim0
[
w
])
&
(
Flip1
^
pSim1
[
w
]);
pSim
[
w
]
=
(
Flip0
^
pSim0
[
w
])
&
(
Flip1
^
pSim1
[
w
]);
if
(
!
fUpdate
)
if
(
!
fUpdate
)
...
@@ -635,7 +635,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
...
@@ -635,7 +635,7 @@ void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int f
{
{
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
pSim
=
Ssw_RarObjSim
(
p
,
Aig_ObjId
(
pObj
)
);
pSim0
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId0
(
pObj
)
);
pSim0
=
Ssw_RarObjSim
(
p
,
Aig_ObjFaninId0
(
pObj
)
);
Flip
=
Aig_ObjFaninC0
(
pObj
)
?
~
0
:
0
;
Flip
=
Aig_ObjFaninC0
(
pObj
)
?
~
(
word
)
0
:
0
;
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
for
(
w
=
0
;
w
<
p
->
nWords
;
w
++
)
pSim
[
w
]
=
Flip
^
pSim0
[
w
];
pSim
[
w
]
=
Flip
^
pSim0
[
w
];
}
}
...
...
src/sat/cnf/cnfFast.c
View file @
4ed89d00
...
@@ -145,7 +145,7 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
...
@@ -145,7 +145,7 @@ word Cnf_CutDeriveTruth( Aig_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes
0xFFFF0000FFFF0000
,
0xFFFF0000FFFF0000
,
0xFFFFFFFF00000000
0xFFFFFFFF00000000
};
};
static
word
C
[
2
]
=
{
0
,
~
0
};
static
word
C
[
2
]
=
{
0
,
~
(
word
)
0
};
static
word
S
[
256
];
static
word
S
[
256
];
Aig_Obj_t
*
pObj
;
Aig_Obj_t
*
pObj
;
int
i
;
int
i
;
...
@@ -240,7 +240,7 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot,
...
@@ -240,7 +240,7 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot,
assert
(
Vec_PtrSize
(
vLeaves
)
<=
6
);
assert
(
Vec_PtrSize
(
vLeaves
)
<=
6
);
Truth
=
Cnf_CutDeriveTruth
(
p
,
vLeaves
,
vNodes
);
Truth
=
Cnf_CutDeriveTruth
(
p
,
vLeaves
,
vNodes
);
if
(
Truth
==
0
||
Truth
==
~
0
)
if
(
Truth
==
0
||
Truth
==
~
(
word
)
0
)
{
{
Vec_IntPush
(
vClauses
,
0
);
Vec_IntPush
(
vClauses
,
0
);
Vec_IntPush
(
vClauses
,
(
Truth
==
0
)
?
(
OutLit
^
1
)
:
OutLit
);
Vec_IntPush
(
vClauses
,
(
Truth
==
0
)
?
(
OutLit
^
1
)
:
OutLit
);
...
...
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