let const_of_smtlib_atom b t = let res = (* Empty strings are invalid *) if HString.length t = 0 then (* String is empty *) raise (Invalid_argument "num_expr_of_smtlib_token") else try (* Return numeral of string *) Term.mk_num (Numeral.of_string (HString.string_of_hstring t)) (* String is not a decimal *) with Invalid_argument _ -> try (* Return decimal of string *) Term.mk_dec (Decimal.of_string (HString.string_of_hstring t)) with Invalid_argument _ -> try (* Return decimal of string *) Term.mk_dec (Decimal.of_num (Num.num_of_string (HString.string_of_hstring t))) with Invalid_argument _ | Failure _ -> (* try (* Return bitvector of string *) Term.mk_bv (bitvector_of_hstring t) with Invalid_argument _ -> *) try (* Return symbol of string *) Term.mk_bool (bool_of_hstring t) (* String is not an interpreted symbol *) with Invalid_argument _ -> try (* Return bound symbol *) Term.mk_var (List.assq t b) (* String is not a bound variable *) with Not_found -> try (* Name of state variable *) let state_var_name = HString.string_of_hstring t in (* State variable of name and given scope *) let state_var = StateVar.state_var_of_long_string state_var_name in (* State variable at instant zero *) let var = Var.mk_state_var_instance state_var Numeral.zero in (* Return term *) Term.mk_var var (* String is not a state variable *) with Not_found -> try (* Return uninterpreted constant *) Term.mk_uf (UfSymbol.uf_symbol_of_string (HString.string_of_hstring t)) [] with Not_found -> Debug.smtexpr "const_of_smtlib_token %s failed" (HString.string_of_hstring t); (* Cannot convert to an expression *) (* raise Not_found *) failwith "Invalid constant symbol in S-expression" in Debug.smtexpr "const_of_smtlib_token %s is %a" (HString.string_of_hstring t) pp_print_term res; res