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