You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 19, 2023. It is now read-only.
これをやるとして、ite の中に ite があったりする場合には何度も SAT ソルバーと理論ソルバーを動かす必要が出てきそう……。
(=> a b) (a => b)を表す ImpliesExpression を作り、(ite a b c) を (and (=> a b) (=> (not a) c)) で書き換えたらどうか。 ← ite 関数の引数は a が Bool で b と c が同一の Sort ならなんでも良いので、これではダメ
The text was updated successfully, but these errors were encountered:
ref: http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf
概要
QF_UF
理論では、if-then-else を表現するための関数ite
が事前に定義されている必要がある。方針
現在の
SMTSolver.expandLet
のように、ite
のところを展開する処理を入れる。これができるのは SAT ソルバーによる各式への真偽値割り当てが完了した後になる。真偽値割り当てと Expression を与え、その真偽値割り当てのときの与えられた式の真偽値がどうなるか再帰的に追うような関数を用意し、それを利用して
ite
の第一引数の真偽値を取得したら、それが真なら第二引数を、偽なら第三引数を返すようにする。うまく工夫すればメモ化することができそうなので、型環境と式を持ったクラスを別に作ってite
を助けてあげるようにするとスッキリする?これをやるとして、ite の中に ite があったりする場合には何度も SAT ソルバーと理論ソルバーを動かす必要が出てきそう……。
← ite 関数の引数は a が Bool で b と c が同一の Sort ならなんでも良いので、これではダメ(=> a b)
(a => b)を表す ImpliesExpression を作り、(ite a b c)
を(and (=> a b) (=> (not a) c))
で書き換えたらどうか。The text was updated successfully, but these errors were encountered: