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