“拉式嵌套量词”选项似乎会在 UFBV 上下文中引起问题？

Question

我目前正在尝试使用 Z3 作为用 Alloy（一种关系逻辑/语言）编写的规范的有界引擎。我使用 UFBV 作为目标语言。

我使用 Z3 选项 (set-option :pull-nested-quantifiers true) 检测到问题。

对于两个语义相同的 SMT 规范 Spec1 和 Spec2，Z3 在证明 Spec1 时超时（200 秒），但在证明 Spec2 时超时（200 秒）。

Spec1 和 Spec2 之间的唯一区别是它们具有不同的函数标识符（因为我使用 java 哈希名称）。这可能与错误有关吗？

我想分享和讨论的第二个观察结果是 UFBV 上下文中的“iff”运算符。如果设置了(set-logic UFBV)，则不支持此运算符。我的解决方案是使用“=”代替，但如果操作数包含深度嵌套量词并且设置了“pull-nested-quantifiers”，则这种方法效果不佳。另一个保护解决方案是使用双重蕴涵。

现在的问题是： UFBV 中的模型“iff”是否还有其他更好的解决方案，因为我认为，使用双重蕴涵通常会释放可能可用的语义信息以进行改进/简化。

http://i12www.ira.uka.de/~elghazi/tmp/

您可以找到：spec1 和 spec2 两个（我认为）语义相同的 SMT 规范，以及 spec3 使用“=”建模的 SMT 规范“iff”，z3 超时。

Answer 1

UFBV 逻辑的默认策略对您的问题无效。实际上，默认策略在不到 1 秒的时间内解决了所有问题。要强制 Z3 使用默认策略，您只需在脚本中注释以下行即可。

; (set-logic UFBV)
; (set-option :pull-nested-quantifiers true)
; (set-option :macro-finder true)

如果警告消息困扰您，您可以添加：

(set-option :print-warning false)

话虽这么说，我会尽力解决您提出的问题。
标识符名称会影响 Z3 的行为吗？是的，他们确实这么做了。
从版本 3.0 开始，我们开始在 Z3 表达式上使用全序来执行操作，例如：对关联交换运算符的参数进行排序。
该总顺序基于标识符名称。
讽刺的是，这一修改是由用户反馈推动的。在以前的版本中，我们使用内部 ID 来执行排序等操作，以及在许多不同的启发式中打破平局。然而，这些 ID 是基于 Z3 创建/删除表达式的顺序，而该顺序又基于用户声明符号的顺序。因此，Z3 2.x 的行为会受到一些细微修改的影响，例如删除未使用的声明。

关于iff，它不是SMT-LIB 2.0标准的一部分。在 SMT-LIB 2.0 中，= 用于公式和术语。为了确保 Z3 完全符合 SMT-LIB 2.0 标准，每当用户指定 SMT-LIB 支持的逻辑（或即将支持，例如 UFBV）时，Z3 仅“加载”其中定义的符号。当未指定逻辑时，Z3 假设用户正在使用“Z3 逻辑”，其中包含 Z3 中所有支持的理论，以及许多额外的别名，例如：iff for布尔值 =、if 代表 ite 等。