Check the status of SatML in Satml_frontend

As explained in the issue #1293,
Satml_frontend does not send to SatML a formula already present in its
lazy cnf. In particular, `assume` and `unsat` of `Satml_frontend` can
answer `unknown` for obviously unsat environment. After this commit, we
always check the status of SatML in `assume` and `unsat`.

If the solver is already unsat, the command `unsat` should return the
unsat core. As SatML does not yet support this feature, I returned an
empty explanation.

src/lib/reasoners/satml.ml

@@ -84,6 +84,9 @@ type conflict_origin =
 (* not even the final one *)
 let vraie_form = E.vrai
 
+type status =
+  | Sat
+  | Unsat of Atom.clause list option
 
 module type SAT_ML = sig
   (*module Make (Dummy : sig end) : sig*)
@@ -141,6 +144,7 @@ module type SAT_ML = sig
 
   val optimize : t -> Objective.Function.t -> unit
 
+  val status : t -> status
 end
 
 module MFF = FF.Map
@@ -2289,4 +2293,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     else
       Vec.replace (fun fns -> fn :: fns) env.objectives
         (Vec.size env.objectives - 1)
+
+  let[@inline always] status env =
+    if env.is_unsat then Unsat env.unsat_core
+    else Sat
 end

src/lib/reasoners/satml.mli

@@ -36,6 +36,10 @@ type conflict_origin =
   | C_bool of Atom.clause
   | C_theory of Explanation.t
 
+type status =
+  | Sat
+  | Unsat of Atom.clause list option
+
 val src : Logs.src
 
 module type SAT_ML = sig
@@ -97,6 +101,10 @@ module type SAT_ML = sig
       [env].
 
       @raise invalid_argurment if the decision level of [env] is not zero. *)
+
+  val status : t -> status
+  (** [unsat env] returns the status of the solver. If the status is [Unsat],
+      the explanation is an unsat core. *)
 end
 
 module Make (Th : Theory.S) : SAT_ML with type th = Th.t

src/lib/reasoners/satml_frontend.ml

@@ -1331,43 +1331,58 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     checks_implemented_features ();
     let gf = add_guard env gf in
     Debug.unsat gf;
-    (*fprintf fmt "FF.unsat@.";*)
-    (* In dfs_sat goals' terms are added to env.inst *)
-    env.inst <-
-      Inst.add_terms env.inst
-        (E.max_ground_terms_rec_of_form gf.E.ff) gf;
-    try
-      assert (SAT.decision_level env.satml == 0);
-      let _updated = assume_aux ~dec_lvl:0 env [gf] in
-      let max_t = max_term_depth_in_sat env in
-      env.inst <- Inst.register_max_term_depth env.inst max_t;
-      unsat_rec_prem env ~first_call:true;
-      assert false
-    with
-    | IUnsat (_env, dep) ->
-      assert begin
-        Ex.fold_atoms
-          (fun e b -> match e with
-             | Ex.Bj _ -> false (* only used in fun_sat *)
-             | Ex.Literal _ | Ex.Fresh _ -> false (* bug if this happens *)
-             | Ex.RootDep _ | Ex.Dep _ -> b
-          )dep true
-      end;
-      dep
+    match SAT.status env.satml with
+    | Unsat _ ->
+      (* XXX: SatML does not yet support unsat core. Instead, an empty
+         explanation is returned. *)
+      Ex.empty
+    | Sat -> (
+        (*fprintf fmt "FF.unsat@.";*)
+        (* In dfs_sat goals' terms are added to env.inst *)
+        env.inst <-
+          Inst.add_terms env.inst
+            (E.max_ground_terms_rec_of_form gf.E.ff) gf;
+        try
+          assert (SAT.decision_level env.satml == 0);
+          let _updated = assume_aux ~dec_lvl:0 env [gf] in
+          let max_t = max_term_depth_in_sat env in
+          env.inst <- Inst.register_max_term_depth env.inst max_t;
+          unsat_rec_prem env ~first_call:true;
+          assert false
+        with
+        | IUnsat (_env, dep) ->
+          assert begin
+            Ex.fold_atoms
+              (fun e b -> match e with
+                 | Ex.Bj _ -> false (* only used in fun_sat *)
+                 | Ex.Literal _ | Ex.Fresh _ -> false (* bug if this happens *)
+                 | Ex.RootDep _ | Ex.Dep _ -> b
+              )dep true
+          end;
+          dep)
 
   let assume env gf _dep =
     (* dep currently not used. No unsat-cores in satML yet *)
     assert (SAT.decision_level env.satml == 0);
-    try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf])
-    with | IUnsat (_env, dep) -> raise (Unsat dep)
-         | Util.Timeout ->
-           (* don't attempt to compute a model if timeout before
-              calling unsat function *)
-           i_dont_know env (Timeout Assume)
-         | Util.Step_limit_reached n ->
-           (* When reaching the step limit on an assume, we do not want to
-              answer 'unknown' right away. *)
-           env.unknown_reason <- Some (Step_limit n)
+    match SAT.status env.satml with
+    | Unsat _ ->
+      (* XXX: SatML does not yet support unsat core. Instead, an empty
+         explanation is returned. *)
+      raise (Unsat Ex.empty)
+    | Sat -> (
+        try
+          let _ : bool = assume_aux ~dec_lvl:0 env [add_guard env gf] in
+          ()
+        with
+        | IUnsat (_env, dep) -> raise (Unsat dep)
+        | Util.Timeout ->
+          (* don't attempt to compute a model if timeout before
+             calling unsat function *)
+          i_dont_know env (Timeout Assume)
+        | Util.Step_limit_reached n ->
+          (* When reaching the step limit on an assume, we do not want to
+             answer 'unknown' right away. *)
+          env.unknown_reason <- Some (Step_limit n))
 
   (* instrumentation of relevant exported functions for profiling *)
   let assume t ff dep =