Существуют ли какие-либо другие доступные (и до сих пор поддерживаемые) инструменты SMT, которые выполняют исключение квантификаторов для линейной целочисленной арифметики помимо Z3?
Спасибо.
Инструменты для исключения квантификаторов в линейной целочисленной арифметике
Ответы (1)
Вы можете попробовать Princess от Филиппа Рюммера. Он поддерживает удаление квантификаторов и активно поддерживается.
person
Philippe
schedule
10.06.2012
