Algebraic numbers in Z3

user_10802473 0
Viewed 79

The following code sets some Z3 constraints for x,y that are satisfied (only) by: x = sqrt(2) and 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 output is:

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

It thus appear that the .index() function, which is supposed to extract the index of an algebraic number, does not work: Both $sqrt(2)$ and $- sqrt(2)$ are given the same index.

I have reported this issue in the Z3 github (link) but unfortunately the devs do not have the bandwidth to solve this issue.

I had a look at the python code for the .index() function (path z3/lib.z3.py):

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

which just calls:

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

which basically (?) calls the method Z3_algebraic_get_i of the Z3 library in the C language.

I am not familiar myself with C, so I am seeking some help:

QUESTION is the Z3_algebraic_get_i function of the C Z3 library actually working, or it's just Python?

Thanks

EDIT: This is the source code of the C function from here

    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);
    }
z3py z3
1 Answers

This indeed seems to be a bug in z3py; and I strongly suspect in the python bindings only. However, fixing it will take intimate knowledge of the code-base, even though it might be a simple thing at the end. You did the right thing by reporting it to the developers. It's unfortunate that they don't have the bandwidth to rectify the issue.

However, I can offer a hack, which can provide a workaround till there's a proper fix, if ever. Define:

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

Now you can change the last two lines of your program to say:

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))

And this prints:

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

This does the right thing for your particular example, and I think it'll do the right thing in general; so long as the result is a root-object. The hack is to print the object as an s-expr, which shows it as a root-object and extract the index value. Of course, you might want to be careful and do some checking on the result of sexpr() to make sure it indeed does look like a root-object first, and if not, throw an error or return some default value.

I should emphasize that this is a hack, and should be used sparingly and only with care; but it can help you if no one steps up to fix the corresponding bug in z3py.

user_9363100
Related