0

有没有办法告诉 Z3 一个逻辑公理可能适用于某种情况？例如，P(x) ==> \exists x P(x) 总是有效的。但是如果 P 足够复杂，那么 Z3 可能会感到困惑并说未知。

(declare-const size Int)
(declare-const h (Array Int Int))
(assert  (forall ((j Int) (k Int)) (=> (and (<= 0 k) (< k size) (<= 0 j) (< j size) (not (= k j))) (not (= (select h j) (select h k))))))
(assert (not (exists ((g (Array Int Int))) (forall ((j Int) (k Int)) (=> (and (<= 0 k) (< k size) (<= 0 j) (< j size) (not (= k j))) (not (= (select g j) (select g k))))))))
(check-sat)

第一个断言说 h 是一个将不同整数从 0..size-1 映射到不同整数的数组。第二个断言说这样的数组不存在。是否可以在 SMT 文件中提供简单有效的公理，例如 P(x) ==> \exists x P(x) 来帮助 Z3？可能是我误解了这个例子中发生的事情。但是根据我有限的理解，如果Z3实例化我提到的公理，它可能会成功证明这个公式是不饱和的。

4

1 回答 1

1

这似乎是一个触发问题，即 Z3 没有实例化存在量化的公理（也可能不是普遍量化的公理）。看看下面的简化示例：

(set-option :AUTO_CONFIG false)
(set-option :SMT.MBQI false)

(declare-fun f (Int) Bool)

(assert (forall ((x Int))
  (=> (<= 0 x) (f x))
))

(assert (not (exists ((x Int))
  (=> (<= 0 x) (f x))
)))

; (assert (f -10))

(check-sat)

Z3（版本 4.3.2，64 位，构建哈希码 96f4606a7f2d）报告unknown，但如果您取消注释最后一个断言，它会报告unsat。因此，我假设 Z3 为这两个公理推断的模式是:pattern ((f x))，这意味着它f x必须在句法上发生，然后才能实例化公理。

您可以在 z3 指南中阅读有关量词模式的更多信息。

于 2013-04-18T11:27:04.403 回答