added dummy_fof prover to Sledgehammer
authordesharna
Wed, 04 Aug 2021 08:23:12 +0200
changeset 74380 30ab39ab4117
parent 74379 5cd8b5cd0451
child 74381 a61e8cb998aa
child 74386 49884e54f13a
added dummy_fof prover to Sledgehammer
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 03 10:33:35 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 04 08:23:12 2021 +0200
@@ -54,6 +54,7 @@
   val z3_tptpN : string
   val zipperpositionN : string
   val remote_prefix : string
+  val dummy_fofN : string
   val dummy_tfxN : string
   val dummy_thfN : string
 
@@ -117,6 +118,7 @@
 val z3_tptpN = "z3_tptp"
 val zipperpositionN = "zipperposition"
 val remote_prefix = "remote_"
+val dummy_fofN = "dummy_fof"
 val dummy_tfxN = "dummy_tfx"
 val dummy_thfN = "dummy_thf"
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Aug 03 10:33:35 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Aug 04 08:23:12 2021 +0200
@@ -681,6 +681,11 @@
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
+
+val dummy_fof_format = FOF
+val dummy_fof_config = dummy_config Hypothesis dummy_fof_format "mono_guards??" false
+val dummy_fof = (dummy_fofN, fn () => dummy_fof_config)
+
 val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
 val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
 val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
@@ -725,7 +730,7 @@
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_waldmeister, remote_zipperposition, dummy_tfx, dummy_thf]
+   remote_waldmeister, remote_zipperposition, dummy_fof, dummy_tfx, dummy_thf]
 
 val _ = Theory.setup (fold add_atp atps)