1(* ========================================================================= *) 2(* INTERFACE TO TPTP PROBLEM FILES *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["mlibStream", "mlibUseful", "mlibParser", "mlibTerm", "mlibSubst"]; 8*) 9 10(* 11*) 12structure mlibTptp :> mlibTptp = 13struct 14 15open mlibParser mlibUseful mlibTerm; 16 17infixr 9 >>++; 18infixr 8 ++; 19infixr 7 >>; 20infixr 6 ||; 21infix |-> ## ::>; 22 23structure S = mlibStream; local open mlibStream in end; 24 25val |<>| = mlibSubst.|<>|; 26val op ::> = mlibSubst.::>; 27val term_subst = mlibSubst.term_subst; 28 29(* ------------------------------------------------------------------------- *) 30(* Abbreviating relation and function names in TPTP problems. *) 31(* ------------------------------------------------------------------------- *) 32 33type rename = {tptp : string, fol : string, arity : int}; 34 35val renaming : rename list ref = ref 36 [(* Mapping TPTP functions to nice symbols *) 37 {tptp = "equal", fol = "=", arity = 2}, 38 {tptp = "equalish", fol = "==", arity = 2}, 39 {tptp = "less_equal", fol = "<=", arity = 2}, 40 {tptp = "multiply", fol = "*", arity = 2}, 41 {tptp = "divide", fol = "/", arity = 2}, 42 {tptp = "add", fol = "+", arity = 2}, 43 {tptp = "subtract", fol = "-", arity = 2}, 44 45 (* Mapping HOL symbols to TPTP alphanumerics *) 46 {tptp = "bool", fol = "$", arity = 1}, 47 {tptp = "type", fol = ":", arity = 2}, 48 {tptp = "apply", fol = "%", arity = 2}] 49 50(* ------------------------------------------------------------------------- *) 51(* Reading from a TPTP file in CNF/FOF format: pass in a filename. *) 52(* ------------------------------------------------------------------------- *) 53 54val comment = equal #"%" o hd o explode; 55 56val input_lines = S.filter (non comment) o S.from_textfile; 57 58val input_chars = S.flatten o S.map (S.from_list o explode); 59 60datatype tok_type = Lower | Upper | Punct; 61 62local 63 fun f [] = raise Bug "exact_puncts" 64 | f [x] = x | f (h :: t) = (h ++ f t) >> K (); 65in 66 val exact_puncts = f o map (fn c => exact (Punct, str c) >> K ()) o explode; 67end; 68 69val lexer = 70 (many (some space) ++ 71 (((some lower || some digit) ++ many (some alphanum) >> 72 (fn (a, b) => (Lower, implode (a :: b)))) || 73 (some upper ++ many (some alphanum) >> 74 (fn (a, b) => (Upper, implode (a :: b)))) || 75 ((some symbol || some punct) >> (fn c => (Punct, str c))))) >> snd; 76 77val lex = many lexer ++ (many (some space) ++ finished) >> fst; 78 79val input_toks = S.from_list o fst o lex; 80 81local 82 fun mapped (f,a) (m : rename list) = 83 let fun g {tptp, arity, fol = _} = tptp = f andalso arity = length a 84 in case List.find g m of SOME {fol, ...} => (fol, a) | NONE => (f, a) 85 end; 86in 87 fun Fn' A = Fn (mapped A (!renaming)); 88end; 89 90val var_parser = some (equal Upper o fst) >> snd; 91 92fun term_parser input = 93 ((var_parser >> Var) || 94 ((some (equal Lower o fst) >> snd) ++ 95 (optional 96 (exact (Punct, "(") ++ term_parser ++ 97 many ((exact (Punct, ",") ++ term_parser) >> snd) ++ 98 exact (Punct, ")")) >> 99 (fn SOME (_,(t,(ts,_))) => t :: ts | NONE => [])) >> 100 Fn')) input; 101 102val atom_parser = 103 term_parser >> (fn t => Atom (case t of Var v => Fn (v,[]) | _ => t)); 104 105val literal_parser = 106 (((exact_puncts "++" >> K true) || (exact_puncts "--" >> K false)) ++ 107 atom_parser) >> mk_literal; 108 109val clause_parser = 110 (exact (Lower, "input_clause") ++ exact (Punct, "(") ++ any ++ 111 exact (Punct, ",") ++ any ++ exact (Punct, ",") ++ exact (Punct, "[") ++ 112 literal_parser ++ many ((exact (Punct, ",") ++ literal_parser) >> snd) ++ 113 exact (Punct, "]") ++ exact (Punct, ")") ++ exact (Punct, ".")) >> 114 (fn (_,(_,(name,(_,(typ,(_,(_,(l,(ls,_))))))))) => 115 (snd name, snd typ, list_mk_disj (l :: ls))); 116 117val varl_parser = 118 (exact (Punct, "[") ++ var_parser ++ 119 many ((exact (Punct, ",") ++ var_parser) >> snd) ++ exact (Punct, "]")) >> 120 (fn (_,(h,(t,_))) => h :: t); 121 122fun form_parser inp = 123 (qform_parser ++ 124 (iform_parser "|" Or || 125 iform_parser "&" And || 126 iform_parser "<=>" Iff || 127 iform_parser "<~>" (Not o Iff) || 128 iform_parser "=>" Imp || 129 iform_parser "<=" (Imp o swap) || 130 iform_parser "~|" (Not o Or) || 131 iform_parser "~&" (Not o And) || 132 (nothing >> (fn () => I))) >> 133 (fn (a,f) => f a)) inp 134and iform_parser sym con inp = 135 (atleastone ((exact_puncts sym ++ qform_parser) >> snd) 136 >> (fn l => fn i => 137 let val x = rev (i :: l) in foldl con (hd x) (tl x) end)) inp 138and qform_parser inp = 139 (((exact (Punct, "~") ++ qform_parser) >> (Not o snd)) || 140 ((exact (Punct, "!") ++ varl_parser ++ exact (Punct, ":") ++ qform_parser) 141 >> (fn (_,(v,(_,b))) => list_mk_forall (v,b))) || 142 ((exact (Punct, "?") ++ varl_parser ++ exact (Punct, ":") ++ qform_parser) 143 >> (fn (_,(v,(_,b))) => list_mk_exists (v,b))) || 144 ((exact (Punct, "(") ++ form_parser ++ exact (Punct, ")")) 145 >> (fst o snd)) || 146 atom_parser) inp; 147 148val fof_parser = 149 (exact (Lower, "input_formula") ++ exact (Punct, "(") ++ any ++ 150 exact (Punct, ",") ++ any ++ exact (Punct, ",") ++ form_parser ++ 151 exact (Punct, ")") ++ exact (Punct, ".")) >> 152 (fn (_,(_,(name,(_,(typ,(_,(f,_))))))) => (snd name, snd typ, f)); 153 154datatype problem = CNF | FOF; 155 156val problem_parser = 157 fst o 158 (((many clause_parser ++ finished) >> (fn (a,_) => (CNF,a))) || 159 ((many fof_parser ++ finished) >> (fn (a,_) => (FOF,a)))); 160 161local 162 val to_form = list_mk_conj o map (fn (_,_,a) => generalize a); 163in 164 val input_problem = 165 (fn (CNF,(a,b)) => Imp (to_form a, Imp (to_form b, False)) 166 | (FOF,(a,b)) => Imp (to_form a, if null b then False else to_form b)) o 167 (I ## List.partition (not o equal "conjecture" o #2)) o 168 problem_parser; 169end; 170 171val read = input_problem o input_toks o input_chars o input_lines; 172 173(* Quick testing 174installPP mlibTerm.pp_formula; 175val num1 = read "../../test/NUM001-1.tptp"; 176val lcl9 = read "../../test/LCL009-1.tptp"; 177val set11 = read "../../test/SET011+3.fof"; 178*) 179 180(* ------------------------------------------------------------------------- *) 181(* Writing to a TPTP file in CNF format: pass in a formula and filename. *) 182(* ------------------------------------------------------------------------- *) 183 184local 185 val separator = 186 "%-------------------------------------" ^ 187 "-------------------------------------\n"; 188 189 fun name n = "% File : " ^ n ^ "\n"; 190 191 fun varify s = 192 case explode s of [] => raise Error "write_cnf: empty string variable" 193 | x :: xs => if Char.isUpper x then s else implode (Char.toUpper x :: xs); 194 195 fun funify r s = 196 let 197 fun g {fol, arity, tptp = _} = fol = s andalso arity = r 198 in 199 case List.find g (!renaming) of SOME {tptp, ...} => tptp 200 | NONE => 201 case explode s of [] => raise Error "write_cnf: empty string function" 202 | x :: y => if Char.isLower x then s else implode (Char.toLower x :: y) 203 end; 204 205 fun term pr = 206 let 207 fun tm (Var v) = pr (varify v) 208 | tm (Fn (f, l)) = (pr (funify (length l) f); tms l) 209 and tms [] = () 210 | tms (x :: y) = (pr "("; tm x; app (fn z => (pr ","; tm z)) y) 211 in 212 tm 213 end 214 215 fun literal pr (Not (Atom a)) = (pr "--"; term pr a) 216 | literal pr (Atom a) = (pr "++"; term pr a) 217 | literal _ _ = raise Error "write_cnf: not in CNF"; 218 219 fun clause pr ty (cl, n) = 220 let 221 val () = if n = 0 then () else pr "\n" 222 val () = pr ("input_clause(clause" ^ int_to_string n ^ "," ^ ty ^ ",\n") 223 val () = pr " ["; 224 val () = 225 case (strip_disj o snd o strip_forall) cl of [] => () 226 | x :: y => (literal pr x; app (fn z => (pr ",\n ";literal pr z)) y) 227 val () = pr "]).\n" 228 in 229 n + 1 230 end; 231in 232 fun write {filename = n} (Imp (a, Imp (b, False))) = 233 let 234 open TextIO 235 val h = openOut n 236 fun pr x = output (h, x) 237 val () = pr separator 238 val () = pr (name n) 239 val () = pr separator 240 val n = foldl (clause pr "hypothesis") 0 (strip_conj a) 241 val n = foldl (clause pr "conjecture") n (strip_conj b) 242 val () = assert (0 < n) (Error "write: no clauses") 243 val () = pr separator 244 val () = closeOut h 245 in 246 () 247 end 248 | write _ _ = raise Error "write: not in CNF format"; 249end; 250 251(* Quick testing 252val () = write num1 "../file"; 253*) 254 255(* ------------------------------------------------------------------------- *) 256(* Making TPTP formulas more palatable. *) 257(* ------------------------------------------------------------------------- *) 258 259local 260 fun cycle _ ([], _) = raise Bug "cycle" 261 | cycle f (h :: t, avoid) = 262 let val h' = f h avoid in (h', (t @ [h], h' :: avoid)) end; 263 264 exception Too_many_vars; 265 266 val vars = ["x", "y", "z", "v", "w"]; 267 268 val MAX_PRIME = 3 * length vars; 269 270 fun f _ True = True 271 | f _ False = False 272 | f (s,_,_) (Atom tm) = Atom (term_subst s tm) 273 | f x (Not a) = Not (f x a) 274 | f x (And (a,b)) = And (f x a, f x b) 275 | f x (Or (a,b)) = Or (f x a, f x b) 276 | f x (Iff (a,b)) = Iff (f x a, f x b) 277 | f x (Imp (a,b)) = Imp (f x a, f x b) 278 | f x (Forall (v,b)) = g x Forall v b 279 | f x (Exists (v,b)) = g x Exists v b 280 and g (_,0,_) _ _ _ = raise Too_many_vars 281 | g (s,n,x) quant v b = 282 let 283 val variant_fn = if 0 <= n then variant else variant_num 284 val n = n - 1 285 val (w,x) = cycle variant_fn x 286 val s = (v |-> Var w) ::> s 287 in 288 quant (w, f (s,n,x) b) 289 end; 290 291 val prettify1 = f (|<>|, MAX_PRIME, (vars, [])); 292 val prettify2 = f (|<>|, ~1, (vars, [])); 293in 294 fun prettify fm = prettify1 fm handle Too_many_vars => prettify2 fm; 295end; 296 297(* Quick testing 298installPP mlibTerm.pp_formula; 299val num1 = (prettify o read) "../../test/NUM001-1.tptp"; 300val lcl9 = (prettify o read) "../../test/LCL009-1.tptp"; 301val set11 = (prettify o read) "../../test/SET011+3.tptp"; 302*) 303 304end 305