使用 z3 直接访问理论决策程序

Direct access to Theory decision procedures using z3

本文关键字：理论决策程序访问 z3 使用更新时间：2023-10-16

是否有用于直接查询理论决策过程的 z3 c++ api？

意思是，给定一组理论谓词，

我想检查它们在某个给定的理论中是否冲突，而不调用 z3 证明者它们的连词。

例如，我想检查相等逻辑中的以下一组谓词是否冲突：x=y， y=z， x！=z

你可能可以使用一些策略，这取决于你到底需要理论的哪些部分（参见 Z3 策略）。

如果你只想要非常快速的完全无法求解的检查，那么你应该使用简化器，它将对所有理论应用重写规则并返回一个简化的表达式，可以是真或假。重写器还用于计算给定某个模型的表达式，因此当所有变量/常量/函数都有解释时，它支持计算表达式所需的一切（并且可以启用模型完成以填充缺失的）。