Abstract internal/fresh values in X.to_model_term

We do not replace all the fresh names by abstract values during the
model generation. This commit adds an argument `abstract` to [X.to_model_term].
`abstract` is a function of type `E.t -> E.t` that generates abstract
values and `X.to_model_term` calls it on appropriate leaves. `abstract`
contains a cache in its closure to prevent from duplicating abstract
values for the same name.

src/lib/reasoners/adt.ml

@@ -418,15 +418,15 @@ module Shostak (X : ALIEN) = struct
        in [Adt_rel]. *)
     None
 
-  let to_model_term r =
+  let to_model_term abstract r =
     match embed r with
     | Constr { c_name; c_ty; c_args } ->
       let args =
-        My_list.try_map (fun (_, arg) -> X.to_model_term arg) c_args
+        My_list.try_map (fun (_, arg) -> X.to_model_term abstract arg) c_args
       in
       Option.bind args @@ fun args ->
       Some (E.mk_constr c_name args c_ty)
 
     | Select _ -> None
-    | Alien a -> X.to_model_term a
+    | Alien a -> X.to_model_term abstract a
 end

src/lib/reasoners/arith.ml

@@ -744,7 +744,7 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-  let to_model_term r =
+  let to_model_term _abstract r =
     match P.is_const (embed r), X.type_info r with
     | Some i, Ty.Tint ->
       assert (Z.equal (Q.den i) Z.one);

src/lib/reasoners/bitv.ml

@@ -1584,7 +1584,7 @@ module Shostak(X : ALIEN) = struct
         let bv = String.make sz '0' in
         Some (E.bitv bv (Ty.Tbitv sz), true)
 
-  let to_model_term r =
+  let to_model_term _abstract r =
     match embed r with
     | [{ bv = Cte b; sz }] ->
       let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in

src/lib/reasoners/records.ml

@@ -401,7 +401,7 @@ module Shostak (X : ALIEN) = struct
         Some (s, false) (* false <-> not a case-split *)
       | _ -> assert false
 
-  let to_model_term =
+  let to_model_term abstract =
     let rec to_model_term r =
       match r with
       | Record (fields, ty) ->
@@ -414,7 +414,7 @@ module Shostak (X : ALIEN) = struct
         Some (E.mk_term Sy.(Op Record) l ty)
 
       | Other (a, _) ->
-        X.to_model_term a
+        X.to_model_term abstract a
       | Access _ -> None
     in fun r -> to_model_term (embed r)
 end

src/lib/reasoners/shostak.ml

@@ -232,14 +232,20 @@ struct
     | Ac _ -> None, false (* SYLVAIN : TODO *)
     | Term t -> Some t, true
 
-  let to_model_term r =
+  let to_model_term abstract r =
     let res =
       match r.v with
-      | Arith _ -> ARITH.to_model_term r
-      | Records _ -> RECORDS.to_model_term r
-      | Bitv _ -> BITV.to_model_term r
-      | Adt _ -> ADT.to_model_term r
-      | Term t when Expr.is_model_term t -> Some t
+      | Arith _ -> ARITH.to_model_term abstract r
+      | Records _ -> RECORDS.to_model_term abstract r
+      | Bitv _ -> BITV.to_model_term abstract r
+      | Adt _ -> ADT.to_model_term abstract r
+      | Term t when Expr.is_model_term t ->
+        let Expr.{ f; _ } = Expr.term_view t in
+        (match f with
+         | Symbols.Name { ns = Internal | Fresh | Fresh_ac; _ } ->
+           Some (abstract t)
+         | _ ->
+           Some t)
       | Ac _ | Term _ -> None
     in
     Option.bind res @@ fun t ->

src/lib/reasoners/sig.mli

@@ -137,24 +137,24 @@ module type SHOSTAK = sig
      [Some (t, false)], then there must be no context in which
      [solve r (fst X.make t)] raises [Unsolvable]. You have been warned! *)
 
-  val to_model_term : r -> Expr.t option
-  (** [to_model_term r] creates a model term if [r] is constant.
-      The function cannot fail if [r] is a constant (that is statisfied the
-      predicate [X.is_constant]).
-
-      The returned value always satisfies the predicate
-      [Expr.is_model_term]. See its documentation for more details about
-      model terms. *)
+  val to_model_term : (Expr.t -> Expr.t) -> r -> Expr.t option
+  (** [to_model_term abstract r] creates a model term if [r] is constant.
+      The function must succeed when [r] is a constant, this is [r] satisfied
+      the predicate [X.is_constant].
+
+      The [abstract] function is used to replace internal or fresh names by
+      abstract values.
+
+      The returned value always satisfies the predicate [Expr.is_model_term].
+      Refer to its documentation for more details about model terms. *)
 end
 
 module type X = sig
   type r
 
   val save_cache : unit -> unit
-  (** saves the module's current cache *)
 
   val reinit_cache : unit -> unit
-  (** restores the module's cache *)
 
   val make : Expr.t -> r * Expr.t list
 
@@ -178,7 +178,7 @@ module type X = sig
 
   val term_embed : Expr.t -> r
 
-  val term_extract : r -> Expr.t option * bool (* original term ? *)
+  val term_extract : r -> Expr.t option * bool
 
   val ac_embed : r ac -> r
 
@@ -196,19 +196,8 @@ module type X = sig
 
   val is_solvable_theory_symbol : Symbols.t -> bool
 
-  (* the returned bool is true when the returned term in a constant of the
-     theory. Otherwise, the term contains aliens that should be assigned
-     (eg. records). In this case, it's a unit fact, not a decision
-  *)
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
 
-  val to_model_term : r -> Expr.t option
-  (** [to_model_term r] creates a model term if [r] is constant.
-      The function cannot fail if [r] is a constant (that is statisfied the
-      predicate [X.is_constant]).
-
-      The returned value always satisfies the predicate
-      [Expr.is_model_term]. See its documentation for more details about
-      model terms. *)
+  val to_model_term : (Expr.t -> Expr.t) -> r -> Expr.t option
 end