wil*_*007 5 smt z3
说我有
t1<x and x<t2
是否可以隐藏变量x以便 t1<t2 在Z3中？
t1<t2
Leo*_*ura 6
你可以使用量词消除来做到这一点.这是一个例子:
(declare-const t1 Int) (declare-const t2 Int) (elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))
您可以在线试用此示例:http://rise4fun.com/Z3/kp0X
归档时间：
13 年，5 月 前
查看次数：
437 次
最近记录：
12 年，5 月 前