Use Expr.t to store model values

Use `Expr.t` values instead of strings to store the value of the
first-order model.

Add a new function `to_term_const` in the signature of `Shostak`.
Basically this function is the inverse function of `X.make` on the
constant terms only. The function always returns a term `t` such that
`Expr.is_const_term t` is `true`.

Notice that we need this function during model generation. Indeed, even
if the class of a semantic value in UF contains terms whose the `make`
is constant according to `X.is_constant`, these terms aren't necessary
constant according to `Expr.is_const_term`. For instance, the term `0 +
1` will become the semantic value `1` and we expect that
`X.to_term_const` returns `Some 1`.

Modify the definition of `Expr.is_const_term` (formerly named
`const_term`). The previous definition considered that the application
of constructor of an ADT to constant terms isn't a constant term. The
same went for record definitions. Now, there are constant too.
We have to check that this modification is correct for the

Notice that we keep the old definion `const_term` in the module `Expr`
but we don't expose it anymore. Indeed, this function is used to detect
constants in the smart constructor of the let bindings because the
definition of the depth of formulae have been tweaked to prevent
regressions. Modifying this function could be dangereous.

src/lib/frontend/models.ml

@@ -35,7 +35,7 @@ module E = Expr
 type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
-  terms_values : (Shostak.Combine.r * string) Expr.Map.t
+  terms_values : Expr.t Expr.Map.t
 }
 
 let empty = {

src/lib/frontend/models.mli

@@ -33,7 +33,7 @@
 type t = {
   propositional : Expr.Set.t;
   model : ModelMap.t;
-  terms_values : (Shostak.Combine.r * string) Expr.Map.t
+  terms_values : Expr.t Expr.Map.t
   (** A map from terms to their values in the model (as a
       representative of type X.r and as a string. *)
 }

src/lib/reasoners/ac.ml

@@ -325,7 +325,7 @@ module Make (X : Sig.X) = struct
     let module SX = Set.Make(struct type t=r let compare = X.hash_cmp end) in
     let exception Found of Expr.t in
     fun r distincts eq ->
-      if List.exists (fun (t,(_:r)) -> Expr.const_term t) eq then
+      if List.exists (fun (t,(_:r)) -> Expr.is_const_term t) eq then
         None
       else
         (*match X.ac_extract r with

src/lib/reasoners/adt.ml

@@ -441,9 +441,8 @@ module Shostak (X : ALIEN) = struct
       "[ADTs.models] assign_value currently not implemented";
     raise (Util.Not_implemented "Models for ADTs")
 
-  let choose_adequate_model _ _ _ =
+  let to_const_term _r =
     Printer.print_err
-      "[ADTs.models] choose_adequate_model currently not implemented";
+      "[ADTs.models] to_const_term currently not implemented";
     raise (Util.Not_implemented "Models for ADTs")
-
 end

src/lib/reasoners/arith.ml

@@ -809,49 +809,11 @@ module Shostak
         cpt := Q.add Q.one (max_constant distincts !cpt);
         Some (term_of_cst (Q.to_string !cpt), true)
 
-  let pp_constant ppf r =
+  let to_const_term r =
     match P.is_const (embed r), X.type_info r with
-    | Some q, Ty.Tint ->
-      assert (Z.equal (Q.den q) Z.one);
-      let i = Q.num q in
-      if Z.sign i = -1 then
-        Fmt.pf ppf "(- %a)" Z.pp_print (Z.abs i)
-      else
-        Fmt.pf ppf "%a" Z.pp_print i
-    | Some q, Ty.Treal ->
-      if Z.equal (Q.den q) Z.one then
-        Fmt.pf ppf "%a.0" Z.pp_print (Q.num q)
-      else if Q.sign q = -1 then
-        Fmt.pf ppf "(/ (- %a) %a)"
-          Z.pp_print (Z.abs (Q.num q))
-          Z.pp_print (Q.den q)
-      else
-        Fmt.pf ppf "(/ %a %a)" Z.pp_print (Q.num q) Z.pp_print (Q.den q)
-    | _ -> assert false
-
-  let choose_adequate_model t r l =
-    if Options.get_debug_interpretation () then
-      Printer.print_dbg
-        ~module_name:"Arith" ~function_name:"choose_adequate_model"
-        "choose_adequate_model for %a" E.print t;
-    let l = List.filter (fun (_, r) -> P.is_const (embed r) != None) l in
-    let r =
-      match l with
-      | [] ->
-        (* We do this, because terms of some semantic values created
-           by CS are not created and added to UF *)
-        if (P.is_const (embed r) == None) then begin
-          Printer.print_dbg
-            ~module_name:"Arith" ~function_name:"choose_adequate_model"
-            "no adequate model found for %a" X.print r;
-          assert false
-        end;
-        r
-
-      | (_,r)::l ->
-        List.iter (fun (_,x) -> assert (X.equal x r)) l;
-        r
-    in
-    r, Fmt.str "%a" pp_constant r
-
+    | Some i, Ty.Tint ->
+      assert (Z.equal (Q.den i) Z.one);
+      Some (Expr.Ints.of_Z (Q.num i))
+    | Some q, Ty.Treal -> Some (Expr.Reals.of_Q q)
+    | _ -> None
 end

src/lib/reasoners/arrays.ml

@@ -60,28 +60,12 @@ module Shostak (X : ALIEN) = struct
   let abstract_selectors _ _ = assert false
   let solve _ _ = assert false
   let assign_value r _ eq =
-    if List.exists (fun (t,_) -> Expr.const_term t) eq then None
+    if List.exists (fun (t,_) -> Expr.is_const_term t) eq then None
     else
       match X.term_extract r with
       | Some _, true ->
         Some (Expr.fresh_name (X.type_info r), false)
       | _ -> assert false
 
-  let choose_adequate_model _ _ l =
-    let acc =
-      List.fold_left
-        (fun acc (s, r) ->
-           if not (Expr.const_term s) then acc
-           else
-             match acc with
-             | Some(s', _) when Expr.compare s' s > 0 -> acc
-             | _ -> Some (s, r)
-        ) None l
-    in
-    match acc with
-    | Some (_, r) ->
-      r, Format.asprintf "%a" X.print r (* it's a EUF constant *)
-
-    | _ -> assert false
-
+  let to_const_term _r = assert false
 end

src/lib/reasoners/bitv.ml

@@ -1536,34 +1536,14 @@ module Shostak(X : ALIEN) = struct
         let bv = String.make sz '0' in
         Some (E.bitv bv (Ty.Tbitv sz), true)
 
-  let choose_adequate_model t r l =
-    if Options.get_debug_interpretation () then
-      Printer.print_dbg
-        ~module_name:"Bitv" ~function_name:"choose_adequate_model"
-        "choose_adequate_model for %a" E.print t;
-    let l = List.map (fun (t, r) -> (t, r, embed r)) l in
-    let l = List.filter (fun (_, _, a) -> is_cte_abstract a) l in
-    let r, a =
-      match l with
-      | [] ->
-        let a = embed r in
-        assert (is_cte_abstract a);
-        r, a
-      | (_, r, a) :: l ->
-        List.iter (fun (_, x, _) -> assert (X.equal x r)) l;
-        r, a
-    in
-    let s =
-      List.map (function
-          | { bv = Cte b; sz } ->
-            Z.format ("%0" ^ string_of_int sz ^ "b") b
-          | _ ->
-            (* Cannot happen because [a] must satisfy [is_cte_abstract] at this
-               point. *)
-            assert false
-        ) a
-      |> String.concat ""
-    in
-    r, "#b" ^ s
-
+  let to_const_term r =
+    match embed r with
+    | [{ bv = Cte b; sz }] ->
+      let s = Z.format ("%0" ^ string_of_int sz ^ "b") b in
+      Some (Expr.bitv s Ty.(Tbitv sz))
+    | _ :: _ ->
+      Fmt.pr "HERE@.";
+      None
+    | _ ->
+      None
 end

src/lib/reasoners/enum.ml

@@ -195,21 +195,9 @@ module Shostak (X : ALIEN) = struct
        Thus we don't need to guess new values here. *)
     None
 
-  let choose_adequate_model _ r l =
-    let l =
-      List.filter
-        (fun (_, r) -> match embed r with Cons _ -> true | _ -> false) l
-    in
-    let r = match l with
-      | (_,r)::l ->
-        List.iter (fun (_,x) -> assert (X.equal x r)) l;
-        r
-
-      | [] ->
-        (* We do this, because terms of some semantic values created
-           by CS are not created and added to UF *)
-        match embed r with Cons _ -> r | _ -> assert false
-    in
-    r, Format.asprintf "%a" X.print r  (* it's a EUF constant *)
-
+  let to_const_term r =
+    match embed r with
+    | Cons (hs, ty) ->
+      Some (E.mk_term Sy.(Op (Constr hs)) [] ty)
+    | Alien a -> X.to_const_term a
 end

src/lib/reasoners/ite.ml

@@ -60,5 +60,5 @@ module Shostak (X : ALIEN) = struct
   let abstract_selectors _ _ = assert false
   let solve _ _ = assert false
   let assign_value _ _ _ = assert false
-  let choose_adequate_model _ _ _ = assert false
+  let to_const_term _r = assert false
 end

src/lib/reasoners/records.ml

@@ -30,6 +30,7 @@
 
 module Hs = Hstring
 module E = Expr
+module Sy = Symbols
 
 type 'a abstract =
   | Record of (Hs.t * 'a abstract) list * Ty.t
@@ -414,7 +415,7 @@ module Shostak (X : ALIEN) = struct
     | Access _ -> None
 
     | Record (_, ty) ->
-      if List.exists (fun (t,_) -> Expr.const_term t) eq
+      if List.exists (fun (t,_) -> Expr.is_const_term t) eq
       then None
       else Some (Expr.fresh_name ty, false)
 
@@ -426,20 +427,19 @@ module Shostak (X : ALIEN) = struct
         Some (s, false) (* false <-> not a case-split *)
       | _ -> assert false
 
-  let choose_adequate_model _ _ l =
-    let acc =
-      List.fold_left
-        (fun acc (s, r) ->
-           if not (Expr.const_term s) then acc
-           else
-             match acc with
-             | Some(s', _) when Expr.compare s' s > 0 -> acc
-             | _ -> Some (s, r)
-        ) None l
-    in
-    match acc with
-    | Some (_,r) ->
-      r, Format.asprintf "%a" X.print r  (* it's a EUF constant *)
-    | _ -> assert false
+  let to_const_term =
+    let rec to_const_term r =
+      match r with
+      | Record (fields, ty) ->
+        (* We can ignore the names of fields as they are inlined in the
+           type [ty] of the record. *)
+        let l =
+          Lists.try_map (fun (_name, rf) -> to_const_term rf) fields
+        in
+        Option.bind l @@ fun l ->
+        Some (E.mk_term Sy.(Op Record) l ty)
 
+      | Other (a, _) -> X.to_const_term a
+      | Access _ -> None
+    in fun r -> to_const_term (embed r)
 end

src/lib/reasoners/shostak.ml

@@ -270,6 +270,23 @@ struct
     | Ac _ -> None, false (* SYLVAIN : TODO *)
     | Term t -> Some t, true
 
+  let to_const_term r =
+    let res =
+      match r.v with
+      | Arith _ -> ARITH.to_const_term r
+      | Records _ -> RECORDS.to_const_term r
+      | Bitv _ -> BITV.to_const_term r
+      | Arrays _ -> ARRAYS.to_const_term r
+      | Enum _ -> ENUM.to_const_term r
+      | Adt _ -> ADT.to_const_term r
+      | Ite _ -> ITE.to_const_term r
+      | Term t when Expr.is_const_term t -> Some t
+      | Ac _ | Term _ -> None
+    in
+    Option.bind res @@ fun t ->
+    assert (Expr.is_const_term t);
+    Some t
+
   let top () = term_embed Expr.vrai
   let bot () = term_embed Expr.faux
 
@@ -369,7 +386,14 @@ struct
     | Enum t -> ENUM.is_constant t
     | Adt t -> ADT.is_constant t
     | Ite t -> ITE.is_constant t
-    | Ac _ | Term _ -> false
+    | Term t ->
+      begin
+        let Expr.{ f; xs; _ } = Expr.term_view t in
+        match f, xs with
+        | Symbols.(True | False | Void), [] -> true
+        | _ -> false
+      end
+    | Ac _ -> false
 
   let subst p v r =
     if equal p v then r
@@ -646,8 +670,8 @@ struct
           end
 
       | Term t, ty      -> (* case disable_adts() handled here *)
-        if Expr.const_term t ||
-           List.exists (fun (t,_) -> Expr.const_term t) eq then None
+        if Expr.is_const_term t ||
+           List.exists (fun (t,_) -> Expr.is_const_term t) eq then None
         else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *)
       | _               ->
         (* There is no model-generation support for the AC symbols yet.
@@ -663,66 +687,6 @@ struct
          | None -> Format.asprintf "None"
          | Some(res, _is_cs) -> Format.asprintf "%a" Expr.print res);
     opt
-
-  let choose_adequate_model t rep l =
-    let r, pprint =
-      match Expr.type_info t with
-      | Ty.Tint
-      | Ty.Treal     -> ARITH.choose_adequate_model t rep l
-      | Ty.Tbitv _   -> BITV.choose_adequate_model t rep l
-      | Ty.Tsum _    -> ENUM.choose_adequate_model t rep l
-      | Ty.Tadt _    when not (Options.get_disable_adts()) ->
-        ADT.choose_adequate_model t rep l
-      | Ty.Trecord _ -> RECORDS.choose_adequate_model t rep l
-      | Ty.Tfarray _ -> ARRAYS.choose_adequate_model t rep l
-      | Ty.Tbool ->
-        (* case split is now supposed to be done for internal bools if
-           needed as well *)
-        assert (is_bool_const rep);
-        rep, Format.asprintf "%a" print rep
-      | _            ->
-        let acc =
-          List.fold_left
-            (fun acc (s, r) ->
-               if Expr.const_term s then
-                 match acc with
-                 | Some(s', _) when Expr.compare s' s > 0 -> acc
-                 | _ -> Some (s, r)
-               else
-                 acc
-            ) None l
-        in
-        let r =
-          match acc with
-          | Some (_,r) -> r
-          | None ->
-            match term_extract rep with
-            | Some t, true when Expr.const_term t -> rep
-            | _ ->
-              let print_aux fmt (t,r) =
-                Format.fprintf fmt "> impossible case: %a -- %a@ "
-                  Expr.print t
-                  print r
-              in
-              if Options.get_debug_interpretation () then
-                Printer.print_dbg
-                  ~module_name:"Shostak" ~function_name:"choose_adequate_model"
-                  "@[<v 2>What to choose for term %a with rep %a?\
-                   %a@]"
-                  Expr.print t
-                  print rep
-                  (Printer.pp_list_no_space print_aux) l;
-              assert false
-        in
-        r, Format.asprintf "%a" print r (* it's a EUF constant *)
-    in
-    if Options.get_debug_interpretation () then
-      Printer.print_dbg
-        ~module_name:"Shostak" ~function_name:"choose_adequate_model"
-        "%a selected as a model for %a"
-        print r Expr.print t;
-    r, pprint
-
 end
 
 and TARITH : Polynome.T

src/lib/reasoners/sig.mli

@@ -128,11 +128,7 @@ 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! *)
 
-  (* choose the value to print and how to print it for the given term.
-     The second term is its representative. The list is its equivalence class
-  *)
-  val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string
-
+  val to_const_term : r -> Expr.t option
 end
 
 module type X = sig
@@ -191,8 +187,5 @@ module type X = sig
   val assign_value :
     r -> r list -> (Expr.t * r) list -> (Expr.t * bool) option
 
-  (* choose the value to print and how to print it for the given term.
-     The second term is its representative. The list is its equivalence class
-  *)
-  val choose_adequate_model : Expr.t -> r -> (Expr.t * r) list -> r * string
+  val to_const_term : r -> Expr.t option
 end