From cfbc8bc31255932d53dc219cfd9737a4cef25218 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 28 Mar 2024 11:07:04 +0100 Subject: [PATCH] Poetry --- src/bin/common/solving_loop.ml | 23 +++++++++-------------- src/lib/reasoners/satml.ml | 11 ++++++----- src/lib/util/options.mli | 4 ++-- tests/adts/simple_1.ae | 3 +-- tests/adts/simple_1.expected | 2 ++ 5 files changed, 20 insertions(+), 23 deletions(-) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index cfb963a95..ed30e32c3 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -431,21 +431,16 @@ let main () = (* Before each query, we push the current environment. This allows to keep a fresh one for the next assertions. *) - let internal_push st = - if State.get is_decision_env st then - (* We already performed a check-sat *) - st - else - begin - let module Api = (val (DO.SatSolverModule.get st)) in - Api.FE.push 1 Api.env; - State.set is_decision_env true st - end + let push_before_query st = + assert (not (State.get is_decision_env st)); + let module Api = (val (DO.SatSolverModule.get st)) in + Api.FE.push 1 Api.env; + State.set is_decision_env true st in (* The pop corresponding to the previous push. It is applied everytime the mode goes from Sat/Unsat to Assert. *) - let internal_pop st = + let pop_if_post_query st = if State.get is_decision_env st then begin let module Api = (val (DO.SatSolverModule.get st)) in @@ -641,7 +636,7 @@ let main () = DO.Mode.add_hook (fun _ ~old:_ ~new_ st -> match new_ with - | Assert -> internal_pop st + | Assert -> pop_if_post_query st | _ -> st ) in @@ -1070,12 +1065,12 @@ let main () = the hook on D_state_option.Mode. *) let handle_query st id loc attrs contents = let module Api = (val (DO.SatSolverModule.get st)) in - let st = internal_pop st in + let st = pop_if_post_query st in (* Pushing the environment once. This allows to keep a trace of the old environment in case we want to assert afterwards. The `pop` instruction is handled by the hook on the mode: when we assert anything, we must make sure to go back to `Assert` mode. *) - let st = internal_push st in + let st = push_before_query st in let st_loc = let file_loc = (State.get State.logic_file st).loc in dl_to_ael file_loc loc diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index f6da1af5e..8036729ca 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1039,6 +1039,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct assert (ta.is_true); assert (ta.var.level >= 0); if ta.var.level = 0 then begin + incr nb_f; (ta.lit, Th_util.Other, Ex.empty, 0, env.cpt_current_propagations) :: acc end @@ -1243,11 +1244,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let print_aux fmt hc = Format.fprintf fmt "%a@," Atom.pr_clause hc - let is_unsat env : unit = env.is_unsat <- true + let set_unsat env : unit = env.is_unsat <- true let report_b_unsat env linit = if not (Options.get_unsat_core ()) then begin - is_unsat env; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1287,7 +1288,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let unsat_core = HUC.fold (fun c _ l -> c :: l) uc [] in Printer.print_dbg ~header:false "@[UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - is_unsat env; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) @@ -1295,7 +1296,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct let report_t_unsat env dep = if not (Options.get_unsat_core ()) then begin - is_unsat env; + set_unsat env; env.unsat_core <- None; raise (Unsat None) end @@ -1336,7 +1337,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct Printer.print_dbg ~header:false "@[T-UNSAT_CORE:@ %a@]" (Printer.pp_list_no_space print_aux) unsat_core; - is_unsat env; + set_unsat env; let unsat_core = Some unsat_core in env.unsat_core <- unsat_core; raise (Unsat unsat_core) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index c5cbcd3d7..02998e7d6 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -298,7 +298,7 @@ val set_triggers_var : bool -> unit (** Set [type_smt2] accessible with {!val:get_type_smt2} *) val set_type_smt2 : bool -> unit -(** Set [type_smt2] accessible with {!val:get_type_smt2} *) +(** Set [imperative_mode] accessible with {!val:get_imperative_mode} *) val set_imperative_mode : bool -> unit (** Set [unsat_core] accessible with {!val:get_unsat_core} *) @@ -663,7 +663,7 @@ val get_type_only : unit -> bool val get_type_smt2 : unit -> bool (** Default to [false] *) -(** [true] if the program shall stop after SMT2 typing. *) +(** [true] if the solving loop should work in a pure imperative mode. *) val get_imperative_mode : unit -> bool (** Default to [false] *) diff --git a/tests/adts/simple_1.ae b/tests/adts/simple_1.ae index fa271f926..416c8f617 100644 --- a/tests/adts/simple_1.ae +++ b/tests/adts/simple_1.ae @@ -50,14 +50,13 @@ goal g_valid_4_2: false (* Isse 1008: this goal fail when encapsulated by a push/pop. *) -(* goal g_valid_5_1: forall n : int. n >= 0 -> (* just here for E-matching *) not (e ? A) -> not (e ? B) -> exists x : int[x]. e = C(x) -*) + goal g_valid_5_2: forall n : int. diff --git a/tests/adts/simple_1.expected b/tests/adts/simple_1.expected index f97cc55c7..f8919c465 100644 --- a/tests/adts/simple_1.expected +++ b/tests/adts/simple_1.expected @@ -20,3 +20,5 @@ unsat unsat unsat + +unsat