перекрестное произведение в 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.

Пример также доказывает следующий тривиальный факт, что если 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)

Для формата smt-lib нет директивы #include. Z3 предоставляет несколько других способов ввода. Входной формат Python использует весь Python, поэтому импорт файлов, естественно, поддерживается. На http://rise4fun.com/z3py есть руководство по Z3Py.