[models] Add support for printing arrays (#659)

This patch adds the support for printing arrays in the models output.
Rather than printing default values, we print smtlib abstract values
(@xxx) for the unknown elements, because we don't have a default value
available easily otherwise.

The example model in #555 now displays as:

```smtlib2
(
  (define-fun x () Int 0)
  (define-fun y () Int 0)
  (define-fun a1 () (Array Int Int) (store (as @A1 (Array Int Int)) 0 0))
)
```

This also removes the "Functions" / "Constants" / "Arrays" sections
because they were now wrong (some arrays were in constants, other in
arrays) and hence somewhat confusing. Instead, the "values" section is
added then printing with `--model-type constraints`.

Uses of Printer.print_fmt have also been replaced with Format.fprintf
because they were causing weird looking outputs with some combinations
of options. Only the final value is printer with `print_fmt`, which
should do the appropriate (actually, I don't think it is needed here,
but better safe than sorry) cleanup dance only once.

Fixes #555

src/lib/frontend/models.ml

@@ -323,31 +323,34 @@ module SmtlibCounterExample = struct
       with _ -> t
     in
 
-    Printer.print_fmt ~flushed:false fmt
-      "(define-fun %a (%a) %a %s)@ "
+    Format.fprintf fmt
+      "@ (define-fun %a (%a) %a %s)"
       Sy.print name
       (Printer.pp_list_space (print_args)) args
       Ty.print ty
       defined_value
 
-  let output_constants_counterexample fmt records cprofs =
+  let output_constants_counterexample ?(ignored = Sy.Set.empty) fmt records =
     ModelMap.iter
       (fun (f, xs_ty, ty) st ->
          assert (xs_ty == []);
-         match ModelMap.V.elements st with
-         | [[], rep] ->
-           let rep = Format.asprintf "%a" x_print rep in
-           let rep =
-             match ty with
-             | Ty.Trecord r ->
-               let constr = mk_records_constr records f r in
-               sprintf "(%s)" constr
-             | _ -> rep
-           in
-
-           print_fun_def fmt f [] ty rep
-         | _ -> assert false
-      ) cprofs
+         begin match ty with
+           | Ty.Tfarray _ when Sy.Set.mem f ignored -> ()
+           | _ ->
+             match ModelMap.V.elements st with
+             | [[], rep] ->
+               let rep = Format.asprintf "%a" x_print rep in
+               let rep =
+                 match ty with
+                 | Ty.Trecord r ->
+                   let constr = mk_records_constr records f r in
+                   sprintf "(%s)" constr
+                 | _ -> rep
+               in
+
+               print_fun_def fmt f [] ty rep
+             | _ -> assert false
+         end)
 
   let output_functions_counterexample fmt records fprofs =
     let  records = ref records in
@@ -422,8 +425,28 @@ module SmtlibCounterExample = struct
       ) fprofs;
     !records
 
-  let output_arrays_counterexample fmt _arrays =
-    Printer.print_fmt fmt "@ ; Arrays not yet supported@ "
+  let output_arrays_counterexample fmt arrays =
+    let pp_array ppf (symbol, dty, st) =
+      let abstract =
+        Format.dprintf "(as @@%a %t)" Sy.print symbol dty
+      in
+      ModelMap.V.fold (fun (keys, (_value_r, value_s)) rst ->
+          Format.dprintf "(@[<hv>store@ %t@ %a %s)@]"
+            rst
+            Fmt.(list ~sep:sp (using (fun (_, (_, s)) -> s) string)) keys
+            value_s
+        ) st abstract ppf
+    in
+    let pp_array_ty ppf (args_ty, ret_ty) =
+      Format.fprintf ppf "(@[Array@ %a@ %a)@]"
+        Fmt.(list ~sep:sp Ty.print) args_ty
+        Ty.print ret_ty
+    in
+    ModelMap.iter
+      (fun (f, xs_ty, ty) st ->
+         let dty = Format.dprintf "%a" pp_array_ty (xs_ty, ty) in
+         Format.fprintf fmt "@ (@[define-fun %a () %t@ %a)@]"
+           Sy.print f dty pp_array (f, dty, st)) arrays
 
 end
 (* of module SmtlibCounterExample *)
@@ -432,41 +455,48 @@ module Why3CounterExample = struct
 
   let output_constraints fmt prop_model =
     let assertions = SE.fold (fun e acc ->
-        (asprintf "%s(assert %a)@ " acc SmtlibCounterExample.pp_term e)
-      ) prop_model "" in
-    Printer.print_fmt ~flushed:false fmt "@ ; constants@ ";
+        (dprintf "%t(assert %a)@ " acc SmtlibCounterExample.pp_term e)
+      ) prop_model (dprintf "") in
+    Format.fprintf fmt "@ ; constraints@ ";
     MS.iter (fun _ (name,ty,args_ty) ->
         match args_ty with
         | [] ->
-          Printer.print_fmt ~flushed:false fmt "(declare-const %s %s)@ "
+          Format.fprintf fmt "(declare-const %s %s)@ "
             name ty
         | l ->
-          Printer.print_fmt ~flushed:false fmt "(declare-fun %s (%s) %s)@ "
+          Format.fprintf fmt "(declare-fun %s (%s) %s)@ "
             name
             (String.concat " " l)
             ty
       ) !constraints;
