z3 - 固定小数点をサポートするSMTツール

Question

フィックスポイントをサポートするZ3以外のsmtツールがあることを知っていますか？

Answer 1

不動点とは、ホーン節のクエリを解くことを意味していると思います。同様の性質の問題を解決するツールはたくさんありますが、まったく同じ形式ではない可能性があります。 Philippe SuterのLeonツールはさまざまなアルゴリズムを使用しており、再帰プログラムに対する多くの正しさのクエリを解決できます。Andrey RybalchenkoのARMCツールは、線形実数演算でもホーン式を解きます。また、終了条件を確立することもできます。タブ付きのCLPシステムは、Z3と同様の形式でクエリを解決するのにも適している必要があります（どちらも入力形式としてホーン式を使用します）。コンテキストに応じて使用できるシンボリックモデル検査ソルバーも多数あります。