1 (*open satCommonTools dimacsTools minisatParse satScript*)
3 (* functions for replaying minisat proof LCF-style.
4 Called from minisatProve.ml after proof log has
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));;
20 h0::h1::t -> (h0,h1,t)
21 | _ -> failwith("Match failure in l2hh");;
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
28 let get_var_num lfn v = lookup_sat_var v - 1;;
30 (* mcth maps clause term t to thm of the form cnf |- t, *)
31 (* where t is a clause of the cnf term *)
33 let pth_and = TAUT `F \/ F <=> F` and pth_not = TAUT `~T <=> F` in
34 let rec REFUTE_DISJ tm =
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
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
47 EQ_MP (INSTANTIATE_ALL_UNDERLYING(REFUTE_DISJ t))
48 (Termmap.find t mcth),t_tm,TRUTH;;
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
57 (* will return clause info at index ci *)
59 exception Fn_get_clause__match;;
60 exception Fn_get_root_clause__match;;
62 (* will return clause info at index ci *)
63 let getRootClause cl ci =
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
70 (* will return clause thm at index ci *)
72 let getClause lfn mcth cl ci =
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
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) *)
87 let pth = UNDISCH(TAUT `F ==> p`) in
89 and f_tm = hd(hyp pth) in
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
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
105 let resolveChain lfn mcth cl rci =
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
117 resolveClause lfn mcth cl vi rci (ci,rci))
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
126 match (Array.get cl (srl-1)) with
128 | _ -> failwith("unsatProveTrace") in