`ite` 関数の対応

[private-yusuke]

ref: http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf

概要

QF_UF 理論では、if-then-else を表現するための関数 ite が事前に定義されている必要がある。

方針

現在の SMTSolver.expandLet のように、ite のところを展開する処理を入れる。これができるのは SAT ソルバーによる各式への真偽値割り当てが完了した後になる。 真偽値割り当てと Expression を与え、その真偽値割り当てのときの与えられた式の真偽値がどうなるか再帰的に追うような関数を用意し、それを利用して ite の第一引数の真偽値を取得したら、それが真なら第二引数を、偽なら第三引数を返すようにする。うまく工夫すればメモ化することができそうなので、型環境と式を持ったクラスを別に作って ite を助けてあげるようにするとスッキリする？

これをやるとして、ite の中に ite があったりする場合には何度も SAT ソルバーと理論ソルバーを動かす必要が出てきそう……。

(=> a b) （a => b）を表す ImpliesExpression を作り、(ite a b c) を (and (=> a b) (=> (not a) c)) で書き換えたらどうか。 ← ite 関数の引数は a が Bool で b と c が同一の Sort ならなんでも良いので、これではダメ

[private-yusuke]

例えば、 (= (f (ite e1 e2 e3)) x) のような制約は (or (and e1 (= (f e2) x)) (and (not e1) (= (f e3) x))) のように置換することで解けるようになる。このような挙動をうまく実装できれば愚直だが動くようになるはず。