z3 - 如何在用户理论插件中访问理论算术中的vars？

Question

在用户理论插件中，假设我有一个客户排序“T”，我在 T 上定义了一个带有“ Z3_func_decl”的函数“f”，它接受排序 T 的参数并返回排序 Int（排序由“ Z3_mk_int_sort”制成）。我对返回的 Int 值还有其他限制。

在搜索中，我想在一些回调（例如new_assignment或new_eq回调）中捕获 Int 返回值的具体值，以便我可以做出额外的断言来解决排序 T 的参数值。但问题是那些回调不会被调用在搜索中。

我看了一下Z3_contextSAT解决方案。在理论算术中，我看到：

vars: v0 #24 lo: -oo, up: 4, value: 0, occs: 0, atom: 1, int, non-base, shared: 0, activity: 0, unassigned: 0, rel: 1, def: #24

“#24”是我的函数，“up”中显示的“4”是我函数返回值的SAT解。

我的问题是如何在搜索中获得值“4”。我试图在回调的#24 的等价类中找到它，final_check但没有运气。

谢谢！

Answer 1

不幸的是，你不能在 Z3 中做到这一点。一个理论无法访问其他理论中使用的内部数据结构。理论只知道共享项是否相等（不相等）。这个设计决策允许我们在不影响其他人的情况下改变理论的实现。算术理论就是一个很好的例子。我们将用更高效的实现替换当前的实现。新的实现将使用不同的数据结构。在上面的示例中， lo和up是 term 的已知下限和上限#24。4Z3 选择（上限）作为 的解释只是一个巧合#24。

而且，在Z3的当前版本中，模型构建是在Z3建立问题后开始的。因此，理论算术赋予的实际解释不能真正用于帮助其他理论。