“拉式嵌套量词"选项似乎在 UFBV 的上下文中引起问题? [英] The "pull-nested-quantifiers" option seems to cause problems in the context for UFBV?

问题描述

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

I am currently experimenting with Z3 as bounded engine for specifications written in Alloy (a relational logic/language). I am using the UFBV as target language.

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

I detect a problem using the Z3 option (set-option :pull-nested-quantifiers true).

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

For two semantically identical SMT specifications Spec1 and Spec2, Z3 times out (200 sec) for proving Spec1 but proves Spec2.

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

The only different between Spec1 and Spec2 is that they have different function identifiers (because I use java hash names). Can this be related to a bug?

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

The second observation I would like to share and discuss, is the "iff" operator in the context of UFBV. This operator is not supported, if (set-logic UFBV) is set. My solution was to use "=" instead but this do not work well if the operands contains deeply nested quantifiers and the "pull-nested-quantifiers" is set. The other saver solution is to use double implication.

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

Now the question: Is there any other better solution for model "iff" in UFBV, because I think, that using double implication will in general loose maybe useable semantic information for improvement/simplifications.

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

您可以找到:spec1 和 spec2 两个(我认为)语义相同的 SMT 规范，以及 spec3 使用="的 SMT 规范" 对 "iff" 建模，为此 z3 超时.

you can find: spec1 and spec2 the tow (I think) semantically identical SMT specifications, and spec3 an SMT specification using "=" to model "iff", for which z3 times out.

推荐答案

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

The default strategy for the UFBV logic is not effective for your problems. Actually, the default strategy solves all of them in less than 1 sec. To force Z3 to use the default strategy, you just need to comment the following lines in your script.

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

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

If the warning messages are bothering you, you can add:

(set-option :print-warning false)

话虽如此，我会尽力解决您提出的问题.标识符名称会影响 Z3 的行为吗?是的，他们这样做.从 3.0 版本开始，我们开始在 Z3 表达式上使用全序来执行操作，例如:对关联交换运算符的参数进行排序.此总顺序基于标识符名称.具有讽刺意味的是，这种修改的动机是用户反馈.在以前的版本中，我们使用内部 ID 来执行诸如排序和在许多不同启发式中打破联系之类的操作.但是，这些 ID 基于 Z3 创建/删除表达式的顺序，该顺序基于用户声明符号的顺序.因此，Z3 2.x 的行为会受到一些微不足道的修改的影响，例如删除未使用的声明.

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.

关于 iff，它不是 SMT-LIB 2.0 标准的一部分.在 SMT-LIB 2.0 中，= 用于公式和术语.为确保 Z3 完全符合 SMT-LIB 2.0 标准，每当用户指定 SMT-LIB 支持的逻辑(或即将支持的，例如 UFBV)时，Z3 仅加载"其中定义的符号.当未指定逻辑时，Z3 假定用户使用的Z3 逻辑"包含 Z3 中所有支持的理论，以及许多额外的 aliases 例如:iff forBoolean =, if for ite 等

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.

这篇关于“拉式嵌套量词"选项似乎在 UFBV 的上下文中引起问题?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！