博士

ロボ子、今日のニュースは文字の分類をSIMD命令で高速化する話じゃ。

ロボ子

SIMD命令ですか。文字の分類を高速化するニーズがあるのですね。

博士

そうじゃ。例えば、base64デコード時にどの文字がbase64文字かを高速に識別する必要があるんじゃ。この記事によると、SIMD命令を使うと、標準的なルックアップテーブルが不向きになるらしいぞ。

ロボ子

なるほど。SIMD命令を使う場合は、別の方法が必要になるのですね。

博士

そこで、各文字のASCII値を上位と下位の4ビットニブルに分割し、16バイトのルックアップテーブルを使うんじゃ。`f(c) = lut_lo[c & 0x0F] AND lut_hi[c >> 4]`という関数で分類するらしい。

ロボ子

ルックアップテーブルを使うのは同じですが、計算方法が違うのですね。`lut_lo`と`lut_hi`の中身はどうやって決めるんですか？

博士

そこが面白いところじゃ！Z3のような定理証明器を使って、分類制約を充足可能性問題としてモデル化し、自動的に計算するんじゃ。

ロボ子

定理証明器ですか！そんなものが使えるんですね。具体的にはどうやるんですか？

博士

PythonでZ3をインポートして、`lut_lo`と`lut_hi`を表すビットベクトル変数を定義するんじゃ。そして、base64文字セットと無効な文字を定義して、制約をソルバーに追加する。「base64文字は0に分類する必要があり、無効な文字は0より大きい値に分類する必要がある」という制約じゃ。

ロボ子

なるほど。制約を定義して、ソルバーに解かせるんですね。すごい！

博士

Z3による解決例として、こんなテーブルが出てくるぞ。