任何方式從未解釋的學期代表轉到z3學期？

Question

我正在使用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中是否有類似的功能？或者一種模仿它的方式？

在這種簡單的情況下，我可以簡單地走我的所有條款，並建立從代表到術語的地圖。但在我的實際案例中，我不想在每次生成模型時都使用所有術語，因爲有很多術語。

Answer 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'> 

Answer 2

如果獲得此信息一次，然後多次使用聲明變量，最好的辦法可能是生成地圖，作爲建議，然後利用它來進行查找。

否則，通過一點重構，該問題將適用於Z3_get_implied_equalities，這解決了非常類似的任務。雖然，我無法說出是否會或者應該表現更好。