equal
deleted
inserted
replaced
36 open Sledgehammer_Prover |
36 open Sledgehammer_Prover |
37 |
37 |
38 val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true) |
38 val smt_builtins = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_builtins\<close> (K true) |
39 val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true) |
39 val smt_triggers = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_smt_triggers\<close> (K true) |
40 |
40 |
41 val smts = SMT_Config.all_solvers_of |
41 val smts = sort_strings o SMT_Config.all_solvers_of |
42 |
42 |
43 val is_smt_prover = member (op =) o smts |
43 val is_smt_prover = member (op =) o smts |
44 val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of |
44 val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of |
45 |
45 |
46 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |
46 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out |