Do not leak non-abstract names in model

This patch changes the definition of `is_model_term` to align with the
definition of a _value term_ in the SMT-LIB standard (value terms are
particular ground terms defined in a logic for each sort (see Subsection
5.5.1) in [1].)

It is now the responsibility of `Uf.assign_next` and `X.assign_value` to
ensure they create value terms for all terms in the model, which
involves assigning them new names of `abstract` kind. In particular, we
no longer need to create abstract names in the `Uf` module.

In order to make sure those names show up as the canonical
representative when they exist, they are given a depth of `0`, i.e. less
than any other term (except the `true` and `false` constants).

Fixes #1213
Fixes #1270

[1]: The SMT-LIB Standard Version 2.7
     https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-07-07.pdf

Author: bclement-ocp

src/lib/reasoners/shostak.ml

@@ -544,12 +544,6 @@ struct
       | _, Ty.Tint
       | _, Ty.Treal     -> ARITH.assign_value r distincts eq
       | _, Ty.Tbitv _   -> BITV.assign_value r distincts eq
-      | Term t, Ty.Tfarray _ ->
-        begin
-          if List.exists (fun (t,_) -> Expr.is_model_term t) eq then None
-          else
-            Some (Expr.fresh_name (Expr.type_info t), false)
-        end
 
       | _, Ty.Tadt _    when not (Options.get_disable_adts()) ->
         ADT.assign_value r distincts eq
@@ -575,7 +569,7 @@ struct
       | Term t, ty      -> (* case disable_adts() handled here *)
         if Expr.is_model_term t ||
            List.exists (fun (t,_) -> Expr.is_model_term t) eq then None
-        else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *)
+        else Some (Expr.mk_abstract ty, false) (* false <-> not a case-split *)
       | _               ->
         (* There is no model-generation support for the AC symbols yet.
            The function [AC.assign_value] always returns [None]. *)

src/lib/reasoners/uf.ml

@@ -1093,18 +1093,19 @@ let reinit_cache () =
 (****************************************************************************)
 
 let model_repr_of_term t env mrepr =
-  try ME.find t mrepr, mrepr
-  with Not_found ->
-    let mk = try ME.find t env.make with Not_found -> assert false in
-    let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in
-    (* We call this function during the model generation only. At this time,
-       we are sure that class representatives are constant semantic values, or
-       uninterpreted names. *)
-    match X.to_model_term rep with
-    | Some v -> v, ME.add t v mrepr
-    | None ->
-      (* [X.to_model_term] cannot fail on constant semantic values. *)
-      assert false
+  if E.is_model_term t then t, mrepr else
+    try ME.find t mrepr, mrepr
+    with Not_found ->
+      let mk = try ME.find t env.make with Not_found -> assert false in
+      let rep, _ = try MapX.find mk env.repr with Not_found -> assert false in
+      (* We call this function during the model generation only. At this time,
+         we are sure that class representatives are constant semantic values, or
+         uninterpreted names. *)
+      match X.to_model_term rep with
+      | Some v -> v, ME.add t v mrepr
+      | None ->
+        (* [X.to_model_term] cannot fail on constant semantic values. *)
+        assert false
 
 (* A map of expressions to terms, ordered by depth first, and then by
    [Expr.compare] for expressions with same depth. This structure will
@@ -1152,25 +1153,11 @@ module Cache = struct
       E.Table.add arrays_cache t values
     | values ->
       E.Table.replace values i v
-
-  let get_abstract_for abstracts_cache env (t : E.t) =
-    let r, _ = find env t in
-    match Shostak.HX.find abstracts_cache r with
-    | exception Not_found ->
-      let abstract = E.mk_abstract (E.type_info t) in
-      Shostak.HX.add abstracts_cache r abstract;
-      abstract
-    | abstract -> abstract
 end
 
 type cache = {
   array_selects: Expr.t E.Table.t E.Table.t;
   (** Stores all the get accesses to array names. *)
-
-  abstracts: Expr.t Shostak.HX.t;
-  (** Stores all the abstract values generated. This cache is necessary
-      to ensure we do not generate twice an abstract value for a given
-      symbol. *)
 }
 
 let is_destructor = function
@@ -1189,9 +1176,8 @@ let is_destructor = function
      Alt-Ergo cannot produces a constant value for them. This function creates
      a new abstract value in this case. *)
 let compute_concrete_model_of_val cache =
