1signature QbfConv = sig 2 type conv = Abbrev.conv 3 4 (* put an arbitrary QBF into the required form *) 5 (* specifically, 6 input term: 7 - has type bool 8 - is closed 9 - contains only: 10 - first order connectives (/\,\/,==>,~) 11 (TODO: allow equality?) 12 - quantifiers (!,?) 13 - variables 14 output term: 15 - of the form Q_1 x_1. ... Q_n x_n. phi 16 - each Q_i is either ! or ? 17 - Q_n is ? 18 - each x_i appears in phi 19 - phi is closed and in CNF 20 alternatively, the output term might simply be 'T' or 'F' 21 *) 22 val qbf_prenex_conv : conv 23 24 (* simplifies clauses (specialisation of SIMP_CONV). In particular, does the following rewrites: 25 (���x. x ��� P) = P, (���x. ��x ��� P) = P, (���x. x) = F, (���x. ��x) = F, (UOK) 26 and associativity/commutativity normalisation for conjunction and disjunction *) 27 val simp_clauses : conv 28 29 (* conversion that takes [!x:bool. t] where t is in CNF and may contain x and 30 removes the quantifier and all occurrences of x. also simplifies clauses (as above). *) 31 val remove_forall : conv 32 33 (* [last_quant_conv c] strips a quantifier (! and ? only) prefix down 34 to the last quantifier then applies c to the (singly quantified) body *) 35 val last_quant_conv : conv -> conv 36 37 (* applies a conversion under a quantifier prefix of foralls and exists *) 38 val strip_prefix_conv : conv -> conv 39 40 (* [last_quant_seq_conv cq cb] applies cb under the quantifier prefix and 41 then cq before each quantifier. That is: 42 Q1 x1. Q2 x2. ... Qn xn. P --> cq (Q1 x1. cq (Q2 x2. ... cq (Qn. xn. cb P)))) 43 *) 44 val last_quant_seq_conv : conv -> conv -> conv 45 46 (* applies cb under the quantifier prefix, and then, if the innermost 47 quantifiers are all universal, applies cq before each of them *) 48 val last_forall_seq_conv : conv -> conv -> conv 49 50end 51