问SMT中的混合理论

EN

我想要构造一个SMT公式，它包含一些关于整数、线性算法和布尔变量的断言，以及一些针对实际非线性算法和布尔变量的断言。整数和reals上的断言只共享布尔变量。作为一个例子，请考虑以下公式：

(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“的约束。我推测这意味着非线性约束本身对于求解者来说并不难。问题应该是整数上的(线性)约束和reals上的(非线性)约束。

所以我的问题如下。使用z3 (如果有的话)处理这种混合公式的正确方法是什么？我对DPLL(T)的理解是，它应该能够处理这样的公式，使用不同的理论求解器对不同的约束。如果我错了请纠正我。