1
2structure minisatResolve = struct
3
4local
5
6open Globals Parse HolKernel
7open Array boolSyntax boolTheory Drule Conv Rewrite
8open satCommonTools dimacsTools satTheory
9
10
11in
12
13fun l2hh (h0::h1::t) = (h0,h1,t)
14  | l2hh _ = raise Match
15
16(*+1 because minisat var numbers start at 0,SatLib at 1*)
17fun mk_sat_var lfn sva n =
18    let val rv = Array.sub(sva,n+1)
19        handle Subscript => failwith("mk_sat_var"^(int_to_string (n+1))^"\n")
20    in rbapply lfn rv handle NotFound => rv end
21
22local
23
24val A = mk_var("A",bool)
25val B = mk_var("B",bool)
26val AND_INV_IMP2 = SPEC_ALL AND_INV_IMP
27fun INSTANTIATE_UNDERLYING lfn th =
28    let val fvs = HOLset.listItems (hyp_frees th)
29        val tms = map (fn v => tryrbapplyd lfn v v) fvs
30    in INST (map2 (fn t => fn fv => fv |-> t) tms fvs) th end
31in
32
33(* let
34     - xi denote cnf definition variables such that pi is the rhs of the
35       definition
36     - clauseth[i] gives i'th clause of CNF, as a pair (t,[tm] |- t')
37   where t = (x0 \/ ... \/ xn) and t' = (p0 \/ ... \/ pn),
38   i.e. the "expanded" t
39*)
40fun dualise lfn orc clauseth ci =
41    let
42      fun dualise' th =
43          let
44            val c = rand (land (concl th))
45          in
46            if is_disj c then
47              let val (d0,d1) = dest_disj c
48                  val th1 =
49                      if is_neg d0
50                      then EQ_MP (INST [A |-> dest_neg d0,B |-> d1] OR_DUAL3) th
51                      else EQ_MP (INST [A|->d0,B |-> d1] OR_DUAL2) th
52              in dualise' (UNDISCH th1) end
53            else
54              UNDISCH (if is_neg c
55                       then CONV_RULE (LAND_CONV NOT_NOT_CONV) th
56                       else MP (INST [A |-> c] AND_INV2) th)
57            end
58        val (t1,th1) = Array.sub(clauseth,orc) (* t, [tm] |- t') *)
59            handle Subscript => failwith("dualise"^(int_to_string (ci))^"\n")
60        val res =
61            if RBM.numItems lfn = 0 then
62              (* original problem in CNF, so th1 is [tm] |- t *)
63              let val th2 = MP (INST [A|->t1] AND_INV_IMP2) th1
64                               (*[tm] |- ~t ==> F*)
65              in dualise' th2 end
66            else (* [~p0,...,~pn,tm] |- F *)
67              let val th2 = MP (INST [A|->t1] AND_INV_IMP2) (ASSUME t1)
68                            (*[tm,t] |- ~t ==> F *)
69                  val dth =  dualise' th2 (* [~x0,...,~xn,tm,t] |- F *)
70              in
71                PROVE_HYP th1 (INSTANTIATE_UNDERLYING lfn dth)
72              end (* [~p0,...,~pn,tm] |- F *)
73     in res end
74end
75
76(* convert clause term to dualised thm form on first use *)
77fun prepareRootClause lfn orc clauseth cl ci =
78    let
79        val th = dualise lfn orc clauseth ci
80        val _ = Dynarray.update(cl,ci,th)
81     in th end
82
83(* will return clause thm at index ci *)
84fun getClause cl ci = Dynarray.sub(cl,ci)
85    handle Subscript => failwith("getClause"^(int_to_string (ci))^"\n")
86
87(* ground resolve clauses c0 and c1 on v,
88   where v is the only var that occurs with opposite signs in c0 and c1 *)
89(* if n0 then v negated in c0 (but remember we are working with dualised
90   clauses)*)
91fun resolve v n0 rth0 rth1 =
92    let
93        val th' = if n0 then DISCH v rth0 else DISCH v rth1
94        val th = PROVE_HYP th' (if n0 then rth1 else rth0)
95     in th end
96
97val counter = ref 0
98
99(* resolve c0 against c1 wrt v *)
100fun resolveClause lfn sva cl piv rth0 c1i =
101    let
102      val rth1 = getClause cl c1i
103      (* piv is the pivot lit in c1i. if piv mode 2 = 0, then must be
104         negated in c0i *)
105      val n0 = (piv mod 2 = 0)
106      val v = mk_sat_var lfn sva (piv div 2)
107      val rth  = resolve v n0 rth0 rth1
108      val _ = (counter:=(!counter)+1)
109    in rth end
110
111fun resolveChain lfn sva cl (nl,lnl) rci =
112    let val ((_,c0i),(vi,c1i),nlt) = l2hh nl
113        val r0 = getClause cl c0i
114        val r1 = resolveClause lfn sva cl vi r0 c1i
115        val res = List.foldl (fn ((vi,ci),th) =>
116                                 resolveClause lfn sva cl vi th ci) r1 nlt
117        val _ = Dynarray.update(cl,rci,res)
118    in () end
119
120end
121end
122