Produce assignments option

src/bin/common/solving_loop.ml

@@ -391,10 +391,15 @@ let main () =
           print_wrn_opt ~name:":reproducible-resource-limit" st_loc
             "nonnegative integer" value
       end
+    | ":produce-assignments",  Symbol { name = Simple b; _ } ->
+      begin
+        match bool_of_string_opt b with
+        | None -> print_wrn_opt ~name:":verbosity" st_loc "integer" value
+        | Some b -> Options.set_produce_assignments b
+      end
     | (":global-declarations"
       | ":interactive-mode"
       | ":produce-assertions"
-      | ":produce-assignments"
       | ":produce-proofs"
       | ":produce-unsat-assumptions"
       | ":print-success"

src/lib/util/options.ml

@@ -344,6 +344,7 @@ 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_dump_models b = dump_models := b
@@ -352,6 +353,7 @@ 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
@@ -391,6 +393,7 @@ 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

@@ -291,6 +291,9 @@ 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
 
@@ -764,6 +767,10 @@ 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.