в чем разница между упрощением и ctx-solver-simplify в z3

Тактика simplify выполняет только «локальные упрощения». Для каждого термина t у нас есть simplify(t) новый термин, эквивалентный t. Более того, результат simplify(t) не зависит от контекста, в котором встречается t. Под контекстом я имел в виду утверждение F, где встречается t, и все остальные утверждения. Поскольку simplify является локальным, он очень эффективен. Реализация по существу основана на восходящем применении правил упрощения. Более того, поскольку результат simplify(t) не зависит от контекстной информации, мы можем его кэшировать. Таким образом, даже если t встречается в формуле F N раз, нам нужно упростить ее только один раз. Все встроенные решатели в Z3 применяют такое упрощение. Таким образом, такие тактики, как simplify, были тщательно протестированы.

Тактика ctx-solver-simplify использует контекст, в котором встречается t, чтобы применять упрощения. Основная идея состоит в том, чтобы упростить формулу F путем обхода ее с помощью решателя S. Решатель S по существу содержит «контекст». Всякий раз, когда S.check() возвращает unsat, мы знаем, что текущий контекст несовместим, и мы можем заменить текущую формулу на false. ctx-solver-simplify намного дороже. Во-первых, он выполняет множество вызовов S.check(). Каждый из этих вызовов потенциально очень дорог. Также намного сложнее кэшировать промежуточные результаты. Z3, возможно, придется упростить подформулу t много раз, потому что она встречается в разных контекстах.

Ошибка, о которой вы сообщили в своем вопросе, была исправлена. Исправление будет доступно в следующем выпуске (версия 4.1). Если вам нужно, мы можем предоставить вам предварительную версию Z3 4.1.