Poetry

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

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,15 +1288,15 @@ 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 "@[<v 2>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)
 
 
   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
         "@[<v 2>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)

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] *)
 

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.

tests/adts/simple_1.expected

@@ -20,3 +20,5 @@ unsat
 unsat
 
 unsat
+
+unsat