Commit 9ccc3cd0 authored by Sylvain Dailler's avatar Sylvain Dailler

Updated itp driver for real and float.

parent bcd08e11
......@@ -32,3 +32,33 @@ theory map.Map
syntax function ([<-]) "{%1 with [%2] = %3}"
end
theory ieee_float.GenericFloat
syntax function (.+) "(%1 .+ %2)"
syntax function (.-) "(%1 .- %2)"
syntax function (.*) "(%1 .* %2)"
syntax function (.-_) "(.-%1)"
syntax function (./) "(%1 ./ %2)"
syntax predicate (.<=) "(%1 <= %2)"
syntax predicate (.<) "(%1 < %2)"
syntax predicate (.>=) "(%1 >= %2)"
syntax predicate (.>) "(%1 > %2)"
syntax predicate (.=) "(%1 .= %2)"
end
theory real.Real
syntax function (+) "(%1 + %2)"
syntax function (-) "(%1 - %2)"
syntax function (*) "(%1 * %2)"
syntax function (-_) "(-%1)"
syntax predicate (<=) "(%1 <= %2)"
syntax predicate (<) "(%1 < %2)"
syntax predicate (>=) "(%1 >= %2)"
syntax predicate (>) "(%1 > %2)"
end
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