[Solver] WIP: simplify context and internal error handling

astral/main.ml

@@ -2,7 +2,7 @@
  *
  * Author: Tomas Dacik (idacik@fit.vut.cz), 2021 *)
 
-let () =
+let run () =
   Astral.Profiler.add "Start";
   let input_file = Astral.Options.parse () in
   Astral.Debug.init (); (* Debug initialisation needs to be called after options' parsing *)
@@ -21,3 +21,10 @@ let () =
 
   Reporter.report result;
   Checker.check result
+
+let () =
+  try run ()
+  with
+    | Astral.Exceptions.InternalError (reason, details) ->
+      Astral.Exceptions.pretty_internal_error reason details
+    | Astral.Exceptions.CmdOptionError _ -> ()

src/solver/Exceptions.ml

@@ -0,0 +1,30 @@
+(* Representation of internal exceptions used by solver.
+ *
+ * Author: Tomas Dacik (idacik00@fit.vut.cz), 2025 *)
+
+exception UnknownResult of string * string
+
+exception UnsupportedFragment of string * string
+
+exception CmdOptionError of string
+
+exception InternalError of string * string
+
+let unsupported_fragment ~reason ?(details="") =
+  raise @@ UnsupportedFragment (reason, details)
+
+let unknown_result ~reason ?(details="") =
+  raise @@ UnknownResult (reason, details)
+
+let internal_error ~reason ?(details="") =
+  raise @@ InternalError (reason, details)
+
+
+(** Pretty printers *)
+let pretty_internal_error reason details =
+  Format.eprintf "%s[Internal error]%s %s\n" Colors.red Colors.white reason;
+  (*if backtrace then begin
+    Format.eprintf "\nBacktrace:\n%s"
+      (Printexc.raw_backtrace_to_string stack)
+  end;*)
+  if true then Format.fprintf Format.err_formatter "\n%s\n" details

src/solver/Exceptions.mli

@@ -0,0 +1,22 @@
+(* Representation of solver's internal error.
+ *
+ * Author: Tomas Dacik (idacik00@fit.vut.cz), 2025 *)
+
+exception UnsupportedFragment of string * string
+(** This exception is raised when unsupported fragment is detected. *)
+
+exception UnknownResult of string * string
+
+exception InternalError of string * string
+(** This exception represents an internal error. It should not
+    be catched inside Astral library. *)
+
+exception CmdOptionError of string
+
+val unknown_result : reason:string -> ?details:string -> _
+
+val unsupported_fragment : reason:string -> ?details:string -> _
+
+val internal_error : reason:string -> ?details:string -> _
+
+val pretty_internal_error : string -> string -> unit

src/solver/context.ml

@@ -34,7 +34,6 @@ type t = {
   status : status option;
   model : StackHeapModel.t option;
   unsat_core : SL.t list option;
-  reason_unknown : string option;
 }
 
 let init input = {
@@ -55,7 +54,6 @@ let init input = {
   status = None;
   model = None;
   unsat_core = None;
-  reason_unknown = None;
 }
 
 let (let*) f ctx = match ctx.status with
@@ -80,12 +78,11 @@ let set_preprocessed input phi vars = {input with phi = phi; vars = vars}
 
 let set_size input size = {input with size = Some size}
 
-let set_result status ?(model=None) ?(unsat_core=None) ?(reason=None) input =
+let set_result status ?model ?unsat_core input =
   {input with
     status = Some status;
     model = model;
     unsat_core = unsat_core;
-    reason_unknown = reason;
   }
 
 

src/solver/engine.ml

@@ -23,15 +23,14 @@ let debug_info input = match SL.classify_fragment input.phi with
   | Positive -> Logger.debug "Solving as positive formula\n"
   | Arbitrary -> Logger.debug "Solving as arbitrary formula\n"
 
-let solve (raw_input : ParserContext.t) =
+let solve (input : Context.t) =
   SID.init ();
-  let input = Context.init raw_input in
   let input = Preprocessor.first_phase input in
   SID.preprocess_user_definitions PredicatePreprocessing.normalise;
 
   let sl_graph = SL_graph.compute input.phi in
   if SL_graph.has_contradiction sl_graph then
-    Context.set_result `Unsat ~unsat_core:(Some []) input
+    Context.set_result `Unsat ~unsat_core:[] input
   else match FragmentChecker.check input with
   | Error reason -> Context.set_result (`Unknown reason) input
   | Ok () ->
@@ -71,4 +70,13 @@ let solve (raw_input : ParserContext.t) =
       let res' = Context.apply_model_adapter res in
       (match res'.model with None -> () | Some sh -> Debug.model sh);
       res'
-    else Context.set_result (`Unknown "dry run") ~reason:(Some "dry run") input
+    else Context.set_result (`Unknown "dry run") input
+
+(* TODO: Do not return just input in case of exception. *)
+let solve input =
+  let ctx = Context.init input in
+  try solve ctx with
+  | Exceptions.UnknownResult (reason, _) ->
+    Context.set_result (`Unknown reason) ctx
+  | Exceptions.UnsupportedFragment (reason, _) ->
+    Context.set_result (`Unknown ("Unsupported fragment" ^ reason)) ctx

src/translation/location_encoding/LocationBuilder.ml

@@ -27,9 +27,9 @@ module Make (Locations : LOCATIONS_BASE) = struct
     | Some (_, mapper) -> SMT.Array.mk_select mapper locs.null
     | None ->*) locs.null
 
-  let internal_error self msg_prefix =
-    let msg = Format.asprintf "%s in location encoding:\n%s" msg_prefix (show self)
-    in Utils.internal_error msg
+  let internal_error self reason =
+    let details = Format.asprintf "Location encoding:\n%s" (show self) in
+    Exceptions.internal_error ~reason ~details
 
   let get_encoding locs sort =
     try Sort.Map.find sort locs.sort_encoding

src/translation/translation.ml

@@ -353,7 +353,7 @@ module Make (Encoding : Translation_sig.ENCODING) (Backend : Backend_sig.BACKEND
 
     if ctx.can_skolemise
     then translate_septraction_skolemised ctx domain witness_heap phi psi1 psi2
-    else raise @@ SolverUtils.UnsupportedFragment "magic wand/negative septraction"
+    else Exceptions.unsupported_fragment ~reason:"magic wand/negative septraction" ~details:""
 
   and translate_septraction_skolemised ctx domain witness_heap phi psi1 psi2 =
     let fp1 = formula_footprint ctx psi1 in
@@ -668,18 +668,19 @@ let translate_phi (ctx : Context.t) ssl_phi =
     | SMT_Sat (Some (smt_model, backend_model)) ->
       let smt_model = SetEncoding.rewrite_back translated1 smt_model in
       let _ = Debug.smt_model smt_model in
-      let sh = translate_model ctx smt_model in
-      Input.set_result `Sat ~model:(Some sh) input
+      let model = translate_model ctx smt_model in
+      Input.set_result `Sat ~model input
 
     (* TODO: unsat cores *)
-    | SMT_Unsat unsat_core -> Input.set_result `Unsat ~unsat_core:(Some []) input
+    | SMT_Unsat unsat_core -> Input.set_result `Unsat ~unsat_core:[] input
 
     (* TODO: remove duplicit reason *)
-    | SMT_Unknown reason -> Input.set_result (`Unknown reason) ~reason:(Some reason) input
+    | SMT_Unknown reason -> Input.set_result (`Unknown reason) input
 
-  let solve input =
+  (*let solve input =
     try solve input
     with SolverUtils.UnsupportedFragment str ->
       let reason = "unsupported SL fragment: " ^ str in
       Input.set_result (`Unknown reason) ~reason:(Some reason) input
+  *)
 end