fix(AC, Arith): Use a separate namespace for AC abstractions

We are using the same name space for all the constants introduced by any
abstraction procedure. However, we also have code in the arithmetic
module that cares specifically about abstractions introduced by AC(X) in
order to determine whether distributivity should be applied or not.

This patch uses different namespaces for symbols introduced for AC(X)
purposes and symbols introduced by other abstraction procedures (such as
Shostak's record abstraction). After reviewing the different places
where we use `Expr.fresh_name`, I believe only the two locations changed
to `Expr.fresh_ac_name` in this commit are related to AC(X), and other
uses of `Expr.fresh_name` are for separate, independent abstraction
procedures.

Fixes OCamlPro#1172

Author: bclement-ocp

src/lib/reasoners/ac.ml

@@ -214,7 +214,7 @@ module Make (X : Sig.X) = struct
         let eq = Expr.mk_eq ~iff:false aro_t t in
         X.term_embed aro_t, eq::acc
       | _, { ty; _ } ->
-        let k = Expr.fresh_name ty in
+        let k = Expr.fresh_ac_name ty in
         let eq = Expr.mk_eq ~iff:false k t in
         X.term_embed k, eq::acc
 

src/lib/reasoners/arith.ml

@@ -455,7 +455,7 @@ module Shostak
     List.exists
       (fun x ->
          match X.term_extract x with
-         | Some t, _ -> E.is_internal_name t
+         | Some t, _ -> E.is_fresh_ac_name t
          | _ -> false
       ) (X.leaves xp)
 
@@ -540,7 +540,7 @@ module Shostak
     List.fold_left
       (fun (l, sb) (b, y) ->
          if X.ac_extract y != None && X.str_cmp y x > 0 then
-           let k = X.term_embed (E.fresh_name Ty.Tint) in
+           let k = X.term_embed (E.fresh_ac_name Ty.Tint) in
            (b, k) :: l, (y, embed k)::sb
          else (b, y) :: l, sb)
       ([], []) l

src/lib/reasoners/uf.ml

@@ -1188,8 +1188,7 @@ let compute_concrete_model_of_val cache =
        We should check if these symbols can be defined as solvable to
        remove this particular case here. *)
     if X.is_solvable_theory_symbol f || is_destructor f
-       || Sy.is_internal f || E.is_internal_name t || E.is_internal_skolem t
-       || E.equal t E.vrai || E.equal t E.faux
+       || Sy.is_internal f || E.equal t E.vrai || E.equal t E.faux
     then
       (* These terms are built-in interpreted ones and we don't have
          to produce a definition for them. *)

src/lib/structures/expr.ml

@@ -987,13 +987,14 @@ let fresh_name ty =
 let mk_abstract ty =
   mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty
 
-let is_internal_name t =
+let fresh_ac_name ty =
+  mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty
+
+let is_fresh_ac_name t =
   match t with
-  | { f = Name { ns = Fresh; _ }; xs = []; _ } -> true
+  | { f = Name { ns = Fresh_ac; _ }; xs = []; _ } -> true
   | _ -> false
 
-let is_internal_skolem t = Sy.is_fresh_skolem t.f
-
 let positive_int i = mk_term (Sy.int i) [] Ty.Tint
 
 let int i =

src/lib/structures/expr.mli

@@ -228,8 +228,6 @@ val size : t -> int
 val depth : t -> int
 val is_positive : t -> bool
 val neg : t -> t
-val is_internal_name : t -> bool
-val is_internal_skolem : t -> bool
 val is_int : t -> bool
 val is_real : t -> bool
 val type_info : t -> Ty.t
@@ -256,6 +254,11 @@ val real : string -> t
 val bitv : string -> Ty.t -> t
 val fresh_name : Ty.t -> t
 
+(* Special names used for AC(X) abstraction.
+   These corresponds to the K sort in the AC(X) paper. *)
+val fresh_ac_name : Ty.t -> t
+val is_fresh_ac_name : t -> bool
+
 val mk_abstract : Ty.t -> t
 (** [mk_abstract ty] creates an abstract model term of type [ty].
     This function is intended to be used only in models. *)

src/lib/structures/symbols.ml

@@ -75,7 +75,7 @@ type form =
 
 type name_kind = Ac | Other
 
-type name_space = User | Internal | Fresh | Skolem | Abstract
+type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract
 
 let compare_name_space ns1 ns2 =
   match ns1, ns2 with
@@ -91,6 +91,10 @@ let compare_name_space ns1 ns2 =
   | Fresh, _ -> -1
   | _, Fresh -> 1
 
+  | Fresh_ac, Fresh_ac -> 0
+  | Fresh_ac, _ -> -1
+  | _, Fresh_ac -> 1
+
   | Skolem, Skolem -> 0
   | Skolem, _ -> -1
   | _, Skolem -> 1
@@ -128,6 +132,7 @@ let mangle ns s =
   | User -> s
   | Internal -> ".!" ^ s
   | Fresh -> ".k" ^ s
+  | Fresh_ac -> ".K" ^ s
   | Skolem -> ".?__" ^ s
   | Abstract -> "@a" ^ s
 
@@ -514,10 +519,6 @@ let fresh_skolem_string base = Id.Namespace.Skolem.fresh ~base ()
 let fresh_skolem_name base = name ~ns:Skolem (fresh_skolem_string base)
 let fresh_skolem_var base = Var.of_string (fresh_skolem_string base)
 
-let is_fresh_skolem = function
-  | Name { ns = Skolem; _ } -> true
-  | _ -> false
-
 let is_get f = equal f (Op Get)
 let is_set f = equal f (Op Set)
 

src/lib/structures/symbols.mli

@@ -102,15 +102,30 @@ type name_space =
   (** This symbol is a "fresh" internal name. Fresh internal names play a
       similar role as internal names, but they always represent a constant
       that was introduced during solving as part of some kind of purification
-      or abstraction procedure. This is notably used by some parts of AC(X)
-      that check if terms contains fresh symbols (see [contains_a_fresh_alien]
-      in the [Arith] module for an example).
+      or abstraction procedure.
+
+      In order to correctly implement AC(X) in the presence of distributive
+      symbols, symbols generated for AC(X) abstraction use a special
+      namespace, [Fresh_ac] below.
 
       To ensure uniqueness, fresh names must always be generated using
       [Id.Namespace.Internal.fresh ()].
 
       In particular, fresh names are only used to denote constants, not
       arbitrary functions. *)
+  | Fresh_ac
+  (** This symbol has been introduced as part of the AC(X) abstraction process.
+      This is notably used by some parts of AC(X) that check if terms contains
+      fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an
+      example).
+
+      These correspond to the K sort in the AC(X) paper. They use a different
+      name space from other fresh symbols because we need to be able to know
+      whether a fresh symbol comes from the AC(X) abstraction procedure in order
+      to prevent loops.
+
+      To ensure uniqueness, AC abstraction names must always be generated using
+      [Id.Namespace.Internal.fresh ()]. *)
   | Skolem
   (** This symbol has been introduced as part of skolemization, and represents
       the (dependent) variable of an existential quantifier. Skolem names can
@@ -202,7 +217,6 @@ val pp_smtlib_operator : operator Fmt.t
 
 val fresh_skolem_var : string -> Var.t
 val fresh_skolem_name : string -> t
-val is_fresh_skolem : t -> bool
 
 (** Resets to 0 the fresh symbol counter *)