Minisat/minisat_resolve.ml

   1 (*open satCommonTools dimacsTools minisatParse satScript*)
   2
   3 (* functions for replaying minisat proof LCF-style.
   4    Called from minisatProve.ml after proof log has
   5    been parsed. *)
   6
   7 (* p is a literal *)
   8 let toVar p =
   9   if is_neg p
  10   then rand p
  11   else p;;
  12
  13 let (NOT_NOT_ELIM,NOT_NOT_CONV) =
  14   let t = mk_var("t",bool_ty) in
  15   let NOT_NOT2 = SPEC_ALL NOT_NOT in
  16   ((fun th -> EQ_MP (INST [rand(rand(concl th)),t] NOT_NOT2) th),
  17    (fun tm -> INST [rand(rand tm),t] NOT_NOT2));;
  18
  19 let l2hh = function
  20     h0::h1::t -> (h0,h1,t)
  21   |  _ -> failwith("Match failure in l2hh");;
  22
  23 (*+1 because minisat var numbers start at 0, dimacsTools at 1*)
  24 let mk_sat_var lfn n =
  25   let rv = lookup_sat_num (n+1) in
  26   tryapplyd lfn rv rv;;
  27
  28 let get_var_num lfn v = lookup_sat_var v - 1;;
  29
  30 (* mcth maps clause term t to thm of the form cnf |- t, *)
  31 (*  where t is a clause of the cnf term                 *)
  32 let dualise =
  33   let pth_and = TAUT `F \/ F <=> F` and pth_not = TAUT `~T <=> F` in
  34   let rec REFUTE_DISJ tm =
  35     match tm with
  36       Comb(Comb(Const("\\/",_) as op,l),r) ->
  37         TRANS (MK_COMB(AP_TERM op (REFUTE_DISJ l),REFUTE_DISJ r)) pth_and
  38     | Comb(Const("~",_) as l,r) ->
  39         TRANS (AP_TERM l (EQT_INTRO(ASSUME r))) pth_not
  40     | _ ->
  41         ASSUME(mk_iff(tm,f_tm)) in
  42   fun lfn -> let INSTANTIATE_ALL_UNDERLYING th =
  43              let fvs = thm_frees th in
  44              let tms = map (fun v -> tryapplyd lfn v v) fvs in
  45              INST (zip tms fvs) th in
  46              fun mcth t ->
  47                EQ_MP (INSTANTIATE_ALL_UNDERLYING(REFUTE_DISJ t))
  48                      (Termmap.find t mcth),t_tm,TRUTH;;
  49
  50
  51 (* convert clause term to dualised thm form on first use *)
  52 let prepareRootClause lfn mcth cl (t,lns) ci =
  53     let (th,dl,cdef) = dualise lfn mcth t in
  54     let _ = Array.set cl ci (Root (Rthm (th,lns,dl,cdef))) in
  55     (th,lns);;
  56
  57 (* will return clause info at index ci *)
  58
  59 exception Fn_get_clause__match;;
  60 exception Fn_get_root_clause__match;;
  61
  62 (* will return clause info at index ci *)
  63 let getRootClause cl ci =
  64   let res =
  65     match (Array.get cl ci) with
  66       Root (Rthm (t,lns,dl,cdef)) -> (t,lns,dl,cdef)
  67     | _ -> raise Fn_get_root_clause__match in
  68   res;;
  69
  70 (* will return clause thm at index ci *)
  71
  72 let getClause lfn mcth cl ci =
  73   let res =
  74     match (Array.get cl ci) with
  75       Root (Ll (t,lns)) -> prepareRootClause lfn mcth cl (t,lns) ci
  76     | Root (Rthm (t,lns,dl,cdef)) -> (t,lns)
  77     | Chain _ -> raise Fn_get_clause__match
  78     | Learnt (th,lns) ->  (th,lns)
  79     | Blank -> raise Fn_get_clause__match in
  80   res;;
  81
  82 (* ground resolve clauses c0 and c1 on v,
  83    where v is the only var that occurs with opposite signs in c0 and c1 *)
  84 (* if n0 then v negated in c0 *)
  85 (*   (but remember we are working with dualised clauses) *)
  86 let resolve =
  87   let pth = UNDISCH(TAUT `F ==> p`) in
  88   let p = concl pth
  89   and f_tm = hd(hyp pth) in
  90   fun v n0 rth0 rth1 ->
  91     let th0 = DEDUCT_ANTISYM_RULE (INST [v,p] pth) (if n0 then rth0 else rth1)
  92     and th1 = DEDUCT_ANTISYM_RULE (INST [mk_iff(v,f_tm),p] pth)
  93                                   (if n0 then rth1 else rth0) in
  94     EQ_MP th1 th0;;
  95
  96 (* resolve c0 against c1 wrt v *)
  97 let resolveClause lfn mcth cl vi rci (c0i,c1i) =
  98   let ((rth0,lns0),(rth1,lns1)) = pair_map (getClause lfn mcth cl) (c0i,c1i) in
  99   let piv = mk_sat_var lfn vi in
 100   let n0 = mem piv (hyp rth0) in
 101   let rth  = resolve piv n0 rth0 rth1 in
 102   let _ = Array.set cl rci (Learnt (rth,lns0)) in
 103   ();;
 104
 105 let resolveChain lfn mcth cl rci =
 106     let (nl,lnl) =
 107       match (Array.get cl rci) with
 108         Chain (l,ll) -> (l,ll)
 109       | _            -> failwith("resolveChain") in
 110     let (vil,cil) = unzip nl in
 111     let vil = tl vil in (* first pivot var is actually dummy value -1 *)
 112     let (c0i,c1i,cilt) = l2hh cil in
 113     let _ = resolveClause lfn mcth cl (List.hd vil) rci (c0i,c1i) in
 114     let _ =
 115       List.iter
 116         (fun (vi,ci) ->
 117           resolveClause lfn mcth cl vi rci (ci,rci))
 118         (tl (tl nl)) in
 119     ();;
 120
 121 (* rth should be A |- F, where A contains all and only *)
 122 (* the root clauses used in the proof                  *)
 123 let unsatProveResolve lfn mcth (cl,sk,srl) =
 124   let _ = List.iter (resolveChain lfn mcth cl) (List.rev sk) in
 125   let rth =
 126     match (Array.get cl (srl-1)) with
 127       Learnt (th,_) -> th
 128     | _ -> failwith("unsatProveTrace") in
 129   rth;;