z3 - 如何使用 Z3-Py 进行量词消除？

Question

我正在尝试使用以下代码获取无量词公式：

S, E, I, R = Reals('S E I R')
b, n, s, g, m = Reals('b n s g m')
SS = Then('qe', 'smt').solver()
SS.add(Exists([S,E,I,R], And(m+g*R-m*S-b*I*S == 0,
   b*I*S-(m+s)*E==0, s*E-(n+m)*I==0, n*I-(m+g)*R==0,
   S > 0, I > 0, E > 0, R >0)))
SS.add(b > 0, n > 0, s >0 , g >0, m>0)
print SS
print SS.check()

但我正在获得输出：

unknown

请你告诉我我的代码会发生什么？非常感谢。

Answer 1

量词消除仅适用于加法运算。它不会从变量与其他变量相乘的公式中消除量词。这就是为什么量词消除不会为您的问题生成简化公式的原因。

但是请注意，公式 Exists x 。phi[x] 等价于 phi[x] 形式的公式，因此不需要在公式上放置存在量词。nlsat 策略通过乘法处理实数上的无量词公式。