如何用Z3隐藏变量

Question

说我有

t1<x and x<t2

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

Answer 1

你可以使用量词消除来做到这一点.这是一个例子:

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

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

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