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