diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-25 12:17:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-25 12:17:12 -0700 |
| commit | a277d450bf7c624392d41739788f115f1d655556 (patch) | |
| tree | d24c5a50f62bbc12e0d93b1e78d5be9dfe65c80e /src/sat/bsat | |
| parent | c7bc6b63298f532270b6c696a6f36545429dfb52 (diff) | |
| download | abc-a277d450bf7c624392d41739788f115f1d655556.tar.gz abc-a277d450bf7c624392d41739788f115f1d655556.tar.bz2 abc-a277d450bf7c624392d41739788f115f1d655556.zip | |
Experiments with simulation-based engines.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satClause.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index d2ed3b75..74e685c3 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -88,7 +88,8 @@ static inline void Sat_MemWriteLimit( int * p, int nInts ) { p[0] = nI static inline int Sat_MemHandPage( Sat_Mem_t * p, cla h ) { return h >> p->nPageSize; } static inline int Sat_MemHandShift( Sat_Mem_t * p, cla h ) { return h & p->uPageMask; } -static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; } +//static inline int Sat_MemIntSize( int size, int lrn ) { return (size + 2 + lrn) & ~01; } +static inline int Sat_MemIntSize( int size, int lrn ) { return 2*((size + 2 + lrn)/2); } static inline int Sat_MemClauseSize( clause * p ) { return Sat_MemIntSize(p->size, p->lrn); } static inline int Sat_MemClauseSize2( clause * p ) { return Sat_MemIntSize(p->size, 1); } |