我可以通过 C++ API 检查变量是否具有确定性值吗

Question

我注意到 Z3 可以从一些纸上做 allsmt。在我的项目中，我必须在 SMT 公式中搜索确定性变量。通过确定性，我的意思是变量只能采用一个 int 值来使公式可满足。是否有可以执行此任务的 c++/c API 函数？

到目前为止，我能做的最好的事情是多次调用solver.check() 函数来否定我感兴趣的每个变量。有没有更快的方法通过使用API​​ 来做到这一点？

基本上，我想做 allsmt 和谓词抽象/投影。

Answer 1

没有专门的 API 来检查给定变量的所有模型是否必须就相同的值达成一致。您可以在 Z3 之上实现或多或少有效的算法来解决这个问题。 这是一个可能的算法：

1. 从 Z3 获取模型 M。
2. 对于您感兴趣的变量，断言：Not (And([(M.eval(x) == x) for x in Vars]))
3. 重新检查可满足性。如果新状态不可满足，那么 Vars 中剩余的变量必须具有相同的值。否则，从 Vars 中删除评估为与旧 M.eval(x) 不同的新值的变量，并重复 (2) 直到 Vars 为空或上下文不可满足。