let gen_expr_or_lambda_of_string_sexpr' ({ s_define_fun; s_declare_fun } as conv) bound_vars = function (* (define-fun c () Bool t) *) | HStringSExpr.List [HStringSExpr.Atom s; (* define-fun *) HStringSExpr.Atom i; (* identifier *) HStringSExpr.List []; (* Parameters *) ty; (* Result type *) t (* Expression *) ] when s == s_define_fun -> (* Register the new symbol with its type if it does not exist *) (try UfSymbol.uf_symbol_of_string (HString.string_of_hstring i) with Not_found -> UfSymbol.mk_uf_symbol (HString.string_of_hstring i) [] (conv.type_of_sexpr ty)) |> ignore; (i, Model.Term (gen_expr_of_string_sexpr' conv bound_vars t)) (* (define-fun A ((x1 Int) (x2 Int)) Bool t) *) | HStringSExpr.List [HStringSExpr.Atom s; (* define-fun *) HStringSExpr.Atom i; (* identifier *) HStringSExpr.List v; (* Parameters *) ty; (* Result type *) t (* Expression *) ] when s == s_define_fun -> (* Get list of variables bound by the quantifier *) let 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)) vars in (* Register the new symbol with its type if it does not exist *) (try UfSymbol.uf_symbol_of_string (HString.string_of_hstring i) with Not_found -> UfSymbol.mk_uf_symbol (HString.string_of_hstring i) (List.map Var.type_of_var vars) (conv.type_of_sexpr ty)) |> ignore; (i, Model.Lambda (Term.mk_lambda vars (gen_expr_of_string_sexpr' conv (bound_vars @ bound_vars') t))) (* delcare-fun f () ty *) | HStringSExpr.List [HStringSExpr.Atom s; (* define-fun *) HStringSExpr.Atom i; (* identifier *) HStringSExpr.List []; (* Parameters *) ty; (* Result type *) ] when s == s_declare_fun -> (* Register the new symbol with its type *) UfSymbol.mk_uf_symbol (HString.string_of_hstring i) [] (conv.type_of_sexpr ty) |> ignore; (* and move on to the next element of the model *) raise Not_found (* (unsupported ... *) | _ -> raise Not_found