實現作爲表達式的樓層，而不是陳述

Question

是否可以表達樓層，使其可以用作表達式而不是語句？在Yices，我們可以做這樣的事情，這將產生sat和(= fooInt 5)：

(define floor::(-> x::real (subtype (y::int) (and (<= y x) (< x (+ y 1)))))) 
(define fooReal::real 11/2) 
(define fooInt::int) 
(assert (= fooInt (floor fooReal)) 

我可以在Z3得到最接近的是如下（我想既然Z3不支持依賴類型）：

作爲一個表達式的底面是理想的，因爲它會更接近地匹配我從中生成Z3輸入的AST。如果我錯過了一個明顯的解決方案，我很抱歉。

Answer 1

看起來你可以利用的to_int語義作爲SMT-LIB2規定（見http://smtlib.cs.uiowa.edu/theories/Reals_Ints.smt2）使用功能要發言（rise4fun鏈接：http://rise4fun.com/Z3/da5I）：

(define-fun floor ((x Real)) Int 
    (to_int x)) 

(declare-const fooInt Int) 
(define-fun fooReal() Real 5.5) 
(assert (= fooInt (floor fooReal))) 
(check-sat) ; sat 
(get-model) ; 5 

(assert (> fooInt 5)) 
(check-sat) ; unsat