-  let store_array_select = Cache.store_array_get cache.array_selects
-  and get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun env t ((mdl, mrepr) as acc) ->
+  let store_array_select = Cache.store_array_get cache.array_selects in
+  fun env t ((mdl, mrepr) as acc) ->
     let { E.f; xs; ty; _ } = E.term_view t in
     (* TODO: We have to filter out destructors here as we don't consider
        pending destructors as solvable theory symbols of the ADT theory.
@@ -1217,41 +1203,23 @@ let compute_concrete_model_of_val cache =
         in
         let ret_rep, mrepr = model_repr_of_term t env mrepr in
         match f, arg_vals, ty with
-        | Sy.Name _, [], Ty.Tfarray _ ->
-          begin
-            match E.Table.find cache.array_selects t with
-            | exception Not_found ->
-              (* We have to add an abstract array in case there is no
-                 constraint on its values. *)
-              E.Table.add cache.array_selects t (E.Table.create 17);
-              acc
-            | _ -> acc
-          end
-
         | Sy.Op Sy.Set, _, _ -> acc
 
         | Sy.Op Sy.Get, [a; i], _ ->
           begin
+            let a, mrepr = model_repr_of_term a env mrepr in
+            let i, mrepr = model_repr_of_term i env mrepr in
             let E.{ f = fa; _ } = E.term_view a in
             match fa with
             | Sy.Name _ ->
               store_array_select a i ret_rep;
-              acc
+              mdl, mrepr
             | _ ->
               acc
           end
 
         | Sy.Name { hs = id; _ }, _, _ ->
-          let value =
-            match ty with
-            | Ty.Text _ ->
-              (* We cannot produce a concrete value as the type is abstract.
-                 In this case, we produce an abstract value with the appropriate
-                 type. *)
-              get_abstract_for env t
-            | _ -> ret_rep
-          in
-          ModelMap.(add (id, arg_tys, ty) arg_vals value mdl), mrepr
+          ModelMap.(add (id, arg_tys, ty) arg_vals ret_rep mdl), mrepr
 
         | _ ->
           Printer.print_err
@@ -1262,8 +1230,7 @@ let compute_concrete_model_of_val cache =
 
 let extract_concrete_model cache =
   let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
-  let get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun ~prop_model ~declared_ids env ->
+  fun ~prop_model ~declared_ids env ->
     let terms, suspicious = terms env in
     let model, mrepr =
       MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
@@ -1273,12 +1240,12 @@ let extract_concrete_model cache =
       E.Table.fold (fun t vals mdl ->
           (* We produce a fresh identifiant for abstract value in order to
              prevent any capture. *)
-          let abstract = get_abstract_for env t in
+          assert (E.is_model_term t);
           let ty = Expr.type_info t in
           let arr_val =
             E.Table.fold (fun i v arr_val ->
                 Expr.ArraysEx.store arr_val i v
-              ) vals abstract
+              ) vals t
           in
           let id, is_user =
             let Expr.{ f; _ } = Expr.term_view t in
@@ -1309,8 +1276,5 @@ let extract_concrete_model cache =
     { Models.propositional = prop_model; model; term_values = mrepr }
 
 let extract_concrete_model ~prop_model ~declared_ids =
-  let cache : cache = {
-    array_selects = E.Table.create 17;
-    abstracts = Shostak.HX.create 17;
-  }
-  in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
+  let cache : cache = { array_selects = E.Table.create 17 } in
+  fun env -> extract_concrete_model cache ~prop_model ~declared_ids env

src/lib/structures/expr.ml

@@ -890,8 +890,15 @@ let mk_trigger ?user:(from_user = false) ?depth ?(hyp = []) content =
 let mk_term s l ty =
   assert (match s with Sy.Lit _ | Sy.Form _ -> false | _ -> true);
   let d = match l with
-    | [] ->
-      1 (*no args ? depth = 1 (ie. current app s, ie constant)*)
+    | [] -> (
+        (* no args ? depth = 1 (ie. current app s, ie constant)
+
+           abstract constants must be smaller than other terms
+           so that they end up in models. *)
+        match s with
+        | Name { ns = Abstract; _ } -> 0 (* 3rd smallest depth *)
+        | _ -> 1
+      )
     | _ ->
       (* if args, d is 1 + max_depth of args (equals at least to 1 *)
       1 + List.fold_left (fun z t -> max z t.depth) 1 l
@@ -1077,7 +1084,8 @@ let rec is_model_term e =
   | Op Div, [{ f = Real _; _ }; { f = Real _; _ }] -> true
   | Op Minus, [{ f = Real q; _ }; { f = Real _; _ }] -> Q.equal q Q.zero
   | Op Minus, [{ f = Int i; _ }; { f = Int _; _ }] -> Z.equal i Z.zero
-  | (True | False | Name _ | Int _ | Real _ | Bitv _), [] -> true
+  | Name { ns = Abstract; _ }, [] -> true
+  | (True | False | Int _ | Real _ | Bitv _), [] -> true
   | _ -> false
 
 let[@inline always] is_value_term e =

src/lib/structures/expr.mli

@@ -437,7 +437,10 @@ val is_model_term : t -> bool
     A model term can be:
     - A constructor application involving only model terms,
     - A literal of a basic type (integer, real, boolean, unit or bitvector),
-    - A name. *)
+    - An abstract name, representing an abstract value (following SMT-LIB
+      terminology).
+
+    The definition of model term maps to value terms in the SMT-LIB standard. *)
 
 val save_cache: unit -> unit
 (** Saves the modules cache *)

