在Z3中從滿足賦值集合中均勻採樣

Question

有沒有一種方法可以使用Z3定理證明器從滿足賦值集合中均勻採樣？如果不是，那麼Z3最接近這個系統的系統是什麼？

Answer 1

沒有一種讓Z3統一爲你做樣本的直接方法。

雖然這是一個有趣的問題。例如，它取決於你使用什麼統一的理論。

FORMULA工具以一種方式在Z3頂部實施隨機抽樣，其方式 考慮到理論的某些性質。