(* Title: HOL/Tools/Nitpick/nitrox.ML
Author: Jasmin Blanchette, TU Muenchen
Copyright 2010, 2011
Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
*)
signature NITROX =
sig
val pick_nits_in_fof_file : string -> string
end;
structure Nitrox : NITROX =
struct
open ATP_Util
open ATP_Problem
open ATP_Proof
open Nitpick
open Nitpick_Isar
exception SYNTAX of string
val parse_keyword = Scan.this_string
fun parse_file_path (c :: ss) =
if c = "'" orelse c = "\"" then
ss |> chop_while (curry (op <>) c) |>> implode ||> tl
else
raise SYNTAX "invalid file path"
| parse_file_path [] = raise SYNTAX "invalid file path"
fun parse_include x =
let
val (file_name, rest) =
(parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
--| $$ ".") x
in
((), (file_name |> Path.explode |> File.read
|> strip_spaces true (K true)
|> raw_explode) @ rest)
end
val parse_fof_or_cnf =
(parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
Scan.many (not_equal ",") |-- $$ "," |--
(parse_keyword "axiom" || parse_keyword "definition"
|| parse_keyword "theorem" || parse_keyword "lemma"
|| parse_keyword "hypothesis" || parse_keyword "conjecture"
|| parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
--| $$ ")" --| $$ "."
>> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
val parse_problem =
Scan.repeat parse_include
|-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)
val parse_tptp_problem =
Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
parse_problem))
o raw_explode o strip_spaces true (K true)
val boolT = @{typ bool}
val iotaT = @{typ iota}
val quantT = (iotaT --> boolT) --> boolT
fun is_variable s = Char.isUpper (String.sub (s, 0))
fun hol_term_from_fo_term res_T (ATerm (x, us)) =
let val ts = map (hol_term_from_fo_term iotaT) us in
list_comb ((case x of
"$true" => @{const_name True}
| "$false" => @{const_name False}
| "=" => @{const_name HOL.eq}
| _ => x, map fastype_of ts ---> res_T)
|> (if is_variable x then Free else Const), ts)
end
fun hol_prop_from_formula phi =
case phi of
AQuant (_, [], phi') => hol_prop_from_formula phi'
| AQuant (q, (x, _) :: xs, phi') =>
Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
quantT)
$ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))
| AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
| AConn (c, [u1, u2]) =>
pairself hol_prop_from_formula (u1, u2)
|> (case c of
AAnd => HOLogic.mk_conj
| AOr => HOLogic.mk_disj
| AImplies => HOLogic.mk_imp
| AIf => HOLogic.mk_imp o swap
| AIff => HOLogic.mk_eq
| ANotIff => HOLogic.mk_not o HOLogic.mk_eq
| ANot => raise Fail "binary \"ANot\"")
| AConn _ => raise Fail "malformed AConn"
| AAtom u => hol_term_from_fo_term boolT u
fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t
fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
fun pick_nits_in_fof_file file_name =
case parse_tptp_problem (File.read (Path.explode file_name)) of
(_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
| (phis, []) =>
let
val ts = map (HOLogic.mk_Trueprop o close_hol_prop
o hol_prop_from_formula) phis
(*
val _ = warning (PolyML.makestring phis)
val _ = app (warning o Syntax.string_of_term @{context}) ts
*)
val state = Proof.init @{context}
val params =
[("card", "1\<emdash>8"),
("box", "false"),
("sat_solver", "smart"),
("max_threads", "1"),
("batch_size", "10"),
(* ("debug", "true"), *)
("verbose", "true"),
(* ("overlord", "true"), *)
("show_consts", "true"),
("format", "1000"),
("max_potential", "0"),
("timeout", "none"),
("expect", genuineN)]
|> default_params @{theory}
val i = 1
val n = 1
val step = 0
val subst = []
in
pick_nits_in_term state params Normal i n step subst ts @{prop False}
|> fst
end
end;