feat: get-assignment statement (#848)

* Produce assignments option

* Placeholder for get_assignments

* Gathering the named formulae

* Pulling threads up to the SAT solver

* Update tests

* Proprification

* Adding basic get_value

* Update tests

* Poetry

* Removing useless check

* Removing spurious term selection in binder

* Poetry

* Adding tests

* Adding tests & handling case where model gen is disabled

* Update test

src/bin/common/solving_loop.ml

@@ -95,6 +95,47 @@ let enable_maxsmt b =
   else
     DStd.Extensions.Smtlib2.(disable maxsmt)
 
+(* Dolmen util *)
+
+(** 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) ->
+          (* TODO: consider catching the terms in the binder *)
+          [t] :: 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
 
@@ -295,6 +336,14 @@ let main () =
     State.create_key ~pipe:"" "optimize"
   in
 
+  let produce_assignment: bool State.key =
+    State.create_key ~pipe:"" "produce_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@]@."
@@ -407,6 +456,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 produce_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
@@ -534,10 +585,18 @@ let main () =
               solver;
             st
       )
+    | ":produce-assignments",  Symbol { name = Simple b; _ } ->
+      begin
+        match bool_of_string_opt b with
+        | None ->
+          print_wrn_opt ~name:":verbosity" st_loc "boolean" value;
+          st
+        | Some b ->
+          State.set produce_assignment b st
+      end
     | (":global-declarations"
       | ":interactive-mode"
       | ":produce-assertions"
-      | ":produce-assignments"
       | ":produce-proofs"
       | ":produce-unsat-assumptions"
       | ":print-success"
@@ -648,13 +707,58 @@ let main () =
       unsupported_opt name
   in
 
+  (* Fetches the term value in the current model. *)
+  let evaluate_term get_value name term =
+    let ae_form =
+      D_cnf.make_form
+        name
+        term
+        Loc.dummy
+        ~decl_kind:Expr.Dgoal
+    in
+    match get_value ae_form with
+    | None -> "unknown" (* Not in the standard, but useful for recording when
+                           Alt-Ergo fails to guess the value of a term. *)
+    | Some v -> Fmt.to_to_string Expr.print v
+  in
+
+  let print_terms_assignments =
+    Fmt.list
+      ~sep:Fmt.cut
+      (fun fmt (name, v) -> Fmt.pf fmt "(%s %s)" name v)
+  in
+
+  let handle_get_assignment ~get_value st =
+    let assignments =
+      Util.MS.fold
+        (fun name term acc ->
+           if DStd.Expr.Ty.equal term.DStd.Expr.term_ty DStd.Expr.Ty.bool then
+             (name, evaluate_term get_value name term) :: acc
+           else
+             acc
+        )
+        (State.get named_terms st)
+        []
+    in
+    Printer.print_std
+      "(@[<v 0>%a@])@,"
+      print_terms_assignments
+      assignments
+  in
+
   let handle_stmt :
     Frontend.used_context -> State.t ->
     _ D_loop.Typer_Pipe.stmt -> State.t =
     let goal_cnt = ref 0 in
     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 *)
@@ -761,6 +865,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 produce_assignment false
+        |> State.set named_terms Util.MS.empty
 
       | {contents = `Exit; _} -> raise Exit
 
@@ -776,6 +882,26 @@ let main () =
         handle_get_info st kind;
         st
 
+      | {contents = `Get_assignment; _} ->
+        begin
+          match State.get partial_model_key st with
+          | Some Model ((module SAT), partial_model) ->
+            if State.get produce_assignment st then
+              handle_get_assignment
+                ~get_value:(SAT.get_value partial_model)
+                st
+            else
+              recoverable_error
+                "Produce assignments disabled; \
+                 add (set-option :produce-assignments true)";
+            st
+          | None ->
+            (* TODO: add the location of the statement. *)
+            recoverable_error
+              "No model produced, cannot execute get-assignment.";
+            st
+        end
+
       | {contents = `Other (custom, args); _} ->
         handle_custom_statement custom args st
 

src/lib/frontend/d_cnf.mli

@@ -31,6 +31,13 @@
 val clear_cache : unit -> unit
 (** Empties the internal cache of the module. *)
 
+val make_form :
+  string ->
+  D_loop.DStd.Expr.term ->
+  Loc.t ->
+  decl_kind:Expr.decl_kind ->
+  Expr.t
+
 val make :
   D_loop.DStd.Loc.file ->
   Commands.sat_tdecl list ->

src/lib/reasoners/fun_sat.ml

@@ -1847,6 +1847,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
+
   let reinit_ctx () =
     (* all_models_sat_env := None; *)
     (* latest_saved_env := None;

src/lib/reasoners/sat_solver_sig.ml

@@ -89,6 +89,10 @@ module type S = sig
   (** [get_unknown_reason t] returns the reason Alt-Ergo raised
       [I_dont_know] if it did. If it did not, returns None. *)
   val get_unknown_reason : t -> unknown_reason option
+
+  (** [get_value t e] returns the value of [e] as a constant expression
+      in the current model generated. Returns [None] if can't decide. *)
+  val get_value : t -> Expr.t -> Expr.t option
 end
 
 

src/lib/reasoners/sat_solver_sig.mli

@@ -90,6 +90,10 @@ module type S = sig
   (** [get_unknown_reason t] returns the reason Alt-Ergo raised
       [I_dont_know] if it did. If it did not, returns None. *)
   val get_unknown_reason : t -> unknown_reason option
+
+  (** [get_value t e] returns the value of [e] as a constant expression
+      in the current model generated. Returns [None] if can't decide. *)
+  val get_value : t -> Expr.t -> Expr.t option
 end
 
 

src/lib/reasoners/satml_frontend.ml

@@ -1384,6 +1384,16 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let get_unknown_reason env = env.unknown_reason
 
+  let get_value env t =
+    match E.type_info t with
+    | Ty.Tbool ->
+      begin
+        match ME.find_opt t env.gamma with
+        | None -> Some E.faux
+        | Some _ -> Some E.vrai
+      end
+    | _ -> None
+
   let reinit_ctx () =
     Steps.reinit_steps ();
     Th.reinit_cpt ();

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:

tests/models/bool/bool1.models.expected

@@ -3,9 +3,15 @@ unknown
 (
   (define-fun q () Bool false)
 )
+((notp false)
+ (notnq true))
+
 
 unknown
 (
   (define-fun p () Bool true)
   (define-fun q () Bool true)
 )
+((notp false)
+ (notnq false))
+