z3 - 在 Z3 中创建传递而非自反函数

Question

我正在尝试在 Z3 中创建一个传递但不自反的函数。 IE。如果(transitive a b)和(transitive b c)然后按住(transitive a c)应该成立，但是(transitive a a)不应该。

我尝试按照以下方式进行操作，进行了 5 次“测试”。第一个符合我的预期，但第二个失败并导致 unknown 。

(declare-datatypes () ((T T1 T2 T3)))

(declare-fun f (T T) Bool)
(assert(f T1 T2))
(assert(f T2 T3))

; Make sure that f is not reflexive
(assert
  (forall ((x T))
    (not (f x x))))

; Now we create the transitivity function ourselves
(define-fun-rec transitive ((x T) (y T)) Bool
    (or 
        (f x y)
        (exists ((z T))
            (and 
                (f x z)
                (transitive z y)))))

; This works and gives sat
(push)
(assert (not (transitive T1 T1)))
(assert (not (transitive T2 T2)))
(assert (not (transitive T3 T3)))
(check-sat)
(pop)

; This fails with "unknown" and the verbose flag gives: (smt.mbqi "max instantiations 1000 reached")
(push)
(assert 
    (forall ((x T))
        (not (transitive x x))))
(check-sat)
(pop)

我的问题是:第二次测试与第一次测试有何不同？为什么最后一个给出 unknown ，而之前的那个工作得很好？

Answer 1

这里的“详细”消息是一个提示。 mbqi 代表基于模型的量词实例化。这是SMT求解中处理量词的一种方法。在第一种情况下，MBQI 设法找到了一个模型。但是您的 transitive 函数对于 MBQI 来说太复杂了，无法处理，因此它放弃了。增加限制不太可能解决问题，也不是长期解决方案。

说来话长，递归定义很难处理，带有量词的递归定义就更难了。逻辑变得半可判定，并且你受到启发式的支配。即使您找到了一种让 z3 计算模型的方法，它也会很脆弱。这类问题不适合SMT解决；最好使用适当的定理证明器，如 Isabelle、Hol、Coq、Lean。 Agda 等。几乎所有这些工具都提供“策略”来将子目标分派(dispatch)给 SMT 求解器，因此您可以两全其美。 (当然，您会失去完全自动化，但是有了量词，您就不能指望更好了。)