是否可以在 z3(使用 SMT-LIB2 接口)中定义一个具有全量化断言的函数? [英] Is it possible to define a function with an all quantified assertion in z3 (with SMT-LIB2 interface)?

问题描述

我的目标是定义一个函数，它接受一个输入整数序列并输出一个相同长度的整数序列，但只包含输入的第一个元素序列.例如(在伪代码中):

My goal is to define a function, which takes an input integer sequence and outputs an integer sequence with the same length, but containing only the first element of the input sequence. For example (in pseudo-code):

f([7,5,6]) = [7,7,7]

为此，我在 z3 中声明了一个函数:

For this I declare a function in z3 as:

(declare-fun f ((Seq Int)) (Seq Int))

并尝试通过断言强制预期行为:

and try to force the expected behavior with the assertion:

(assert 
    (forall ((arr (Seq Int)))
        (and
            (=
                (seq.len arr)
                (seq.len (f arr))
            )
            (forall ((i Int))
                (implies
                    (and
                        (>= i 0)
                        (< i (seq.len arr))
                    )
                    (=
                        (seq.at arr 0)
                        (seq.at (f arr) i)
                    )
                )
            )
        )
    ))

问题是程序没有终止，我怀疑这是由全量词引起的.为了测试我的条件是否正确，我声明了两个常量，并看到对于 concrete 值，条件是正确的:

The problem is that the program does not terminate, which I suspect is caused by the all-quantifier. To test whether my conditions are correct I declared two constants and saw that for concrete values the conditions are correct:

(define-const first (Seq Int)
    (seq.++ (seq.unit 1) (seq.unit 2))
)
(declare-const second (Seq Int))
(assert 
    (and
        (=
            (seq.len first)
            (seq.len second)
        )
        (forall ((i Int))
            (implies
                (and
                    (>= i 0)
                    (< i (seq.len first))
                )
                (=
                    (seq.at first 0)
                    (seq.at second i)
                )
            )
        )
    )
)
(check-sat)
(get-model)

我的问题:如何将断言中的条件与 f 函数的预期行为相结合?该函数应该是 total 的，这意味着应该为所有可能的输入序列定义它，但这让我认为在我的情况下肯定需要一个 all 量词.

My question: How would it be possible to integrate the conditions in the assertions with the expected behavior of the f function? The function should be total, which means it should be defined for all possible input sequences, but this leads me to think that an all quantifier is definitely needed in my case.

推荐答案

使用这种递归数据类型/值进行推理并不适合 SMT 求解器.大多数问题都需要归纳，而 SMT 求解器不会开箱即用地进行归纳.

Reasoning with such recursive data-types/values is not a strong suit for SMT solvers. Most problems will require induction and SMT-solvers don't do induction out-of-the box.

话虽如此，您可以使用新的 declare-fun-rec 结构编写您想要的代码:

Having said that, you can code what you want using the new declare-fun-rec construct:

(define-fun-rec copyHeadAux ((x (Seq Int)) (l (Seq Int))) (Seq Int)
   (ite (= 0 (seq.len l))
        (as seq.empty (Seq Int))
    (seq.++ x (copyHeadAux x (seq.extract l 1 (seq.len l))))))


(define-fun copyHead ((l (Seq Int))) (Seq Int)
   (ite (= 0 (seq.len l))
        (as seq.empty (Seq Int))
    (copyHeadAux (seq.at l 0) l)))

(define-fun test () (Seq Int) (seq.++ (seq.unit 7) (seq.unit 5) (seq.unit 6)))
(declare-const out (Seq Int))
(assert (= out (copyHead test)))
(check-sat)
(get-model)

当我运行这个时，我得到:

When I run this, I get:

sat
(
  (define-fun out () (Seq Int)
    (seq.++ (seq.unit 7) (seq.unit 7) (seq.unit 7)))
  (define-fun test () (Seq Int)
    (seq.++ (seq.unit 7) (seq.unit 5) (seq.unit 6)))
  (define-fun copyHead ((x!0 (Seq Int))) (Seq Int)
    (ite (= 0 (seq.len x!0))
         (as seq.empty (Seq Int))
         (copyHeadAux (seq.at x!0 0) x!0)))
)

这是您正在寻找的正确答案.但除非你的约束只涉及不断折叠"情况(即，copyHead 总是应用于一个常数已知值)，你很可能得到 unknown 作为答案，或者让求解器进入一个无限的 e-匹配循环.

which is the correct answer you're looking for. But unless your constraints only involve "constant-folding" cases (i.e., where copyHead is always applied to a constant known value), you're likely to get unknown as the answer, or have the solver go into an infinite e-matching loop.

最好使用适当的定理证明器(Isabelle、HOL、Lean、ACL2 等)来对这些递归定义进行推理.当然，随着时间的推移，SMT 求解器会变得越来越好，也许有一天他们能够开箱即用地处理更多这样的问题，但我不会屏住呼吸.

It's best to use a proper theorem prover (Isabelle, HOL, Lean, ACL2 etc.) for reasoning with these sorts of recursive definitions. Of course, SMT solvers get better over time and maybe one day they'll be able to handle more problems like this out-of-the-box, but I wouldn't hold my breath.

这篇关于是否可以在 z3(使用 SMT-LIB2 接口)中定义一个具有全量化断言的函数?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！