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