Gathering the named formulae

src/bin/common/solving_loop.ml

@@ -95,6 +95,52 @@ let enable_maxsmt b =
   else
     DStd.Extensions.Smtlib2.(disable maxsmt)
 
+(* Dolmen util *)
+
+(** Returns the list of terms inside a dolmen binder. *)
+let terms_of_dolmen_binder = function
+  | DStd.Expr.Let_seq l | Let_par l ->
+     List.map snd l
+  | Lambda _ | Exists _ | Forall _ -> []
+
+(** Adds the named terms of the term [term] to the map accumulator [acc] *)
+let get_named_of_term
+      (acc : DStd.Expr.term Util.MS.t)
+      (term : DStd.Expr.term) =
+  let rec loop acc terms_to_check =
+    match terms_to_check with
+    | [] -> acc
+    | [] :: rest -> loop acc rest
+    | (term :: tl) :: rest ->
+       let terms_to_check = tl :: rest in
+       let terms_to_check =
+         match term.DStd.Expr.term_descr with
+         | DStd.Expr.Var _ | Cst _ -> terms_to_check
+         | App (t, _, tl) -> (t :: tl) :: terms_to_check
+         | Binder (b, t) ->
+            (t :: terms_of_dolmen_binder b) :: terms_to_check
+         | Match (t, plt) -> (t :: (List.map snd plt)) :: terms_to_check
+       in
+       match DStd.Expr.Term.get_tag term DStd.Expr.Tags.named with
+       | None -> loop acc terms_to_check
+       | Some name -> loop (Util.MS.add name term acc) terms_to_check
+  in
+  loop acc [[term]]
+
+(** Adds the named terms of the statement [stmt] to the map accumulator [acc] *)
+let get_named_of_stmt
+      ~(acc : DStd.Expr.term Util.MS.t)
+      (stmt : Typer_Pipe.typechecked D_loop.Typer_Pipe.stmt) =
+  match stmt.contents with
+  | `Hyp f | `Goal f -> get_named_of_term acc f
+  | `Clause l -> List.fold_left get_named_of_term acc l
+  | `Solve (l1, l2) ->
+     List.fold_left
+       get_named_of_term
+       (List.fold_left get_named_of_term acc l1)
+       l2
+  | _ -> acc
+
 (* We currently use the full state of the solver as model. *)
 type model = Model : 'a sat_module * 'a -> model
 
@@ -297,6 +343,14 @@ let main () =
     State.create_key ~pipe:"" "optimize"
   in
 
+  let get_assignment: bool State.key =
+    State.create_key ~pipe:"" "get_assignment"
+  in
+
+  let named_terms: DStd.Expr.term Util.MS.t State.key =
+    State.create_key ~pipe:"" "named_terms"
+  in
+
   let debug_parsed_pipe st c =
     if State.get State.debug st then
       Format.eprintf "[logic][parsed][%a] @[<hov>%a@]@."
@@ -409,6 +463,8 @@ let main () =
     |> State.set solver_ctx_key solver_ctx
     |> State.set partial_model_key partial_model
     |> State.set optimize_key (O.get_optimize ())
+    |> State.set get_assignment false
+    |> State.set named_terms Util.MS.empty
     |> State.init ~debug ~report_style ~reports ~max_warn ~time_limit
       ~size_limit ~response_file
     |> Parser.init
@@ -537,13 +593,14 @@ let main () =
             st
       )
     | ":produce-assignments",  Symbol { name = Simple b; _ } ->
-       let () =
+       begin
          match bool_of_string_opt b with
          | None ->
-            print_wrn_opt ~name:":verbosity" st_loc "integer" value
+            print_wrn_opt ~name:":verbosity" st_loc "integer" value;
+            st
          | Some b ->
