src/HOL/Tools/Nitpick/kodkod.ML
changeset 35185 9b8f351cced6
parent 35079 592edca1dfb3
child 35187 3acab6c90d4a
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 11:20:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Feb 17 12:14:08 2010 +0100
     1.3 @@ -167,6 +167,7 @@
     1.4  
     1.5    val max_arity : int -> int
     1.6    val arity_of_rel_expr : rel_expr -> int
     1.7 +  val is_problem_trivially_false : problem -> bool
     1.8    val problems_equivalent : problem -> problem -> bool
     1.9    val solve_any_problem :
    1.10      bool -> Time.time option -> int -> int -> problem list -> outcome
    1.11 @@ -491,6 +492,10 @@
    1.12    | arity_of_decl (DeclSome ((n, _), _)) = n
    1.13    | arity_of_decl (DeclSet ((n, _), _)) = n
    1.14  
    1.15 +(* problem -> bool *)
    1.16 +fun is_problem_trivially_false ({formula = False, ...} : problem) = true
    1.17 +  | is_problem_trivially_false _ = false
    1.18 +
    1.19  (* string -> bool *)
    1.20  val is_relevant_setting = not o member (op =) ["solver", "delay"]
    1.21  
    1.22 @@ -1014,7 +1019,7 @@
    1.23      val indexed_problems = if j >= 0 then
    1.24                               [(j, nth problems j)]
    1.25                             else
    1.26 -                             filter (not_equal False o #formula o snd)
    1.27 +                             filter (is_problem_trivially_false o snd)
    1.28                                      (0 upto length problems - 1 ~~ problems)
    1.29      val triv_js = filter_out (AList.defined (op =) indexed_problems)
    1.30                               (0 upto length problems - 1)