Clean up documentation of the SAT API (#1020)

* Clean up documentation of the SAT API

* Review changes

src/bin/js/worker_js.ml

@@ -123,7 +123,7 @@ let main worker_id content =
     let solve all_context (cnf, goal_name) =
       let used_context = Frontend.choose_used_context all_context ~goal_name in
       SAT.reset_refs ();
-      let sat_env = SAT.empty_with_inst add_inst in
+      let sat_env = SAT.empty ~selector:add_inst () in
       let ftnd_env = FE.init_env ~sat_env used_context in
       List.iter
         (FE.process_decl ~hook_on_status:get_status_and_print ftnd_env)

src/lib/reasoners/fun_sat.ml

@@ -1803,7 +1803,7 @@ module Make (Th : Theory.S) = struct
     Stack.push (Expr.vrai,{unit_facts = ME.empty}) guards.stack_elt;
     guards
 
-  let empty () =
+  let empty ?(selector=fun _ -> true) () =
     (* initialize some structures in SAT.empty. Otherwise, E.faux is never
        added as it is replaced with (not E.vrai) *)
     reset_refs ();
@@ -1834,17 +1834,14 @@ module Make (Th : Theory.S) = struct
       model_gen_phase = ref false;
       unit_facts_cache = ref ME.empty;
       guards = init_guards ();
-      add_inst = (fun _ -> true);
+      add_inst = selector;
       last_saved_model = ref None;
       unknown_reason = None;
     }
     in
     assume env gf_true Ex.empty
   (*maybe usefull when -no-theory is on*)
 
-  let empty_with_inst add_inst =
-    { (empty ()) with add_inst = add_inst }
-
   let assume_th_elt env th_elt dep =
     {env with tbox = Th.assume_th_elt env.tbox th_elt dep}
 

src/lib/reasoners/fun_sat.mli

@@ -36,9 +36,7 @@ module Make (Th : Theory.S) : sig
   exception Unsat of Explanation.t
   exception I_dont_know of t
 
-  val empty : unit -> t
-
-  val empty_with_inst : (Expr.t -> bool) -> t
+  val empty : ?selector:(Expr.t -> bool) -> unit -> t
 
   val push : t -> int -> t
 

src/lib/reasoners/fun_sat_frontend.ml

@@ -37,9 +37,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   type t = FS.t ref
 
-  let empty () = ref (FS.empty ())
-
-  let empty_with_inst f = ref (FS.empty_with_inst f)
+  let empty ?selector () = ref (FS.empty ?selector ())
 
   let exn_handler f env =
     try f !env with

src/lib/reasoners/sat_solver_sig.ml

@@ -72,58 +72,82 @@ module type S = sig
   exception Unsat of Explanation.t
   exception I_dont_know
 
-  (* the empty sat-solver context *)
-  val empty : unit -> t
-  val empty_with_inst : (Expr.t -> bool) -> t
-
-  (** [push env n] add n new assertion levels.
-      A guard g is added for every expression e assumed at the current
-      assertion level.
-      Ie. assuming e after the push will become g -> e,
-      a g will be forced to be true (but not propagated at level 0) *)
+  val empty : ?selector:(Expr.t -> bool) -> unit -> t
+  (** [empty ~selector ()] creates an empty environment.
+
+      The optional argument [selector] is used to filter ground facts
+      discovered by the instantiation engine. *)
+
   val push : t -> int -> unit
+  (** [push env n] adds [n] new assertion levels in [env].
+
+      Internally, for each new assertion level, a fresh guard [g] is created
+      and all formulas [f] assumed at this assertion level is replaced by
+      [g ==> f].
+
+      The guard [g] is forced to be [true] but not propagated at level [0]. *)
 
-  (** [pop env n] remove an assertion level.
-      Internally, the guard g introduced in the push correponsding to this pop
-      will be propagated to false (at level 0) *)
   val pop : t -> int -> unit
+  (** [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]. *)
 
-  (* [assume env f] assume a new formula [f] in [env]. Raises Unsat if
-     [f] is unsatisfiable in [env] *)
   val assume : t -> Expr.gformula -> Explanation.t -> unit
