Можно ли убрать факты в движке данных Z3?Самое близкое, что я могу найти в документации, это Z3_fixedpoint_update_rule, который я не смог заставить работать так, как я хочу.
Z3_fixedpoint_update_rule
Я видел другие вопросы, связанные с отводом с использованием check-sat-assuming (например, Инкрементный решатель SMT со способностью отбрасывать определенные ограничения ) Есть ли следствие для механизма с фиксированной точкой / регистрацией данных?
check-sat-assuming
Краткий ответ: нет.После того, как факты добавлены, правила предварительно обрабатываются на их основе, создаются другие факты и т. Д., Поэтому сейчас нет пути назад.Я думаю, что только LogicBlox поддерживает такую функцию.