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