From 1cd1fbe070f7000195b1fa59b004150d80368702 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 3 Jan 2024 10:51:49 +0100 Subject: [PATCH] Clean up documentation of the SAT API --- src/bin/js/worker_js.ml | 2 +- src/lib/reasoners/fun_sat.ml | 7 +-- src/lib/reasoners/fun_sat.mli | 4 +- src/lib/reasoners/fun_sat_frontend.ml | 4 +- src/lib/reasoners/sat_solver_sig.ml | 72 ++++++++++++++++--------- src/lib/reasoners/sat_solver_sig.mli | 77 ++++++++++++++++----------- src/lib/reasoners/satml_frontend.ml | 7 +-- 7 files changed, 100 insertions(+), 73 deletions(-) diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index c2ac73feb..931c45c1f 100644 --- a/src/bin/js/worker_js.ml +++ b/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) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 879645be9..d943a0045 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/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,7 +1834,7 @@ 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; } @@ -1842,9 +1842,6 @@ module Make (Th : Theory.S) = struct 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} diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index ca5382fe6..1e9ba0719 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/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 diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index bad7812b0..789854334 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/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 diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 24c2f1f3b..81b102b2f 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -72,58 +72,78 @@ 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. + + 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 size] checks the unsatisfiability of [f] in [env]. + + @raise I_dont_know when the proof tree's height reaches [size]. + @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 diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 72b361905..dc0c88812 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/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,78 @@ 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. + + 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 size] checks the unsatisfiability of [f] in [env]. + + @raise I_dont_know when the proof tree's height reaches [size]. + @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 diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 678d855e1..6547ddde6 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/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