diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 21e52c6e5..ff90a8977 100644 --- a/src/bin/common/solving_loop.ml +++ b/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] @[%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 () = - match bool_of_string_opt b with - | None -> - print_wrn_opt ~name:":verbosity" st_loc "integer" value - | Some b -> - Options.set_produce_assignments b - in st + begin + match bool_of_string_opt b with + | None -> + print_wrn_opt ~name:":verbosity" st_loc "integer" value; + st + | Some b -> + 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 : DStd.Expr.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 "(@[%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 diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index 34dcf529e..f63009014 100644 --- a/src/lib/util/options.ml +++ b/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 *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index f037536b9..0725fdb60 100644 --- a/src/lib/util/options.mli +++ b/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. diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index fb796fd78..fdbe3b2ba 100644 --- a/src/lib/util/util.ml +++ b/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) diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 92458b95f..9a6d6e115 100644 --- a/src/lib/util/util.mli +++ b/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: