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