Z3/SMTLIB2 支持 `distinct`

Question

我一直在使用 (ML) z3 绑定(bind)和 API 函数

val mk_distinct : context -> ast array -> ast

多年来一直忠实地服务。我现在正在尝试切换
到 SMTLIB2 接口(interface)，但我发现 distinct命令
是 unsupported .例如，查询:

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

产生响应:

unsupported
; distinct  
sat

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

谢谢!

兰 git 。

Answer 1

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