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