整数の線形演算とブール変数に対するいくつかのアサーションと、実際の非線形演算とブール変数に対するいくつかのアサーションを持つ SMT 式を作成したいと思います。整数と実数に対するアサーションは、ブール変数のみを共有します。例として、次の式を考えてみましょう。
(declare-fun b () Bool)
(assert (= b true))
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (or (not b) (>= (+ x y) (- x (+ (* 2 z) 1)))))
(declare-fun r () Real)
(assert (or (not b) (= (+ (* r r) (* 3 r) (- 4)) 0)))
この式を z3 に入力すると、すぐに「不明」と報告されます。しかし、その整数部分を削除すると、すぐに解が得られます。これは、変数 "r" の制約を満たします。これは、非線形制約自体がソルバーにとって難しくないことを意味していると思います。この問題は、整数に対する (線形) 制約と実数に対する (非線形) 制約の混在にあるはずです。
だから私の質問は次のとおりです。z3 を使用してこの種の混合数式を処理する正しい方法は何ですか (存在する場合)? DPLL(T) についての私の理解では、さまざまな制約に対してさまざまな理論ソルバーを使用して、そのような式を処理できるはずです。私が間違っている場合は、私を修正してください。