tests/cram.t/run.t

@@ -11,8 +11,8 @@ appropriate here.
   (
     (define-fun x () Int 0)
     (define-fun y () Int 0)
-    (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
-    (define-fun a2 () (Array Int Int) (as @a0 (Array Int Int)))
+    (define-fun a1 () (Array Int Int) (store (as @a0 (Array Int Int)) 0 0))
+    (define-fun a2 () (Array Int Int) (as @a1 (Array Int Int)))
   )
 
 Now we will test some semantic triggers.

tests/issues/1212.default.expected

@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun a () (Array Int Int) (as @a3 (Array Int Int)))
-  (define-fun b () (Array Int Int) (as @a2 (Array Int Int)))
+  (define-fun a () (Array Int Int) (as @a2 (Array Int Int)))
+  (define-fun b () (Array Int Int) (as @a0 (Array Int Int)))
 )

tests/issues/1213.default.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun a () (List T) nil)
+  (define-fun b () (List T) nil)
+  (define-fun c () (List T) (cons (as @a0 T) nil))
+  (define-fun d () (List T) nil)
+)

tests/issues/1213.default.smt2

@@ -0,0 +1,18 @@
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-datatypes ((List 1)) (
+  (par (T) (
+    (nil)
+    (cons (head T) (tail (List T)))
+  ))
+))
+(declare-sort T 0)
+(declare-const a (List T))
+(declare-const b (List T))
+(declare-const c (List T))
+(declare-const d (List T))
+(assert (= (tail a) b))
+(assert ((_ is cons) c))
+(assert (= (tail c) d))
+(check-sat)
+(get-model)

tests/issues/1270.default.expected

@@ -0,0 +1,8 @@
+
+unknown
+(
+  (define-fun q ((arg_0 t)) Int
+   (ite (= arg_0 (as @a1 t)) 1 (ite (= arg_0 (as @a0 t)) 0 (- 1))))
+  (define-fun o ((arg_0 Int)) t
+   (ite (= arg_0 0) (as @a0 t) (ite (= arg_0 1) (as @a1 t) (as @a2 t))))
+)

tests/issues/1270.default.smt2

@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-sort t 0)
+(declare-fun q (t) Int)
+(declare-fun o (Int) t)
+(assert (forall ((i Int)) (or (> 0 0) (= i (q (o i))))))
+(check-sat)
+(get-model)