diff --git a/src/HOL/Tools/SMT/smt_solver.ML b/src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML +++ b/src/HOL/Tools/SMT/smt_solver.ML @@ -1,321 +1,332 @@ (* Title: HOL/Tools/SMT/smt_solver.ML Author: Sascha Boehme, TU Muenchen SMT solvers registry and SMT tactic. *) signature SMT_SOLVER = sig (*configuration*) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, good_slices: ((int * bool * bool * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (*registry*) val add_solver: solver_config -> theory -> theory val good_slices: Proof.context -> string -> ((int * bool * bool * int * string) * string list) list (*filter*) val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> int -> Time.time -> string list -> parsed_proof (*tactic*) val smt_tac: Proof.context -> thm list -> int -> tactic val smt_tac': Proof.context -> thm list -> int -> tactic + + (*solver information*) + type solver_info = { + command: unit -> string list, + smt_options: (string * string) list, + good_slices: ((int * bool * bool * int * string) * string list) list, + parse_proof: Proof.context -> SMT_Translate.replay_data -> + ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> + parsed_proof, + replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm} + val name_and_info_of: Proof.context -> string * solver_info end; structure SMT_Solver: SMT_SOLVER = struct (* interface to external solvers *) local fun make_command command options problem_path proof_path = Bash.strings (command () @ options) ^ " " ^ File.bash_platform_path problem_path ^ " > " ^ File.bash_path proof_path ^ " 2>&1" fun with_trace ctxt msg f x = let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () in f x end fun run ctxt name mk_cmd input = (case SMT_Config.certificates_of ctxt of NONE => if not (SMT_Config.is_available ctxt name) then error ("The SMT solver " ^ quote name ^ " is not installed") else if Config.get ctxt SMT_Config.debug_files = "" then with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input else let val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) val in_path = Path.ext "smt_in" base_path val out_path = Path.ext "smt_out" base_path in Cache_IO.raw_run mk_cmd input in_path out_path end | SOME certs => (case Cache_IO.lookup certs input of (NONE, key) => if Config.get ctxt SMT_Config.read_only_certificates then error ("Bad certificate cache: missing certificate") else Cache_IO.run_and_cache certs key mk_cmd input | (SOME output, _) => with_trace ctxt ("Using cached certificate from " ^ Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output)) (* Z3 and cvc returns 1 if "get-proof" or "get-model" fails. veriT returns 255 in that case and 14 for timeouts. *) fun normal_return_codes "z3" = [0, 1] | normal_return_codes "verit" = [0, 14, 255] | normal_return_codes _ = [0, 1] fun run_solver ctxt name mk_cmd input = let fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines)) val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) = Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val output = drop_suffix (equal "") res val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] val _ = member (op =) (normal_return_codes name) return_code orelse raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in output end fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) = let fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) in SMT_Config.trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "Names:" [ Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () end in fun invoke name command options smt_options ithms ctxt = let val options = options @ SMT_Config.solver_options_of ctxt val comments = [space_implode " " options] val (str, replay_data as {context = ctxt', ...}) = ithms |> tap (trace_assms ctxt) |> SMT_Translate.translate ctxt name smt_options comments ||> tap trace_replay_data in (run_solver ctxt' name (make_command command options) str, replay_data) end end (* configuration *) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, good_slices: ((int * bool * bool * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (* check well-sortedness *) val has_topsort = Term.exists_type (Term.exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)) (* top sorts cause problems with atomization *) fun check_topsort ctxt thm = if has_topsort (Thm.prop_of thm) then (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) else thm (* registry *) type solver_info = { command: unit -> string list, smt_options: (string * string) list, good_slices: ((int * bool * bool * int * string) * string list) list, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm} structure Solvers = Generic_Data ( type T = solver_info Symtab.table val empty = Symtab.empty fun merge data = Symtab.merge (K true) data ) local fun parse_proof outcome parse_proof0 outer_ctxt replay_data xfacts prems concl output = (case outcome output of (Unsat, lines) => (case parse_proof0 of SOME pp => pp outer_ctxt replay_data xfacts prems concl lines | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []}) | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) fun replay outcome replay0 oracle outer_ctxt (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output = (case outcome output of (Unsat, lines) => if Config.get ctxt SMT_Config.oracle then oracle () else (case replay0 of SOME replay => replay outer_ctxt replay_data lines | NONE => error "No proof reconstruction for solver -- \ \declare [[smt_oracle]] to allow oracle") | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) val cfalse = Thm.cterm_of \<^context> \<^prop>\False\ in fun add_solver ({name, class, avail, command, options, smt_options, good_slices, outcome, parse_proof = parse_proof0, replay = replay0} : solver_config) = let fun solver oracle = { command = command, smt_options = smt_options, good_slices = good_slices, parse_proof = parse_proof (outcome name) parse_proof0, replay = replay (outcome name) replay0 oracle} val info = {name = name, class = class, avail = avail, options = options} in Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, oracle) => Context.theory_map (Solvers.map (Symtab.update_new (name, solver oracle)))) #> Context.theory_map (SMT_Config.add_solver info) end end fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) fun name_and_info_of ctxt = let val name = SMT_Config.solver_of ctxt in (name, get_info ctxt name) end val good_slices = #good_slices oo get_info fun apply_solver_and_replay ctxt thms0 = let val thms = map (pair SMT_Util.Axiom o check_topsort ctxt) thms0 val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt val (output, replay_data) = invoke name command [] smt_options (SMT_Normalize.normalize ctxt thms) ctxt in replay ctxt replay_data output end (* filter (for Sledgehammer) *) fun smt_filter ctxt0 goal xfacts i time_limit options = let val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit) val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal fun negate ct = Thm.dest_comb ct ||> Thm.apply \<^cterm>\Not\ |-> Thm.apply val cprop = (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of SOME ct => ct | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal")) val conjecture = Thm.assume cprop val thms = (SMT_Util.Conjecture, conjecture) :: map (pair SMT_Util.Hypothesis) prems @ map (pair SMT_Util.Axiom o snd) xfacts |> map (apsnd (check_topsort ctxt)) val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt val (output, replay_data) = invoke name command options smt_options (SMT_Normalize.normalize ctxt thms) ctxt in parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output end handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []} (* SMT tactic *) local fun str_of ctxt fail = "Solver " ^ SMT_Config.solver_of ctxt ^ ": " ^ SMT_Failure.string_of_failure fail fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts) handle SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) => (SMT_Config.verbose_msg ctxt (K ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^ SMT_Failure.string_of_failure fail ^ " (setting the " ^ "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")) (); NONE) | SMT_Failure.SMT fail => error (str_of ctxt fail) fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 | resolve _ NONE = no_tac fun tac prove ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' resolve_tac ctxt @{thms ccontr} THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve ctxt' (prove ctxt' (rules @ prems))) ctxt in val smt_tac = tac safe_solve val smt_tac' = tac (SOME oo apply_solver_and_replay) end end; diff --git a/src/HOL/Tools/SMT/smtlib_proof.ML b/src/HOL/Tools/SMT/smtlib_proof.ML --- a/src/HOL/Tools/SMT/smtlib_proof.ML +++ b/src/HOL/Tools/SMT/smtlib_proof.ML @@ -1,374 +1,379 @@ (* Title: HOL/Tools/SMT/smtlib_proof.ML Author: Sascha Boehme, TU Muenchen Author: Mathias Fleury, ENS Rennes Author: Jasmin Blanchette, TU Muenchen SMT-LIB-2-style proofs: parsing and abstract syntax tree. *) signature SMTLIB_PROOF = sig datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None type ('a, 'b) context val mk_context: Proof.context -> int -> 'b shared Symtab.table -> typ Symtab.table -> term Symtab.table -> 'a -> ('a, 'b) context val empty_context: Proof.context -> typ Symtab.table -> term Symtab.table -> ('a list, 'b) context val ctxt_of: ('a, 'b) context -> Proof.context val lookup_binding: ('a, 'b) context -> string -> 'b shared val update_binding: string * 'b shared -> ('a, 'b) context -> ('a, 'b) context val with_bindings: (string * 'b shared) list -> (('a, 'b) context -> 'c * ('d, 'b) context) -> ('a, 'b) context -> 'c * ('d, 'b) context val next_id: ('a, 'b) context -> int * ('a, 'b) context val with_fresh_names: (('a list, 'b) context -> term * ((string * (string * typ)) list, 'b) context) -> ('c, 'b) context -> (term * string list) (*type and term parsers*) type type_parser = SMTLIB.tree * typ list -> typ option type term_parser = SMTLIB.tree * term list -> term option val add_type_parser: type_parser -> Context.generic -> Context.generic val add_term_parser: term_parser -> Context.generic -> Context.generic exception SMTLIB_PARSE of string * SMTLIB.tree val declare_fun: string -> typ -> ((string * typ) list, 'a) context -> ((string * typ) list, 'a) context val dest_binding: SMTLIB.tree -> string * 'a shared val type_of: ('a, 'b) context -> SMTLIB.tree -> typ val term_of: SMTLIB.tree -> ((string * (string * typ)) list, 'a) context -> term * ((string * (string * typ)) list, 'a) context (*name bindings*) type name_bindings val empty_name_binding: name_bindings val update_name_binding: Symtab.key * SMTLIB.tree -> name_bindings -> name_bindings val extract_name_bindings: SMTLIB.tree -> name_bindings -> name_bindings * string list val expand_name_bindings: SMTLIB.tree -> name_bindings -> SMTLIB.tree * name_bindings val extract_and_update_name_bindings: SMTLIB.tree -> name_bindings -> (SMTLIB.tree * name_bindings) * string list val remove_name_bindings: SMTLIB.tree -> SMTLIB.tree end; structure SMTLIB_Proof: SMTLIB_PROOF = struct (* proof parser context *) datatype 'b shared = Tree of SMTLIB.tree | Term of term | Proof of 'b | None type ('a, 'b) context = { ctxt: Proof.context, id: int, syms: 'b shared Symtab.table, typs: typ Symtab.table, funs: term Symtab.table, extra: 'a} fun mk_context ctxt id syms typs funs extra: ('a, 'b) context = {ctxt = ctxt, id = id, syms = syms, typs = typs, funs = funs, extra = extra} fun empty_context ctxt typs funs = mk_context ctxt 1 Symtab.empty typs funs [] fun ctxt_of ({ctxt, ...}: ('a, 'b) context) = ctxt fun lookup_binding ({syms, ...}: ('a, 'b) context) = the_default None o Symtab.lookup syms fun map_syms f ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = mk_context ctxt id (f syms) typs funs extra fun update_binding b = map_syms (Symtab.update b) fun with_bindings bs f cx = let val bs' = map (lookup_binding cx o fst) bs in cx |> fold update_binding bs |> f ||> fold2 (fn (name, _) => update_binding o pair name) bs bs' end fun next_id ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = (id, mk_context ctxt (id + 1) syms typs funs extra) fun with_fresh_names f ({ctxt, id, syms, typs, funs, ...}: ('a, 'b) context) = let fun bind (_, v as (_, T)) t = Logic.all_const T $ Term.absfree v t val needs_inferT = equal Term.dummyT orf Term.is_TVar val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT) fun infer_types ctxt = singleton (Type_Infer_Context.infer_types ctxt) #> singleton (Proof_Context.standard_term_check_finish ctxt) fun infer ctxt t = if needs_infer t then infer_types ctxt t else t val (t, {ctxt = ctxt', extra = names, ...}: ((string * (string * typ)) list, 'b) context) = f (mk_context ctxt id syms typs funs []) val t' = infer ctxt' (fold_rev bind names (HOLogic.mk_Trueprop t)) in (t', map fst names) end fun lookup_typ ({typs, ...}: ('a, 'b) context) = Symtab.lookup typs fun lookup_fun ({funs, ...}: ('a, 'b) context) = Symtab.lookup funs (* core type and term parser *) fun core_type_parser (SMTLIB.Sym "Bool", []) = SOME \<^typ>\HOL.bool\ | core_type_parser (SMTLIB.Sym "Int", []) = SOME \<^typ>\Int.int\ | core_type_parser _ = NONE fun mk_unary n t = let val T = fastype_of t in Const (n, T --> T) $ t end fun mk_binary' n T U t1 t2 = Const (n, [T, T] ---> U) $ t1 $ t2 fun mk_binary n t1 t2 = let val T = fastype_of t1 in mk_binary' n T T t1 t2 end fun mk_rassoc f t ts = let val us = rev (t :: ts) in fold f (tl us) (hd us) end fun mk_lassoc f t ts = fold (fn u1 => fn u2 => f u2 u1) ts t fun mk_lassoc' n = mk_lassoc (mk_binary n) fun mk_binary_pred n S t1 t2 = let val T1 = fastype_of t1 val T2 = fastype_of t2 val T = if T1 <> Term.dummyT then T1 else if T2 <> Term.dummyT then T2 else TVar (("?a", serial ()), S) in mk_binary' n T \<^typ>\HOL.bool\ t1 t2 end fun mk_less t1 t2 = mk_binary_pred \<^const_name>\ord_class.less\ \<^sort>\linorder\ t1 t2 fun mk_less_eq t1 t2 = mk_binary_pred \<^const_name>\ord_class.less_eq\ \<^sort>\linorder\ t1 t2 fun core_term_parser (SMTLIB.Sym "true", _) = SOME \<^Const>\True\ | core_term_parser (SMTLIB.Sym "false", _) = SOME \<^Const>\False\ | core_term_parser (SMTLIB.Sym "not", [t]) = SOME (HOLogic.mk_not t) | core_term_parser (SMTLIB.Sym "and", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_conj) t ts) | core_term_parser (SMTLIB.Sym "or", t :: ts) = SOME (mk_rassoc (curry HOLogic.mk_disj) t ts) | core_term_parser (SMTLIB.Sym "=>", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) | core_term_parser (SMTLIB.Sym "implies", [t1, t2]) = SOME (HOLogic.mk_imp (t1, t2)) | core_term_parser (SMTLIB.Sym "=", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) | core_term_parser (SMTLIB.Sym "~", [t1, t2]) = SOME (HOLogic.mk_eq (t1, t2)) | core_term_parser (SMTLIB.Sym "ite", [t1, t2, t3]) = let val T = fastype_of t2 val c = Const (\<^const_name>\HOL.If\, [\<^typ>\HOL.bool\, T, T] ---> T) in SOME (c $ t1 $ t2 $ t3) end | core_term_parser (SMTLIB.Num i, []) = SOME (HOLogic.mk_number \<^typ>\Int.int\ i) | core_term_parser (SMTLIB.Sym "-", [t]) = SOME (mk_unary \<^const_name>\uminus_class.uminus\ t) | core_term_parser (SMTLIB.Sym "~", [t]) = SOME (mk_unary \<^const_name>\uminus_class.uminus\ t) | core_term_parser (SMTLIB.Sym "+", t :: ts) = SOME (mk_lassoc' \<^const_name>\plus_class.plus\ t ts) | core_term_parser (SMTLIB.Sym "-", t :: ts) = SOME (mk_lassoc' \<^const_name>\minus_class.minus\ t ts) | core_term_parser (SMTLIB.Sym "*", t :: ts) = SOME (mk_lassoc' \<^const_name>\times_class.times\ t ts) | core_term_parser (SMTLIB.Sym "div", [t1, t2]) = SOME (mk_binary \<^const_name>\z3div\ t1 t2) | core_term_parser (SMTLIB.Sym "mod", [t1, t2]) = SOME (mk_binary \<^const_name>\z3mod\ t1 t2) | core_term_parser (SMTLIB.Sym "<", [t1, t2]) = SOME (mk_less t1 t2) | core_term_parser (SMTLIB.Sym ">", [t1, t2]) = SOME (mk_less t2 t1) | core_term_parser (SMTLIB.Sym "<=", [t1, t2]) = SOME (mk_less_eq t1 t2) | core_term_parser (SMTLIB.Sym ">=", [t1, t2]) = SOME (mk_less_eq t2 t1) | core_term_parser _ = NONE (* custom type and term parsers *) type type_parser = SMTLIB.tree * typ list -> typ option type term_parser = SMTLIB.tree * term list -> term option fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2) structure Parsers = Generic_Data ( type T = (int * type_parser) list * (int * term_parser) list val empty : T = ([(serial (), core_type_parser)], [(serial (), core_term_parser)]) fun merge ((tys1, ts1), (tys2, ts2)) = (Ord_List.merge id_ord (tys1, tys2), Ord_List.merge id_ord (ts1, ts2)) ) fun add_type_parser type_parser = Parsers.map (apfst (Ord_List.insert id_ord (serial (), type_parser))) fun add_term_parser term_parser = Parsers.map (apsnd (Ord_List.insert id_ord (serial (), term_parser))) fun get_type_parsers ctxt = map snd (fst (Parsers.get (Context.Proof ctxt))) fun get_term_parsers ctxt = map snd (snd (Parsers.get (Context.Proof ctxt))) fun apply_parsers parsers x = let fun apply [] = NONE | apply (parser :: parsers) = (case parser x of SOME y => SOME y | NONE => apply parsers) in apply parsers end (* type and term parsing *) exception SMTLIB_PARSE of string * SMTLIB.tree val desymbolize = Name.desymbolize (SOME false) o perhaps (try (unprefix "?")) fun fresh_fun add name n T ({ctxt, id, syms, typs, funs, extra}: ('a, 'b) context) = let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt val t = Free (n', T) val funs' = Symtab.update (name, t) funs in (t, mk_context ctxt' id syms typs funs' (add (n', T) extra)) end fun declare_fun name = snd oo fresh_fun cons name (desymbolize name) fun declare_free name = fresh_fun (cons o pair name) name (desymbolize name) fun parse_type cx ty Ts = (case apply_parsers (get_type_parsers (ctxt_of cx)) (ty, Ts) of SOME T => T | NONE => (case ty of SMTLIB.Sym name => (case lookup_typ cx name of SOME T => T | NONE => raise SMTLIB_PARSE ("unknown SMT type", ty)) | _ => raise SMTLIB_PARSE ("bad SMT type format", ty))) fun parse_term t ts cx = (case apply_parsers (get_term_parsers (ctxt_of cx)) (t, ts) of SOME u => (u, cx) | NONE => (case t of SMTLIB.Sym name => (case lookup_fun cx name of SOME u => (Term.list_comb (u, ts), cx) | NONE => if null ts then declare_free name Term.dummyT cx else raise SMTLIB_PARSE ("bad SMT term", t)) | _ => raise SMTLIB_PARSE ("bad SMT term format", t))) fun type_of cx ty = (case try (parse_type cx ty) [] of SOME T => T | NONE => (case ty of SMTLIB.S (ty' :: tys) => parse_type cx ty' (map (type_of cx) tys) | _ => raise SMTLIB_PARSE ("bad SMT type", ty))) fun dest_var cx (SMTLIB.S [SMTLIB.Sym name, ty]) = (name, (desymbolize name, type_of cx ty)) | dest_var _ v = raise SMTLIB_PARSE ("bad SMT quantifier variable format", v) fun dest_body (SMTLIB.S (SMTLIB.Sym "!" :: body :: _)) = dest_body body | dest_body body = body fun dest_binding (SMTLIB.S [SMTLIB.Sym name, t]) = (name, Tree t) | dest_binding b = raise SMTLIB_PARSE ("bad SMT let binding format", b) fun mk_choice (x, T, P) = HOLogic.choice_const T $ absfree (x, T) P fun term_of t cx = (case t of SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S vars, body] => quant HOLogic.mk_all vars body cx | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S vars, body] => quant HOLogic.mk_exists vars body cx | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S vars, body] => quant mk_choice vars body cx | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] => with_bindings (map dest_binding bindings) (term_of body) cx | SMTLIB.S (SMTLIB.Sym "!" :: t :: _) => term_of t cx | SMTLIB.S (f :: args) => cx |> fold_map term_of args |-> parse_term f | SMTLIB.Sym name => (case lookup_binding cx name of Tree u => cx |> term_of u |-> (fn u' => pair u' o update_binding (name, Term u')) | Term u => (u, cx) | None => parse_term t [] cx | _ => raise SMTLIB_PARSE ("bad SMT term format", t)) | _ => parse_term t [] cx) and quant q vars body cx = let val vs = map (dest_var cx) vars in cx |> with_bindings (map (apsnd (Term o Free)) vs) (term_of (dest_body body)) |>> fold_rev (fn (_, (n, T)) => fn t => q (n, T, t)) vs end (* Sharing of terms via "! _ :named name"*) type name_bindings = SMTLIB.tree Symtab.table * SMTLIB.tree Symtab.table val empty_name_binding = (Symtab.empty, Symtab.empty) fun update_name_binding (name, t) (tab, exp_tab) = (tab, Symtab.update (name, t) exp_tab) fun remove_name_bindings (SMTLIB.S (SMTLIB.Sym "!" :: body :: _)) = remove_name_bindings body | remove_name_bindings (SMTLIB.S body) = SMTLIB.S (map remove_name_bindings body) | remove_name_bindings t = t fun extract_name_bindings t (tab, exp_tab) = let fun extract t (tab, new) = (case t of SMTLIB.S [SMTLIB.Sym "forall", SMTLIB.S _, body] => extract body (tab, new) | SMTLIB.S [SMTLIB.Sym "exists", SMTLIB.S _, body] => extract body (tab, new) | SMTLIB.S [SMTLIB.Sym "choice", SMTLIB.S _, body] => extract body (tab, new) - | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S bindings, body] => + | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S lets, body] => ( + let val bindings = map (fn SMTLIB.S (var :: bindings) => bindings) lets in + fold (fn bdgs => fn st => fold extract bdgs st) bindings (tab, new) + |> extract body + end) + | SMTLIB.S [SMTLIB.Sym "let", SMTLIB.S [_, bindings], body] => raise (Fail "unsupported let construction in name extraction") | SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name]) => extract t (tab, new) |>> Symtab.update (name, remove_name_bindings t) ||> curry (op :: ) name | SMTLIB.S args => fold extract args (tab, new) | _ => ((tab, new))) val (tab, new) = extract t (tab, []) in ((tab, exp_tab), new) end fun expand_name_bindings t (tab, exp_tab) = let fun expand_update (SMTLIB.Sym sym) exp_tab = (case Symtab.lookup exp_tab sym of SOME t => (t, exp_tab) | NONE => (case (Symtab.lookup tab sym) of NONE => (SMTLIB.Sym sym, exp_tab) | SOME u => let val (u2, exp_tab) = expand_update u exp_tab in (u2, Symtab.update (sym, u2) exp_tab) end ) ) | expand_update (t as SMTLIB.Key _) exp_tab = (t, exp_tab) | expand_update (t as SMTLIB.Num _) exp_tab = (t, exp_tab) | expand_update (t as SMTLIB.Dec _) exp_tab = (t, exp_tab) | expand_update (t as SMTLIB.Str _) exp_tab = (t, exp_tab) | expand_update (SMTLIB.S s) (exp_tab : SMTLIB.tree Symtab.table) = fold_map expand_update s exp_tab |>> (fn s => SMTLIB.S s) in expand_update t exp_tab |> (fn (t, exp_tab) => (remove_name_bindings t, (tab, exp_tab))) end fun extract_and_update_name_bindings t tab = extract_name_bindings t tab |>> expand_name_bindings (remove_name_bindings t) end;