Разница в кодировании одной и той же аксиомы

Question

Мне интересно, в чем разница между этими двумя кодировками одной и той же аксиомы списка:

(define-sort T1 () Int)

(declare-fun list_length ( (List T1) ) Int)

(assert (forall ( (i T1) (l (List T1)) )
                (ite (= l (as nil (List T1)))
                     (= (list_length l) 0)
                     (= (list_length (insert i l)) (+ 1 (list_length l))))))

а также

(define-sort T1 () Int)

(declare-fun list_length ( (List T1) ) Int)

(assert (= (list_length (as nil (List T1))) 0))

(assert (forall ( (i T1) (l (List T1)) )
                (= (list_length (insert i l)) (+ 1 (list_length l)))))

Для этого теста:

(declare-const a T1)
(declare-const b T1)

(assert (not
         (= (list_length (insert b (insert a (as nil (List T1))))) 2)))

(check-sat)

Каким-то образом z3 может рассуждать о второй версии, но не о первой (где кажется, что она зацикливается вечно).

Редактировать: то же самое с cvc4 с первой вернувшейся версией.

Answer 1

Логика первого порядка с квантификаторами, по существу, полуразрешима. В контексте SMT это означает, что не существует процедуры принятия решения для правильного ответа на каждый запрос, как sat/unsat,

(Если говорить теоретически, это не так важно: если вы полностью игнорируете соображения эффективности, то существуют алгоритмы, которые могут правильно отвечать на все выполнимые запросы, но нет алгоритмов, которые могут правильно выводить unsat, В этом последнем случае они будут зациклены навсегда. Но это отступление.)

Таким образом, для работы с квантификаторами SMT-решатели обычно используют метод, известный как E-match. По сути, когда они образуют базовый термин с упоминанием неинтерпретируемых функций, они пытаются создать квантифицированные аксиомы для их соответствия и переписать соответственно. Этот метод может быть довольно эффективным на практике и хорошо масштабируется с типичными проблемами проверки программного обеспечения, но, очевидно, это не панацея. Подробности см. В этом документе: https://pdfs.semanticscholar.org/4eb2/c5e05ab5c53f20c6050f8252a30cc23561be.pdf.

Относительно вашего вопроса: по сути, когда у вас есть ite В форме аксиомы алгоритм электронного сопоставления просто не может найти правильную замену для создания своей аксиомы. Из соображений эффективности e-matcher действительно просматривает почти "точные" совпадения. (Возьмите это с крошкой соли; это умнее, но не намного.) Слишком умная работа на практике вряд ли когда-нибудь окупится, так как вы можете получить слишком много совпадений и в конечном итоге взорвать пространство поиска. Как обычно, это баланс между практичностью, эффективностью и охватом как можно большего количества случаев.

Z3 позволяет задавать шаблоны, которые будут направлять этот поиск в определенной степени, но шаблоны довольно сложны в использовании и хрупки. (Я бы указал вам правильное место в документации по шаблонам, увы, сайт документации z3 пока недоступен, как вы сами заметили!) Возможно, вы захотите поиграть с ними, чтобы увидеть, дают ли они вам лучшие результаты, Но эмпирическое правило заключается в том, чтобы ваши количественные аксиомы были максимально простыми и очевидными. И ваш второй вариант именно так и поступает по сравнению с первым. Для этой конкретной задачи определенно разделите аксиому на две части и отстаивайте обе отдельно, чтобы покрыть nil/insert случаев. Объединение их в одно правило просто превосходит возможности нынешнего e-matcher.