Parse smt2 logic correctly

src/ast/ty.ml

@@ -134,9 +134,8 @@ let binop_equal o1 o2 =
   | String_last_index, String_last_index ->
     true
   | ( ( Add | Sub | Mul | Div | DivU | Rem | RemU | Shl | ShrA | ShrL | And | Or
-      | Xor | Pow | Min | Max | Rotl | Rotr | At | List_cons
-      | List_append | String_prefix | String_suffix | String_contains
-      | String_last_index )
+      | Xor | Pow | Min | Max | Rotl | Rotr | At | List_cons | List_append
+      | String_prefix | String_suffix | String_contains | String_last_index )
     , _ ) ->
     false
 
@@ -326,7 +325,7 @@ let pp_binop fmt (op : binop) =
   | Rotl -> Fmt.string fmt "rotl"
   | Rotr -> Fmt.string fmt "rotr"
   | At -> Fmt.string fmt "at"
-  | List_cons-> Fmt.string fmt "cons"
+  | List_cons -> Fmt.string fmt "cons"
   | List_append -> Fmt.string fmt "append"
   | String_prefix -> Fmt.string fmt "prefixof"
   | String_suffix -> Fmt.string fmt "suffixof"
@@ -428,6 +427,37 @@ let pp_logic fmt = function
   | UFLRA -> Fmt.string fmt "UFLRA"
   | UFNIA -> Fmt.string fmt "UFNIA"
 
+let logic_of_string logic =
+  match String.map Char.lowercase_ascii logic with
+  | "ALL" -> Ok ALL
+  | "AUFLIA" -> Ok AUFLIA
+  | "AUFLIRA" -> Ok AUFLIRA
+  | "AUFNIRA" -> Ok AUFNIRA
+  | "LIA" -> Ok LIA
+  | "LRA" -> Ok LRA
+  | "QF_ABV" -> Ok QF_ABV
+  | "QF_AUFBV" -> Ok QF_AUFBV
+  | "QF_AUFLIA" -> Ok QF_AUFLIA
+  | "QF_AX" -> Ok QF_AX
+  | "QF_BV" -> Ok QF_BV
+  | "QF_BVFP" -> Ok QF_BVFP
+  | "QF_IDL" -> Ok QF_IDL
+  | "QF_LIA" -> Ok QF_LIA
+  | "QF_LRA" -> Ok QF_LRA
+  | "QF_NIA" -> Ok QF_NIA
+  | "QF_NRA" -> Ok QF_NRA
+  | "QF_RDL" -> Ok QF_RDL
+  | "QF_S" -> Ok QF_S
+  | "QF_UF" -> Ok QF_UF
+  | "QF_UFBV" -> Ok QF_UFBV
+  | "QF_UFIDL" -> Ok QF_UFIDL
+  | "QF_UFLIA" -> Ok QF_UFLIA
+  | "QF_UFLRA" -> Ok QF_UFLRA
+  | "QF_UFNRA" -> Ok QF_UFNRA
+  | "UFLRA" -> Ok UFLRA
+  | "UFNIA" -> Ok UFNIA
+  | _ -> Error (`Msg (Fmt.str "unknown logic %s" logic))
+
 let discr = function
   | Ty_app -> 0
   | Ty_bool -> 1

src/ast/ty.mli

@@ -162,22 +162,6 @@ type logic =
   | UFLRA
   | UFNIA
 
-val pp_unop : Fmt.formatter -> unop -> unit
-
-val pp_binop : Fmt.formatter -> binop -> unit
-
-val pp_triop : Fmt.formatter -> triop -> unit
-
-val pp_relop : Fmt.formatter -> relop -> unit
-
-val pp_cvtop : Fmt.formatter -> cvtop -> unit
-
-val pp_naryop : Fmt.formatter -> naryop -> unit
-
-val pp : Fmt.formatter -> t -> unit
-
-val pp_logic : Fmt.formatter -> logic -> unit
-
 val compare : t -> t -> int
 
 val unop_equal : unop -> unop -> bool
@@ -194,6 +178,24 @@ val naryop_equal : naryop -> naryop -> bool
 
 val equal : t -> t -> bool
 
+val logic_of_string : string -> (logic, [> `Msg of string]) result
+
+val pp_unop : Fmt.formatter -> unop -> unit
+
+val pp_binop : Fmt.formatter -> binop -> unit
+
+val pp_triop : Fmt.formatter -> triop -> unit
+
+val pp_relop : Fmt.formatter -> relop -> unit
+
+val pp_cvtop : Fmt.formatter -> cvtop -> unit
+
+val pp_naryop : Fmt.formatter -> naryop -> unit
+
+val pp : Fmt.formatter -> t -> unit
+
+val pp_logic : Fmt.formatter -> logic -> unit
+
 val string_of_type : t -> string
 
 val size : t -> int

src/parser/smtlib.ml

@@ -320,10 +320,14 @@ module Statement = struct
 
   let set_option ?loc:_ term = Set_option term
 
-  let set_logic ?loc:_ _logic =
-    (* FIXME: TODO Ty.logic_of_string *)
-    (* Set_logic (Ty.logic_of_string logic) *)
-    Set_logic ALL
+  let set_logic ?loc logic =
+    let logic =
+      Logs.on_error ~level:Logs.Warning
+        ~pp:(fun fmt (`Msg err) -> Fmt.pf fmt "%a%s. Using: ALL" pp_loc loc err)
+        ~use:(fun _ -> Ty.ALL)
+        (Ty.logic_of_string logic)
+    in
+    Set_logic logic
 end
 
 module Extension = struct