z3 - 将 floor 实现为表达式，而不是语句

Question

是否可以表达 floor 使其可以用作表达式而不是语句？在 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 不支持依赖类型）：

(declare-const fooInt Int)
(define-fun fooReal () Real 5.5)
(assert (and (>= fooReal fooInt)(< fooReal (+ fooInt 1))))

Floor 作为表达式是理想的，因为它会更接近地匹配我从中生成 Z3 输入的 AST。如果我错过了一个明显的解决方案，我深表歉意。

Answer 1

看起来您可以利用to_intSMT-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