How does one use trigonometric functions like sin and cos and the constant Pi from the Z3 java API?
If I use the java API like so:
Solver s = context.getSolver() s.add(z3.parseSMTLIB2String( "(declare-fun theta () Real)\n"+ "(declare-fun offset () Real)\n"+ "(assert (> (cos theta) (/ 1 pi)))\n" //a sequence of empty arrays
Then z3 will attempt to reason about pi and cosine.
But I cannot figure out how to declare that in the java API. There is no
pi constant available. So how would one encode this with the java API? Is it perhaps a simple over-sight that this function and the constant
pi are not exposed?