1
2structure satTools = struct
3
4local
5
6(*
7app load ["Binaryset","FileSys","TextIO","Process","Char","String","Substring","Conv"]
8*)
9
10open Lib boolLib Globals Parse Term Type Thm Drule Psyntax Conv Feedback
11open SatSolvers satCommonTools satTheory
12
13
14in
15
16infix |->;
17
18(*
19** Use Binaryset to encode mapping between HOL variable names
20** and DIMACS  variable numbers as a set of string*int pairs.
21*)
22
23(* Functions for parsing the output of SAT solvers *)
24
25(*
26** substringContains s ss
27** tests whether substring ss contains string s
28*)
29
30fun substringContains s ss = not(Substring.isEmpty(snd(Substring.position s ss)));
31
32(*
33** parseSat (s1,s2) ss
34** returns a list of numbers corresponding to the tokenised
35** substring of ss (tokenised wrt Char.isSpace) that starts immediately
36** after the first occurrence of s1 and ends just before the first
37** occurrence of s2 that is after the first occurrence of s1
38*)
39
40fun parseSat (s1,s2) ss =
41 let val (ss1,ss2) = Substring.position s1 ss
42     val ss3       = Substring.triml (String.size s1) ss2
43     val (ss4,ss5) = Substring.position s2 ss3
44     val ssl       = Substring.tokens Char.isSpace ss4
45 in
46  List.map (valOf o Int.fromString o Substring.string) ssl
47 end
48 handle _ => failwith("parseSat");
49
50(*
51** Test for success of the result of Process.system
52** N.B. isSuccess expected to primitive in next release of
53** Moscow ML, and Process.status will lose eqtype status
54*)
55
56fun isSuccess s = Process.isSuccess s
57
58(*
59** invokeSat solver t
60** invokes solver on t and returns SOME s (where s is the satisfying instance
61** as a string of integers) or NONE, if unsatisfiable
62*)
63
64fun sat_sysl s = Systeml.system_ps s
65
66fun invokeSat sat_solver tm vc nr svm sva infile =
67 let
68      val (name,executable,notime_run,only_true,
69          failure_string,start_string,end_string) =
70         (getSolverName sat_solver,getSolverExe sat_solver,getSolverRun sat_solver,
71          getSolverTrue sat_solver,getSolverFail sat_solver,getSolverStart sat_solver,
72          getSolverEnd sat_solver)
73     val outfile    = infile ^ "." ^ name
74     val run_cmd    = notime_run executable (infile,outfile)
75     val code       = sat_sysl run_cmd
76     val _          = if isSuccess code orelse
77                         (name="minisat" orelse name="minisatp")
78                      then () (* minisat returns non-std exit code on success *)
79                      else print("Warning:\n Process.system reports failure \
80                                 \signal returned by\n " ^ run_cmd ^ "\n")
81     val ins        = TextIO.openIn outfile
82     val sat_res_ss = Substring.full (TextIO.inputAll ins)
83     val _          = TextIO.closeIn ins
84     val result     = substringContains failure_string sat_res_ss
85 in
86  if result
87   then NONE
88   else
89    let val model1 = parseSat (start_string,end_string) sat_res_ss
90        val model2 = if only_true
91                      then model1 @
92                           (map (fn n => 0-n)
93                                (subtract (map snd (snd(dimacsTools.showSatVarMap svm))) model1))
94                     else model1
95    in let val model3 = SOME(map (dimacsTools.intToLiteral sva) model2)
96        in model3 end
97    end
98 end
99handle Io _ => NONE
100
101(*
102** satCheck [l1,...,ln] t
103** attempts to prove (l1 /\ ... /\ ln) ==> t
104** if it succeeds then the theorem is returned, else
105** exception satCheckError is raised
106*)
107
108exception satCheckError;
109fun satCheck model t =
110   let
111      val mtm  = list_mk_conj model (*  (l1 /\ ... /\ ln) *)
112      val th1  = ASSUME mtm (* l1 /\ ... /\ ln |- l1 /\ ... /\ ln *)
113      val thl  = map
114                  (fn th => if is_neg(concl th)
115                             then MP (SPEC (dest_neg(concl th))EQF_Imp1) th
116                             else MP (SPEC(concl th)EQT_Imp1) th)
117                  (CONJUNCTS th1) (* [ l1 /\ ... /\ ln |- l1 = T, ... ] *)
118      val subl = map (fn th => lhs(concl th) |-> th) thl (*[l1 |-> l1 /\ ... /\ ln |- l1 = T,...]*)
119      val th2 = SUBST_CONV subl t t (* l1 /\ ... /\ ln |- t = t[l1/T,...] *)
120      val th3 = CONV_RULE (RHS_CONV computeLib.EVAL_CONV) th2 (* l1 /\ ... /\ ln |- t = T *)
121      val th4 = EQT_ELIM th3 (* l1 /\ ... /\ ln |- t *)
122   in
123      DISCH mtm th4 (* |- l1 /\ ... /\ ln ==> t *)
124   end
125   handle Interrupt => raise Interrupt
126        | HOL_ERR {origin_function = "EQT_ELIM", ...} =>
127             if is_neg t
128                then UNDISCH (EQF_ELIM (REWRITE_CONV [] t))
129                     handle HOL_ERR _ => raise satCheckError
130             else raise satCheckError
131        |  _ => raise satCheckError;
132
133end
134end
135