better error message in Refute when specifying a non-existing SAT solver
authorblanchet
Mon Dec 07 11:44:49 2009 +0100 (2009-12-07)
changeset 34017ef2776c89799
parent 34015 5426ada71790
child 34018 39f21f7bad7e
better error message in Refute when specifying a non-existing SAT solver
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Mon Dec 07 09:35:18 2009 +0100
     1.2 +++ b/src/HOL/Tools/refute.ML	Mon Dec 07 11:44:49 2009 +0100
     1.3 @@ -1192,9 +1192,15 @@
     1.4          val fm_u  = (if negate then toFalse else toTrue) (hd intrs)
     1.5          val fm_ax = PropLogic.all (map toTrue (tl intrs))
     1.6          val fm    = PropLogic.all [#wellformed args, fm_ax, fm_u]
     1.7 +        val solver =
     1.8 +          SatSolver.invoke_solver satsolver
     1.9 +          handle Option.Option =>
    1.10 +                 error ("Unknown SAT solver: " ^ quote satsolver ^
    1.11 +                        ". Available solvers: " ^
    1.12 +                        commas (map (quote o fst) (!SatSolver.solvers)) ^ ".")
    1.13        in
    1.14          priority "Invoking SAT solver...";
    1.15 -        (case SatSolver.invoke_solver satsolver fm of
    1.16 +        (case solver fm of
    1.17            SatSolver.SATISFIABLE assignment =>
    1.18            (priority ("*** Model found: ***\n" ^ print_model thy model
    1.19              (fn i => case assignment i of SOME b => b | NONE => true));