Expose the map in ModelMap, and add find and fold functions over that map

src/lib/structures/modelMap.ml

@@ -19,6 +19,11 @@
 module X = Shostak.Combine
 module Sy = Symbols
 
+module M: Map.S with type key = Expr.t list = Map.Make
+    (struct
+      type t = Expr.t list [@@deriving ord]
+    end)
+
 (* 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
@@ -27,10 +32,6 @@ module Sy = Symbols
    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]
-      end)
 
   type t = Expr.t M.t
 
@@ -137,6 +138,12 @@ let add ((id, arg_tys, _) as sy) arg_vals ret_val { values; suspicious } =
   in
   { values; suspicious }
 
+let find k {values; _ } =
+  P.find k values
+
+let fold f {values;_} acc  =
+  P.fold f values acc
+
 let empty ~suspicious declared_ids =
   let values =
     List.fold_left

src/lib/structures/modelMap.mli

@@ -16,6 +16,15 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module M: Map.S with type key = Expr.t list
+
+type graph =
+  | Free of Expr.t
+  (* Represents a graph without any constraint. The expression is
+     an abstract value. *)
+
+  | C of Expr.t M.t
+
 type t
 (** Type of model. *)
 
@@ -28,6 +37,14 @@ val empty : suspicious:bool -> Id.typed list -> t
     model may be wrong as it involves symbols from theories for which the
     model generation is known to be incomplete. *)
 
+val find : Id.typed -> t -> graph
+(** [find sy mdl] returns the graph associated with the symbol [sy] in the model
+    [mdl], raises [Not_found] if it doesn't exist. *)
+
+val fold: (Id.typed -> graph -> 'a -> 'a) -> t -> 'a -> 'a
+(** [fold f mdl init] folds over the bindings in the model [mdl] with the
+    function [f] and with [init] as a initial value for the accumulator. *)
+
 val subst : Id.t -> Expr.t -> t -> t
 (** [subst id e mdl] substitutes all the occurrences of the identifier [id]
     in the model [mdl] by the model term [e].