Merge branch 'OCamlPro:next' into bv-primitives

OCamlPro · Jul 10, 2023 · be74d71 · be74d71
2 parents 0405db3 + 9422063
commit be74d71
Show file tree

Hide file tree

Showing 6 changed files with 67 additions and 31 deletions.
diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml
@@ -212,12 +212,12 @@ let assume env _ la =
 let assume env uf la =
   if Options.get_timers() then
     try
-      Timers.exec_timer_start Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_start Timers.M_Ite Timers.F_assume;
       let res =assume env uf la in
-      Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_pause Timers.M_Ite Timers.F_assume;
       res
     with e ->
-      Timers.exec_timer_pause Timers.M_Arrays Timers.F_assume;
+      Timers.exec_timer_pause Timers.M_Ite Timers.F_assume;
       raise e
   else assume env uf la
 

diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml
@@ -43,22 +43,24 @@ type ty_module =
   | M_Expr
   | M_Triggers
   | M_Simplex
+  | M_Ite
 
 let mtag k = match k with
-  | M_None   -> 0
-  | M_Typing -> 1
-  | M_Sat    -> 2
-  | M_Match  -> 3
-  | M_CC     -> 4
-  | M_UF     -> 5
-  | M_Arith  -> 6
-  | M_Arrays -> 7
-  | M_Sum    -> 8
-  | M_Records-> 9
-  | M_AC     -> 10
-  | M_Expr-> 11
-  | M_Triggers->12
-  | M_Simplex->13
+  | M_None     -> 0
+  | M_Typing   -> 1
+  | M_Sat      -> 2
+  | M_Match    -> 3
+  | M_CC       -> 4
+  | M_UF       -> 5
+  | M_Arith    -> 6
+  | M_Arrays   -> 7
+  | M_Sum      -> 8
+  | M_Records  -> 9
+  | M_AC       -> 10
+  | M_Expr     -> 11
+  | M_Triggers -> 12
+  | M_Simplex  -> 13
+  | M_Ite      -> 14
 
 let nb_mtag = 14
 
@@ -109,20 +111,21 @@ let ftag f = match f with
 let nb_ftag = 20
 
 let string_of_ty_module k = match k with
-  | M_None   -> "None"
-  | M_Typing -> "Typing"
-  | M_Sat    -> "Sat"
-  | M_Match  -> "Match"
-  | M_CC     -> "CC"
-  | M_UF     -> "UF"
-  | M_Arith  -> "Arith"
-  | M_Arrays -> "Arrays"
-  | M_Sum    -> "Sum"
-  | M_Records-> "Records"
-  | M_AC     -> "AC"
-  | M_Expr-> "Expr"
-  | M_Triggers->"Triggers"
-  | M_Simplex->"Simplex"
+  | M_None     -> "None"
+  | M_Typing   -> "Typing"
+  | M_Sat      -> "Sat"
+  | M_Match    -> "Match"
+  | M_CC       -> "CC"
+  | M_UF       -> "UF"
+  | M_Arith    -> "Arith"
+  | M_Arrays   -> "Arrays"
+  | M_Sum      -> "Sum"
+  | M_Records  -> "Records"
+  | M_AC       -> "AC"
+  | M_Expr     -> "Expr"
+  | M_Triggers -> "Triggers"
+  | M_Simplex  -> "Simplex"
+  | M_Ite      -> "Ite"
 
 let string_of_ty_function f = match f with
   | F_add           -> "add"

diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli
@@ -43,6 +43,7 @@ type ty_module =
   | M_Expr
   | M_Triggers
   | M_Simplex
+  | M_Ite
 
 type ty_function =
   | F_add

diff --git a/src/preludes/ria.ae b/src/preludes/ria.ae
@@ -56,6 +56,34 @@ theory Real_of_Int extends RIA =
      {i <= real_of_int(x)}.
      k <= x
 
+  (* floor(x) ≤ i iff x < i + 1 *)
+  axiom int_floor_ub:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in ]?, i], y |-> real_of_int(i + 1) ]
+    { int_floor(x) <= i }.
+    x < y
+
+  (* i <= floor(x) iff i <= x *)
+  axiom int_floor_lb:
+    forall x, y : real, i : int
+    [ int_floor(x), not_theory_constant(x), int_floor(x) in [i, ?[, y |-> real_of_int(i) ]
+    { i <= int_floor(x) }.
+    y <= x
+
+  (* ceil(x) ≤ i iff x ≤ i *)
+  axiom int_ceil_ub:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in ]?, i], y |-> real_of_int(i) ]
+    { int_ceil(x) <= i }.
+    x <= y
+
+  (* i <= ceil(x) iff i - 1 < x *)
+  axiom int_ceil_lb:
+    forall x, y : real, i : int
+    [ int_ceil(x), not_theory_constant(x), int_ceil(x) in [i, ?[, y |-> real_of_int(i - 1) ]
+    { i <= int_ceil(x) }.
+    y < x
+
    (* can add other axioms on strict ineqs on rationals ? *)
 
 end

diff --git a/tests/arith/ceil_floor_propagate.ae b/tests/arith/ceil_floor_propagate.ae
@@ -0,0 +1,2 @@
+logic x: real
+goal g: int_ceil(x) = 0 and int_floor(x) = 0 -> x = 0.
diff --git a/tests/arith/ceil_floor_propagate.expected b/tests/arith/ceil_floor_propagate.expected
@@ -0,0 +1,2 @@
+
+unknown