From 607b93a796a0d3fd8aa9cba09480eafdbccc5f88 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Tue, 23 Jan 2024 12:14:08 +0100
Subject: [PATCH] fix(Shostak): names must return `false` for `X.is_constant`
 (#1031)

The `X.is_constant` function is intended to determine whether a semantic
value is a constant value (it is documented to be equivalent to having
an empty `X.leaves`). This invariant is relied upon by the code for
delayed computation in `Rel_utils` that it was introduced for in #869.
While the change only makes the delayed computation code less efficient,
it makes the `X.is_constant` function worthless for its original purpose
in planned patches.

The invariant was broken in #925 which causes `X.is_constant` to now
consider some terms (specifically, names, i.e. uninterpreted constants)
as constants, which is incorrect for the intended and documented purpose
of `X.is_constant` (uninterpreted constants have different values in
different context, they are thus not constant values).

This patch restores the original semantic of `X.is_constant` with
improved documentation, and removes the assertion introduced in #925
which seems to be the only incorrect use.
---
 src/lib/reasoners/shostak.ml |  9 ++-------
 src/lib/reasoners/sig.mli    | 11 +++++++++--
 src/lib/reasoners/uf.ml      |  4 ++--
 3 files changed, 13 insertions(+), 11 deletions(-)

diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index e0724c2b8..d5e16d59d 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -389,14 +389,9 @@ struct
     | Term t ->
       begin
         let Expr.{ f; xs; _ } = Expr.term_view t in
-        (* We don't use [Expr.is_model_term] here to ensure that [t] is a
-           constant term because most of model terms are represented by
-           semantic values of builtin theories. Constant terms not managed by
-           builtin theories have to be considered as constant semantic
-           values. In particular, this code enforces the invariant:
-             [e] is a model term ==> [X.make e] is a constant semantic value. *)
+        (* Constant terms that have no theories. *)
         match f, xs with
-        | Symbols.(True | False | Void | Name _), [] -> true
+        | Symbols.(True | False | Void), [] -> true
         | _ -> false
       end
     | Ac _ -> false
diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli
index 08d626d7c..21e325308 100644
--- a/src/lib/reasoners/sig.mli
+++ b/src/lib/reasoners/sig.mli
@@ -62,8 +62,15 @@ module type SHOSTAK = sig
   (** Give the leaves of a term of the theory *)
   val leaves : t -> r list
 
-  (** Determines whether the term is a constant. [is_constant t] is equivalent
-      to [leaves t == []], but is more efficient.
+  (** Determines whether the semantic value is a constant value. [is_constant t]
+      is equivalent to [leaves t == []] (except for the special cases below),
+      but is more efficient.
+
+      In addition, some terms (e.g. [true], [false], [void]) that have no
+      associated theories are considered as constant by this function.
+
+      Semantic value for which [is_constant] returns [true] contains no free
+      names and thus have the same concrete value in all contexts.
 
       Note that for some theories (e.g. records, arrays) the constant may not be
       pure: it may involve nested (constant) terms of other theories. *)
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index d590db0e9..341fae771 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1014,8 +1014,8 @@ let model_repr_of_term t env mrepr =
     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. *)
-    assert (X.is_constant rep);
+       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 ->