-            Options.set_produce_assignments b
-       in st
+            State.set get_assignment b st
+       end
     | (":global-declarations"
       | ":interactive-mode"
       | ":produce-assertions"
@@ -657,8 +714,20 @@ let main () =
       unsupported_opt name
   in
 
-  let handle_get_assignment _ =
-    failwith "TODO: handle_get_assignment"
+  let evaluate_term _term = "unknown" in
+
+  let handle_term name term fmt =
+    Fmt.pf fmt "@,(%s %s)" name (evaluate_term term)
+  in
+
+  let handle_terms fmt map =
+    Util.MS.iter
+      (fun name term -> Fmt.pf fmt "%t" (handle_term name term))
+      map
+  in
+
+  let handle_get_assignment st =
+    Printer.print_std "(@[<v 0>%a@])@," handle_terms (State.get named_terms st)
   in
 
   let handle_stmt :
@@ -668,6 +737,12 @@ let main () =
     fun all_context st td ->
       let file_loc = (State.get State.logic_file st).loc in
       let solver_ctx = State.get solver_ctx_key st in
+      let st =
+        let named_terms_map =
+          get_named_of_stmt ~acc:(State.get named_terms st) td
+        in
+        State.set named_terms named_terms_map st
+      in
       match td with
       (* When the next statement is a goal, the solver is called and provided
          the goal and the current context *)
@@ -774,6 +849,8 @@ let main () =
         |> State.set partial_model_key None
         |> State.set solver_ctx_key empty_solver_ctx
         |> State.set optimize_key (O.get_optimize ())
+        |> State.set get_assignment false
+        |> State.set named_terms Util.MS.empty
 
       | {contents = `Exit; _} -> raise Exit
 
@@ -790,12 +867,13 @@ let main () =
         st
 
       | {contents = `Get_assignment; _} ->
-        if Options.get_produce_assignments () then
-          handle_get_assignment ()
+        if State.get get_assignment st then
+          let () = handle_get_assignment st in st
         else
           begin
             Printer.print_smtlib_err
-              "Produce assignments disabled; add (set-option :produce-assignment)";
+              "Produce assignments disabled; \
+               add (set-option :produce-assignments true)";
             st
           end
 

src/lib/util/options.ml

@@ -345,7 +345,6 @@ let output_format = ref Native
 let model_type = ref Value
 let infer_output_format = ref true
 let unsat_core = ref false
-let produce_assignments = ref false
 
 let set_interpretation b = interpretation := b
 let set_optimize b = optimize := b
@@ -355,7 +354,6 @@ let set_output_format b = output_format := b
 let set_model_type t = model_type := t
 let set_infer_output_format b = infer_output_format := b
 let set_unsat_core b = unsat_core := b
-let set_produce_assignments b = produce_assignments := b
 
 let equal_mode a b =
   match a, b with
@@ -396,7 +394,6 @@ let get_model_type () = !model_type
 let get_model_type_constraints () = equal_mode_type !model_type Constraints
 let get_infer_output_format () = !infer_output_format
 let get_unsat_core () = !unsat_core || !save_used_context || !debug_unsat_core
-let get_produce_assignments () = !produce_assignments
 
 (** Profiling options *)
 

src/lib/util/options.mli

@@ -294,9 +294,6 @@ val set_type_smt2 : bool -> unit
 (** Set [unsat_core] accessible with {!val:get_unsat_core} *)
 val set_unsat_core : bool -> unit
 
-(** Set [produce_assignments] accessible with {!val:get_produce_assignments} *)
-val set_produce_assignments : bool -> unit
-
 (** Set [verbose] accessible with {!val:get_verbose} *)
 val set_verbose : bool -> unit
 
@@ -772,10 +769,6 @@ val get_infer_output_format : unit -> bool
 val get_unsat_core : unit -> bool
 (** Default to [false] *)
 
-(** [true] if Alt-Ergo allow to display the truth assignment for the labeled
-    formulas. *)
-val get_produce_assignments : unit -> bool
-
 (** {4 Profiling options} *)
 
 (** [true] if the profiling module is activated.

src/lib/util/util.ml

@@ -52,6 +52,8 @@ module MI = Map.Make(struct type t = int
 module SI = Set.Make(struct type t = int
     let compare (x: int) y = Stdlib.compare x y end)
 
+module MS = Map.Make(String)
+
 module SS = Set.Make(String)
 
 

src/lib/util/util.mli

@@ -36,6 +36,7 @@ exception Not_implemented of string
 
 module MI : Map.S with type key = int
 module SI : Set.S with type elt = int
+module MS : Map.S with type key = string
 module SS : Set.S with type elt = string
 
 (** Different values for -case-split-policy option: