Generate complete model

This PR fixes the issue OCamlPro#778. The suggested solution by this PR is as follows:
- Collect user-declared symbols in `D_cnf`;
- As the function `make` of the module `D_cnf` returns a list of
  commands, we add a new command `Decl` in `Frontend` to declare
  symbols;
- The declared symbols are given to the SAT solver through a new
  function `declaration` in `sat_solver_sig`.
- These symbols are collected in vectors and we keep indexes in another
  PR in order to manage properly the push/pop mechanism.
- Finally the declared symbols are given to `Uf` and we create the empty
  model with them.

Another annoying point comes from the current datastructure used in
`ModelMap`. The type of `ModelMap` saves model values in the form of graphs.
A graph is a finite set of constraints but there is no appropriate
representation for the graph without constraints. Let's imagine we have
the input:
```smt2
(set-option :produce-models true)
(set-logic ALL)
(declare-fun (Int) Int)
(check-sat)
(get-model)
```
We expect an output as follows:
```smt2
(
  (define-fun f (_x Int) (@A as Int))
)
```
But `Graph.empty` cannot hold the abstract value `@a`. A naive solution
consists in using an ADT:
```ocaml
type graph =
| Empty of Id.typed
| G of Graph.t
```
But we'll add an extra indirection. Probably the best solution would be
to use a custom datastructure instead of a map to store the constraints.
In this PR, we detect in `ModelMap.add` if the only constraint in the
graph is of the form `something -> abstract value`. In this case we
remove this constraint.

This solution isn't perfect as explained in issue OCamlPro#1018. The biggest
drawback of this solution is the fact we have to declare symbols in the
SAT API, otherwise models returned by `get_model` could be
incomplete.

src/lib/frontend/d_cnf.ml

@@ -53,6 +53,12 @@ module HT = Hashtbl.Make(
     let hash = Fun.id
   end)
 
+module DeclSet = Set.Make
+    (struct
+      type t = Id.typed
+      let compare = Id.compare_typed
+    end)
+
 (** Helper function: returns the basename of a dolmen path, since in AE
     the problems are contained in one-file (for now at least), the path is
     irrelevant and only the basename matters *)
@@ -701,8 +707,15 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
     end
   in
   Cache.store_sy tcst sy;
+  Cache.store_ty_vars id_ty;
   (* Adding polymorphic types to the cache. *)
