equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/Nitpick/nitrox.ML |
1 (* Title: HOL/Tools/Nitpick/nitrox.ML |
2 Author: Jasmin Blanchette, TU Muenchen |
2 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2010, 2011 |
3 Copyright 2010, 2011 |
4 |
4 |
5 Finite model generation for TPTP first-order formulas via Nitpick. |
5 Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick. |
6 *) |
6 *) |
7 |
7 |
8 signature NITROX = |
8 signature NITROX = |
9 sig |
9 sig |
10 val pick_nits_in_fof_file : string -> string |
10 val pick_nits_in_fof_file : string -> string |
180 val _ = warning (PolyML.makestring phis) |
180 val _ = warning (PolyML.makestring phis) |
181 val _ = app (warning o Syntax.string_of_term @{context}) ts |
181 val _ = app (warning o Syntax.string_of_term @{context}) ts |
182 *) |
182 *) |
183 val state = Proof.init @{context} |
183 val state = Proof.init @{context} |
184 val params = |
184 val params = |
185 [("card iota", "1\<midarrow>100"), |
185 [("card", "1\<emdash>8"), |
186 ("card", "1\<midarrow>8"), |
|
187 ("box", "false"), |
186 ("box", "false"), |
188 ("sat_solver", "smart"), |
187 ("sat_solver", "smart"), |
189 ("max_threads", "1"), |
188 ("max_threads", "1"), |
190 ("batch_size", "10"), |
189 ("batch_size", "10"), |
191 (* ("debug", "true"), *) |
190 (* ("debug", "true"), *) |