说我有
t1<x and x<t2
是否可以隐藏变量 x 以便
t1<t2在Z3？
最佳答案
您可以使用量词消除来做到这一点。下面是一个例子:
(declare-const t1 Int)
(declare-const t2 Int)
(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))
您可以在线试用此示例:http://rise4fun.com/Z3/kp0X
关于z3 - 如何使用 Z3 隐藏变量，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/11625388/