向Z3提供简单的公理

Question

有没有办法告诉Z3一个逻辑公理可能适用于某种情况？ 例如，P（x）==> \存在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）==> \存在x P（x）以帮助Z3吗？这可能是我误解了这个例子中发生的事情。但根据我的有限理解，如果Z3实例化我提到的公理，Z3可能成功地证明公式不成立。

Answer 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指南中阅读有关quantifier patterns的更多信息。