+  (** [assume env f dep] assumes the ground formula [f] in [env].
+      The [dep] argument can be used to generate an unsat core.
+
+      @raise Unsat if [f] is unsatisfiable in [env]. *)
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
+  (** [assume env f exp] assumes a new formula [f] with the explanation [exp]
+      in the theory environment of [env]. *)
 
-  (* [pred_def env f] assume a new predicate definition [f] in [env]. *)
   val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit
+  (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 
-  (** [optimize env ~is_max o] registers the expression [o]
-      as an objective function. *)
   val optimize : t -> is_max:bool -> Expr.t -> unit
+  (** [optimize env ~is_max o] registers the expression [o] as an objective
+      function.
+
+      The solver will try to maximize [o] if [is_max] is [true]. Otherwise,
+      it will try to minimize it.
+
+      After optimization, the value of this objective is returned by
+      [get_objectives]. *)
 
-  (* [unsat env f size] checks the unsatisfiability of [f] in
-     [env]. Raises I_dont_know when the proof tree's height reaches
-     [size]. Raises Sat if [f] is satisfiable in [env] *)
   val unsat : t -> Expr.gformula -> Explanation.t
+  (** [unsat env f] checks the unsatisfiability of [f] in [env].
+
+      @raise I_dont_know if the solver cannot prove the unsatisfiability
+             of [env].
+      @raise Sat if [f] is satisfiable in [env]. *)
 
   val reset_refs : unit -> unit
 
-  (** [reinit_ctx ()] reinitializes the solving context. *)
   val reinit_ctx : unit -> unit
+  (** [reinit_ctx ()] reinitializes the solving context. *)
 
-  (** [get_model t] produces the current model. *)
   val get_model: t -> Models.t option
+  (** [get_model t] produces the current first-order model.
+      Notice that this model is a best-effort.
+
+      @return [None] if the model generation is not enabled or the
+      environment is unsatisfiable. *)
 
-  (** [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_unknown_reason t] returns the reason Alt-Ergo raised
+      [I_dont_know] if it did. If it did not, returns [None]. *)
 
+  val get_value : t -> Expr.t -> Expr.t 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
 
-  (** [get_objectives t] produces the current objectives. *)
   val get_objectives : t -> Objective.Model.t option
+  (** [get_objectives t] returns the current objective values.
+
+      @return [None] if there is no objective or the environment is
+      unsatisfiable. *)
 end
 
 

src/lib/reasoners/sat_solver_sig.mli

@@ -39,11 +39,11 @@ type unknown_reason =
   | Step_limit of int
   | Timeout of timeout_reason
 
-(** Prints the unknown reason in the default SMT-LIB format *)
 val pp_smt_unknown_reason: unknown_reason Fmt.t
+(** Prints the unknown reason in the default SMT-LIB format. *)
 
-(** Prints an optional unknown reason in Alt-Ergo format *)
 val pp_ae_unknown_reason_opt : unknown_reason option Fmt.t
+(** Prints an optional unknown reason in Alt-Ergo format. *)
 
 module type S = sig
   type t
@@ -52,61 +52,82 @@ module type S = sig
   exception Unsat of Explanation.t
   exception I_dont_know
 
-  (** the empty sat-solver context *)
-  val empty : unit -> t
-  val empty_with_inst : (Expr.t -> bool) -> t
+  val empty : ?selector:(Expr.t -> bool) -> unit -> t
+  (** [empty ~selector ()] creates an empty environment.
+
+      The optional argument [selector] is used to filter ground facts
+      discovered by the instantiation engine. *)
 
-  (** [push env n] add n new assertion levels.
-      A guard g is added for every expression e assumed at the current
-      assertion level.
-      Ie. assuming e after the push will become g -> e,
-      a g will be forced to be true (but not propagated at level 0) *)
   val push : t -> int -> unit
+  (** [push env n] adds [n] new assertion levels in [env].
+
+      Internally, for each new assertion level, a fresh guard [g] is created
+      and all formulas [f] assumed at this assertion level is replaced by
+      [g ==> f].
+
+      The guard [g] is forced to be [true] but not propagated at level [0]. *)
 
-  (** [pop env n] remove an assertion level.
-      Internally, the guard g introduced in the push correponsding to this pop
-      will be propagated to false (at level 0) *)
   val pop : t -> int -> unit
+  (** [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]. *)
 
-  (** [assume env f] assume a new formula [f] in [env]. Raises Unsat if
-      [f] is unsatisfiable in [env] *)
   val assume : t -> Expr.gformula -> Explanation.t -> unit
+  (** [assume env f dep] assumes the ground formula [f] in [env].
+      The [dep] argument can be used to generate an unsat core.
+
+      @raise Unsat if [f] is unsatisfiable in [env]. *)
 
-  (** [assume env f exp] assume a new formula [f] with the explanation [exp]
-      in the theories environment of [env]. *)
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
+  (** [assume env f exp] assumes a new formula [f] with the explanation [exp]
+      in the theory environment of [env]. *)
 
-  (** [pred_def env f] assume a new predicate definition [f] in [env]. *)
   val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> unit
+  (** [pred_def env f] assumes a new predicate definition [f] in [env]. *)
 
-  (** [optimize env ~is_max o] registers the expression [o]
-      as an objective function. *)
   val optimize : t -> is_max:bool -> Expr.t -> unit
+  (** [optimize env ~is_max o] registers the expression [o] as an objective
+      function.
+
+      The solver will try to maximize [o] if [is_max] is [true]. Otherwise,
+      it will try to minimize it.
+
+      After optimization, the value of this objective is returned by
+      [get_objectives]. *)
 
-  (** [unsat env f size] checks the unsatisfiability of [f] in
-      [env]. Raises I_dont_know when the proof tree's height reaches
-      [size]. Raises Sat if [f] is satisfiable in [env] *)
   val unsat : t -> Expr.gformula -> Explanation.t
+  (** [unsat env f] checks the unsatisfiability of [f] in [env].
+
+      @raise I_dont_know if the solver cannot prove the unsatisfiability
+             of [env].
+      @raise Sat if [f] is satisfiable in [env]. *)
 
-  (** [print_model header fmt env] print propositional model and theory model
-      on the corresponding fmt. *)
   val reset_refs : unit -> unit
 
-  (** [reinit_ctx ()] reinitializes the solving context. *)
   val reinit_ctx : unit -> unit
+  (** [reinit_ctx ()] reinitializes the solving context. *)
 
-  (** [get_model t] produces the current model. *)
   val get_model: t -> Models.t option
+  (** [get_model t] produces the current first-order model.
+      Notice that this model is a best-effort.
+
+      @return [None] if the model generation is not enabled or the
+      environment is unsatisfiable. *)
 
-  (** [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_unknown_reason t] returns the reason Alt-Ergo raised
+      [I_dont_know] if it did. If it did not, returns [None]. *)
 
+  val get_value : t -> Expr.t -> Expr.t 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
 
   val get_objectives : t -> Objective.Model.t option
+  (** [get_objectives t] returns the current objective values.
+
+      @return [None] if there is no objective or the environment is
+      unsatisfiable. *)
 end
 
 

src/lib/reasoners/satml_frontend.ml

@@ -79,7 +79,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Stack.push Expr.vrai guards.stack_guard;
     guards
 
-  let empty () =
+  let empty ?(selector=fun _ -> true) () =
     { gamma = ME.empty;
       satml = SAT.empty ();
       ff_hcons_env = FF.empty_hcons_env ();
@@ -93,15 +93,12 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       inst = Inst.empty;
       skolems = ME.empty;
       guards = init_guards ();
-      add_inst = (fun _ -> true);
+      add_inst = selector;
       last_saved_model = None;
       last_saved_objectives = None;
       unknown_reason = None;
     }
 
-  let empty_with_inst add_inst =
-    { (empty ()) with add_inst = add_inst }
-
   exception Sat
   exception Unsat of Explanation.t
   exception I_dont_know