1structure QbfConv :> QbfConv = struct
2
3  open Canon Conv Feedback boolSyntax
4
5  local open Tactical bossLib simpLib boolSimps boolTheory Thm
6    val QMETIS_TAC = Feedback.trace ("metis", 0) (METIS_TAC [])
7    val th1 = Tactical.prove(``(!x. (x \/ P)) = P``, QMETIS_TAC)
8    val th2 = prove(``(!x. (~x \/ P)) = P``,SIMP_TAC bool_ss [])
9    val th3 = SYM F_DEF
10    val th4 = prove(``(!x. ~x) = F``,SIMP_TAC bool_ss [])
11    val th5 = AC DISJ_COMM DISJ_ASSOC
12    val th6 = AC CONJ_COMM CONJ_ASSOC
13  in
14    val simp_clauses = SIMP_CONV bool_ss [th1,th2,th3,th4,th5,th6]
15  end
16
17  local
18    open boolSyntax boolTheory markerLib
19    fun literal x t = t = x orelse dest_neg t = x handle HOL_ERR _ => false
20  in
21    val remove_forall =
22      Ho_Rewrite.PURE_REWRITE_CONV [FORALL_AND_THM] THENC
23      EVERY_CONJ_CONV (fn t =>
24        let val (x,_) = dest_forall t in
25          CHANGED_CONV (Rewrite.PURE_REWRITE_CONV [FORALL_SIMP])
26            ORELSEC
27          QUANT_CONV (move_disj_left (literal x))
28        end t) THENC
29      simp_clauses
30  end
31
32  fun last_quant_conv c = let
33    exception Innermost
34    fun f t =
35      QUANT_CONV f t handle
36        HOL_ERR {origin_function="RAND_CONV",...} => raise Innermost
37      | Innermost => c t
38  in f end
39
40  fun strip_prefix_conv c = let
41    fun f tm =
42      (if is_forall tm orelse is_exists tm
43       then STRIP_QUANT_CONV f
44       else c) tm
45  in f end
46
47  fun last_quant_seq_conv cq cb = let
48    fun f t =
49      (QUANT_CONV f THENC cq) t handle
50        HOL_ERR {origin_function="RAND_CONV",...} => cb t
51  in f end
52
53  fun last_forall_seq_conv cq cb = let
54    exception Innermost
55    fun f tm =
56      if is_exists tm then STRIP_QUANT_CONV f tm
57      else if is_forall tm then
58        STRIP_QUANT_CONV
59          (fn t => if is_exists t then f t else raise Innermost)
60          tm
61        handle Innermost => last_quant_seq_conv cq cb tm
62      else cb tm
63  in f end
64
65  val qbf_prenex_conv =
66    (* remove equalities THENC *)
67    PRENEX_CONV THENC
68    (last_forall_seq_conv
69       remove_forall
70       (NNF_CONV NO_CONV true THENC
71        PROP_CNF_CONV THENC
72        simp_clauses))
73
74end
75