Use an ADT to discriminate free graph and constant graph

src/lib/structures/modelMap.ml

@@ -31,7 +31,14 @@
 module X = Shostak.Combine
 module Sy = Symbols
 
-module Graph = struct
+(* The type of this module represents a model value for a function [f] by a
+   finite set of constraints of the form:
+     f(e_1, ..., e_n) = e
+   where [e_i] and [e] are model terms according to [Expr.is_model_term].
+
+   As functions in the SMT-LIB standard are total, one of the expressions [e]
+   above is used as the default value of the function. *)
+module Constraints = struct
   module M = Map.Make
       (struct
         type t = Expr.t list [@@deriving ord]
@@ -42,14 +49,12 @@ module Graph = struct
   let empty = M.empty
   let add = M.add
   let map = M.map
-  let cardinal = M.cardinal
-  let choose = M.choose
 
   (* A fiber of the function [f] over a value [v] is the set of all the values
      in the domain of [f] whose the image by [f] is [v].
 
      The function [inverse] of this module constructs a map of all the
-     non-empty fibers of the function represented by its graph. *)
+     non-empty fibers of the function represented by a set of constraints. *)
   module Fiber = struct
     include Set.Make (struct
         type t = Expr.t list [@@deriving ord]
@@ -58,8 +63,8 @@ module Graph = struct
     let pp_arg ppf (ctr, arg) =
       Fmt.pf ppf "(= arg_%i %a)" ctr Expr.pp_smtlib arg
 
-    (* For an argument (x_1, ..., x_n) of the function represented by the graph,
-       prints the SMT-LIB formula:
+    (* For an argument (x_1, ..., x_n) of the function, prints the SMT-LIB
+       formula:
         (and (= arg_0 x_1)(= arg_1 x2) ... (= arg_n x_n)).
     *)
     let pp_args ppf = function
@@ -69,8 +74,7 @@ module Graph = struct
       | args ->
         Fmt.pf ppf "(and %a)" Fmt.(iter_bindings ~sep:sp List.iteri pp_arg) args
 
-    (* For a fiber [x; y; z; ...] of the function represented by the graph,
-       prints the SMT-LIB formula:
+    (* For a fiber [x; y; z; ...] of the function, prints the SMT-LIB formula:
         (or
           (and (= arg_0 x_0) (= arg_1 x_1) ...)
           (and (= arg_0 y_0) (= arg_1 y_1) ...)
@@ -86,17 +90,18 @@ module Graph = struct
         Fmt.pf ppf "(or %a)" (Fmt.iter ~sep:Fmt.sp iter pp_args) fiber
   end
 
-  (* Compute all the fibers of the function represented by the graph. *)
-  let inverse graph =
+  (* Compute all the fibers of the function represented by the set of
+     constraints [c]. *)
+  let inverse c =
     M.fold (fun arg_vals ret_val acc ->
         match Expr.Map.find_opt ret_val acc with
         | Some fib ->
           Expr.Map.add ret_val (Fiber.add arg_vals fib) acc
         | None ->
           Expr.Map.add ret_val (Fiber.of_list [arg_vals]) acc
-      ) graph Expr.Map.empty
+      ) c Expr.Map.empty
 
-  let pp_inverse ppf rel =
+  let pp_inverse ppf c =
     let rec aux ppf seq =
       match seq () with
       | Seq.Nil -> ()
@@ -108,7 +113,7 @@ module Graph = struct
           Expr.pp_smtlib ret_val
           aux seq
     in
-    aux ppf (Expr.Map.to_seq rel)
+    aux ppf (Expr.Map.to_seq c)
 end
 
 module P = Map.Make
@@ -118,44 +123,37 @@ module P = Map.Make
       let compare = Id.compare_typed
     end)
 
+type graph =
+  | Free of Expr.t
+  (* Represents a graph without any constraint. The expression is
+     an abstract value. *)
+
+  | C of Constraints.t
+
 type t = {
-  values : Graph.t P.t;
+  values : graph P.t;
   suspicious : bool;
 }
 
 let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } =
   if List.compare_lengths arg_tys arg_vals <> 0 then
     Fmt.invalid_arg "The arity of the symbol %a doesn't agree the number of \
                      arguments" Id.pp id;
-  let graph =
-    try
-      let graph = P.find sy values in
-      (* If the graph associated with [sy] contains only an abstract value,
-         it means there is no constraint on this graph. We replace it by
-         the graph with the only constraint given by [arg_vals] and
-         [ret_val]. *)
-      if Graph.cardinal graph = 1 then
-        let _, value = Graph.choose graph in
-        let Expr.{ f; _ } = Expr.term_view value in
-        match f with
-        | Sy.Name { hs; _ }
-          when Id.Namespace.Abstract.is_id (Hstring.view hs) ->
-          Graph.empty
-        | _ -> graph
-      else
-        graph
-    with Not_found -> Graph.empty in
-  let values = P.add sy (Graph.add arg_vals ret_val graph) values in
+  let constraints =
+    match P.find sy values with
+    | C g -> g
+    | Free _ | exception Not_found -> Constraints.empty
+  in
+  let values =
+    P.add sy (C (Constraints.add arg_vals ret_val constraints)) values
+  in
   { values; suspicious }
 
 let empty ~suspicious declared_ids =
   let values =
     List.fold_left
-      (fun values ((_, arg_tys, ret_ty) as sy) ->
-         let arg_vals = List.map Expr.mk_abstract arg_tys in
-         let ret_val = Expr.mk_abstract ret_ty in
-         let graph = Graph.add arg_vals ret_val Graph.empty in
-         P.add sy graph values
+      (fun values ((_, _, ret_ty) as sy) ->
+         P.add sy (Free (Expr.mk_abstract ret_ty)) values
       )
       P.empty declared_ids
   in
@@ -178,22 +176,37 @@ let rec subst_in_term id e c =
 let subst id e { values; suspicious } =
   if not @@ Expr.is_model_term e then
     raise (Errors.Error (Model_error (Subst_not_model_term e)));
-  let values = P.map (Graph.map (subst_in_term id e)) values in
+
+  let values =
+    P.map
+      (fun graph ->
+         match graph with
+         | C constraints -> C (Constraints.map (subst_in_term id e) constraints)
+         | Free a -> Free (subst_in_term id e a)
+      ) values in
   { values; suspicious }
 
 let pp_named_arg_ty ~unused ppf (arg_name, arg_ty) =
   let pp_unused ppf unused = if unused then Fmt.pf ppf "_" else () in
   Fmt.pf ppf "(%aarg_%i %a)" pp_unused unused arg_name Ty.pp_smtlib arg_ty
 
-let pp_define_fun ppf ((id, arg_tys, ret_ty), graph) =
-  let inverse_rel = Graph.inverse graph in
-  let is_constant = Expr.Map.cardinal inverse_rel = 1 in
+let pp_define_fun ~is_constant pp ppf ((id, arg_tys, ret_ty), a) =
   let named_arg_tys = List.mapi (fun i arg_ty -> (i, arg_ty)) arg_tys in
   Fmt.pf ppf "(@[define-fun %a (%a) %a@ %a)@]"
     Id.pp id
     Fmt.(list ~sep:sp (pp_named_arg_ty ~unused:is_constant)) named_arg_tys
     Ty.pp_smtlib ret_ty
-    Graph.pp_inverse inverse_rel
+    pp a
+
+let pp_define_fun ppf (sy, graph) =
+  match graph with
+  | Free a ->
+    pp_define_fun ~is_constant:true Expr.pp_smtlib ppf (sy, a)
+
+  | C constraints ->
+    let inverse_rel = Constraints.inverse constraints  in
+    let is_constant = Expr.Map.cardinal inverse_rel = 1 in
+    pp_define_fun ~is_constant Constraints.pp_inverse ppf (sy, inverse_rel)
 
 let pp ppf {values; suspicious} =
   if suspicious then begin

tests/issues/854/function.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun f ((_arg_0 Int)) Int 0)
   (define-fun a1 () Int 0)

tests/issues/854/original.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )

tests/issues/854/twice_eq.models.expected

@@ -1,8 +1,8 @@
 
 unknown
 (
-  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a6 intref))
-  (define-fun another_mk ((_arg_0 Int)) intref (as @a6 intref))
+  (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref))
+  (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref))
   (define-fun a () Int 0)
   (define-fun a1 () Int 0)
 )

tests/models/complete_2.models.expected

@@ -1,6 +1,6 @@
 
 unknown
 (
-  (define-fun x () Int (as @a2 Int))
-  (define-fun f ((_arg_0 Int)) Int (as @a1 Int))
+  (define-fun x () Int (as @a1 Int))
+  (define-fun f ((_arg_0 Int)) Int (as @a0 Int))
 )