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