Z3中警告消息背后的原因是什么：“未能找到量词的模式（量词id：k！18）”答案

【问题标题】：What is the reason behind the warning message in Z3: "failed to find a pattern for quantifier (quantifier id: k!18) "Z3中警告消息背后的原因是什么：“未能找到量词的模式（量词id：k！18）”
【发布时间】：2012-02-08 08:36:47
【问题描述】：

我发现以下简单 SMT-LIB 程序中显示的问题。

SMT-LIB 代码：

(declare-fun isDigit (Int) Bool)
(assert (forall ((x Int))
    (=>     (isDigit x)
        (and (>= x 0) (< x 10))
    )
  )
) 

(assert (forall ((x Int))   
    (=>     (and (>= x 12) (< x 15))
        (exists ((y Int))
            (and    (>= y 1) (< y 6)
                (isHost (- x y))
            )
        )
    )
  )
)

(check-sat)
(get-model)

这会给出以下警告：

WARNING: failed to find a pattern for quantifier (quantifier id: k!18)
sat
........
........

我想知道警告信息。我知道我错过了一些东西，但我无法理解。谁能帮我解决这个问题？

【问题讨论】：

标签： z3

【解决方案1】：

Z3 使用不同的引擎来处理量词（请参阅Z3 guide）。这些引擎之一基于模式匹配（E-Matching）。 Z3 尝试为每个量化公式推断模式。如果找不到，它会发出警告消息。用户还可以为每个量词提供模式。该指南显示了如何做到这一点。 id k!18 是 Z3 创建的默认 id。它基于行号（在您的情况下为第 18 行）。您还可以为量词提供自己的 ID。该警告只是告诉用户电子匹配引擎将无法处理指定的量词。

【讨论】：