1(* Copyright (c) 2010 Tjark Weber. All rights reserved. *) 2 3(* Common auxiliary functions. *) 4 5structure QbfLibrary = 6struct 7 8 val ERR = Feedback.mk_HOL_ERR "QbfLibrary" 9 10(* ------------------------------------------------------------------------- *) 11(* write_strings_to_file: opens 'path' as an output text file; writes all *) 12(* elements of 'strings' to this file (in the order given); closes the *) 13(* file *) 14(* ------------------------------------------------------------------------- *) 15 16 fun write_strings_to_file path strings = 17 let 18 val outstream = TextIO.openOut path 19 in 20 List.app (TextIO.output o Lib.pair outstream) strings; 21 TextIO.closeOut outstream 22 end 23 24(* ------------------------------------------------------------------------- *) 25(* read_lines_from_file: opens 'path' as an input text file; reads all lines *) 26(* of this file (using TextIO.inputLine); closes the file before *) 27(* returning the lines read (as a list of strings, each terminated by *) 28(* "\n") *) 29(* ------------------------------------------------------------------------- *) 30 31 fun read_lines_from_file path = 32 let 33 val instream = TextIO.openIn path 34 fun input acc = 35 case TextIO.inputLine instream of 36 SOME line => 37 input (line :: acc) 38 | NONE => 39 List.rev acc 40 in 41 input [] before TextIO.closeIn instream 42 end 43 44(* ------------------------------------------------------------------------- *) 45(* enumerate_quantified_vars: takes a term 't' of the form *) 46(* "Qn xn. ... Q1 x1. phi" (where n>=0, and each Qi is either ? or !), *) 47(* and returns (n+1, [(n, xn, qn), ..., (1, x1, q1)], phi), where qi is *) 48(* true if Qi is !, and false if Qi is ?. *) 49(* ------------------------------------------------------------------------- *) 50 51 fun enumerate_quantified_vars t = 52 let 53 val ((var, body), is_forall) = (boolSyntax.dest_forall t, true) 54 handle Feedback.HOL_ERR _ => (* 't' is not universally quantified *) 55 (boolSyntax.dest_exists t, false) 56 val (next_index, vars, body) = enumerate_quantified_vars body 57 in 58 (next_index + 1, (next_index, var, is_forall) :: vars, body) 59 end 60 handle Feedback.HOL_ERR _ => (* 't' is not quantified *) 61 (1, [], t) 62 63(* ------------------------------------------------------------------------- *) 64(* A |- p1 \/ ... \/ pn *) 65(* --------------------- CLAUSE_TO_SEQUENT *) 66(* A, ~p1, ..., ~pn |- F *) 67(* ------------------------------------------------------------------------- *) 68 69 fun CLAUSE_TO_SEQUENT thm = 70 let 71 val concl = Thm.concl thm 72 in 73 let 74 val (p, q) = boolSyntax.dest_disj concl 75 in 76 Thm.DISJ_CASES thm 77 (CLAUSE_TO_SEQUENT (Thm.ASSUME p)) (CLAUSE_TO_SEQUENT (Thm.ASSUME q)) 78 end 79 handle Feedback.HOL_ERR _ => (* 'concl' is not a disjunction *) 80 if boolLib.Feq concl then thm 81 else ( 82 Thm.MP (Thm.NOT_ELIM thm) (Thm.ASSUME (boolSyntax.dest_neg concl)) 83 handle Feedback.HOL_ERR _ => (* 'concl' is not a negation *) 84 Thm.MP (Thm.NOT_ELIM (Thm.ASSUME (boolSyntax.mk_neg concl))) thm 85 ) 86 end 87 88(* ------------------------------------------------------------------------- *) 89(* literals_in_clause: takes a function 'index_fn' that maps variables to a *) 90(* pair consisting of a positive integer i and a Boolean q, and a *) 91(* clause theorem 'thm' in sequent form, as produced by *) 92(* 'CLAUSE_TO_SEQUENT'. Returns a list of triples ([~]i, [~]var, q), *) 93(* with one element for every hypothesis of 'thm' that is a literal *) 94(* (i.e., a possibly negated variable). The list is sorted with *) 95(* respect to the absolute value of its elements first component, [~]i. *) 96(* ------------------------------------------------------------------------- *) 97 98 fun literals_in_clause index_fn thm = 99 let 100 val set = HOLset.foldl (fn (t, set) => 101 let 102 val (i, q) = index_fn (boolSyntax.dest_neg t) 103 in 104 HOLset.add (set, (~ i, t, q)) 105 end 106 handle Feedback.HOL_ERR _ => (* 't' is not a negation *) 107 let 108 val (i, q) = index_fn t 109 in 110 HOLset.add (set, (i, t, q)) 111 end 112 handle Feedback.HOL_ERR _ => (* 't' is not a variable *) 113 set) (HOLset.empty (Int.compare o Lib.## (Int.abs o #1, Int.abs o #1))) 114 (Thm.hypset thm) 115 in 116 HOLset.listItems set 117 end 118 119(* ------------------------------------------------------------------------- *) 120(* discharge_lit: discharges a possibly negated variable (i.e., a literal) *) 121(* from a theorem 'thm' by instantiating it to (either) "T" or "F". *) 122(* *) 123(* A, v |- t *) 124(* ---------------- discharge_lit v *) 125(* A[T/v] |- t[T/v] *) 126(* *) 127(* A, ~v |- t *) 128(* ---------------- discharge_lit ~v *) 129(* A[F/v] |- t[F/v] *) 130(* ------------------------------------------------------------------------- *) 131 132local 133 val NOT_FALSE = bossLib.DECIDE ``~F`` 134in 135 fun discharge_lit lit thm = 136 let 137 val var = boolSyntax.dest_neg lit 138 in 139 Thm.MP (Thm.INST [{redex = var, residue = boolSyntax.F}] 140 (Thm.DISCH lit thm)) NOT_FALSE 141 end 142 handle Feedback.HOL_ERR _ => (* 'lit' is not negated *) 143 Thm.MP (Thm.INST [{redex = lit, residue = boolSyntax.T}] 144 (Thm.DISCH lit thm)) boolTheory.TRUTH 145end 146 147(* ------------------------------------------------------------------------- *) 148(* A, hyp |- t *) 149(* ----------------- bind_var hyp var true *) 150(* A, !var. hyp |- t *) 151(* *) 152(* A, hyp |- t *) 153(* ----------------- bind_var hyp var false (var not free in A or t) *) 154(* A, ?var. hyp |- t *) 155(* ------------------------------------------------------------------------- *) 156 157 fun bind_var thm hyp var is_forall = 158 if is_forall then (*Profile.profile "bind_var(forall)"*) (fn () => 159 let 160 val hyp' = boolSyntax.mk_forall (var, hyp) 161 val thm = Thm.MP (Thm.DISCH hyp thm) (Thm.SPEC var (Thm.ASSUME hyp')) 162 in 163 (thm, hyp') 164 end) () 165 else (*Profile.profile "bind_var(exists)"*) (fn () => 166 (* 'var' must not be free in the hypotheses of 'thm' (except in 'hyp') *) 167 let 168 val hyp' = boolSyntax.mk_exists (var, hyp) 169 val thm = Thm.CHOOSE (var, Thm.ASSUME hyp') thm 170 in 171 (thm, hyp') 172 end) () 173 174(* ------------------------------------------------------------------------- *) 175(* Implements forall-reduction. Takes a clause in sequent form, a list of *) 176(* variables to be introduced eventually, the partial QBF (which should *) 177(* be a hypothesis of the clause) that is missing these variables, and *) 178(* the list of literals present in the clause. Both lists must be *) 179(* ordered, with variables that are in the scope of other variables *) 180(* coming first. *) 181(* ------------------------------------------------------------------------- *) 182 183 fun forall_reduce (thm, [], hyp, []) = 184 (thm, [], hyp, []) 185 | forall_reduce (thm, (_, var, is_forall) :: vars, hyp, []) = 186 let 187 val (thm, hyp) = bind_var thm hyp var is_forall 188 in 189 forall_reduce (thm, vars, hyp, []) 190 end 191 | forall_reduce (thm, vars as (i, var, v_is_forall) :: vartail, hyp, 192 lits as (j, lit, l_is_forall) :: littail) = 193 194 if v_is_forall then 195 let 196 val (thm, hyp) = bind_var thm hyp var v_is_forall 197 (* discharge the variable if it occurs *) 198 val (thm, lits') = if i < Int.abs j then 199 (thm, lits) 200 else (* i = Int.abs j *) 201 ((*Profile.profile "discharge_lit"*) (discharge_lit lit) thm, 202 littail) 203 in 204 forall_reduce (thm, vartail, hyp, lits') 205 end 206 else if l_is_forall then 207 (* late binding of existentials: only when the innermost literal is 208 universal *) 209 let 210 val (thm, hyp) = bind_var thm hyp var v_is_forall 211 in 212 forall_reduce (thm, vartail, hyp, lits) 213 end 214 else 215 (thm, vars, hyp, lits) 216 | forall_reduce (_, [], _, _ :: _) = 217 raise Match 218 219(* ------------------------------------------------------------------------- *) 220(* merge: merges two lists of tuples whose first components are integers *) 221(* sorted wrt. absolute value into a single list sorted wrt. absolute *) 222(* value; drops duplicates that occur in both lists *) 223(* ------------------------------------------------------------------------- *) 224 225 fun merge xs [] : (int * 'a * 'b) list = xs 226 | merge [] ys = ys 227 | merge (xs as xhd :: xtails) (ys as yhd :: ytails) = 228 let 229 val absx = Int.abs (#1 xhd) 230 val absy = Int.abs (#1 yhd) 231 in 232 if absx = absy then 233 (* drop 'yhd' *) 234 xhd :: merge xtails ytails 235 else if absx < absy then 236 xhd :: merge xtails ys 237 else 238 yhd :: merge xs ytails 239 end 240 241(* ------------------------------------------------------------------------- *) 242(* QRESOLVE_CLAUSES: performs propositional resolution of clauses in sequent *) 243(* form, followed by forall-reduction. *) 244(* ------------------------------------------------------------------------- *) 245 246 fun QRESOLVE_CLAUSES ((th1, vars1, hyp1, lits1), 247 (th2, vars2, hyp2, lits2)) = 248 let 249 (* returns the resulting set of literals, along with the pivot as it occurs 250 in lits1 and lits2, respectively; cf. merge *) 251 fun find_pivot acc [] _ = 252 raise ERR "QRESOLVE_CLAUSES" "no pivot literal" 253 | find_pivot acc _ [] = 254 raise ERR "QRESOLVE_CLAUSES" "no pivot literal" 255 | find_pivot acc (lits1 as (hd1 as (i, l1, _)) :: tail1) 256 (lits2 as (hd2 as (j, l2, _)) :: tail2) = 257 if i = ~j then 258 (List.rev acc @ merge tail1 tail2, l1, l2, i > 0) 259 else if i = j then 260 find_pivot (hd1 :: acc) tail1 tail2 261 else if Int.abs i < Int.abs j then 262 find_pivot (hd1 :: acc) tail1 lits2 263 else (* Int.abs j < Int.abs i *) 264 find_pivot (hd2 :: acc) lits1 tail2 265 val (lits, p, p', p_is_pos) = find_pivot [] lits1 lits2 266 267 (* resolution *) 268 val th = (*Profile.profile "resolve"*) (fn () => 269 let 270 val th1 = Thm.DISCH p th1 271 val th2 = Thm.DISCH p' th2 272 in 273 if p_is_pos then 274 Thm.MP th2 (Thm.NOT_INTRO th1) 275 else 276 Thm.MP th1 (Thm.NOT_INTRO th2) 277 end) () 278 279 (* since variables are always bound innermost first, we simply 280 return the larger set -- no need to actually merge *) 281 fun merge_vars (vars1, hyp1) ([], _) = (vars1, hyp1) 282 | merge_vars ([], _) (vars2, hyp2) = (vars2, hyp2) 283 | merge_vars (vars1, hyp1) (vars2, hyp2) = 284 if #1 (List.hd vars1) < #1 (List.hd vars2) then 285 (vars1, hyp1) 286 else 287 (vars2, hyp2) 288 val (vars, hyp) = merge_vars (vars1, hyp1) (vars2, hyp2) 289 in 290 forall_reduce (th, vars, hyp, lits) 291 end 292 293end 294