SMTソルバ
SMT(satisfiability modulo theories)
充足可能性モジュロ理論?
モジュロはどういう意味なのだろうか
SATソルバではできなかったことができる、より広範囲に適用できるやつ
算術演算
データ構造
ビットベクトル(bit-vectors)
配列
文字列
代数データ型
浮動小数点
etc
SMT LIBのページに対応しているものっぽいのが書かれていた
SMT-LIB The Satisfiability Modulo Theories Library
SMTソルバは、与えられたSMT問題が充足可能(SAT) か充足不能 (UNSAT)かを判定するソフトウェア
述語論理を使って解くらしい
いろいろな算術演算や各データ構造を処理するソルバは、理論ソルバと呼ばれる
ソフトウェア
Z3
cvc5
Alt-Ergo
その他のソフトウェアのリストはこっちが詳しそう
→Satisfiability modulo theories - Wikipedia
SMT LIB
SMTソルバの競技ページ
SMT-COMP 2023 | SMT-COMP
toysolverというSMTソルバの実装例
GitHub - msakai/toysolver: My sandbox for experimenting with solver algorithms.
確認用
Q. SMTソルバ
参考
事前に問題を検出できる仕組み SATソルバとSMTソルバによる充足可能性判定 - ログミーTech
★SAT/SMTソルバの仕組み
Satisfiability modulo theories - Wikipedia
★SAT技術の進化と応用 〜パズルからプログラム検証まで〜:7. SMTソルバーによるプログラム検証 情報学広場:情報処理学会電子図書館
SAT/SMTソルバを自作してみる話 - るくすの日記 ~ Out_Of_Range ~
関連
LiquidHaskell
AWS Tiros
IAM Access Analyzer
Zelkova