QF_UF パーサー実装メモ
キーワード
declare-sort
自分の実装で2変数以上のときどうなってるんだっけ……
declare-const
まだ無いことにしておく(
declare-fun
とほぼ同じように扱えるのでそこそこ簡単だと思う)
declare-fun
assert
check-sat
get-model
let
簡易的な let 式のサポートを追加した。