有什么办法可以从未解释的术语代表到 z3 中的术语？答案

【问题标题】：Any way to go from uninterpreted term representative to term in z3?有什么办法可以从未解释的术语代表到 z3 中的术语？
【发布时间】：2016-11-24 16:11:18
【问题描述】：

我正在使用 c++ API。我创建了一个未解释的和该类型的术语 x、y 和 z。

z3::context ctx;
auto termSort = ctx.uninterpreted_sort("USORT");
auto x = ctx.constant("x", termSort);
auto y = ctx.constant("y", termSort);
auto z = ctx.constant("z", termSort);

solver s(ctx);
s.add(x == y);
s.add(y != z);
s.check();
auto model = s.get_model();

当我打印模型时，我得到以下内容，这实际上是打印出每个术语的内部代表。

x: USORT!val!0
y: USORT!val!0
z: USORT!val!1

我的问题是：我怎样才能快速从代表转为任期？我想要这样的功能：

repr_to_term(USORT!val!0) => [x, y]
repr_to_term(USORT!val!1) => [z]

Z3 API 中是否有类似的功能？或者是一种模仿它的方法？

在这个简单的例子中，我可以简单地遍历我的所有术语并构建一张从代表到术语的地图。但在我的实际情况中，我不想在每次生成模型时都遍历所有项，因为有很多项。

【问题讨论】：

标签： c++ z3

【解决方案1】：

我从未使用过 C++ API，这个答案可能不是您想要的。但是在 z3py 中，我们可以通过以下方式声明变量

>>> from z3 import *
>>> for i in xrange(9):
...     globals()['a%i' % i]=BitVec('a%i' %i,8)
... 
>>> type(a0)
<type 'instance'>

【讨论】：

【解决方案2】：

如果此信息只获得一次，然后多次使用，最好的办法可能是按照建议生成地图，然后将其用于查找。

否则，通过一点重构，问题将适合Z3_get_implied_equalities，它解决了一个非常相似的任务。虽然，我不能说这是否会或应该表现更好。

【讨论】：