Теория неустойчивости стохастичности

Question

Кто-нибудь знает, поддерживает ли Z3 SSMT (т. Е. Рандомизированные кванторы) или если есть какие-либо планы по его добавлению?

Reference paper

Answer 1

Там нет текущих планов непосредственно обрабатывать рандомизированные кванторов. У авторов этой статьи может быть больше информации. В документе указывается на систему: https://projects.avacs.org/projects/sisat/wiki/SiSAT_Manual Тем не менее, последние 3 года неактивны, поэтому я не уверен, что это то, что авторы срочно преследуют, это . Может быть, в системах. Самый близкий, который я рассматриваю, чередует минимальные/максимальные цели. То есть вы должны иметь возможность вычислить некоторую целевую функцию f (x, y), такую, что x, y удовлетворяют ограничениям Phi (x, y) и подчиняются min x max y f (x, y). Последнее означает найти x, что f (x, y) минимизировано по всем y.

Answer 2

Существует постоянные (но в настоящее время низкой активности) усилия по осуществлению SSMT (и подобный) сверху (не внутри) из Z3, который превосходит методы Тина Teige в и Prism на некоторых конкретных проблемах, см here и here.