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