z3 - "pull-nested-quantifiers"选项似乎在 UFBV 的上下文中引起问题？

Question

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

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

对于两个语义相同的 SMT 规范 Spec1 和 Spec2，Z3 为证明 Spec1 超时(200 秒)但证明了 Spec2。

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

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

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

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

您可以找到:spec1 和 spec2 两个(我认为)语义相同的 SMT 规范，spec3 是使用“=”来建模“iff”的 SMT 规范，为此 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 逻辑”，以及许多额外的 aliases如: iff对于 bool = , if为 ite ， 等等。