1(* Copyright (c) 2009-2012 Tjark Weber. All rights reserved. *)
2
3(* Definition of SMT solvers *)
4
5structure SolverSpec = struct
6
7  datatype result = SAT of string option  (* model, should perhaps be a thm *)
8                  | UNSAT of Thm.thm option  (* assumptions |- conclusion *)
9                  | UNKNOWN of string option  (* reason for failure *)
10
11  (* calls 'pre' (which is supposed to translate a HOL goal into a list of
12     strings that the SMT solver will understand); writes these strings into a
13     file; appends the names of input and output files to 'cmd_stem' before
14     executing it as a system command; calls 'post' (which is supposed to parse
15     the output file generated by the SMT solver); deletes input and output
16     file (unless '!trace' = 4); emits messages according to '!trace' *)
17  fun make_solver (pre : Abbrev.goal -> 'a * string list)
18                  (cmd_stem : string)
19                  (post : 'a -> string -> result) : Abbrev.goal -> result =
20  fn goal =>
21  let
22    (* call 'pre goal' to generate SMT solver input *)
23    val (x, inputs) = pre goal
24    val infile = FileSys.tmpName ()
25    val _ = Library.write_strings_to_file infile inputs
26    val outfile = FileSys.tmpName ()
27    val cmd = cmd_stem ^ infile ^ " > " ^ outfile
28    (* the actual system call to the SMT solver *)
29    val _ = if !Library.trace > 1 then
30        Feedback.HOL_MESG ("HolSmtLib: calling external command '" ^ cmd ^ "'")
31      else ()
32    val _ = Systeml.system_ps cmd
33    (* call 'post' to determine the result *)
34    val result = post x outfile
35    val _ = if !Library.trace > 1 then
36        Feedback.HOL_MESG ("HolSmtLib: solver reports negated term to be '" ^
37          (case result of
38             SAT NONE => "satisfiable' (no model given)"
39           | SAT (SOME _) => "satisfiable' (model given)"
40           | UNSAT NONE => "unsatisfiable' (no proof given)"
41           | UNSAT (SOME thm) =>
42             if !Library.trace > 2 then
43               "unsatisfiable' (theorem: " ^ Hol_pp.thm_to_string thm ^ ")"
44             else
45               "unsatisfiable' (proof checked)"
46           | UNKNOWN NONE => "unknown' (no reason given)"
47           | UNKNOWN (SOME _) => "unknown' (reason given)"))
48      else ()
49    (* if the SMT solver returned a theorem 'thm', then this should be of the
50       form "A' |- g" with A' \subseteq A, where (A, g) is the input goal *)
51    val _ = if !Library.trace > 0 then
52        case result of
53          UNSAT (SOME thm) =>
54            let
55              val (As, g) = goal
56              val As = HOLset.fromList Term.compare As
57            in
58              if not (HOLset.isSubset (Thm.hypset thm, As)) then
59                Feedback.HOL_WARNING "SolverSpec" "make_solver"
60                  "theorem contains additional hyp(s)"
61              else ();
62              if not (Term.aconv (Thm.concl thm) g) then
63                Feedback.HOL_WARNING "SolverSpec" "make_solver"
64                  "conclusion of theorem does not match goal"
65              else ()
66            end
67        | _ =>
68          ()
69      else ()
70    (* delete all temporary files *)
71    val _ = if !Library.trace < 4 then
72        List.app (fn path => OS.FileSys.remove path handle SysErr _ => ())
73          [infile, outfile]
74      else ()
75  in
76    result
77  end
78
79  (* simplifies the goal to eliminate (some) terms that are not supported by
80     the respective SMT solver; simp_tac must produce at most one subgoal *)
81  fun simplify simp_tac goal =
82  let
83    val (new_goal, validation) = case simp_tac goal of
84        ([], validation) =>
85        (* apply the SMT solver anyway, but to the trivial goal ``T`` *)
86        (([], boolSyntax.T), fn _ => validation [])
87      | ([new_goal], validation) =>
88        (new_goal, validation)
89      | _ =>
90        raise Feedback.mk_HOL_ERR "SolverSpec" "simplify"
91          "simplification produced more than one subgoal"
92  in
93    if !Library.trace > 2 then
94      let
95        fun goal_to_string (asl, g) =
96          "[" ^ String.concatWith ", " (List.map Hol_pp.term_to_string asl) ^
97            "] |- " ^ Hol_pp.term_to_string g
98      in
99        Feedback.HOL_MESG
100          ("HolSmtLib: simplified goal is " ^ goal_to_string new_goal)
101      end
102    else ();
103    (new_goal, validation)
104  end
105
106end
107