【发布时间】：2012-10-04 19:42:22
【问题描述】：
有没有办法使用 Z3 定理证明器从一组令人满意的作业中统一采样？如果没有，最接近 Z3 且具备此功能的系统是什么？
【问题讨论】：
标签： probability z3 smt theorem-proving
【发布时间】：2012-10-04 19:42:22
【问题描述】：
没有直接的方式让Z3统一为你做样片。
不过，这是一个有趣的问题。例如，这取决于什么 你使用的关于制服意味着什么的理论。
FORMULA 工具以某种方式在 Z3 之上实现随机抽样 这考虑了一些理论的性质。
【讨论】：