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