title: Implement floor as an expression, not a statement
body: <p>Is it possible to express floor such that it can be used as an expression instead of a statement? In Yices, we can do something like this, which yields <code>sat</code> and <code>(= fooInt 5)</code>: </p>
  
  <pre><code>(define floor::(-&gt; x::real (subtype (y::int) (and (&lt;= y x) (&lt; x (+ y 1)))))) 
  (define fooReal::real 11/2)
  (define fooInt::int)
  (assert (= fooInt (floor fooReal))
  </code></pre>
  
  <p>The closest I can get in Z3 is the following (I think since Z3 does not support dependent types):</p>
  
  <pre><code>(declare-const fooInt Int)
  (define-fun fooReal () Real 5.5)
  (assert (and (&gt;= fooReal fooInt)(&lt; fooReal (+ fooInt 1))))
  </code></pre>
  
  <p>Floor as an expression is ideal since it would more closely match the AST I'm generating the Z3 input from. My apologies if I've missed an obvious solution. </p>