I would like to do something like: Exists y. 0<=cos(y)<=1., which could return a model e.g., y:=50. Is this possible in Z3?
I know SMT solvers overall are problematic for non-linear/trascendental operations [1], and indeed have not been implemented for a while [2,3]. However, it looks like at least for trigonometric functions there is some support [4,5] and, moreover, it looks like it is already built-in, like in the function cos of [6].
Thus, I tried the following in Z3-PY:
from z3 import *
x = Real('x')
solver = Solver()
solver.add(Exists([x],cos(x)<1))
solver.check()
model = solver.model()
... but looks like cos is not recognized. Do you know how can I use this? I have some alternative methods in mind that do no use Z3, but I want to explore this possibility in order to keep everything implemented in the same block.
[2] Can Z3 handle sinusoidal and exponential functions
[3] Z3 support for nonlinear arithmetic
[4] https://github.com/Z3Prover/z3/issues/680
[5] Support of trigonometric functions ( e.g.: cos, tan) in Z3
You can use trigonometric functions in z3 if you stick to the SMTLib interface:
(set-option :produce-models true)
(set-logic ALL)
(declare-fun x () Real)
(assert (< (cos x) 1.0))
(check-sat)
alas, this doesn't get you far. For the above, z3 says:
unknown
and this'll be the case for most problems using trigonometric functions. Support for them is extremely lightweight: They are more or less treated as uninterpreted functions with some axioms (like sin^2 + cos^2 = 1), which can handle some simple queries but not much.
It doesn't look like you can access these from the Python API. Not because it can't be done, but probably no-one bothered since the support is rather weak anyhow. (i.e., you can define them yourself on the Python side as uninterpreted functions with several axioms, and you'd pretty much match what z3 SMTLib support for them there is.)
If you're interested in trigonometric functions and automated theorem proving, your best bet is MetiTarski (https://www.cl.cam.ac.uk/~lp15/papers/Arith/). If you want something a bit more push-button and are happy with delta-satisfiability, then dReal is another tool you should look at: https://dreal.github.io.