Treat missing values in models as abstract (#860)

When printing models, we can end up with class representatives that are
not actually in the model. This can happen if a class representative is
a defined constant, but also if it is an intermediate fresh constant
introduced by the solver (!kXXX). This is because, in a class containing
only uninterpreted terms, the representative will be the minimum term,
independently of whether it is defined or fresh.

This patch records and adds such terms to the `values` table as a
(named) `Abstract` constant. This ensures that the same abstract value
is used for all uses of a given constant.

This is backported from a0575d2 for branch 2.5.x.

Fixes #854

src/lib/frontend/models.ml

@@ -243,7 +243,8 @@ module SmtlibCounterExample = struct
     | 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)
+    | _ ->
+      Fmt.pf ppf "(as @@%a %a)" pp_term (Expr.fresh_name ty) Ty.pp_smtlib ty
 
   let pp_dummy_value_of_type fmt ty =
     if not (Options.get_interpretation_use_underscore ()) then
@@ -457,6 +458,8 @@ type value_defn =
   | Value of X.r * string
   (* A leaf semantic value. This must be an actual value, i.e. it must not
      contain any uninterpreted terms. *)
+  | Abstract of string
+  (* An unique abstract value *)
 
 let value (r, s) =
   match X.term_extract r with
@@ -476,6 +479,7 @@ let rec pp_value ppk ppf = function
       (pp_value ppk) v
   | Constant (sy, t) -> ppk ppf (sy, t)
   | Value (_, s) -> Format.pp_print_string ppf s
+  | Abstract s -> Format.pp_print_string ppf s
 
 let pp_constant ppf (_, t) =
   Format.fprintf ppf "%a" SmtlibCounterExample.pp_dummy_value_of_type t
@@ -494,6 +498,13 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
     end;
 
   let values = Hashtbl.create 17 in
+  let find_or_add sy f =
+    try Hashtbl.find values sy
+    with Not_found ->
+      let value = f () in
+      Hashtbl.replace values sy value;
+      value
+  in
   (* Add the constants *)
   ModelMap.iter (fun (f, xs_ty, _) st ->
       assert (Lists.is_empty xs_ty);
@@ -516,8 +527,16 @@ let output_concrete_model fmt props ~functions ~constants ~arrays =
     arrays;
 
   let pp_value =
-    pp_value (fun ppf (sy, _) ->
-        pp_value pp_constant ppf (Hashtbl.find values sy))
+    pp_value (fun ppf (sy, ty) ->
+        let v =
+          find_or_add sy @@ fun () ->
+          (* NB: It is important that we call `pp_dummy_value_of_type`
+             immediately (not in a delayed fashion) so that we make sure that
+             the same abstract value will get printed each time. *)
+          Abstract (
+            Fmt.to_to_string SmtlibCounterExample.pp_dummy_value_of_type ty)
+        in
+        pp_value pp_constant ppf v)
   in
 
   let pp_x ppf xs = pp_value ppf (value xs) in

tests/dune.inc

@@ -117958,9 +117958,8 @@
       (ignore-stderr
        (with-accepted-exit-codes 0
         (run %{bin:alt-ergo}
-             --timelimit=2
-             --enable-assertions
              --output=smtlib2
+             --timelimit=2
              --frontend dolmen
              %{input})))))))
   (rule
@@ -173288,6 +173287,71 @@
 ; Auto-generated part end
 ; File auto-generated by gentests
 
+; Auto-generated part begin
+(subdir issues/854
+  (rule
+   (target twice_eq.models_tableaux.output)
+   (deps (:input twice_eq.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 twice_eq.models.expected twice_eq.models_tableaux.output)))
+  (rule
+   (target original.models_tableaux.output)
+   (deps (:input original.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 original.models.expected original.models_tableaux.output)))
+  (rule
+   (target function.models_tableaux.output)
+   (deps (:input function.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 function.models.expected function.models_tableaux.output))))
+; Auto-generated part end
+; File auto-generated by gentests
+
 ; Auto-generated part begin
 (subdir ite
   (rule

tests/issues/854/function.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k2 intref))
+  (define-fun f ((arg_0 Int)) Int 0)
+  (define-fun a () Int 0)
+  (define-fun a1 () Int 0)
+)

tests/issues/854/function.models.smt2

@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-option :produce-models true)
+(declare-sort intref 0)
+(declare-fun intrefqtmk (Int) intref)
+(declare-fun a () Int)
+(declare-fun f (Int) Int)
+(define-fun aqtunused ((x Int)) intref (intrefqtmk (f a)))
+(assert (= (aqtunused 0) (aqtunused 1)))
+(declare-fun a1 () Int)
+(assert (not (and (<= 5 a1) (<= a1 15))))
+(check-sat)
+(get-model)

tests/issues/854/original.models.expected

@@ -0,0 +1,7 @@
+
+unknown
+(
+  (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k1 intref))
+  (define-fun a () Int 0)
+  (define-fun a1 () Int 0)
+)

tests/issues/854/original.models.smt2

@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-option :produce-models true)
+(declare-sort intref 0)
+(declare-fun intrefqtmk (Int) intref)
+(declare-fun a () Int)
+(define-fun aqtunused () intref (intrefqtmk a))
+(declare-fun a1 () Int)
+(assert (not (and (<= 5 a1) (<= a1 15))))
+(check-sat)
+(get-model)

tests/issues/854/twice_eq.models.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun intrefqtmk ((arg_0 Int)) intref (as @!k1 intref))
+  (define-fun another_mk ((arg_0 Int)) intref (as @!k1 intref))
+  (define-fun a () Int 0)
+  (define-fun a1 () Int 0)
+)

tests/issues/854/twice_eq.models.smt2

@@ -0,0 +1,13 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-option :produce-models true)
+(declare-sort intref 0)
+(declare-fun intrefqtmk (Int) intref)
+(declare-fun another_mk (Int) intref)
+(declare-fun a () Int)
+(define-fun aqtunused () intref (intrefqtmk a))
+(assert (= aqtunused (another_mk a)))
+(declare-fun a1 () Int)
+(assert (not (and (<= 5 a1) (<= a1 15))))
+(check-sat)
+(get-model)