From f61fc4b14939555c31de72543be20ac15987ca1e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Sat, 7 Sep 2024 13:45:07 +0200 Subject: [PATCH] fix: Make sure model generation is complete for more operators 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