z3smtquantifiersfirst-order-logic

Searching Skolem functions in non-linear arithmetics

I found that the following paper/code (https://github.com/grigoryfedyukovich/aeval) solves Skolem function search for linear arithmetic. It performs really well.

However, I would like to compute Skolem functions for non-linear arithmetic. Does anyone know any tool for this? For instance, given Forall x. Exists y. (x^2<y) should return f(x)=x^2+1.

I know Z3 is not the best for such queries, but do you know any method in the state of the art for this?

Solution

  • I'm afraid this answer from 2013 is still the state of affairs, so far as z3 is concerned: Does Z3 v4.3+ support quantifier elimination for NON-linear arithmetic

    Also see https://github.com/Z3Prover/z3/issues/6790. So, the answer is negative: z3 does not do quantifier elimination for non-linear arithmetic.