如何用 Z3 隐藏变量答案

【问题标题】：How to hide variable with Z3如何用 Z3 隐藏变量
【发布时间】：2012-07-22 10:44:47
【问题描述】：

说我有

t1<x and x<t2

是否可以隐藏变量 x 以便 t1<t2 在 Z3 中？

【问题讨论】：

标签： z3 smt

【解决方案1】：

使用Redlog的Redlog的可能解决方案：

【讨论】：

【解决方案2】：

您可以使用量词消除来做到这一点。这是一个例子：

(declare-const t1 Int)
(declare-const t2 Int)

(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))

您可以在线尝试此示例：http://rise4fun.com/Z3/kp0X

【讨论】：

谢谢，但为什么结果是 t1-t2
因为t1、t2 和x 是整数。对于整数，如果a < b 那么a <= b - 1。因此，结合不等式t1 <= x - 1 和x <= t2 - 1，我们得到t1 - t2 <= -2。如果我们将Int替换为Real，我们将得到一个等价于t1 - t2 < 0的公式。
这个答案似乎已经过时，因为它产生“不受支持”的结果（也在rise4fun上）