Логика первого порядка с кванторами по существу полуразрешима. В контексте SMT это означает, что не существует процедуры принятия решения для правильного ответа на каждый запрос как sat/unsat.
(Кроме теории, это не так важно: если полностью игнорировать соображения эффективности, то есть алгоритмы, которые могут правильно ответить на все удовлетворяющие запросы, но нет алгоритмов, которые могут правильно вывести unsat. В последнем случае случае, они будут зацикливаться навсегда. Но это отступление.)
Таким образом, для работы с квантификаторами решатели SMT обычно используют метод, известный как E-сопоставление. По сути, когда они формируют базовый термин, в котором упоминаются неинтерпретируемые функции, они пытаются примерить количественные аксиомы, чтобы они соответствовали им, и соответствующим образом переписывают. Этот метод может быть весьма эффективным на практике и хорошо масштабируется с типичными проблемами верификации программного обеспечения, но очевидно, что это не панацея. Подробнее см. в этой статье: https://pdfs.semanticscholar.org/4eb2/c5e05ab5c53f20c6050f8252a310cc23. .
Что касается вашего вопроса: по сути, когда у вас есть форма ite аксиомы, алгоритм электронного сопоставления просто не может найти подходящую замену для реализации вашей аксиомы. Из соображений эффективности e-matcher действительно рассматривает почти «точные» совпадения. (Воспринимайте это с долей скептицизма; это умнее, чем это, но ненамного.) Быть слишком умным здесь вряд ли когда-либо окупается на практике, поскольку вы можете в конечном итоге сгенерировать слишком много совпадений и в конечном итоге взорвать свое пространство поиска. Как обычно, это баланс между практичностью, эффективностью и охватом как можно большего количества случаев.
Z3 позволяет указывать шаблоны, чтобы в определенной степени направлять этот поиск, но шаблоны довольно сложны в использовании и хрупки. (Я бы указал вам правильное место в документации по шаблонам, увы, сайт документации по z3 в настоящее время не работает, как вы сами заметили!) Возможно, вы захотите поиграть с ними, чтобы посмотреть, дадут ли они вам лучшие результаты. . Но эмпирическое правило состоит в том, чтобы ваши квантифицированные аксиомы были как можно более простыми и очевидными. И ваш второй вариант именно так и делает, по сравнению с первым. Для этой конкретной проблемы определенно разделите аксиому на две части и утвердите обе по отдельности, чтобы охватить случаи nil/insert. Объединение их в одно правило просто превышает возможности текущего e-matcher.
person
alias
schedule
05.01.2019
