1(* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *) 2 3(* Functions to invoke the Z3 SMT solver *) 4 5structure Z3 = struct 6 7 (* returns SAT if Z3 reported "sat", UNSAT if Z3 reported "unsat" *) 8 fun is_sat_stream instream = 9 case Option.map (String.tokens Char.isSpace) (TextIO.inputLine instream) of 10 NONE => SolverSpec.UNKNOWN NONE 11 | SOME ["sat"] => SolverSpec.SAT NONE 12 | SOME ["unsat"] => SolverSpec.UNSAT NONE 13 | _ => is_sat_stream instream 14 15 fun is_sat_file path = 16 let 17 val instream = TextIO.openIn path 18 in 19 is_sat_stream instream 20 before TextIO.closeIn instream 21 end 22 23 fun is_configured () = 24 Option.isSome (OS.Process.getEnv "HOL4_Z3_EXECUTABLE") 25 26 fun mk_Z3_fun name pre cmd_stem post goal = 27 case OS.Process.getEnv "HOL4_Z3_EXECUTABLE" of 28 SOME file => 29 SolverSpec.make_solver pre (file ^ cmd_stem) post goal 30 | NONE => 31 raise Feedback.mk_HOL_ERR "Z3" name 32 "Z3 not configured: set the HOL4_Z3_EXECUTABLE environment variable to point to the Z3 executable file." 33 34 (* Z3 (Linux/Unix), SMT-LIB file format, no proofs *) 35 val Z3_SMT_Oracle = 36 mk_Z3_fun "Z3_SMT_Oracle" 37 (fn goal => 38 let 39 val (goal, _) = SolverSpec.simplify (SmtLib.SIMP_TAC false) goal 40 val (_, strings) = SmtLib.goal_to_SmtLib goal 41 in 42 ((), strings) 43 end) 44 " -smt2 -file:" 45 (Lib.K is_sat_file) 46 47 (* e.g. "Z3 version 4.5.0 - 64 bit" *) 48 fun parse_Z3_version fname = 49 let 50 val instrm = TextIO.openIn fname 51 val s = TextIO.inputAll instrm before TextIO.closeIn instrm 52 val tokens = String.tokens Char.isSpace s 53 in 54 List.nth (tokens, 2) 55 end 56 57 val Z3version = 58 case OS.Process.getEnv "HOL4_Z3_EXECUTABLE" of 59 NONE => "0" 60 | SOME p => 61 let 62 val outfile = OS.FileSys.tmpName() 63 fun work () = let 64 val _ = OS.Process.system (p ^ " -version > " ^ outfile) 65 in 66 parse_Z3_version outfile 67 end 68 fun finish () = 69 OS.FileSys.remove outfile handle SysErr _ => () 70 in 71 Portable.finally finish work () 72 end 73 74 val doproofs = 75 if String.sub(Z3version, 0) = #"2" then true 76 else if String.sub(Z3version, 0) = #"0" then false 77 else 78 (Feedback.HOL_MESG ("Can't replay proofs with Z3 v"^Z3version); false) 79 80 (* Z3 (Linux/Unix), SMT-LIB file format, with proofs *) 81 val Z3_SMT_Prover = if not doproofs then Z3_SMT_Oracle else 82 mk_Z3_fun "Z3_SMT_Prover" 83 (fn goal => 84 let 85 val (goal, validation) = SolverSpec.simplify (SmtLib.SIMP_TAC true) goal 86 val (ty_tm_dict, strings) = SmtLib.goal_to_SmtLib_with_get_proof goal 87 in 88 (((goal, validation), ty_tm_dict), strings) 89 end) 90 " PROOF_MODE=2 -smt2 -file:" 91 (fn ((goal, validation), (ty_dict, tm_dict)) => 92 fn outfile => 93 let 94 val instream = TextIO.openIn outfile 95 val result = is_sat_stream instream 96 in 97 case result of 98 SolverSpec.UNSAT NONE => 99 let 100 (* invert 'ty_dict' and 'tm_dict', create parsing functions *) 101 val ty_dict = Redblackmap.foldl (fn (ty, s, dict) => 102 (* types don't take arguments *) 103 Redblackmap.insert (dict, s, [SmtLib_Theories.K_zero_zero ty])) 104 (Redblackmap.mkDict String.compare) ty_dict 105 val tm_dict = Redblackmap.foldl (fn ((tm, n), s, dict) => 106 Redblackmap.insert (dict, s, [Lib.K (SmtLib_Theories.zero_args 107 (fn args => 108 if List.length args = n then 109 Term.list_mk_comb (tm, args) 110 else 111 raise Feedback.mk_HOL_ERR "Z3" ("<" ^ s ^ ">") 112 "wrong number of arguments"))])) 113 (Redblackmap.mkDict String.compare) tm_dict 114 (* add relevant SMT-LIB types/terms to dictionaries *) 115 val ty_dict = Library.union_dict (Library.union_dict 116 SmtLib_Logics.AUFNIRA.tydict SmtLib_Logics.QF_ABV.tydict) 117 ty_dict 118 val tm_dict = Library.union_dict (Library.union_dict 119 SmtLib_Logics.AUFNIRA.tmdict SmtLib_Logics.QF_ABV.tmdict) 120 tm_dict 121 (* parse the proof and check it in HOL *) 122 val proof = Z3_ProofParser.parse_stream (ty_dict, tm_dict) 123 instream 124 val _ = TextIO.closeIn instream 125 val thm = Z3_ProofReplay.check_proof proof 126 val (As, g) = goal 127 val thm = Thm.CCONTR g thm 128 val thm = validation [thm] 129 in 130 SolverSpec.UNSAT (SOME thm) 131 end 132 | _ => (result before TextIO.closeIn instream) 133 end) 134 135end 136