Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
9ed1be10
Commit
9ed1be10
authored
May 05, 2014
by
Andrei Paskevich
Browse files
fix the TPTP TFA drivers
parent
bc4ea0a8
Changes
4
Hide whitespace changes
Inline
Side-by-side
drivers/beagle.drv
View file @
9ed1be10
...
...
@@ -245,10 +245,35 @@ theory tptp.Real
syntax function to_real "$to_real(%1)"
end
theory real.FromInt
syntax function from_int "$to_real(%1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Truncate
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function floor "$to_int(%1)"
syntax function ceil "$to_int($ceil(%1))"
syntax function truncate "$to_int($truncate(%1))"
remove prop Truncate_int
remove prop Truncate_down_pos
remove prop Truncate_up_neg
remove prop Real_of_truncate
remove prop Truncate_monotonic
remove prop Truncate_monotonic_int1
remove prop Truncate_monotonic_int2
remove prop Floor_int
remove prop Ceil_int
remove prop Floor_down
remove prop Ceil_up
remove prop Floor_monotonic
remove prop Ceil_monotonic
end
theory tptp.RealTrunc
...
...
drivers/princess.drv
View file @
9ed1be10
...
...
@@ -242,10 +242,35 @@ theory tptp.Real
syntax function to_real "$to_real(%1)"
end
theory real.FromInt
syntax function from_int "$to_real(%1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Truncate
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function floor "$to_int(%1)"
syntax function ceil "$to_int($ceil(%1))"
syntax function truncate "$to_int($truncate(%1))"
remove prop Truncate_int
remove prop Truncate_down_pos
remove prop Truncate_up_neg
remove prop Real_of_truncate
remove prop Truncate_monotonic
remove prop Truncate_monotonic_int1
remove prop Truncate_monotonic_int2
remove prop Floor_int
remove prop Ceil_int
remove prop Floor_down
remove prop Ceil_up
remove prop Floor_monotonic
remove prop Ceil_monotonic
end
theory tptp.RealTrunc
...
...
drivers/tptp-tff0.drv
View file @
9ed1be10
...
...
@@ -237,10 +237,35 @@ theory tptp.Real
syntax function to_real "$to_real(%1)"
end
theory real.FromInt
syntax function from_int "$to_real(%1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Truncate
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function floor "$to_int(%1)"
syntax function ceil "$to_int($ceil(%1))"
syntax function truncate "$to_int($truncate(%1))"
remove prop Truncate_int
remove prop Truncate_down_pos
remove prop Truncate_up_neg
remove prop Real_of_truncate
remove prop Truncate_monotonic
remove prop Truncate_monotonic_int1
remove prop Truncate_monotonic_int2
remove prop Floor_int
remove prop Ceil_int
remove prop Floor_down
remove prop Ceil_up
remove prop Floor_monotonic
remove prop Ceil_monotonic
end
theory tptp.RealTrunc
...
...
drivers/tptp-tff1.drv
View file @
9ed1be10
...
...
@@ -226,10 +226,35 @@ theory tptp.Real
syntax function to_real "$to_real(%1)"
end
theory real.FromInt
syntax function from_int "$to_real(%1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Truncate
syntax function floor "$floor(%1)"
syntax function ceil "$ceil(%1)"
syntax function truncate "$truncate(%1)"
syntax function floor "$to_int(%1)"
syntax function ceil "$to_int($ceil(%1))"
syntax function truncate "$to_int($truncate(%1))"
remove prop Truncate_int
remove prop Truncate_down_pos
remove prop Truncate_up_neg
remove prop Real_of_truncate
remove prop Truncate_monotonic
remove prop Truncate_monotonic_int1
remove prop Truncate_monotonic_int2
remove prop Floor_int
remove prop Ceil_int
remove prop Floor_down
remove prop Ceil_up
remove prop Floor_monotonic
remove prop Ceil_monotonic
end
theory tptp.RealTrunc
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment