src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 54308 1a87db1f3701
parent 53815 e8aa538e959e
child 54062 427380d5d1d7
equal deleted inserted replaced
54307:903ab115e9fd 54308:1a87db1f3701
   307 
   307 
   308       val launch_full_atps = launch_atps "ATP" NONE full_atps
   308       val launch_full_atps = launch_atps "ATP" NONE full_atps
   309 
   309 
   310       val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
   310       val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
   311 
   311 
   312       fun launch_atps_and_smt_solvers () =
   312       fun launch_atps_and_smt_solvers p =
   313         [launch_full_atps, launch_smts, launch_ueq_atps]
   313         [launch_full_atps, launch_smts, launch_ueq_atps]
   314         |> Par_List.map (fn f => ignore (f (unknownN, state)))
   314         |> Par_List.map (fn f => fst (f p))
   315         handle ERROR msg => (print ("Error: " ^ msg); error msg)
   315         handle ERROR msg => (print ("Error: " ^ msg); error msg)
   316 
   316 
   317       fun maybe f (accum as (outcome_code, _)) =
   317       fun maybe f (accum as (outcome_code, _)) =
   318         accum |> (mode = Normal orelse outcome_code <> someN) ? f
   318         accum |> (mode = Normal orelse outcome_code <> someN) ? f
   319     in
   319     in
   320       (unknownN, state)
   320       (unknownN, state)
   321       |> (if blocking then
   321       |> (if mode = Auto_Try then
   322             launch_full_atps
   322             launch_full_atps
   323             #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
   323           else if blocking then
   324           else
   324             launch_atps_and_smt_solvers #> max_outcome_code #> rpair state
   325             (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
   325           else
       
   326             (fn p => (Future.fork (tap (fn () => launch_atps_and_smt_solvers p)); p)))
   326       handle TimeLimit.TimeOut =>
   327       handle TimeLimit.TimeOut =>
   327              (print "Sledgehammer ran out of time."; (unknownN, state))
   328              (print "Sledgehammer ran out of time."; (unknownN, state))
   328     end
   329     end
   329     |> `(fn (outcome_code, _) => outcome_code = someN)
   330     |> `(fn (outcome_code, _) => outcome_code = someN)
   330 
   331