Bit Vectorを命題論理に変換する作業。例えばl-bitのaとbがあって、a or bという項は それぞれの1bitごとに、a[i] or b[i]を取ってandという事になる。 足し算x + yは同様に1 bitごとに考えれば良いが桁上がりなどがあるので、半加算器を考える必要がある。 a=x[i],b=y[i]とすると、 s ≡ (a + b + i ) mod 2 ≡ a ⊕ b ⊕ i o ≡ (a + b + i ) div 2 ≡ a · b + a · i + b · i となって、これをTseitin encodingでCNFにすると、 (a ∨ b ∨ ¬o) ∧ (a ∨ ¬b ∨ i ∨ ¬o) ∧ (a ∨ ¬b ∨ ¬i ∨ o)∧ (¬a ∨ b ∨ i ∨ ¬o) ∧ (¬a ∨ b ∨ ¬i ∨ o) ∧ (¬a ∨ ¬b ∨ o) となる。つまり1 bitの加算でもこれだけのCNFになる。 x+yの全bitについて考えるとさらに増える。 掛け算は11000個のリテラルになって現状のSAT solverでは解けない。
stpでは項はBBTermで、1-bitがBBNode、n-bitをBBNodeVecとする。BBNodeVec[0]が0-bit目。 blasterされた結果の命題論理はBBNode配列のポインタで返される。 大体の流れはSMTLIB2とかの外部ファイルをパースしてASTに変換。lib/ToSat/BitBlaster.cppでASTを 走査しつつ得たterm等の演算の種類をGetKindで取得してBit Vectorから命題論理への変換をそれぞれ行う。 BitBlasterクラスはBitBlaster<ASTNode, BBNodeManagerASTNode>かBitBlaster<BBNodeAIG, BBNodeManagerAIG> を使用する。前者は通常のASTNode、後者はBBNodeAIGというAIG(And-inverter graph)形式のノード。BitBlasterで まずSMTLIB2構文の比較演算子等を同値なAND,OR,XORなどの扱いやすい命題論理に変換する。この変換した後のノード がASTNodeになるかAIGになるかという話。その後ToSat/ASTNode/ASTtoCNF.cでCNFに変換。
構文解析はflex,bison使ってlex*.cppとparse*.cppを生成する。 ちなみにlib/Parser/smt2.yの構文解析の中でASTNodeを生成するようなコードを埋め込んでる。 BitBlasterで論理式に変換。ASTtoCNFでTseting EncodingでCNFに変換してSATに投げる。 tools/stp/main_common.cppで入力ファイルをパースしてASTに変換して順次stp->TopLevelSTP() に投げていく。(lib/STPManager.cpp)のTopLevelSTPからsolve_by_sat_solver()->TopLevelSTPAux で、inputToSatにASTを代入。このinputToSatをPropagateEqualities等でなるべく簡易化していき、 bb.BBForm(inputToSat)でBitBlasting開始。その後CallSAT_ResultCheckにBitBlastingに よって変化したmodified_inputとそのままのoriginal_inputの両方をCallSAT_ResultCheckに渡す。そこからCallSAT(lib/ToSat/ASTNode/ToSAT.cpp)してconvertToCNF(ASTToCNF.cpp)でCNFに変換する。 BitBlasting(lib/ToSat.c)ではBBNodeManagerのnfやNodeFactoryのASTNFでノード群を作成してresultで返す。