z3 - Z3はRealからIntへの変換をサポートしていますか？

Question

Z3では、Intに相当するRealを取得するためにto_realが必要です。逆変換、つまり切り捨て、丸めなどへのサポートはありますか？否定的なケースでは、もしあれば、それらを定義する最もZ3に適した方法は何でしょうか？みんなに感謝します。

Answer 1

はい、Z3 にはto_intReal を整数に変換する関数があります。のセマンティクスは、 SMT 2.0 標準to_intで定義されています。以下に例を示します: http://rise4fun.com/Z3/uJ3J

(declare-fun x () Real)

(assert (= (to_int x) 2))
(assert (not (= x 2.0)))

(check-sat)
(get-model)