-    Printer.print_fmt ~flushed:false fmt "@ ; assertions@ ";
-    Printer.print_fmt fmt ~flushed:false "%s" assertions
+    Format.fprintf fmt "@ ; assertions@ ";
+    Format.fprintf fmt "%t" assertions
 
 end
 (* of module Why3CounterExample *)
 
 let output_concrete_model fmt props ~functions ~constants ~arrays =
-  Printer.print_fmt ~flushed:false fmt "@[<v 2>(@,";
+  Format.fprintf fmt "@[<v 2>(";
   if Options.get_model_type_constraints () then
     begin
-      Why3CounterExample.output_constraints fmt props
+      Why3CounterExample.output_constraints fmt props;
+      Format.fprintf fmt "@ ; values"
     end;
 
-  Printer.print_fmt fmt "@ ; Functions@ ";
+  (* Functions *)
   let records = SmtlibCounterExample.output_functions_counterexample
       fmt  MS.empty functions in
 
-  Printer.print_fmt fmt "@ ; Constants@ ";
+  let array_symbols =
+    ModelMap.fold (fun (f, _, _) _ -> Sy.Set.add f) arrays Sy.Set.empty
+  in
+
+  (* Constants *)
+  (* If the constant is present in the arrays map, it will be printed there. *)
   SmtlibCounterExample.output_constants_counterexample
-    fmt records constants;
+    ~ignored:array_symbols fmt records constants;
 
+  (* Arrays *)
   SmtlibCounterExample.output_arrays_counterexample fmt arrays;
 
-  Printer.print_fmt fmt "@]@ )";
+  Printer.print_fmt fmt "@]@,)";

src/lib/reasoners/uf.ml

@@ -1085,4 +1085,3 @@ let save_cache () =
 
 let reinit_cache () =
   LX.reinit_cache ()
-

tests/cram.t/model555.smt2

@@ -0,0 +1,10 @@
+; From https://github.com/OCamlPro/alt-ergo/issues/555
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a1 (Array Int Int))
+(declare-const a2 (Array Int Int))
+(assert (= (select a1 x) x))
+(assert (= (store a1 x y) a1))
+(check-sat)
+(get-model)

tests/cram.t/run.t

@@ -3,3 +3,16 @@
   alt-ergo: ; Fatal Error: [Dynlink] Loading the 'inequalities' reasoner (FM module) plugin in "does-not-exist" failed!
             >> Failure message: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"$TESTCASE_ROOT/does-not-exist: cannot open shared object file: No such file or directory\")")
   [125]
+
+Now we will have some tests for the models. Note that it is okay if the format
+changes slightly, you should be concerned with ensuring the semantic is
+appropriate here.
+
+  $ alt-ergo --frontend dolmen --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null
+
+  unknown
+  (
+    (define-fun x () Int 0)
+    (define-fun y () Int 0)
+    (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+  )

tests/issues/555/models/555.expected

@@ -0,0 +1,7 @@
+
+unknown
+(
+  (define-fun x () Int 0)
+  (define-fun y () Int 0)
+  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+)

tests/issues/555/models/555.smt2

@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a1 (Array Int Int))
+(declare-const a2 (Array Int Int))
+(assert (= (select a1 x) x))
+(assert (= (store a1 x y) a1))
+(check-sat)
+(get-model)

tests/models/arith/arith1.expected

@@ -1,14 +1,5 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun x () Int 0)
-
- ; Arrays not yet supported
-
-
+  (define-fun x () Int 0)
 )

tests/models/arith/arith2.expected

@@ -1,16 +1,6 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun x () Int 8)
-
-(define-fun y () Int 42)
-
- ; Arrays not yet supported
-
-
+  (define-fun x () Int 8)
+  (define-fun y () Int 42)
 )

tests/models/bool/bool1.expected

@@ -1,30 +1,11 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
- ; Arrays not yet supported
-
-
 )
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
-(define-fun p () Bool true)
-
-(define-fun q () Bool true)
-
-(define-fun nq () Bool true)
-
- ; Arrays not yet supported
-
-
+  (define-fun p () Bool true)
+  (define-fun q () Bool true)
+  (define-fun nq () Bool true)
 )

tests/models/bool/bool2.expected

@@ -1,12 +1,4 @@
 
 unknown
 (
-
- ; Functions
-
- ; Constants
-
- ; Arrays not yet supported
-
-
 )

tests/models/uf/uf1.expected

@@ -1,18 +1,7 @@
 
 unknown
 (
-
- ; Functions
-
-(define-fun f ((arg_0 Int)) Int 0)
-
- ; Constants
-
-(define-fun a () Int 0)
-
-(define-fun b () Int 0)
-
- ; Arrays not yet supported
-
-
+  (define-fun f ((arg_0 Int)) Int 0)
+  (define-fun a () Int 0)
+  (define-fun b () Int 0)
 )

tests/models/uf/uf2.expected

@@ -1,18 +1,7 @@
 
 unknown
 (
-
- ; Functions
-
-(define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0))
-
- ; Constants
-
-(define-fun a () Int 0)
-
-(define-fun b () Int (- 2))
-
- ; Arrays not yet supported
-
-
+  (define-fun f ((arg_0 Int)) Int (ite (= arg_0 a) 2 0))
+  (define-fun a () Int 0)
+  (define-fun b () Int (- 2))
 )