src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 34123 c4988215a691
parent 34121 5e831d805118
child 34936 c4f04bee79f3
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 12:31:00 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 16:48:49 2009 +0100
     1.3 @@ -466,11 +466,11 @@
     1.4      PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
     1.5  
     1.6  (* var -> (int -> bool option) -> literal list -> literal list *)
     1.7 -fun literals_from_assignments max_var asgns lits =
     1.8 +fun literals_from_assignments max_var assigns lits =
     1.9    fold (fn x => fn accum =>
    1.10             if AList.defined (op =) lits x then
    1.11               accum
    1.12 -           else case asgns x of
    1.13 +           else case assigns x of
    1.14               SOME b => (x, sign_from_bool b) :: accum
    1.15             | NONE => accum) (max_var downto 1) lits
    1.16  
    1.17 @@ -505,10 +505,13 @@
    1.18        val prop = PropLogic.all (map prop_for_literal lits @
    1.19                                  map prop_for_comp comps @
    1.20                                  map prop_for_sign_expr sexps)
    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 SatSolver.invoke_solver "dpll" prop of
    1.26 -        SatSolver.SATISFIABLE asgns =>
    1.27 -        SOME (literals_from_assignments max_var asgns lits
    1.28 +      case snd (hd solvers) prop of
    1.29 +        SatSolver.SATISFIABLE assigns =>
    1.30 +        SOME (literals_from_assignments max_var assigns lits
    1.31                |> tap print_solution)
    1.32        | _ => NONE
    1.33      end