title: Undocumented trigonometric functions in Z3 reparable?
body: <p>Officially, there is no trig support in Z3. For example, see <a href="https://stackoverflow.com/questions/15148707/can-z3-handle-sinusoidal-and-exponential-functions/15149800#15149800">this question</a>, or <a href="https://stackoverflow.com/questions/18064822/z3-supports-for-nonlinear-arithmetics/18130976#18130976">this one</a>.  However, there are undocumented trigonometric operators in Z3 -- they are used for example in the <a href="https://github.com/Z3Prover/z3test/tree/master/regressions/smt2" rel="nofollow">regression tests</a>.  There is even a built-in symbol called <code>pi</code>.  Z3 can even do some trivial proofs with these operators, e.g.:</p>
  
  <pre><code>(declare-fun x () Real)
  (assert (= (cos pi) x))
  (check-sat)
  (get-value (x))
  </code></pre>
  
  <p>Comes back with:</p>
  
  <pre><code>sat
  ((x (- 1.0)))
  </code></pre>
  
  <p>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 <a href="https://github.com/Z3Prover/z3/commit/9b91e6ff0aa6d3ca759a61b701f987e71eb04540" rel="nofollow">this commit</a> (now):</p>
  
  <pre><code>(declare-fun x () Real)
  (assert (&lt; (sin x) -1.0))
  (check-sat)
  </code></pre>
  
  <p>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?</p>