1(* Copyright (c) 2010-2011 Tjark Weber. All rights reserved. *) 2 3(* Entry point into HolQbfLib. *) 4 5structure HolQbfLib :> HolQbfLib = struct 6 7 fun get_certificate t = 8 let 9 val path = FileSys.tmpName () 10 val dict = QDimacs.write_qdimacs_file path t 11 (* the actual system call to Squolem *) 12 val cmd = "squolem2 -c " ^ path ^ " >/dev/null 2>&1" 13 val _ = if !QbfTrace.trace > 1 then 14 Feedback.HOL_MESG ("HolQbfLib: calling external command '" ^ cmd ^ "'") 15 else () 16 val _ = Systeml.system_ps cmd 17 val cert_path = path ^ ".qbc" (* the file name is hard-wired in Squolem *) 18 val cert = QbfCertificate.read_certificate_file cert_path 19 (* delete temporary files *) 20 val _ = if !QbfTrace.trace < 4 then 21 List.app (fn path => OS.FileSys.remove path handle SysErr _ => ()) 22 [path, cert_path] 23 else () 24 in 25 (dict, cert) 26 end 27 28 (* 'prove' can prove valid QBFs in prenex form by validating a 29 certificate of validity generated by the QBF solver Squolem. 30 Returns a theorem "|- t". Fails if Squolem does not generate a 31 certificate of validity. *) 32 fun prove t = 33 let 34 val (dict, cert) = get_certificate t 35 in 36 case cert of 37 QbfCertificate.VALID _ => QbfCertificate.check t dict cert 38 | _ => 39 raise Feedback.mk_HOL_ERR "HolQbfLib" "prove" "certificate says invalid" 40 end 41 42 (* 'disprove' can disprove invalid QBFs in prenex form by validating 43 a certificate of invalidity generated by the QBF solver Squolem. 44 Returns a theorem "t |- F". Fails if Squolem does not generate a 45 certificate of invalidity. *) 46 fun disprove t = 47 let 48 val (dict, cert) = get_certificate t 49 in 50 case cert of 51 QbfCertificate.INVALID _ => 52 QbfCertificate.check t dict cert 53 | _ => 54 raise Feedback.mk_HOL_ERR "HolQbfLib" "disprove" "certificate says valid" 55 end 56 57 (* 'decide_prenex' can prove valid and disprove invalid QBFs in 58 prenex form by validating a certificate (of validity or 59 invalidity, respectively) generated by the QBF solver 60 Squolem. Returns a theorem "|- t" or "t |- F". Fails if Squolem 61 does not generate a certificate. *) 62 fun decide_prenex t = 63 let 64 val (dict, cert) = get_certificate t 65 in 66 QbfCertificate.check t dict cert 67 end 68 69 (* Similar to 'decide_prenex' but accepts QBFs with fewer form 70 restrictions. In case of free variables in an invalid formula, 71 they will be universally quantified in the resulting theorem's 72 assumptions. *) 73 fun decide t = 74 let 75 open Thm Drule boolSyntax 76 val fvs = Term.free_vars t 77 val t = list_mk_forall (fvs,t) 78 val tt = QbfConv.qbf_prenex_conv t 79 val t' = rhs (concl tt) 80 in if t' = T then SPECL fvs (EQ_MP (SYM tt) boolTheory.TRUTH) else 81 if t' = F then EQ_MP tt (ASSUME t) else let 82 val (dict, cert) = get_certificate t' 83 val th = QbfCertificate.check t' dict cert 84 in case cert of 85 QbfCertificate.INVALID _ => 86 UNDISCH (SUBS_OCCS [([1],SYM tt)] (DISCH t' th)) 87 | QbfCertificate.VALID _ => 88 SPECL fvs (EQ_MP (SYM tt) th) 89 end end 90 91 fun set_sat_prove s = QbfCertificate.sat_prove := s 92 93end 94