Commit c62462f7 authored by Sylvain Dailler's avatar Sylvain Dailler

add syntax function for truncate, floor and ceil

parent f47b643d
......@@ -131,6 +131,16 @@ theory real.FromInt
remove allprops
end
theory real.Truncate
syntax function truncate "(ite (>= %1 0.0)
(to_int %1)
(- (to_int (- %1))))"
syntax function floor "(to_int %1)"
syntax function ceil "(- 1 (to_int (- 1.0 %1)))"
remove allprops
end
theory Bool
syntax type bool "Bool"
syntax function True "true"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment