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