1 2structure minisatProve :> minisatProve = 3struct 4 5local 6 7open Lib boolLib Globals Parse Term Type Thm Drule Conv Feedback FileSys 8open dimacsTools satTools SatSolvers satCommonTools minisatParse satConfig 9 dpll def_cnf 10 11 12in 13 14exception SAT_cex of thm 15 16val mk_sat_oracle_thm = mk_oracle_thm "HolSatLib"; 17 18val sat_warn = ref true (* control interactive warnings *) 19val sat_limit = ref 100 20 (* if > sat_limit clauses then interactive warning if using SML prover *) 21val _ = register_btrace ("HolSatLib_warn",sat_warn); 22 23fun warn ss = 24 if !Globals.interactive andalso !sat_warn 25 then print ("\nHolSat WARNING: "^ss^ 26 "\nTo turn off this warning, type: \ 27 \set_trace \"HolSatLib_warn\" 0; RET\n\n") 28 else () 29 30fun replay_proof is_proved sva nr in_name solver vc clauseth lfn ntm proof = 31 if is_proved then 32 ((case getSolverPostExe solver of (* post-process proof, if required *) 33 SOME post_exe => let 34 val (fin,fout) = (in_name,in_name^"."^(getSolverName solver)) 35 in 36 ignore(Systeml.system_ps 37 (getSolverPostRun solver post_exe (fin,fout))) 38 end 39 | NONE => ()); 40 (case replayProof sva nr in_name solver vc clauseth lfn proof of 41 SOME th => th 42 | NONE => (warn "Proof replay failed. Using internal prover."; 43 DPLL_TAUT (dest_neg ntm)))) (*triv prob/unknown err*) 44 else mk_sat_oracle_thm([ntm],F) 45 46local 47 fun transform_model cnfv lfn model = 48 let val model2 = 49 if isSome cnfv then 50 mapfilter (fn l => let val x = hd(free_vars l) 51 val y = rbapply lfn x 52 in if is_var y then subst [x|->y] l 53 else failwith"" end) model 54 else model 55 in model2 end 56in 57fun invoke_solver solver lfn ntm clauseth cnfv vc is_proved svm sva in_name = 58 let val nr = Array.length clauseth 59 in 60 if access(getSolverExe solver,[A_EXEC]) then 61 let 62 val answer = invokeSat solver T (SOME vc) (SOME nr) svm sva in_name 63 in case answer of 64 SOME model => (* returns |- model ==> ~t *) 65 let val model' = transform_model cnfv lfn model 66 in if is_proved then satCheck model' ntm 67 else mk_sat_oracle_thm([],mk_imp(list_mk_conj model',ntm)) end 68 | NONE => (* returns ~t |- F *) 69 replay_proof is_proved sva nr in_name solver vc clauseth 70 lfn ntm NONE 71 end 72 else (* do not have execute access to solver binary, or it doesn't exist*) 73 (if nr > !sat_limit then 74 warn "SAT solver not found. Using slow internal prover." 75 else (); 76 DPLL_TAUT (dest_neg ntm)) 77 end 78end 79 80(* cleanup temp files. this won't work fully if we cannot delete files 81 generated by the SAT solver *) 82fun clean_delete s = OS.FileSys.remove s handle Interrupt => raise Interrupt 83 | e => () 84(* then raise exception if countermodel was found, 85 else deduce input term from solver's result *) 86fun finalise solver infile is_cnf th tmpname in_name = 87 let val solver_name = getSolverName solver 88 val _ = if isSome infile then () 89 else 90 app clean_delete [ 91 "resolve_trace", (* in case using ZChaff *) 92 in_name, (* CNF *) 93 tmpname,(* tmpfile(created by Poly/ML, but not MoscowML) *) 94 in_name^"."^solver_name, (* result/status *) 95 in_name^"."^solver_name^".proof", (* proof *) 96 in_name^"."^solver_name^".stats" 97 ] 98 val res = 99 if is_imp(concl th) 100 then raise (SAT_cex th) 101 else 102 if is_cnf 103 then (NOT_INTRO(DISCH_ALL th)) 104 else CONV_RULE NOT_NOT_CONV (NOT_INTRO(DISCH_ALL th)) 105 in res end 106 107(* convert input to term to CNF and write out DIMACS file *) 108(* if infile is SOME name, then assume name.cnf exists and is_cnf=true *) 109(* if is_cnf, then assume tm \equiv ~s where s is in CNF *) 110(* if CNF conversion found true or false, return theorem directly *) 111exception initexp of thm; 112fun initialise infile is_cnf tm = 113 let val (cnfv,vc,svm,sva,tmpname,in_name,ntm,lfn,clauseth) = 114 if isSome infile 115 then let val fname = valOf infile 116 val (tm,svm,sva) = genReadDimacs fname 117 val (cnfv,vc,lfn,clauseth) = to_cnf is_cnf (mk_neg tm) 118 in (cnfv,vc,svm,sva,"",fname,mk_neg tm,lfn,clauseth) end 119 else let val (cnfv,vc,lfn,clauseth) = to_cnf is_cnf (mk_neg tm) 120 val (tmpname,cnfname,sva,svm) = 121 generateDimacs (SOME vc) tm (SOME clauseth) 122 (SOME (Array.length clauseth)) 123 in (cnfv,vc,svm,sva,tmpname,cnfname,mk_neg tm,lfn,clauseth) end 124 in if vc=0 then 125 (* no vars: all 'presimp'-ified conjuncts were either T or F *) 126 let val th0 = presimp_conv (dest_neg ntm) 127 in if is_F (rhs (concl th0)) then raise SAT_cex (EQF_ELIM th0) 128 else raise initexp (EQT_ELIM th0) 129 end 130 else 131 (cnfv,vc,svm,sva,tmpname,in_name,ntm,lfn,clauseth) 132 end 133 134val dbg_show_input = ref false; 135 136fun GEN_SAT conf = (* single entry point into HolSatLib *) 137 let val (tm,solver,infile,proof,is_cnf,is_proved) = dest_config conf 138 val _ = if !dbg_show_input then (print "\n"; print_term tm; print "\n") 139 else () 140 val (cnfv,vc,svm,sva,tmpname,in_name,ntm,lfn,clauseth) = 141 initialise infile is_cnf tm 142 val th = if isSome proof 143 then replay_proof is_proved sva (Array.length clauseth) in_name 144 solver vc clauseth lfn ntm proof 145 else invoke_solver solver lfn ntm clauseth cnfv vc 146 is_proved svm sva in_name 147 val res = finalise solver infile is_cnf th tmpname in_name 148 in res end 149 handle initexp th => th 150 151(* default config invokes pre-installed MiniSat 1.14p *) 152fun SAT_PROVE tm = GEN_SAT (set_term tm base_config) 153fun SAT_ORACLE tm = 154 GEN_SAT ((set_term tm o set_flag_is_proved false) base_config) 155 156(* same functionality for ZChaff, if installed by user *) 157val zchaff_config = set_solver zchaff base_config 158fun ZSAT_PROVE tm = GEN_SAT (set_term tm zchaff_config) 159fun ZSAT_ORACLE tm = 160 GEN_SAT ((set_term tm o set_flag_is_proved false) zchaff_config) 161 162end 163end 164