Z3 / SMTLIB2 支持“distinct”

Question

我已经使用 (ML) z3 绑定一段时间了，API 函数

val mk_distinct : context -> ast array -> ast

多年来一直忠实服务。我现在尝试切换到 SMTLIB2 界面，但我发现该distinct命令是unsupported. 例如，查询：

(declare-fun x () Int)
(declare-fun y () Int)
(distinct x y)
(assert (= x y))
(check-sat)

产生响应：

unsupported
; distinct  
sat

在网络演示上。有一些解决方法吗？

谢谢！

兰吉特。

Answer 1

您应该使用(assert (distinct x y))而不是(distinct x y). 以下是更新示例的链接： http: //rise4fun.com/Z3/uVrX