| 1 |
/*********************************************************************** |
| 2 |
* |
| 3 |
* file: simplify.c |
| 4 |
* |
| 5 |
* 論理式の簡単化(Quine-Mucluskey 法) |
| 6 |
* |
| 7 |
* $Id: simplify.c 185 2007-12-25 06:56:46Z chapuni $ |
| 8 |
* |
| 9 |
*/ |
| 10 |
|
| 11 |
#include <assert.h> |
| 12 |
#include <limits.h> |
| 13 |
#include <stdio.h> |
| 14 |
#include <stdlib.h> |
| 15 |
#include <string.h> |
| 16 |
|
| 17 |
#include "debug.h" |
| 18 |
#include "simplify.h" |
| 19 |
#include "util.h" |
| 20 |
|
| 21 |
/*************************************************************** |
| 22 |
* |
| 23 |
* 必須主項が前へ来るようにソート |
| 24 |
* |
| 25 |
*/ |
| 26 |
|
| 27 |
static |
| 28 |
int |
| 29 |
cmp_minterm_cov(void const *va, void const *vb) |
| 30 |
{ |
| 31 |
uint64_t a = *(uint64_t const *)va; |
| 32 |
uint64_t b = *(uint64_t const *)vb; |
| 33 |
return popcnt64(a) - popcnt64(b); |
| 34 |
} |
| 35 |
|
| 36 |
/*************************************************************** |
| 37 |
* |
| 38 |
* 被覆表から最小被覆を取り出す |
| 39 |
* |
| 40 |
* cov[] の 1 ワードを和項とみなすと |
| 41 |
* 各々 1 ビットづつ拾うという概念。 |
| 42 |
* |
| 43 |
* すでに拾われたビット(cand)を含む項はスキップ可能。 |
| 44 |
* |
| 45 |
*/ |
| 46 |
|
| 47 |
static |
| 48 |
uint64_t |
| 49 |
extract_mincov(uint64_t const *cov, /* 被覆表 */ |
| 50 |
int covn, /* 被覆表要素数 */ |
| 51 |
uint64_t cand, /* 決定している被覆候補 */ |
| 52 |
int min) /* 最小記録 */ |
| 53 |
{ |
| 54 |
int candn; |
| 55 |
int candni; |
| 56 |
uint64_t c; |
| 57 |
uint64_t b; |
| 58 |
uint64_t r = ~0ULL; |
| 59 |
|
| 60 |
/* cand の項数は、ビット数そのもの */ |
| 61 |
candn = popcnt64(cand); |
| 62 |
|
| 63 |
/* cand に含まれている、すなわちすでに候補がある項は |
| 64 |
決定済みとみなせるのでスキップする */ |
| 65 |
do |
| 66 |
{ |
| 67 |
/* 表のケツまでなめきったら判定 */ |
| 68 |
if (covn == 0) |
| 69 |
return (min > candn |
| 70 |
? cand |
| 71 |
: r); |
| 72 |
} |
| 73 |
while (--covn, ((c = *cov++) & cand)); |
| 74 |
|
| 75 |
/* 以降は、候補から項がひとつ、 |
| 76 |
すなわちビットがひとつ増えたものを扱う */ |
| 77 |
candni = candn + 1; |
| 78 |
|
| 79 |
for (b = 1ULL; b; b <<= 1) |
| 80 |
{ |
| 81 |
int n; |
| 82 |
uint64_t m; |
| 83 |
|
| 84 |
if (!(c & b)) |
| 85 |
continue; |
| 86 |
|
| 87 |
/* 最小記録を更新できないと判断した場合 */ |
| 88 |
if (min <= candni) |
| 89 |
return r; |
| 90 |
|
| 91 |
/* この処理は省いても構わないが、 |
| 92 |
再帰深度をちょっとだけ和らげ、高速化につながる */ |
| 93 |
if (covn == 0) |
| 94 |
return cand | b; |
| 95 |
|
| 96 |
/* 後段を計算させてみる。 |
| 97 |
min を更新できなかった場合は ~0ULL が返る */ |
| 98 |
m = extract_mincov(cov, covn, cand | b, min); |
| 99 |
n = popcnt64(m); |
| 100 |
if (min > n) |
| 101 |
{ |
| 102 |
/* 記録更新 */ |
| 103 |
min = n; |
| 104 |
r = m; |
| 105 |
} |
| 106 |
} |
| 107 |
|
| 108 |
/* 記録が更新できなかったら ~0ULL が返ることになる */ |
| 109 |
return r; |
| 110 |
} |
| 111 |
|
| 112 |
/*************************************************************** |
| 113 |
* |
| 114 |
* Quine-McCluskey 法により bmp を簡単化する |
| 115 |
* |
| 116 |
* 概算項数を返す |
| 117 |
* あきらめたときは INT_MAX を返し、全主項を生成する |
| 118 |
* |
| 119 |
* aox に積和形による結果を返す(m==0 terminated) |
| 120 |
* |
| 121 |
*/ |
| 122 |
|
| 123 |
#define QMX_N_ELIM 0x80 /* QMX::n における削除印 */ |
| 124 |
|
| 125 |
int |
| 126 |
simplify_qm(struct QMX *aox, |
| 127 |
uint64_t bmp, /* 真理値表 */ |
| 128 |
uint64_t dc) /* 1 のビットは D/C */ |
| 129 |
{ |
| 130 |
int i, j; |
| 131 |
uint64_t m; |
| 132 |
int n_dcs; /* D/C の個数 */ |
| 133 |
|
| 134 |
/* 戻り値: 概算出力項数 */ |
| 135 |
int n_estimated_terms; |
| 136 |
|
| 137 |
/* 最小項 */ |
| 138 |
int n_minterms; |
| 139 |
struct QMX minterms[QMX_LEN]; |
| 140 |
uint64_t minterm_cov[QMX_LEN]; /* 被覆 */ |
| 141 |
uint64_t covered_minterms; /* 必須主項が被覆する最小項 */ |
| 142 |
|
| 143 |
/* 主項 */ |
| 144 |
int n_pterms; |
| 145 |
struct QMX atmx[256 * QMX_LEN]; /* 64k を超えないくらいが目安? */ |
| 146 |
int max_pterms = sizeof(atmx) / sizeof(struct QMX); |
| 147 |
struct QMX *pterms = atmx; |
| 148 |
|
| 149 |
/* 必須主項およびその被覆 */ |
| 150 |
uint64_t essential_pterms; /* 必須主項 */ |
| 151 |
int n_essential_pterms; /* 必須主項項数 */ |
| 152 |
|
| 153 |
/* 主項算出用に, D/C 項を列挙する */ |
| 154 |
n_dcs = 0; |
| 155 |
for (i = 0; i < QMX_LEN; i++) |
| 156 |
if (dc & (1ULL << i)) |
| 157 |
{ |
| 158 |
pterms[n_dcs ].m = QMX_N_MASK; |
| 159 |
pterms[n_dcs++].n = i; |
| 160 |
} |
| 161 |
|
| 162 |
/* 最小項(1 の項)を列挙する */ |
| 163 |
bmp &= ~dc; |
| 164 |
n_minterms = 0; |
| 165 |
for (i = 0; i < QMX_LEN; i++) |
| 166 |
if (bmp & (1ULL << i)) |
| 167 |
{ |
| 168 |
minterms[n_minterms ].m = QMX_N_MASK; |
| 169 |
minterms[n_minterms++].n = i & QMX_N_MASK; |
| 170 |
} |
| 171 |
|
| 172 |
debug_printf(2, F016LLX"/"F016LLX" n_minterms=%d n_dcs=%d\n", |
| 173 |
A016LLX(bmp), |
| 174 |
A016LLX(dc), |
| 175 |
n_minterms, n_dcs); |
| 176 |
|
| 177 |
#define C(i,s) (pterms[i].m & (1 << (s)) ? (pterms[i].n & (1 << (s)) ? '1' : '0') : '-') |
| 178 |
|
| 179 |
/* 頭の悪い総当たりで主項を求める */ |
| 180 |
memcpy(&pterms[n_dcs], minterms, n_minterms * sizeof(struct QMX)); |
| 181 |
n_pterms = n_minterms + n_dcs; |
| 182 |
do |
| 183 |
{ |
| 184 |
int pterm_idx = n_pterms; |
| 185 |
|
| 186 |
/* 距離が近いものを主項として抜き出す */ |
| 187 |
for (i = 0; i < n_pterms; i++) |
| 188 |
for (j = i + 1; j < n_pterms; j++) |
| 189 |
{ |
| 190 |
int k; |
| 191 |
unsigned x; |
| 192 |
if (pterms[i].m != pterms[j].m) |
| 193 |
continue; |
| 194 |
x = (pterms[i].n ^ pterms[j].n) & pterms[i].m; |
| 195 |
assert(x != 0); /* 前ステージにて除去済みのハズ */ |
| 196 |
if (!IS_POWER2(x)) |
| 197 |
continue; |
| 198 |
/* ハミング距離が1なので項をまとめる |
| 199 |
異なるビットからマスクを生成 */ |
| 200 |
x = QMX_N_MASK & ~x; |
| 201 |
/* 同一項は再生成しないように(節約) */ |
| 202 |
for (k = n_pterms; k < pterm_idx; k++) |
| 203 |
if (pterms[k].m == (pterms[i].m & x) |
| 204 |
&& pterms[k].n == (pterms[i].n & x)) |
| 205 |
goto tmx_dup; |
| 206 |
/* 項をケツに登録 */ |
| 207 |
pterms[pterm_idx ].m = pterms[i].m & x; |
| 208 |
pterms[pterm_idx++].n = pterms[i].n & x; |
| 209 |
assert (pterm_idx <= max_pterms); |
| 210 |
if (pterm_idx == max_pterms) |
| 211 |
{ |
| 212 |
/* pterms の拡張 |
| 213 |
ローカル領域をはみ出たらヒープから取得 */ |
| 214 |
assert(max_pterms < INT_MAX / sizeof(struct QMX) / 2); |
| 215 |
max_pterms *= 2; |
| 216 |
if (pterms == atmx) |
| 217 |
{ |
| 218 |
pterms = malloc(max_pterms * sizeof(struct QMX)); |
| 219 |
memcpy(pterms, atmx, sizeof(atmx)); |
| 220 |
debug_printf(1, "allocated: %d->%d\n", pterm_idx, max_pterms); |
| 221 |
} |
| 222 |
else |
| 223 |
{ |
| 224 |
pterms = realloc(pterms, max_pterms * sizeof(struct QMX)); |
| 225 |
debug_printf(1, "extended: %d->%d\n", pterm_idx, max_pterms); |
| 226 |
} |
| 227 |
} |
| 228 |
tmx_dup: |
| 229 |
/* まとめあげられた項に削除印(とりあえずMSB) */ |
| 230 |
pterms[i].n |= QMX_N_ELIM; |
| 231 |
pterms[j].n |= QMX_N_ELIM; |
| 232 |
} |
| 233 |
|
| 234 |
/* 抜き出されたものから重複を除去しておく */ |
| 235 |
for (i = 0; i < pterm_idx; i++) |
| 236 |
for (j = i + 1; j < pterm_idx; j++) |
| 237 |
if (pterms[i].m == pterms[j].m |
| 238 |
&& ((pterms[i].n ^ pterms[j].n) & QMX_N_MASK) == 0) |
| 239 |
{ |
| 240 |
pterms[i].n |= QMX_N_ELIM; |
| 241 |
break; /* next i */ |
| 242 |
} |
| 243 |
|
| 244 |
/* 削除されたものを捨てる |
| 245 |
頭から順不同で詰めていく感じ */ |
| 246 |
for (i = j = 0; i < pterm_idx; i++) |
| 247 |
if (!(pterms[i].n & QMX_N_ELIM)) |
| 248 |
{ |
| 249 |
if (i != j) |
| 250 |
pterms[j] = pterms[i]; |
| 251 |
j++; |
| 252 |
} |
| 253 |
|
| 254 |
debug_printf(2, "n_pterms=%d pterm_idx=%d j=%d\n", n_pterms, pterm_idx, j); |
| 255 |
n_pterms = j; |
| 256 |
} |
| 257 |
while (i != j); |
| 258 |
|
| 259 |
/* 各最小項において、主項による被覆表を生成 |
| 260 |
必須主項を検出し、必須主項被覆を記録 */ |
| 261 |
memset(minterm_cov, 0, n_minterms * sizeof(*minterm_cov)); |
| 262 |
assert(n_minterms <= 64); |
| 263 |
assert(n_pterms <= 64); |
| 264 |
essential_pterms = 0; |
| 265 |
covered_minterms = 0; |
| 266 |
for (i = 0; i < n_minterms; i++) |
| 267 |
{ |
| 268 |
int ep = -1; /* 必須主項の場所 */ |
| 269 |
for (j = 0; j < n_pterms; j++) |
| 270 |
if ((minterms[i].m & pterms[j].m) == pterms[j].m |
| 271 |
&& (minterms[i].n & pterms[j].m) == (pterms[j].n & pterms[j].m)) |
| 272 |
minterm_cov[i] |= 1ULL << (ep = j); |
| 273 |
|
| 274 |
if (ep >= 0 |
| 275 |
&& IS_POWER2(minterm_cov[i])) |
| 276 |
{ |
| 277 |
/* 必須主項が被覆するものをマーキングする */ |
| 278 |
for (j = 0; j < n_minterms; j++) |
| 279 |
if ((minterms[j].m & pterms[ep].m) == pterms[ep].m |
| 280 |
&& (minterms[j].n & pterms[ep].m) == (pterms[ep].n & pterms[ep].m)) |
| 281 |
{ |
| 282 |
essential_pterms |= 1ULL << ep; |
| 283 |
covered_minterms |= 1ULL << j; |
| 284 |
} |
| 285 |
} |
| 286 |
} |
| 287 |
|
| 288 |
/* 主項-最小項マトリクスのダンプ; for debug */ |
| 289 |
#if DEBUG>=1 |
| 290 |
printf(" "); |
| 291 |
for (j = 0; j < n_minterms; j++) |
| 292 |
if (IS_POWER2(minterm_cov[j])) |
| 293 |
printf("*"); |
| 294 |
else if (covered_minterms & (1ULL << j)) |
| 295 |
printf("+"); |
| 296 |
else |
| 297 |
printf("#"); |
| 298 |
printf("\n"); |
| 299 |
|
| 300 |
for (i = 0; i < n_pterms; i++) |
| 301 |
{ |
| 302 |
printf("%3d: %c%c%c%c%c%c: ", |
| 303 |
i, |
| 304 |
C(i,5), C(i,4), C(i,3), C(i,2), C(i,1), C(i,0)); |
| 305 |
for (j = 0; j < n_minterms; j++) |
| 306 |
if (minterm_cov[j] & (1ULL << i)) |
| 307 |
{ |
| 308 |
if (IS_POWER2(minterm_cov[j])) |
| 309 |
{ |
| 310 |
assert(covered_minterms & (1ULL << j)); |
| 311 |
printf("*"); |
| 312 |
} |
| 313 |
else if (covered_minterms & (1ULL << j)) |
| 314 |
printf("+"); |
| 315 |
else |
| 316 |
printf("#"); |
| 317 |
} |
| 318 |
else |
| 319 |
{ |
| 320 |
printf("-"); |
| 321 |
} |
| 322 |
printf("\n"); |
| 323 |
} |
| 324 |
#endif |
| 325 |
|
| 326 |
/* 主項が64個を超えてしまった場合、あきらめる(マジカヨ) */ |
| 327 |
if (n_pterms > 64) |
| 328 |
return INT_MAX; |
| 329 |
|
| 330 |
/* 被覆表の重複を取り除く */ |
| 331 |
n_estimated_terms = 1; |
| 332 |
for (i = 0; i < n_minterms; i++) |
| 333 |
{ |
| 334 |
for (j = i + 1; j < n_minterms; j++) |
| 335 |
if (minterm_cov[i] == minterm_cov[j]) |
| 336 |
{ |
| 337 |
minterm_cov[j] = minterm_cov[--n_minterms]; |
| 338 |
j--; continue; /* redo */ |
| 339 |
} |
| 340 |
if (minterm_cov[i]) |
| 341 |
n_estimated_terms *= popcnt64(minterm_cov[i]); |
| 342 |
} |
| 343 |
|
| 344 |
debug_printf(2, |
| 345 |
"n_minterms=%d n_pterms=%d n_estimated_terms=%d\n", |
| 346 |
n_minterms, n_pterms, n_estimated_terms); |
| 347 |
|
| 348 |
#if DEBUG>=2 |
| 349 |
for (i = 0; i < n_minterms; i++) |
| 350 |
if (minterm_cov[i]) |
| 351 |
printf("%2d: "F016LLX"\n", i, A016LLX(minterm_cov[i])); |
| 352 |
#endif |
| 353 |
|
| 354 |
/* ビット数の小さいものから(==必須主項が前へ) |
| 355 |
ソートすることにより、計算がぐっと楽になる(ハズ) */ |
| 356 |
qsort(minterm_cov, n_minterms, sizeof(*minterm_cov), cmp_minterm_cov); |
| 357 |
|
| 358 |
/* 最小被覆の抽出 |
| 359 |
(最小なのか?) |
| 360 |
耐えきれなかったら全主項を選択した状態となる */ |
| 361 |
m = extract_mincov(minterm_cov, |
| 362 |
n_minterms, |
| 363 |
0ULL, |
| 364 |
64); |
| 365 |
#if DEBUG>=1 |
| 366 |
debug_printf(1, |
| 367 |
"ess:"F016LLX" cov:"F016LLX" all:"F016LLX"\n", |
| 368 |
A016LLX(essential_pterms), |
| 369 |
A016LLX(m & ~essential_pterms), |
| 370 |
A016LLX(m)); |
| 371 |
assert((m & essential_pterms) == essential_pterms); |
| 372 |
#endif |
| 373 |
essential_pterms = m; |
| 374 |
|
| 375 |
/* 結果を展開 */ |
| 376 |
n_estimated_terms = n_essential_pterms = popcnt64(essential_pterms); |
| 377 |
essential_pterms &= ((1ULL << n_pterms) - 1); |
| 378 |
j = 0; |
| 379 |
for (i = 0; i < n_pterms; i++) |
| 380 |
if (essential_pterms & (1ULL << i)) |
| 381 |
{ |
| 382 |
n_estimated_terms += popcnt32(pterms[i].m); |
| 383 |
if (aox) |
| 384 |
aox[j++] = pterms[i]; |
| 385 |
|
| 386 |
debug_printf(2, "%c%c%c%c%c%c:%3d\n", |
| 387 |
C(i,5), C(i,4), C(i,3), C(i,2), C(i,1), C(i,0), |
| 388 |
n_estimated_terms); |
| 389 |
|
| 390 |
assert(j <= QMX_LEN); |
| 391 |
} |
| 392 |
|
| 393 |
/* たぶん番人 */ |
| 394 |
if (aox && j < QMX_LEN) |
| 395 |
aox[j].m = 0; |
| 396 |
|
| 397 |
debug_printf(1, "nterm=%d j=%d\n", n_estimated_terms, j); |
| 398 |
|
| 399 |
#if DEBUG>=1 |
| 400 |
if (aox) |
| 401 |
{ |
| 402 |
/* 生成された式の検算 */ |
| 403 |
static const uint64_t a6[] = |
| 404 |
{ |
| 405 |
0xAAAAAAAAAAAAAAAAULL, |
| 406 |
0xCCCCCCCCCCCCCCCCULL, |
| 407 |
0xF0F0F0F0F0F0F0F0ULL, |
| 408 |
0xFF00FF00FF00FF00ULL, |
| 409 |
0xFFFF0000FFFF0000ULL, |
| 410 |
0xFFFFFFFF00000000ULL, |
| 411 |
}; |
| 412 |
uint64_t o = 0; |
| 413 |
for (i = 0; aox[i].m; i++) |
| 414 |
{ |
| 415 |
uint64_t a = 0xFFFFFFFFFFFFFFFFULL; |
| 416 |
for (j = 0; j < 6; j++) |
| 417 |
if (aox[i].m & (1 << j)) |
| 418 |
a &= (aox[i].n & (1 << j) |
| 419 |
? a6[j] |
| 420 |
: ~a6[j]); |
| 421 |
o |= a; |
| 422 |
} |
| 423 |
debug_eprintf(1, "bmp="F016LLX", o="F016LLX", dc="F016LLX"\n", |
| 424 |
A016LLX(bmp), |
| 425 |
A016LLX(o), |
| 426 |
A016LLX(dc)); |
| 427 |
assert(((bmp ^ o) & ~dc) == 0); |
| 428 |
} |
| 429 |
#endif |
| 430 |
|
| 431 |
/* pterms が拡張されている場合のあとしまつ */ |
| 432 |
if (pterms != atmx) |
| 433 |
free(pterms); |
| 434 |
|
| 435 |
/* 全部展開してしまった場合 */ |
| 436 |
return (n_essential_pterms > n_pterms ? INT_MAX : n_estimated_terms); |
| 437 |
} |
| 438 |
|
| 439 |
/* |
| 440 |
* Local Variables: |
| 441 |
* tab-width: 4 |
| 442 |
* End: |
| 443 |
* |
| 444 |
* EOF */ |
Parent Directory
Revision Log