z3 - 如何用 Z3 隐藏变量

Question

说我有

t1<x and x<t2

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

score 6 · Accepted Answer

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

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

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

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

score 2 · Accepted Answer

2

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

在此处输入图像描述

于 2013-07-28T20:31:05.713 回答

2 回答 2