fix: Make sure model generation is complete for more operators (#1234) (#1238)

Some RIA operators are not complete even in the presence of the
corresponding prelude. Add them as delayed functions to ensure we loop
rather than generating an incorrect model.

Author: bclement-ocp

docs/sphinx_docs/Model_generation.md

@@ -40,24 +40,25 @@ following constructs:
  - Algebraic data types (including records and enumerated types in the native
    language)
 
- - Integer and real primitives (addition, subtraction, multiplication,
-   division, modulo, exponentiation, and comparisons), but not conversion
-   operators between reals and integers
+ - The following integer and real primitives: addition, subtraction,
+   multiplication, division, modulo, comparisons, and exponentiations *with an
+   integer exponent*
 
  - Bit-vector primitives (concatenation, extraction, `bvadd`, `bvand`, `bvule`,
    etc.), including `bv2nat` and `int2bv`
 
 Completeness for the following constructs is only guaranteed with certain
 command-line flags:
 
- - Conversions operators between integers and reals require the
-   `--enable-theories ria` flag
+ - Conversions operators from integers to reals `real_of_int` and `real_is_int`
+   require the `--enable-theories ria` flag
 
  - Floating-point primitives (`ae.round`, `ae.float32` etc. in the SMT-LIB
    language; `float`, `float32` and `float64` in the native language) require
    the `--enable-theories fpa` flag
 
-Model generation is known to be sometimes incomplete in the presence of arrays.
+Model generation is known to be sometimes incomplete in the presence of arrays,
+and is incomplete for the `integer_round` function.
 
 ## Examples
 

src/lib/frontend/d_cnf.ml

@@ -164,6 +164,7 @@ type _ DStd.Builtin.t +=
   | Sqrt_real_excess
   | Ceiling_to_int of [ `Real ]
   | Max_real
+  | Min_real
   | Max_int
   | Min_int
   | Integer_log2
@@ -360,6 +361,9 @@ let ae_fpa_builtins =
     (* maximum of two reals *)
     |> op "max_real" Max_real ([real; real] ->. real)
 
+    (* minimum of two reals *)
+    |> op "min_real" Min_real ([real; real] ->. real)
+
     (* maximum of two ints *)
     |> op "max_int" Max_int ([int; int] ->. int)
 
@@ -1349,6 +1353,7 @@ let rec mk_expr
           | B.Is_int `Real, _ -> op Real_is_int
           | Ceiling_to_int `Real, _ -> op Int_ceil
           | Max_real, _ -> op Max_real
+          | Min_real, _ -> op Min_real
           | Max_int, _ -> op Max_int
           | Min_int, _ -> op Min_int
           | Integer_log2, _ -> op Integer_log2

src/lib/frontend/typechecker.ml

@@ -404,6 +404,9 @@ module Env = struct
       (* maximum of two reals *)
       |> op "max_real" Max_real ([real; real] ->. real)
 
+      (* minimum of two reals *)
+      |> op "min_real" Min_real ([real; real] ->. real)
+
       (* maximum of two ints *)
       |> op "max_int" Max_int ([int; int] ->. int)
 

src/lib/reasoners/intervalCalculus.ml

@@ -676,11 +676,51 @@ let delayed_pow uf _op = function
   | [ a; b ] -> calc_pow a b (E.type_info a) uf
   | _ -> assert false
 
+let delayed_op1 ~ty fn uf _op = function
+  | [ x ] ->
+    let rx, exx = Uf.find uf x in
+    Option.bind (P.is_const (poly_of rx)) @@ fun cx ->
+    Some (alien_of (P.create [] (fn cx) ty), exx)
+  | _ -> assert false
+
+let delayed_op2 ~ty fn uf _op = function
+  | [ x; y ] ->
+    let rx, exx = Uf.find uf x in
+    let ry, exy = Uf.find uf y in
+    Option.bind (P.is_const (poly_of rx)) @@ fun cx ->
+    Option.bind (P.is_const (poly_of ry)) @@ fun cy ->
+    Some (alien_of (P.create [] (fn cx cy) ty), Ex.union exx exy)
+  | _ -> assert false
+
+let delayed_integer_log2 uf _op = function
+  | [ x ] -> (
+      let rx, exx = Uf.find uf x in
+      let px = poly_of rx in
+      match P.is_const px with
+      | None -> None
+      | Some cb ->
+        if Q.compare cb Q.zero <= 0 then None
+        else
+          let res =
+            alien_of @@
+            P.create [] (Q.from_int (Fpa_rounding.integer_log_2 cb)) Treal
+          in
+          Some (res, exx)
+    )
+  | _ -> assert false
+
 (* These are the partially interpreted functions that we know how to compute.
    They will be computed immediately if possible, or as soon as we learn the
    value of their arguments. *)
 let dispatch = function
   | Symbols.Pow -> Some delayed_pow
+  | Symbols.Integer_log2 -> Some delayed_integer_log2
+  | Symbols.Int_floor -> Some (delayed_op1 ~ty:Tint Numbers.Q.floor)
+  | Symbols.Int_ceil -> Some (delayed_op1 ~ty:Tint Numbers.Q.ceiling)
+  | Symbols.Min_int -> Some (delayed_op2 ~ty:Tint Q.min)
+  | Symbols.Max_int -> Some (delayed_op2 ~ty:Tint Q.max)
+  | Symbols.Min_real -> Some (delayed_op2 ~ty:Treal Q.min)
+  | Symbols.Max_real -> Some (delayed_op2 ~ty:Treal Q.max)
   | _ -> None
 
 let empty uf = {

src/lib/structures/expr.ml

@@ -2958,7 +2958,6 @@ let int_view t =
   | _ ->
     Fmt.failwith "The given term %a is not an integer" print t
 
-
 let rounding_mode_view t =
   match const_view t with
   | RoundingMode m -> m