let gen_expr_of_string_sexpr' ({ s_let; s_forall; s_exists; s_div; s_minus; prime_symbol; const_of_atom; symbol_of_atom; expr_of_string_sexpr; expr_or_lambda_of_string_sexpr } as conv) bound_vars = function (* An empty list *) | HStringSExpr.List [] -> (* Cannot convert to an expression *) failwith "Invalid Nil in S-expression" (* An list with a list as first element *) | HStringSExpr.List (HStringSExpr.List _ :: _) -> (* Cannot convert to an expression *) failwith "Invalid S-expression" (* A singleton list: treat as atom *) | HStringSExpr.List [e] -> expr_of_string_sexpr conv bound_vars e (* A let binding *) | HStringSExpr.List ((HStringSExpr.Atom s) :: [HStringSExpr.List v; t]) when s == s_let -> (* Convert bindings and obtain a list of bound variables *) let bindings = gen_bindings_of_string_sexpr conv bound_vars [] v in (* Convert bindings to an association list from strings to variables *) let bound_vars' = List.map (function (v, _) -> (Var.hstring_of_free_var v, v)) bindings in (* Parse the subterm, giving an association list of bound variables and return a let bound term *) Term.mk_let bindings (expr_of_string_sexpr conv (bound_vars @ bound_vars') t) (* A universal or existential quantifier *) | HStringSExpr.List ((HStringSExpr.Atom s) :: [HStringSExpr.List v; t]) when s == s_forall || s == s_exists -> (* Get list of variables bound by the quantifier *) let quantified_vars = gen_bound_vars_of_string_sexpr conv bound_vars [] v in (* Convert bindings to an association list from strings to variables *) let bound_vars' = List.map (function v -> (Var.hstring_of_free_var v, v)) quantified_vars in (* Parse the subterm, giving an association list of bound variables and return a universally or existenially quantified term *) (if s == s_forall then Term.mk_forall else if s == s_exists then Term.mk_exists else assert false) quantified_vars (expr_of_string_sexpr conv (bound_vars @ bound_vars') t) (* Parse (/ n d) as rational constant *) | HStringSExpr.List [HStringSExpr.Atom s; HStringSExpr.Atom n; HStringSExpr.Atom d] when s == s_div && (try let _ = Numeral.of_string (HString.string_of_hstring n) in true with _ -> false) && (try let _ = Numeral.of_string (HString.string_of_hstring d) in true with _ -> false) -> Term.mk_dec Decimal. ((HString.string_of_hstring n |> of_string) / (HString.string_of_hstring d |> of_string)) (* Parse (/ (- n) d) as rational constant *) | HStringSExpr.List [HStringSExpr.Atom s2; HStringSExpr.List [HStringSExpr.Atom s1; HStringSExpr.Atom n]; HStringSExpr.Atom d] when s1 == s_minus && s2 == s_div && (try let _ = Numeral.of_string (HString.string_of_hstring n) in true with _ -> false) && (try let _ = Numeral.of_string (HString.string_of_hstring d) in true with _ -> false) -> Term.mk_dec Decimal. (- (HString.string_of_hstring n |> of_string) / (HString.string_of_hstring d |> of_string)) (* Atom *) | HStringSExpr.Atom s -> (* Leaf in the symbol tree *) (const_of_atom bound_vars s) (* Prime symbol if it exists *) | HStringSExpr.List [HStringSExpr.Atom s; e] when (match prime_symbol with | None -> false | Some s' -> s == s') -> expr_of_string_sexpr conv bound_vars e |> Term.bump_state Numeral.one (* A list with more than one element *) | HStringSExpr.List ((HStringSExpr.Atom h) :: tl) -> ( (* Symbol from string *) let s = try (* Map the string to an interpreted function symbol *) symbol_of_atom h with (* Function symbol is uninterpreted *) | Not_found -> (* Uninterpreted symbol from string *) let u = try UfSymbol.uf_symbol_of_string (HString.string_of_hstring h) with Not_found -> (* Cannot convert to an expression *) failwith (Format.sprintf "Undeclared uninterpreted function symbol %s in S-expression" (HString.string_of_hstring h)) in (* Get the uninterpreted symbol of the string *) Symbol.mk_symbol (`UF u) in (* parse arguments *) let args = List.map (expr_of_string_sexpr conv bound_vars) tl in (* Add correct type to select *) let s = match Symbol.node_of_symbol s, args with | `SELECT _, [a; _] -> Symbol.mk_symbol (`SELECT (Term.type_of_term a)) | _ -> s in (* Create an application of the function symbol to the subterms *) let t = Term.mk_app s args in (* Convert (= 0 (mod t n)) to (t divisible n) *) Term.mod_to_divisible t (* |> Term.reinterpret_select *) )