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