From 36fb88c3795c8a493bdec49582190cf4bbcc66f1 Mon Sep 17 00:00:00 2001
From: Pierrot <tiky.halbaroth@gmail.com>
Date: Mon, 11 Sep 2023 17:11:02 +0200
Subject: [PATCH] Replace dummy values in Model by abstract values (#804)

---
 src/lib/frontend/models.ml                   | 28 ++++++++------------
 tests/cram.t/run.t                           |  3 +--
 tests/issues/555.models.expected             |  3 +--
 tests/models/records/record1.models.expected |  2 +-
 4 files changed, 14 insertions(+), 22 deletions(-)

diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index a9533764e..fef43a5bf 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -236,20 +236,11 @@ module SmtlibCounterExample = struct
     else
       E.print fmt t
 
-  let rec pp_dummy_value_of_type ppf ty =
-    match ty with
-      Ty.Tint -> Fmt.pf ppf "0"
-    | Ty.Treal -> Fmt.pf ppf "0.0"
-    | Ty.Tbool -> Fmt.pf ppf "false"
-    | Ty.Tfarray (_, rty) ->
-      Fmt.pf ppf "((as const %a) %a)" Ty.pp_smtlib ty pp_dummy_value_of_type rty
-    | _ -> Fmt.pf ppf "@@%a" pp_term (Expr.fresh_name ty)
-
-  let pp_dummy_value_of_type fmt ty =
-    if not (Options.get_interpretation_use_underscore ()) then
-      pp_dummy_value_of_type fmt ty
+  let pp_abstract_value_of_type ppf (name, ty) =
+    if not @@ Options.get_interpretation_use_underscore () then
+      Fmt.pf ppf "(as @@%s %a)" name Ty.pp_smtlib ty
     else
-      fprintf fmt "_ "
+      Fmt.pf ppf "_ "
 
   let add_records_destr records record_name destr_name rep =
     let destrs =
@@ -273,7 +264,8 @@ module SmtlibCounterExample = struct
           let destr = Hstring.view destr in
           match find_destrs destr destrs with
           | None ->
-            pp_dummy_value_of_type fmt ty_destr
+            let name = Hstring.fresh_string () in
+            pp_abstract_value_of_type fmt (name, ty_destr)
           | Some rep -> fprintf fmt "%s " rep
         ) lbs
     in
@@ -396,7 +388,8 @@ module SmtlibCounterExample = struct
 
            let rec reps_aux reps =
              match reps with
-             | [] -> dprintf "%a" pp_dummy_value_of_type ty
+             | [] -> dprintf "%a" pp_abstract_value_of_type
+                       (Symbols.to_string f, ty)
              | [srep,xs_values_list] ->
                if Options.get_interpretation_use_underscore () then
                  dprintf "(@[<hv>ite %t@ %a@ %t)@]"
@@ -483,8 +476,9 @@ let rec pp_value ppk ppf = function
   | Constant (sy, t) -> ppk ppf (sy, t)
   | Value (_, s) -> Format.pp_print_string ppf s
 
-let pp_constant ppf (_, t) =
-  Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
+let pp_constant ppf (sy, t) =
+  Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type
+    (Symbols.to_string sy, t)
 
 let output_concrete_model fmt props ~functions ~constants ~arrays =
   if ModelMap.(is_suspicious functions || is_suspicious constants
diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t
index b12111977..d6ea52647 100644
--- a/tests/cram.t/run.t
+++ b/tests/cram.t/run.t
@@ -11,8 +11,7 @@ appropriate here.
   
   unknown
   (
-    (define-fun a1 () (Array Int Int)
-     (store ((as const (Array Int Int)) 0) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
     (define-fun x () Int 0)
     (define-fun y () Int 0)
   )
diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected
index e81320831..b29c7ff8c 100644
--- a/tests/issues/555.models.expected
+++ b/tests/issues/555.models.expected
@@ -1,8 +1,7 @@
 
 unknown
 (
-  (define-fun a1 () (Array Int Int)
-   (store ((as const (Array Int Int)) 0) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
   (define-fun x () Int 0)
   (define-fun y () Int 0)
 )
diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected
index da5e88f8f..20e26682b 100644
--- a/tests/models/records/record1.models.expected
+++ b/tests/models/records/record1.models.expected
@@ -1,5 +1,5 @@
 
 unknown
 (
-  (define-fun a () Pair (pair 5 0))
+  (define-fun a () Pair (pair 5 (as @!k3 Int)))
 )