CODEWITHSUNDEEP
z3
Douglas B. Staple
Douglas B. Staple

Reputation: 10946

Undocumented trigonometric functions in Z3 reparable?

Officially, there is no trig support in Z3. For example, see this question, or this one. However, there are undocumented trigonometric operators in Z3 -- they are used for example in the regression tests. There is even a built-in symbol called pi. Z3 can even do some trivial proofs with these operators, e.g.:

(declare-fun x () Real)
(assert (= (cos pi) x))
(check-sat)
(get-value (x))

Comes back with:

sat
((x (- 1.0)))

These operators do not work well. For example, this little input file will cause a seg fault with Z3 4.4.1, or cause a rapid explosion in memory usage with the master branch as this commit (now):

(declare-fun x () Real)
(assert (< (sin x) -1.0))
(check-sat)

I'm not surprised that an undocumented feature that the team says doesn't exist doesn't work. My question is: are they possible to fix? What level of performance would be a justified addition to Z3? I know that I can do a number of trigonometric proofs with Z3 using uninterpreted functions plus trigonometric identities. Is there any interest in this among the Z3 team?

Upvotes: 1

Views: 174

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Thanks, Z3 should not crash in such cases. It should be more graceful about handling these operations. I checked in a fix to this now, 9b91e6f..cb29c07. OTOH, there is essentially no theory reasoning for such operators. For example, Z3 does not know the bounds for sin. You would have to axiomatize such properties yourself. Z3 returns "unknown" (or "unsat", but not "sat") when you use the built-in functions that have no (partial) decision procedure support.

Upvotes: 2

Related Questions