z3中的叉积答案

【问题标题】：cross product in z3z3中的叉积
【发布时间】：2012-05-17 19:51:33
【问题描述】：

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

【问题讨论】：

标签： z3

【解决方案1】：

您可以在 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

该示例还证明了以下琐碎事实，即如果l = product([a], [b])，则first(head(l)) 必须是a。

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

有关 Z3 中代数数据类型的更多信息，请访问在线教程http://rise4fun.com/Z3/tutorial/guide（数据类型部分）。

;; 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 中是否有类似“#include”的东西，这样我就不需要一遍又一遍地复制和粘贴相同的脚本？
您可以使用type（windows）或cat（OSX 和Linux）连接文件并将结果发送到Z3。示例：type file1.smt2 file2.smt2 2>NUL | z3 -in -smt2。 -in 指令告诉 Z3 从标准输入读取 SMT2 文件。
在 OSX 和 Linux 上，您可以使用：cat file1.smt2 file2.smt2 | z3 -in -smt2。

【解决方案2】：

smt-lib 格式没有#include 指令。 Z3 提供了几种其他方式来提供输入。 Python 输入格式利用了所有 Python，因此自然支持导入文件。在http://rise4fun.com/z3py有一个关于Z3Py的教程

【讨论】：