4

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

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

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

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

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

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

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

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

4

1 回答 1

4

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

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

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

(set-option :print-warning false)

That being said, I will try to address the issues you raised. Does identifier names affect the behavior of Z3? Yes, they do. Starting at version 3.0, we started using a total order on Z3 expressions for performing operations such as: sorting the arguments of associative-commutative operators. This total order is based on the identifier names. Ironically, this modification was motivated by user feedback. In previous versions, we used an internal ID for performing operations such as sorting, and breaking ties in many different heuristics. However, these IDs are based on the order Z3 creates/deletes expressions, which is based on the order users declare symbols. So, Z3 2.x behavior would be affected by trivial modifications such as removing unused declarations.

Regarding iff, it is not part of SMT-LIB 2.0 standard. In SMT-LIB 2.0, = is used for formulas and terms. To make sure Z3 is fully compliant with the SMT-LIB 2.0 standard, whenever users specify a SMT-LIB supported logic (or soon to be supported such as UFBV), Z3 only "loads" the symbols defined in it. When, a logic is not specified, Z3 assumes the user is using the "Z3 logic" that contains all supported theories in Z3, and many extra aliases such as: iff for Boolean =, if for ite, etc.

于 2011-11-18T15:50:15.407 回答