accumulate record accesses

src/lib/frontend/models.ml

@@ -261,29 +261,33 @@ module SmtlibCounterExample = struct
     MS.add record_name destrs records
 
   let mk_records_constr records record_name
-      { Ty.name = _n; record_constr = cstr; lbs = lbs; _} =
+      { Ty.record_constr = cstr; lbs; _ } =
     let find_destrs destr destrs =
       try let rep = MS.find destr destrs in
         Some rep
       with Not_found -> None
     in
 
-    let print_destr fmt (destrs,lbs) =
-      List.iter (fun (destr, ty_destr) ->
-          let destr = Hstring.view destr in
-          match find_destrs destr destrs with
-          | None ->
-            pp_dummy_value_of_type fmt ty_destr
-          | Some rep -> fprintf fmt "%s " rep
-        ) lbs
+    let pp_destr destrs ppf (destr, ty_destr) =
+      match find_destrs (Hstring.view destr) destrs with
+      | None ->
+        Fmt.pf ppf "%a"
+          pp_dummy_value_of_type ty_destr
+      | Some rep ->
+        Fmt.pf ppf "%s" rep
     in
+
+    let pp_destrs destrs =
+      Fmt.list ~sep:(fun ppf () -> Fmt.pf ppf " ") (pp_destr destrs)
+    in
+
     let destrs =
       try MS.find (Sy.to_string record_name) records
       with Not_found -> MS.empty
     in
     asprintf "%s %a"
       (Hstring.view cstr)
-      print_destr (destrs,lbs)
+      (pp_destrs destrs) lbs
 
   let add_record_constr records record_name
       { Ty.name = _n; record_constr = _cstr; lbs = lbs; _} xs_values =
@@ -480,7 +484,7 @@ let rec pp_value ppk ppf = function
 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 =
+let output_concrete_model fmt props ~functions ~constants ~arrays ~records =
   if ModelMap.(is_suspicious functions || is_suspicious constants
                || is_suspicious arrays) then
     Format.fprintf fmt "; This model is a best-effort. It includes symbols
@@ -524,7 +528,7 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
 
   (* Functions *)
   let records = SmtlibCounterExample.output_functions_counterexample
-      pp_x fmt  MS.empty functions
+      pp_x fmt records functions
   in
 
   (* Constants *)

src/lib/frontend/models.mli

@@ -28,6 +28,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module MS : Map.S with type key = string
+
 (** {1 Models module} *)
 
 (** Print the given counterexample on the given formatter with the
@@ -42,4 +44,5 @@ val output_concrete_model :
   functions:ModelMap.t ->
   constants:ModelMap.t ->
   arrays:ModelMap.t ->
+  records:string MS.t MS.t ->
   unit

src/lib/reasoners/shostak.ml

@@ -330,10 +330,10 @@ struct
   let is_solvable_theory_symbol sb ty =
     X1.is_mine_symb sb ty ||
     not (Options.get_restricted ()) &&
-    (X2.is_mine_symb sb ty ||
-     X3.is_mine_symb sb ty ||
-     X4.is_mine_symb sb ty ||
-     X5.is_mine_symb sb ty)
+    ((*X2.is_mine_symb sb ty || *)
+      X3.is_mine_symb sb ty ||
+      X4.is_mine_symb sb ty ||
+      X5.is_mine_symb sb ty)
 
 
   let is_a_leaf r = match r.v with

src/lib/reasoners/uf.ml

@@ -36,6 +36,7 @@ module Ex = Explanation
 module Sy = Symbols
 module E = Expr
 module ME = Expr.Map
+module MS = Models.MS
 module SE = Expr.Set
 
 module LX =
@@ -1024,7 +1025,7 @@ let model_repr_of_term t env mrepr =
 
 let compute_concrete_model ({ make; _ } as env) =
   ME.fold
-    (fun t _mk ((fprofs, cprofs, carrays, mrepr) as acc) ->
+    (fun t _mk ((fprofs, cprofs, carrays, crecords, mrepr) as acc) ->
        let { E.f; xs; ty; _ } = E.term_view t in
        if X.is_solvable_theory_symbol f ty
        || E.is_fresh t || E.is_fresh_skolem t
@@ -1045,6 +1046,22 @@ let compute_concrete_model ({ make; _ } as env) =
          let rep, mrepr = model_repr_of_term t env mrepr in
          assert (is_a_good_model_value rep);
          match f, xs, ty with
+         | Sy.Op Sy.Record, _, _ -> acc
+
+         | Sy.Op Sy.Access field, [(_, (_, srep))], _ ->
+           let fields =
+             let fields =
+               try MS.find srep crecords
+               with Not_found -> MS.empty
+             in
+             MS.add (Hstring.view field) (snd rep) fields
+           in
+           fprofs,
+           cprofs,
+           carrays,
+           MS.add srep fields crecords,
+           mrepr
+
          | Sy.Op Sy.Set, _, _ -> acc
 
          | Sy.Op Sy.Get, [(_,(a,_));((_,(i,_)) as e)], _ ->
@@ -1056,6 +1073,7 @@ let compute_concrete_model ({ make; _ } as env) =
                fprofs,
                cprofs,
                ModelMap.add (f_ta,[X.type_info i], ty) ([e], rep) carrays,
+               crecords,
                mrepr
 
              | _ -> assert false
@@ -1064,19 +1082,18 @@ let compute_concrete_model ({ make; _ } as env) =
          | _ ->
            if tys == [] then
              fprofs, ModelMap.add (f, tys, ty) (xs, rep) cprofs, carrays,
-             mrepr
+             crecords, mrepr
            else
              ModelMap.add (f, tys, ty) (xs, rep) fprofs, cprofs, carrays,
-             mrepr
+             crecords, mrepr
 
     ) make
-    (ModelMap.empty, ModelMap.empty, ModelMap.empty, ME.empty)
+    (ModelMap.empty, ModelMap.empty, ModelMap.empty, MS.empty, ME.empty)
 
 let output_concrete_model fmt ~prop_model env =
   if Options.get_interpretation () then
-    let functions, constants, arrays, _ =
-      compute_concrete_model env in
-    Models.output_concrete_model fmt prop_model ~functions ~constants ~arrays
+    let functions, constants, arrays, records, _ = compute_concrete_model env in
+    Models.output_concrete_model fmt prop_model ~functions ~constants ~arrays ~records
 
 let save_cache () =
   LX.save_cache ()

tests/dune.inc

@@ -186808,6 +186808,31 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir models/record
+  (rule
+   (target record1.models_tableaux.output)
+   (deps (:input record1.models.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --output=smtlib2
+             --frontend dolmen
+             --timelimit=2
+             --sat-solver Tableaux
+             %{input})))))))
+  (rule
+   (alias runtest-quick)
+    (package alt-ergo)
+     (action
+      (diff record1.models.expected record1.models_tableaux.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir models/uf
   (rule

tests/models/record/record1.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun a () Pair (pair 5 0))
+)

tests/models/record/record1.models.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-datatype Pair
+((pair (first Int) (second Int))))
+(declare-const a Pair)
+(assert (= (first a) 5))
+(check-sat)
+(get-model)