z3 - 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