Issue 705

CHANGES.md

@@ -1,5 +1,30 @@
 ## unreleased
 
+### New features
+* add context reinitialisation (PR #490)
+* add Dolmen frontend (PR #491,#541,#545)
+* add model generation (PR #530)
+* support mutually recursive definitions in the native language (PR #549, #550)
+* support of some options of the SMT-LIB statement (set-option) (PR #608)
+* support for the (get-model) statement (required the Dolmen frontend) (PR #614)
+* support ground reasoning with some bitvector primitives (PR #730, #733, #745).
+* improve the ite reasoning (simplification of some ites) (PR #731)
+
+### Build
+* update to the new version of ocplib-simplex (0.5)
+* remove the support of the deprecated library num. Alt-Ergo only uses Zarith (PR #600)
+* remove the deprecated graphical interface (PR #601)
+* use Dune >= 3.5.
+
+### Bug fixes
+* issue 475 (PR #478)
+* issue 504 (PR #524)
+* issue 509 (PR #524)
+* fix infinite loop in Expr.SMTPrinter (PR #540)
+* remove flattening of arithmetic expressions in order to fix some regressions (PR #566)
+* fix a leak memory in the vector module (PR #606)
+* issue 737 (PR #738)
+
 ## v2.4.3 (2023-04-14)
 
 ### Build

src/lib/frontend/models.ml

@@ -481,6 +481,11 @@ let pp_constant ppf (_, t) =
   Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
 
 let output_concrete_model fmt props ~functions ~constants ~arrays =
+  if ModelMap.(is_suspicious_model functions || is_suspicious_model constants
+               || is_suspicious_model arrays) then
+    Format.fprintf fmt "This model is a best-effort. Please note tht it \
+                        could be wrong. @.";
+
   Format.fprintf fmt "@[<v 2>(";
   if Options.get_model_type_constraints () then
     begin

src/lib/structures/modelMap.ml

@@ -80,24 +80,49 @@ module V = Set.Make
 
 type key = P.key
 type elt = V.t
-type t = V.t P.t
 
-let add p v mp =
-  let prof_p = try P.find p mp with Not_found -> V.empty in
-  if V.mem v prof_p then mp
-  else P.add p (V.add v prof_p) mp
+type t = {
+  values : V.t P.t;
+  suspicious : bool;
+}
 
-let iter f =
+let is_suspicious_name hs =
+  match Hstring.view hs with
+  | "@/" | "@%" | "@*" -> true
+  | _ -> false
+
+(* The model generation is not ready for FPA and Bitvector theories. *)
+let is_suspicious_symbol = function
+  | Sy.Op (Float | Fixed | Abs_int | Abs_real | Sqrt_real
+          | Sqrt_real_default | Sqrt_real_excess
+          | Real_of_int | Int_floor | Int_ceil
+          | Max_int | Max_real | Min_int | Min_real
+          | Pow | Integer_log2 | Int2BV _ | BV2Nat
+          | BVand | BVor | Integer_round) -> true
+  | Sy.Name (hs, _, _) when is_suspicious_name hs -> true
+  | _ -> false
+
+let add ((sy, _, _) as p) v { values; suspicious } =
+  let prof_p = try P.find p values with Not_found -> V.empty in
+  let values =
+    if V.mem v prof_p then values
+    else P.add p (V.add v prof_p) values
+  in
+  { values; suspicious = suspicious || is_suspicious_symbol sy }
+
+let iter f { values; _ } =
   P.iter (fun ((sy, _, _) as key) value ->
       match sy with
       | Sy.Name (_, _, true) ->
         (* We don't print constants defined by the user. *)
         ()
       | _ -> f key value
-    )
+    ) values
+
+let[@inline always] is_suspicious_model { suspicious; _ } = suspicious
 
-let fold = P.fold
+let fold f { values; _ } acc = P.fold f values acc
 
-let empty = P.empty
+let empty = { values = P.empty; suspicious = false }
 
-let is_empty = P.is_empty
+let is_empty { values; _ } = P.is_empty values

src/lib/structures/modelMap.mli

@@ -42,7 +42,8 @@ module V : Set.S with type elt =
 
 type key = P.key
 type elt = V.t
-type t = V.t P.t
+
+type t
 
 val add : key -> V.elt -> t -> t
 
@@ -53,3 +54,7 @@ val fold : (key -> elt -> 'acc -> 'acc) -> t -> 'acc -> 'acc
 val empty : t
 
 val is_empty : t -> bool
+
+val is_suspicious_model : t -> bool
+(* Determine if the model is suspicious as it contains symbols
+   of theories for which the model generation is not properly supported. *)