src/HOL/Tools/ATP/atp_systems.ML
changeset 43221 2c88166938eb
parent 43060 e998e85e41ff
child 43288 7a4eebdebb23
equal deleted inserted replaced
43220:a6bda1a47c0a 43221:2c88166938eb
   300    conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
   300    conj_sym_kind = Conjecture, (* FIXME: try out Hypothesis *)
   301    prem_kind = Conjecture,
   301    prem_kind = Conjecture,
   302    formats = [FOF],
   302    formats = [FOF],
   303    best_slices = fn ctxt =>
   303    best_slices = fn ctxt =>
   304      (* FUDGE *)
   304      (* FUDGE *)
   305      [(0.333, (false, (400, ["mangled_preds_heavy"]))) (* SOS *),
   305      [(0.333, (false, (200, ["mangled_preds_heavy"]))) (* SOS *),
   306       (0.333, (false, (400, ["mangled_tags?"]))) (* SOS *),
   306       (0.333, (false, (300, ["mangled_tags?"]))) (* SOS *),
   307       (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
   307       (0.334, (true, (400, ["poly_preds"]))) (* ~SOS *)]
   308      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   308      |> (if Config.get ctxt vampire_force_sos then hd #> apfst (K 1.0) #> single
   309          else I)}
   309          else I)}
   310 
   310 
   311 val vampire = (vampireN, vampire_config)
   311 val vampire = (vampireN, vampire_config)