有人知道Z3是否支持SSMT（即随机量词）或是否有计划添加它？
Reference paper
在Z3的顶部（而非内部）实施SSMT（和类似的）正在进行（但目前活动较少），在某些特定问题上优于Tino Teige的方法和Prism，见here和here .
目前没有直接处理随机量词的计划 . 该论文的作者可能有更多信息 . 该文件指出了一个系统：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上最小化 .
2 回答
在Z3的顶部（而非内部）实施SSMT（和类似的）正在进行（但目前活动较少），在某些特定问题上优于Tino Teige的方法和Prism，见here和here .
目前没有直接处理随机量词的计划 . 该论文的作者可能有更多信息 . 该文件指出了一个系统：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上最小化 .