fix the fix in e548a9c5d

drivers/beagle.drv

@@ -151,7 +151,7 @@ end
 
 theory tptp.IntTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -219,7 +219,7 @@ end
 
 theory tptp.RatTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -258,7 +258,7 @@ end
 
 theory real.Truncate
   syntax function floor    "$to_int(%1)"
-  syntax function ceil     "$to_int($ceil(%1))"
+  syntax function ceil     "$to_int($ceiling(%1))"
   syntax function truncate "$to_int($truncate(%1))"
 
   remove prop Truncate_int
@@ -277,6 +277,9 @@ theory real.Truncate
 end
 
 theory tptp.RealTrunc
+  syntax function floor    "$floor(%1)"
+  syntax function ceiling  "$ceiling(%1)"
+  syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
   syntax function to_int   "$to_int(%1)"

drivers/princess.drv

@@ -148,7 +148,7 @@ end
 
 theory tptp.IntTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -216,7 +216,7 @@ end
 
 theory tptp.RatTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -255,7 +255,7 @@ end
 
 theory real.Truncate
   syntax function floor    "$to_int(%1)"
-  syntax function ceil     "$to_int($ceil(%1))"
+  syntax function ceil     "$to_int($ceiling(%1))"
   syntax function truncate "$to_int($truncate(%1))"
 
   remove prop Truncate_int
@@ -274,6 +274,9 @@ theory real.Truncate
 end
 
 theory tptp.RealTrunc
+  syntax function floor    "$floor(%1)"
+  syntax function ceiling  "$ceiling(%1)"
+  syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
   syntax function to_int   "$to_int(%1)"

drivers/tptp-tff0.drv

@@ -143,7 +143,7 @@ end
 
 theory tptp.IntTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -211,7 +211,7 @@ end
 
 theory tptp.RatTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -250,7 +250,7 @@ end
 
 theory real.Truncate
   syntax function floor    "$to_int(%1)"
-  syntax function ceil     "$to_int($ceil(%1))"
+  syntax function ceil     "$to_int($ceiling(%1))"
   syntax function truncate "$to_int($truncate(%1))"
 
   remove prop Truncate_int
@@ -269,6 +269,9 @@ theory real.Truncate
 end
 
 theory tptp.RealTrunc
+  syntax function floor    "$floor(%1)"
+  syntax function ceiling  "$ceiling(%1)"
+  syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
   syntax function to_int   "$to_int(%1)"

drivers/tptp-tff1.drv

@@ -134,7 +134,7 @@ end
 
 theory tptp.IntTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -200,7 +200,7 @@ end
 
 theory tptp.RatTrunc
   syntax function floor    "$floor(%1)"
-  syntax function ceil     "$ceil(%1)"
+  syntax function ceiling  "$ceiling(%1)"
   syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
@@ -239,7 +239,7 @@ end
 
 theory real.Truncate
   syntax function floor    "$to_int(%1)"
-  syntax function ceil     "$to_int($ceil(%1))"
+  syntax function ceil     "$to_int($ceiling(%1))"
   syntax function truncate "$to_int($truncate(%1))"
 
   remove prop Truncate_int
@@ -258,6 +258,9 @@ theory real.Truncate
 end
 
 theory tptp.RealTrunc
+  syntax function floor    "$floor(%1)"
+  syntax function ceiling  "$ceiling(%1)"
+  syntax function truncate "$truncate(%1)"
   syntax function round    "$round(%1)"
 
   syntax function to_int   "$to_int(%1)"

plugins/tptp/tptp_typing.ml

@@ -171,7 +171,7 @@ let defined_arith ~loc denv env impl dw tl =
     | DF DFrem_t -> ns_find_ls th.th_export ["mod_t"]
     | DF DFrem_f -> ns_find_ls th.th_export ["mod_f"]
     | DF DFfloor -> ns_find_ls th.th_export ["floor"]
-    | DF DFceil -> ns_find_ls th.th_export ["ceil"]
+    | DF DFceil -> ns_find_ls th.th_export ["ceiling"]
     | DF DFtrunc -> ns_find_ls th.th_export ["truncate"]
     | DF DFround -> ns_find_ls th.th_export ["round"]
     | DF DFtoint -> ns_find_ls th.th_export ["to_int"]

theories/tptp.why

@@ -14,7 +14,7 @@ end
 
 theory IntTrunc
   function floor (x : int) : int = x
-  function ceil (x : int) : int = x
+  function ceiling (x : int) : int = x
   function truncate (x : int) : int = x
   function round (x : int) : int = x
 
@@ -83,7 +83,7 @@ theory RatTrunc
 
   (* TODO: axiomatize *)
   function floor (x : rat) : rat
-  function ceil (x : rat) : rat
+  function ceiling (x : rat) : rat
   function truncate (x : rat) : rat
   function round (x : rat) : rat
 
@@ -121,17 +121,21 @@ end
 
 theory RealTrunc
   use import Real
-  use import real.FromInt
-  use export real.Truncate
+  use real.FromInt
+  use real.Truncate
+
+  function floor (x : real) : real = FromInt.from_int (Truncate.floor x)
+  function ceiling (x : real) : real = FromInt.from_int (Truncate.ceil x)
+  function truncate (x : real) : real = FromInt.from_int (Truncate.truncate x)
 
   (* TODO : axiomatize *)
   function round (x : real) : real
 
-  function to_int (x : real) : int = floor x
+  function to_int (x : real) : int = Truncate.floor x
 
-  predicate is_int (r : real) = r = from_int (truncate r)
+  predicate is_int (r : real) = r = FromInt.from_int (Truncate.truncate r)
   predicate is_rat (r : real) =
-    exists n d : int. d <> 0 /\ r * from_int d = from_int n
+    exists n d : int. d <> 0 /\ r * FromInt.from_int d = FromInt.from_int n
 end
 
 theory RealDivE
@@ -159,9 +163,9 @@ theory IntToRat
 end
 
 theory IntToReal
-  use import real.FromInt
+  use real.FromInt
 
-  function to_real (x : int) : real = from_int x
+  function to_real (x : int) : real = FromInt.from_int x
 end
 
 theory RealToRat
@@ -174,8 +178,8 @@ end
 theory RatToReal
   use import Rat
   use import real.Real
-  use import real.FromInt
+  use real.FromInt
 
   function to_real (x : rat) : real =
-    from_int (numerator x) / from_int (denominator x)
+    FromInt.from_int (numerator x) / FromInt.from_int (denominator x)
 end