Minisat/minisat_prove.ml

   1 (* open satTools dimacsTools SatSolvers minisatResolve
   2    satCommonTools minisatParse satScript def_cnf *)
   3
   4 (*
   5 for interactive use:
   6
   7    #load "str.cma";;
   8    #use "def_cnf.ml";;
   9    #use "satCommonTools.ml";;
  10    #use "dimacsTools.ml";;
  11    #use "SatSolvers.ml";;
  12    #use "satScript.ml";;
  13    #use "satTools.ml";;
  14    #use "minisatParse.ml";;
  15    #use "minisatResolve.ml";;
  16    #use "minisatProve.ml";;
  17    #use "taut.ml";;
  18 *)
  19 (* ------------------------------------------------------------------------- *)
  20 (* Flag to (de-)activate debugging facilities.                               *)
  21 (* ------------------------------------------------------------------------- *)
  22
  23 let sat_debugging = ref false;;
  24
  25 (* ------------------------------------------------------------------------- *)
  26 (* Split up a theorem according to conjuncts, in a general sense.            *)
  27 (* ------------------------------------------------------------------------- *)
  28
  29 let GCONJUNCTS =
  30   let [pth_ni1; pth_ni2; pth_no1; pth_no2; pth_an1; pth_an2; pth_nn] =
  31     (map UNDISCH_ALL o CONJUNCTS o TAUT)
  32     `(~(p ==> q) ==> p) /\
  33      (~(p ==> q) ==> ~q) /\
  34      (~(p \/ q) ==> ~p) /\
  35      (~(p \/ q) ==> ~q) /\
  36      (p /\ q ==> p) /\
  37      (p /\ q ==> q) /\
  38      (~ ~p ==> p)` in
  39   let p_tm = concl pth_an1 and q_tm = concl pth_an2 in
  40   let rec GCONJUNCTS th acc =
  41     match (concl th) with
  42       Comb(Const("~",_),Comb(Comb(Const("==>",_),p),q)) ->
  43        GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_ni1))
  44                   (GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_ni2))
  45                               acc)
  46     | Comb(Const("~",_),Comb(Comb(Const("\\/",_),p),q)) ->
  47        GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_no1))
  48                   (GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_no2))
  49                               acc)
  50     | Comb(Comb(Const("/\\",_),p),q) ->
  51        GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_an1))
  52                   (GCONJUNCTS (PROVE_HYP th (INST [p,p_tm; q,q_tm] pth_an2))
  53                               acc)
  54     | Comb(Const("~",_),Comb(Const("~",_),p)) ->
  55           GCONJUNCTS (PROVE_HYP th (INST [p,p_tm] pth_nn)) acc
  56     | _ -> th::acc in
  57   fun th -> GCONJUNCTS th [];;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* Generate fresh variable names (could just use genvars).                   *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let propvar i = mk_var("x"^string_of_int i,bool_ty);;
  64
  65 (* ------------------------------------------------------------------------- *)
  66 (* Set up the basic definitional arrangement.                                *)
  67 (* ------------------------------------------------------------------------- *)
  68
  69 let rec localdefs tm (n,defs,lfn) =
  70   if is_neg tm then
  71     let n1,v1,defs1,lfn1 = localdefs (rand tm) (n,defs,lfn) in
  72     let tm' = mk_neg v1 in
  73     try (n1,apply defs1 tm',defs1,lfn1) with Failure _ ->
  74     let n2 = n1 + 1 in
  75     let v2 = propvar n2 in
  76     n2,v2,(tm' |-> v2) defs1,(v2 |-> tm) lfn1
  77   else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
  78     let n1,v1,defs1,lfn1 = localdefs (lhand tm) (n,defs,lfn) in
  79     let n2,v2,defs2,lfn2 = localdefs (rand tm) (n1,defs1,lfn1) in
  80     let tm' = mk_comb(mk_comb(rator(rator tm),v1),v2) in
  81     try (n2,apply defs2 tm',defs2,lfn2) with Failure _ ->
  82     let n3 = n2 + 1 in
  83     let v3 = propvar n3 in
  84     n3,v3,(tm' |-> v3) defs2,(v3 |-> tm) lfn2
  85   else try (n,apply defs tm,defs,lfn) with Failure _ ->
  86        let n1 = n + 1 in
  87        let v1 = propvar n1 in
  88        n1,v1,(tm |-> v1) defs,(v1 |-> tm) lfn;;
  89
  90 (* ------------------------------------------------------------------------- *)
  91 (* Just translate to fresh variables, but otherwise leave unchanged.         *)
  92 (* ------------------------------------------------------------------------- *)
  93
  94 let rec transvar (n,tm,vdefs,lfn) =
  95   if is_neg tm then
  96     let n1,tm1,vdefs1,lfn1 = transvar (n,rand tm,vdefs,lfn) in
  97     n1,mk_comb(rator tm,tm1),vdefs1,lfn1
  98   else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
  99     let n1,tm1,vdefs1,lfn1 = transvar (n,lhand tm,vdefs,lfn) in
 100     let n2,tm2,vdefs2,lfn2 = transvar (n1,rand tm,vdefs1,lfn1) in
 101     n2,mk_comb(mk_comb(rator(rator tm),tm1),tm2),vdefs2,lfn2
 102   else try n,apply vdefs tm,vdefs,lfn with Failure _ ->
 103        let n1 = n + 1 in
 104        let v1 = propvar n1 in
 105        n1,v1,(tm |-> v1) vdefs,(v1 |-> tm) lfn;;
 106
 107 (* ------------------------------------------------------------------------- *)
 108 (* Flag to choose whether to exploit existing conjunctive structure.         *)
 109 (* ------------------------------------------------------------------------- *)
 110
 111 let exploit_conjunctive_structure = ref true;;
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* Check if something is clausal (slightly stupid).                          *)
 115 (* ------------------------------------------------------------------------- *)
 116
 117 let is_literal tm = is_var tm or is_neg tm & is_var(rand tm);;
 118
 119 let is_clausal tm =
 120   let djs = disjuncts tm in
 121   forall is_literal djs & list_mk_disj djs = tm;;
 122
 123 (* ------------------------------------------------------------------------- *)
 124 (* Now do the definitional arrangement but not wastefully at the top.        *)
 125 (* ------------------------------------------------------------------------- *)
 126
 127 let definitionalize =
 128   let transform_imp =
 129     let pth = TAUT `(p ==> q) <=> ~p \/ q` in
 130     let ptm = rand(concl pth) in
 131     let p_tm = rand(lhand ptm) and q_tm = rand ptm in
 132     fun th -> let ip,q = dest_comb(concl th) in
 133               let p = rand ip in
 134               EQ_MP (INST [p,p_tm; q,q_tm] pth) th
 135   and transform_iff_1 =
 136     let pth = UNDISCH(TAUT `(p <=> q) ==> (p \/ ~q)`) in
 137     let ptm = concl pth in
 138     let p_tm = lhand ptm and q_tm = rand(rand ptm) in
 139     fun th -> let ip,q = dest_comb(concl th) in
 140               let p = rand ip in
 141               PROVE_HYP th (INST [p,p_tm; q,q_tm] pth)
 142   and transform_iff_2 =
 143     let pth = UNDISCH(TAUT `(p <=> q) ==> (~p \/ q)`) in
 144     let ptm = concl pth in
 145     let p_tm = rand(lhand ptm) and q_tm = rand ptm in
 146     fun th -> let ip,q = dest_comb(concl th) in
 147               let p = rand ip in
 148               PROVE_HYP th (INST [p,p_tm; q,q_tm] pth) in
 149   let definitionalize th (n,tops,defs,lfn) =
 150     let t = concl th in
 151     if is_clausal t then
 152       let n',v,defs',lfn' = transvar (n,t,defs,lfn) in
 153       (n',(v,th)::tops,defs',lfn')
 154     else if is_neg t then
 155        let n1,v1,defs1,lfn1 = localdefs (rand t) (n,defs,lfn) in
 156        (n1,(mk_neg v1,th)::tops,defs1,lfn1)
 157     else if is_disj t then
 158       let n1,v1,defs1,lfn1 = localdefs (lhand t) (n,defs,lfn) in
 159       let n2,v2,defs2,lfn2 = localdefs (rand t) (n1,defs1,lfn1) in
 160       (n2,(mk_disj(v1,v2),th)::tops,defs2,lfn2)
 161     else if is_imp t then
 162       let n1,v1,defs1,lfn1 = localdefs (lhand t) (n,defs,lfn) in
 163       let n2,v2,defs2,lfn2 = localdefs (rand t) (n1,defs1,lfn1) in
 164       (n2,(mk_disj(v1,v2),transform_imp th)::tops,defs2,lfn2)
 165     else if is_iff t then
 166       let n1,v1,defs1,lfn1 = localdefs (lhand t) (n,defs,lfn) in
 167       let n2,v2,defs2,lfn2 = localdefs (rand t) (n1,defs1,lfn1) in
 168       (n2,(mk_disj(v1,mk_neg v2),transform_iff_1 th)::
 169           (mk_disj(mk_neg v1,v2),transform_iff_2 th)::tops,defs2,lfn2)
 170     else
 171       let n',v,defs',lfn' = localdefs t (n,defs,lfn) in
 172       (n',(v,th)::tops,defs',lfn') in
 173   definitionalize;;
 174
 175 (* SAT_PROVE is the main interface function.
 176    Takes in a term t and returns thm or exception if not a taut *)
 177 (* invokes minisatp, returns |- t  or |- model ==> ~t *)
 178
 179 (* if minisatp proof log does not exist after minisatp call returns,
 180    we will assume that minisatp discovered UNSAT during the read-in
 181    phase and did not bother with a proof log.
 182    In that case the problem is simple and can be delegated to TAUT *)
 183
 184 (* FIXME: I do not like the TAUT solution;
 185    what is trivial for Minisat may not be so for TAUT *)
 186
 187 exception Sat_counterexample of thm;;
 188
 189 (* delete temporary files *)
 190 (* if zChaff was used, also delete hard-wired trace filenames*)
 191 let CLEANUP fname solvername =
 192   let delete fname = try Sys.remove fname with Sys_error _ -> () in
 193   (delete fname;
 194    delete (fname^".cnf");
 195    delete (fname^"."^solvername);
 196    delete (fname^"."^solvername^".proof");
 197    delete (fname^"."^solvername^".stats");
 198    if solvername="zchaff" then
 199      (delete(Filename.concat (!temp_path) "resolve_trace");
 200       delete(Filename.concat (!temp_path) "zc2mso_trace"))
 201    else ());;
 202
 203 let GEN_SAT_PROVE solver solvername =
 204   let false_tm = `F`
 205   and presimp_conv = GEN_REWRITE_CONV DEPTH_CONV
 206    [NOT_CLAUSES; AND_CLAUSES; OR_CLAUSES; IMP_CLAUSES; EQ_CLAUSES]
 207   and p_tm = `p:bool` and q_tm = `q:bool`
 208   and pth_triv = TAUT `(~p <=> F) <=> p`
 209   and pth_main = UNDISCH_ALL(TAUT `(~p <=> q) ==> (q ==> F) ==> p`) in
 210   let triv_rule p th = EQ_MP(INST [p,p_tm] pth_triv) th
 211   and main_rule p q sth th =
 212     itlist PROVE_HYP [sth; DISCH_ALL th] (INST [p,p_tm; q,q_tm] pth_main) in
 213   let invoke_minisat lfn mcth stm t rcv vc =
 214     let nr = Array.length rcv in
 215     let res = match invokeSat solver None t (Some vc) with
 216       Some model ->
 217         let model2 =
 218           mapfilter (fun l -> let x = hd(frees l) in
 219                               let y = apply lfn x in
 220                               if is_var y then vsubst [y,x] l else fail())
 221                     model in
 222           satCheck model2 stm
 223     | None ->
 224       (match parseMinisatProof nr ((!tmp_name)^"."^solvername^".proof") vc rcv with
 225          Some (cl,sk,scl,srl,cc) ->
 226             unsatProveResolve lfn mcth (cl,sk,srl) (* returns p |- F *)
 227       | None -> UNDISCH(TAUT(mk_imp(stm,false_tm)))) in
 228     res in
 229   fun tm ->
 230     let sth = presimp_conv (mk_neg tm) in
 231     let stm = rand(concl sth) in
 232     if stm = false_tm then triv_rule tm sth else
 233     let th = ASSUME stm in
 234     let ths = if !exploit_conjunctive_structure then GCONJUNCTS th
 235               else [th] in
 236     let n,tops,defs,lfn =
 237       itlist definitionalize ths (-1,[],undefined,undefined) in
 238     let defg = foldl (fun a t nv -> (t,nv)::a) [] defs in
 239     let mdefs = filter (fun (r,_) -> not (is_var r)) defg in
 240     let eqs = map (fun (r,l) -> mk_iff(l,r)) mdefs in
 241     let clausify eq cls =
 242       let fvs = frees eq and eth = (NNFC_CONV THENC CNF_CONV) eq in
 243       let tth = INST (map (fun v -> apply lfn v,v) fvs) eth in
 244       let xth = ADD_ASSUM stm (EQ_MP tth (REFL(apply lfn (lhand eq)))) in
 245       zip (conjuncts(rand(concl eth))) (CONJUNCTS xth) @ cls in
 246     let all_clauses = itlist clausify eqs tops in
 247     let mcth = itlist (fun (c,th) m -> Termmap.add c th m) all_clauses
 248                       Termmap.empty in
 249     let vc = n + 1 in
 250     let rcv = Array.of_list (map fst all_clauses) in
 251     let ntdcnf = list_mk_conj (map fst all_clauses) in
 252     let th = invoke_minisat lfn mcth stm ntdcnf rcv vc in
 253     (if not (!sat_debugging) then CLEANUP (!tmp_name) solvername else ();
 254     if is_imp(concl th)
 255     then raise (Sat_counterexample
 256       (EQ_MP (AP_TERM (rator(concl th)) (SYM sth)) th))
 257     else main_rule tm stm sth th);;
 258
 259 let SAT_PROVE = GEN_SAT_PROVE minisatp "minisatp";;
 260
 261 let ZSAT_PROVE = GEN_SAT_PROVE zchaff "zchaff";;