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