whitespace tuning
authorblanchet
Tue Oct 26 10:59:28 2010 +0200 (2010-10-26)
changeset 40146f2a14b6effcf
parent 40145 04a05b2a7a36
child 40147 d170c322157a
whitespace tuning
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 26 10:57:04 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Oct 26 10:59:28 2010 +0200
     1.3 @@ -505,29 +505,29 @@
     1.4    end
     1.5  
     1.6  fun solve max_var (lits, comps, sexps) =
     1.7 -    let
     1.8 -      fun do_assigns assigns =
     1.9 -        SOME (literals_from_assignments max_var assigns lits
    1.10 -              |> tap print_solution)
    1.11 -      val _ = print_problem lits comps sexps
    1.12 -      val prop = PropLogic.all (map prop_for_literal lits @
    1.13 -                                map prop_for_comp comps @
    1.14 -                                map prop_for_sign_expr sexps)
    1.15 -      val default_val = bool_from_sign Minus
    1.16 -    in
    1.17 -      if PropLogic.eval (K default_val) prop then
    1.18 -        do_assigns (K (SOME default_val))
    1.19 -      else
    1.20 -        let
    1.21 -          (* use the first ML solver (to avoid startup overhead) *)
    1.22 -          val solvers = !SatSolver.solvers
    1.23 -                        |> filter (member (op =) ["dptsat", "dpll"] o fst)
    1.24 -        in
    1.25 -          case snd (hd solvers) prop of
    1.26 -            SatSolver.SATISFIABLE assigns => do_assigns assigns
    1.27 -          | _ => NONE
    1.28 -        end
    1.29 -    end
    1.30 +  let
    1.31 +    fun do_assigns assigns =
    1.32 +      SOME (literals_from_assignments max_var assigns lits
    1.33 +            |> tap print_solution)
    1.34 +    val _ = print_problem lits comps sexps
    1.35 +    val prop = PropLogic.all (map prop_for_literal lits @
    1.36 +                              map prop_for_comp comps @
    1.37 +                              map prop_for_sign_expr sexps)
    1.38 +    val default_val = bool_from_sign Minus
    1.39 +  in
    1.40 +    if PropLogic.eval (K default_val) prop then
    1.41 +      do_assigns (K (SOME default_val))
    1.42 +    else
    1.43 +      let
    1.44 +        (* use the first ML solver (to avoid startup overhead) *)
    1.45 +        val solvers = !SatSolver.solvers
    1.46 +                      |> filter (member (op =) ["dptsat", "dpll"] o fst)
    1.47 +      in
    1.48 +        case snd (hd solvers) prop of
    1.49 +          SatSolver.SATISFIABLE assigns => do_assigns assigns
    1.50 +        | _ => NONE
    1.51 +      end
    1.52 +  end
    1.53  
    1.54  type mtype_schema = mtyp * constraint_set
    1.55  type mtype_context =