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 mkCos or 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?
