Z3 是否支持量化公式中的仅变量模式？

Question

我想使用仅变量模式来获得使用量化公理编码的某些理论的决策程序。更准确地说，我想强制这些公理中的某些变量用相应类别的所有项来实例化。这些变量只出现在谓词符号下方，因此不会产生匹配循环的危险。

例如，考虑以下部分查询：

(declare-sort Loc 0)
(declare-sort Map 2)
(declare-fun read ((Map Loc Loc) Loc) Loc)
(declare-fun Btwn ((Map Loc Loc) Loc Loc Loc) Bool)
... 
(assert (forall ((?f (Map Loc Loc)) (?x Loc) (?y Loc))
           (or (not (= (read ?f ?x) ?x)) (not (Btwn ?f ?x ?y ?y)) (= ?x ?y))))

在公理中，我想将变量 ?f 和 ?x 实例化为与 read ?f ?x 匹配的所有基本项，并将变量 ?y 与所有排序项 Loc 实例化。

如果我在公理中添加以下多模式：

:pattern ((read ?f ?x) ?y)

然后 Z3 报告仅变量模式 ?y 的错误。如果我在模式中省略?y，如下所示：

:pattern ((read ?f ?x))

然后 Z3 报告一个警告，指出并非所有变量都出现在模式中。似乎无法抑制此警告。此外，在这种情况下，我不确定该模式是否真的产生了预期的实例化。有没有一种解决方案可以为我提供我正在寻找的实例（没有警告）？

请注意，我感兴趣的理论不属于 MBQI 单独产生决策过程的任何片段（据我所知）。我可以预先部分实例化公理以获得 EPR 理论（这是我目前所做的），但我更希望求解器为我做这件事。

Answer 1

基于模式的实例化引擎要求变量在函数符号的范围内。否则，一个变量可以匹配任何适当类型的基础术语，这不能很好地工作，特别是当实例化创建与变量相同类型的新术语时。 您在 Z3 中可以做的是指定一个使用两个谓词的多模式：((read ?f ?x) (Btwn ?f ?x ?y ?y))。您还可以指定原始问题中没有出现的辅助谓词。 例如，谓词 (Known ?y)。您还必须添加公理来控制您想知道哪些术语。然后你可以使用多模式 ((read ?f ?x) (known ?y))。当然，这通常会比第一个多模式创建更多的实例化。