z3 中原子的自定义理论

Question

我希望 z3 中有一些变量，它们取某个无限集合中的值，其元素除了相等比较之外没有任何操作（lisp 意义上的原子理论）。目前，我只是简单地通过字符串对值进行编码，但是 z3 可能会分配我想避免的格式错误的字符串，并且我担心字符串上的其他操作可能会成为求解器的开销。

我在这个集合上有一个关系

P(x, y, z)

，给定两个变量，另一个变量只有有限多种可能性。一个例子可能是

x^2 + y^2 + z^2 = 0 mod 10000

，但就我而言，它要复杂得多，而且我认为将关系直接编码或公理化为 z3 并不方便。因此，我计划编写一个自定义传播器，每当分配

x = "a"

和

z = "b"

时，都会添加诸如“

y = "ab"

和

y = "ba"

暗示

x

或

z

”之类的蕴含子句。这是正确的方法吗？或者这类问题是否可以通过其他方法更好地解决？

Answer 1

如果您需要的只是相等，那么 EUF（未解释函数的相等）就是正确的选择。这是一篇很好的文章：https://www21.in.tum.de/teaching/sar/SS20/6.pdf

几乎所有SMT求解器都支持EUF，并且它具有可判定的理论。当您关心的是原子上的相等性时，不要使用字符串或任何其他数据类型使您的模型复杂化。 EUF 正是您应该使用的逻辑。

关于你们的关系

P

：这实际上取决于这是一种什么样的关系。你可以有关于它的简单公理，它们会很好地实现。如果您有量化公理，那么您将处于半可判定片段中。这实际上完全取决于

P

需要满足什么。 （z3 中还有对传递闭包的自定义支持，如果这是您关心的事情。但是如果没有看到问题的详细信息，很难判断它是否适用。）