Z3 中的代数数

Question

以下代码为 x,y 设置了一些（仅）满足的 Z3 约束： x = sqrt(2) 和 y = -sqrt(2).

x, y = Reals('x y')
s = Solver()
s.add( x*x == 2 )
s.add( x>0)
s.add( y*y == 2 )
s.add( y<0)
s.check()
m = s.model()
val_x = m.get_interp(x)
val_y = m.get_interp(y)

print(f"The solutions are: x={val_x} and y={val_y}")
print(f"The defining polynomial of x has integer coefficients", val_x.poly(), " and root index ", val_x.index())
print(f"The defining polynomial of y has integer coefficients", val_y.poly(), " and root index ", val_y.index())

输出为：

The solutions are: x=1.4142135623? and y=-1.4142135623?

the defining polynomial of x has integer coefficients [-2, 0, 1]  and root index  0

the defining polynomial of y has integer coefficients [-2, 0, 1]  and root index  0

因此，似乎 .index() 函数（应该提取代数数的索引）不起作用：给出了 $sqrt(2)$ 和 $- sqrt(2)$相同的索引。

我已经在 Z3 github (link) 中报告了这个问题，但不幸的是开发者没有足够的带宽来解决这个问题。

我查看了 .index() 函数的 python 代码（路径 z3/lib.z3.py）：

def index(self):
    return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())

它只是调用：

def Z3_algebraic_get_i(a0, a1, _elems=Elementaries(_lib.Z3_algebraic_get_i)):
  r = _elems.f(a0, a1)
  _elems.Check(a0)
  return r

这基本上（？）调用了 C 语言中 Z3 库的方法 Z3_algebraic_get_i。

本人对C不熟悉，求助：

QUESTION 是 C Z3 库的 Z3_algebraic_get_i 函数实际工作，还是只是 Python?

谢谢

编辑：这是来自 here

的 C 函数的源代码

    unsigned Z3_API Z3_algebraic_get_i(Z3_context c, Z3_ast a) {
        Z3_TRY;
        LOG_Z3_algebraic_get_i(c, a);
        RESET_ERROR_CODE();
        CHECK_IS_ALGEBRAIC(a, 0);
        algebraic_numbers::manager & _am = am(c);
        algebraic_numbers::anum const & av = get_irrational(c, a);
        return _am.get_i(av);
        Z3_CATCH_RETURN(0);
    }

Answer 1

这似乎确实是 z3py 中的一个错误；我强烈怀疑仅在 python 绑定中。然而，修复它需要对 code-base 有深入的了解，即使最后这可能是一件简单的事情。您向开发人员报告是正确的做法。不幸的是，他们没有带宽来解决这个问题。

但是，我可以提供一个 hack，它可以提供一个解决方法，直到有一个适当的修复，如果有的话。定义：

def get_root_obj_index(ar):
    return Int(ar.sexpr().split()[-1][:-1])

现在您可以将程序的最后两行更改为：

print(f"The defining polynomial of x has integer coefficients", val_x.poly(), " and root index ", get_root_obj_index(val_x))
print(f"The defining polynomial of y has integer coefficients", val_y.poly(), " and root index ", get_root_obj_index(val_y))

这会打印：

The defining polynomial of x has integer coefficients [-2, 0, 1]  and root index  2
The defining polynomial of y has integer coefficients [-2, 0, 1]  and root index  1

这对您的特定示例做了正确的事情，我认为它通常会做正确的事情；只要结果是 root-object。技巧是将对象打印为 s-expr，显示为 root-object 并提取索引值。当然，您可能要小心并首先检查 sexpr() 的结果以确保它确实看起来像 root-object，如果不是，则抛出错误或 return 一些默认值。

我应该强调这是一个 hack，应该谨慎使用并且小心使用；但如果没有人站出来修复 z3py 中的相应错误，它可以帮助你。

Z3 中的代数数

Algebraic numbers in Z3

z3

z3py