z3 中的叉积 [英] cross product in z3

问题描述

z3 是否提供两个列表的叉积功能?如果不是，是否可以在不使用高阶函数或使用提供的列表函数的情况下定义一个?我一直在尝试定义一个问题.我知道如何使用 map 定义一个，但我认为 z3 不支持.

Does z3 provide a cross product function for two lists? If not is it possible to define one without using higher order functions or using the provided list functions? I have been having trouble trying to define one. I know how to define one using map but I don't think that is supported in z3.

推荐答案

您可以在 SMT 2.0 中声明叉积函数.然而，任何非平凡的财产都需要归纳证明.Z3 目前不支持归纳证明.因此，它只能证明非常简单的事实.顺便说一句，通过列表的交叉乘积，我假设您想要一个函数，该函数给出列表 [a, b] 和 [c, d] 返回列表或对 [(a, c), (a, d), (b, c), (b, d)].这是一个定义 product 函数的脚本.该脚本还演示了 SMT 2.0 语言的一些限制.例如，SMT 2.0 不支持参数化公理或函数的定义.所以，我使用未解释的排序来模拟"它.我还必须定义辅助函数 append 和 product-aux.你可以在网上试试这个例子:http://rise4fun.com/Z3/QahiP

You can declare the cross product function in SMT 2.0. However, any non-trivial property will require a proof by induction. Z3 currently does not support proofs by induction. Thus, it will only be able to prove very simple facts. BTW, by cross-product of lists, I'm assuming you want a function that given the lists [a, b] and [c, d] returns the list or pairs [(a, c), (a, d), (b, c), (b, d)]. Here is a script that defines the product function. The script also demonstrates some limitations of the SMT 2.0 language. For example, SMT 2.0 does not support the definition of parametric axioms or functions. So, I used uninterpreted sorts to "simulate" that. I also had to define the auxiliary functions append and product-aux. You can try this example online at: http://rise4fun.com/Z3/QahiP

这个例子也证明了下面这个微不足道的事实，如果l = product([a], [b])，那么first(head(l))一定是a.

The example also proves the following trivial fact that if l = product([a], [b]), then first(head(l)) must be a.

如果您对证明非平凡属性感兴趣.我看到两个选项.我们可以尝试使用 Z3 来证明基本情况和归纳情况.这种方法的主要缺点是我们必须手动创建这些案例，并且可能会出错.另一种选择是使用交互式定理证明器，例如 Isabelle.顺便说一句，Isabelle 有更丰富的输入语言，并提供了调用 Z3 的策略.

If you are insterested in proving non-trivial properties. I see two options. We can try to prove the base case and inductive cases using Z3. The main disadvantage in this approach is that we have to manually create these cases, and mistakes can be made. Another option is to use an interactive theorem prover such as Isabelle. BTW, Isabelle has a much richer input language, and provides tactics for invoking Z3.

有关 Z3 中代数数据类型的更多信息，请访问在线教程 http://rise4fun.com/Z3/tutorial/guide(节数据类型).

For more information about algebraic datatypes in Z3, go to the online tutorial http://rise4fun.com/Z3/tutorial/guide (Section Datatypes).

;; List is a builtin datatype in Z3
;; It has the constructors insert and nil

;; Declaring Pair type using algebraic datatypes
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

;; SMT 2.0 does not support parametric function definitions.
;; So, I'm using two uninterpreted sorts.
(declare-sort T1)
(declare-sort T2)
;; Remark: We can "instantiate" these sorts to interpreted sorts (Int, Real) by replacing the declarations above
;; with the definitions
;; (define-sort T1 () Int)
;; (define-sort T2 () Real)

(declare-fun append ((List (Pair T1 T2)) (List (Pair T1 T2))) (List (Pair T1 T2)))
;; Remark: I'm using (as nil (Pair T1 T2)) because nil is overloaded. So, I must tell which one I want.
(assert (forall ((l (List (Pair T1 T2)))) 
                (= (append (as nil (List (Pair T1 T2))) l) l)))
(assert (forall ((h (Pair T1 T2)) (t (List (Pair T1 T2))) (l (List (Pair T1 T2))))
                (= (append (insert h t) l) (insert h (append t l)))))

;; Auxiliary definition
;; Given [a, b, c], d  returns [(a, d), (b, d), (c, d)] 
(declare-fun product-aux ((List T1) T2) (List (Pair T1 T2)))
(assert (forall ((v T2))
                (= (product-aux (as nil (List T1)) v)
                   (as nil (List (Pair T1 T2))))))
(assert (forall ((h T1) (t (List T1)) (v T2))
                (= (product-aux (insert h t) v)
                   (insert (mk-pair h v) (product-aux t v)))))

(declare-fun product ((List T1) (List T2)) (List (Pair T1 T2)))

(assert (forall ((l (List T1)))
                (= (product l (as nil (List T2))) (as nil (List (Pair T1 T2))))))

(assert (forall ((l (List T1)) (h T2) (t (List T2)))
                (= (product l (insert h t))
                   (append (product-aux l h) (product l t)))))

(declare-const a T1)
(declare-const b T2)
(declare-const l (List (Pair T1 T2)))

(assert (= (product (insert a (as nil (List T1))) (insert b (as nil (List T2))))
           l))

(assert (not (= (first (head l)) a)))

(check-sat)

这篇关于z3 中的叉积的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！