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 val _ = OS.Process.system (p ^ " -version > " ^ outfile) 64 in 65 parse_Z3_version outfile 66 end 67 68 val doproofs = 69 if String.sub(Z3version, 0) = #"2" then true 70 else if String.sub(Z3version, 0) = #"0" then false 71 else 72 (Feedback.HOL_MESG ("Can't replay proofs with Z3 v"^Z3version); false) 73 74 (* Z3 (Linux/Unix), SMT-LIB file format, with proofs *) 75 val Z3_SMT_Prover = if not doproofs then Z3_SMT_Oracle else 76 mk_Z3_fun "Z3_SMT_Prover" 77 (fn goal => 78 let 79 val (goal, validation) = SolverSpec.simplify (SmtLib.SIMP_TAC true) goal 80 val (ty_tm_dict, strings) = SmtLib.goal_to_SmtLib_with_get_proof goal 81 in 82 (((goal, validation), ty_tm_dict), strings) 83 end) 84 " PROOF_MODE=2 -smt2 -file:" 85 (fn ((goal, validation), (ty_dict, tm_dict)) => 86 fn outfile => 87 let 88 val instream = TextIO.openIn outfile 89 val result = is_sat_stream instream 90 in 91 case result of 92 SolverSpec.UNSAT NONE => 93 let 94 (* invert 'ty_dict' and 'tm_dict', create parsing functions *) 95 val ty_dict = Redblackmap.foldl (fn (ty, s, dict) => 96 (* types don't take arguments *) 97 Redblackmap.insert (dict, s, [SmtLib_Theories.K_zero_zero ty])) 98 (Redblackmap.mkDict String.compare) ty_dict 99 val tm_dict = Redblackmap.foldl (fn ((tm, n), s, dict) => 100 Redblackmap.insert (dict, s, [Lib.K (SmtLib_Theories.zero_args 101 (fn args => 102 if List.length args = n then 103 Term.list_mk_comb (tm, args) 104 else 105 raise Feedback.mk_HOL_ERR "Z3" ("<" ^ s ^ ">") 106 "wrong number of arguments"))])) 107 (Redblackmap.mkDict String.compare) tm_dict 108 (* add relevant SMT-LIB types/terms to dictionaries *) 109 val ty_dict = Library.union_dict (Library.union_dict 110 SmtLib_Logics.AUFNIRA.tydict SmtLib_Logics.QF_ABV.tydict) 111 ty_dict 112 val tm_dict = Library.union_dict (Library.union_dict 113 SmtLib_Logics.AUFNIRA.tmdict SmtLib_Logics.QF_ABV.tmdict) 114 tm_dict 115 (* parse the proof and check it in HOL *) 116 val proof = Z3_ProofParser.parse_stream (ty_dict, tm_dict) 117 instream 118 val _ = TextIO.closeIn instream 119 val thm = Z3_ProofReplay.check_proof proof 120 val (As, g) = goal 121 val thm = Thm.CCONTR g thm 122 val thm = validation [thm] 123 in 124 SolverSpec.UNSAT (SOME thm) 125 end 126 | _ => (result before TextIO.closeIn instream) 127 end) 128 129end 130