-  Cache.store_ty_vars id_ty
+  let arg_tys, ret_ty =
+    match DT.view id_ty with
+    | `Arrow (arg_tys, ret_ty) ->
+      List.map dty_to_ty arg_tys, dty_to_ty ret_ty
+    | _ -> [], dty_to_ty id_ty
+  in
+  (Hstring.make name, arg_tys, ret_ty)
 
 (** Handles the definitions of a list of mutually recursive types.
     - If one of the types is an ADT, the ADTs that have only one case are
@@ -2087,14 +2100,24 @@ let make dloc_file acc stmt =
             assert false
         ) defs
 
-    | {contents = `Decls [td]; _ } ->
-      begin match td with
-        | `Type_decl (td, _def) -> mk_ty_decl td
-        | `Term_decl td -> mk_term_decl td
-      end;
-      acc
+    | {contents = `Decls [td]; loc; _ } ->
+      let decl = match td with
+        | `Type_decl (td, _def) ->
+          mk_ty_decl td;
+          None
+
+        | `Term_decl td ->
+          Some (mk_term_decl td)
+      in
+      begin match decl with
+        | Some d ->
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl d; st_loc } :: acc
+        | None ->
+          acc
+      end
 
-    | {contents = `Decls dcl; _ } ->
+    | {contents = `Decls dcl; loc; _ } ->
       let rec aux acc tdl =
         (* for now, when acc has more than one element it is assumed that the
            types are mutually recursive. Which is not necessarily the case.
@@ -2107,21 +2130,24 @@ let make dloc_file acc stmt =
             | [otd] -> mk_ty_decl otd
             | _ -> mk_mr_ty_decls (List.rev acc)
           end;
-          mk_term_decl td;
-          aux [] tl
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl (mk_term_decl td); st_loc } :: aux [] tl
 
         | `Type_decl (td, _def) :: tl ->
           aux (td :: acc) tl
 
         | [] ->
-          begin match acc with
-            | [] -> ()
-            | [otd] -> mk_ty_decl otd
-            | _ ->  mk_mr_ty_decls (List.rev acc)
+          begin
+            let () =
+              match acc with
+              | [] -> ()
+              | [otd] -> mk_ty_decl otd
+              | _ ->  mk_mr_ty_decls (List.rev acc)
+            in
+            []
           end
       in
-      aux [] dcl;
-      acc
+      aux [] dcl @ acc
 
     | { contents = `Set_logic _ | `Set_info _ | `Get_info _ ; _ } -> acc
 

src/lib/frontend/frontend.ml

@@ -302,6 +302,13 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
     if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc})
     else Ex.empty
 
+  let internal_decl ?(loc = Loc.dummy) (id : Id.typed) (env : env) : unit =
+    ignore loc;
+    match env.res with
+    | `Sat | `Unknown ->
+      SAT.declare env.sat_env id
+    | `Unsat -> ()
+
   let internal_push ?(loc = Loc.dummy) (n : int) (env : env) : unit =
     ignore loc;
     Util.loop ~f:(fun _ res () -> Stack.push res env.consistent_dep_stack)
@@ -443,6 +450,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
   let process_decl ?(hook_on_status=(fun _ -> ignore)) env d =
     try
       match d.st_decl with
+      | Decl id -> check_if_over (internal_decl ~loc:d.st_loc id) env
       | Push n -> check_if_over (internal_push ~loc:d.st_loc n) env
       | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
       | Assume (n, f, mf) ->

src/lib/frontend/models.ml

@@ -43,7 +43,7 @@ type t = {
 
 let empty = {
   propositional = Expr.Set.empty;
-  model = ModelMap.empty ~suspicious:false;
+  model = ModelMap.empty ~suspicious:false [];
   term_values = Expr.Map.empty;
 }
 

src/lib/reasoners/ccx.ml

@@ -86,7 +86,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 
@@ -748,6 +751,6 @@ module Main : S = struct
     in
     Uf.term_repr env.uf t
 
-  let extract_concrete_model ~prop_model env =
-    Uf.extract_concrete_model ~prop_model env.uf
+  let extract_concrete_model ~prop_model ~declared_ids env =
+    Uf.extract_concrete_model ~prop_model ~declared_ids env.uf
 end

src/lib/reasoners/ccx.mli

@@ -77,7 +77,10 @@ module type S = sig
     Matching_types.info Expr.Map.t * Expr.t list Expr.Map.t Symbols.Map.t ->
     t -> (Expr.t -> Expr.t -> bool) -> t * Sig_rel.instances
 
-  val extract_concrete_model : prop_model:Expr.Set.t -> t -> Models.t
+  val extract_concrete_model :
+    prop_model:Expr.Set.t ->
+    declared_ids:Id.typed list ->
+    t -> Models.t
 
 end
 

src/lib/reasoners/fun_sat.ml

@@ -177,6 +177,8 @@ module Make (Th : Theory.S) = struct
     unit_facts_cache : (E.gformula * Ex.t) ME.t ref;
     last_saved_model : Models.t Lazy.t option ref;
     unknown_reason : Sat_solver_sig.unknown_reason option;
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let reset_refs () =
@@ -1123,7 +1125,8 @@ module Make (Th : Theory.S) = struct
     else begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
-        let model, _ = Th.compute_concrete_model env.tbox in
+        let declared_ids = Vec.to_list env.declare_ids in
+        let model, _ = Th.compute_concrete_model ~declared_ids env.tbox in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->
@@ -1611,6 +1614,10 @@ module Make (Th : Theory.S) = struct
           "solved with backward!";
       raise e
 
+  let declare env id =
+    Vec.push env.declare_ids id;
+    env
+
   let push env to_push =
     if Options.get_tableaux_cdcl () then
       Errors.run_error
@@ -1626,6 +1633,7 @@ module Make (Th : Theory.S) = struct
           let guards = ME.add new_guard
               (mk_gf new_guard "" true true,Ex.empty)
               acc.guards.guards in
+          Vec.push env.declare_lim (Vec.size env.declare_ids);
           {acc with guards =
                       { acc.guards with
                         current_guard = new_guard;
@@ -1656,6 +1664,8 @@ module Make (Th : Theory.S) = struct
           in
           acc.model_gen_phase := false;
           env.last_saved_model := None;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim;
           {acc with inst;
                     guards =
                       { acc.guards with
@@ -1837,6 +1847,8 @@ module Make (Th : Theory.S) = struct
       add_inst = selector;
       last_saved_model = ref None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
     in
     assume env gf_true Ex.empty

src/lib/reasoners/fun_sat.mli

@@ -38,6 +38,8 @@ module Make (Th : Theory.S) : sig
 
   val empty : ?selector:(Expr.t -> bool) -> unit -> t
 
+  val declare : t -> Id.typed -> t
+
   val push : t -> int -> t
 
   val pop : t -> int -> t

src/lib/reasoners/fun_sat_frontend.ml

@@ -45,6 +45,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     | FS.Unsat expl -> raise (Unsat expl)
     | FS.I_dont_know e -> env := e; raise I_dont_know
 
+  let declare t id =
+    t := FS.declare !t id
+
   let push t i = exn_handler (fun env -> t := FS.push env i) t
 
   let pop t i = exn_handler (fun env -> t := FS.pop env i) t

src/lib/reasoners/sat_solver_sig.ml

@@ -78,6 +78,13 @@ module type S = sig
       The optional argument [selector] is used to filter ground facts
       discovered by the instantiation engine. *)
 
+  val declare : t -> Id.typed -> unit
+  (** [declare env id] declares a new identifier [id].
+
+      If the environment [env] isn't unsatisfiable and the model generation
+      is enabled, the solver produces a model term for [id] which can be
+      retrieved with [get_model]. *)
+
   val push : t -> int -> unit
   (** [push env n] adds [n] new assertion levels in [env].
 

src/lib/reasoners/sat_solver_sig.mli

@@ -58,6 +58,13 @@ module type S = sig
       The optional argument [selector] is used to filter ground facts
       discovered by the instantiation engine. *)
 
+  val declare : t -> Id.typed -> unit
+  (** [declare env id] declares a new identifier [id].
+
+      If the environment [env] isn't unsatisfiable and the model generation
+      is enabled, the solver produces a model term for [id] which can be
+      retrieved with [get_model]. *)
+
   val push : t -> int -> unit
   (** [push env n] adds [n] new assertion levels in [env].
 

src/lib/reasoners/satml_frontend.ml

@@ -67,6 +67,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     mutable unknown_reason : Sat_solver_sig.unknown_reason option;
     (** The reason why satml raised [I_dont_know] if it does; [None] by
         default. *)
+    declare_ids : Id.typed Vec.t;
+    declare_lim : int Vec.t;
   }
 
   let empty_guards () = {
@@ -97,6 +99,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       last_saved_model = None;
       last_saved_objectives = None;
       unknown_reason = None;
+      declare_ids = Vec.make 17 ~dummy:Id.dummy_typed;
+      declare_lim = Vec.make 17 ~dummy:(-1);
     }
 
   exception Sat
@@ -965,8 +969,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     if compute then begin
       try
         (* also performs case-split and pushes pending atoms to CS *)
+        let declared_ids = Vec.to_list env.declare_ids in
         let model, objectives =
-          Th.compute_concrete_model (SAT.current_tbox env.satml)
+          Th.compute_concrete_model ~declared_ids (SAT.current_tbox env.satml)
         in
         env.last_saved_model <- Some model;
         env.last_saved_objectives <- Some objectives;
@@ -1204,14 +1209,17 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       expr_guard, atom_guard
     | _ -> assert false
 
+  let declare env id = Vec.push env.declare_ids id
+
   let push env to_push =
     Util.loop ~f:(fun _n () () ->
         try
           let expr_guard, atom_guard = create_guard env in
           SAT.push env.satml atom_guard;
           Stack.push expr_guard env.guards.stack_guard;
           Steps.push_steps ();
-          env.guards.current_guard <- expr_guard
+          env.guards.current_guard <- expr_guard;
+          Vec.push env.declare_lim (Vec.size env.declare_ids)
         with
         | Util.Step_limit_reached _ ->
           (* This function should be called without step limit
@@ -1234,7 +1242,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           env.last_saved_model <- None;
           env.last_saved_objectives <- None;
           env.inst <- inst;
-          env.guards.current_guard <- b
+          env.guards.current_guard <- b;
+          let lim = Vec.size env.declare_ids - Vec.pop env.declare_lim in
+          Vec.shrink env.declare_ids lim
         )
       ~max:to_pop
       ~elt:()

src/lib/reasoners/theory.ml

@@ -61,7 +61,10 @@ module type S = sig
   val do_case_split : t -> Util.case_split_policy -> t * Expr.Set.t
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :
@@ -879,13 +882,14 @@ module Main_Default : S = struct
   let get_real_env t = t.gamma
   let get_case_split_env t = t.gamma_finite
 
-  let compute_concrete_model env =
+  let compute_concrete_model env ~declared_ids =
     let { gamma_finite; assumed_set; objectives; _ }, _ =
       do_case_split_aux env ~for_model:true
     in
     lazy (
       CC_X.extract_concrete_model
         ~prop_model:assumed_set
+        ~declared_ids
         gamma_finite
     ), objectives
 
@@ -940,7 +944,8 @@ module Main_Empty : S = struct
   let get_case_split_env _ = CC_X.empty
   let do_case_split env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
-  let compute_concrete_model _env = lazy Models.empty, Objective.Model.empty
+  let compute_concrete_model _env ~declared_ids:_ =
+    lazy Models.empty, Objective.Model.empty
 
   let assume_th_elt e _ _ = e
   let theories_instances ~do_syntactic_matching:_ _ e _ _ _ = e, []

src/lib/reasoners/theory.mli

@@ -54,7 +54,10 @@ module type S = sig
 
   val add_term : t -> Expr.t -> add_in_cs:bool -> t
 
-  val compute_concrete_model : t -> Models.t Lazy.t * Objective.Model.t
+  val compute_concrete_model :
+    t ->
+    declared_ids:Id.typed list ->
+    Models.t Lazy.t * Objective.Model.t
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> t
   val theories_instances :

src/lib/reasoners/uf.ml

@@ -1167,11 +1167,11 @@ let compute_concrete_model_of_val cache =
 let extract_concrete_model cache =
   let compute_concrete_model_of_val = compute_concrete_model_of_val cache in
   let get_abstract_for = Cache.get_abstract_for cache.abstracts
-  in fun ~prop_model env ->
+  in fun ~prop_model ~declared_ids env ->
     let terms, suspicious = terms env in
     let model, mrepr =
       MED.fold (fun t _mk acc -> compute_concrete_model_of_val env t acc)
-        terms (ModelMap.empty ~suspicious, ME.empty)
+        terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
     in
     let model =
       Hashtbl.fold (fun t vals mdl ->
@@ -1212,9 +1212,9 @@ let extract_concrete_model cache =
     in
     { Models.propositional = prop_model; model; term_values = mrepr }
 
-let extract_concrete_model ~prop_model =
+let extract_concrete_model ~prop_model ~declared_ids =
   let cache : cache = {
     array_selects = Hashtbl.create 17;
     abstracts = Hashtbl.create 17;
   }
-  in fun env -> extract_concrete_model cache ~prop_model env
+  in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env