CODEWITHSUNDEEP
z3smtquantifiersfirst-order-logic
Theo Deep
Theo Deep

Reputation: 766

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?

Upvotes: 0

Views: 39

Answers (1)

alias
alias

Reputation: 30438

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.

Upvotes: 1

Related Questions