CODEWITHSUNDEEP
pythonpython-3.xz3z3py
Owl Owl
Owl Owl

Reputation: 201

z3 Real Exponentiation

I've run into a strange situation where z3py produces two separate answers for what would logically be the same problem.

Version 1:

>>> import z3
>>> r, r2, q = z3.Reals('r r2 q')
>>> s = z3.Solver()
>>> s.add(r > 2, r2 == r, q == r2 ** z3.RealVal(0.5))
>>> s.check()
unknown

Version 2

>>> import z3
>>> r, r2, q = z3.Reals('r r2 q')
>>> s = z3.Solver()
>>> s.add(r > 2, r2 == r, q * q == r2)
>>> s.check()
sat

How do I change what I'm doing with version 1 so that it will produce an accurate result? These constraints are being generated on-the-fly and would possibly add significantly to the complexity of the application if I were to attempt to re-write them on-the-fly. Also, in the case where the root is truly symbolic, it would simply not be possible for Python itself to solve that problem.

Edit: I've discovered that if I use the following setup for my Solver, it will solve successfully (although a bit slower):

z3.Then("simplify","solve-eqs","smt").solver()

It's not entirely clear to me what the implications are of specifying that rather than just the default solver, however.

Upvotes: 0

Views: 147

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

The out of the box performance of Z3 on non-linear real problems is not great, it will definitely take some fiddling to make it find all the solutions you need. My first attempt is always to switch to the NLSAT solver (apply the qfnra-nlsat tactic, or make a solver from it). That solver is often much better on QF_NRA problems, but it doesn't support any theory combination, i.e., if you have other types of variables it will bail out.

Also, search stackoverflow for "Z3" and "non-linear", there have been a multitude of questions and answers to various aspects thereof.

Upvotes: 1

Related Questions