make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
authorblanchet
Mon Nov 08 02:33:48 2010 +0100 (2010-11-08)
changeset 40419718b44dbd74d
parent 40418 8b73059e97a1
child 40420 552563ea3304
child 40421 b41aabb629ce
child 40426 339f56417109
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
src/HOL/Tools/Sledgehammer/sledgehammer.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 02:32:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 08 02:33:48 2010 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4      else is_atp_installed thy name
     1.5    end
     1.6  
     1.7 -val smt_default_max_relevant = 250 (* FUDGE (FIXME) *)
     1.8 +val smt_default_max_relevant = 200 (* FUDGE *)
     1.9  val auto_max_relevant_divisor = 2 (* FUDGE *)
    1.10  
    1.11  fun default_max_relevant_for_prover thy name =
    1.12 @@ -414,29 +414,43 @@
    1.13    | failure_from_smt_failure SMT_Solver.Out_Of_Memory = OutOfResources
    1.14    | failure_from_smt_failure _ = UnknownError
    1.15  
    1.16 -val smt_filter_max_iter = 5
    1.17 -val smt_filter_fact_divisor = 2
    1.18 +val smt_max_iter = 5
    1.19 +val smt_iter_fact_divisor = 2
    1.20 +val smt_iter_min_msecs = 5000
    1.21 +val smt_iter_timeout_divisor = 2
    1.22  
    1.23  fun smt_filter_loop iter outcome0 msecs_so_far remote timeout state facts i =
    1.24    let
    1.25      val timer = Timer.startRealTimer ()
    1.26 +    val ms = timeout |> Time.toMilliseconds
    1.27 +    val iter_timeout =
    1.28 +      if iter < smt_max_iter then
    1.29 +        Int.min (ms, Int.max (smt_iter_min_msecs,
    1.30 +                              ms div smt_iter_timeout_divisor))
    1.31 +        |> Time.fromMilliseconds
    1.32 +      else
    1.33 +        timeout
    1.34      val {outcome, used_facts, run_time_in_msecs} =
    1.35 -      SMT_Solver.smt_filter remote timeout state facts i
    1.36 +      TimeLimit.timeLimit iter_timeout
    1.37 +          (SMT_Solver.smt_filter remote iter_timeout state facts) i
    1.38 +      handle TimeLimit.TimeOut =>
    1.39 +             {outcome = SOME SMT_Solver.Time_Out, used_facts = [],
    1.40 +              run_time_in_msecs = NONE}
    1.41      val outcome0 = if is_none outcome0 then SOME outcome else outcome0
    1.42      val msecs_so_far = int_opt_add run_time_in_msecs msecs_so_far
    1.43      val too_many_facts_perhaps =
    1.44        case outcome of
    1.45          NONE => false
    1.46        | SOME (SMT_Solver.Counterexample _) => false
    1.47 -      | SOME SMT_Solver.Time_Out => false
    1.48 +      | SOME SMT_Solver.Time_Out => iter_timeout <> timeout
    1.49        | SOME SMT_Solver.Out_Of_Memory => true
    1.50        | SOME _ => true
    1.51 +    val timeout = Time.- (timeout, Timer.checkRealTimer timer)
    1.52    in
    1.53 -    if too_many_facts_perhaps andalso iter < smt_filter_max_iter andalso
    1.54 -       not (null facts) then
    1.55 -      let val facts = take (length facts div smt_filter_fact_divisor) facts in
    1.56 -        smt_filter_loop (iter + 1) outcome0 msecs_so_far remote
    1.57 -                        (Time.- (timeout, Timer.checkRealTimer timer)) state
    1.58 +    if too_many_facts_perhaps andalso iter < smt_max_iter andalso
    1.59 +       not (null facts) andalso timeout > Time.zeroTime then
    1.60 +      let val facts = take (length facts div smt_iter_fact_divisor) facts in
    1.61 +        smt_filter_loop (iter + 1) outcome0 msecs_so_far remote timeout state
    1.62                          facts i
    1.63        end
    1.64      else