我想构建一个 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) 的理解是，它应该能够使用针对不同约束的不同理论求解器来处理此类公式。如果我错了，请纠正我。