Skip to content

Commit

Permalink
Make lbool explicitly signed (#650)
Browse files Browse the repository at this point in the history
This avoids issues due to some platforms making `char` signed and others
unsigned. In particular, on platforms where `char` is unsigned,
https://github.com/lsils/mockturtle/blob/50ffa108484ba65b44eee4a713832b7ee821d6d8/lib/bill/bill/sat/interface/abc_bsat2.hpp#L156
promotes an `lbool` to `int` and compares to -1 ... but promoting
`(unsigned char)-1` to `int` produces 255.`
  • Loading branch information
rocallahan authored Jul 11, 2024
1 parent 50ffa10 commit 91e15a9
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 2 deletions.
4 changes: 3 additions & 1 deletion lib/abcsat/abc/satVec.h
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,9 @@ static inline void vecp_remove(vecp* v, void* e)
typedef int lit;
typedef int cla;

typedef char lbool;
// Explicitly make it signed so promotion-to-int behavior doesn't vary
// across platforms that define signedness of char differently.
typedef signed char lbool;

// CryptoMinisat defines it's own var_Undef values.
// When it's included we prefer the ABC version instead.
Expand Down
4 changes: 3 additions & 1 deletion lib/bill/bill/sat/solver/abc/satVec.h
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,9 @@ static inline void vecp_remove(vecp* v, void* e)
typedef int lit;
typedef int cla;

typedef char lbool;
// Explicitly make it signed so promotion-to-int behavior doesn't vary
// across platforms that define signedness of char differently.
typedef signed char lbool;

// CryptoMinisat defines it's own var_Undef values.
// When it's included we prefer the ABC version instead.
Expand Down

0 comments on commit 91e15a9

Please sign in to comment.