在 Z3 中创建传递而不是自反函数 [英] Creating a transitive and not reflexive function in Z3

问题描述

我正在尝试在 Z3 中创建一个可传递但不具有自反性的函数.IE.如果 (transitive ab) 和 (transitive bc)hold 那么 (transitive ac) 应该成立，但是 (transitive aa)代码>不应该.

I'm trying to create a function in Z3 that is transitive but not reflexive. I.e. if (transitive a b) and (transitive b c)hold then (transitive a c) should hold, but (transitive a a) should not.

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

I've tried to do it the following way, with 5 "tests". The first does what I expect, but the second one fails and results in 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，而前一个工作正常?

My question is: how does the second test differ from the first? Why does the last one give unknown, whereas the one before that works just fine?

推荐答案

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

The "verbose" message is a hint here. mbqi stands for model-based-quantifier-instantiation. It's a method of dealing with quantifiers in SMT solving. In the first case, MBQI manages to find a model. But your transitive function is just too complicated for MBQI to handle, and thus it gives up. Increasing the limit will not likely address the problem, nor it's a long term solution.

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

Short story long, recursive definitions are difficult to deal with, and recursive definitions with quantifiers are even harder. The logic becomes semi-decidable, and you're at the mercy of heuristics. Even if you found a way to make z3 compute a model for this, it would be brittle. These sorts of problems are just not suitable for SMT solving; better use a proper theorem prover like Isabelle, Hol, Coq, Lean. Agda, etc. Almost all these tools offer "tactics" to dispatch subgoals to SMT solvers, so you have the best of both worlds. (Of course you lose full automation, but with quantifiers present, you can't expect any better.)

这篇关于在 Z3 中创建传递而不是自反函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！