Допустим, у меня есть определяемый пользователем коммутативный и ассоциативный оператор op. Приведенный ниже код недействителен, так как я использую op с более чем двумя аргументами. Давайте на мгновение предположим, что это действительно и означает, что «способ применения операции не имеет значения».
(declare-sort T 0)
(declare-fun op (T T) T)
(declare-fun P (T) Bool)
(declare-const a T)
(declare-const b T)
(declare-const c T)
(declare-const d T)
(declare-const k T)
; associativity
(assert (forall ((x T) (y T)) (z T))
(= (op x (op y z))
(op (op x y) z))))
; commutativity
(assert (forall ((x T) (y T)))
(= (op x y)
(op y x))))
; assumption 1
(assert (forall ((x T) (y T)) (= (op x y) k)))
; assumption 2
(assert (P (op a c k)))
; conjecture
(assert (not (P (op a b c d))))
Каков наилучший способ гарантировать, что предположение 1 реализуется с x, y := b, d, а предположение 2 становится применимым для доказательства гипотезы?
Одно из решений, которое я рассматриваю, состоит в том, чтобы сгенерировать все возможные бинарные деревья, соответствующие (op a b c d). Однако это довольно дорого: есть 5 различных бинарных деревьев с 4 листьями и 24 различными перестановками листьев, всего 120 различных бинарных деревьев. Я также могу воздержаться и надеяться, что z3 использует ассоциативность и коммутативность самостоятельно и вызовет правильную реализацию предположения 1.
Проблема становится еще более сложной, если мы учтем, что цепочки типа (op a b c) могут появляться внутри универсальной квантификации. Вероятно, мы могли бы использовать шаблоны (op a (op b c)), (op b (op a c)) и т. д., чтобы максимизировать шансы на конкретизацию количественного определения, но шаблон должен где-то появиться, и у z3, вероятно, нет указаний для этого. сделать так, чтобы оно появилось само по себе.
Могу ли я сделать что-нибудь лучше?
Спасибо! Саймон
