1

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

4

2 回答 2

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

该示例还证明了以下微不足道的事实，即 if l = product([a], [b]), thenfirst(head(l))必须是a。

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

有关 Z3 中代数数据类型的更多信息，请访问在线教程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)
于 2012-05-17T20:53:48.370 回答
0

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

于 2012-05-18T03:23:19.057 回答