在Z3py中，爲什麼簡化將分解轉換爲未解釋的函數？

Question

TL; DR：當使用simplify時，位向量分割節點從Z3_OP_BSDIV變爲Z3_OP_UNINTERPRETED。我怎樣才能從未解釋的操作中告訴分裂操作？

說明：

以下會話顯示位向量分裂被解釋，但是，使用simplify()之後，它被未解釋。看看下面的變量d會發生什麼。

>>> x, y = BitVecs('x y', 32) 
>>> n = x/y 
>>> n.decl().kind() 
1031L 
>>> d = simplify(x/y) 
>>> d.decl().kind() 
2051L 

我們可以看到，一個手動聲明未解釋的功能和UDiv有同樣的爲好。

>>> foo = Function('foo', BitVecSort(32), BitVecSort(32), BitVecSort(32)) 
>>> u = foo(x, y) 
>>> u.decl().kind() 
2051L 
>>> d1 = simplify(UDiv(x,y)) 
>>> d1.decl().kind() 
2051L 

但是，它似乎並沒有影響求解：求解器似乎仍然將操作解釋爲實際的分割。

>>> prove(d != 400) 
counterexample 
[y = 1, x = 400] 

我想通過自己的各種處理節點，但是這一次似乎「謊言」關於它的種類 - 是有沒有辦法知道它的真正解釋，即使其kind是Z3_OP_UNINTERPRETED？這是一個錯誤？

Answer 1

這不一定是一個錯誤。當分母爲零時，bvudiv/bvsdiv運算符的結果未定義（請參閱QF_BV logic definition）。因此，「x/y」的結果可能被認爲是未定義的，並且如果沒有其他約束，則用未解釋的函數進行替換是有保證的。因此，位矢量公式的簡化器必須考慮到未解釋的函數可能以簡化的形式出現。