1(* Title: HOL/Tools/SMT/smt_systems.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Setup SMT solvers. 5*) 6 7signature SMT_SYSTEMS = 8sig 9 val cvc4_extensions: bool Config.T 10 val z3_extensions: bool Config.T 11end; 12 13structure SMT_Systems: SMT_SYSTEMS = 14struct 15 16(* helper functions *) 17 18fun make_avail name () = getenv (name ^ "_SOLVER") <> "" 19 20fun make_command name () = [getenv (name ^ "_SOLVER")] 21 22fun outcome_of unsat sat unknown timeout solver_name line = 23 if String.isPrefix unsat line then SMT_Solver.Unsat 24 else if String.isPrefix sat line then SMT_Solver.Sat 25 else if String.isPrefix unknown line then SMT_Solver.Unknown 26 else if String.isPrefix timeout line then SMT_Solver.Time_Out 27 else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ 28 " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ 29 " option for details")) 30 31fun is_blank_or_error_line "" = true 32 | is_blank_or_error_line s = String.isPrefix "(error " s 33 34fun on_first_line test_outcome solver_name lines = 35 let 36 val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) 37 val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines) 38 in (test_outcome solver_name l, ls) end 39 40fun on_first_non_unsupported_line test_outcome solver_name lines = 41 on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) 42 43(* CVC3 *) 44 45local 46 fun cvc3_options ctxt = [ 47 "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed), 48 "-lang", "smt2", 49 "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))] 50in 51 52val cvc3: SMT_Solver.solver_config = { 53 name = "cvc3", 54 class = K SMTLIB_Interface.smtlibC, 55 avail = make_avail "CVC3", 56 command = make_command "CVC3", 57 options = cvc3_options, 58 smt_options = [], 59 default_max_relevant = 400 (* FUDGE *), 60 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), 61 parse_proof = NONE, 62 replay = NONE } 63 64end 65 66 67(* CVC4 *) 68 69val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false) 70 71local 72 fun cvc4_options ctxt = [ 73 "--no-statistics", 74 "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), 75 "--lang=smt2", 76 "--continued-execution", 77 "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))] 78 79 fun select_class ctxt = 80 if Config.get ctxt cvc4_extensions then 81 if Config.get ctxt SMT_Config.higher_order then 82 CVC4_Interface.hosmtlib_cvc4C 83 else 84 CVC4_Interface.smtlib_cvc4C 85 else 86 if Config.get ctxt SMT_Config.higher_order then 87 SMTLIB_Interface.hosmtlibC 88 else 89 SMTLIB_Interface.smtlibC 90in 91 92val cvc4: SMT_Solver.solver_config = { 93 name = "cvc4", 94 class = select_class, 95 avail = make_avail "CVC4", 96 command = make_command "CVC4", 97 options = cvc4_options, 98 smt_options = [(":produce-unsat-cores", "true")], 99 default_max_relevant = 400 (* FUDGE *), 100 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), 101 parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), 102 replay = NONE } 103 104end 105 106 107(* veriT *) 108 109local 110 fun select_class ctxt = 111 if Config.get ctxt SMT_Config.higher_order then 112 SMTLIB_Interface.hosmtlibC 113 else 114 SMTLIB_Interface.smtlibC 115in 116 117val veriT: SMT_Solver.solver_config = { 118 name = "verit", 119 class = select_class, 120 avail = make_avail "VERIT", 121 command = make_command "VERIT", 122 options = (fn ctxt => [ 123 "--proof-version=2", 124 "--proof-prune", 125 "--proof-merge", 126 "--disable-print-success", 127 "--disable-banner", 128 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), 129 smt_options = [(":produce-proofs", "true")], 130 default_max_relevant = 200 (* FUDGE *), 131 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "timeout"), 132 parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), 133 replay = SOME Verit_Replay.replay } 134 135end 136 137 138(* Z3 *) 139 140val z3_extensions = Attrib.setup_config_bool \<^binding>\<open>z3_extensions\<close> (K false) 141 142local 143 fun z3_options ctxt = 144 ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), 145 "smt.refine_inj_axioms=false", 146 "-T:" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout)), 147 "-smt2"] 148 149 fun select_class ctxt = 150 if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else SMTLIB_Interface.smtlibC 151in 152 153val z3: SMT_Solver.solver_config = { 154 name = "z3", 155 class = select_class, 156 avail = make_avail "Z3", 157 command = make_command "Z3", 158 options = z3_options, 159 smt_options = [(":produce-proofs", "true")], 160 default_max_relevant = 350 (* FUDGE *), 161 outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), 162 parse_proof = SOME Z3_Replay.parse_proof, 163 replay = SOME Z3_Replay.replay } 164 165end 166 167 168(* overall setup *) 169 170val _ = Theory.setup ( 171 SMT_Solver.add_solver cvc3 #> 172 SMT_Solver.add_solver cvc4 #> 173 SMT_Solver.add_solver veriT #> 174 SMT_Solver.add_solver z3) 175 176end; 177