From fea288be807e4529152192ad814e4e74b5972438 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 25 Sep 2023 14:08:32 +0200 Subject: [PATCH 1/4] Support of get-info SMT2 command --- src/bin/common/solving_loop.ml | 55 ++++++++++++++++++- src/lib/frontend/frontend.ml | 42 ++++++++------ src/lib/frontend/frontend.mli | 2 + src/lib/reasoners/fun_sat.ml | 39 +++++-------- src/lib/reasoners/sat_solver_sig.ml | 24 +++++--- src/lib/reasoners/sat_solver_sig.mli | 21 ++++--- src/lib/reasoners/satml_frontend.ml | 32 ++++++----- src/lib/util/printer.mli | 6 +- tests/dune.inc | 22 ++++++++ ...estfile-smt-instr-get-info.dolmen.expected | 11 ++++ .../testfile-smt-instr-get-info.dolmen.smt2 | 17 ++++++ 11 files changed, 197 insertions(+), 74 deletions(-) create mode 100644 tests/everything/testfile-smt-instr-get-info.dolmen.expected create mode 100644 tests/everything/testfile-smt-instr-get-info.dolmen.smt2 diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 22afb5053..e28f6e33f 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -50,6 +50,9 @@ let empty_solver_ctx = { global = []; } +let unsupported_opt () = + Printer.print_std "unsupported" + let main () = let () = Dolmen_loop.Code.init [] in @@ -399,8 +402,52 @@ let main () = | ":produce-unsat-assumptions" | ":print-success" | ":random-seed"), _ - -> Printer.print_wrn "unsupported option %s" name - | _ -> Printer.print_wrn "unsupported option %s" name + -> + unsupported_opt (); + Printer.print_wrn "unsupported option '%s'" name + | _ -> + unsupported_opt (); + Printer.print_err "unknown option '%s'" name + in + + let handle_get_info (st : State.t) (name: string) = + let print_std = + fun (type a) (pp :a Fmt.t) (a : a) -> + Printer.print_std "(%s %a)" name pp a + in + let pp_reason_unknown st = + let err () = + let msg = "Invalid (get-info :reason-unknown)" in + Printer.print_smtlib_err "%s" msg + in + match State.get partial_model_key st with + | None -> err () + | Some sat -> + match SAT.get_unknown_reason sat with + | None -> err () + | Some s -> + print_std + Format.pp_print_string + (Frontend.unknown_reason_to_string s) + in + match name with + | ":authors" -> + print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo developers" + | ":error-behavior" -> + print_std Fmt.string "immediate-exit" + | ":name" -> + print_std (fun fmt -> Fmt.pf fmt "%S") "Alt-Ergo" + | ":reason-unknown" -> + pp_reason_unknown st + | ":version" -> + print_std Fmt.string Version._version + | ":all-statistics" + | ":assertion-stack-levels" -> + unsupported_opt (); + Printer.print_wrn "unsupported option '%s'" name + | _ -> + unsupported_opt (); + Printer.print_err "unknown option '%s'" name in let handle_stmt : @@ -504,6 +551,10 @@ let main () = st end + | {contents = `Get_info kind; _ } -> + handle_get_info st kind; + st + | _ -> (* TODO: - Separate statements that should be ignored from unsupported diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 8de0f2c4d..1e2e07f5c 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -32,6 +32,21 @@ open Commands open Format open Options +let timeout_reason_to_string = function + | Sat_solver_sig.Assume -> "Assume" + | ProofSearch -> "ProofSearch" + | ModelGen -> "ModelGen" + +let unknown_reason_to_string = function + | Sat_solver_sig.Incomplete -> "Incomplete" + | Memout -> "Memout" + | Timeout t -> Format.sprintf "Timeout:%s" (timeout_reason_to_string t) + +let unknown_reason_opt_to_string = + function + | None -> "Decided" + | Some r -> unknown_reason_to_string r + module E = Expr module Ex = Explanation module type S = sig @@ -154,27 +169,20 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if Options.get_unsat_core () then Ex.singleton (Ex.RootDep {name;f;loc}) else Ex.empty - let timeout_reason_to_string = function - | None -> "(?)" - | Some SAT.NoTimeout -> "NoTimeout" - | Some SAT.Assume -> "Assume" - | Some SAT.ProofSearch -> "ProofSearch" - | Some SAT.ModelGen -> "ModelGen" - - let print_model env timeout = + let print_model env unknown_reason_opt = if Options.(get_interpretation () && get_dump_models ()) then begin - let s = timeout_reason_to_string timeout in + let s = unknown_reason_opt_to_string unknown_reason_opt in match SAT.get_model env with | None -> Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) "@[It seems that no model has been computed so \ far. You may need to change your model generation strategy \ - or to increase your timeouts. Returned timeout reason = %s@]" s + or to increase your timeouts. Returned unknown reason = %s@]" s | Some (lazy model) -> Printer.print_fmt (Options.Output.get_fmt_diagnostic ()) - "@[; Returned timeout reason = %s@]" s; + "@[; Returned unknown reason = %s@]" s; Models.output_concrete_model (Options.Output.get_fmt_models ()) model end @@ -270,7 +278,7 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct (* This case should mainly occur when a query has a non-unsat result, so we want to print the status in this case. *) print_status (Sat (d,t)) (Steps.get_steps ()); - print_model env (Some SAT.NoTimeout); + print_model env None; env, `Sat t, dep | SAT.Unsat dep' -> (* This case should mainly occur when a new assumption results in an unsat @@ -280,14 +288,16 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct if get_debug_unsat_core () then check_produced_unsat_core dep; (* print_status (Inconsistent d) (Steps.get_steps ()); *) env , `Unsat, dep - | SAT.I_dont_know {env = t; timeout} -> + | SAT.I_dont_know t -> (* TODO: always print Unknown for why3 ? *) + let ur = SAT.get_unknown_reason t in let status = - if timeout != NoTimeout then (Timeout (Some d)) - else (Unknown (d, t)) + match ur with + | Some (Sat_solver_sig.Timeout _) -> Timeout (Some d) + | _ -> Unknown (d, t) in print_status status (Steps.get_steps ()); - print_model t (Some timeout); + print_model t ur; (* TODO: Is it an appropriate behaviour? *) (* if timeout != NoTimeout then raise Util.Timeout; *) env, `Unknown t, dep diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index cbdbd3bd1..768d21833 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -63,3 +63,5 @@ module type S = sig end module Make (SAT: Sat_solver_sig.S) : S with type sat_env = SAT.t + +val unknown_reason_to_string : Sat_solver_sig.unknown_reason -> string diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 19ad29cb2..b8da8fdf8 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -176,6 +176,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct add_inst: E.t -> bool; unit_facts_cache : (E.gformula * Ex.t) ME.t ref; last_saved_model : Models.t Lazy.t option ref; + unknown_reason : Sat_solver_sig.unknown_reason option; } let reset_refs () = @@ -192,25 +193,13 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct { env with unit_facts_cache = ref refs.unit_facts}, guard - (* Specify the pass in which Alt-Ergo runs out of time. This information - is used to decide if the last produced model is relevant. *) - type timeout_reason = - | NoTimeout - | Assume - (* Timeout while assuming a ground formula. *) - - | ProofSearch - (* Timeout while doing instantiation or backtracking phases - during the proof search. *) - - | ModelGen - (* Timeout while generating a new model. *) - exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of { env : t; timeout : timeout_reason } + exception I_dont_know of t exception IUnsat of Ex.t * SE.t list + let i_dont_know env ur = + raise (I_dont_know {env with unknown_reason = Some ur}) (*BISECT-IGNORE-BEGIN*) module Debug = struct @@ -1144,14 +1133,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct raise (IUnsat (expl, classes)) end - let update_model_and_return_unknown env compute_model ~timeout = + let update_model_and_return_unknown env compute_model ~unknown_reason = try let env = may_update_last_saved_model env compute_model in Options.Time.unset_timeout (); - raise (I_dont_know {env; timeout }) + i_dont_know env unknown_reason with Util.Timeout when !(env.model_gen_phase) -> (* In this case, timeout reason becomes 'ModelGen' *) - raise (I_dont_know {env; timeout = ModelGen }) + i_dont_know env (Timeout ModelGen) let model_gen_on_timeout env = let i = Options.get_interpretation () in @@ -1160,7 +1149,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct !(env.model_gen_phase) || (* we timeouted in model-gen-phase *) Stdlib.(=) ti 0. (* no time allocated for extra model search *) then - raise (I_dont_know {env; timeout = ProofSearch}) + i_dont_know env (Timeout ProofSearch) else begin (* Beware: models generated on timeout of ProofSearch phase may @@ -1170,7 +1159,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Options.Time.unset_timeout (); Options.Time.set_timeout ti; update_model_and_return_unknown - env i ~timeout:ProofSearch (* may becomes ModelGen *) + env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *) end let reduce_hypotheses tcp_cache tmp_cache env acc (hyp, gf, dep) = @@ -1286,7 +1275,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct this returns a wrong model. *) update_model_and_return_unknown env (Options.get_last_interpretation ()) - ~timeout:NoTimeout (* may becomes ModelGen *) + ~unknown_reason:Incomplete (* may becomes ModelGen *) | IAuto | IGreedy -> let gre_inst = ME.fold @@ -1314,7 +1303,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct else update_model_and_return_unknown env (Options.get_last_interpretation ()) - ~timeout:NoTimeout (* may becomes ModelGen *) + ~unknown_reason:Incomplete (* may becomes ModelGen *) let normal_instantiation env try_greedy = Debug.print_nb_related env; @@ -1763,8 +1752,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Util.Timeout -> (* don't attempt to compute a model if timeout before calling unsat function *) - raise (I_dont_know {env; timeout = Assume}) - + i_dont_know env (Timeout Assume) let pred_def env f name dep _loc = Debug.pred_def f; @@ -1842,6 +1830,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct guards = init_guards (); add_inst = (fun _ -> true); last_saved_model = ref None; + unknown_reason = None; } in assume env gf_true Ex.empty @@ -1856,6 +1845,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct (** returns the latest model stored in the env if any *) let get_model env = !(env.last_saved_model) + let get_unknown_reason env = env.unknown_reason + let reinit_ctx () = (* all_models_sat_env := None; *) (* latest_saved_env := None; diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 0c10a0d49..28da86b4c 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -31,18 +31,25 @@ (* We put an ml file for the module type, to avoid issues when building the lib *) +type timeout_reason = + | Assume + | ProofSearch + | ModelGen + +type unknown_reason = + | Incomplete + | Memout + | Timeout of timeout_reason + +(* TODO: use an ADT and add Timeout when library starts acting like a + library. *) + module type S = sig type t - type timeout_reason = - | NoTimeout - | Assume - | ProofSearch - | ModelGen - exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of { env : t; timeout : timeout_reason } + exception I_dont_know of t (* the empty sat-solver context *) val empty : unit -> t @@ -82,6 +89,9 @@ module type S = sig (** [get_model t] produces the current model. *) val get_model: t -> Models.t Lazy.t 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_unknown_reason : t -> unknown_reason option end diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index 611b6034d..53282e144 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -28,18 +28,22 @@ (* *) (**************************************************************************) +type timeout_reason = + | Assume + | ProofSearch + | ModelGen + +type unknown_reason = + | Incomplete + | Memout + | Timeout of timeout_reason + module type S = sig type t - type timeout_reason = - | NoTimeout - | Assume - | ProofSearch - | ModelGen - exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of { env : t; timeout : timeout_reason } + exception I_dont_know of t (** the empty sat-solver context *) val empty : unit -> t @@ -83,6 +87,9 @@ module type S = sig (** [get_model t] produces the current model. *) val get_model: t -> Models.t Lazy.t 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_unknown_reason : t -> unknown_reason option end diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 9348554f8..499551a13 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -62,6 +62,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct guards : guards; last_saved_model : Models.t Lazy.t option ref; model_gen_phase : bool ref; + unknown_reason : Sat_solver_sig.unknown_reason option; + (** The reason why satml raised [I_dont_know] if it does; [None] by + default. *) } let empty_guards () = { @@ -91,20 +94,18 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct add_inst = (fun _ -> true); last_saved_model = ref None; model_gen_phase = ref false; + unknown_reason = None; } let empty_with_inst add_inst = { (empty ()) with add_inst = add_inst } - type timeout_reason = - | NoTimeout - | Assume - | ProofSearch - | ModelGen - exception Sat of t exception Unsat of Explanation.t - exception I_dont_know of { env : t; timeout : timeout_reason } + exception I_dont_know of t + + let i_dont_know env ur = + raise (I_dont_know {env with unknown_reason = Some ur}) exception IUnsat of t * Explanation.t @@ -1005,15 +1006,14 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct end - let update_model_and_return_unknown env compute_model ~timeout = + let update_model_and_return_unknown env compute_model ~unknown_reason = try let env = may_update_last_saved_model env compute_model in Options.Time.unset_timeout (); - raise (I_dont_know {env; timeout }) + i_dont_know env unknown_reason with Util.Timeout when !(env.model_gen_phase) -> (* In this case, timeout reason becomes 'ModelGen' *) - raise (I_dont_know {env; timeout = ModelGen }) - + i_dont_know env (Timeout ModelGen) let model_gen_on_timeout env = let i = Options.get_interpretation () in @@ -1022,7 +1022,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct !(env.model_gen_phase) || (* we timeouted in model-gen-phase *) Stdlib.(=) ti 0. (* no time allocated for extra model search *) then - raise (I_dont_know {env; timeout = ProofSearch}) + i_dont_know env (Timeout ProofSearch) else begin (* Beware: models generated on timeout of ProofSearch phase may @@ -1032,7 +1032,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct Options.Time.unset_timeout (); Options.Time.set_timeout ti; update_model_and_return_unknown - env i ~timeout:ProofSearch (* may becomes ModelGen *) + env i ~unknown_reason:(Timeout ProofSearch) (* may becomes ModelGen *) end let rec unsat_rec env ~first_call:_ : unit = @@ -1079,7 +1079,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct if not updated then update_model_and_return_unknown env (Options.get_last_interpretation ()) - ~timeout:NoTimeout; (* may becomes ModelGen *) + ~unknown_reason:Incomplete; (* may becomes ModelGen *) unsat_rec env ~first_call:false with @@ -1214,7 +1214,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct | Util.Timeout -> (* don't attempt to compute a model if timeout before calling unsat function *) - raise (I_dont_know {env; timeout = Assume}) + i_dont_know env (Timeout Assume) (* instrumentation of relevant exported functions for profiling *) let assume t ff dep = @@ -1247,6 +1247,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct let get_model env = !(env.last_saved_model) + let get_unknown_reason env = env.unknown_reason + let reinit_ctx () = Steps.reinit_steps (); Th.reinit_cpt (); diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index 95bd65c02..fcb58d750 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -175,9 +175,9 @@ val print_status_preprocess : float option -> int option -> unit -(** Print smtlib error message on the error formatter accessible with - {!val:Options.get_fmt_err} and set by default to stderr. - The err formatter is flushed after the print if flushed is set *) +(** Print smtlib error message on the regular formatter, accessible with + {!val:Options.get_fmt_regular} and set by default to stdout. + The regular formatter is flushed after the print if flushed is set. *) val print_smtlib_err : ?flushed:bool -> ('a, Format.formatter, unit) format -> 'a diff --git a/tests/dune.inc b/tests/dune.inc index 1413e9191..ee4679110 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -155091,6 +155091,28 @@ (package alt-ergo) (action (diff testfile-tab001.expected testfile-tab001_fpa.output))) + (rule + (target testfile-smt-instr-get-info.dolmen_dolmen.output) + (deps (:input testfile-smt-instr-get-info.dolmen.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff + testfile-smt-instr-get-info.dolmen.expected + testfile-smt-instr-get-info.dolmen_dolmen.output))) (rule (target testfile-predicate002_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-predicate002.ae)) diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.expected b/tests/everything/testfile-smt-instr-get-info.dolmen.expected new file mode 100644 index 000000000..5aa61ed6b --- /dev/null +++ b/tests/everything/testfile-smt-instr-get-info.dolmen.expected @@ -0,0 +1,11 @@ +(error "Invalid (get-info :reason-unknown)") + +unknown +(:all-statistics unsupported) +(:assertion-stack-levels unsupported) +(:authors "Alt-Ergo developers") +(:error-behavior immediate-exit) +(:name "Alt-Ergo") +(:reason-unknown incomplete) +(:version dev) +(error "unknown option ':foo'") diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 b/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 new file mode 100644 index 000000000..4fd233ce5 --- /dev/null +++ b/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 @@ -0,0 +1,17 @@ +(set-logic ALL) + +(declare-const x Int) +(declare-const y Int) + +(assert (= (* x x) 4)) + +(get-info :reason-unknown) +(check-sat) +(get-info :all-statistics) +(get-info :assertion-stack-levels) +(get-info :authors) +(get-info :error-behavior) +(get-info :name) +(get-info :reason-unknown) +(get-info :version) +(get-info :foo) \ No newline at end of file From 52532f4c09a481f941800387c965d09f914f5565 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Sep 2023 11:44:39 +0200 Subject: [PATCH 2/4] Update tests --- tests/dune.inc | 11 +++++------ .../testfile-smt-instr-get-info.dolmen.expected | 10 ++++++---- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/tests/dune.inc b/tests/dune.inc index ee4679110..a3a299604 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -155107,12 +155107,11 @@ --frontend dolmen %{input}))))))) (rule - (alias runtest-quick) - (package alt-ergo) - (action - (diff - testfile-smt-instr-get-info.dolmen.expected - testfile-smt-instr-get-info.dolmen_dolmen.output))) + (deps testfile-smt-instr-get-info.dolmen_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-smt-instr-get-info.dolmen.expected testfile-smt-instr-get-info.dolmen_dolmen.output))) (rule (target testfile-predicate002_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-predicate002.ae)) diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.expected b/tests/everything/testfile-smt-instr-get-info.dolmen.expected index 5aa61ed6b..d3e05dee0 100644 --- a/tests/everything/testfile-smt-instr-get-info.dolmen.expected +++ b/tests/everything/testfile-smt-instr-get-info.dolmen.expected @@ -1,11 +1,13 @@ (error "Invalid (get-info :reason-unknown)") unknown -(:all-statistics unsupported) -(:assertion-stack-levels unsupported) +unsupported + +unsupported + (:authors "Alt-Ergo developers") (:error-behavior immediate-exit) (:name "Alt-Ergo") -(:reason-unknown incomplete) +(:reason-unknown Incomplete) (:version dev) -(error "unknown option ':foo'") +unsupported From 2c2b300302f575ff881a1733cbe1430b887e2f68 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Sep 2023 11:49:32 +0200 Subject: [PATCH 3/4] Format --- src/lib/reasoners/satml_frontend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 499551a13..74cceb381 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -104,7 +104,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct exception Unsat of Explanation.t exception I_dont_know of t - let i_dont_know env ur = + let i_dont_know env ur = raise (I_dont_know {env with unknown_reason = Some ur}) exception IUnsat of t * Explanation.t From 96e04dfdc51d648a5f99078601bc390266865171 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 2 Oct 2023 14:40:41 +0200 Subject: [PATCH 4/4] Removing comment --- src/lib/reasoners/sat_solver_sig.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 28da86b4c..f53c0ab22 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -41,9 +41,6 @@ type unknown_reason = | Memout | Timeout of timeout_reason -(* TODO: use an ADT and add Timeout when library starts acting like a - library. *) - module type S = sig type t