Complete model

src/lib/frontend/d_cnf.ml

@@ -702,7 +702,14 @@ let mk_term_decl ({ id_ty; path; tags; _ } as tcst: DE.term_cst) =
   in
   Cache.store_sy tcst sy;
   (* Adding polymorphic types to the cache. *)
-  Cache.store_ty_vars id_ty
+  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,41 +2094,48 @@ let make dloc_file acc stmt =
             assert false
         ) defs
 
-    | {contents = `Decls [td]; _ } ->
+    | {contents = `Decls [td]; loc; _ } ->
       begin match td with
-        | `Type_decl (td, _def) -> mk_ty_decl td
-        | `Term_decl td -> mk_term_decl td
-      end;
-      acc
+        | `Type_decl (td, _def) ->
+          mk_ty_decl td;
+          acc
+
+        | `Term_decl td ->
+          let st_loc = dl_to_ael dloc_file loc in
+          C.{ st_decl = Decl (mk_term_decl td); st_loc } :: acc
+      end
 
-    | {contents = `Decls dcl; _ } ->
-      let rec aux acc tdl =
+    | {contents = `Decls dcl; loc; _ } ->
+      let rec aux ty_decls tdl acc =
         (* for now, when acc has more than one element it is assumed that the
            types are mutually recursive. Which is not necessarily the case.
            But it doesn't affect the execution.
         *)
         match tdl with
         | `Term_decl td :: tl ->
-          begin match acc with
+          begin match ty_decls with
             | [] -> ()
             | [otd] -> mk_ty_decl otd
-            | _ -> mk_mr_ty_decls (List.rev acc)
+            | _ -> mk_mr_ty_decls (List.rev ty_decls)
           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 acc
 
         | `Type_decl (td, _def) :: tl ->
-          aux (td :: acc) tl
+          aux (td :: ty_decls) tl acc
 
         | [] ->
-          begin match acc with
-            | [] -> ()
-            | [otd] -> mk_ty_decl otd
-            | _ ->  mk_mr_ty_decls (List.rev acc)
+          begin
+            let () =
+              match ty_decls with
+              | [] -> ()
+              | [otd] -> mk_ty_decl otd
+              | _ ->  mk_mr_ty_decls (List.rev ty_decls)
+            in
+            acc
           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,12 @@ 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_top : Id.typed list ref;
+    declare_tail : Id.typed list Stack.t;
+    (** Stack of the declared symbols by the user. The field [declare_top]
+        is the top of the stack and [declare_tail] is tail. In particular, this
+        stack is never empty. *)
   }
 
   let reset_refs () =
@@ -1123,7 +1129,9 @@ 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 model, _ =
+          Th.compute_concrete_model ~declared_ids:!(env.declare_top) env.tbox
+        in
         env.last_saved_model := Some model;
         env
       with Ex.Inconsistent (expl, classes) ->
@@ -1611,6 +1619,10 @@ module Make (Th : Theory.S) = struct
           "solved with backward!";
       raise e
 
+  let declare env id =
+    env.declare_top := id :: !(env.declare_top);
+    env
+
   let push env to_push =
     if Options.get_tableaux_cdcl () then
       Errors.run_error
@@ -1626,6 +1638,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
+          Stack.push !(env.declare_top) env.declare_tail;
           {acc with guards =
                       { acc.guards with
                         current_guard = new_guard;
@@ -1656,6 +1669,11 @@ module Make (Th : Theory.S) = struct
           in
           acc.model_gen_phase := false;
           env.last_saved_model := None;
+          let () =
+            try env.declare_top := Stack.pop env.declare_tail
+            with Stack.Empty ->
+              Errors.error (Run_error Stack_underflow)
+          in
           {acc with inst;
                     guards =
                       { acc.guards with
@@ -1837,6 +1855,8 @@ module Make (Th : Theory.S) = struct
       add_inst = selector;
       last_saved_model = ref None;
       unknown_reason = None;
+      declare_top = ref [];
+      declare_tail = Stack.create ();
     }
     in
     assume env gf_true Ex.empty

src/lib/reasoners/fun_sat.mli

@@ -38,9 +38,14 @@ 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
+  (** [pop env n] pops [n] assertion levels of the environment [env].
+
+      @raise Errors.Error if there is no [n] assertion levels in [env]. *)
 
   val assume : t -> Expr.gformula -> Explanation.t -> 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].
 
@@ -91,7 +98,9 @@ module type S = sig
   (** [pop env n] removes [n] assertion levels in [env].
 
       Internally, the guard [g] introduced in [push] corresponding to this pop
-      is propagated to [false] at level [0]. *)
+      is propagated to [false] at level [0].
+
+      @raise Errors.Error if there is no [n] assertion levels in [env]. *)
 
   val assume : t -> Expr.gformula -> Explanation.t -> unit
   (** [assume env f dep] assumes the ground formula [f] 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].
 
@@ -71,7 +78,9 @@ module type S = sig
   (** [pop env n] removes [n] assertion levels in [env].
 
       Internally, the guard [g] introduced in [push] corresponding to this pop
-      is propagated to [false] at level [0]. *)
+      is propagated to [false] at level [0].
+
+      @raise Errors.Error if there is no [n] assertion levels in [env]. *)
 
   val assume : t -> Expr.gformula -> Explanation.t -> unit
   (** [assume env f dep] assumes the ground formula [f] in [env].

src/lib/reasoners/satml_frontend.ml

@@ -67,6 +67,12 @@ 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. *)
+
+    mutable declare_top : Id.typed list;
+    declare_tail : Id.typed list Stack.t;
+    (** Stack of the declared symbols by the user. The field [declare_top]
+        is the top of the stack and [declare_tail] is tail. In particular, this
+        stack is never empty. *)
   }
 
   let empty_guards () = {
@@ -97,6 +103,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       last_saved_model = None;
       last_saved_objectives = None;
       unknown_reason = None;
+      declare_top = [];
+      declare_tail = Stack.create ();
     }
 
   exception Sat
@@ -966,7 +974,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       try
         (* also performs case-split and pushes pending atoms to CS *)
         let model, objectives =
-          Th.compute_concrete_model (SAT.current_tbox env.satml)
+          Th.compute_concrete_model ~declared_ids:env.declare_top
+            (SAT.current_tbox env.satml)
         in
         env.last_saved_model <- Some model;
         env.last_saved_objectives <- Some objectives;
@@ -1204,14 +1213,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       expr_guard, atom_guard
     | _ -> assert false
 
+  let declare env id =
+    env.declare_top <- id :: env.declare_top
+
   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;
+          Stack.push env.declare_top env.declare_tail;
         with
         | Util.Step_limit_reached _ ->
           (* This function should be called without step limit
@@ -1234,7 +1247,14 @@ 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 declare_top =
+            try
+              Stack.pop env.declare_tail
+            with Stack.Empty ->
+              Errors.error (Run_error Stack_underflow)
+          in
+          env.declare_top <- declare_top;
         )
       ~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, []