[数学]
SMT
- 「Satisfiability modulo theories」の略
- 定訳がなさそうなのだけど充足可能性モジュロ理論とかでいいのだろうか？
ざっくり言うと式を入れたら解を求めてくれるやつ
- 使用できるModulo Theories(=モジュロ理論)
- Linear Integer/Real Arithmetic
- 整数に関する線形の演算
- 普通の計算
- Non-linear Arithmetic
- Bit-Vector
- Bit束ねたもので固定長の整数に対する演算をサポート
- 数え上げ
- Uninterpreted Functions
- Arrays
- Quantifiers
- 量化記号∀, ∃を使うやつ
- Linear Integer/Real Arithmetic
SMT-LIB 2との対応