From 26afeaf52edd339b158dfbfc3b47d4232041e02f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Tue, 17 Sep 2024 15:29:10 +0200 Subject: [PATCH] fix: Make sure model generation is complete for more operators (#1234) 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. --- docs/sphinx_docs/Model_generation.md | 13 +++++---- src/lib/frontend/d_cnf.ml | 5 ++++ src/lib/frontend/typechecker.ml | 3 ++ src/lib/reasoners/intervalCalculus.ml | 40 +++++++++++++++++++++++++++ src/lib/structures/expr.ml | 1 - 5 files changed, 55 insertions(+), 7 deletions(-) diff --git a/docs/sphinx_docs/Model_generation.md b/docs/sphinx_docs/Model_generation.md index a6098dd75..56227d6ec 100644 --- a/docs/sphinx_docs/Model_generation.md +++ b/docs/sphinx_docs/Model_generation.md @@ -40,9 +40,9 @@ 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` @@ -50,14 +50,15 @@ following constructs: 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 diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 7c417b946..d63c835dd 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/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 diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 569b4f85d..7dfc844a9 100644 --- a/src/lib/frontend/typechecker.ml +++ b/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) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index a11045bf6..5e037b74a 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/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 = { diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7fec2a89e..7c726bafc 100644 --- a/src/lib/structures/expr.ml +++ b/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